Skip to content

Commit 8ca2883

Browse files
ajewellamzajewellamz
authored
chore: improve performance (#1622)
1 parent c67e3c9 commit 8ca2883

30 files changed

+1487
-302
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/DynamoDbEncryption/test/Beacon.dfy‎

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,11 @@ module TestBaseBeacon {
1818
import DDB = ComAmazonawsDynamodbTypes
1919
import SE = AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes
2020

21+
const x123 : UTF8.ValidUTF8Bytes :=
22+
var s := [0x31, 0x32, 0x33];
23+
assert s == UTF8.EncodeAscii("123");
24+
s
25+
2126
method {:test} TestBeacon() {
2227
var primitives :- expect Primitives.AtomicPrimitives();
2328

@@ -31,7 +36,7 @@ module TestBaseBeacon {
3136
expect bytes[7] == 0x80;
3237
str :- expect b.hash([], key := [1,2]);
3338
expect str == "80";
34-
bytes :- expect bb.getHmac(UTF8.EncodeAscii("123"), key := [1,2]);
39+
bytes :- expect bb.getHmac(x123, key := [1,2]);
3540
expect bytes[7] == 0x61;
3641
}
3742

‎DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoDbEncryptionBranchKeyIdSupplierTest.dfy‎

Lines changed: 22 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,12 @@ module DynamoDbEncryptionBranchKeyIdSupplierTest {
2727

2828
// These tests require a keystore populated with a key with this Id
2929
const BRANCH_KEY_ID := "3f43a9af-08c5-4317-b694-3d3e883dcaef"
30-
const BRANCH_KEY_ID_UTF8 := UTF8.EncodeAscii(BRANCH_KEY_ID)
30+
31+
const BRANCH_KEY_ID_UTF8 : UTF8.ValidUTF8Bytes :=
32+
var s := [0x33, 0x66, 0x34, 0x33, 0x61, 0x39, 0x61, 0x66, 0x2d, 0x30, 0x38, 0x63, 0x35, 0x2d, 0x34, 0x33, 0x31, 0x37, 0x2d, 0x62, 0x36, 0x39, 0x34, 0x2d, 0x33, 0x64, 0x33, 0x65, 0x38, 0x38, 0x33, 0x64, 0x63, 0x61, 0x65, 0x66];
33+
assert s == UTF8.EncodeAscii("3f43a9af-08c5-4317-b694-3d3e883dcaef");
34+
s
35+
3136
const ALTERNATE_BRANCH_KEY_ID := "4bb57643-07c1-419e-92ad-0df0df149d7c"
3237

3338
// Constants for TestBranchKeySupplier
@@ -41,10 +46,23 @@ module DynamoDbEncryptionBranchKeyIdSupplierTest {
4146
const CASE_B_BYTES: seq<uint8> := STRING_TYPE_ID + [0x43, 0x41, 0x53, 0x45, 0x5f, 0x42]
4247
const BRANCH_KEY_ID_A := BRANCH_KEY_ID
4348
const BRANCH_KEY_ID_B := ALTERNATE_BRANCH_KEY_ID
44-
const EC_PARTITION_NAME := UTF8.EncodeAscii("aws-crypto-partition-name")
49+
50+
const EC_PARTITION_NAME : UTF8.ValidUTF8Bytes :=
51+
var s := [0x61, 0x77, 0x73, 0x2d, 0x63, 0x72, 0x79, 0x70, 0x74, 0x6f, 0x2d, 0x70, 0x61, 0x72, 0x74, 0x69, 0x74, 0x69, 0x6f, 0x6e, 0x2d, 0x6e, 0x61, 0x6d, 0x65];
52+
assert s == UTF8.EncodeAscii("aws-crypto-partition-name");
53+
s
54+
4555
const RESERVED_PREFIX := "aws-crypto-attr."
46-
const KEY_ATTR_NAME := UTF8.EncodeAscii(RESERVED_PREFIX + BRANCH_KEY)
47-
const BRANCH_KEY_NAME := UTF8.EncodeAscii(BRANCH_KEY)
56+
57+
const KEY_ATTR_NAME : UTF8.ValidUTF8Bytes :=
58+
var s := [0x61, 0x77, 0x73, 0x2d, 0x63, 0x72, 0x79, 0x70, 0x74, 0x6f, 0x2d, 0x61, 0x74, 0x74, 0x72, 0x2e, 0x62, 0x72, 0x61, 0x6e, 0x63, 0x68, 0x4b, 0x65, 0x79];
59+
assert s == UTF8.EncodeAscii(RESERVED_PREFIX + BRANCH_KEY);
60+
s
61+
62+
const BRANCH_KEY_NAME : UTF8.ValidUTF8Bytes :=
63+
var s := [0x62, 0x72, 0x61, 0x6e, 0x63, 0x68, 0x4b, 0x65, 0x79];
64+
assert s == UTF8.EncodeAscii(BRANCH_KEY);
65+
s
4866

4967
method {:test} {:vcs_split_on_every_assert} TestHappyCase()
5068
{

‎DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoDbGetEncryptedDataKeyDescriptionTest.dfy‎

Lines changed: 43 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -14,20 +14,55 @@ module DynamoDbGetEncryptedDataKeyDescriptionTest {
1414
import EdkWrapping
1515
import AlgorithmSuites
1616

17+
const abc : UTF8.ValidUTF8Bytes :=
18+
var s := [0x61, 0x62, 0x63];
19+
assert s == UTF8.EncodeAscii("abc");
20+
s
21+
22+
const def : UTF8.ValidUTF8Bytes :=
23+
var s := [0x64, 0x65, 0x66];
24+
assert s == UTF8.EncodeAscii("def");
25+
s
26+
27+
const aws_kms : UTF8.ValidUTF8Bytes :=
28+
var s := [0x61, 0x77, 0x73, 0x2d, 0x6b, 0x6d, 0x73];
29+
assert s == UTF8.EncodeAscii("aws-kms");
30+
s
31+
32+
const keyproviderInfo : UTF8.ValidUTF8Bytes :=
33+
var s := [0x6b, 0x65, 0x79, 0x70, 0x72, 0x6f, 0x76, 0x69, 0x64, 0x65, 0x72, 0x49, 0x6e, 0x66, 0x6f];
34+
assert s == UTF8.EncodeAscii("keyproviderInfo");
35+
s
36+
37+
const aws_kms_hierarchy : UTF8.ValidUTF8Bytes :=
38+
var s := [0x61, 0x77, 0x73, 0x2d, 0x6b, 0x6d, 0x73, 0x2d, 0x68, 0x69, 0x65, 0x72, 0x61, 0x72, 0x63, 0x68, 0x79];
39+
assert s == UTF8.EncodeAscii("aws-kms-hierarchy");
40+
s
41+
42+
const raw_rsa : UTF8.ValidUTF8Bytes :=
43+
var s := [0x72, 0x61, 0x77, 0x2d, 0x72, 0x73, 0x61];
44+
assert s == UTF8.EncodeAscii("raw-rsa");
45+
s
46+
47+
const aws_kms_rsa : UTF8.ValidUTF8Bytes :=
48+
var s := [0x61, 0x77, 0x73, 0x2d, 0x6b, 0x6d, 0x73, 0x2d, 0x72, 0x73, 0x61];
49+
assert s == UTF8.EncodeAscii("aws-kms-rsa");
50+
s
51+
1752
// THIS IS A TESTING RESOURCE DO NOT USE IN A PRODUCTION ENVIRONMENT
1853
const testVersion : Version := 1
1954
const testFlavor0 : Flavor := 0
2055
const testFlavor1 : Flavor := 1
2156
const testMsgID : MessageID := [1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32]
2257
const testLegend : Legend := [0x65, 0x73]
23-
const testEncContext : CMPEncryptionContext := map[EncodeAscii("abc") := EncodeAscii("def")]
58+
const testEncContext : CMPEncryptionContext := map[abc := def]
2459
const testAwsKmsDataKey := CMP.EncryptedDataKey(
25-
keyProviderId := EncodeAscii("aws-kms") ,
26-
keyProviderInfo := EncodeAscii("keyproviderInfo"),
60+
keyProviderId := aws_kms ,
61+
keyProviderInfo := keyproviderInfo,
2762
ciphertext := [1, 2, 3, 4, 5])
2863
const testAwsKmsHDataKey := CMP.EncryptedDataKey(
29-
keyProviderId := EncodeAscii("aws-kms-hierarchy") ,
30-
keyProviderInfo := EncodeAscii("keyproviderInfo"),
64+
keyProviderId := aws_kms_hierarchy,
65+
keyProviderInfo := keyproviderInfo,
3166
ciphertext := [
3267
64, 92, 115, 7, 85, 121, 112, 79, 69, 12, 82, 25, 67, 34,
3368
11, 66, 93, 45, 40, 23, 90, 61, 16, 28, 59, 114, 52, 122,
@@ -40,12 +75,12 @@ module DynamoDbGetEncryptedDataKeyDescriptionTest {
4075
114, 76, 18, 103, 84, 34, 123, 1, 125, 61, 33, 13, 18, 81,
4176
24, 53, 53, 26, 60, 52, 85, 81, 96, 85, 72])
4277
const testRawRsaDataKey := CMP.EncryptedDataKey(
43-
keyProviderId := EncodeAscii("raw-rsa") ,
78+
keyProviderId := raw_rsa,
4479
keyProviderInfo := [1, 2, 3, 4, 5],
4580
ciphertext := [6, 7, 8, 9])
4681
const testAwsKmsRsaDataKey := CMP.EncryptedDataKey(
47-
keyProviderId := EncodeAscii("aws-kms-rsa") ,
48-
keyProviderInfo := EncodeAscii("keyproviderInfo"),
82+
keyProviderId := aws_kms_rsa,
83+
keyProviderInfo := keyproviderInfo,
4984
ciphertext := [1, 2, 3, 4, 5])
5085

5186
method CreatePartialHeader(version : Version, flavor : Flavor, msgID : MessageID, legend : Legend, encContext : CMPEncryptionContext, dataKeyList : CMPEncryptedDataKeyList)

‎DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DynamoDbMiddlewareSupport.dfy‎

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -121,7 +121,10 @@ module DynamoDbMiddlewareSupport {
121121
.MapFailure(e => AwsCryptographyDbEncryptionSdkDynamoDb(e))
122122
}
123123

124-
const HierarchicalKeyringId := UTF8.EncodeAscii("aws-kms-hierarchy")
124+
const HierarchicalKeyringId : UTF8.ValidUTF8Bytes :=
125+
var s := [0x61, 0x77, 0x73, 0x2d, 0x6b, 0x6d, 0x73, 0x2d, 0x68, 0x69, 0x65, 0x72, 0x61, 0x72, 0x63, 0x68, 0x79];
126+
assert s == UTF8.EncodeAscii("aws-kms-hierarchy");
127+
s
125128

126129
// Return Beacon Key ID for use in beaconizing records to be written
127130
function method GetKeyIdFromHeader(config : ValidTableConfig, output : AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes.EncryptItemOutput) :

0 commit comments

Comments
 (0)