Merge branch 'main' into TestExecuteStatement

Author: rishav-karanjit

.github/workflows/ci_test_vector_net.yml

@@ -97,7 +97,6 @@ jobs:
       - name: Test TestVectors on .NET 6.0
         working-directory: ./${{matrix.library}}/runtimes/net
         run: |
-          cp ../java/decrypt_java_*.json ../java/decrypt_dotnet_*.json ../java/decrypt_rust_*.json ../java/large_records.json .
-          dotnet run
           cp ../java/*.json .
+          dotnet run
           dotnet run --framework net6.0

.github/workflows/dafny_interop_test_vector_net.yml

@@ -108,7 +108,6 @@ jobs:
       - name: Test TestVectors on .NET 6.0
         working-directory: ./${{matrix.library}}/runtimes/net
         run: |
-          cp ../java/decrypt_java_*.json ../java/decrypt_dotnet_*.json ../java/decrypt_rust_*.json .
-          dotnet run
           cp ../java/*.json .
+          dotnet run
           dotnet run --framework net6.0

DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy

@@ -652,12 +652,12 @@ module DynamoToStruct {
     //= specification/dynamodb-encryption-client/ddb-attribute-serialization.md#key-value-pair-entries
     //# Entries in a serialized Map MUST be ordered by key value,
     //# ordered in ascending [UTF-16 binary order](./string-ordering.md#utf-16-binary-order).
-    var attrNames := SortedSets.ComputeSetToOrderedSequence2(m.Keys, CharLess);
+    var attrNames : seq<AttributeName> := SortedSets.ComputeSetToOrderedSequence2(m.Keys, CharLess);
     SequenceIsSafeBecauseItIsInMemory(attrNames);
     var len := |attrNames| as uint64;
     var output :- U32ToBigEndian64(len);
     for i : uint64 := 0 to len {
-      var k := attrNames[i];
+      var k : AttributeName := attrNames[i];
       var val := AttrToBytes(m[k], true, depth+1);
       if val.Failure? {
         var result := Failure(val.error);