From 38941fc971a88a719a0c52f798a96934cc4521e1 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Tue, 29 Apr 2025 11:10:45 -0700 Subject: [PATCH 1/3] chore: run test vectors in net and java on MacOS --- .github/workflows/ci_test_vector_java.yml | 7 ++++++- .github/workflows/ci_test_vector_net.yml | 7 ++++++- .github/workflows/library_rust_tests.yml | 2 +- 3 files changed, 13 insertions(+), 3 deletions(-) diff --git a/.github/workflows/ci_test_vector_java.yml b/.github/workflows/ci_test_vector_java.yml index 6f310c42d..fc09ee5e1 100644 --- a/.github/workflows/ci_test_vector_java.yml +++ b/.github/workflows/ci_test_vector_java.yml @@ -32,13 +32,18 @@ jobs: os: [ # Run on ubuntu image that comes pre-configured with docker ubuntu-22.04, + macos-13, ] runs-on: ${{ matrix.os }} permissions: id-token: write contents: read steps: - - name: Setup DynamoDB Local + - name: Setup Docker + if: matrix.os == 'macos-13' && matrix.library == 'TestVectors' + uses: douglascamata/setup-docker-macos-action@v1.0.0 + + - name: Setup DynamoDB Local uses: rrainn/dynamodb-action@v4.0.0 with: port: 8000 diff --git a/.github/workflows/ci_test_vector_net.yml b/.github/workflows/ci_test_vector_net.yml index 999e04e47..64b115f2d 100644 --- a/.github/workflows/ci_test_vector_net.yml +++ b/.github/workflows/ci_test_vector_net.yml @@ -28,13 +28,18 @@ jobs: os: [ # Run on ubuntu image that comes pre-configured with docker ubuntu-22.04, + macos-13, ] runs-on: ${{ matrix.os }} permissions: id-token: write contents: read steps: - - name: Setup DynamoDB Local + - name: Setup Docker + if: matrix.os == 'macos-13' && matrix.library == 'TestVectors' + uses: douglascamata/setup-docker-macos-action@v1.0.0 + + - name: Setup DynamoDB Local uses: rrainn/dynamodb-action@v4.0.0 with: port: 8000 diff --git a/.github/workflows/library_rust_tests.yml b/.github/workflows/library_rust_tests.yml index 987a6946a..a6167f536 100644 --- a/.github/workflows/library_rust_tests.yml +++ b/.github/workflows/library_rust_tests.yml @@ -36,7 +36,7 @@ jobs: steps: - name: Setup Docker if: matrix.os == 'macos-13' && matrix.library == 'TestVectors' - uses: douglascamata/setup-docker-macos-action@v1-alpha + uses: douglascamata/setup-docker-macos-action@v1.0.0 - name: Setup DynamoDB Local if: matrix.library == 'TestVectors' From b81c0607ba90e3f278a1daa150c697b7a4c41d88 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Tue, 29 Apr 2025 11:18:02 -0700 Subject: [PATCH 2/3] m --- .github/workflows/ci_test_vector_java.yml | 2 +- .github/workflows/ci_test_vector_net.yml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/ci_test_vector_java.yml b/.github/workflows/ci_test_vector_java.yml index fc09ee5e1..7dc7fa627 100644 --- a/.github/workflows/ci_test_vector_java.yml +++ b/.github/workflows/ci_test_vector_java.yml @@ -43,7 +43,7 @@ jobs: if: matrix.os == 'macos-13' && matrix.library == 'TestVectors' uses: douglascamata/setup-docker-macos-action@v1.0.0 - - name: Setup DynamoDB Local + - name: Setup DynamoDB Local uses: rrainn/dynamodb-action@v4.0.0 with: port: 8000 diff --git a/.github/workflows/ci_test_vector_net.yml b/.github/workflows/ci_test_vector_net.yml index 64b115f2d..010892dc5 100644 --- a/.github/workflows/ci_test_vector_net.yml +++ b/.github/workflows/ci_test_vector_net.yml @@ -39,7 +39,7 @@ jobs: if: matrix.os == 'macos-13' && matrix.library == 'TestVectors' uses: douglascamata/setup-docker-macos-action@v1.0.0 - - name: Setup DynamoDB Local + - name: Setup DynamoDB Local uses: rrainn/dynamodb-action@v4.0.0 with: port: 8000 From 4b0c56da7cc729ec0d8aaa55338fe7a33946e864 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Tue, 29 Apr 2025 15:37:50 -0700 Subject: [PATCH 3/3] m --- TestVectors/dafny/DDBEncryption/src/TestVectors.dfy | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy index ba6588ca5..8ed52309d 100644 --- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy +++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy @@ -665,13 +665,10 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { results[i] := FullSearch(client, queries[i]); } - var configs := tableEncryptionConfigs.Keys; - while configs != {} - decreases |configs| - invariant forall k <- configs :: k in tableEncryptionConfigs + var configs := SortedSets.ComputeSetToOrderedSequence2(tableEncryptionConfigs.Keys, CharLess); + for i := 0 to |configs| { - var config :| config in configs; - configs := configs - { config }; + var config := configs[i]; BasicQueryTestConfig(tableEncryptionConfigs[config], results, globalRecords); } }