180
180
import aws_encryption_sdk .internaldafny .generated .KeyDerivation as KeyDerivation
181
181
import aws_encryption_sdk .internaldafny .generated .EncryptDecryptHelpers as EncryptDecryptHelpers
182
182
import aws_encryption_sdk .internaldafny .generated .AwsEncryptionSdkOperations as AwsEncryptionSdkOperations
183
- import aws_encryption_sdk .internaldafny .generated .EncryptionSdk as EncryptionSdk
183
+ import aws_encryption_sdk .internaldafny .generated .ESDK as ESDK
184
184
import aws_cryptography_materialproviders_test_vectors .internaldafny .generated .MplManifestOptions as MplManifestOptions
185
185
import smithy_dafny_standard_library .internaldafny .generated .GetOpt as GetOpt
186
186
import aws_cryptography_materialproviders_test_vectors .internaldafny .generated .AllAlgorithmSuites as AllAlgorithmSuites
@@ -240,7 +240,7 @@ def StartDecryptVectors(op):
240
240
output = (d_2_valueOrError1_ ).PropagateFailure ()
241
241
return output
242
242
d_3_valueOrError2_ : Wrappers .Result = Wrappers .Result .default (_dafny .Seq )()
243
- d_3_valueOrError2_ = ParseEsdkJsonManifest .default__ .BuildDecryptTestVector (op , (d_1_decryptManifest_ ).version , (d_1_decryptManifest_ ).keys , (d_1_decryptManifest_ ).jsonTests )
243
+ d_3_valueOrError2_ = ParseEsdkJsonManifest .default__ .BuildDecryptTestVector (op , (d_1_decryptManifest_ ).clientName , ( d_1_decryptManifest_ ). clientVersion , ( d_1_decryptManifest_ ). version , (d_1_decryptManifest_ ).keys , (d_1_decryptManifest_ ).jsonTests )
244
244
if (d_3_valueOrError2_ ).IsFailure ():
245
245
output = (d_3_valueOrError2_ ).PropagateFailure ()
246
246
return output
@@ -288,9 +288,10 @@ def TestDecrypts(keys, vectors):
288
288
_dafny .print (_dafny .string_of (_dafny .Seq ("Skipped: " )))
289
289
_dafny .print (_dafny .string_of (d_1_skipped_ ))
290
290
_dafny .print (_dafny .string_of (_dafny .Seq ("\n " )))
291
- if not (not (d_0_hasFailure_ )):
292
- raise _dafny .HaltException ("dafny/TestVectors/src/EsdkTestManifests.dfy(92,4): " + _dafny .string_of (_dafny .Seq ("expectation violation" )))
293
- manifest = Wrappers .Result_Success (_dafny .Seq ([]))
291
+ if not (d_0_hasFailure_ ):
292
+ manifest = Wrappers .Result_Success (_dafny .Seq ([]))
293
+ elif True :
294
+ manifest = Wrappers .Result_Failure (_dafny .Seq ("Test Vectors failed, see errors above.\n " ))
294
295
return manifest
295
296
296
297
@staticmethod
@@ -520,81 +521,95 @@ def lambda0_(d_4_e_):
520
521
d_12_typ_ : _dafny .Seq
521
522
d_12_typ_ = (d_11_valueOrError5_ ).Extract ()
522
523
d_13_valueOrError6_ : Wrappers .Result = Wrappers .Result .default (_dafny .Seq )()
523
- d_13_valueOrError6_ = JSONHelpers .default__ .GetString (_dafny .Seq ("keys " ), (d_5_manifestJson_ ).obj )
524
+ d_13_valueOrError6_ = JSONHelpers .default__ .GetObject (_dafny .Seq ("client " ), (d_5_manifestJson_ ).obj )
524
525
if (d_13_valueOrError6_ ).IsFailure ():
525
526
manifestData = (d_13_valueOrError6_ ).PropagateFailure ()
526
527
return manifestData
527
- d_14_keyManifestUri_ : _dafny .Seq
528
- d_14_keyManifestUri_ = (d_13_valueOrError6_ ).Extract ()
529
- d_15_valueOrError7_ : Wrappers .Outcome = Wrappers .Outcome .default ()()
530
- d_15_valueOrError7_ = Wrappers .default__ .Need (( _dafny .Seq ("file://" )) < ( d_14_keyManifestUri_ ), _dafny . Seq ( "Unexpected URI prefix" ) )
528
+ d_14_client_ : _dafny .Seq
529
+ d_14_client_ = (d_13_valueOrError6_ ).Extract ()
530
+ d_15_valueOrError7_ : Wrappers .Result = Wrappers .Result .default (_dafny . Seq )()
531
+ d_15_valueOrError7_ = JSONHelpers .default__ .GetString ( _dafny .Seq ("name" ), d_14_client_ )
531
532
if (d_15_valueOrError7_ ).IsFailure ():
532
533
manifestData = (d_15_valueOrError7_ ).PropagateFailure ()
533
534
return manifestData
534
- d_16_keyManifestPath_ : _dafny .Seq
535
- d_16_keyManifestPath_ = (manifestPath ) + (_dafny .Seq ((d_14_keyManifestUri_ )[7 ::]))
536
- d_17_valueOrError8_ : Wrappers .Result = None
537
- out1_ : Wrappers .Result
538
- out1_ = KeyVectors .default__ .KeyVectors (AwsCryptographyMaterialProvidersTestVectorKeysTypes .KeyVectorsConfig_KeyVectorsConfig (d_16_keyManifestPath_ ))
539
- d_17_valueOrError8_ = out1_
540
- if not (not ((d_17_valueOrError8_ ).IsFailure ())):
541
- raise _dafny .HaltException ("dafny/TestVectors/src/EsdkTestManifests.dfy(263,16): " + _dafny .string_of (d_17_valueOrError8_ ))
542
- d_18_keys_ : KeyVectors .KeyVectorsClient
543
- d_18_keys_ = (d_17_valueOrError8_ ).Extract ()
535
+ d_16_clientName_ : _dafny .Seq
536
+ d_16_clientName_ = (d_15_valueOrError7_ ).Extract ()
537
+ d_17_valueOrError8_ : Wrappers .Result = Wrappers .Result .default (_dafny .Seq )()
538
+ d_17_valueOrError8_ = JSONHelpers .default__ .GetString (_dafny .Seq ("version" ), d_14_client_ )
539
+ if (d_17_valueOrError8_ ).IsFailure ():
540
+ manifestData = (d_17_valueOrError8_ ).PropagateFailure ()
541
+ return manifestData
542
+ d_18_clientVersion_ : _dafny .Seq
543
+ d_18_clientVersion_ = (d_17_valueOrError8_ ).Extract ()
544
544
d_19_valueOrError9_ : Wrappers .Result = Wrappers .Result .default (_dafny .Seq )()
545
- d_19_valueOrError9_ = JSONHelpers .default__ .GetObject (_dafny .Seq ("tests " ), (d_5_manifestJson_ ).obj )
545
+ d_19_valueOrError9_ = JSONHelpers .default__ .GetString (_dafny .Seq ("keys " ), (d_5_manifestJson_ ).obj )
546
546
if (d_19_valueOrError9_ ).IsFailure ():
547
547
manifestData = (d_19_valueOrError9_ ).PropagateFailure ()
548
548
return manifestData
549
- d_20_jsonTests_ : _dafny .Seq
550
- d_20_jsonTests_ = (d_19_valueOrError9_ ).Extract ()
549
+ d_20_keyManifestUri_ : _dafny .Seq
550
+ d_20_keyManifestUri_ = (d_19_valueOrError9_ ).Extract ()
551
+ d_21_valueOrError10_ : Wrappers .Outcome = Wrappers .Outcome .default ()()
552
+ d_21_valueOrError10_ = Wrappers .default__ .Need ((_dafny .Seq ("file://" )) < (d_20_keyManifestUri_ ), _dafny .Seq ("Unexpected URI prefix" ))
553
+ if (d_21_valueOrError10_ ).IsFailure ():
554
+ manifestData = (d_21_valueOrError10_ ).PropagateFailure ()
555
+ return manifestData
556
+ d_22_keyManifestPath_ : _dafny .Seq
557
+ d_22_keyManifestPath_ = (manifestPath ) + (_dafny .Seq ((d_20_keyManifestUri_ )[7 ::]))
558
+ d_23_valueOrError11_ : Wrappers .Result = None
559
+ out1_ : Wrappers .Result
560
+ out1_ = KeyVectors .default__ .KeyVectors (AwsCryptographyMaterialProvidersTestVectorKeysTypes .KeyVectorsConfig_KeyVectorsConfig (d_22_keyManifestPath_ ))
561
+ d_23_valueOrError11_ = out1_
562
+ if not (not ((d_23_valueOrError11_ ).IsFailure ())):
563
+ raise _dafny .HaltException ("dafny/TestVectors/src/EsdkTestManifests.dfy(268,16): " + _dafny .string_of (d_23_valueOrError11_ ))
564
+ d_24_keys_ : KeyVectors .KeyVectorsClient
565
+ d_24_keys_ = (d_23_valueOrError11_ ).Extract ()
566
+ d_25_valueOrError12_ : Wrappers .Result = Wrappers .Result .default (_dafny .Seq )()
567
+ d_25_valueOrError12_ = JSONHelpers .default__ .GetObject (_dafny .Seq ("tests" ), (d_5_manifestJson_ ).obj )
568
+ if (d_25_valueOrError12_ ).IsFailure ():
569
+ manifestData = (d_25_valueOrError12_ ).PropagateFailure ()
570
+ return manifestData
571
+ d_26_jsonTests_ : _dafny .Seq
572
+ d_26_jsonTests_ = (d_25_valueOrError12_ ).Extract ()
551
573
source0_ = d_12_typ_
552
574
with _dafny .label ("match0" ):
553
575
if True :
554
576
if (source0_ ) == (_dafny .Seq ("awses-decrypt" )):
555
- d_21_valueOrError10_ : Wrappers .Outcome = Wrappers .Outcome .default ()()
556
- d_21_valueOrError10_ = Wrappers .default__ .Need (EsdkTestVectors .default__ .SupportedDecryptVersion_q (d_10_version_ ), _dafny .Seq ("Unsupported manifest version" ))
557
- if (d_21_valueOrError10_ ).IsFailure ():
558
- manifestData = (d_21_valueOrError10_ ).PropagateFailure ()
559
- return manifestData
560
- d_22_valueOrError11_ : Wrappers .Result = Wrappers .Result .default (JSON_Values .JSON .default ())()
561
- d_22_valueOrError11_ = JSONHelpers .default__ .Get (_dafny .Seq ("client" ), (d_5_manifestJson_ ).obj )
562
- if (d_22_valueOrError11_ ).IsFailure ():
563
- manifestData = (d_22_valueOrError11_ ).PropagateFailure ()
577
+ d_27_valueOrError13_ : Wrappers .Outcome = Wrappers .Outcome .default ()()
578
+ d_27_valueOrError13_ = Wrappers .default__ .Need (EsdkTestVectors .default__ .SupportedDecryptVersion_q (d_10_version_ ), _dafny .Seq ("Unsupported manifest version" ))
579
+ if (d_27_valueOrError13_ ).IsFailure ():
580
+ manifestData = (d_27_valueOrError13_ ).PropagateFailure ()
564
581
return manifestData
565
- d_23_client_ : JSON_Values .JSON
566
- d_23_client_ = (d_22_valueOrError11_ ).Extract ()
567
- manifestData = Wrappers .Result_Success (ManifestData_DecryptManifest (d_10_version_ , d_18_keys_ , d_23_client_ , d_20_jsonTests_ ))
582
+ manifestData = Wrappers .Result_Success (ManifestData_DecryptManifest (d_10_version_ , d_24_keys_ , d_16_clientName_ , d_18_clientVersion_ , d_26_jsonTests_ ))
568
583
raise _dafny .Break ("match0" )
569
584
if True :
570
585
if (source0_ ) == (_dafny .Seq ("awses-encrypt" )):
571
- d_24_valueOrError12_ : Wrappers .Outcome = Wrappers .Outcome .default ()()
572
- d_24_valueOrError12_ = Wrappers .default__ .Need (EsdkTestVectors .default__ .SupportedEncryptVersion_q (d_10_version_ ), _dafny .Seq ("Unsupported manifest version" ))
573
- if (d_24_valueOrError12_ ).IsFailure ():
574
- manifestData = (d_24_valueOrError12_ ).PropagateFailure ()
586
+ d_28_valueOrError14_ : Wrappers .Outcome = Wrappers .Outcome .default ()()
587
+ d_28_valueOrError14_ = Wrappers .default__ .Need (EsdkTestVectors .default__ .SupportedEncryptVersion_q (d_10_version_ ), _dafny .Seq ("Unsupported manifest version" ))
588
+ if (d_28_valueOrError14_ ).IsFailure ():
589
+ manifestData = (d_28_valueOrError14_ ).PropagateFailure ()
575
590
return manifestData
576
- d_25_valueOrError13_ : Wrappers .Result = Wrappers .Result .default (_dafny .Seq )()
577
- d_25_valueOrError13_ = JSONHelpers .default__ .GetObject (_dafny .Seq ("plaintexts" ), (d_5_manifestJson_ ).obj )
578
- if (d_25_valueOrError13_ ).IsFailure ():
579
- manifestData = (d_25_valueOrError13_ ).PropagateFailure ()
591
+ d_29_valueOrError15_ : Wrappers .Result = Wrappers .Result .default (_dafny .Seq )()
592
+ d_29_valueOrError15_ = JSONHelpers .default__ .GetObject (_dafny .Seq ("plaintexts" ), (d_5_manifestJson_ ).obj )
593
+ if (d_29_valueOrError15_ ).IsFailure ():
594
+ manifestData = (d_29_valueOrError15_ ).PropagateFailure ()
580
595
return manifestData
581
- d_26_plaintextsJson_ : _dafny .Seq
582
- d_26_plaintextsJson_ = (d_25_valueOrError13_ ).Extract ()
583
- d_27_valueOrError15_ : Wrappers .Result = Wrappers .Result .default (_dafny .Seq )()
584
- def lambda1_ (d_28_obj_ ):
596
+ d_30_plaintextsJson_ : _dafny .Seq
597
+ d_30_plaintextsJson_ = (d_29_valueOrError15_ ).Extract ()
598
+ d_31_valueOrError17_ : Wrappers .Result = Wrappers .Result .default (_dafny .Seq )()
599
+ def lambda1_ (d_32_obj_ ):
585
600
def iife0_ (_pat_let7_0 ):
586
- def iife1_ (d_29_valueOrError14_ ):
587
- return ((d_29_valueOrError14_ ).PropagateFailure () if (d_29_valueOrError14_ ).IsFailure () else Wrappers .Result_Success (((d_28_obj_ )[0 ], (((d_28_obj_ )[1 ]).num ).n )))
601
+ def iife1_ (d_33_valueOrError16_ ):
602
+ return ((d_33_valueOrError16_ ).PropagateFailure () if (d_33_valueOrError16_ ).IsFailure () else Wrappers .Result_Success (((d_32_obj_ )[0 ], (((d_32_obj_ )[1 ]).num ).n )))
588
603
return iife1_ (_pat_let7_0 )
589
- return iife0_ (Wrappers .default__ .Need ((((d_28_obj_ )[1 ]).is_Number ) and (((0 ) < ((((d_28_obj_ )[1 ]).num ).n )) and (((((d_28_obj_ )[1 ]).num ).n ) <= (BoundedInts .default__ .INT32__MAX ))), _dafny .Seq ("Size is not a natural number." )))
604
+ return iife0_ (Wrappers .default__ .Need ((((d_32_obj_ )[1 ]).is_Number ) and (((0 ) < ((((d_32_obj_ )[1 ]).num ).n )) and (((((d_32_obj_ )[1 ]).num ).n ) <= (BoundedInts .default__ .INT32__MAX ))), _dafny .Seq ("Size is not a natural number." )))
590
605
591
- d_27_valueOrError15_ = Seq .default__ .MapWithResult (lambda1_ , d_26_plaintextsJson_ )
592
- if (d_27_valueOrError15_ ).IsFailure ():
593
- manifestData = (d_27_valueOrError15_ ).PropagateFailure ()
606
+ d_31_valueOrError17_ = Seq .default__ .MapWithResult (lambda1_ , d_30_plaintextsJson_ )
607
+ if (d_31_valueOrError17_ ).IsFailure ():
608
+ manifestData = (d_31_valueOrError17_ ).PropagateFailure ()
594
609
return manifestData
595
- d_30_plaintextsLength_ : _dafny .Seq
596
- d_30_plaintextsLength_ = (d_27_valueOrError15_ ).Extract ()
597
- manifestData = Wrappers .Result_Success (ManifestData_EncryptManifest (d_10_version_ , d_18_keys_ , d_30_plaintextsLength_ , d_20_jsonTests_ ))
610
+ d_34_plaintextsLength_ : _dafny .Seq
611
+ d_34_plaintextsLength_ = (d_31_valueOrError17_ ).Extract ()
612
+ manifestData = Wrappers .Result_Success (ManifestData_EncryptManifest (d_10_version_ , d_24_keys_ , d_34_plaintextsLength_ , d_26_jsonTests_ ))
598
613
raise _dafny .Break ("match0" )
599
614
if True :
600
615
manifestData = Wrappers .Result_Failure ((_dafny .Seq ("Unsupported manifest type:" )) + (d_12_typ_ ))
@@ -605,7 +620,7 @@ def iife1_(d_29_valueOrError14_):
605
620
class ManifestData :
606
621
@classmethod
607
622
def default (cls , ):
608
- return lambda : ManifestData_DecryptManifest (int (0 ), None , JSON_Values . JSON . default ()( ), _dafny .Seq ({}))
623
+ return lambda : ManifestData_DecryptManifest (int (0 ), None , _dafny . Seq ( "" ), _dafny . Seq ( "" ), _dafny .Seq ({}))
609
624
def __ne__ (self , __o : object ) -> bool :
610
625
return not self .__eq__ (__o )
611
626
@property
@@ -615,11 +630,11 @@ def is_DecryptManifest(self) -> bool:
615
630
def is_EncryptManifest (self ) -> bool :
616
631
return isinstance (self , ManifestData_EncryptManifest )
617
632
618
- class ManifestData_DecryptManifest (ManifestData , NamedTuple ('DecryptManifest' , [('version' , Any ), ('keys' , Any ), ('client ' , Any ), ('jsonTests' , Any )])):
633
+ class ManifestData_DecryptManifest (ManifestData , NamedTuple ('DecryptManifest' , [('version' , Any ), ('keys' , Any ), ('clientName' , Any ), ( 'clientVersion ' , Any ), ('jsonTests' , Any )])):
619
634
def __dafnystr__ (self ) -> str :
620
- return f'EsdkTestManifests.ManifestData.DecryptManifest({ _dafny .string_of (self .version )} , { _dafny .string_of (self .keys )} , { _dafny .string_of (self .client )} , { _dafny .string_of (self .jsonTests )} )'
635
+ return f'EsdkTestManifests.ManifestData.DecryptManifest({ _dafny .string_of (self .version )} , { _dafny .string_of (self .keys )} , { _dafny .string_of (self .clientName ) } , { _dafny . string_of ( self . clientVersion )} , { _dafny .string_of (self .jsonTests )} )'
621
636
def __eq__ (self , __o : object ) -> bool :
622
- return isinstance (__o , ManifestData_DecryptManifest ) and self .version == __o .version and self .keys == __o .keys and self .client == __o .client and self .jsonTests == __o .jsonTests
637
+ return isinstance (__o , ManifestData_DecryptManifest ) and self .version == __o .version and self .keys == __o .keys and self .clientName == __o .clientName and self . clientVersion == __o . clientVersion and self .jsonTests == __o .jsonTests
623
638
def __hash__ (self ) -> int :
624
639
return super ().__hash__ ()
625
640
0 commit comments