Reduce and clarify difference in verification

aws · Aug 22, 2024 · 05d7945 · 05d7945
1 parent a79e9f5
commit 05d7945
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 4 deletions.
diff --git a/...ographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMMs/DefaultCMM.dfy b/...ographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMMs/DefaultCMM.dfy
@@ -373,7 +373,6 @@ module DefaultCMM {
       //# the values MUST be equal or the operation MUST fail.
       ensures
         && (output.Success? ==> CMM.ReproducedEncryptionContext?(input))
-      ensures
         && (!CMM.ReproducedEncryptionContext?(input) ==> output.Failure?)
       //= aws-encryption-sdk-specification/framework/cmm-interface.md#decrypt-materials
       //= type=implication
@@ -490,10 +489,10 @@ module DefaultCMM {
           invariant |keysSet'| == |keysSeq| - i
           invariant forall key
                       |
-                      && key in input.reproducedEncryptionContext.value.Keys
+                      && key in input.reproducedEncryptionContext.value
                       && key in input.encryptionContext
                       && key !in keysSet'
-                      :: input.encryptionContext[key] == input.reproducedEncryptionContext.value[key]
+                      :: input.reproducedEncryptionContext.value[key] == input.encryptionContext[key]
           invariant forall key <- requiredEncryptionContextKeys
                       :: key !in input.encryptionContext
         {

diff --git a/...oviders/dafny/AwsCryptographicMaterialProviders/src/CMMs/RequiredEncryptionContextCMM.dfy b/...oviders/dafny/AwsCryptographicMaterialProviders/src/CMMs/RequiredEncryptionContextCMM.dfy
@@ -54,7 +54,9 @@ module RequiredEncryptionContextCMM {
     {
       var keySet := inputKeys;
       var keySeq := SortedSets.ComputeSetToSequence(keySet);
-
+      assert |keySeq| == |keySet| == |inputKeys|;
+      assert forall k <- keySeq
+               :: k in inputKeys;
       underlyingCMM := inputCMM;
       requiredEncryptionContextKeys := keySeq;