From 776a5a100c31d1041021c6c28298ee834749825b Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Thu, 21 Aug 2025 10:28:50 -0700 Subject: [PATCH 1/4] auto commit --- .../dafny/DynamoDbEncryption/src/DynamoToStruct.dfy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy index a2dfff698..5dbcabe81 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy @@ -40,7 +40,7 @@ module DynamoToStruct { } by method { var attrNames : seq := SortedSets.ComputeSetToSequence(item.Keys); - var m := new DafnyLibraries.MutableMap(); + var m := new DafnyLibraries.MutableMap((k: seq, v: StructuredDataTerminal) => true, false); SequenceIsSafeBecauseItIsInMemory(attrNames); for i : uint64 := 0 to |attrNames| as uint64 { var k := attrNames[i]; From 4f7b718dcbd09794eeb9efdccc4ac9c0d5f040c5 Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Thu, 21 Aug 2025 10:30:18 -0700 Subject: [PATCH 2/4] auto commit --- submodules/MaterialProviders | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/submodules/MaterialProviders b/submodules/MaterialProviders index 952c42f1c..49aa27cde 160000 --- a/submodules/MaterialProviders +++ b/submodules/MaterialProviders @@ -1 +1 @@ -Subproject commit 952c42f1c7cfad57cc9ea0115c2a0cb38164ead7 +Subproject commit 49aa27cded9ab29a98c35a8748c864b86c4fece4 From c1ffe0f0afd3bfcb3a9dd76dc17b815ffa7acc1b Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Fri, 22 Aug 2025 10:37:57 -0700 Subject: [PATCH 3/4] auto commit --- submodules/MaterialProviders | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/submodules/MaterialProviders b/submodules/MaterialProviders index 49aa27cde..bb0ec0cb9 160000 --- a/submodules/MaterialProviders +++ b/submodules/MaterialProviders @@ -1 +1 @@ -Subproject commit 49aa27cded9ab29a98c35a8748c864b86c4fece4 +Subproject commit bb0ec0cb959e6982cf2c154458c39865db083e84 From e40780564db5eaf1254f745e1748b7d9c1d5401a Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Fri, 22 Aug 2025 10:58:49 -0700 Subject: [PATCH 4/4] auto commit --- .../dafny/DynamoDbEncryption/src/DynamoToStruct.dfy | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy index 5dbcabe81..8af15b5b7 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy @@ -40,7 +40,7 @@ module DynamoToStruct { } by method { var attrNames : seq := SortedSets.ComputeSetToSequence(item.Keys); - var m := new DafnyLibraries.MutableMap((k: seq, v: StructuredDataTerminal) => true, false); + var m := new DafnyLibraries.MutableMap((k: AttributeName, v: StructuredDataTerminal) => true, false); SequenceIsSafeBecauseItIsInMemory(attrNames); for i : uint64 := 0 to |attrNames| as uint64 { var k := attrNames[i]; @@ -76,7 +76,7 @@ module DynamoToStruct { } by method { var attrNames : seq := SortedSets.ComputeSetToSequence(orig.Keys); - var m := new DafnyLibraries.MutableMap(); + var m := new DafnyLibraries.MutableMap((k: AttributeName, v: AttributeValue) => true, false); SequenceIsSafeBecauseItIsInMemory(attrNames); for i : uint64 := 0 to |attrNames| as uint64 { var k := attrNames[i]; @@ -125,7 +125,7 @@ module DynamoToStruct { } by method { var attrNames : seq := SortedSets.ComputeSetToSequence(orig.Keys); - var m := new DafnyLibraries.MutableMap(); + var m := new DafnyLibraries.MutableMap((k: AttributeName, v: AttributeValue) => true, false); SequenceIsSafeBecauseItIsInMemory(attrNames); for i : uint64 := 0 to |attrNames| as uint64 { var k := attrNames[i];