m

Author: ajewellamz

TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy

@@ -500,8 +500,8 @@ module {:options "-functionSyntax:4"} JsonConfig {
     var compoundBeacons : seq<Types.CompoundBeacon> := [];
     var virtualFields : seq<Types.VirtualField> := [];
     var keySource : Option<Types.BeaconKeySource> := None;
-    var maximumNumberOfBuckets: Option<Types.BucketCount> := None;
-    var defaultNumberOfBuckets: Option<Types.BucketCount> := None;
+    var maximumNumberOfPartitions: Option<Types.PartitionCount> := None;
+    var defaultNumberOfPartitions: Option<Types.PartitionCount> := None;
 
     for i := 0 to |data.obj| {
       var obj := data.obj[i];
@@ -510,20 +510,20 @@ module {:options "-functionSyntax:4"} JsonConfig {
         case "standardBeacons" => standardBeacons :- GetStandardBeacons(obj.1);
         case "compoundBeacons" => compoundBeacons :- GetCompoundBeacons(obj.1);
         case "virtualFields" => virtualFields :- GetVirtualFields(obj.1);
-        case "maximumNumberOfBuckets" =>
-          :- Need(obj.1.Number?, "maximumNumberOfBuckets must be of type Number.");
+        case "maximumNumberOfPartitions" =>
+          :- Need(obj.1.Number?, "maximumNumberOfPartitions must be of type Number.");
           var num :- DecimalToNat(obj.1.num);
           expect 0 < num < INT32_MAX_LIMIT;
           var num2 := num as int32;
-          expect Types.IsValid_BucketCount(num2);
-          maximumNumberOfBuckets := Some(num as Types.BucketCount);
-        case "defaultNumberOfBuckets" =>
-          :- Need(obj.1.Number?, "defaultNumberOfBuckets must be of type Number.");
+          expect Types.IsValid_PartitionCount(num2);
+          maximumNumberOfPartitions := Some(num as Types.PartitionCount);
+        case "defaultNumberOfPartitions" =>
+          :- Need(obj.1.Number?, "defaultNumberOfPartitions must be of type Number.");
           var num :- DecimalToNat(obj.1.num);
           expect 0 < num < INT32_MAX_LIMIT;
           var num2 := num as int32;
-          expect Types.IsValid_BucketCount(num2);
-          defaultNumberOfBuckets := Some(num as Types.BucketCount);
+          expect Types.IsValid_PartitionCount(num2);
+          defaultNumberOfPartitions := Some(num as Types.PartitionCount);
         case _ => return Failure("Unexpected part of a beacon version : '" + obj.0 + "'");
       }
     }
@@ -547,8 +547,8 @@ module {:options "-functionSyntax:4"} JsonConfig {
                      virtualFields := OptSeq(virtualFields),
                      encryptedParts := None,
                      signedParts := None,
-                     maximumNumberOfBuckets := maximumNumberOfBuckets,
-                     defaultNumberOfBuckets := defaultNumberOfBuckets
+                     maximumNumberOfPartitions := maximumNumberOfPartitions,
+                     defaultNumberOfPartitions := defaultNumberOfPartitions
                    )
       );
   }
@@ -590,7 +590,7 @@ module {:options "-functionSyntax:4"} JsonConfig {
 
     var src := SI.KeySource(client, store, SI.SingleLoc("foo"), cache, 100 as uint32, partitionIdBytes, logicalKeyStoreNameBytes);
 
-    var sel := new SearchConfigToInfo.DefaultBucketSelector();
+    var sel := new SearchConfigToInfo.DefaultPartitionSelector();
     var bv :- expect SI.MakeBeaconVersion(1, src, map[], map[], map[], sel, 1);
     return Success(bv);
   }
@@ -1116,7 +1116,7 @@ module {:options "-functionSyntax:4"} JsonConfig {
     var name : string := "";
     var length : int := -1;
     var loc : Option<Types.TerminalLocation> := None;
-    var numberOfBuckets: Option<Types.BucketCount> := None;
+    var numberOfPartitions: Option<Types.PartitionCount> := None;
 
     for i := 0 to |data.obj| {
       var obj := data.obj[i];
@@ -1131,19 +1131,19 @@ module {:options "-functionSyntax:4"} JsonConfig {
           :- Need(obj.1.String?, "Standard Beacon Location must be a string");
           :- Need(0 < |obj.1.str|, "Standard Beacon Location must not be an empty string.");
           loc := Some(obj.1.str);
-        case "numberOfBuckets" =>
-          :- Need(obj.1.Number?, "numberOfBuckets must be of type Number.");
+        case "numberOfPartitions" =>
+          :- Need(obj.1.Number?, "numberOfPartitions must be of type Number.");
           var num :- DecimalToNat(obj.1.num);
           expect 0 < num < INT32_MAX_LIMIT;
           var num2 := num as int32;
-          expect Types.IsValid_BucketCount(num2);
-          numberOfBuckets := Some(num as Types.BucketCount);
+          expect Types.IsValid_PartitionCount(num2);
+          numberOfPartitions := Some(num as Types.PartitionCount);
         case _ => return Failure("Unexpected part of a standard beacon : '" + data.obj[i].0 + "'");
       }
     }
     :- Need(0 < |name|, "Each Standard Beacon needs a name.");
     :- Need(0 < length < 100 && Types.IsValid_BeaconBitLength(length as int32), "Each Standard Beacon needs a length between 1 and 63.");
-    return Success(Types.StandardBeacon(name := name, length := length as Types.BeaconBitLength, loc := loc, style := None, numberOfBuckets := numberOfBuckets));
+    return Success(Types.StandardBeacon(name := name, length := length as Types.BeaconBitLength, loc := loc, style := None, numberOfPartitions := numberOfPartitions));
   }
 
   method GetGSIs(data : JSON) returns (output : Result<seq<DDB.GlobalSecondaryIndex> , string>)