feat(dafny): Add bucket beacon support by ajewellamz · Pull Request #1943 · aws/aws-database-encryption-sdk-dynamodb

ajewellamz · 2025-06-19T18:56:16Z

Issue #, if available:

Description of changes:

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

…ion-sdk-dynamodb into ajewell/buckets

rishav-karanjit

I have reviewed everything under specification and testVectors. There is one blocking comment in spec. Remaining are suggestions but not blocking.

I will review rest the next time.

rishav-karanjit · 2026-02-16T18:24:31Z

specification/changes/2025-08-25-beacon-partitions/background.md

+and then constrain the number of partitions for the other two beacons.
+
+The partition used to calculate the hash for a constrained beacon is
+`ItemsPartition % BeaconConstraint` where `%` is the `modulo` or `remainder` operation.


Question: is ItemsPartition, the partition number assigned to the whole table?

Answering my own question: ItemsPartition is assigned to each item which is a random number between 0 to max partition. Correct me if I am understanding wrong

specification/changes/2025-08-25-beacon-partitions/background.md

rishav-karanjit · 2026-02-16T19:18:02Z

specification/changes/2025-08-25-beacon-partitions/background.md

+then you will immediately need to start making 7 queries,
+but the sixth and seventh queries will return a comparatively small number of items.
+
+### Beacon Constraints


Question: this should be optional right?

specification/changes/2025-08-25-beacon-partitions/background.md

rishav-karanjit · 2026-02-16T20:17:01Z

specification/changes/2025-08-25-beacon-partitions/change.md

+
+- An integer in the range 0..254
+- The number of the partition currently under consideration in some context
+- For customers not using PartitionBeacons, this is always `1`


Blocking: Shouldn't this be 0?

TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy

TestVectors/dafny/DDBEncryption/src/TestVectors.dfy

rishav-karanjit · 2026-02-17T00:26:12Z

TestVectors/dafny/DDBEncryption/src/TestVectors.dfy

Currently, there are lots of test which is great. In addition to current test, some tests to take into consideration are:

I don't see any test using defaultNumberOfPartitions. So, we might want to check defaultNumberOfPartitions Behavior. Something like:

set defaultNumberOfPartitions to 3

Beacon A: no numberOfPartitions specified, uses 3

Beacon B: numberOfPartitions specified, uses the specific numberOfPartitions

Currently, I see the maximum number of partitions is only 5. I am not too worried when it comes to integer but in addition to current test we at-least might want to test when max number of partitions is 1 which will reflect number of partitions before beacon partition was introduced.

Currently, we query only already existing values. It should be worth it to add a test that queries non existed value and see what it returns

TestVectors/dafny/DDBEncryption/src/TestVectors.dfy

github-actions · 2026-02-17T00:28:54Z

@ajewellamz and @rishav-karanjit, I noticed you are updating the smithy model files.
Does this update need new or updated javadoc trait documentation?
Are you adding constraints inside list, map or union? Do you know about this issue: smithy-lang/smithy-dafny#491?

Co-authored-by: Rishav karanjit <[email protected]>

github-actions · 2026-03-18T18:34:23Z

@ajewellamz and @mahnushm, I noticed you are updating the smithy model files.
Does this update need new or updated javadoc trait documentation?
Are you adding constraints inside list, map or union? Do you know about this issue: smithy-lang/smithy-dafny#491?

rishav-karanjit

I am few comments/question

rishav-karanjit · 2026-03-19T22:00:06Z

DynamoDbEncryption/dafny/DynamoDbEncryption/src/FilterExpr.dfy

+    for i : uint64 := 0 to |values| as uint64
+      invariant result <= bv.numPartitions
+    {
+      var partitions := values[i].0.getNumQueries(bv.numPartitions, values[0].1);


Should the second partition be values[i].1 instead of values[0].1?

rishav-karanjit · 2026-03-19T22:09:49Z

DynamoDbEncryption/dafny/DynamoDbEncryption/src/DDBSupport.dfy

      var keyId :- Filter.GetBeaconKeyId(search.value.curr(), req.KeyConditionExpression, req.FilterExpression, req.ExpressionAttributeValues, req.ExpressionAttributeNames);
-      var oldContext := Filter.ExprContext(req.KeyConditionExpression, req.FilterExpression, req.ExpressionAttributeValues, req.ExpressionAttributeNames);
-      var newContext :- Filter.Beaconize(search.value.curr(), oldContext, keyId);
+      var foo :- ExtractPartition(search.value.curr(), req.FilterExpression, req.KeyConditionExpression, req.ExpressionAttributeNames, req.ExpressionAttributeValues, actions);


I see the function signature of ExtractPartition to be following:

method ExtractPartition(search : SearchableEncryptionInfo.BeaconVersion, keyExpr : Option<string>, filterExpr : Option<string>, names : Option<DDB.ExpressionAttributeNameMap>, values : Option<DDB.ExpressionAttributeValueMap>, actions : AttributeActions) returns (output : Result<(Option<DDB.ExpressionAttributeValueMap>, PartitionNumber), Error>)

The second parameter is keyExpression and 3rd parameter is filter expression but in this line I see the second parameter is filter expression and third parameter is keycondition expression. Am I missing something?

rishav-karanjit · 2026-03-19T22:12:26Z

DynamoDbEncryption/dafny/DynamoDbEncryption/src/DDBSupport.dfy

+    var filterHasEncField := Filter.UsesEncryptedField(Filter.ParseExprOpt(filterExpr), actions, names);
+    var keyHasEncField := Filter.UsesEncryptedField(Filter.ParseExprOpt(keyExpr), actions, names);
+    if keyHasEncField.Some? || filterHasEncField.Some? {
+      return Failure(E("When numberOfPartitions is greater than one, XXXValues must contain " + PartitionName));


"XXXValues" in the error message seems to be a typo?

github-actions · 2026-03-19T23:10:36Z

@ajewellamz and @rishav-karanjit, I noticed you are updating the smithy model files.
Does this update need new or updated javadoc trait documentation?
Are you adding constraints inside list, map or union? Do you know about this issue: smithy-lang/smithy-dafny#491?

Adding partitions to the breacons.

github-actions · 2026-03-26T20:19:03Z

Detected changes to the release files or to the check-files action

github-actions · 2026-03-26T20:19:05Z

Changes to the release files or the check-files action requires 2 approvals from CODEOWNERS

Add comments to clarify the purpose of numQueries.

github-actions · 2026-03-30T21:19:59Z

Detected changes to the release files or to the check-files action

github-actions · 2026-03-30T21:20:00Z

Changes to the release files or the check-files action requires 2 approvals from CODEOWNERS

Updated the default value for PartitionNumber from 1 to 0 for customers not using PartitionBeacons.

github-actions · 2026-03-31T22:59:43Z

Detected changes to the release files or to the check-files action

github-actions · 2026-03-31T22:59:44Z

Changes to the release files or the check-files action requires 2 approvals from CODEOWNERS

chore(dafny): Add bucket beacon support

ac87a66

ajewellamz requested a review from a team as a code owner June 19, 2025 18:56

ajewellamz and others added 28 commits June 19, 2025 15:20

m

da790a0

m

c2746c5

m

7e17008

m

ab174cb

m

9130859

Merge branch 'main' into ajewell/buckets

082a815

m

bd5e532

m

4ff8d8c

m

c3ae7ca

Merge branch 'main' into ajewell/buckets

0370e3c

m

fc77ceb

Merge branch 'main' into ajewell/buckets

8cd220b

Merge branch 'main' into ajewell/buckets

2fbfdc5

m

90822df

m

1388574

m

bee7476

m

8ec3cd5

m

3b71365

m

05cc97d

m

ae0ef6f

m

e96ce28

m

d622567

m

a1814ee

m

d087faf

m

d0ace70

m

0b4fd63

new smithy-dafny

09adff0

m

57080c2

ajewellamz and others added 9 commits October 10, 2025 17:31

m

8cf041d

m

5491603

m

86b328d

Merge branch 'main' into ajewell/buckets

2f6dd1c

m

0b242da

Merge branch 'ajewell/buckets' of github.com:aws/aws-database-encrypt…

096094f

…ion-sdk-dynamodb into ajewell/buckets

Merge branch 'main' into ajewell/buckets

8c4eded

Merge branch 'main' into ajewell/buckets

5536644

Merge branch 'main' into ajewell/buckets

64003f3

rishav-karanjit reviewed Feb 17, 2026

View reviewed changes

mahnushm and others added 4 commits February 20, 2026 09:13

Update specification/changes/2025-08-25-beacon-partitions/background.md

2c4f418

Co-authored-by: Rishav karanjit <[email protected]>

Update TestVectors/dafny/DDBEncryption/src/TestVectors.dfy

1bb16f3

Co-authored-by: Rishav karanjit <[email protected]>

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

e148f29

Co-authored-by: Rishav karanjit <[email protected]>

Update TestVectors/dafny/DDBEncryption/src/TestVectors.dfy

f43f5e5

Co-authored-by: Rishav karanjit <[email protected]>

texastony added 2 commits March 18, 2026 13:35

Merge branch 'main' into ajewell/buckets

3300f8c

fix: typo in test vectors

e1f56d9

rishav-karanjit reviewed Mar 19, 2026

View reviewed changes

rishav-karanjit changed the title ~~chore(dafny): Add bucket beacon support~~ feat(dafny): Add bucket beacon support Mar 19, 2026

Update BasicSearchableEncryptionExample.cs

6d8e4c0

Adding partitions to the breacons.

Clarify numQueries usage with additional comments

6f77834

Add comments to clarify the purpose of numQueries.

Change default PartitionNumber value to 0

9a4c67c

Updated the default value for PartitionNumber from 1 to 0 for customers not using PartitionBeacons.

Conversation

ajewellamz commented Jun 19, 2025

Uh oh!

rishav-karanjit left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

github-actions bot commented Feb 17, 2026

Uh oh!

github-actions bot commented Mar 18, 2026

Uh oh!

rishav-karanjit left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

github-actions bot commented Mar 19, 2026

Uh oh!

github-actions bot commented Mar 26, 2026

Uh oh!

github-actions bot commented Mar 26, 2026

Uh oh!

github-actions bot commented Mar 30, 2026

Uh oh!

github-actions bot commented Mar 30, 2026

Uh oh!

github-actions bot commented Mar 31, 2026

Uh oh!

github-actions bot commented Mar 31, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants