auto commit

rishav-karanjit · rishav-karanjit · commit 776a5a100c31 · 2025-08-21T10:28:50.000-07:00
diff --git 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<AttributeName> := SortedSets.ComputeSetToSequence(item.Keys);
-    var m := new DafnyLibraries.MutableMap<AttributeName, StructuredDataTerminal>();
+    var m := new DafnyLibraries.MutableMap<AttributeName, StructuredDataTerminal>((k: seq<AttributeName>, v: StructuredDataTerminal) => true, false);
     SequenceIsSafeBecauseItIsInMemory(attrNames);
     for i : uint64 := 0 to |attrNames| as uint64 {
       var k := attrNames[i];

Original file line number	Diff line number	Diff line change
`@@ -40,7 +40,7 @@ module DynamoToStruct {`
`40`	`40`	`}`
`41`	`41`	`by method {`
`42`	`42`	`var attrNames : seq<AttributeName> := SortedSets.ComputeSetToSequence(item.Keys);`
`43`		`- var m := new DafnyLibraries.MutableMap<AttributeName, StructuredDataTerminal>();`
	`43`	`+ var m := new DafnyLibraries.MutableMap<AttributeName, StructuredDataTerminal>((k: seq<AttributeName>, v: StructuredDataTerminal) => true, false);`
`44`	`44`	`SequenceIsSafeBecauseItIsInMemory(attrNames);`
`45`	`45`	`for i : uint64 := 0 to \|attrNames\| as uint64 {`
`46`	`46`	`var k := attrNames[i];`