fix

Author: ajewellamz

DynamoDbEncryption/dafny/StructuredEncryption/src/AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy

@@ -543,10 +543,10 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
 
   function method UnBuildCryptoMap(list : CryptoList, dataSoFar : StructuredDataMap := map[], actionsSoFar : CryptoSchemaMap := map[]) :
     (res : Result<(StructuredDataMap, CryptoSchemaMap), Error>)
-    requires dataSoFar.Keys == actionsSoFar.Keys
+    requires forall k <- actionsSoFar :: k in dataSoFar
     requires (forall v :: v in actionsSoFar.Values ==> IsAuthAttr(v))
     ensures res.Success? ==>
-              && res.value.0.Keys == res.value.1.Keys
+              && (forall k <- res.value.1 :: k in res.value.0)
               && (forall v :: v in res.value.1.Values ==> IsAuthAttr(v))
   {
     if |list| == 0 then
@@ -557,7 +557,7 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
       if IsAuthAttr(list[0].action) then
         UnBuildCryptoMap(list[1..], dataSoFar[key := list[0].data], actionsSoFar[key := list[0].action])
       else
-        UnBuildCryptoMap(list[1..], dataSoFar, actionsSoFar)
+        UnBuildCryptoMap(list[1..], dataSoFar[key := list[0].data], actionsSoFar)
   }
 
 

DynamoDbEncryption/dafny/StructuredEncryption/test/HappyCaseTests.dfy

@@ -79,7 +79,7 @@ module HappyCaseTests {
     //#   - [Stored Encryption Context](./header.md#encryption-context): The Encryption Context stored in the header.
     //#   - [Encrypted Data Keys](./header.md#encrypted-data-keys): The Encrypted Data Keys stored in the header.
     var parsedHeader := decryptRes.value.parsedHeader;
-    expect decryptRes.value.cryptoSchema == StructuredDataTestFixtures.TEST_CRYPTO_SCHEMA;
+    expect decryptRes.value.cryptoSchema == StructuredDataTestFixtures.TEST_CRYPTO_SCHEMA_AUTH_ONLY;
     expect parsedHeader.algorithmSuiteId == algSuiteId;
     expect encContext.Keys <= parsedHeader.storedEncryptionContext.Keys;
     expect forall k <- encContext.Keys :: parsedHeader.storedEncryptionContext[k] == encContext[k];