Skip to content

chore(dafny): Add bucket beacon support#1943

Open
ajewellamz wants to merge 103 commits intomainfrom
ajewell/buckets
Open

chore(dafny): Add bucket beacon support#1943
ajewellamz wants to merge 103 commits intomainfrom
ajewell/buckets

Conversation

@ajewellamz
Copy link
Contributor

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.

@ajewellamz ajewellamz requested a review from a team as a code owner June 19, 2025 18:56
@github-actions
Copy link

@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?

@github-actions
Copy link

@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?

@github-actions
Copy link

@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?

mahnushm
mahnushm previously approved these changes Sep 29, 2025
@github-actions
Copy link

@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?

Copy link
Member

@rishav-karanjit rishav-karanjit left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

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.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

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
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Question: this should be optional right?


- 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`
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Blocking: Shouldn't this be 0?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

  1. 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
  2. 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.
  3. 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

@github-actions
Copy link

@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?

mahnushm and others added 4 commits February 20, 2026 09:13
Co-authored-by: Rishav karanjit <karanjitrishav4@gmail.com>
Co-authored-by: Rishav karanjit <karanjitrishav4@gmail.com>
Co-authored-by: Rishav karanjit <karanjitrishav4@gmail.com>
Co-authored-by: Rishav karanjit <karanjitrishav4@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

5 participants