From 472e198f18ac58869f58c82fcaf12b8da71ddcf1 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Tue, 9 Jul 2024 12:41:33 -0400 Subject: [PATCH 1/4] chore: bump dafny verification version to 4.7 --- .github/workflows/ci_verification.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci_verification.yml b/.github/workflows/ci_verification.yml index a9855fd7b..27ebac75a 100644 --- a/.github/workflows/ci_verification.yml +++ b/.github/workflows/ci_verification.yml @@ -50,7 +50,7 @@ jobs: uses: dafny-lang/setup-dafny-action@v1.7.0 with: # A && B || C is the closest thing to an if .. then ... else ... or ?: expression the GitHub Actions syntax supports. - dafny-version: ${{ (github.event_name == 'schedule' || inputs.nightly) && 'nightly-latest' || '4.6.0' }} + dafny-version: ${{ (github.event_name == 'schedule' || inputs.nightly) && 'nightly-latest' || '4.7.0' }} - name: Regenerate code using smithy-dafny if necessary if: ${{ github.event_name == 'schedule' || inputs.nightly }} From 69bafbcf8abc5c1945b3b37c23c668f176d0bd2d Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Tue, 9 Jul 2024 12:51:02 -0400 Subject: [PATCH 2/4] m --- DynamoDbEncryption/dafny/StructuredEncryption/src/Canonize.dfy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Canonize.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Canonize.dfy index 4bf84c2cb..8ba90e724 100644 --- 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} From 7ba8315798eeb480276832feccf81d3f927d6bd4 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Tue, 9 Jul 2024 13:01:05 -0400 Subject: [PATCH 3/4] 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); } From aa287882a74260ae7dea1c85bade491863dbf1c1 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Tue, 9 Jul 2024 14:35:49 -0400 Subject: [PATCH 4/4] m --- .../StructuredEncryption/src/Canonize.dfy | 34 +++++++++---------- 1 file changed, 16 insertions(+), 18 deletions(-) diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Canonize.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Canonize.dfy index ce0935b2e..85c6f93f9 100644 --- a/DynamoDbEncryption/dafny/StructuredEncryption/src/Canonize.dfy +++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/Canonize.dfy @@ -658,28 +658,26 @@ module {:options "/functionSyntax:4" } Canonize { } } - // command line tools that say /vcsSplitOnEveryAssert fail without the {:vcs_split_on_every_assert false} - lemma {:vcs_split_on_every_assert false} InputIsInput(origData : AuthList, input : CanonCryptoList) - 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) + ghost predicate Updated2Exists(origData : AuthList, item : CanonCryptoItem) { - // 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); + exists x :: x in origData && Updated2(x, item, DoDecrypt) } - // command line tools that say /vcsSplitOnEveryAssert fail without the {:vcs_split_on_every_assert false} - lemma {:vcs_split_on_every_assert false} InputIsInput2(origData : CryptoList, input : CanonCryptoList) - requires forall val <- input :: exists x :: x in origData && Updated5(x, val, DoEncrypt) - ensures forall i | 0 <= i < |input| :: exists x :: x in origData && Updated5(x, input[i], DoEncrypt) + ghost predicate Updated5Exists(origData : CryptoList, item : CanonCryptoItem) + { + exists x :: x in origData && Updated5(x, item, DoEncrypt) + } + + lemma InputIsInput(origData : AuthList, input : CanonCryptoList) + requires forall val <- input :: Updated2Exists(origData, val) + ensures forall i | 0 <= i < |input| :: Updated2Exists(origData, input[i]) + { + } + + lemma InputIsInput2(origData : CryptoList, input : CanonCryptoList) + requires forall val <- input :: Updated5Exists(origData, val) + ensures forall i | 0 <= i < |input| :: Updated5Exists(origData, input[i]) { - assert forall i | 0 <= i < |input| :: input[i] in input; - forall i | 0 <= i < |input| ensures exists x :: x in origData && Updated5(x, input[i], DoEncrypt) { - var x :| x in origData && Updated5(x, input[i], DoEncrypt); - } - assert forall i | 0 <= i < |input| :: exists x :: x in origData && Updated5(x, input[i], DoEncrypt); } lemma CryptoUpdatedAuthMaps(origData : AuthList, input : CanonCryptoList, output : CryptoList)