Merge branch 'main' into primitives-name

Author: lucasmcdonald3

AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMMs/DefaultCMM.dfy

@@ -23,6 +23,7 @@ module DefaultCMM {
   import Defaults
   import Commitment
   import Seq
+  import SortedSets
 
   class DefaultCMM
     extends CMM.VerifiableInterface
@@ -329,7 +330,7 @@ module DefaultCMM {
     //# - The operations made on the encryption context on the Get Encryption Materials call
     //# SHOULD be inverted on the Decrypt Materials call.
 
-    method DecryptMaterials'(
+    method {:vcs_split_on_every_assert} DecryptMaterials'(
       input: Types.DecryptMaterialsInput
     )
       returns (output: Result<Types.DecryptMaterialsOutput, Types.Error>)
@@ -478,25 +479,36 @@ module DefaultCMM {
       var requiredEncryptionContextKeys := [];
       if input.reproducedEncryptionContext.Some? {
         var keysSet := input.reproducedEncryptionContext.value.Keys;
-        while keysSet != {}
+        ghost var keysSet' := keysSet;
+        var keysSeq := SortedSets.ComputeSetToSequence(keysSet);
+        var i := 0;
+        while i < |keysSeq|
+          invariant Seq.HasNoDuplicates(keysSeq)
+          invariant forall j | 0 <= j < i && i < |keysSeq| :: keysSeq[j] !in keysSet'
+          invariant forall j | i <= j < |keysSeq| :: keysSeq[j] in keysSet'
+          invariant |keysSet'| == |keysSeq| - i
           invariant forall key
                       |
                       && key in input.reproducedEncryptionContext.value
                       && key in input.encryptionContext
-                      && key !in keysSet
+                      && key !in keysSet'
                       :: input.reproducedEncryptionContext.value[key] == input.encryptionContext[key]
           invariant forall key <- requiredEncryptionContextKeys
                       :: key !in input.encryptionContext
         {
-          var key :| key in keysSet;
+          var key := keysSeq[i];
           if key in input.encryptionContext {
             :- Need(input.reproducedEncryptionContext.value[key] == input.encryptionContext[key],
                     Types.AwsCryptographicMaterialProvidersException(
                       message := "Encryption context does not match reproduced encryption context."));
           } else {
             requiredEncryptionContextKeys :=  requiredEncryptionContextKeys + [key];
           }
-          keysSet := keysSet - {key};
+          keysSet' := keysSet' - {key};
+          i := i + 1;
+          assert forall j | i <= j < |keysSeq| :: keysSeq[j] in keysSet' by {
+            reveal Seq.HasNoDuplicates();
+          }
         }
       }
 

AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMMs/RequiredEncryptionContextCMM.dfy

@@ -16,6 +16,7 @@ module RequiredEncryptionContextCMM {
   import UTF8
   import Types = AwsCryptographyMaterialProvidersTypes
   import Seq
+  import SortedSets
 
   class RequiredEncryptionContextCMM
     extends CMM.VerifiableInterface
@@ -52,17 +53,10 @@ module RequiredEncryptionContextCMM {
       ensures Modifies == { History } + underlyingCMM.Modifies
     {
       var keySet := inputKeys;
-      var keySeq := [];
-      while keySet != {}
-        invariant |keySeq| + |keySet| == |inputKeys|
-        invariant forall k <- keySeq
-                    :: k in inputKeys
-      {
-        var key :| key in keySet;
-        keySeq := keySeq + [key];
-        keySet := keySet - {key};
-      }
-
+      var keySeq := SortedSets.ComputeSetToSequence(keySet);
+      assert |keySeq| == |keySet| == |inputKeys|;
+      assert forall k <- keySeq
+          :: k in inputKeys;
       underlyingCMM := inputCMM;
       requiredEncryptionContextKeys := keySeq;
 

AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CanonicalEncryptionContext.dfy

@@ -9,6 +9,7 @@ module CanonicalEncryptionContext {
   import Types = AwsCryptographyMaterialProvidersTypes
   import opened Wrappers
   import Seq
+  import SortedSets
 
   //= aws-encryption-sdk-specification/framework/raw-aes-keyring.md#onencrypt
   //# The keyring MUST attempt to serialize the [encryption materials']
@@ -25,7 +26,7 @@ module CanonicalEncryptionContext {
   {
     :- Need(|encryptionContext| < UINT16_LIMIT,
             Types.AwsCryptographicMaterialProvidersException( message := "Encryption Context is too large" ));
-    var keys := SetToOrderedSequence(encryptionContext.Keys, UInt.UInt8Less);
+    var keys := SortedSets.ComputeSetToOrderedSequence2(encryptionContext.Keys, UInt.UInt8Less);
 
     if |keys| == 0 then
       Success([])

AwsCryptographyPrimitives/test/TestRSA.dfy

@@ -9,6 +9,7 @@ module {:options "-functionSyntax:4"} TestAwsCryptographyPrimitivesRSA {
   import opened Wrappers
   import opened StandardLibrary.UInt
   import UTF8
+  import SortedSets
 
   const RSA_PUBLIC_2048 := "-----BEGIN PUBLIC KEY-----\n"
                            + "MIIBIjANBgkqhkiG9w0BAQEFAAOCAQ8AMIIBCgKCAQEAqBvECLsPdF1J5DOkaA1n\n"
@@ -130,10 +131,11 @@ module {:options "-functionSyntax:4"} TestAwsCryptographyPrimitivesRSA {
         lengthBits := 2048,
         pem := PrivateKeyFromGenerateRSAKeyPairPemBytes
       ));
-
-    while allPadding != {}
+    var paddingSeq := SortedSets.ComputeSetToSequence(allPadding);
+    for paddingIdx := 0 to |paddingSeq|
     {
-      var padding :| padding in allPadding;
+      var padding := paddingSeq[paddingIdx];
+
       BasicRSAEncryptTest(
         AtomicPrimitives.Types.RSAEncryptInput(
           padding := padding,
@@ -144,7 +146,6 @@ module {:options "-functionSyntax:4"} TestAwsCryptographyPrimitivesRSA {
         KeyFromGenerateRSAKeyPair
       );
 
-      allPadding := allPadding - {padding};
     }
   }
 
@@ -164,9 +165,10 @@ module {:options "-functionSyntax:4"} TestAwsCryptographyPrimitivesRSA {
         pem := PrivateKeyFromTestVectorsPemBytes
       ));
 
-    while allPadding != {}
+    var paddingSeq := SortedSets.ComputeSetToSequence(allPadding);
+    for paddingIdx := 0 to |paddingSeq|
     {
-      var padding :| padding in allPadding;
+      var padding := paddingSeq[paddingIdx];
 
       BasicRSAEncryptTest(
         AtomicPrimitives.Types.RSAEncryptInput(
@@ -178,7 +180,6 @@ module {:options "-functionSyntax:4"} TestAwsCryptographyPrimitivesRSA {
         KeyFromTestVectorsPair
       );
 
-      allPadding := allPadding - {padding};
     }
   }