Skip to content

Commit ccf61d6

Browse files
ajewellamzajewellamz
authored
chore(dafny): improve performance (#1900)
1 parent f2997be commit ccf61d6

File tree

2 files changed

+141
-12
lines changed

2 files changed

+141
-12
lines changed

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

+140-11
Original file line numberDiff line numberDiff line change
@@ -32,20 +32,37 @@ module DynamoToStruct {
3232

3333
// Identical to ItemToStructured, except that the result does not include any attributes configured as DO_NOTHING\
3434
// Such attributes are unneeded, as they do not partake in signing nor encryption
35-
function method ItemToStructured2(item : AttributeMap, actions : Types.AttributeActions) : (ret : Result<TerminalDataMap, Error>)
35+
function ItemToStructured2(item : AttributeMap, actions : Types.AttributeActions) : (ret : Result<TerminalDataMap, Error>)
3636
{
37-
// var m := new DafnyLibraries.MutableMap<AttributeName, StructuredDataTerminal>();
38-
// return MakeError("Not valid attribute names : ");
39-
4037
var structuredMap := map k <- item | k !in actions || actions[k] != DO_NOTHING || ReservedPrefix <= k :: k := AttrToStructured(item[k]);
4138
MapKeysMatchItems(item);
4239
MapError(SimplifyMapValue(structuredMap))
4340
}
41+
by method {
42+
var attrNames : seq<AttributeName> := SortedSets.ComputeSetToSequence(item.Keys);
43+
var m := new DafnyLibraries.MutableMap<AttributeName, StructuredDataTerminal>();
44+
SequenceIsSafeBecauseItIsInMemory(attrNames);
45+
for i : uint64 := 0 to |attrNames| as uint64 {
46+
var k := attrNames[i];
47+
if k !in actions || actions[k] != DO_NOTHING || ReservedPrefix <= k {
48+
var val := AttrToStructured(item[k]);
49+
if val.Failure? {
50+
var result := Failure(E(val.error));
51+
assume {:axiom} ItemToStructured2(item, actions) == result;
52+
return result;
53+
}
54+
m.Put(k, val.value);
55+
}
56+
}
57+
var result := Success(m.content());
58+
assume {:axiom} ItemToStructured2(item, actions) == result;
59+
return result;
60+
}
4461

4562
// Identical to StructuredToItem, except that any non encrypted fields in the original are passed through unchanged
4663
// and only encrypted fields are run through StructuredToAttr
4764
// This one is used for encryption, and so anything in s but not in orig is also kept
48-
function method StructuredToItemEncrypt(s : TerminalDataMap, orig : AttributeMap, actions : CryptoSchemaMap) : (ret : Result<AttributeMap, Error>)
65+
function StructuredToItemEncrypt(s : TerminalDataMap, orig : AttributeMap, actions : CryptoSchemaMap) : (ret : Result<AttributeMap, Error>)
4966
{
5067
var ddbMap := map k <- orig :: k := if (k in s && k in actions && actions[k] == ENCRYPT_AND_SIGN) then StructuredToAttr(s[k]) else Success(orig[k]);
5168
MapKeysMatchItems(orig);
@@ -57,16 +74,79 @@ module DynamoToStruct {
5774

5875
Success(oldMap + newMap)
5976
}
77+
by method {
78+
var attrNames : seq<AttributeName> := SortedSets.ComputeSetToSequence(orig.Keys);
79+
var m := new DafnyLibraries.MutableMap<AttributeName, AttributeValue>();
80+
SequenceIsSafeBecauseItIsInMemory(attrNames);
81+
for i : uint64 := 0 to |attrNames| as uint64 {
82+
var k := attrNames[i];
83+
if !(ReservedPrefix <= k) {
84+
if (k in s && k in actions && actions[k] == ENCRYPT_AND_SIGN) {
85+
var val := StructuredToAttr(s[k]);
86+
if val.Failure? {
87+
var result := Failure(E(val.error));
88+
assume {:axiom} StructuredToItemEncrypt(s, orig, actions) == result;
89+
return result;
90+
}
91+
m.Put(k, val.value);
92+
} else {
93+
m.Put(k, orig[k]);
94+
}
95+
}
96+
}
97+
attrNames := SortedSets.ComputeSetToSequence(s.Keys);
98+
SequenceIsSafeBecauseItIsInMemory(attrNames);
99+
for i : uint64 := 0 to |attrNames| as uint64 {
100+
var k := attrNames[i];
101+
if k !in orig {
102+
var val := StructuredToAttr(s[k]);
103+
if val.Failure? {
104+
var result := Failure(E(val.error));
105+
assume {:axiom} StructuredToItemEncrypt(s, orig, actions) == result;
106+
return result;
107+
}
108+
m.Put(k, val.value);
109+
}
110+
}
111+
112+
var result := Success(m.content());
113+
assume {:axiom} StructuredToItemEncrypt(s, orig, actions) == result;
114+
return result;
115+
}
60116

61117
// Identical to StructuredToItem, except that any non encrypted fields in the original are passed through unchanged
62118
// and only encrypted fields are run through StructuredToAttr\
63119
// This one is used for decryption, and so anything in s but not in orig is ignored
64-
function method StructuredToItemDecrypt(s : TerminalDataMap, orig : AttributeMap, actions : CryptoSchemaMap) : (ret : Result<AttributeMap, Error>)
120+
function StructuredToItemDecrypt(s : TerminalDataMap, orig : AttributeMap, actions : CryptoSchemaMap) : (ret : Result<AttributeMap, Error>)
65121
{
66122
var ddbMap := map k <- orig | !(ReservedPrefix <= k) :: k := if (k in s && k in actions && actions[k] == ENCRYPT_AND_SIGN) then StructuredToAttr(s[k]) else Success(orig[k]);
67123
MapKeysMatchItems(orig);
68124
MapError(SimplifyMapValue(ddbMap))
69125
}
126+
by method {
127+
var attrNames : seq<AttributeName> := SortedSets.ComputeSetToSequence(orig.Keys);
128+
var m := new DafnyLibraries.MutableMap<AttributeName, AttributeValue>();
129+
SequenceIsSafeBecauseItIsInMemory(attrNames);
130+
for i : uint64 := 0 to |attrNames| as uint64 {
131+
var k := attrNames[i];
132+
if !(ReservedPrefix <= k) {
133+
if (k in s && k in actions && actions[k] == ENCRYPT_AND_SIGN) {
134+
var val := StructuredToAttr(s[k]);
135+
if val.Failure? {
136+
var result := Failure(E(val.error));
137+
assume {:axiom} StructuredToItemDecrypt(s, orig, actions) == result;
138+
return result;
139+
}
140+
m.Put(k, val.value);
141+
} else {
142+
m.Put(k, orig[k]);
143+
}
144+
}
145+
}
146+
var result := Success(m.content());
147+
assume {:axiom} StructuredToItemDecrypt(s, orig, actions) == result;
148+
return result;
149+
}
70150

71151
// Convert AttributeMap to StructuredDataMap
72152
function method {:opaque} ItemToStructured(item : AttributeMap) : (ret : Result<TerminalDataMap, Error>)
@@ -520,13 +600,15 @@ module DynamoToStruct {
520600
Success(count + body)
521601
}
522602

523-
// Specifying the parent (particularly, as the first parameter),
524-
// along with the corresponding precondition,
525-
// lets Dafny find the correct termination metric.
526-
// See "The Parent Trick" for details: <https://leino.science/papers/krml283.html>.
527-
function method MapAttrToBytes(ghost parent: AttributeValue, m: MapAttributeValue, depth : uint64): (ret: Result<seq<uint8>, string>)
603+
function MapAttrToBytesGhost(parent: AttributeValue, m: MapAttributeValue, depth : uint64): (ret: Result<seq<uint8>, string>)
528604
requires forall k <- m :: m[k] < parent
529605
requires depth <= MAX_STRUCTURE_DEPTH
606+
decreases parent, 1
607+
ensures ret.Success? ==>
608+
&& U32ToBigEndian(|m|).Success?
609+
&& |ret.value| >= LENGTH_LEN
610+
&& (|m| == 0 ==> |ret.value| == LENGTH_LEN)
611+
&& ret.value[0..LENGTH_LEN] == U32ToBigEndian(|m|).value
530612
{
531613
//= specification/dynamodb-encryption-client/ddb-attribute-serialization.md#value-type
532614
//# Value Type MUST be the [Type ID](#type-id) of the type of [Map Value](#map-value).
@@ -550,6 +632,53 @@ module DynamoToStruct {
550632
Success(count + body)
551633
}
552634

635+
// Specifying the parent (particularly, as the first parameter),
636+
// along with the corresponding precondition,
637+
// lets Dafny find the correct termination metric.
638+
// See "The Parent Trick" for details: <https://leino.science/papers/krml283.html>.
639+
function MapAttrToBytes(parent: AttributeValue, m: MapAttributeValue, depth : uint64): (ret: Result<seq<uint8>, string>)
640+
requires forall k <- m :: m[k] < parent
641+
requires depth <= MAX_STRUCTURE_DEPTH
642+
decreases parent, 2
643+
ensures ret.Success? ==>
644+
&& U32ToBigEndian(|m|).Success?
645+
&& |ret.value| >= LENGTH_LEN
646+
&& (|m| == 0 ==> |ret.value| == LENGTH_LEN)
647+
&& ret.value[0..LENGTH_LEN] == U32ToBigEndian(|m|).value
648+
{
649+
MapAttrToBytesGhost(parent, m, depth)
650+
}
651+
by method {
652+
//= specification/dynamodb-encryption-client/ddb-attribute-serialization.md#key-value-pair-entries
653+
//# Entries in a serialized Map MUST be ordered by key value,
654+
//# ordered in ascending [UTF-16 binary order](./string-ordering.md#utf-16-binary-order).
655+
var attrNames := SortedSets.ComputeSetToOrderedSequence2(m.Keys, CharLess);
656+
SequenceIsSafeBecauseItIsInMemory(attrNames);
657+
var len := |attrNames| as uint64;
658+
var output :- U32ToBigEndian64(len);
659+
for i : uint64 := 0 to len {
660+
var k := attrNames[i];
661+
var val := AttrToBytes(m[k], true, depth+1);
662+
if val.Failure? {
663+
var result := Failure(val.error);
664+
assume {:axiom} MapAttrToBytesGhost(parent, m, depth) == result;
665+
return result;
666+
}
667+
var data := SerializeMapItem(k, val.value);
668+
if data.Failure? {
669+
var result := Failure(data.error);
670+
assume {:axiom} MapAttrToBytesGhost(parent, m, depth) == result;
671+
return result;
672+
}
673+
output := output + data.value;
674+
}
675+
676+
var result := Success(output);
677+
assume {:axiom} MapAttrToBytesGhost(parent, m, depth) == result;
678+
return result;
679+
}
680+
681+
553682
function method ListAttrToBytes(l: ListAttributeValue, depth : uint64): (ret: Result<seq<uint8>, string>)
554683
requires depth <= MAX_STRUCTURE_DEPTH
555684
ensures ret.Success? ==>

‎submodules/MaterialProviders

0 commit comments

Comments
 (0)