chore: bump dafny verification version to 4.7 (#1181)

* chore: bump dafny verification version to 4.7

Author: ajewellamz

.github/workflows/ci_verification.yml

@@ -50,7 +50,7 @@ jobs:
         uses: dafny-lang/[email protected]
         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 }}

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);
-    }
-    assert 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)