m

Author: ajewellamz

DynamoDbEncryption/dafny/DynamoDbEncryption/src/DDBSupport.dfy

@@ -307,7 +307,6 @@ module DynamoDBSupport {
       return Success(req);
     } else {
       var keyId :- Filter.GetBeaconKeyId(search.value.curr(), req.KeyConditionExpression, req.FilterExpression, req.ExpressionAttributeValues, req.ExpressionAttributeNames);
-
       var foo :- ExtractBucket(search.value.curr(), req.FilterExpression, req.KeyConditionExpression, req.ExpressionAttributeNames, req.ExpressionAttributeValues, actions);
       var (newValues, bucket) := foo;
       var numQueries :- Filter.GetNumQueries(actions, req.KeyConditionExpression, req.ExpressionAttributeNames, search.value.curr());

DynamoDbEncryption/dafny/DynamoDbEncryption/src/FilterExpr.dfy

@@ -1999,7 +1999,7 @@ module DynamoDBFilterExpr {
 
   // return the number of queries necessary for these encrypted attributes
   method GetNumQueriesForAttrs(attrs : seq<string>, b : SI.BeaconVersion) returns (output : Result<BucketCount, Error>)
-    ensures output.Success? ==> 0 < output.value
+    ensures output.Success? ==> output.value <= b.numBuckets
   {
     if |attrs| == 0 {
       return Success(1);
@@ -2031,6 +2031,7 @@ module DynamoDBFilterExpr {
     b : SI.BeaconVersion
   )
     returns (output : Result<BucketCount, Error>)
+    ensures output.Success? ==> output.value <= b.numBuckets
   {
     if expr.None? {
       return Success(1);

DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy

@@ -545,9 +545,13 @@ module SearchableEncryptionInfo {
     | Compound(cmp : CompoundBeacon.ValidCompoundBeacon)
   {
     function method getNumQueries(globalMax : BucketCount) : BucketCount
+      ensures 0 <= getNumQueries(globalMax) <= globalMax
     {
       if Standard? then
-        std.numberOfBuckets
+        if std.numberOfBuckets <= globalMax then
+          std.numberOfBuckets
+        else
+          globalMax
       else
         cmp.getNumQueries(globalMax)
     }