chore(dafny): Add bucket beacon support

Author: ajewellamz

DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy

@@ -17,7 +17,7 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internald
   import AwsCryptographyKeyStoreTypes
   import AwsCryptographyPrimitivesTypes
   import ComAmazonawsDynamodbTypes
-    // Generic helpers for verification of mock/unit tests.
+  // Generic helpers for verification of mock/unit tests.
   datatype DafnyCallEvent<I, O> = DafnyCallEvent(input: I, output: O)
 
   // Begin Generated Types
@@ -46,12 +46,17 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internald
     nameonly compoundBeacons: Option<CompoundBeaconList> := Option.None ,
     nameonly virtualFields: Option<VirtualFieldList> := Option.None ,
     nameonly encryptedParts: Option<EncryptedPartsList> := Option.None ,
-    nameonly signedParts: Option<SignedPartsList> := Option.None
+    nameonly signedParts: Option<SignedPartsList> := Option.None ,
+    nameonly numberOfBuckets: Option<BucketCount> := Option.None
   )
   type BeaconVersionList = x: seq<BeaconVersion> | IsValid_BeaconVersionList(x) witness *
   predicate method IsValid_BeaconVersionList(x: seq<BeaconVersion>) {
     ( 1 <= |x| <= 1 )
   }
+  type BucketCount = x: int32 | IsValid_BucketCount(x) witness *
+  predicate method IsValid_BucketCount(x: int32) {
+    ( 1 <= x  )
+  }
   type Char = x: string | IsValid_Char(x) witness *
   predicate method IsValid_Char(x: string) {
     ( 1 <= |x| <= 1 )

DynamoDbEncryption/dafny/DynamoDbEncryption/Model/DynamoDbEncryption.smithy

@@ -286,6 +286,9 @@ integer BeaconBitLength
 @range(min: 1)
 integer VersionNumber
 
+@range(min: 1)
+integer BucketCount
+
 @length(min: 1, max: 1)
 string Char
 
@@ -796,6 +799,8 @@ structure BeaconVersion {
   encryptedParts : EncryptedPartsList,
   @javadoc("The list of Signed Parts that may be included in any compound beacon.")
   signedParts : SignedPartsList,
+  @javadoc("The number of separate buckets across which beacons should be divided.")
+  numberOfBuckets : BucketCount
 }
 
 //= specification/searchable-encryption/search-config.md#initialization

DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy

@@ -17,7 +17,7 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.transform
   import AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes
   import AwsCryptographyMaterialProvidersTypes
   import ComAmazonawsDynamodbTypes
-    // Generic helpers for verification of mock/unit tests.
+  // Generic helpers for verification of mock/unit tests.
   datatype DafnyCallEvent<I, O> = DafnyCallEvent(input: I, output: O)
 
   // Begin Generated Types

DynamoDbEncryption/dafny/DynamoDbItemEncryptor/Model/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes.dfy

@@ -17,7 +17,7 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencry
   import AwsCryptographyMaterialProvidersTypes
   import AwsCryptographyPrimitivesTypes
   import ComAmazonawsDynamodbTypes
-    // Generic helpers for verification of mock/unit tests.
+  // Generic helpers for verification of mock/unit tests.
   datatype DafnyCallEvent<I, O> = DafnyCallEvent(input: I, output: O)
 
   // Begin Generated Types

DynamoDbEncryption/dafny/StructuredEncryption/Model/AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes.dfy

@@ -11,7 +11,7 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.structuredencrypti
   import opened UTF8
   import AwsCryptographyMaterialProvidersTypes
   import AwsCryptographyPrimitivesTypes
-    // Generic helpers for verification of mock/unit tests.
+  // Generic helpers for verification of mock/unit tests.
   datatype DafnyCallEvent<I, O> = DafnyCallEvent(input: I, output: O)
 
   // Begin Generated Types