m

aws · Jul 9, 2024 · 7ba8315 · 7ba8315
1 parent 69bafbc
commit 7ba8315
Showing 1 changed file with 4 additions and 4 deletions.
diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Canonize.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Canonize.dfy
@@ -663,10 +663,10 @@ module {:options "/functionSyntax:4" } Canonize {
     requires forall val <- input :: exists x :: x in origData && Updated2(x, val, DoDecrypt)
     ensures forall i | 0 <= i < |input| :: exists x :: x in origData && Updated2(x, input[i], DoDecrypt)
   {
-    assert forall i | 0 <= i < |input| :: input[i] in input;
-    forall i | 0 <= i < |input| ensures exists x :: x in origData && Updated2(x, input[i], DoDecrypt) {
-      var x :| x in origData && Updated2(x, input[i], DoDecrypt);
-    }
+    // assert forall i | 0 <= i < |input| :: input[i] in input;
+    // forall i | 0 <= i < |input| ensures exists x :: x in origData && Updated2(x, input[i], DoDecrypt) {
+    //   var x :| x in origData && Updated2(x, input[i], DoDecrypt);
+    // }
     assume {:axiom} forall i | 0 <= i < |input| :: exists x :: x in origData && Updated2(x, input[i], DoDecrypt);
   }