Skip to content

Commit a0b4787

Browse files
ajewellamzajewellamz
committed
m
1 parent 8daf0d5 commit a0b4787

File tree

7 files changed

+65
-34
lines changed

7 files changed

+65
-34
lines changed

‎DynamoDbEncryption/dafny/DynamoDbEncryption/src/CompoundBeacon.dfy

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,7 @@ module CompoundBeacon {
2020
import UTF8
2121
import Seq
2222
import SortedSets
23+
import StandardLibrary.Sequence
2324

2425
type Prefix = x : string | 0 < |x| witness *
2526

@@ -289,7 +290,7 @@ module CompoundBeacon {
289290
// return all the fields involved in this beacon
290291
function method GetFields(virtualFields : VirtualFieldMap) : seq<string>
291292
{
292-
Seq.Flatten(Seq.Map((p : BeaconPart) => p.GetFields(virtualFields), parts))
293+
Sequence.Flatten(Seq.Map((p : BeaconPart) => p.GetFields(virtualFields), parts))
293294
}
294295

295296
// calculate value for a single piece of a compound beacon query string
@@ -315,9 +316,9 @@ module CompoundBeacon {
315316
Failure(E("CompoundBeacon " + base.name + " can only be queried as a string, not as " + AttrTypeToStr(value)))
316317
else
317318
var parts := Split(value.S, split);
318-
var partsUsed :- Seq.MapWithResult(s => getPartFromPrefix(s), parts);
319+
var partsUsed :- Sequence.MapWithResult(s => getPartFromPrefix(s), parts);
319320
var _ :- ValidatePartOrder(partsUsed, value.S);
320-
var beaconParts :- Seq.MapWithResult(s => FindAndCalcPart(s, keys), parts);
321+
var beaconParts :- Sequence.MapWithResult(s => FindAndCalcPart(s, keys), parts);
321322
var lastIsPrefix :- justPrefix(Seq.Last(parts));
322323
if !forEquality && lastIsPrefix then
323324
var result := Join(beaconParts[..|parts|-1] + [Seq.Last(parts)], [split]);
@@ -534,7 +535,7 @@ module CompoundBeacon {
534535
requires pos < |parts|
535536
{
536537
var partNumbers : seq<nat> := seq(|parts|, (i : nat) => i as nat);
537-
var _ :- Seq.MapWithResult((p : int) requires 0 <= p < |parts| => CheckOnePrefixPart(pos, p), seq(|parts|, i => i));
538+
var _ :- Sequence.MapWithResult((p : int) requires 0 <= p < |parts| => CheckOnePrefixPart(pos, p), seq(|parts|, i => i));
538539
Success(true)
539540
}
540541

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

Lines changed: 30 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@ module DynamoToStruct {
1818
import Seq
1919
import Norm = DynamoDbNormalizeNumber
2020
import SE = StructuredEncryptionUtil
21+
import StandardLibrary.Sequence
2122

2223
type Error = AwsCryptographyDbEncryptionSdkDynamoDbTypes.Error
2324

@@ -437,7 +438,7 @@ module DynamoToStruct {
437438
:- Need(|asSet| == |ns|, "Number Set had duplicate values");
438439
Seq.LemmaNoDuplicatesCardinalityOfSet(ns);
439440

440-
var normList :- Seq.MapWithResult(n => Norm.NormalizeNumber(n), ns);
441+
var normList :- Sequence.MapWithResult(n => Norm.NormalizeNumber(n), ns);
441442
var asSet := Seq.ToSet(normList);
442443
:- Need(|asSet| == |normList|, "Number Set had duplicate values after normalization.");
443444

@@ -454,6 +455,10 @@ module DynamoToStruct {
454455

455456
function method BinarySetAttrToBytes(bs: BinarySetAttributeValue): (ret: Result<seq<uint8>, string>)
456457
ensures ret.Success? ==> Seq.HasNoDuplicates(bs)
458+
ensures ret.Success? ==>
459+
&& U32ToBigEndian(|bs|).Success?
460+
&& LENGTH_LEN <= |ret.value|
461+
&& ret.value[..LENGTH_LEN] == U32ToBigEndian(|bs|).value
457462
{
458463
var asSet := Seq.ToSet(bs);
459464
:- Need(|asSet| == |bs|, "Binary Set had duplicate values");
@@ -561,14 +566,17 @@ module DynamoToStruct {
561566
// String Set or Number Set to Bytes
562567
function method {:tailrecursion} {:opaque} CollectString(
563568
setToSerialize : StringSetAttributeValue,
569+
pos : nat := 0,
564570
serialized : seq<uint8> := [])
565571
: Result<seq<uint8>, string>
572+
requires pos <= |setToSerialize|
573+
decreases |setToSerialize| - pos
566574
{
567-
if |setToSerialize| == 0 then
575+
if |setToSerialize| == pos then
568576
Success(serialized)
569577
else
570-
var entry :- EncodeString(setToSerialize[0]);
571-
CollectString(setToSerialize[1..], serialized + entry)
578+
var entry :- EncodeString(setToSerialize[pos]);
579+
CollectString(setToSerialize, pos+1, serialized + entry)
572580
}
573581

574582

@@ -596,13 +604,19 @@ module DynamoToStruct {
596604
}
597605

598606
// Binary Set to Bytes
599-
function method {:tailrecursion} CollectBinary(setToSerialize : BinarySetAttributeValue, serialized : seq<uint8> := []) : Result<seq<uint8>, string>
607+
function method {:tailrecursion} CollectBinary(
608+
setToSerialize : BinarySetAttributeValue,
609+
pos : nat := 0,
610+
serialized : seq<uint8> := []
611+
) : Result<seq<uint8>, string>
612+
requires pos <= |setToSerialize|
613+
decreases |setToSerialize| - pos
600614
{
601-
if |setToSerialize| == 0 then
615+
if |setToSerialize| == pos then
602616
Success(serialized)
603617
else
604-
var item :- SerializeBinaryValue(setToSerialize[0]);
605-
CollectBinary(setToSerialize[1..], serialized + item)
618+
var item :- SerializeBinaryValue(setToSerialize[pos]);
619+
CollectBinary(setToSerialize, pos+1, serialized + item)
606620
}
607621

608622
// List to Bytes
@@ -641,6 +655,7 @@ module DynamoToStruct {
641655
if |listToSerialize| == 0 then
642656
Success(serialized)
643657
else
658+
// Can't do the `pos` optimization, because I can't appease the `decreases`
644659
var val :- AttrToBytes(listToSerialize[0], true, depth+1);
645660
CollectList(listToSerialize[1..], depth, serialized + val)
646661
}
@@ -705,24 +720,27 @@ module DynamoToStruct {
705720
//# Entries in a serialized Map MUST be ordered by key value,
706721
//# ordered in ascending [UTF-16 binary order](./string-ordering.md#utf-16-binary-order).
707722
var keys := SortedSets.ComputeSetToOrderedSequence2(mapToSerialize.Keys, CharLess);
708-
CollectOrderedMapSubset(keys, mapToSerialize, serialized)
723+
CollectOrderedMapSubset(keys, mapToSerialize, 0, serialized)
709724
}
710725

711726
function method {:tailrecursion} {:opaque} CollectOrderedMapSubset(
712727
keys : seq<AttributeName>,
713728
mapToSerialize : map<AttributeName, seq<uint8>>,
729+
pos : nat := 0,
714730
serialized : seq<uint8> := []
715731
)
716732
: (ret : Result<seq<uint8>, string>)
733+
requires pos <= |keys|
717734
requires forall k <- keys :: k in mapToSerialize
718735
ensures (ret.Success? && |keys| == 0) ==> (ret.value == serialized)
719736
ensures (ret.Success? && |keys| == 0) ==> (|ret.value| == |serialized|)
737+
decreases |keys| - pos
720738
{
721-
if |keys| == 0 then
739+
if |keys| == pos then
722740
Success(serialized)
723741
else
724-
var data :- SerializeMapItem(keys[0], mapToSerialize[keys[0]]);
725-
CollectOrderedMapSubset(keys[1..], mapToSerialize, serialized + data)
742+
var data :- SerializeMapItem(keys[pos], mapToSerialize[keys[pos]]);
743+
CollectOrderedMapSubset(keys, mapToSerialize, pos+1, serialized + data)
726744
}
727745

728746
function method BoolToUint8(b : bool) : uint8

‎DynamoDbEncryption/dafny/DynamoDbEncryption/src/FilterExpr.dfy

Lines changed: 13 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -1271,25 +1271,27 @@ module DynamoDBFilterExpr {
12711271
// If only surrogates are involved, comparison is normal
12721272
// if one surrogate is involved, the surrogate is larger
12731273
// results undefined if not valid UTF16 encodings, but the idea of 'less' is also undefined for invalid encodings.
1274-
predicate method {:tailrecursion} UnicodeLess(a : string, b : string)
1274+
predicate method {:tailrecursion} UnicodeLess(a : string, b : string, pos : nat := 0)
1275+
requires pos <= |a|
1276+
requires pos <= |b|
1277+
decreases |a| - pos
12751278
{
1276-
if |a| == 0 && |b| == 0 then
1279+
if |a| == pos && |b| == pos then
12771280
false
1278-
else if |a| == 0 then
1281+
else if |a| == pos then
12791282
true
1280-
else if |b| == 0 then
1283+
else if |b| == pos then
12811284
false
1285+
else if a[pos] == b[pos] then
1286+
UnicodeLess(a, b, pos+1) // correct independent of surrogate status
12821287
else
1283-
if a[0] == b[0] then
1284-
UnicodeLess(a[1..], b[1..]) // correct independent of surrogate status
1285-
else
1286-
var aIsHighSurrogate := IsHighSurrogate(a[0]);
1287-
var bIsHighSurrogate := IsHighSurrogate(b[0]);
1288+
var aIsHighSurrogate := IsHighSurrogate(a[pos]);
1289+
var bIsHighSurrogate := IsHighSurrogate(b[pos]);
12881290
if aIsHighSurrogate == bIsHighSurrogate then
1289-
a[0] < b[0]
1291+
a[pos] < b[pos]
12901292
else
12911293
bIsHighSurrogate
1292-
// we know aIsHighSurrogate != bIsHighSurrogate and a[0] != b[0]
1294+
// we know aIsHighSurrogate != bIsHighSurrogate and a[pos] != b[pos]
12931295
// so if bIsHighSurrogate then a is less
12941296
// and if aIsHighSurrogate then a is greater
12951297
}

‎DynamoDbEncryption/dafny/DynamoDbEncryption/src/Virtual.dfy

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,11 +23,12 @@ module DdbVirtualFields {
2323
import DDB = ComAmazonawsDynamodbTypes
2424
import Seq
2525
import TermLoc
26+
import StandardLibrary.Sequence
2627

2728

2829
function method ParseVirtualFieldConfig(vf : VirtualField) : Result<VirtField, Error>
2930
{
30-
var parts :- Seq.MapWithResult((p : VirtualPart) => ParseVirtualPartConfig(p), vf.parts);
31+
var parts :- Sequence.MapWithResult((p : VirtualPart) => ParseVirtualPartConfig(p), vf.parts);
3132
Success(VirtField(vf.name, parts))
3233
}
3334

‎DynamoDbEncryption/dafny/StructuredEncryption/src/Header.dfy

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -821,11 +821,11 @@ module StructuredEncryptionHeader {
821821
}
822822

823823
// GetOneKVPair ==> SerializeOneKVPair
824-
lemma GetOneKVPairRoundTrip(data : Bytes)
825-
requires GetOneKVPair(data, 0).Success?
824+
lemma GetOneKVPairRoundTrip(data : Bytes, pos : nat)
825+
requires GetOneKVPair(data, pos).Success?
826826
ensures
827-
&& var cont := GetOneKVPair(data, 0).value;
828-
&& SerializeOneKVPair(cont.0, cont.1) == data[..cont.2]
827+
&& var cont := GetOneKVPair(data, pos).value;
828+
&& SerializeOneKVPair(cont.0, cont.1) == data[pos..cont.2+pos]
829829
{}
830830

831831
// SerializeOneDataKey ==> GetOneDataKey

‎TestVectors/dafny/DDBEncryption/src/DecryptManifest.dfy

Lines changed: 10 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,7 @@ module {:options "-functionSyntax:4"} DecryptManifest {
2121
import JsonConfig
2222
import ENC = AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes
2323
import KeyVectors
24+
import OsLang
2425

2526
method OnePositiveTest(name : string, config : JSON, encrypted : JSON, plaintext : JSON, keys : KeyVectors.KeyVectorsClient)
2627
returns (output : Result<bool, string>)
@@ -110,6 +111,14 @@ module {:options "-functionSyntax:4"} DecryptManifest {
110111
}
111112
}
112113

114+
function LogFileName() : string
115+
{
116+
if OsLang.GetOsShort() == "Windows" && OsLang.GetLanguageShort() == "Dotnet" then
117+
"..\\..\\PerfLog.txt"
118+
else
119+
"../../PerfLog.txt"
120+
}
121+
113122
method Decrypt(inFile : string, keyVectors: KeyVectors.KeyVectorsClient)
114123
returns (output : Result<bool, string>)
115124
requires keyVectors.ValidState()
@@ -174,7 +183,7 @@ module {:options "-functionSyntax:4"} DecryptManifest {
174183
:- Need(obj.1.Object?, "Value of test '" + obj.0 + "' must be an Object.");
175184
var _ :- OneTest(obj.0, obj.1, keyVectors);
176185
}
177-
Time.PrintTimeSinceLong(time, "DB-ESDK-TV " + inFile);
186+
Time.PrintTimeSinceLong(time, "DB-ESDK-TV-Decrypt-" + inFile, Some(LogFileName()));
178187

179188
timeStamp :- expect Time.GetCurrentTimeStamp();
180189
print timeStamp + " Tests Complete.\n";

‎submodules/MaterialProviders

0 commit comments

Comments
 (0)