Skip to content

Commit 3194054

Browse files
ajewellamzajewellamz
authored
chore: further performance improvements (#1826)
1 parent 8ca2883 commit 3194054

File tree

7 files changed

+1236
-13
lines changed

7 files changed

+1236
-13
lines changed

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

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -77,7 +77,7 @@ module DynamoToStruct {
7777
&& StructuredToAttr(s[kv.0]).Success?
7878
&& kv.1 == StructuredToAttr(s[kv.0]).value
7979
{
80-
if forall k <- s.Keys :: IsValid_AttributeName(k) then
80+
if forall k <- s :: IsValid_AttributeName(k) then
8181
var structuredData := map k <- s :: k := StructuredToAttr(s[k]);
8282
MapKeysMatchItems(s);
8383
MapError(SimplifyMapValue(structuredData))
@@ -477,7 +477,7 @@ module DynamoToStruct {
477477
// lets Dafny find the correct termination metric.
478478
// See "The Parent Trick" for details: <https://leino.science/papers/krml283.html>.
479479
function method MapAttrToBytes(ghost parent: AttributeValue, m: MapAttributeValue, depth : nat): (ret: Result<seq<uint8>, string>)
480-
requires forall kv <- m.Items :: kv.1 < parent
480+
requires forall k <- m :: m[k] < parent
481481
{
482482
//= specification/dynamodb-encryption-client/ddb-attribute-serialization.md#value-type
483483
//# Value Type MUST be the [Type ID](#type-id) of the type of [Map Value](#map-value).
@@ -492,7 +492,8 @@ module DynamoToStruct {
492492
//= specification/dynamodb-encryption-client/ddb-attribute-serialization.md#map-value
493493
//# A Map MAY hold any DynamoDB Attribute Value data type,
494494
//# and MAY hold values of different types.
495-
var bytesResults := map kv <- m.Items :: kv.0 := AttrToBytes(kv.1, true, depth+1);
495+
var bytesResults := map k <- m :: k := AttrToBytes(m[k], true, depth+1);
496+
496497
var count :- U32ToBigEndian(|m|);
497498
var bytes :- SimplifyMapValue(bytesResults);
498499
var body :- CollectMap(bytes);

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

Lines changed: 16 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -57,12 +57,23 @@ module StructuredEncryptionHeader {
5757
type Legend = x : seq<LegendByte> | |x| < UINT16_LIMIT
5858
type CMPUtf8Bytes = x : CMP.Utf8Bytes | |x| < UINT16_LIMIT
5959

60-
predicate method IsVersion2Schema(data : CanonCryptoList)
61-
{
62-
exists x <- data :: x.action == SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT
60+
predicate method {:tailrecursion} IsVersion2Schema(data : CanonCryptoList, pos : uint32 := 0) : (ret : bool)
61+
requires |data| < UINT32_LIMIT
62+
requires pos <= |data| as uint32
63+
requires forall i | 0 <= i < pos :: data[i].action != SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT
64+
decreases |data| as uint32 - pos
65+
ensures ret <==> (exists x <- data :: x.action == SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT)
66+
{
67+
if pos == |data| as uint32 then
68+
false
69+
else if data[pos].action == SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT then
70+
true
71+
else
72+
IsVersion2Schema(data, pos+1)
6373
}
6474

6575
function method VersionFromSchema(data : CanonCryptoList) : (ret : Version)
76+
requires |data| < UINT32_LIMIT
6677
ensures (exists x <- data :: x.action == SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT) <==> (ret == 2)
6778
ensures !(exists x <- data :: x.action == SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT) <==> (ret == 1)
6879
{
@@ -229,8 +240,9 @@ module StructuredEncryptionHeader {
229240
//# If any [Crypto Action](./structures.md#crypto-action) is configured as
230241
//# [SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT Crypto Action](./structures.md#sign_and_include_in_encryption_context)
231242
//# the Version MUST be 0x02; otherwise, Version MUST be 0x01.
232-
ensures ret.Success? ==> ret.value.version == VersionFromSchema(schema)
243+
ensures ret.Success? ==> |schema| < UINT32_LIMIT && ret.value.version == VersionFromSchema(schema)
233244
{
245+
:- Need(|schema| < UINT32_LIMIT, E("Unexpected large schema"));
234246
:- Need(ValidEncryptionContext(mat.encryptionContext), E("Invalid Encryption Context"));
235247
:- Need(0 < |mat.encryptedDataKeys|, E("There must be at least one data key"));
236248
:- Need(|mat.encryptedDataKeys| < UINT8_LIMIT, E("Too many data keys."));

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -220,7 +220,7 @@ module StructuredEncryptionUtil {
220220
// attribute is "authorized", a.k.a. included in the signature
221221
predicate method IsAuthAttr(x : CryptoAction)
222222
{
223-
x.ENCRYPT_AND_SIGN? || x.SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT? || x.SIGN_ONLY?
223+
!x.DO_NOTHING?
224224
}
225225

226226
// wrap a value in a StructuredData

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -61,6 +61,7 @@ module WrappedDDBEncryptionMain {
6161
config :- expect AddJson(config, "data.json", keyVectors);
6262
config :- expect AddJson(config, "iotest.json", keyVectors);
6363
config :- expect AddJson(config, "PermTest.json", keyVectors);
64+
config :- expect AddJson(config, "large_records.json", keyVectors);
6465
config.RunAllTests(keyVectors);
6566
}
6667
}

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

Lines changed: 46 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -46,9 +46,15 @@ module {:options "-functionSyntax:4"} JsonConfig {
4646
item : DDB.AttributeMap
4747
)
4848

49+
datatype LargeRecord = LargeRecord (
50+
name : string,
51+
count : nat,
52+
item : DDB.AttributeMap
53+
)
54+
4955
datatype TableConfig = TableConfig (
5056
name : ConfigName,
51-
config : Types.DynamoDbTableEncryptionConfig,
57+
config : AwsCryptographyDbEncryptionSdkDynamoDbTypes.DynamoDbTableEncryptionConfig,
5258
vanilla : bool
5359
)
5460

@@ -1410,7 +1416,6 @@ module {:options "-functionSyntax:4"} JsonConfig {
14101416
return Success(results);
14111417
}
14121418

1413-
14141419
method GetRecord(data : JSON) returns (output : Result<Record, string>)
14151420
{
14161421
var item :- JsonToDdbItem(data);
@@ -1424,4 +1429,43 @@ module {:options "-functionSyntax:4"} JsonConfig {
14241429
var num :- StrToNat(hash.N);
14251430
return Success(Record(num, item));
14261431
}
1432+
1433+
method GetLarge(name : string, data : JSON) returns (output : Result<LargeRecord, string>)
1434+
{
1435+
:- Need(data.Object?, "LargeRecord must be a JSON object.");
1436+
var count := 0;
1437+
var item : DDB.AttributeMap := map[];
1438+
for i := 0 to |data.obj| {
1439+
var obj := data.obj[i];
1440+
match obj.0 {
1441+
case "Count" =>
1442+
:- Need(obj.1.Number?, "GetPrefix length must be a number");
1443+
count :- DecimalToInt(obj.1.num);
1444+
case "Item" => var src :- JsonToDdbItem(obj.1); item := src;
1445+
case _ => return Failure("Unexpected part of a LargeRecord : '" + obj.0 + "'");
1446+
}
1447+
}
1448+
if (count <= 0) {
1449+
return Failure("Missing or invalid Count in LargeRecord : '" + name + "'");
1450+
}
1451+
if (|item| == 0) {
1452+
return Failure("Missing or Empty LargeRecord : '" + name + "'");
1453+
}
1454+
var record := LargeRecord(name, count, item);
1455+
return Success(record);
1456+
}
1457+
1458+
method GetLarges(data : JSON) returns (output : Result<seq<LargeRecord>, string>)
1459+
{
1460+
:- Need(data.Object?, "Larges must be a JSON object.");
1461+
var results : seq<LargeRecord> := [];
1462+
for i := 0 to |data.obj| {
1463+
var obj := data.obj[i];
1464+
var record :- GetLarge(obj.0, obj.1);
1465+
results := results + [record];
1466+
}
1467+
return Success(results);
1468+
}
1469+
1470+
14271471
}

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

Lines changed: 100 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -41,12 +41,18 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
4141
import MPT = AwsCryptographyMaterialProvidersTypes
4242
import Primitives = AtomicPrimitives
4343
import ParseJsonManifests
44+
import Time
45+
import Trans = AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes
46+
import TransOp = AwsCryptographyDbEncryptionSdkDynamoDbTransformsOperations
47+
import DdbMiddlewareConfig
48+
import DynamoDbEncryptionTransforms
4449

4550

4651
datatype TestVectorConfig = TestVectorConfig (
4752
schemaOnEncrypt : DDB.CreateTableInput,
4853
globalRecords : seq<Record>,
4954
tableEncryptionConfigs : map<ConfigName, TableConfig>,
55+
largeEncryptionConfigs : map<ConfigName, TableConfig>,
5056
queries : seq<SimpleQuery>,
5157
names : DDB.ExpressionAttributeNameMap,
5258
values : DDB.ExpressionAttributeValueMap,
@@ -58,7 +64,8 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
5864
writeTests : seq<WriteTest>,
5965
roundTripTests : seq<RoundTripTest>,
6066
decryptTests : seq<DecryptTest>,
61-
strings : seq<string>
67+
strings : seq<string>,
68+
large : seq<LargeRecord>
6269
) {
6370

6471
method RunAllTests(keyVectors: KeyVectors.KeyVectorsClient)
@@ -69,6 +76,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
6976
print "DBE Test Vectors\n";
7077
print |globalRecords|, " records.\n";
7178
print |tableEncryptionConfigs|, " tableEncryptionConfigs.\n";
79+
print |largeEncryptionConfigs|, " largeEncryptionConfigs.\n";
7280
print |queries|, " queries.\n";
7381
print |names|, " names.\n";
7482
print |values|, " values.\n";
@@ -78,6 +86,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
7886
print |configsForIoTest|, " configsForIoTest.\n";
7987
print |configsForModTest|, " configsForModTest.\n";
8088
print |strings|, " strings.\n";
89+
print |large|, " large.\n";
8190
if |roundTripTests| != 0 {
8291
print |roundTripTests[0].configs|, " configs and ", |roundTripTests[0].records|, " records for round trip.\n";
8392
}
@@ -107,6 +116,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
107116
return;
108117
}
109118
StringOrdering();
119+
LargeTests();
110120
BasicIoTest();
111121
RunIoTests();
112122
BasicQueryTest();
@@ -484,6 +494,87 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
484494
}
485495
}
486496

497+
const TestConfigs : set<string> := {"all"}
498+
const TestRecords : set<string> := {"all"}
499+
500+
predicate DoTestConfig(name : string)
501+
{
502+
"all" in TestConfigs || name in TestConfigs
503+
}
504+
505+
predicate DoTestRecord(name : string)
506+
{
507+
"all" in TestRecords || name in TestRecords
508+
}
509+
510+
method LargeTests()
511+
{
512+
print "LargeTests\n";
513+
DoLargeTest("do_nothing");
514+
DoLargeTest("do_nothing_nosign");
515+
DoLargeTest("full_encrypt");
516+
DoLargeTest("full_encrypt_nosign");
517+
DoLargeTest("full_sign");
518+
DoLargeTest("full_sign_nosign");
519+
}
520+
521+
method DoLargeTest(config : string)
522+
{
523+
if !DoTestConfig(config) {
524+
return;
525+
}
526+
expect config in largeEncryptionConfigs;
527+
var tconfig := largeEncryptionConfigs[config];
528+
var configs := Types.DynamoDbTablesEncryptionConfig (
529+
tableEncryptionConfigs := map[TableName := tconfig.config]
530+
);
531+
// because there are lots of pre-conditions on configs
532+
assume {:axiom} false;
533+
var client :- expect DynamoDbEncryptionTransforms.DynamoDbEncryptionTransforms(configs);
534+
LargeTestsClient(client, config);
535+
}
536+
537+
method LargeTestsClient(client : Trans.IDynamoDbEncryptionTransformsClient, config : string)
538+
requires client.ValidState()
539+
ensures client.ValidState()
540+
modifies client.Modifies
541+
{
542+
for i := 0 to |large| {
543+
RunLargeTest(large[i], client, config);
544+
}
545+
}
546+
547+
method RunLargeTest(record : LargeRecord, client : Trans.IDynamoDbEncryptionTransformsClient, config : string)
548+
requires client.ValidState()
549+
ensures client.ValidState()
550+
modifies client.Modifies
551+
{
552+
if !DoTestRecord(record.name) {
553+
return;
554+
}
555+
556+
var time := Time.GetAbsoluteTime();
557+
for i := 0 to record.count {
558+
var put_input_input := Trans.PutItemInputTransformInput ( sdkInput := DDB.PutItemInput (TableName := TableName, Item := record.item));
559+
var put_input_output :- expect client.PutItemInputTransform(put_input_input);
560+
}
561+
var elapsed := Time.TimeSince(time);
562+
Time.PrintTimeLong(elapsed, "Large Encrypt " + record.name + "(" + Base10Int2String(record.count) + ") " + config);
563+
564+
var put_input_input := Trans.PutItemInputTransformInput ( sdkInput := DDB.PutItemInput (TableName := TableName, Item := record.item));
565+
var put_input_output :- expect client.PutItemInputTransform(put_input_input);
566+
time := Time.GetAbsoluteTime();
567+
for i := 0 to record.count {
568+
var orig_get_input := DDB.GetItemInput(TableName := TableName, Key := map[]);
569+
var get_output := DDB.GetItemOutput(Item := Some(put_input_output.transformedInput.Item));
570+
var trans_get_input := Trans.GetItemOutputTransformInput(sdkOutput := get_output, originalInput := orig_get_input);
571+
var put_output :- expect client.GetItemOutputTransform(trans_get_input);
572+
573+
}
574+
elapsed := Time.TimeSince(time);
575+
Time.PrintTimeLong(elapsed, "Large Decrypt " + record.name + "(" + Base10Int2String(record.count) + ") " + config);
576+
}
577+
487578
method RoundTripTests()
488579
{
489580
print "RoundTripTests\n";
@@ -999,7 +1090,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
9991090

10001091
function MakeEmptyTestVector() : TestVectorConfig
10011092
{
1002-
TestVectorConfig(MakeCreateTableInput(), [], map[], [], map[], map[], [], [], [], [], [], [], [], [], [])
1093+
TestVectorConfig(MakeCreateTableInput(), [], map[], map[], [], map[], map[], [], [], [], [], [], [], [], [], [], [])
10031094
}
10041095

10051096
method ParseTestVector(data : JSON, prev : TestVectorConfig, keyVectors: KeyVectors.KeyVectorsClient)
@@ -1020,10 +1111,12 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
10201111
var ioTests : seq<IoTest> := [];
10211112
var gsi : seq<DDB.GlobalSecondaryIndex> := [];
10221113
var tableEncryptionConfigs : map<string, TableConfig> := map[];
1114+
var largeEncryptionConfigs : map<string, TableConfig> := map[];
10231115
var writeTests : seq<WriteTest> := [];
10241116
var roundTripTests : seq<RoundTripTest> := [];
10251117
var decryptTests : seq<DecryptTest> := [];
10261118
var strings : seq<string> := [];
1119+
var large : seq<LargeRecord> := [];
10271120

10281121
for i := 0 to |data.obj| {
10291122
match data.obj[i].0 {
@@ -1038,10 +1131,12 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
10381131
case "IoTests" => ioTests :- GetIoTests(data.obj[i].1, keyVectors);
10391132
case "GSI" => gsi :- GetGSIs(data.obj[i].1);
10401133
case "tableEncryptionConfigs" => tableEncryptionConfigs :- GetTableConfigs(data.obj[i].1, keyVectors);
1134+
case "largeEncryptionConfigs" => largeEncryptionConfigs :- GetTableConfigs(data.obj[i].1, keyVectors);
10411135
case "WriteTests" => writeTests :- GetWriteTests(data.obj[i].1, keyVectors);
10421136
case "RoundTripTest" => roundTripTests :- GetRoundTripTests(data.obj[i].1, keyVectors);
10431137
case "DecryptTests" => decryptTests :- GetDecryptTests(data.obj[i].1, keyVectors);
10441138
case "Strings" => strings :- GetStrings(data.obj[i].1);
1139+
case "Large" => large :- GetLarges(data.obj[i].1);
10451140
case _ => return Failure("Unexpected top level tag " + data.obj[i].0);
10461141
}
10471142
}
@@ -1052,6 +1147,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
10521147
schemaOnEncrypt := newSchema,
10531148
globalRecords := prev.globalRecords + records,
10541149
tableEncryptionConfigs := prev.tableEncryptionConfigs + tableEncryptionConfigs,
1150+
largeEncryptionConfigs := prev.largeEncryptionConfigs + largeEncryptionConfigs,
10551151
queries := prev.queries + queries,
10561152
failingQueries := prev.failingQueries + failingQueries,
10571153
names := prev.names + names,
@@ -1063,7 +1159,8 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
10631159
writeTests := prev.writeTests + writeTests,
10641160
roundTripTests := prev.roundTripTests + roundTripTests,
10651161
decryptTests := prev.decryptTests + decryptTests,
1066-
strings := prev.strings + strings
1162+
strings := prev.strings + strings,
1163+
large := prev.large + large
10671164
)
10681165
);
10691166
}

0 commit comments

Comments
 (0)