Skip to content

Commit e9ea870

Browse files
chore(dafny): bump MPL and update mutable map (#1974)
1 parent b373067 commit e9ea870

File tree

2 files changed

+4
-4
lines changed

2 files changed

+4
-4
lines changed

DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -40,7 +40,7 @@ module DynamoToStruct {
4040
}
4141
by method {
4242
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: AttributeName, v: StructuredDataTerminal) => true, false);
4444
SequenceIsSafeBecauseItIsInMemory(attrNames);
4545
for i : uint64 := 0 to |attrNames| as uint64 {
4646
var k := attrNames[i];
@@ -76,7 +76,7 @@ module DynamoToStruct {
7676
}
7777
by method {
7878
var attrNames : seq<AttributeName> := SortedSets.ComputeSetToSequence(orig.Keys);
79-
var m := new DafnyLibraries.MutableMap<AttributeName, AttributeValue>();
79+
var m := new DafnyLibraries.MutableMap<AttributeName, AttributeValue>((k: AttributeName, v: AttributeValue) => true, false);
8080
SequenceIsSafeBecauseItIsInMemory(attrNames);
8181
for i : uint64 := 0 to |attrNames| as uint64 {
8282
var k := attrNames[i];
@@ -125,7 +125,7 @@ module DynamoToStruct {
125125
}
126126
by method {
127127
var attrNames : seq<AttributeName> := SortedSets.ComputeSetToSequence(orig.Keys);
128-
var m := new DafnyLibraries.MutableMap<AttributeName, AttributeValue>();
128+
var m := new DafnyLibraries.MutableMap<AttributeName, AttributeValue>((k: AttributeName, v: AttributeValue) => true, false);
129129
SequenceIsSafeBecauseItIsInMemory(attrNames);
130130
for i : uint64 := 0 to |attrNames| as uint64 {
131131
var k := attrNames[i];

0 commit comments

Comments
 (0)