diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy index a2dfff698..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(); + 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]; diff --git a/submodules/MaterialProviders b/submodules/MaterialProviders index 952c42f1c..bb0ec0cb9 160000 --- a/submodules/MaterialProviders +++ b/submodules/MaterialProviders @@ -1 +1 @@ -Subproject commit 952c42f1c7cfad57cc9ea0115c2a0cb38164ead7 +Subproject commit bb0ec0cb959e6982cf2c154458c39865db083e84