Merge branch 'python-poc' of github.com:aws/aws-database-encryption-sdk-dynamodb into python-poc

Author: Lucas McDonald

.github/workflows/ci_test_vector_java.yml

@@ -32,12 +32,17 @@ 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 Docker
+        if: matrix.os == 'macos-13' && matrix.library == 'TestVectors'
+        uses: douglascamata/[email protected]
+
       - name: Setup DynamoDB Local
         uses: rrainn/[email protected]
         with:

.github/workflows/ci_test_vector_net.yml

@@ -28,12 +28,17 @@ 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 Docker
+        if: matrix.os == 'macos-13' && matrix.library == 'TestVectors'
+        uses: douglascamata/[email protected]
+
       - name: Setup DynamoDB Local
         uses: rrainn/[email protected]
         with:

.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'

TestVectors/dafny/DDBEncryption/src/TestVectors.dfy

@@ -667,13 +667,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);
       }
     }