m

Author: ajewellamz

DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy

@@ -402,7 +402,8 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internald
     nameonly name: string ,
     nameonly length: BeaconBitLength ,
     nameonly loc: Option<TerminalLocation> := Option.None ,
-    nameonly style: Option<BeaconStyle> := Option.None
+    nameonly style: Option<BeaconStyle> := Option.None ,
+    nameonly numberOfBuckets: Option<BucketCount> := Option.None
   )
   type StandardBeaconList = x: seq<StandardBeacon> | IsValid_StandardBeaconList(x) witness *
   predicate method IsValid_StandardBeaconList(x: seq<StandardBeacon>) {

DynamoDbEncryption/dafny/DynamoDbEncryption/Model/DynamoDbEncryption.smithy

@@ -672,6 +672,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
 }
 
 //= specification/searchable-encryption/beacons.md#compound-beacon-initialization

DynamoDbEncryption/runtimes/go/ImplementationFromDafny-go/awscryptographydbencryptionsdkdynamodbsmithygenerated/to_dafny.go

@@ -834,7 +834,15 @@ public static StandardBeacon StandardBeacon(
           ToDafny.BeaconStyle(nativeValue.style())
         )
         : Option.create_None(BeaconStyle._typeDescriptor());
-    return new StandardBeacon(name, length, loc, style);
+    Option<Integer> numberOfBuckets;
+    numberOfBuckets =
+      Objects.nonNull(nativeValue.numberOfBuckets())
+        ? Option.create_Some(
+          TypeDescriptor.INT,
+          (nativeValue.numberOfBuckets())
+        )
+        : Option.create_None(TypeDescriptor.INT);
+    return new StandardBeacon(name, length, loc, style, numberOfBuckets);
   }
 
   public static Upper Upper(

DynamoDbEncryption/runtimes/go/ImplementationFromDafny-go/awscryptographydbencryptionsdkdynamodbsmithygenerated/to_native.go

@@ -725,6 +725,11 @@ public static StandardBeacon StandardBeacon(
         ToNative.BeaconStyle(dafnyValue.dtor_style().dtor_value())
       );
     }
+    if (dafnyValue.dtor_numberOfBuckets().is_Some()) {
+      nativeBuilder.numberOfBuckets(
+        (dafnyValue.dtor_numberOfBuckets().dtor_value())
+      );
+    }
     return nativeBuilder.build();
   }