From 7ba8315798eeb480276832feccf81d3f927d6bd4 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Tue, 9 Jul 2024 13:01:05 -0400 Subject: [PATCH] m --- .../dafny/StructuredEncryption/src/Canonize.dfy | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Canonize.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Canonize.dfy index 8ba90e724..ce0935b2e 100644 --- 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); }