Commit e9ea870

authored

chore(dafny): bump MPL and update mutable map (#1974)

1 parent b373067 commit e9ea870Copy full SHA for e9ea870

File tree

2 files changed

-4

lines changed

DynamoDbEncryption/dafny/DynamoDbEncryption/src
- DynamoToStruct.dfy
submodules
- MaterialProviders

2 files changed

-4

lines changed

`‎DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy`

Lines changed: 3 additions & 3 deletions

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: 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];`
`@@ -76,7 +76,7 @@ module DynamoToStruct {`
`76`	`76`	`}`
`77`	`77`	`by method {`
`78`	`78`	`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);`
`80`	`80`	`SequenceIsSafeBecauseItIsInMemory(attrNames);`
`81`	`81`	`for i : uint64 := 0 to \|attrNames\| as uint64 {`
`82`	`82`	`var k := attrNames[i];`
`@@ -125,7 +125,7 @@ module DynamoToStruct {`
`125`	`125`	`}`
`126`	`126`	`by method {`
`127`	`127`	`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);`
`129`	`129`	`SequenceIsSafeBecauseItIsInMemory(attrNames);`
`130`	`130`	`for i : uint64 := 0 to \|attrNames\| as uint64 {`
`131`	`131`	`var k := attrNames[i];`

`‎submodules/MaterialProviders`

Submodule MaterialProviders updated from 952c42f to bb0ec0c

0 commit comments

Comments

(0)

Navigation Menu

Search code, repositories, users, issues, pull requests...

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Commit e9ea870

File tree

2 files changed

2 files changed

`‎DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy`

`‎submodules/MaterialProviders`

0 commit comments