Skip to content

Commit 2ddea04

Browse files
ajewellamzajewellamz
committed
m
1 parent 331927d commit 2ddea04

File tree

4 files changed

+168
-36
lines changed

4 files changed

+168
-36
lines changed

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -985,7 +985,7 @@ module {:options "-functionSyntax:4"} JsonConfig {
985985
case "Signed" => Signed :- GetSignedParts(obj.1);
986986
case "Encrypted" => Encrypted :- GetEncryptedParts(obj.1);
987987
case "Constructors" => constructors :- GetConstructors(obj.1);
988-
case _ => return Failure("Unexpected part of a standard beacon : '" + data.obj[i].0 + "'");
988+
case _ => return Failure("Unexpected part of a compound beacon : '" + data.obj[i].0 + "'");
989989
}
990990
}
991991
:- Need(0 < |name|, "Each Compound Beacon needs a name.");
@@ -1129,7 +1129,7 @@ module {:options "-functionSyntax:4"} JsonConfig {
11291129
length :- DecimalToNat(obj.1.num);
11301130
case "Loc" =>
11311131
:- Need(obj.1.String?, "Standard Beacon Location must be a string");
1132-
:- Need(0 < |obj.1.str|, "Standard Beacon Location must nt be an empty string.");
1132+
:- Need(0 < |obj.1.str|, "Standard Beacon Location must not be an empty string.");
11331133
loc := Some(obj.1.str);
11341134
case "numberOfBuckets" =>
11351135
:- Need(obj.1.Number?, "numberOfBuckets must be of type Number.");

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

Lines changed: 72 additions & 33 deletions
Original file line numberDiff line numberDiff line change
@@ -135,37 +135,37 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
135135
print |roundTripTests[1].configs|, " configs and ", |roundTripTests[1].records|, " records for round trip.\n";
136136
}
137137

138-
var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_32.json", keyVectors);
139-
var _ :- expect DecryptManifest.Decrypt("decrypt_java_32.json", keyVectors);
140-
var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_33.json", keyVectors);
141-
var _ :- expect DecryptManifest.Decrypt("decrypt_java_33.json", keyVectors);
142-
var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_33a.json", keyVectors);
143-
var _ :- expect DecryptManifest.Decrypt("decrypt_java_33a.json", keyVectors);
144-
var _ :- expect DecryptManifest.Decrypt("decrypt_rust_38.json", keyVectors);
145-
var _ :- expect DecryptManifest.Decrypt("decrypt_go_38.json", keyVectors);
146-
var _ :- expect DecryptManifest.Decrypt("decrypt_java_39.json", keyVectors);
147-
var _ :- expect WriteManifest.Write("encrypt.json");
148-
var _ :- expect EncryptManifest.Encrypt("encrypt.json", "decrypt.json", "java", "3.3", keyVectors);
149-
var _ :- expect DecryptManifest.Decrypt("decrypt.json", keyVectors);
138+
// var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_32.json", keyVectors);
139+
// var _ :- expect DecryptManifest.Decrypt("decrypt_java_32.json", keyVectors);
140+
// var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_33.json", keyVectors);
141+
// var _ :- expect DecryptManifest.Decrypt("decrypt_java_33.json", keyVectors);
142+
// var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_33a.json", keyVectors);
143+
// var _ :- expect DecryptManifest.Decrypt("decrypt_java_33a.json", keyVectors);
144+
// var _ :- expect DecryptManifest.Decrypt("decrypt_rust_38.json", keyVectors);
145+
// var _ :- expect DecryptManifest.Decrypt("decrypt_go_38.json", keyVectors);
146+
// var _ :- expect DecryptManifest.Decrypt("decrypt_java_39.json", keyVectors);
147+
// var _ :- expect WriteManifest.Write("encrypt.json");
148+
// var _ :- expect EncryptManifest.Encrypt("encrypt.json", "decrypt.json", "java", "3.3", keyVectors);
149+
// var _ :- expect DecryptManifest.Decrypt("decrypt.json", keyVectors);
150150
if |globalRecords| + |tableEncryptionConfigs| + |queries| == 0 {
151151
print "\nRunning no tests\n";
152152
return;
153153
}
154154
Validate();
155155
StringOrdering();
156156
BucketTests();
157-
LargeTests();
158-
PerfQueryTests();
159-
BasicIoTest();
160-
RunIoTests();
161-
BasicQueryTest();
162-
ConfigModTest();
163-
ComplexTests();
164-
WriteTests();
165-
RoundTripTests();
166-
DecryptTests();
167-
var client :- expect CreateInterceptedDDBClient.CreateVanillaDDBClient();
168-
DeleteTable(client);
157+
// LargeTests();
158+
// PerfQueryTests();
159+
// BasicIoTest();
160+
// RunIoTests();
161+
// BasicQueryTest();
162+
// ConfigModTest();
163+
// ComplexTests();
164+
// WriteTests();
165+
// RoundTripTests();
166+
// DecryptTests();
167+
// var client :- expect CreateInterceptedDDBClient.CreateVanillaDDBClient();
168+
// DeleteTable(client);
169169
}
170170

171171
function MakeBucketRecord(x : nat) : DDB.AttributeMap
@@ -175,12 +175,13 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
175175

176176
map[
177177
HashName := DDB.AttributeValue.N(num),
178-
"Attr1" := DDB.AttributeValue.S("AAAA"),
179-
"Attr2" := DDB.AttributeValue.S("BBBB"),
180-
"Attr3" := DDB.AttributeValue.S("CCCC"),
181-
"Attr4" := DDB.AttributeValue.S("DDDD"),
182-
"Attr5" := DDB.AttributeValue.S("EEEE"),
183-
"Attr6" := DDB.AttributeValue.S("FFFF"),
178+
AttrNames[0] := AttrValues[0],
179+
AttrNames[1] := AttrValues[1],
180+
AttrNames[2] := AttrValues[2],
181+
AttrNames[3] := AttrValues[3],
182+
AttrNames[4] := AttrValues[4],
183+
AttrNames[5] := AttrValues[5],
184+
AttrNames[6] := AttrValues[6],
184185
"PreferredBucket" := DDB.AttributeValue.N(num2)
185186
]
186187
}
@@ -353,7 +354,8 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
353354
":attr3",
354355
":attr4",
355356
":attr5",
356-
":attr6"
357+
":attr6",
358+
":attr7"
357359
]
358360

359361
const AttrNames : seq<DDB.AttributeName> :=
@@ -363,7 +365,8 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
363365
"Attr3",
364366
"Attr4",
365367
"Attr5",
366-
"Attr6"
368+
"Attr6",
369+
"Attr7"
367370
]
368371

369372
const AttrValues : seq<DDB.AttributeValue> :=
@@ -373,7 +376,8 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
373376
DDB.AttributeValue.S("CCCC"),
374377
DDB.AttributeValue.S("DDDD"),
375378
DDB.AttributeValue.S("EEEE"),
376-
DDB.AttributeValue.S("FFFF")
379+
DDB.AttributeValue.S("FFFF"),
380+
DDB.AttributeValue.S("GGGG")
377381
]
378382

379383
function GetBucketScan1(attr : nat) : (out : DDB.ScanInput)
@@ -508,6 +512,16 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
508512
}
509513

510514

515+
function GetCompQuery2671() : DDB.QueryInput
516+
{
517+
DDB.QueryInput(
518+
TableName := TableName,
519+
IndexName := Some("ATTR_INDEX2671"),
520+
FilterExpression := None,
521+
KeyConditionExpression := Some("Comp2671 = :attr2671"),
522+
ExpressionAttributeValues := Some(map[":attr2671" := DDB.AttributeValue.S("2_BBBB.6_FFFF.7_GGGG.1_AAAA")])
523+
)
524+
}
511525

512526
function GetBucketQuery1() : DDB.QueryInput
513527
{
@@ -633,6 +647,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
633647
method BucketTests()
634648
{
635649
print "BucketTests\n";
650+
BucketTest4();
636651
BucketTest3();
637652
BucketTest1();
638653
BucketTest2();
@@ -671,6 +686,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
671686
// 2) Every bucket holds at least one item
672687
method BucketTest1()
673688
{
689+
print "BucketTest1\n";
674690
expect "bucket_encrypt" in largeEncryptionConfigs;
675691
var config := largeEncryptionConfigs["bucket_encrypt"];
676692
var wClient, rClient := SetupTestTable(config, config);
@@ -734,9 +750,32 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
734750
}
735751
}
736752

753+
// Similar to BucketTest1, but with complex config
754+
method BucketTest4()
755+
{
756+
print "BucketTest4\n";
757+
expect "complex_bucket_encrypt" in largeEncryptionConfigs;
758+
var config := largeEncryptionConfigs["complex_bucket_encrypt"];
759+
var wClient, rClient := SetupTestTable(config, config);
760+
for i : nat := 0 to 100 {
761+
var putInput := DDB.PutItemInput(
762+
TableName := TableName,
763+
Item := MakeBucketRecord(i)
764+
);
765+
var _ :- expect wClient.PutItem(putInput);
766+
}
767+
print "BucketTest4 Wrote";
768+
TestBucketQueries(rClient, 2, GetCompQuery2671(), "comp query 2671");
769+
print "BucketTest4 Did One";
770+
771+
// TestBucketScan(rClient, GetBucketScan6(0,1,2,3,4,5));
772+
TestBucketScan(rClient, GetBucketScan6(5,4,3,2,1,0));
773+
}
774+
737775
// As BucketTest1, but with custom bucket selector
738776
method BucketTest2()
739777
{
778+
print "BucketTest2\n";
740779
expect "bucket_encrypt" in largeEncryptionConfigs;
741780
var config := largeEncryptionConfigs["bucket_encrypt"];
742781
var testSelector := new TestBucketSelector();

‎TestVectors/runtimes/java/large_records.json‎

Lines changed: 93 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@
55
["ATTR_INDEX3", "aws_dbe_b_Attr3"],
66
["ATTR_INDEX4", "aws_dbe_b_Attr4"],
77
["ATTR_INDEX5", "aws_dbe_b_Attr5"],
8+
["ATTR_INDEX2671", "aws_dbe_b_Comp2671"],
89
["ATTR_INDEX15", "aws_dbe_b_Attr1", "aws_dbe_b_Attr5"],
910
["ATTR_INDEX21", "aws_dbe_b_Attr2", "aws_dbe_b_Attr1"],
1011
["ATTR_INDEX23", "aws_dbe_b_Attr2", "aws_dbe_b_Attr3"],
@@ -23,6 +24,8 @@
2324
"Attr4": "ENCRYPT_AND_SIGN",
2425
"Attr5": "ENCRYPT_AND_SIGN",
2526
"Attr6": "SIGN_ONLY",
27+
"Attr7": "SIGN_ONLY",
28+
"Attr8": "SIGN_ONLY",
2629
"PreferredBucket": "SIGN_ONLY"
2730
},
2831
"search": {
@@ -59,6 +62,96 @@
5962
]
6063
}
6164
},
65+
"complex_bucket_encrypt": {
66+
"partitionKeyName": "RecNum",
67+
"attributeActionsOnEncrypt": {
68+
"RecNum": "SIGN_ONLY",
69+
"Attr1": "ENCRYPT_AND_SIGN",
70+
"Attr2": "ENCRYPT_AND_SIGN",
71+
"Attr3": "ENCRYPT_AND_SIGN",
72+
"Attr4": "ENCRYPT_AND_SIGN",
73+
"Attr5": "ENCRYPT_AND_SIGN",
74+
"Attr6": "SIGN_ONLY",
75+
"Attr7": "SIGN_ONLY",
76+
"Attr8": "SIGN_ONLY",
77+
"PreferredBucket": "SIGN_ONLY"
78+
},
79+
"search": {
80+
"versions": [
81+
{
82+
"maximumNumberOfBuckets": 5,
83+
"compoundBeacons": [
84+
{
85+
"Name": "Comp2671",
86+
"Split": ".",
87+
"Encrypted": [
88+
{
89+
"Name": "Attr1",
90+
"Prefix": "1_"
91+
},
92+
{
93+
"Name": "Attr2",
94+
"Prefix": "2_"
95+
}
96+
],
97+
"Signed": [
98+
{
99+
"Name": "Attr6",
100+
"Prefix": "6_"
101+
},
102+
{
103+
"Name": "Attr7",
104+
"Prefix": "7_"
105+
}
106+
],
107+
"Constructors" : [
108+
[
109+
{
110+
"Name" : "Attr2"
111+
},
112+
{
113+
"Name" : "Attr6"
114+
},
115+
{
116+
"Name" : "Attr7"
117+
},
118+
{
119+
"Name" : "Attr1"
120+
}
121+
]
122+
]
123+
}
124+
],
125+
"standardBeacons": [
126+
{
127+
"Name": "Attr1",
128+
"Length": 32,
129+
"numberOfBuckets": 1
130+
},
131+
{
132+
"Name": "Attr2",
133+
"Length": 32,
134+
"numberOfBuckets": 2
135+
},
136+
{
137+
"Name": "Attr3",
138+
"Length": 32,
139+
"numberOfBuckets": 3
140+
},
141+
{
142+
"Name": "Attr4",
143+
"Length": 32,
144+
"numberOfBuckets": 4
145+
},
146+
{
147+
"Name": "Attr5",
148+
"Length": 32
149+
}
150+
]
151+
}
152+
]
153+
}
154+
},
62155
"full_encrypt": {
63156
"partitionKeyName": "PK",
64157
"attributeActionsOnEncrypt": {

‎submodules/smithy-dafny‎

0 commit comments

Comments
 (0)