@@ -46,6 +46,7 @@ import (
4646 m_Sorting "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/Sorting"
4747 m_StandardLibrary "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary"
4848 m_StandardLibraryInterop "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibraryInterop"
49+ m_StandardLibrary_MemoryMath "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_MemoryMath"
4950 m_StandardLibrary_Sequence "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_Sequence"
5051 m_StandardLibrary_String "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_String"
5152 m_StandardLibrary_UInt "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_UInt"
@@ -66,6 +67,7 @@ var _ m__System.Dummy__
6667var _ m_Wrappers.Dummy__
6768var _ m_BoundedInts.Dummy__
6869var _ m_StandardLibrary_UInt.Dummy__
70+ var _ m_StandardLibrary_MemoryMath.Dummy__
6971var _ m_StandardLibrary_Sequence.Dummy__
7072var _ m_StandardLibrary_String.Dummy__
7173var _ m_StandardLibrary.Dummy__
@@ -158,27 +160,29 @@ func (_static *CompanionStruct_Default___) ValidAwsKmsArn(arn AwsArn) bool {
158160func (_static * CompanionStruct_Default___ ) ParseAwsKmsRawResources (identifier _dafny.Sequence ) m_Wrappers.Result {
159161 var _0_info _dafny.Sequence = m_StandardLibrary .Companion_Default___ .Split (identifier , _dafny .Char ('/' ))
160162 _ = _0_info
161- var _1_valueOrError0 m_Wrappers.Outcome = m_Wrappers .Companion_Default___ .Need (! _dafny .Companion_Sequence_ .Equal ((_0_info ).Select (0 ).(_dafny.Sequence ), _dafny .SeqOfString ("key" )), _dafny .Companion_Sequence_ .Concatenate (_dafny .SeqOfString ("Malformed raw key id: " ), identifier ))
163+ var _1_valueOrError0 m_Wrappers.Outcome = m_Wrappers .Companion_Default___ .Need (! _dafny .Companion_Sequence_ .Equal ((_0_info ).Select (uint32 ( uint32 ( 0 )) ).(_dafny.Sequence ), _dafny .SeqOfString ("key" )), _dafny .Companion_Sequence_ .Concatenate (_dafny .SeqOfString ("Malformed raw key id: " ), identifier ))
162164 _ = _1_valueOrError0
163165 if (_1_valueOrError0 ).IsFailure () {
164166 return (_1_valueOrError0 ).PropagateFailure ()
165- } else if (_dafny .IntOfUint32 ((_0_info ).Cardinality ())).Cmp (_dafny .One ) == 0 {
166- return Companion_Default___ .ParseAwsKmsResources (_dafny .Companion_Sequence_ .Concatenate (_dafny .SeqOfString ("key/" ), identifier ))
167167 } else {
168- return Companion_Default___ .ParseAwsKmsResources (identifier )
168+ if (uint64 ((_0_info ).Cardinality ())) == (uint64 (1 )) {
169+ return Companion_Default___ .ParseAwsKmsResources (_dafny .Companion_Sequence_ .Concatenate (_dafny .SeqOfString ("key/" ), identifier ))
170+ } else {
171+ return Companion_Default___ .ParseAwsKmsResources (identifier )
172+ }
169173 }
170174}
171175func (_static * CompanionStruct_Default___ ) ParseAwsKmsResources (identifier _dafny.Sequence ) m_Wrappers.Result {
172176 var _0_info _dafny.Sequence = m_StandardLibrary .Companion_Default___ .Split (identifier , _dafny .Char ('/' ))
173177 _ = _0_info
174- var _1_valueOrError0 m_Wrappers.Outcome = m_Wrappers .Companion_Default___ .Need ((_dafny . IntOfUint32 ((_0_info ).Cardinality ())). Cmp ( _dafny . One ) > 0 , _dafny .Companion_Sequence_ .Concatenate (_dafny .SeqOfString ("Malformed resource: " ), identifier ))
178+ var _1_valueOrError0 m_Wrappers.Outcome = m_Wrappers .Companion_Default___ .Need ((uint64 ((_0_info ).Cardinality ())) > ( uint64 ( 1 )) , _dafny .Companion_Sequence_ .Concatenate (_dafny .SeqOfString ("Malformed resource: " ), identifier ))
175179 _ = _1_valueOrError0
176180 if (_1_valueOrError0 ).IsFailure () {
177181 return (_1_valueOrError0 ).PropagateFailure ()
178182 } else {
179- var _2_resourceType _dafny.Sequence = (_0_info ).Select (0 ).(_dafny.Sequence )
183+ var _2_resourceType _dafny.Sequence = (_0_info ).Select (uint32 ( uint32 ( 0 )) ).(_dafny.Sequence )
180184 _ = _2_resourceType
181- var _3_value _dafny.Sequence = m_StandardLibrary .Companion_Default___ .Join ((_0_info ).Drop (1 ), _dafny .SeqOfString ("/" ))
185+ var _3_value _dafny.Sequence = m_StandardLibrary .Companion_Default___ .Join ((_0_info ).Drop (uint32 ( uint32 ( 1 )) ), _dafny .SeqOfString ("/" ))
182186 _ = _3_value
183187 var _4_resource AwsResource = Companion_AwsResource_ .Create_AwsResource_ (_2_resourceType , _3_value )
184188 _ = _4_resource
@@ -229,19 +233,19 @@ func (_static *CompanionStruct_Default___) ParseAmazonDynamodbResources(identifi
229233func (_static * CompanionStruct_Default___ ) ParseAwsKmsArn (identifier _dafny.Sequence ) m_Wrappers.Result {
230234 var _0_components _dafny.Sequence = m_StandardLibrary .Companion_Default___ .Split (identifier , _dafny .Char (':' ))
231235 _ = _0_components
232- var _1_valueOrError0 m_Wrappers.Outcome = m_Wrappers .Companion_Default___ .Need ((_dafny . IntOfInt64 (6 )). Cmp ( _dafny . IntOfUint32 ((_0_components ).Cardinality ())) == 0 , _dafny .Companion_Sequence_ .Concatenate (_dafny .SeqOfString ("Malformed arn: " ), identifier ))
236+ var _1_valueOrError0 m_Wrappers.Outcome = m_Wrappers .Companion_Default___ .Need ((uint64 (6 )) == ( uint64 ((_0_components ).Cardinality ())), _dafny .Companion_Sequence_ .Concatenate (_dafny .SeqOfString ("Malformed arn: " ), identifier ))
233237 _ = _1_valueOrError0
234238 if (_1_valueOrError0 ).IsFailure () {
235239 return (_1_valueOrError0 ).PropagateFailure ()
236240 } else {
237- var _2_valueOrError1 m_Wrappers.Result = Companion_Default___ .ParseAwsKmsResources ((_0_components ).Select (5 ).(_dafny.Sequence ))
241+ var _2_valueOrError1 m_Wrappers.Result = Companion_Default___ .ParseAwsKmsResources ((_0_components ).Select (uint32 ( uint32 ( 5 )) ).(_dafny.Sequence ))
238242 _ = _2_valueOrError1
239243 if (_2_valueOrError1 ).IsFailure () {
240244 return (_2_valueOrError1 ).PropagateFailure ()
241245 } else {
242246 var _3_resource AwsResource = (_2_valueOrError1 ).Extract ().(AwsResource )
243247 _ = _3_resource
244- var _4_arn AwsArn = Companion_AwsArn_ .Create_AwsArn_ ((_0_components ).Select (0 ) .(_dafny.Sequence ), (_0_components ).Select (1 ) .(_dafny.Sequence ), (_0_components ).Select (2 ) .(_dafny.Sequence ), (_0_components ).Select (3 ) .(_dafny.Sequence ), (_0_components ).Select (4 ).(_dafny.Sequence ), _3_resource )
248+ var _4_arn AwsArn = Companion_AwsArn_ .Create_AwsArn_ ((_0_components ).Select (uint32 ( uint32 ( 0 ))) .(_dafny.Sequence ), (_0_components ).Select (uint32 ( uint32 ( 1 ))) .(_dafny.Sequence ), (_0_components ).Select (uint32 ( uint32 ( 2 ))) .(_dafny.Sequence ), (_0_components ).Select (uint32 ( uint32 ( 3 ))) .(_dafny.Sequence ), (_0_components ).Select (uint32 ( uint32 ( 4 )) ).(_dafny.Sequence ), _3_resource )
245249 _ = _4_arn
246250 var _5_valueOrError2 m_Wrappers.Outcome = m_Wrappers .Companion_Default___ .Need (Companion_Default___ .ValidAwsKmsArn (_4_arn ), _dafny .Companion_Sequence_ .Concatenate (_dafny .SeqOfString ("Malformed Arn:" ), identifier ))
247251 _ = _5_valueOrError2
@@ -256,19 +260,19 @@ func (_static *CompanionStruct_Default___) ParseAwsKmsArn(identifier _dafny.Sequ
256260func (_static * CompanionStruct_Default___ ) ParseAmazonDynamodbTableArn (identifier _dafny.Sequence ) m_Wrappers.Result {
257261 var _0_components _dafny.Sequence = m_StandardLibrary .Companion_Default___ .Split (identifier , _dafny .Char (':' ))
258262 _ = _0_components
259- var _1_valueOrError0 m_Wrappers.Outcome = m_Wrappers .Companion_Default___ .Need ((_dafny . IntOfInt64 (6 )). Cmp ( _dafny . IntOfUint32 ((_0_components ).Cardinality ())) == 0 , _dafny .Companion_Sequence_ .Concatenate (_dafny .SeqOfString ("Malformed arn: " ), identifier ))
263+ var _1_valueOrError0 m_Wrappers.Outcome = m_Wrappers .Companion_Default___ .Need ((uint64 (6 )) == ( uint64 ((_0_components ).Cardinality ())), _dafny .Companion_Sequence_ .Concatenate (_dafny .SeqOfString ("Malformed arn: " ), identifier ))
260264 _ = _1_valueOrError0
261265 if (_1_valueOrError0 ).IsFailure () {
262266 return (_1_valueOrError0 ).PropagateFailure ()
263267 } else {
264- var _2_valueOrError1 m_Wrappers.Result = Companion_Default___ .ParseAmazonDynamodbResources ((_0_components ).Select (5 ).(_dafny.Sequence ))
268+ var _2_valueOrError1 m_Wrappers.Result = Companion_Default___ .ParseAmazonDynamodbResources ((_0_components ).Select (uint32 ( uint32 ( 5 )) ).(_dafny.Sequence ))
265269 _ = _2_valueOrError1
266270 if (_2_valueOrError1 ).IsFailure () {
267271 return (_2_valueOrError1 ).PropagateFailure ()
268272 } else {
269273 var _3_resource AwsResource = (_2_valueOrError1 ).Extract ().(AwsResource )
270274 _ = _3_resource
271- var _4_arn AwsArn = Companion_AwsArn_ .Create_AwsArn_ ((_0_components ).Select (0 ) .(_dafny.Sequence ), (_0_components ).Select (1 ) .(_dafny.Sequence ), (_0_components ).Select (2 ) .(_dafny.Sequence ), (_0_components ).Select (3 ) .(_dafny.Sequence ), (_0_components ).Select (4 ).(_dafny.Sequence ), _3_resource )
275+ var _4_arn AwsArn = Companion_AwsArn_ .Create_AwsArn_ ((_0_components ).Select (uint32 ( uint32 ( 0 ))) .(_dafny.Sequence ), (_0_components ).Select (uint32 ( uint32 ( 1 ))) .(_dafny.Sequence ), (_0_components ).Select (uint32 ( uint32 ( 2 ))) .(_dafny.Sequence ), (_0_components ).Select (uint32 ( uint32 ( 3 ))) .(_dafny.Sequence ), (_0_components ).Select (uint32 ( uint32 ( 4 )) ).(_dafny.Sequence ), _3_resource )
272276 _ = _4_arn
273277 var _5_valueOrError2 m_Wrappers.Outcome = m_Wrappers .Companion_Default___ .Need (Companion_Default___ .ValidAmazonDynamodbArn (_4_arn ), _dafny .Companion_Sequence_ .Concatenate (_dafny .SeqOfString ("Malformed Arn:" ), identifier ))
274278 _ = _5_valueOrError2
@@ -360,7 +364,7 @@ func (_static *CompanionStruct_Default___) IsAwsKmsIdentifierString(s _dafny.Seq
360364 if (_0_valueOrError0 ).IsFailure () {
361365 return (_0_valueOrError0 ).PropagateFailure ()
362366 } else {
363- var _1_valueOrError1 m_Wrappers.Outcome = m_Wrappers .Companion_Default___ .Need (((_dafny . IntOfUint32 (( s ).Cardinality ())). Sign () == 1 ) && ((_dafny . IntOfUint32 ((s ).Cardinality ())). Cmp (Companion_Default___ .MAX__AWS__KMS__IDENTIFIER__LENGTH ()) <= 0 ), _dafny .SeqOfString ("Identifier exceeds maximum length." ))
367+ var _1_valueOrError1 m_Wrappers.Outcome = m_Wrappers .Companion_Default___ .Need (((uint64 ( 0 )) < ( uint64 (( s ).Cardinality ()))) && ((uint64 ((s ).Cardinality ())) <= (Companion_Default___ .MAX__AWS__KMS__IDENTIFIER__LENGTH ())), _dafny .SeqOfString ("Identifier exceeds maximum length." ))
364368 _ = _1_valueOrError1
365369 if (_1_valueOrError1 ).IsFailure () {
366370 return (_1_valueOrError1 ).PropagateFailure ()
@@ -399,8 +403,8 @@ func (_static *CompanionStruct_Default___) ValidateDdbTableArn(tableArn _dafny.S
399403 }
400404 }
401405}
402- func (_static * CompanionStruct_Default___ ) MAX__AWS__KMS__IDENTIFIER__LENGTH () _dafny. Int {
403- return _dafny . IntOfInt64 (2048 )
406+ func (_static * CompanionStruct_Default___ ) MAX__AWS__KMS__IDENTIFIER__LENGTH () uint64 {
407+ return uint64 (2048 )
404408}
405409
406410// End of class Default__
@@ -507,7 +511,7 @@ var _ _dafny.TraitOffspring = AwsResource{}
507511
508512func (_this AwsResource ) Valid () bool {
509513 {
510- return (true ) && ((_dafny . IntOfUint32 ((( _this ).Dtor_value ()).Cardinality ())). Sign () == 1 )
514+ return (true ) && ((uint64 ( 0 )) < ( uint64 ((( _this ).Dtor_value ()).Cardinality ())))
511515 }
512516}
513517func (_this AwsResource ) ToString () _dafny.Sequence {
@@ -640,7 +644,7 @@ var _ _dafny.TraitOffspring = AwsArn{}
640644
641645func (_this AwsArn ) Valid () bool {
642646 {
643- return (((((_dafny .Companion_Sequence_ .Equal ((_this ).Dtor_arnLiteral (), _dafny .SeqOfString ("arn" ))) && ((_dafny . IntOfUint32 ((( _this ).Dtor_partition ()).Cardinality ())). Sign () == 1 )) && ((_dafny . IntOfUint32 ((( _this ).Dtor_service ()).Cardinality ())). Sign () == 1 )) && ((_dafny . IntOfUint32 ((( _this ).Dtor_region ()).Cardinality ())). Sign () == 1 )) && ((_dafny . IntOfUint32 ((( _this ).Dtor_account ()).Cardinality ())). Sign () == 1 )) && (((_this ).Dtor_resource ()).Valid ())
647+ return (((((_dafny .Companion_Sequence_ .Equal ((_this ).Dtor_arnLiteral (), _dafny .SeqOfString ("arn" ))) && ((uint64 ( 0 )) < ( uint64 ((( _this ).Dtor_partition ()).Cardinality ())))) && ((uint64 ( 0 )) < ( uint64 ((( _this ).Dtor_service ()).Cardinality ())))) && ((uint64 ( 0 )) < ( uint64 ((( _this ).Dtor_region ()).Cardinality ())))) && ((uint64 ( 0 )) < ( uint64 ((( _this ).Dtor_account ()).Cardinality ())))) && (((_this ).Dtor_resource ()).Valid ())
644648 }
645649}
646650func (_this AwsArn ) ToString () _dafny.Sequence {
0 commit comments