Skip to content

Commit 1d851dc

Browse files
ajewellamzajewellamz
committed
m
1 parent 07d6ebe commit 1d851dc

File tree

1 file changed

+171
-63
lines changed

1 file changed

+171
-63
lines changed

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

Lines changed: 171 additions & 63 deletions
Original file line numberDiff line numberDiff line change
@@ -12,56 +12,41 @@ module DynamoToStruct {
1212
import opened StandardLibrary
1313
import opened StandardLibrary.UInt
1414
import opened DynamoDbEncryptionUtil
15-
import AwsCryptographyDbEncryptionSdkDynamoDbTypes
15+
import Types = AwsCryptographyDbEncryptionSdkDynamoDbTypes
1616
import UTF8
1717
import SortedSets
1818
import Seq
1919
import Norm = DynamoDbNormalizeNumber
2020
import SE = StructuredEncryptionUtil
2121
import StandardLibrary.Sequence
22+
import DafnyLibraries
2223

23-
type Error = AwsCryptographyDbEncryptionSdkDynamoDbTypes.Error
24+
type Error = Types.Error
2425

2526
type TerminalDataMap = map<AttributeName, StructuredDataTerminal>
2627

27-
const UINT32_MAX : uint32 := 0xFFFF_FFFF
2828

29-
// TO BE DONE -- move to StandardLibrary
30-
function method SeqPosToUInt32(s: seq<uint8>, pos : uint32): (x: uint32)
31-
requires Add32(4,pos) as int <= |s|
32-
ensures UInt32ToSeq(x) == s[pos..pos+4]
29+
function method ItemToStructured2(item : AttributeMap, actions : Types.AttributeActions) : (ret : Result<TerminalDataMap, Error>)
3330
{
34-
var x0 := s[pos] as uint32 * 0x100_0000;
35-
var x1 := x0 + s[pos+1] as uint32 * 0x1_0000;
36-
var x2 := x1 + s[pos+2] as uint32 * 0x100;
37-
x2 + s[pos+3] as uint32
38-
}
31+
// var m := new DafnyLibraries.MutableMap<AttributeName, StructuredDataTerminal>();
32+
// return MakeError("Not valid attribute names : ");
3933

40-
function method BigEndianPosToU32(x : seq<uint8>, pos : uint32) : (ret : Result<uint32, string>)
41-
requires |x| < UINT32_MAX as int
42-
{
43-
if |x| as uint32 < Add32(pos, LENGTH_LEN32) then
44-
Failure("Length of 4-byte integer was less than 4")
45-
else
46-
Success(SeqPosToUInt32(x, pos))
34+
var structuredMap := map k <- item | k in actions && actions[k] != DO_NOTHING :: k := AttrToStructured(item[k]);
35+
MapKeysMatchItems(item);
36+
MapError(SimplifyMapValue(structuredMap))
4737
}
4838

49-
function method {:opaque} Add32(x : uint32, y : uint32) : (ret : uint32)
50-
ensures x as uint64 + y as uint64 <= UINT32_MAX as uint64
51-
ensures ret == x + y
39+
function method StructuredToItem2(s : TerminalDataMap, orig : AttributeMap, actions : Types.AttributeActions) : (ret : Result<AttributeMap, Error>)
5240
{
53-
var value : uint64 := x as uint64 + y as uint64;
54-
assume {:axiom} value <= UINT32_MAX as uint64;
55-
value as uint32
56-
}
41+
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]);
42+
MapKeysMatchItems(orig);
43+
var oldMap :- MapError(SimplifyMapValue(ddbMap));
5744

58-
function method {:opaque} Add32_3(x : uint32, y : uint32, z : uint32) : (ret : uint32)
59-
ensures x as uint64 + y as uint64 + z as uint64 <= UINT32_MAX as uint64
60-
ensures ret == x + y + z
61-
{
62-
var value : uint64 := x as uint64 + y as uint64 + z as uint64;
63-
assume {:axiom} value <= UINT32_MAX as uint64;
64-
value as uint32
45+
var ddbMap2 := map k <- s | k !in orig :: k := StructuredToAttr(s[k]);
46+
MapKeysMatchItems(s);
47+
var newMap :- MapError(SimplifyMapValue(ddbMap2));
48+
49+
Success(oldMap + newMap)
6550
}
6651

6752
// This file exists for these two functions : ItemToStructured and StructuredToItem
@@ -132,6 +117,46 @@ module DynamoToStruct {
132117

133118
// everything past here is to implement those two
134119

120+
const UINT32_MAX : uint32 := 0xFFFF_FFFF
121+
122+
// TO BE DONE -- move to StandardLibrary
123+
function method SeqPosToUInt32(s: seq<uint8>, pos : uint32): (x: uint32)
124+
requires Add32(4,pos) as int <= |s|
125+
ensures UInt32ToSeq(x) == s[pos..pos+4]
126+
{
127+
var x0 := s[pos] as uint32 * 0x100_0000;
128+
var x1 := x0 + s[pos+1] as uint32 * 0x1_0000;
129+
var x2 := x1 + s[pos+2] as uint32 * 0x100;
130+
x2 + s[pos+3] as uint32
131+
}
132+
133+
function method BigEndianPosToU32(x : seq<uint8>, pos : uint32) : (ret : Result<uint32, string>)
134+
requires |x| < UINT32_MAX as int
135+
{
136+
if |x| as uint32 < Add32(pos, LENGTH_LEN32) then
137+
Failure("Length of 4-byte integer was less than 4")
138+
else
139+
Success(SeqPosToUInt32(x, pos))
140+
}
141+
142+
function method {:opaque} Add32(x : uint32, y : uint32) : (ret : uint32)
143+
ensures x as uint64 + y as uint64 <= UINT32_MAX as uint64
144+
ensures ret == x + y
145+
{
146+
var value : uint64 := x as uint64 + y as uint64;
147+
assume {:axiom} value <= UINT32_MAX as uint64;
148+
value as uint32
149+
}
150+
151+
function method {:opaque} Add32_3(x : uint32, y : uint32, z : uint32) : (ret : uint32)
152+
ensures x as uint64 + y as uint64 + z as uint64 <= UINT32_MAX as uint64
153+
ensures ret == x + y + z
154+
{
155+
var value : uint64 := x as uint64 + y as uint64 + z as uint64;
156+
assume {:axiom} value <= UINT32_MAX as uint64;
157+
value as uint32
158+
}
159+
135160
function method MakeError<T>(s : string) : Result<T, Error> {
136161
Failure(Error.DynamoDbEncryptionException(message := s))
137162
}
@@ -527,6 +552,7 @@ module DynamoToStruct {
527552
&& U32ToBigEndian(|l|).Success?
528553
&& LENGTH_LEN <= |ret.value|
529554
&& ret.value[..LENGTH_LEN] == U32ToBigEndian(|l|).value
555+
decreases l
530556
{
531557
var count :- U32ToBigEndian(|l|);
532558
var body :- CollectList(l, depth);
@@ -675,12 +701,30 @@ module DynamoToStruct {
675701
//# A List MAY hold any DynamoDB Attribute Value data type,
676702
//# and MAY hold values of different types.
677703

704+
function {:opaque} CollectListGhost(
705+
listToSerialize : ListAttributeValue,
706+
depth : uint32,
707+
serialized : seq<uint8> := []
708+
)
709+
: (ret : Result<seq<uint8>, string>)
710+
requires depth <= MAX_STRUCTURE_DEPTH
711+
ensures (ret.Success? && |listToSerialize| == 0) ==> (ret.value == serialized)
712+
ensures (ret.Success? && |listToSerialize| == 0) ==> (|ret.value| == |serialized|)
713+
decreases listToSerialize, 1
714+
{
715+
if |listToSerialize| == 0 then
716+
Success(serialized)
717+
else
718+
var val :- AttrToBytes(listToSerialize[0], true, depth+1);
719+
CollectListGhost(listToSerialize[1..], depth, serialized + val)
720+
}
721+
678722
// Can't be {:tailrecursion} because it calls AttrToBytes which might again call CollectList
679723
// However, we really need this to loop and not recurse.
680724
// This verifies without the `by method`, but Dafny is too broken to let it verify by method
681725
// for example, a call to CollectList somehow does not satisfy the decreases clause
682726
// hence the {:verify false}
683-
function {:opaque} {:verify false} {:axiom} CollectList(
727+
function {:opaque} CollectList(
684728
listToSerialize : ListAttributeValue,
685729
depth : uint32,
686730
serialized : seq<uint8> := []
@@ -689,21 +733,26 @@ module DynamoToStruct {
689733
requires depth <= MAX_STRUCTURE_DEPTH
690734
ensures (ret.Success? && |listToSerialize| == 0) ==> (ret.value == serialized)
691735
ensures (ret.Success? && |listToSerialize| == 0) ==> (|ret.value| == |serialized|)
736+
decreases listToSerialize, 2
692737
{
693-
if |listToSerialize| == 0 then
694-
Success(serialized)
695-
else
696-
var val :- AttrToBytes(listToSerialize[0], true, depth+1);
697-
CollectList(listToSerialize[1..], depth, serialized + val)
738+
CollectListGhost(listToSerialize, depth, serialized)
698739
}
699740
by method {
741+
reveal CollectList();
742+
reveal CollectListGhost();
700743
var result := serialized;
701744
for i := 0 to |listToSerialize|
702745
{
703-
var val :- AttrToBytes(listToSerialize[i], true, depth+1);
704-
result := result + val;
746+
var val := AttrToBytes(listToSerialize[i], true, depth+1);
747+
if val.Failure? {
748+
ret := Failure(val.error);
749+
assume {:axiom} ret == CollectListGhost(listToSerialize, depth, serialized);
750+
return;
751+
}
752+
result := result + val.value;
705753
}
706-
return Success(result);
754+
ret := Success(result);
755+
assume {:axiom} ret == CollectListGhost(listToSerialize, depth, serialized);
707756
}
708757

709758
function method SerializeMapItem(key : string, value : seq<uint8>) : (ret : Result<seq<uint8>, string>)
@@ -939,13 +988,39 @@ module DynamoToStruct {
939988
Success((nResultList, new_pos))
940989
}
941990

991+
function {:vcs_split_on_every_assert} {:opaque} DeserializeListGhost(
992+
serialized : seq<uint8>,
993+
pos : uint32,
994+
orig_pos : uint32,
995+
remainingCount : uint32,
996+
depth : uint32,
997+
resultList : AttrValueAndLength
998+
)
999+
: (ret : Result<AttrValueAndLength, string>)
1000+
requires |serialized| < UINT32_MAX as int
1001+
requires pos as int <= |serialized|
1002+
requires orig_pos <= pos
1003+
requires depth <= MAX_STRUCTURE_DEPTH
1004+
requires resultList.val.L?
1005+
ensures ret.Success? ==> ret.value.val.L?
1006+
requires pos == Add32(orig_pos, resultList.len)
1007+
ensures ret.Success? ==> ret.value.len <= |serialized| as uint32 - orig_pos
1008+
decreases |serialized| as uint32 - pos, 1
1009+
{
1010+
if remainingCount == 0 then
1011+
Success(resultList)
1012+
else
1013+
var (newResultList, npos) :- DeserializeListEntry(serialized, pos, depth, resultList);
1014+
DeserializeListGhost(serialized, npos, orig_pos, remainingCount - 1, depth, newResultList)
1015+
}
1016+
9421017
// Bytes to List
9431018
// Can't be {:tailrecursion} because it calls BytesToAttr which might again call DeserializeList
9441019
// However, we really need this to loop and not recurse.
9451020
// This verifies without the `by method`, but Dafny is too broken to let it verify by method
9461021
// for example, a call to DeserializeListEntry somehow does not satisfy the decreases clause
9471022
// hence the {:verify false}
948-
function {:vcs_split_on_every_assert} {:opaque} {:verify false} DeserializeList(
1023+
function {:vcs_split_on_every_assert} {:opaque} DeserializeList(
9491024
serialized : seq<uint8>,
9501025
pos : uint32,
9511026
ghost orig_pos : uint32,
@@ -962,28 +1037,33 @@ module DynamoToStruct {
9621037
ensures ret.Success? ==> ret.value.val.L?
9631038
requires pos == Add32(orig_pos, resultList.len)
9641039
ensures ret.Success? ==> ret.value.len <= |serialized| as uint32 - orig_pos
965-
decreases |serialized| as uint32 - pos, 1
1040+
decreases |serialized| as uint32 - pos, 2
9661041
{
967-
if remainingCount == 0 then
968-
Success(resultList)
969-
else
970-
var (newResultList, npos) :- DeserializeListEntry(serialized, pos, depth, resultList);
971-
DeserializeList(serialized, npos, orig_pos, remainingCount - 1, depth, newResultList)
1042+
DeserializeListGhost(serialized, pos, orig_pos, remainingCount, depth, resultList)
9721043
}
9731044
by method {
1045+
reveal DeserializeListGhost();
1046+
reveal DeserializeList();
9741047
var npos : uint32 := pos;
9751048
var newResultList := resultList;
9761049
for i := 0 to remainingCount
9771050
invariant serialized == old(serialized)
9781051
invariant newResultList.val.L?
9791052
invariant npos as int <= |serialized|
9801053
invariant npos == Add32(orig_pos, newResultList.len)
1054+
invariant npos >= pos
9811055
{
982-
var test :- DeserializeListEntry(serialized, npos, depth, newResultList);
983-
newResultList := test.0;
984-
npos := test.1;
1056+
var test := DeserializeListEntry(serialized, npos, depth, newResultList);
1057+
if test.Failure? {
1058+
ret := Failure(test.error);
1059+
assume {:axiom} ret == DeserializeListGhost(serialized, pos, orig_pos, remainingCount, depth, resultList);
1060+
return;
1061+
}
1062+
newResultList := test.value.0;
1063+
npos := test.value.1;
9851064
}
9861065
ret := Success(newResultList);
1066+
assume {:axiom} ret == DeserializeListGhost(serialized, pos, orig_pos, remainingCount, depth, resultList);
9871067
}
9881068

9891069
function method {:vcs_split_on_every_assert} DeserializeMapEntry(
@@ -1039,14 +1119,38 @@ module DynamoToStruct {
10391119
Success((newResultMap, pos))
10401120
}
10411121

1122+
function {:vcs_split_on_every_assert} {:opaque} DeserializeMapGhost(
1123+
serialized : seq<uint8>,
1124+
pos : uint32,
1125+
orig_pos : uint32,
1126+
remainingCount : uint32,
1127+
depth : uint32,
1128+
resultMap : AttrValueAndLength)
1129+
: (ret : Result<AttrValueAndLength, string>)
1130+
requires |serialized| < UINT32_MAX as int
1131+
requires pos as int <= |serialized|
1132+
requires orig_pos <= pos
1133+
requires resultMap.val.M?
1134+
requires depth <= MAX_STRUCTURE_DEPTH
1135+
ensures ret.Success? ==> ret.value.val.M?
1136+
requires pos == Add32(orig_pos, resultMap.len)
1137+
ensures ret.Success? ==> ret.value.len <= |serialized| as uint32 - orig_pos
1138+
decreases |serialized| as uint32 - pos, 1
1139+
{
1140+
if remainingCount == 0 then
1141+
Success(resultMap)
1142+
else
1143+
var (newResultMap, npos) :- DeserializeMapEntry(serialized, pos, depth, resultMap);
1144+
DeserializeMapGhost(serialized, npos, orig_pos, remainingCount - 1, depth, newResultMap)
1145+
}
10421146

10431147
// Bytes to Map
10441148
// Can't be {:tailrecursion} because it calls BytesToAttr which might again call DeserializeMap
10451149
// However, we really need this to loop and not recurse.
10461150
// This verifies without the `by method`, but Dafny is too broken to let it verify by method
10471151
// for example, a call to DeserializeMapEntry somehow does not satisfy the decreases clause
10481152
// hence the {:verify false}
1049-
function {:vcs_split_on_every_assert} {:opaque} {:verify false} DeserializeMap(
1153+
function {:vcs_split_on_every_assert} {:opaque} DeserializeMap(
10501154
serialized : seq<uint8>,
10511155
pos : uint32,
10521156
ghost orig_pos : uint32,
@@ -1062,29 +1166,33 @@ module DynamoToStruct {
10621166
ensures ret.Success? ==> ret.value.val.M?
10631167
requires pos == Add32(orig_pos, resultMap.len)
10641168
ensures ret.Success? ==> ret.value.len <= |serialized| as uint32 - orig_pos
1065-
decreases |serialized| as uint32 - pos, 1
1169+
decreases |serialized| as uint32 - pos, 2
10661170
{
1067-
if remainingCount == 0 then
1068-
Success(resultMap)
1069-
else
1070-
var (newResultMap, npos) :- DeserializeMapEntry(serialized, pos, depth, resultMap);
1071-
DeserializeMap(serialized, npos, orig_pos, remainingCount - 1, depth, newResultMap)
1072-
1171+
DeserializeMapGhost(serialized, pos, orig_pos, remainingCount, depth, resultMap)
10731172
}
10741173
by method {
1174+
reveal DeserializeMapGhost();
1175+
reveal DeserializeMap();
10751176
var npos : uint32 := pos;
10761177
var newResultMap := resultMap;
10771178
for i := 0 to remainingCount
10781179
invariant serialized == old(serialized)
10791180
invariant newResultMap.val.M?
10801181
invariant npos as int <= |serialized|
10811182
invariant npos == Add32(orig_pos, newResultMap.len)
1183+
invariant npos >= pos
10821184
{
1083-
var test :- DeserializeMapEntry(serialized, npos, depth, newResultMap);
1084-
newResultMap := test.0;
1085-
npos := test.1;
1185+
var test := DeserializeMapEntry(serialized, npos, depth, newResultMap);
1186+
if test.Failure? {
1187+
ret := Failure(test.error);
1188+
assume {:axiom} ret == DeserializeMapGhost(serialized, pos, orig_pos, remainingCount, depth, resultMap);
1189+
return;
1190+
}
1191+
newResultMap := test.value.0;
1192+
npos := test.value.1;
10861193
}
10871194
ret := Success(newResultMap);
1195+
assume {:axiom} ret == DeserializeMapGhost(serialized, pos, orig_pos, remainingCount, depth, resultMap);
10881196
}
10891197

10901198
// Bytes to AttributeValue

0 commit comments

Comments
 (0)