m

Author: ajewellamz

DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy

@@ -350,7 +350,8 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internald
   )
   datatype GetBucketNumberInput = | GetBucketNumberInput (
     nameonly item: ComAmazonawsDynamodbTypes.AttributeMap ,
-    nameonly numberOfBuckets: BucketCount
+    nameonly numberOfBuckets: BucketCount ,
+    nameonly logicalTableName: string
   )
   datatype GetBucketNumberOutput = | GetBucketNumberOutput (
     nameonly bucketNumber: BucketNumber

DynamoDbEncryption/dafny/DynamoDbEncryption/Model/DynamoDbEncryption.smithy

@@ -65,7 +65,9 @@ structure GetBucketNumberInput {
   @required
   item: AttributeMap,
   @required
-  numberOfBuckets : BucketCount
+  numberOfBuckets : BucketCount,
+  @required
+  logicalTableName: String,
 }
 
 structure GetBucketNumberOutput {

DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DdbMiddlewareConfig.dfy

@@ -44,7 +44,8 @@ module DdbMiddlewareConfig {
       return Success(0);
     }
 
-    var outR := config.search.value.curr().bucketSelector.GetBucketNumber(DDBE.GetBucketNumberInput(item := item, numberOfBuckets := numBuckets));
+    var outR := config.search.value.curr().bucketSelector.GetBucketNumber(DDBE.GetBucketNumberInput(
+      item := item, numberOfBuckets := numBuckets, logicalTableName := config.logicalTableName));
     var out :- outR.MapFailure(e => AwsCryptographyDbEncryptionSdkDynamoDb(e));
     if out.bucketNumber == 0 {
       return Success(0);

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

@@ -584,7 +584,12 @@ public static GetBucketNumberInput GetBucketNumberInput(
       );
     Integer numberOfBuckets;
     numberOfBuckets = (nativeValue.numberOfBuckets());
-    return new GetBucketNumberInput(item, numberOfBuckets);
+    DafnySequence<? extends Character> logicalTableName;
+    logicalTableName =
+      software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence(
+        nativeValue.logicalTableName()
+      );
+    return new GetBucketNumberInput(item, numberOfBuckets, logicalTableName);
   }
 
   public static GetBucketNumberOutput GetBucketNumberOutput(