Skip to content

Commit 30b774f

Browse files
ajewellamzajewellamz
committed
m
1 parent 59a197e commit 30b774f

File tree

3 files changed

+239
-20
lines changed

3 files changed

+239
-20
lines changed

‎DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy

Lines changed: 13 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -368,13 +368,13 @@ module SearchConfigToInfo {
368368
return Failure(E("A beacon key field name of " + name + " was configured, but there's also a virtual field of that name."));
369369
}
370370
}
371-
var bucketSelector;
372-
if outer.search.Some? && outer.search.value.versions[0].bucketSelector.Some? {
373-
bucketSelector := outer.search.value.versions[0].bucketSelector.value;
374-
assume {:axiom} bucketSelector.ValidState();
375-
} else {
376-
bucketSelector := new DefaultBucketSelector();
377-
}
371+
var bucketSelector;
372+
if outer.search.Some? && outer.search.value.versions[0].bucketSelector.Some? {
373+
bucketSelector := outer.search.value.versions[0].bucketSelector.value;
374+
assume {:axiom} bucketSelector.ValidState();
375+
} else {
376+
bucketSelector := new DefaultBucketSelector();
377+
}
378378

379379
return I.MakeBeaconVersion(
380380
config.version as I.VersionNumber,
@@ -587,12 +587,12 @@ module SearchConfigToInfo {
587587
if outer.search.None? || |outer.search.value.versions| == 0 then
588588
Success(1)
589589
else
590-
if BucketCountNone(inner) then
591-
Success(defaultBuckets)
592-
else if inner.value < maxBuckets then
593-
Success(inner.value)
594-
else
595-
Failure(E("Constrained numberOfBuckets for " + name + " is " + Base10Int2String(inner.value as int) + " but it must be less than the maximumNumberOfBuckets " + Base10Int2String(maxBuckets as int)))
590+
if BucketCountNone(inner) then
591+
Success(defaultBuckets)
592+
else if inner.value < maxBuckets then
593+
Success(inner.value)
594+
else
595+
Failure(E("Constrained numberOfBuckets for " + name + " is " + Base10Int2String(inner.value as int) + " but it must be less than the maximumNumberOfBuckets " + Base10Int2String(maxBuckets as int)))
596596
}
597597

598598
// convert configured StandardBeacons to internal Beacons

‎TestVectors/runtimes/java/PermTest.json

Lines changed: 222 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1,222 @@
1-
{"RoundTripTest":{"Records":[{"RecNum":{"N":"200"},"StringSet":{"SS":["aaa"]},"NumberSet":{"NS":["111"]},"BinarySet":{"BS":["AQID"]}},{"RecNum":{"N":"201"},"StringSet":{"SS":["aaa","bbb"]},"NumberSet":{"NS":["111","222"]},"BinarySet":{"BS":["AQID","AgME"]}},{"RecNum":{"N":"202"},"StringSet":{"SS":["bbb","aaa"]},"NumberSet":{"NS":["222","111"]},"BinarySet":{"BS":["AgME","AQID"]}},{"RecNum":{"N":"203"},"StringSet":{"SS":["aaa","bbb","ccc"]},"NumberSet":{"NS":["111","222","333"]},"BinarySet":{"BS":["AQID","AgME","AwQF"]}},{"RecNum":{"N":"204"},"StringSet":{"SS":["bbb","aaa","ccc"]},"NumberSet":{"NS":["222","111","333"]},"BinarySet":{"BS":["AgME","AQID","AwQF"]}},{"RecNum":{"N":"205"},"StringSet":{"SS":["ccc","aaa","bbb"]},"NumberSet":{"NS":["333","111","222"]},"BinarySet":{"BS":["AwQF","AQID","AgME"]}},{"RecNum":{"N":"206"},"StringSet":{"SS":["aaa","ccc","bbb"]},"NumberSet":{"NS":["111","333","222"]},"BinarySet":{"BS":["AQID","AwQF","AgME"]}},{"RecNum":{"N":"207"},"StringSet":{"SS":["aaa","bbb","ccc"]},"NumberSet":{"NS":["111","222","333"]},"BinarySet":{"BS":["AQID","AgME","AwQF"]}},{"RecNum":{"N":"208"},"StringSet":{"SS":["bbb","aaa","ccc"]},"NumberSet":{"NS":["222","111","333"]},"BinarySet":{"BS":["AgME","AQID","AwQF"]}},{"RecNum":{"N":"209"},"StringSet":{"SS":["aaa","bbb","ccc","ddd"]},"NumberSet":{"NS":["111","222","333","444"]},"BinarySet":{"BS":["AQID","AgME","AwQF","BAUG"]}},{"RecNum":{"N":"210"},"StringSet":{"SS":["bbb","aaa","ccc","ddd"]},"NumberSet":{"NS":["222","111","333","444"]},"BinarySet":{"BS":["AgME","AQID","AwQF","BAUG"]}},{"RecNum":{"N":"211"},"StringSet":{"SS":["ccc","aaa","bbb","ddd"]},"NumberSet":{"NS":["333","111","222","444"]},"BinarySet":{"BS":["AwQF","AQID","AgME","BAUG"]}},{"RecNum":{"N":"212"},"StringSet":{"SS":["aaa","ccc","bbb","ddd"]},"NumberSet":{"NS":["111","333","222","444"]},"BinarySet":{"BS":["AQID","AwQF","AgME","BAUG"]}},{"RecNum":{"N":"213"},"StringSet":{"SS":["aaa","bbb","ccc","ddd"]},"NumberSet":{"NS":["111","222","333","444"]},"BinarySet":{"BS":["AQID","AgME","AwQF","BAUG"]}},{"RecNum":{"N":"214"},"StringSet":{"SS":["bbb","aaa","ccc","ddd"]},"NumberSet":{"NS":["222","111","333","444"]},"BinarySet":{"BS":["AgME","AQID","AwQF","BAUG"]}},{"RecNum":{"N":"215"},"StringSet":{"SS":["ddd","aaa","ccc","bbb"]},"NumberSet":{"NS":["444","111","333","222"]},"BinarySet":{"BS":["BAUG","AQID","AwQF","AgME"]}},{"RecNum":{"N":"216"},"StringSet":{"SS":["aaa","ddd","ccc","bbb"]},"NumberSet":{"NS":["111","444","333","222"]},"BinarySet":{"BS":["AQID","BAUG","AwQF","AgME"]}},{"RecNum":{"N":"217"},"StringSet":{"SS":["ccc","ddd","aaa","bbb"]},"NumberSet":{"NS":["333","444","111","222"]},"BinarySet":{"BS":["AwQF","BAUG","AQID","AgME"]}},{"RecNum":{"N":"218"},"StringSet":{"SS":["ddd","ccc","aaa","bbb"]},"NumberSet":{"NS":["444","333","111","222"]},"BinarySet":{"BS":["BAUG","AwQF","AQID","AgME"]}},{"RecNum":{"N":"219"},"StringSet":{"SS":["ddd","aaa","ccc","bbb"]},"NumberSet":{"NS":["444","111","333","222"]},"BinarySet":{"BS":["BAUG","AQID","AwQF","AgME"]}},{"RecNum":{"N":"220"},"StringSet":{"SS":["aaa","ddd","ccc","bbb"]},"NumberSet":{"NS":["111","444","333","222"]},"BinarySet":{"BS":["AQID","BAUG","AwQF","AgME"]}},{"RecNum":{"N":"221"},"StringSet":{"SS":["aaa","bbb","ccc","ddd"]},"NumberSet":{"NS":["111","222","333","444"]},"BinarySet":{"BS":["AQID","AgME","AwQF","BAUG"]}},{"RecNum":{"N":"222"},"StringSet":{"SS":["bbb","aaa","ccc","ddd"]},"NumberSet":{"NS":["222","111","333","444"]},"BinarySet":{"BS":["AgME","AQID","AwQF","BAUG"]}},{"RecNum":{"N":"223"},"StringSet":{"SS":["ccc","aaa","bbb","ddd"]},"NumberSet":{"NS":["333","111","222","444"]},"BinarySet":{"BS":["AwQF","AQID","AgME","BAUG"]}},{"RecNum":{"N":"224"},"StringSet":{"SS":["aaa","ccc","bbb","ddd"]},"NumberSet":{"NS":["111","333","222","444"]},"BinarySet":{"BS":["AQID","AwQF","AgME","BAUG"]}},{"RecNum":{"N":"225"},"StringSet":{"SS":["aaa","bbb","ccc","ddd"]},"NumberSet":{"NS":["111","222","333","444"]},"BinarySet":{"BS":["AQID","AgME","AwQF","BAUG"]}},{"RecNum":{"N":"226"},"StringSet":{"SS":["bbb","aaa","ccc","ddd"]},"NumberSet":{"NS":["222","111","333","444"]},"BinarySet":{"BS":["AgME","AQID","AwQF","BAUG"]}},{"RecNum":{"N":"227"},"StringSet":{"SS":["bbb","aaa","ddd","ccc"]},"NumberSet":{"NS":["222","111","444","333"]},"BinarySet":{"BS":["AgME","AQID","BAUG","AwQF"]}},{"RecNum":{"N":"228"},"StringSet":{"SS":["aaa","bbb","ddd","ccc"]},"NumberSet":{"NS":["111","222","444","333"]},"BinarySet":{"BS":["AQID","AgME","BAUG","AwQF"]}},{"RecNum":{"N":"229"},"StringSet":{"SS":["ddd","bbb","aaa","ccc"]},"NumberSet":{"NS":["444","222","111","333"]},"BinarySet":{"BS":["BAUG","AgME","AQID","AwQF"]}},{"RecNum":{"N":"230"},"StringSet":{"SS":["bbb","ddd","aaa","ccc"]},"NumberSet":{"NS":["222","444","111","333"]},"BinarySet":{"BS":["AgME","BAUG","AQID","AwQF"]}},{"RecNum":{"N":"231"},"StringSet":{"SS":["bbb","aaa","ddd","ccc"]},"NumberSet":{"NS":["222","111","444","333"]},"BinarySet":{"BS":["AgME","AQID","BAUG","AwQF"]}},{"RecNum":{"N":"232"},"StringSet":{"SS":["aaa","bbb","ddd","ccc"]},"NumberSet":{"NS":["111","222","444","333"]},"BinarySet":{"BS":["AQID","AgME","BAUG","AwQF"]}}],"Configs":{"AllSign":{"attributeActionsOnEncrypt":{"RecNum":"SIGN_ONLY","StringSet":"SIGN_ONLY","NumberSet":"SIGN_ONLY","BinarySet":"SIGN_ONLY"}},"AllEncrypt":{"attributeActionsOnEncrypt":{"RecNum":"SIGN_ONLY","StringSet":"ENCRYPT_AND_SIGN","NumberSet":"ENCRYPT_AND_SIGN","BinarySet":"ENCRYPT_AND_SIGN"}}}}}
1+
{
2+
"RoundTripTest": {
3+
"Records": [
4+
{
5+
"RecNum": { "N": "200" },
6+
"StringSet": { "SS": ["aaa"] },
7+
"NumberSet": { "NS": ["111"] },
8+
"BinarySet": { "BS": ["AQID"] }
9+
},
10+
{
11+
"RecNum": { "N": "201" },
12+
"StringSet": { "SS": ["aaa", "bbb"] },
13+
"NumberSet": { "NS": ["111", "222"] },
14+
"BinarySet": { "BS": ["AQID", "AgME"] }
15+
},
16+
{
17+
"RecNum": { "N": "202" },
18+
"StringSet": { "SS": ["bbb", "aaa"] },
19+
"NumberSet": { "NS": ["222", "111"] },
20+
"BinarySet": { "BS": ["AgME", "AQID"] }
21+
},
22+
{
23+
"RecNum": { "N": "203" },
24+
"StringSet": { "SS": ["aaa", "bbb", "ccc"] },
25+
"NumberSet": { "NS": ["111", "222", "333"] },
26+
"BinarySet": { "BS": ["AQID", "AgME", "AwQF"] }
27+
},
28+
{
29+
"RecNum": { "N": "204" },
30+
"StringSet": { "SS": ["bbb", "aaa", "ccc"] },
31+
"NumberSet": { "NS": ["222", "111", "333"] },
32+
"BinarySet": { "BS": ["AgME", "AQID", "AwQF"] }
33+
},
34+
{
35+
"RecNum": { "N": "205" },
36+
"StringSet": { "SS": ["ccc", "aaa", "bbb"] },
37+
"NumberSet": { "NS": ["333", "111", "222"] },
38+
"BinarySet": { "BS": ["AwQF", "AQID", "AgME"] }
39+
},
40+
{
41+
"RecNum": { "N": "206" },
42+
"StringSet": { "SS": ["aaa", "ccc", "bbb"] },
43+
"NumberSet": { "NS": ["111", "333", "222"] },
44+
"BinarySet": { "BS": ["AQID", "AwQF", "AgME"] }
45+
},
46+
{
47+
"RecNum": { "N": "207" },
48+
"StringSet": { "SS": ["aaa", "bbb", "ccc"] },
49+
"NumberSet": { "NS": ["111", "222", "333"] },
50+
"BinarySet": { "BS": ["AQID", "AgME", "AwQF"] }
51+
},
52+
{
53+
"RecNum": { "N": "208" },
54+
"StringSet": { "SS": ["bbb", "aaa", "ccc"] },
55+
"NumberSet": { "NS": ["222", "111", "333"] },
56+
"BinarySet": { "BS": ["AgME", "AQID", "AwQF"] }
57+
},
58+
{
59+
"RecNum": { "N": "209" },
60+
"StringSet": { "SS": ["aaa", "bbb", "ccc", "ddd"] },
61+
"NumberSet": { "NS": ["111", "222", "333", "444"] },
62+
"BinarySet": { "BS": ["AQID", "AgME", "AwQF", "BAUG"] }
63+
},
64+
{
65+
"RecNum": { "N": "210" },
66+
"StringSet": { "SS": ["bbb", "aaa", "ccc", "ddd"] },
67+
"NumberSet": { "NS": ["222", "111", "333", "444"] },
68+
"BinarySet": { "BS": ["AgME", "AQID", "AwQF", "BAUG"] }
69+
},
70+
{
71+
"RecNum": { "N": "211" },
72+
"StringSet": { "SS": ["ccc", "aaa", "bbb", "ddd"] },
73+
"NumberSet": { "NS": ["333", "111", "222", "444"] },
74+
"BinarySet": { "BS": ["AwQF", "AQID", "AgME", "BAUG"] }
75+
},
76+
{
77+
"RecNum": { "N": "212" },
78+
"StringSet": { "SS": ["aaa", "ccc", "bbb", "ddd"] },
79+
"NumberSet": { "NS": ["111", "333", "222", "444"] },
80+
"BinarySet": { "BS": ["AQID", "AwQF", "AgME", "BAUG"] }
81+
},
82+
{
83+
"RecNum": { "N": "213" },
84+
"StringSet": { "SS": ["aaa", "bbb", "ccc", "ddd"] },
85+
"NumberSet": { "NS": ["111", "222", "333", "444"] },
86+
"BinarySet": { "BS": ["AQID", "AgME", "AwQF", "BAUG"] }
87+
},
88+
{
89+
"RecNum": { "N": "214" },
90+
"StringSet": { "SS": ["bbb", "aaa", "ccc", "ddd"] },
91+
"NumberSet": { "NS": ["222", "111", "333", "444"] },
92+
"BinarySet": { "BS": ["AgME", "AQID", "AwQF", "BAUG"] }
93+
},
94+
{
95+
"RecNum": { "N": "215" },
96+
"StringSet": { "SS": ["ddd", "aaa", "ccc", "bbb"] },
97+
"NumberSet": { "NS": ["444", "111", "333", "222"] },
98+
"BinarySet": { "BS": ["BAUG", "AQID", "AwQF", "AgME"] }
99+
},
100+
{
101+
"RecNum": { "N": "216" },
102+
"StringSet": { "SS": ["aaa", "ddd", "ccc", "bbb"] },
103+
"NumberSet": { "NS": ["111", "444", "333", "222"] },
104+
"BinarySet": { "BS": ["AQID", "BAUG", "AwQF", "AgME"] }
105+
},
106+
{
107+
"RecNum": { "N": "217" },
108+
"StringSet": { "SS": ["ccc", "ddd", "aaa", "bbb"] },
109+
"NumberSet": { "NS": ["333", "444", "111", "222"] },
110+
"BinarySet": { "BS": ["AwQF", "BAUG", "AQID", "AgME"] }
111+
},
112+
{
113+
"RecNum": { "N": "218" },
114+
"StringSet": { "SS": ["ddd", "ccc", "aaa", "bbb"] },
115+
"NumberSet": { "NS": ["444", "333", "111", "222"] },
116+
"BinarySet": { "BS": ["BAUG", "AwQF", "AQID", "AgME"] }
117+
},
118+
{
119+
"RecNum": { "N": "219" },
120+
"StringSet": { "SS": ["ddd", "aaa", "ccc", "bbb"] },
121+
"NumberSet": { "NS": ["444", "111", "333", "222"] },
122+
"BinarySet": { "BS": ["BAUG", "AQID", "AwQF", "AgME"] }
123+
},
124+
{
125+
"RecNum": { "N": "220" },
126+
"StringSet": { "SS": ["aaa", "ddd", "ccc", "bbb"] },
127+
"NumberSet": { "NS": ["111", "444", "333", "222"] },
128+
"BinarySet": { "BS": ["AQID", "BAUG", "AwQF", "AgME"] }
129+
},
130+
{
131+
"RecNum": { "N": "221" },
132+
"StringSet": { "SS": ["aaa", "bbb", "ccc", "ddd"] },
133+
"NumberSet": { "NS": ["111", "222", "333", "444"] },
134+
"BinarySet": { "BS": ["AQID", "AgME", "AwQF", "BAUG"] }
135+
},
136+
{
137+
"RecNum": { "N": "222" },
138+
"StringSet": { "SS": ["bbb", "aaa", "ccc", "ddd"] },
139+
"NumberSet": { "NS": ["222", "111", "333", "444"] },
140+
"BinarySet": { "BS": ["AgME", "AQID", "AwQF", "BAUG"] }
141+
},
142+
{
143+
"RecNum": { "N": "223" },
144+
"StringSet": { "SS": ["ccc", "aaa", "bbb", "ddd"] },
145+
"NumberSet": { "NS": ["333", "111", "222", "444"] },
146+
"BinarySet": { "BS": ["AwQF", "AQID", "AgME", "BAUG"] }
147+
},
148+
{
149+
"RecNum": { "N": "224" },
150+
"StringSet": { "SS": ["aaa", "ccc", "bbb", "ddd"] },
151+
"NumberSet": { "NS": ["111", "333", "222", "444"] },
152+
"BinarySet": { "BS": ["AQID", "AwQF", "AgME", "BAUG"] }
153+
},
154+
{
155+
"RecNum": { "N": "225" },
156+
"StringSet": { "SS": ["aaa", "bbb", "ccc", "ddd"] },
157+
"NumberSet": { "NS": ["111", "222", "333", "444"] },
158+
"BinarySet": { "BS": ["AQID", "AgME", "AwQF", "BAUG"] }
159+
},
160+
{
161+
"RecNum": { "N": "226" },
162+
"StringSet": { "SS": ["bbb", "aaa", "ccc", "ddd"] },
163+
"NumberSet": { "NS": ["222", "111", "333", "444"] },
164+
"BinarySet": { "BS": ["AgME", "AQID", "AwQF", "BAUG"] }
165+
},
166+
{
167+
"RecNum": { "N": "227" },
168+
"StringSet": { "SS": ["bbb", "aaa", "ddd", "ccc"] },
169+
"NumberSet": { "NS": ["222", "111", "444", "333"] },
170+
"BinarySet": { "BS": ["AgME", "AQID", "BAUG", "AwQF"] }
171+
},
172+
{
173+
"RecNum": { "N": "228" },
174+
"StringSet": { "SS": ["aaa", "bbb", "ddd", "ccc"] },
175+
"NumberSet": { "NS": ["111", "222", "444", "333"] },
176+
"BinarySet": { "BS": ["AQID", "AgME", "BAUG", "AwQF"] }
177+
},
178+
{
179+
"RecNum": { "N": "229" },
180+
"StringSet": { "SS": ["ddd", "bbb", "aaa", "ccc"] },
181+
"NumberSet": { "NS": ["444", "222", "111", "333"] },
182+
"BinarySet": { "BS": ["BAUG", "AgME", "AQID", "AwQF"] }
183+
},
184+
{
185+
"RecNum": { "N": "230" },
186+
"StringSet": { "SS": ["bbb", "ddd", "aaa", "ccc"] },
187+
"NumberSet": { "NS": ["222", "444", "111", "333"] },
188+
"BinarySet": { "BS": ["AgME", "BAUG", "AQID", "AwQF"] }
189+
},
190+
{
191+
"RecNum": { "N": "231" },
192+
"StringSet": { "SS": ["bbb", "aaa", "ddd", "ccc"] },
193+
"NumberSet": { "NS": ["222", "111", "444", "333"] },
194+
"BinarySet": { "BS": ["AgME", "AQID", "BAUG", "AwQF"] }
195+
},
196+
{
197+
"RecNum": { "N": "232" },
198+
"StringSet": { "SS": ["aaa", "bbb", "ddd", "ccc"] },
199+
"NumberSet": { "NS": ["111", "222", "444", "333"] },
200+
"BinarySet": { "BS": ["AQID", "AgME", "BAUG", "AwQF"] }
201+
}
202+
],
203+
"Configs": {
204+
"AllSign": {
205+
"attributeActionsOnEncrypt": {
206+
"RecNum": "SIGN_ONLY",
207+
"StringSet": "SIGN_ONLY",
208+
"NumberSet": "SIGN_ONLY",
209+
"BinarySet": "SIGN_ONLY"
210+
}
211+
},
212+
"AllEncrypt": {
213+
"attributeActionsOnEncrypt": {
214+
"RecNum": "SIGN_ONLY",
215+
"StringSet": "ENCRYPT_AND_SIGN",
216+
"NumberSet": "ENCRYPT_AND_SIGN",
217+
"BinarySet": "ENCRYPT_AND_SIGN"
218+
}
219+
}
220+
}
221+
}
222+
}

‎TestVectors/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/wrapped/TestDynamoDbEncryption.java

Lines changed: 4 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -85,19 +85,17 @@ > GetEncryptedDataKeyDescription(
8585
}
8686
}
8787

88-
public Result<
89-
GetNumberOfQueriesOutput,
90-
Error
91-
> GetNumberOfQueries(
88+
public Result<GetNumberOfQueriesOutput, Error> GetNumberOfQueries(
9289
GetNumberOfQueriesInput dafnyInput
9390
) {
9491
try {
9592
software.amazon.cryptography.dbencryptionsdk.dynamodb.model.GetNumberOfQueriesInput nativeInput =
9693
ToNative.GetNumberOfQueriesInput(dafnyInput);
9794
software.amazon.cryptography.dbencryptionsdk.dynamodb.model.GetNumberOfQueriesOutput nativeOutput =
9895
this._impl.GetNumberOfQueries(nativeInput);
99-
GetNumberOfQueriesOutput dafnyOutput =
100-
ToDafny.GetNumberOfQueriesOutput(nativeOutput);
96+
GetNumberOfQueriesOutput dafnyOutput = ToDafny.GetNumberOfQueriesOutput(
97+
nativeOutput
98+
);
10199
return Result.create_Success(
102100
GetNumberOfQueriesOutput._typeDescriptor(),
103101
Error._typeDescriptor(),

0 commit comments

Comments
 (0)