rename bucket to partition

Author: ajewellamz

DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy

@@ -47,29 +47,29 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internald
     nameonly virtualFields: Option<VirtualFieldList> := Option.None ,
     nameonly encryptedParts: Option<EncryptedPartsList> := Option.None ,
     nameonly signedParts: Option<SignedPartsList> := Option.None ,
-    nameonly maximumNumberOfBuckets: Option<BucketCount> := Option.None ,
-    nameonly defaultNumberOfBuckets: Option<BucketCount> := Option.None ,
-    nameonly bucketSelector: Option<IBucketSelector> := Option.None
+    nameonly maximumNumberOfPartitions: Option<PartitionCount> := Option.None ,
+    nameonly defaultNumberOfPartitions: Option<PartitionCount> := Option.None ,
+    nameonly partitionSelector: Option<IPartitionSelector> := 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) {
+  type PartitionCount = x: int32 | IsValid_PartitionCount(x) witness *
+  predicate method IsValid_PartitionCount(x: int32) {
     ( 1 <= x <= 255 )
   }
-  type BucketNumber = x: int32 | IsValid_BucketNumber(x) witness *
-  predicate method IsValid_BucketNumber(x: int32) {
+  type PartitionNumber = x: int32 | IsValid_PartitionNumber(x) witness *
+  predicate method IsValid_PartitionNumber(x: int32) {
     ( 0 <= x <= 254 )
   }
-  class IBucketSelectorCallHistory {
+  class IPartitionSelectorCallHistory {
     ghost constructor() {
-      GetBucketNumber := [];
+      GetPartitionNumber := [];
     }
-    ghost var GetBucketNumber: seq<DafnyCallEvent<GetBucketNumberInput, Result<GetBucketNumberOutput, Error>>>
+    ghost var GetPartitionNumber: seq<DafnyCallEvent<GetPartitionNumberInput, Result<GetPartitionNumberOutput, Error>>>
   }
-  trait {:termination false} IBucketSelector
+  trait {:termination false} IPartitionSelector
   {
     // Helper to define any additional modifies/reads clauses.
     // If your operations need to mutate state,
@@ -95,36 +95,36 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internald
     // You MUST also ensure ValidState in your constructor.
     predicate ValidState()
       ensures ValidState() ==> History in Modifies
-    ghost const History: IBucketSelectorCallHistory
-    predicate GetBucketNumberEnsuresPublicly(input: GetBucketNumberInput , output: Result<GetBucketNumberOutput, Error>)
+    ghost const History: IPartitionSelectorCallHistory
+    predicate GetPartitionNumberEnsuresPublicly(input: GetPartitionNumberInput , output: Result<GetPartitionNumberOutput, Error>)
     // The public method to be called by library consumers
-    method GetBucketNumber ( input: GetBucketNumberInput )
-      returns (output: Result<GetBucketNumberOutput, Error>)
+    method GetPartitionNumber ( input: GetPartitionNumberInput )
+      returns (output: Result<GetPartitionNumberOutput, Error>)
       requires
         && ValidState()
       modifies Modifies - {History} ,
-               History`GetBucketNumber
+               History`GetPartitionNumber
       // Dafny will skip type parameters when generating a default decreases clause.
       decreases Modifies - {History}
       ensures
         && ValidState()
-      ensures GetBucketNumberEnsuresPublicly(input, output)
-      ensures History.GetBucketNumber == old(History.GetBucketNumber) + [DafnyCallEvent(input, output)]
+      ensures GetPartitionNumberEnsuresPublicly(input, output)
+      ensures History.GetPartitionNumber == old(History.GetPartitionNumber) + [DafnyCallEvent(input, output)]
     {
-      output := GetBucketNumber' (input);
-      History.GetBucketNumber := History.GetBucketNumber + [DafnyCallEvent(input, output)];
+      output := GetPartitionNumber' (input);
+      History.GetPartitionNumber := History.GetPartitionNumber + [DafnyCallEvent(input, output)];
     }
     // The method to implement in the concrete class.
-    method GetBucketNumber' ( input: GetBucketNumberInput )
-      returns (output: Result<GetBucketNumberOutput, Error>)
+    method GetPartitionNumber' ( input: GetPartitionNumberInput )
+      returns (output: Result<GetPartitionNumberOutput, Error>)
       requires
         && ValidState()
       modifies Modifies - {History}
       // Dafny will skip type parameters when generating a default decreases clause.
       decreases Modifies - {History}
       ensures
         && ValidState()
-      ensures GetBucketNumberEnsuresPublicly(input, output)
+      ensures GetPartitionNumberEnsuresPublicly(input, output)
       ensures unchanged(History)
 
   }
@@ -348,13 +348,13 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internald
   datatype GetBranchKeyIdFromDdbKeyOutput = | GetBranchKeyIdFromDdbKeyOutput (
     nameonly branchKeyId: string
   )
-  datatype GetBucketNumberInput = | GetBucketNumberInput (
+  datatype GetPartitionNumberInput = | GetPartitionNumberInput (
     nameonly item: ComAmazonawsDynamodbTypes.AttributeMap ,
-    nameonly numberOfBuckets: BucketCount ,
+    nameonly numberOfPartitions: PartitionCount ,
     nameonly logicalTableName: string
   )
-  datatype GetBucketNumberOutput = | GetBucketNumberOutput (
-    nameonly bucketNumber: BucketNumber
+  datatype GetPartitionNumberOutput = | GetPartitionNumberOutput (
+    nameonly partitionNumber: PartitionNumber
   )
   datatype GetEncryptedDataKeyDescriptionInput = | GetEncryptedDataKeyDescriptionInput (
     nameonly input: GetEncryptedDataKeyDescriptionUnion
@@ -482,7 +482,7 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internald
     nameonly length: BeaconBitLength ,
     nameonly loc: Option<TerminalLocation> := Option.None ,
     nameonly style: Option<BeaconStyle> := Option.None ,
-    nameonly numberOfBuckets: Option<BucketCount> := Option.None
+    nameonly numberOfPartitions: Option<PartitionCount> := Option.None
   )
   type StandardBeaconList = x: seq<StandardBeacon> | IsValid_StandardBeaconList(x) witness *
   predicate method IsValid_StandardBeaconList(x: seq<StandardBeacon>) {

DynamoDbEncryption/dafny/DynamoDbEncryption/Model/DynamoDbEncryption.smithy

@@ -49,44 +49,44 @@ service DynamoDbEncryption {
     errors: [ DynamoDbEncryptionException ]
 }
 
-resource BucketSelector {
-  operations: [GetBucketNumber]
+resource PartitionSelector {
+  operations: [GetPartitionNumber]
 }
 
-@reference(resource: BucketSelector)
-structure BucketSelectorReference {}
+@reference(resource: PartitionSelector)
+structure PartitionSelectorReference {}
 
-operation GetBucketNumber {
-  input: GetBucketNumberInput,
-  output: GetBucketNumberOutput,
+operation GetPartitionNumber {
+  input: GetPartitionNumberInput,
+  output: GetPartitionNumberOutput,
 }
 
-//= specification/searchable-encryption/search-config.md#bucket-selector
+//= specification/searchable-encryption/search-config.md#partition-selector
 //= type=implication
-//# GetBucketNumber MUST take as input
+//# GetPartitionNumber MUST take as input
 //#
 //# - A DynamoDB Item (i.e an AttributeMap)
-//# - The [number of buckets](#max-buckets) defined in the associated [beacon version](#beacon-version-initialization).
+//# - The [number of partitions](#max-partitions) defined in the associated [beacon version](#beacon-version-initialization).
 //# - The logical table name for this defined in the associated [table config](../dynamodb-encryption-client/ddb-table-encryption-config.md#structure).
 
-structure GetBucketNumberInput {
+structure GetPartitionNumberInput {
   @required
   item: AttributeMap,
   @required
-  numberOfBuckets : BucketCount,
+  numberOfPartitions : PartitionCount,
   @required
   logicalTableName: String,
 }
 
-//= specification/searchable-encryption/search-config.md#bucket-selector
+//= specification/searchable-encryption/search-config.md#partition-selector
 //= type=implication
-//# GetBucketNumber MUST return
+//# GetPartitionNumber MUST return
 //#
-//# - The number of the bucket to use for this item
+//# - The number of the partition to use for this item
 
-structure GetBucketNumberOutput {
+structure GetPartitionNumberOutput {
   @required
-  bucketNumber: BucketNumber
+  partitionNumber: PartitionNumber
 }
 
 @javadoc("Returns encrypted data key description.")
@@ -327,10 +327,10 @@ integer BeaconBitLength
 integer VersionNumber
 
 @range(min: 1, max: 255)
-integer BucketCount
+integer PartitionCount
 
 @range(min: 0, max: 254)
-integer BucketNumber
+integer PartitionNumber
 
 @length(min: 1, max: 1)
 string Char
@@ -715,8 +715,8 @@ structure StandardBeacon {
   loc : TerminalLocation,
   @javadoc("Optional augmented behavior.")
   style : BeaconStyle,
-  @javadoc("The number of separate buckets across which this particular beacon should be divided. Ths must be no greater than the global numberOfBuckets, and can never be changed once an item containing this beacon has been written.")
-  numberOfBuckets : BucketCount
+  @javadoc("The number of separate partitions across which this particular beacon should be divided. Ths must be no greater than the global numberOfPartitions, and can never be changed once an item containing this beacon has been written.")
+  numberOfPartitions : PartitionCount
 }
 
 //= specification/searchable-encryption/beacons.md#compound-beacon-initialization
@@ -845,14 +845,14 @@ structure BeaconVersion {
   @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.")
-  maximumNumberOfBuckets : BucketCount,
+  @javadoc("The number of separate partitions across which beacons should be divided.")
+  maximumNumberOfPartitions : PartitionCount,
 
-  @javadoc("The number of buckets for any beacon that doesn't specify a numberOfBuckets")
-  defaultNumberOfBuckets : BucketCount,
+  @javadoc("The number of partitions for any beacon that doesn't specify a numberOfPartitions")
+  defaultNumberOfPartitions : PartitionCount,
 
-  @javadoc("How to choose the bucket for an item. Default behavior is a random between 0 and maximumNumberOfBuckets.")
-  bucketSelector: BucketSelectorReference,
+  @javadoc("How to choose the partition for an item. Default behavior is a random between 0 and maximumNumberOfPartitions.")
+  partitionSelector: PartitionSelectorReference,
 }
 
 //= specification/searchable-encryption/search-config.md#initialization