@@ -32,6 +32,7 @@ import (
3232 m_Sorting "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/Sorting"
3333 m_StandardLibrary "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary"
3434 m_StandardLibraryInterop "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibraryInterop"
35+ m_StandardLibrary_MemoryMath "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_MemoryMath"
3536 m_StandardLibrary_Sequence "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_Sequence"
3637 m_StandardLibrary_String "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_String"
3738 m_StandardLibrary_UInt "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_UInt"
@@ -73,6 +74,7 @@ var _ m_Power.Dummy__
7374var _ m_Logarithm.Dummy__
7475var _ m_StandardLibraryInterop.Dummy__
7576var _ m_StandardLibrary_UInt.Dummy__
77+ var _ m_StandardLibrary_MemoryMath.Dummy__
7678var _ m_StandardLibrary_Sequence.Dummy__
7779var _ m_StandardLibrary_String.Dummy__
7880var _ m_StandardLibrary.Dummy__
@@ -126,14 +128,14 @@ func (_static *CompanionStruct_Default___) DeterministicMap(action Deterministic
126128 var _0_rs _dafny.Sequence
127129 _ = _0_rs
128130 _0_rs = _dafny .SeqOf ()
129- var _hi0 _dafny. Int = _dafny . IntOfUint32 ((s ).Cardinality ())
131+ var _hi0 uint64 = uint64 ((s ).Cardinality ())
130132 _ = _hi0
131- for _1_i := _dafny . Zero ; _1_i . Cmp ( _hi0 ) < 0 ; _1_i = _1_i . Plus ( _dafny . One ) {
133+ for _1_i := uint64 ( 0 ) ; _1_i < _hi0 ; _1_i ++ {
132134 var _2_r interface {}
133135 _ = _2_r
134136 var _out0 interface {}
135137 _ = _out0
136- _out0 = (action ).Invoke ((s ).Select ((_1_i ). Uint32 ( )).(interface {}))
138+ _out0 = (action ).Invoke ((s ).Select (uint32 (_1_i )).(interface {}))
137139 _2_r = _out0
138140 _0_rs = _dafny .Companion_Sequence_ .Concatenate (_0_rs , _dafny .SeqOf (_2_r ))
139141 }
@@ -147,14 +149,14 @@ func (_static *CompanionStruct_Default___) DeterministicMapWithResult(action Det
147149 var _0_rs _dafny.Sequence
148150 _ = _0_rs
149151 _0_rs = _dafny .SeqOf ()
150- var _hi0 _dafny. Int = _dafny . IntOfUint32 ((s ).Cardinality ())
152+ var _hi0 uint64 = uint64 ((s ).Cardinality ())
151153 _ = _hi0
152- for _1_i := _dafny . Zero ; _1_i . Cmp ( _hi0 ) < 0 ; _1_i = _1_i . Plus ( _dafny . One ) {
154+ for _1_i := uint64 ( 0 ) ; _1_i < _hi0 ; _1_i ++ {
153155 var _2_valueOrError0 m_Wrappers.Result = m_Wrappers.Result {}
154156 _ = _2_valueOrError0
155157 var _out0 interface {}
156158 _ = _out0
157- _out0 = (action ).Invoke ((s ).Select ((_1_i ). Uint32 ( )).(interface {}))
159+ _out0 = (action ).Invoke ((s ).Select (uint32 (_1_i )).(interface {}))
158160 _2_valueOrError0 = _out0 .(m_Wrappers.Result )
159161 if (_2_valueOrError0 ).IsFailure () {
160162 res = (_2_valueOrError0 ).PropagateFailure ()
@@ -175,14 +177,14 @@ func (_static *CompanionStruct_Default___) DeterministicFlatMap(action Determini
175177 var _0_rs _dafny.Sequence
176178 _ = _0_rs
177179 _0_rs = _dafny .SeqOf ()
178- var _hi0 _dafny. Int = _dafny . IntOfUint32 ((s ).Cardinality ())
180+ var _hi0 uint64 = uint64 ((s ).Cardinality ())
179181 _ = _hi0
180- for _1_i := _dafny . Zero ; _1_i . Cmp ( _hi0 ) < 0 ; _1_i = _1_i . Plus ( _dafny . One ) {
182+ for _1_i := uint64 ( 0 ) ; _1_i < _hi0 ; _1_i ++ {
181183 var _2_r _dafny.Sequence
182184 _ = _2_r
183185 var _out0 interface {}
184186 _ = _out0
185- _out0 = (action ).Invoke ((s ).Select ((_1_i ). Uint32 ( )).(interface {}))
187+ _out0 = (action ).Invoke ((s ).Select (uint32 (_1_i )).(interface {}))
186188 _2_r = _out0 .(_dafny.Sequence )
187189 _0_rs = _dafny .Companion_Sequence_ .Concatenate (_0_rs , _2_r )
188190 }
@@ -196,14 +198,14 @@ func (_static *CompanionStruct_Default___) DeterministicFlatMapWithResult(action
196198 var _0_rs _dafny.Sequence
197199 _ = _0_rs
198200 _0_rs = _dafny .SeqOf ()
199- var _hi0 _dafny. Int = _dafny . IntOfUint32 ((s ).Cardinality ())
201+ var _hi0 uint64 = uint64 ((s ).Cardinality ())
200202 _ = _hi0
201- for _1_i := _dafny . Zero ; _1_i . Cmp ( _hi0 ) < 0 ; _1_i = _1_i . Plus ( _dafny . One ) {
203+ for _1_i := uint64 ( 0 ) ; _1_i < _hi0 ; _1_i ++ {
202204 var _2_valueOrError0 m_Wrappers.Result = m_Wrappers .Companion_Result_ .Default (_dafny .EmptySeq )
203205 _ = _2_valueOrError0
204206 var _out0 interface {}
205207 _ = _out0
206- _out0 = (action ).Invoke ((s ).Select ((_1_i ). Uint32 ( )).(interface {}))
208+ _out0 = (action ).Invoke ((s ).Select (uint32 (_1_i )).(interface {}))
207209 _2_valueOrError0 = _out0 .(m_Wrappers.Result )
208210 if (_2_valueOrError0 ).IsFailure () {
209211 res = (_2_valueOrError0 ).PropagateFailure ()
@@ -226,17 +228,17 @@ func (_static *CompanionStruct_Default___) Filter(action DeterministicAction, s
226228 var _0_rs _dafny.Sequence
227229 _ = _0_rs
228230 _0_rs = _dafny .SeqOf ()
229- var _hi0 _dafny. Int = _dafny . IntOfUint32 ((s ).Cardinality ())
231+ var _hi0 uint64 = uint64 ((s ).Cardinality ())
230232 _ = _hi0
231- for _1_i := _dafny . Zero ; _1_i . Cmp ( _hi0 ) < 0 ; _1_i = _1_i . Plus ( _dafny . One ) {
233+ for _1_i := uint64 ( 0 ) ; _1_i < _hi0 ; _1_i ++ {
232234 var _2_r bool
233235 _ = _2_r
234236 var _out0 interface {}
235237 _ = _out0
236- _out0 = (action ).Invoke ((s ).Select ((_1_i ). Uint32 ( )).(interface {}))
238+ _out0 = (action ).Invoke ((s ).Select (uint32 (_1_i )).(interface {}))
237239 _2_r = _out0 .(bool )
238240 if _2_r {
239- _0_rs = _dafny .Companion_Sequence_ .Concatenate (_0_rs , _dafny .SeqOf ((s ).Select ((_1_i ). Uint32 ( )).(interface {})))
241+ _0_rs = _dafny .Companion_Sequence_ .Concatenate (_0_rs , _dafny .SeqOf ((s ).Select (uint32 (_1_i )).(interface {})))
240242 }
241243 }
242244 res = _0_rs
@@ -249,14 +251,14 @@ func (_static *CompanionStruct_Default___) FilterWithResult(action Deterministic
249251 var _0_rs _dafny.Sequence
250252 _ = _0_rs
251253 _0_rs = _dafny .SeqOf ()
252- var _hi0 _dafny. Int = _dafny . IntOfUint32 ((s ).Cardinality ())
254+ var _hi0 uint64 = uint64 ((s ).Cardinality ())
253255 _ = _hi0
254- for _1_i := _dafny . Zero ; _1_i . Cmp ( _hi0 ) < 0 ; _1_i = _1_i . Plus ( _dafny . One ) {
256+ for _1_i := uint64 ( 0 ) ; _1_i < _hi0 ; _1_i ++ {
255257 var _2_valueOrError0 m_Wrappers.Result = m_Wrappers .Companion_Result_ .Default (false )
256258 _ = _2_valueOrError0
257259 var _out0 interface {}
258260 _ = _out0
259- _out0 = (action ).Invoke ((s ).Select ((_1_i ). Uint32 ( )).(interface {}))
261+ _out0 = (action ).Invoke ((s ).Select (uint32 (_1_i )).(interface {}))
260262 _2_valueOrError0 = _out0 .(m_Wrappers.Result )
261263 if (_2_valueOrError0 ).IsFailure () {
262264 res = (_2_valueOrError0 ).PropagateFailure ()
@@ -266,7 +268,7 @@ func (_static *CompanionStruct_Default___) FilterWithResult(action Deterministic
266268 _ = _3_r
267269 _3_r = (_2_valueOrError0 ).Extract ().(bool )
268270 if _3_r {
269- _0_rs = _dafny .Companion_Sequence_ .Concatenate (_0_rs , _dafny .SeqOf ((s ).Select ((_1_i ). Uint32 ( )).(interface {})))
271+ _0_rs = _dafny .Companion_Sequence_ .Concatenate (_0_rs , _dafny .SeqOf ((s ).Select (uint32 (_1_i )).(interface {})))
270272 }
271273 }
272274 res = m_Wrappers .Companion_Result_ .Create_Success_ (_0_rs )
@@ -279,14 +281,14 @@ func (_static *CompanionStruct_Default___) ReduceToSuccess(action ActionWithResu
279281 var _0_attemptedResults _dafny.Sequence
280282 _ = _0_attemptedResults
281283 _0_attemptedResults = _dafny .SeqOf ()
282- var _hi0 _dafny. Int = _dafny . IntOfUint32 ((s ).Cardinality ())
284+ var _hi0 uint64 = uint64 ((s ).Cardinality ())
283285 _ = _hi0
284- for _1_i := _dafny . Zero ; _1_i . Cmp ( _hi0 ) < 0 ; _1_i = _1_i . Plus ( _dafny . One ) {
286+ for _1_i := uint64 ( 0 ) ; _1_i < _hi0 ; _1_i ++ {
285287 var _2_attempt m_Wrappers.Result
286288 _ = _2_attempt
287289 var _out0 interface {}
288290 _ = _out0
289- _out0 = (action ).Invoke ((s ).Select ((_1_i ). Uint32 ( )).(interface {}))
291+ _out0 = (action ).Invoke ((s ).Select (uint32 (_1_i )).(interface {}))
290292 _2_attempt = _out0 .(m_Wrappers.Result )
291293 _0_attemptedResults = _dafny .Companion_Sequence_ .Concatenate (_0_attemptedResults , _dafny .SeqOf (_2_attempt ))
292294 if (_2_attempt ).Is_Success () {
@@ -296,13 +298,13 @@ func (_static *CompanionStruct_Default___) ReduceToSuccess(action ActionWithResu
296298 return res
297299 }
298300 }
299- res = m_Wrappers .Companion_Result_ .Create_Failure_ (m_Seq .Companion_Default___ .Map (func (coer29 func (m_Wrappers.Result ) interface {}) func (interface {}) interface {} {
300- return func (arg33 interface {}) interface {} {
301- return coer29 ( arg33 .(m_Wrappers.Result ))
301+ res = m_Wrappers .Companion_Result_ .Create_Failure_ (m_Seq .Companion_Default___ .Map (func (coer26 func (m_Wrappers.Result ) interface {}) func (interface {}) interface {} {
302+ return func (arg29 interface {}) interface {} {
303+ return coer26 ( arg29 .(m_Wrappers.Result ))
302304 }
303- }(func (coer30 func (m_Wrappers.Result ) interface {}) func (m_Wrappers.Result ) interface {} {
304- return func (arg34 m_Wrappers.Result ) interface {} {
305- return coer30 ( arg34 )
305+ }(func (coer27 func (m_Wrappers.Result ) interface {}) func (m_Wrappers.Result ) interface {} {
306+ return func (arg30 m_Wrappers.Result ) interface {} {
307+ return coer27 ( arg30 )
306308 }
307309 }(Companion_Default___ .PluckErrors )), _0_attemptedResults ))
308310 return res
0 commit comments