m

ajewellamz · ajewellamz · commit 7ba8315798ee · 2024-07-09T13:01:05.000-04:00
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);
   }
 

Original file line number	Diff line number	Diff line change
`@@ -663,10 +663,10 @@ module {:options "/functionSyntax:4" } Canonize {`
`663`	`663`	`requires forall val <- input :: exists x :: x in origData && Updated2(x, val, DoDecrypt)`
`664`	`664`	`ensures forall i \| 0 <= i < \|input\| :: exists x :: x in origData && Updated2(x, input[i], DoDecrypt)`
`665`	`665`	`{`
`666`		`- assert forall i \| 0 <= i < \|input\| :: input[i] in input;`
`667`		`- forall i \| 0 <= i < \|input\| ensures exists x :: x in origData && Updated2(x, input[i], DoDecrypt) {`
`668`		`- var x :\| x in origData && Updated2(x, input[i], DoDecrypt);`
`669`		`- }`
	`666`	`+ // assert forall i \| 0 <= i < \|input\| :: input[i] in input;`
	`667`	`+ // forall i \| 0 <= i < \|input\| ensures exists x :: x in origData && Updated2(x, input[i], DoDecrypt) {`
	`668`	`+ // var x :\| x in origData && Updated2(x, input[i], DoDecrypt);`
	`669`	`+ // }`
`670`	`670`	`assume {:axiom} forall i \| 0 <= i < \|input\| :: exists x :: x in origData && Updated2(x, input[i], DoDecrypt);`
`671`	`671`	`}`
`672`	`672`