From 0461948e9d94dbd452d0d97ed3fc3adfebc3f791 Mon Sep 17 00:00:00 2001
From: Andy Jewell <ajewell@amazon.com>
Date: Sun, 7 Apr 2024 11:29:04 -0400
Subject: [PATCH 1/2] chore: add verify test for test vectors

---
 .github/workflows/ci_tv_verification.yml      | 64 +++++++++++++++++++
 .../dafny/DDBEncryption/src/TestVectors.dfy   |  2 +-
 2 files changed, 65 insertions(+), 1 deletion(-)
 create mode 100644 .github/workflows/ci_tv_verification.yml

diff --git a/.github/workflows/ci_tv_verification.yml b/.github/workflows/ci_tv_verification.yml
new file mode 100644
index 000000000..b2d5510f0
--- /dev/null
+++ b/.github/workflows/ci_tv_verification.yml
@@ -0,0 +1,64 @@
+# This workflow performs verification checks
+name: test vector verification
+
+on:
+  pull_request:
+  push:
+    branches:
+      - main
+  workflow_dispatch:
+    # Manual trigger for this workflow, either the normal version
+    # or the nightly build that uses the latest Dafny prerelease
+    # (accordingly to the "nightly" parameter).
+    inputs:
+      nightly:
+        description: 'Run the nightly build'
+        required: false
+        type: boolean
+  schedule:
+    # Nightly build against Dafny's nightly prereleases,
+    # for early warning of verification issues or regressions.
+    # Timing chosen to be adequately after Dafny's own nightly build,
+    # but this might need to be tweaked:
+    # https://github.com/dafny-lang/dafny/blob/master/.github/workflows/deep-tests.yml#L16
+    - cron: "30 16 * * *"
+
+jobs:
+  verification:
+    # Don't run the nightly build on forks
+    if: github.event_name != 'schedule' || github.repository_owner == 'aws'
+    strategy:
+      matrix:
+        # Break up verification between namespaces over multiple
+        # actions to take advantage of parallelization
+        service: [
+          DynamoDbEncryption
+        ]
+        os: [
+          macos-latest,
+        ]
+    runs-on: ${{ matrix.os }}
+    steps:
+      - uses: actions/checkout@v3
+        with:
+          submodules: recursive
+
+      - name: Setup Dafny
+        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.2.0' }}
+
+      - name: Verify ${{ matrix.library }} Dafny code
+        shell: bash
+        working-directory: ./TestVectors
+        run: |
+          # This works because `node` is installed by default on GHA runners
+          CORES=$(node -e 'console.log(os.cpus().length)')
+          make verify_service CORES=$CORES SERVICE=${{ matrix.service }}
+
+      - name: Check solver resource use
+        shell: bash
+        working-directory: ./TestVectors
+        run: |
+          make dafny-reportgenerator
diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
index 39615e648..0123518b3 100644
--- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
+++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
@@ -569,7 +569,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
         var res := client.Query(GetQueryInput(failingQueries[i], usedNames, usedValues));
         expect res.Failure?;
       }
-      var results := new DDB.ItemList[|queries|];
+      var results := new DDB.ItemList[|queries|](i => []);
       for i := 0 to |queries| {
         results[i] := FullSearch(client, queries[i]);
       }

From 35bbcb7d1bd28a9f18d40b1a90bbde159c2e001b Mon Sep 17 00:00:00 2001
From: Andy Jewell <ajewell@amazon.com>
Date: Sun, 7 Apr 2024 11:31:47 -0400
Subject: [PATCH 2/2] m

---
 .github/workflows/ci_tv_verification.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/ci_tv_verification.yml b/.github/workflows/ci_tv_verification.yml
index b2d5510f0..da76273e0 100644
--- a/.github/workflows/ci_tv_verification.yml
+++ b/.github/workflows/ci_tv_verification.yml
@@ -32,7 +32,7 @@ jobs:
         # Break up verification between namespaces over multiple
         # actions to take advantage of parallelization
         service: [
-          DynamoDbEncryption
+          DDBEncryption
         ]
         os: [
           macos-latest,