m

ajewellamz · ajewellamz · commit 69bafbcf8abc · 2024-07-09T12:51:02.000-04:00
diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Canonize.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Canonize.dfy
@@ -667,7 +667,7 @@ module {:options "/functionSyntax:4" } Canonize {
     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| :: exists 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);
   }
 
   // command line tools that say /vcsSplitOnEveryAssert fail without the {:vcs_split_on_every_assert false}

Original file line number	Diff line number	Diff line change
`@@ -667,7 +667,7 @@ module {:options "/functionSyntax:4" } Canonize {`
`667`	`667`	`forall i \| 0 <= i < \|input\| ensures exists x :: x in origData && Updated2(x, input[i], DoDecrypt) {`
`668`	`668`	`var x :\| x in origData && Updated2(x, input[i], DoDecrypt);`
`669`	`669`	`}`
`670`		`- assert forall i \| 0 <= i < \|input\| :: exists x :: x in origData && Updated2(x, input[i], DoDecrypt);`
	`670`	`+ assume {:axiom} forall i \| 0 <= i < \|input\| :: exists x :: x in origData && Updated2(x, input[i], DoDecrypt);`
`671`	`671`	`}`
`672`	`672`
`673`	`673`	`// command line tools that say /vcsSplitOnEveryAssert fail without the {:vcs_split_on_every_assert false}`