Skip to content

Commit 8b71004

Browse files
authored
chore(dafny): improve performance of searchable encryption (#1931)
1 parent 245ad31 commit 8b71004

File tree

4 files changed

+382
-244
lines changed

4 files changed

+382
-244
lines changed

DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -652,12 +652,12 @@ module DynamoToStruct {
652652
//= specification/dynamodb-encryption-client/ddb-attribute-serialization.md#key-value-pair-entries
653653
//# Entries in a serialized Map MUST be ordered by key value,
654654
//# ordered in ascending [UTF-16 binary order](./string-ordering.md#utf-16-binary-order).
655-
var attrNames := SortedSets.ComputeSetToOrderedSequence2(m.Keys, CharLess);
655+
var attrNames : seq<AttributeName> := SortedSets.ComputeSetToOrderedSequence2(m.Keys, CharLess);
656656
SequenceIsSafeBecauseItIsInMemory(attrNames);
657657
var len := |attrNames| as uint64;
658658
var output :- U32ToBigEndian64(len);
659659
for i : uint64 := 0 to len {
660-
var k := attrNames[i];
660+
var k : AttributeName := attrNames[i];
661661
var val := AttrToBytes(m[k], true, depth+1);
662662
if val.Failure? {
663663
var result := Failure(val.error);

0 commit comments

Comments
 (0)