Skip to content

Commit 787a15c

Browse files
ajewellamzajewellamz
committed
m
1 parent 6ed336b commit 787a15c

File tree

10 files changed

+1883
-1830
lines changed

10 files changed

+1883
-1830
lines changed

‎DynamoDbEncryption/codegen-patches/DynamoDbEncryptionTransforms/dotnet/dafny-4.8.0.patch‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
diff --git b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs
2-
index 024d2aeb..fae8db3b 100644
2+
index b7d2a823..0c973183 100644
33
--- b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs
44
+++ a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs
55
@@ -7,10 +7,6 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb.Transforms
@@ -10,6 +10,6 @@ index 024d2aeb..fae8db3b 100644
1010
-
1111
- private const string ISO8601DateFormatNoMS = "yyyy-MM-dd\\THH:mm:ss\\Z";
1212
-
13-
public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.DynamoDbTablesEncryptionConfig FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S30_DynamoDbTablesEncryptionConfig(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IDynamoDbTablesEncryptionConfig value)
13+
public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.AsSet FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S5_AsSet(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IAsSet value)
1414
{
15-
software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.DynamoDbTablesEncryptionConfig concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.DynamoDbTablesEncryptionConfig)value; AWS.Cryptography.DbEncryptionSDK.DynamoDb.DynamoDbTablesEncryptionConfig converted = new AWS.Cryptography.DbEncryptionSDK.DynamoDb.DynamoDbTablesEncryptionConfig(); converted.TableEncryptionConfigs = (System.Collections.Generic.Dictionary<string, AWS.Cryptography.DbEncryptionSDK.DynamoDb.DynamoDbTableEncryptionConfig>)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S30_DynamoDbTablesEncryptionConfig__M22_tableEncryptionConfigs(concrete._tableEncryptionConfigs); return converted;
15+
software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.AsSet concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.AsSet)value; AWS.Cryptography.DbEncryptionSDK.DynamoDb.AsSet converted = new AWS.Cryptography.DbEncryptionSDK.DynamoDb.AsSet(); return converted;

‎DynamoDbEncryption/codegen-patches/DynamoDbItemEncryptor/dotnet/dafny-4.8.0.patch‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
diff --git b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs
2-
index e8ca3ce8..35957991 100644
2+
index b4a90d1b..b5d5046a 100644
33
--- b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs
44
+++ a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs
55
@@ -7,10 +7,6 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor
@@ -10,6 +10,6 @@ index e8ca3ce8..35957991 100644
1010
-
1111
- private const string ISO8601DateFormatNoMS = "yyyy-MM-dd\\THH:mm:ss\\Z";
1212
-
13-
public static AWS.Cryptography.Primitives.AwsCryptographicPrimitives FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S25_AtomicPrimitivesReference(software.amazon.cryptography.primitives.internaldafny.types.IAwsCryptographicPrimitivesClient value)
13+
public static System.Collections.Generic.Dictionary<string, AWS.Cryptography.DbEncryptionSDK.StructuredEncryption.CryptoAction> FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S16_AttributeActions(Dafny.IMap<Dafny.ISequence<char>, software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny.types._ICryptoAction> value)
1414
{
15-
if (value is software.amazon.cryptography.primitives.internaldafny.types.IAwsCryptographicPrimitivesClient dafnyValue)
15+
return value.ItemEnumerable.ToDictionary(pair => FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S16_AttributeActions__M3_key(pair.Car), pair => FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S16_AttributeActions__M5_value(pair.Cdr));

‎DynamoDbEncryption/codegen-patches/StructuredEncryption/dotnet/dafny-4.8.0.patch‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
diff --git b/DynamoDbEncryption/runtimes/net/Generated/StructuredEncryption/TypeConversion.cs a/DynamoDbEncryption/runtimes/net/Generated/StructuredEncryption/TypeConversion.cs
2-
index b01717ff..02de5d49 100644
2+
index df81f311..ac28fc2a 100644
33
--- b/DynamoDbEncryption/runtimes/net/Generated/StructuredEncryption/TypeConversion.cs
44
+++ a/DynamoDbEncryption/runtimes/net/Generated/StructuredEncryption/TypeConversion.cs
55
@@ -7,10 +7,6 @@ namespace AWS.Cryptography.DbEncryptionSDK.StructuredEncryption
@@ -10,6 +10,6 @@ index b01717ff..02de5d49 100644
1010
-
1111
- private const string ISO8601DateFormatNoMS = "yyyy-MM-dd\\THH:mm:ss\\Z";
1212
-
13-
public static AWS.Cryptography.Primitives.AwsCryptographicPrimitives FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N20_structuredEncryption__S25_AtomicPrimitivesReference(software.amazon.cryptography.primitives.internaldafny.types.IAwsCryptographicPrimitivesClient value)
13+
public static AWS.Cryptography.Primitives.AtomicPrimitives FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N20_structuredEncryption__S25_AtomicPrimitivesReference(software.amazon.cryptography.primitives.internaldafny.types.IAwsCryptographicPrimitivesClient value)
1414
{
1515
if (value is software.amazon.cryptography.primitives.internaldafny.types.IAwsCryptographicPrimitivesClient dafnyValue)

‎DynamoDbEncryption/dafny/DynamoDbEncryption/src/DDBSupport.dfy‎

Lines changed: 19 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -236,6 +236,20 @@ module DynamoDBSupport {
236236
Failure(E("Value of " + name + " is not numeric (i.e. 'N')"))
237237
}
238238

239+
// Unlike Query, Scan must not specify BucketName nor BucketQueriesName
240+
function method TestBucketForScan(names : Option<DDB.ExpressionAttributeValueMap>)
241+
: Result<bool, Error>
242+
{
243+
if names.None? then
244+
Success(true)
245+
else if BucketName in names.value then
246+
Failure(E("A value for " + BucketName + " must not be specified for Scan operations."))
247+
else if BucketQueriesName in names.value then
248+
Failure(E("A value for " + BucketQueriesName + " must not be specified for Scan operations."))
249+
else
250+
Success(true)
251+
}
252+
239253
// If names[":aws_dbe_bucket"] holds S(N)' return (Some(names - {":aws_dbe_bucket"}), Some(N))
240254
// else return (None, None)
241255
function method ExtractBucketNumber(names : Option<DDB.ExpressionAttributeValueMap>)
@@ -400,10 +414,11 @@ module DynamoDBSupport {
400414
return Success(req);
401415
} else {
402416
var keyId :- Filter.GetBeaconKeyId(search.value.curr(), None, req.FilterExpression, req.ExpressionAttributeValues, req.ExpressionAttributeNames);
403-
var foo :- ExtractBucket(search.value.curr(), req.FilterExpression, None, req.ExpressionAttributeNames, req.ExpressionAttributeValues, actions);
404-
var (newValues, bucket, bucket_queries) := foo;
405-
var context := Filter.ExprContext(None, req.FilterExpression, newValues, req.ExpressionAttributeNames);
406-
var newContext :- Filter.DoBeaconize(search.value.curr(), context, keyId, bucket, bucket_queries);
417+
var _ :- TestBucketForScan(req.ExpressionAttributeValues);
418+
var context := Filter.ExprContext(None, req.FilterExpression, req.ExpressionAttributeValues, req.ExpressionAttributeNames);
419+
// For Scan, we always treat it as {:aws_dbe_bucket := 0, :aws_dbe_bucket_queries := 1}
420+
var numQueries := if search.value.curr().numBuckets == 1 then None else Some(1);
421+
var newContext :- Filter.DoBeaconize(search.value.curr(), context, keyId, 0, Some(1));
407422
return Success(req.(
408423
FilterExpression := newContext.filterExpr,
409424
ExpressionAttributeNames := newContext.names,

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

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1789,6 +1789,18 @@ module DynamoDBFilterExpr {
17891789
var result_filter := old_context.filterExpr.value;
17901790
var new_values := SortedSets.ComputeSetToSequence(new_context.values.value.Keys);
17911791
SequenceIsSafeBecauseItIsInMemory(new_values);
1792+
var allUnchanged := true;
1793+
for i : uint64 := 0 to |new_values| as uint64
1794+
{
1795+
if new_values[i] !in old_context.values.value {
1796+
allUnchanged := false;
1797+
break;
1798+
}
1799+
}
1800+
if allUnchanged {
1801+
return Success(old_context);
1802+
}
1803+
17921804
for i : uint64 := 0 to |new_values| as uint64
17931805
{
17941806
var key := new_values[i];

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -310,6 +310,7 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.transform
310310

311311
constructor {:vcs_split_on_every_assert} (config: Operations.InternalConfig)
312312
{
313+
assert Operations.ValidInternalConfig?(config);
313314
this.config := config;
314315
History := new IDynamoDbEncryptionTransformsClientCallHistory();
315316
Modifies := Operations.ModifiesInternalConfig(config) + {History};

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

Lines changed: 27 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -80,7 +80,6 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
8080
ensures GetBucketNumberEnsuresPublicly(input, output)
8181
ensures unchanged(History)
8282
{
83-
// print "\nGetBucketNumber\n", input.item, "\n";
8483
expect "PreferredBucket" in input.item;
8584
expect input.item["PreferredBucket"].N?;
8685
var bucket :- expect StrToInt(input.item["PreferredBucket"].N);
@@ -241,8 +240,30 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
241240
}
242241
}
243242

244-
method TestBucketQueries(client : DDB.IDynamoDBClient, numQueries : nat, q : DDB.QueryInput, queryName : string, custom : bool := false, filtered : bool := false)
243+
method TestBucketQueryFailure(client : DDB.IDynamoDBClient, bucket : nat, query : DDB.QueryInput, counts : array<int>, queryName : string, custom : bool, filtered : bool, numQueries : nat)
244+
requires counts.Length == 100
245+
requires client.ValidState()
246+
requires client.Modifies !! {counts}
245247
requires 0 < numQueries
248+
ensures client.ValidState()
249+
modifies client.Modifies
250+
modifies counts
251+
{
252+
var bucketNumber := DDB.AttributeValue.N(String.Base10Int2String(bucket));
253+
var values : DDB.ExpressionAttributeValueMap := query.ExpressionAttributeValues.UnwrapOr(map[]);
254+
values := values[":aws_dbe_bucket" := bucketNumber];
255+
if filtered {
256+
var bucketQueries := DDB.AttributeValue.N(String.Base10Int2String(numQueries));
257+
values := values[":aws_dbe_bucket_queries" := bucketQueries];
258+
}
259+
var q := query.(ExpressionAttributeValues := Some(values));
260+
var result := client.Query(q);
261+
// expect result.Failure?;
262+
}
263+
264+
265+
method TestBucketQueries(client : DDB.IDynamoDBClient, numQueries : nat, q : DDB.QueryInput, queryName : string, custom : bool := false, filtered : bool := false)
266+
requires 0 < numQueries <= 5
246267
requires client.ValidState()
247268
ensures client.ValidState()
248269
modifies client.Modifies
@@ -251,6 +272,10 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
251272
for i := 0 to numQueries {
252273
DoBucketQuery(client, i, q, counts, queryName, custom, filtered, numQueries);
253274
}
275+
for i := numQueries to 5 {
276+
TestBucketQueryFailure(client, i, q, counts, queryName, custom, filtered, numQueries);
277+
}
278+
254279
var wasBad : bool := false;
255280
for i := 0 to 100 {
256281
if counts[i] == 0 {

0 commit comments

Comments
 (0)