m

Author: ajewellamz

DynamoDbEncryption/dafny/DynamoDbEncryption/Model/DynamoDbEncryption.smithy

@@ -61,6 +61,14 @@ operation GetBucketNumber {
   output: GetBucketNumberOutput,
 }
 
+//= specification/searchable-encryption/search-config.md#bucket-selector
+//= type=implication
+//# GetBucketNumber 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 logical table name for this defined in the associated [table config](../dynamodb-encryption-client/ddb-table-encryption-config.md#structure).
+
 structure GetBucketNumberInput {
   @required
   item: AttributeMap,
@@ -70,6 +78,12 @@ structure GetBucketNumberInput {
   logicalTableName: String,
 }
 
+//= specification/searchable-encryption/search-config.md#bucket-selector
+//= type=implication
+//# GetBucketNumber MUST return
+//#
+//# - The number of the bucket to use for this item
+
 structure GetBucketNumberOutput {
   @required
   bucketNumber: BucketNumber

DynamoDbEncryption/dafny/DynamoDbEncryption/src/Beacon.dfy

@@ -147,6 +147,9 @@ module BaseBeacon {
     numberOfBuckets : BucketCount
   ) {
 
+    //= specification/searchable-encryption/beacons.md#beacon-constraint
+    //# If an item is being written or queried as bucket `X`, but the [standard beacon](#standard-beacon-initialization) is constrained to only `N` buckets,
+    //# then the bucket used to [encode](#bucket-beacon-encoding) the beacon MUST be `X % N`, where `%` is the modulo or remainder operation.
     function method constrained_bucket(bucket : BucketNumber) : BucketBytes
     {
       if numberOfBuckets == 0 || bucket == 0 then
@@ -165,6 +168,8 @@ module BaseBeacon {
 
                 && |ret.value| == (((length as uint8) + 3) / 4) as nat
     {
+      //= specification/searchable-encryption/beacons.md#value-for-a-non-set-standard-beacon
+      //# - The serialized form MUST be augmented as per [bucket beacon encoding](#bucket-beacon-encoding).
       base.hash(val, key, length, constrained_bucket(bucket))
     }
 

DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy

@@ -294,6 +294,8 @@ module SearchConfigToInfo {
       true
     }
 
+    //= specification/searchable-encryption/search-config.md#bucket-selector
+    //# The default implementation of the Bucket Selector MUST return a random number within the acceptable range, i.e.
     method GetBucketNumber'(input: GetBucketNumberInput)
       returns (output: Result<GetBucketNumberOutput, Error> )
       requires ValidState()
@@ -331,14 +333,30 @@ module SearchConfigToInfo {
               && fresh(output.value.bucketSelector.Modifies)
   {
     var maxBuckets : BucketCount := config.maximumNumberOfBuckets.UnwrapOr(1);
-    var defaultBuckets : BucketCount := config.defaultNumberOfBuckets.UnwrapOr(maxBuckets);
-    :- Need(0 <= maxBuckets as nat < MAX_BUCKET_COUNT, E("Invalid number of buckets specified, " + Base10Int2String(maxBuckets as int) + ", must be 0 < maximumNumberOfBuckets <= 255."));
+    :- Need(0 <= maxBuckets as nat < MAX_BUCKET_COUNT, E("Invalid maximumNumberOfBuckets specified, " + Base10Int2String(maxBuckets as int) + ", must be 0 < maximumNumberOfBuckets <= 255."));
     // Zero is invalid, but in Java we can't distinguish None from Some(0)
     if maxBuckets == 0 {
       maxBuckets := 1;
     }
-    if defaultBuckets == 0 {
+
+    var defaultBucketsOpt : Option<BucketCount> := config.defaultNumberOfBuckets;
+    var defaultBuckets;
+
+    //= specification/searchable-encryption/search-config.md#default-buckets
+    //# If not set, Default Buckets MUST default to [Max Buckets](#max-buckets).
+    if defaultBucketsOpt.None? || defaultBucketsOpt.value == 0 {
       defaultBuckets := maxBuckets;
+
+      //= specification/searchable-encryption/search-config.md#beacon-version-initialization
+      //# Initialization MUST fail if [default number of buckets](#default-buckets) is greater than or equal to [maximum number of buckets](#max-buckets).
+
+      // if maximumNumberOfBuckets is not set, then maxBuckets == 1, and so this is also covered
+      //= specification/searchable-encryption/search-config.md#beacon-version-initialization
+      //# Initialization MUST fail if [default number of buckets](#default-buckets) is supplied but [maximum number of buckets](#max-buckets) is not.
+    } else if maxBuckets <= defaultBucketsOpt.value {
+      return(E("Invalid defaultNumberOfBuckets specified, " + Base10Int2String(defaultBucketsOpt.value as int) + ", must be 0 < defaultNumberOfBuckets < maximumNumberOfBuckets."));
+    } else {
+      defaultBuckets := defaultBucketsOpt.value;
     }
 
     var virtualFields :- ConvertVirtualFields(outer, config.virtualFields);
@@ -602,6 +620,9 @@ module SearchConfigToInfo {
     else if inner.value < maxBuckets then
       Success(inner.value)
     else
+      //= specification/searchable-encryption/beacons.md#standard-beacon-initialization
+      //# Initialization MUST fail if [number of buckets](#beacon-constraint) is specified, and is greater than or equal to
+      //# the maximum number of buckets specified in the [beacon version](search-config.md#beacon-version-initialization).
       Failure(E("Constrained numberOfBuckets for  " + name + " is " + Base10Int2String(inner.value as int) + " but it must be less than the maximumNumberOfBuckets " + Base10Int2String(maxBuckets as int)))
   }
 

DynamoDbEncryption/dafny/DynamoDbEncryption/src/Util.dfy

@@ -96,8 +96,12 @@ module DynamoDbEncryptionUtil {
 
   function method BucketNumberToBytes(x : BucketNumber) : BucketBytes
   {
+    //= specification/searchable-encryption/beacons.md#bucket-beacon-encoding
+    //# If this number is zero, then the input sequence of bytes MUST be returned unchanged.
     if x == 0 then
       []
+    //= specification/searchable-encryption/beacons.md#bucket-beacon-encoding
+    //# Otherwise, a single byte with a value equal to this calculated bucket number, MUST be appended to the input sequence of bytes.
     else
       [x as uint8]
   }

DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/DynamoDbEncryptionTransforms.smithy

@@ -81,10 +81,18 @@ operation GetNumberOfQueries {
     input: GetNumberOfQueriesInput,
     output: GetNumberOfQueriesOutput,
 }
+
+//= specification/dynamodb-encryption-client/ddb-get-number-of-queries.md#input
+//= type=implication
+//# This operation MUST take as input the QueryInput structure under consideration.
 structure GetNumberOfQueriesInput {
     @required
     input: QueryInput
 }
+
+//= specification/dynamodb-encryption-client/ddb-get-number-of-queries.md#input
+//= type=implication
+//# This operation MUST return the number of queries necessary.
 structure GetNumberOfQueriesOutput {
     @required
     numberOfQueries: BucketCount

specification/searchable-encryption/search-config.md

@@ -558,7 +558,7 @@ If not set, Max Buckets MUST default to `1`, which is synonymous with "no bucket
 The Default Buckets setting a [beacon version](#beacon-version-initialization) configures the number of buckets used by all
 [standard beacons](beacons.md#standard-beacon-initialization) that do not directly specify a number of buckets.
 
-If not set, Max Buckets MUST default to [Max Buckets](#max-buckets).
+If not set, Default Buckets MUST default to [Max Buckets](#max-buckets).
 
 ### Bucket Selector