m

Author: ajewellamz

DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy

@@ -317,7 +317,7 @@ module SearchConfigToInfo {
     }
 
     var numBuckets : int := config.numberOfBuckets.UnwrapOr(1) as int;
-    :- Need(0 <= numBuckets < INT32_MAX_LIMIT, E("Invalid number of buckets specified, " + Base10Int2String(numBuckets) + ", must be 0 < numberOfBuckets <= 255."));
+    :- Need(0 <= numBuckets < MAX_BUCKET_COUNT, E("Invalid number of buckets specified, " + Base10Int2String(numBuckets) + ", must be 0 < numberOfBuckets <= 255."));
     // Zero is invalid, but in Java we can't distinguish None from Some(0)
     if numBuckets == 0 {
       numBuckets := 1;
@@ -328,7 +328,7 @@ module SearchConfigToInfo {
         beacons,
         virtualFields,
         outer.attributeActionsOnEncrypt,
-        numBuckets as uint32
+        numBuckets as BucketCount
       );
   }
 

DynamoDbEncryption/dafny/DynamoDbEncryption/src/DDBSupport.dfy

@@ -271,7 +271,8 @@ module DynamoDBSupport {
   // Extract aws_dbe_bucket = NN from filterExpr and return bucket
   method ExtractBucket(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>, BucketNumber, Option<BucketCount>), Error>)
-    ensures output.Success? && output.value.2.Some? ==> output.value.1 < output.value.2.value
+    ensures output.Success? ==> output.value.1 < search.numBuckets
+    ensures output.Success? && output.value.2.Some? ==> output.value.1 < output.value.2.value <= search.numBuckets
   {
     if search.numBuckets <= 1 {
       :- Need(values.None? || BucketName !in values.value, E(""));

DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DdbMiddlewareConfig.dfy

@@ -78,15 +78,12 @@ module DdbMiddlewareConfig {
     if config.search.None? {
       return Success(0);
     }
-    var numBuckets : uint32 := config.search.value.versions[0].numBuckets;
+    var numBuckets := config.search.value.versions[0].numBuckets;
     if numBuckets <= 1 {
       return Success(0);
     }
-    if (numBuckets > 255) {
-      return Failure(E("Number of buckets exceeds 255"));
-    }
 
-    var outR := config.bucketSelector.GetBucketNumber(DDBE.GetBucketNumberInput(item := item, numberOfBuckets := numBuckets as DDBE.BucketCount));
+    var outR := config.bucketSelector.GetBucketNumber(DDBE.GetBucketNumberInput(item := item, numberOfBuckets := numBuckets));
     var out :- outR.MapFailure(e => AwsCryptographyDbEncryptionSdkDynamoDb(e));
     if out.bucketNumber == 0 {
       return Success(0);