Verification fixes

Author: robin-aws

DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoDbGetEncryptedDataKeyDescriptionTest.dfy

@@ -156,7 +156,7 @@ module DynamoDbGetEncryptedDataKeyDescriptionTest {
     expect actualDataKeyDescription.EncryptedDataKeyDescriptionOutput[0].keyProviderInfo.value == "keyproviderInfo";
   }
 
-  method {:test} TestDDBItemInputAwsKmsHDataKeyCase()
+  method {:test} {:isolate_assertions} TestDDBItemInputAwsKmsHDataKeyCase()
   {
     var expectedHead := CreatePartialHeader(testVersion, testFlavor0, testMsgID, testLegend, testEncContext, [testAwsKmsHDataKey]);
     var serializedHeader := expectedHead.serialize() + expectedHead.msgID;

DynamoDbEncryption/dafny/StructuredEncryption/src/Canonize.dfy

@@ -663,6 +663,14 @@ module {:options "/functionSyntax:4" } Canonize {
     exists x :: x in origData && Updated2(x, item, DoDecrypt)
   }
 
+  ghost function Updated2Item(origData : AuthList, item : CanonCryptoItem) : (result : AuthItem)
+    requires Updated2Exists(origData, item)
+    ensures Updated2(result, item, DoDecrypt)
+  {
+    var r :| Updated2(r, item, DoDecrypt);
+    r
+  }
+
   ghost predicate Updated5Exists(origData : CryptoList, item : CanonCryptoItem)
   {
     exists x :: x in origData && Updated5(x, item, DoEncrypt)
@@ -693,6 +701,9 @@ module {:options "/functionSyntax:4" } Canonize {
       assert forall val <- input :: exists x :: x in origData && Updated2(x, val, DoDecrypt);
       assert forall i | 0 <= i < |input| :: exists x :: x in origData && Updated2(x, input[i], DoDecrypt) by {
         InputIsInput(origData, input);
+        forall i | 0 <= i < |input| ensures exists x :: x in origData && Updated2(x, input[i], DoDecrypt) {
+          var x := Updated2Item(origData, input[i]);
+        }
       }
       assert forall newVal <- output :: exists x :: x in origData && Updated3(x, newVal, DoDecrypt);
     }