Merge pull request #917 from aws/DDBv2_Upgrade

feat: DDB v2 upgrade
aws · Nov 1, 2024 · f01b7a6 · f01b7a6
2 parents 2926609 + 0b2702f
commit f01b7a6
Show file tree

Hide file tree

Showing 22 changed files with 8,940 additions and 2,266 deletions.
diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/CreateKeyStoreTable.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/CreateKeyStoreTable.dfy
@@ -46,6 +46,7 @@ module CreateKeyStoreTable {
     requires DDB.IsValid_TableName(tableName)
     modifies ddbClient.Modifies
     ensures ddbClient.ValidState()
+    ensures res.Success? ==> DDB.IsValid_TableArn(res.Extract())
 
     //= aws-encryption-sdk-specification/framework/branch-key-store.md#createkeystore
     //= type=implication
@@ -86,6 +87,7 @@ module CreateKeyStoreTable {
              && Seq.Last(ddbClient.History.CreateTable).output.Success?
              && Seq.Last(ddbClient.History.CreateTable).output.value.TableDescription.Some?
              && keyStoreHasExpectedConstruction?(Seq.Last(ddbClient.History.CreateTable).output.value.TableDescription.value)
+             && DDB.IsValid_TableArn(Seq.Last(ddbClient.History.CreateTable).output.value.TableDescription.value.TableArn.value)
              ==>
                && res.Success?
                && res.value == Seq.Last(ddbClient.History.CreateTable).output.value.TableDescription.value.TableArn.value
@@ -154,7 +156,8 @@ module CreateKeyStoreTable {
         } else {
           :- Need(
             && maybeCreateTableResponse.value.TableDescription.Some?
-            && keyStoreHasExpectedConstruction?(maybeCreateTableResponse.value.TableDescription.value),
+            && keyStoreHasExpectedConstruction?(maybeCreateTableResponse.value.TableDescription.value)
+            && DDB.IsValid_TableArn(maybeCreateTableResponse.value.TableDescription.value.TableArn.value),
             E("Configured table name does not conform to expected Key Store construction.")
           );
           //= aws-encryption-sdk-specification/framework/branch-key-store.md#createkeystore
@@ -173,7 +176,8 @@ module CreateKeyStoreTable {
       //# this operation MUST yield an error.
       :- Need(
         && maybeDescribeTableResponse.value.Table.Some?
-        && keyStoreHasExpectedConstruction?(maybeDescribeTableResponse.value.Table.value),
+        && keyStoreHasExpectedConstruction?(maybeDescribeTableResponse.value.Table.value)
+        && DDB.IsValid_TableArn(maybeDescribeTableResponse.value.Table.value.TableArn.value),
         E("Configured table name does not conform to expected Key Store construction.")
       );
       res := Success(maybeDescribeTableResponse.value.Table.value.TableArn.value);

diff --git a/...in/smithy-generated/software/amazon/cryptography/keystore/model/CreateKeyStoreOutput.java b/...in/smithy-generated/software/amazon/cryptography/keystore/model/CreateKeyStoreOutput.java
@@ -73,6 +73,16 @@ public CreateKeyStoreOutput build() {
           "Missing value for required field `tableArn`"
         );
       }
+      if (Objects.nonNull(this.tableArn()) && this.tableArn().length() < 1) {
+        throw new IllegalArgumentException(
+          "The size of `tableArn` must be greater than or equal to 1"
+        );
+      }
+      if (Objects.nonNull(this.tableArn()) && this.tableArn().length() > 1024) {
+        throw new IllegalArgumentException(
+          "The size of `tableArn` must be less than or equal to 1024"
+        );
+      }
       return new CreateKeyStoreOutput(this);
     }
   }

diff --git a/.../aws_cryptographic_material_providers/smithygenerated/aws_cryptography_keystore/models.py b/.../aws_cryptographic_material_providers/smithygenerated/aws_cryptography_keystore/models.py
@@ -292,6 +292,12 @@ def __init__(
         :param table_arn: The ARN of the DynamoDB table that backs this
             Key Store.
         """
+        if (table_arn is not None) and (len(table_arn) < 1):
+            raise ValueError("The size of table_arn must be greater than or equal to 1")
+
+        if (table_arn is not None) and (len(table_arn) > 1024):
+            raise ValueError("The size of table_arn must be less than or equal to 1024")
+
         self.table_arn = table_arn
 
     def as_dict(self) -> Dict[str, Any]:

diff --git a/AwsCryptographyPrimitives/runtimes/net/Extern/RSAEncryption.cs b/AwsCryptographyPrimitives/runtimes/net/Extern/RSAEncryption.cs
@@ -99,7 +99,6 @@ private static IAsymmetricBlockCipher GetEngineForPadding(_IRSAPaddingMode paddi
         // key and returns the AsymmetricKeyParameter for that public key, encoded using UTF-8
         private static AsymmetricKeyParameter GetPublicKeyFromByteSeq(ibyteseq key)
         {
-            AsymmetricKeyParameter keyParam;
             using (var stringReader = new StringReader(Encoding.UTF8.GetString(key.CloneAsArray())))
             {
                 return (AsymmetricKeyParameter)new PemReader(stringReader).ReadObject();

diff --git a/.../runtimes/python/src/aws_cryptography_primitives/internaldafny/generated/dafny_src-py.dtr b/.../runtimes/python/src/aws_cryptography_primitives/internaldafny/generated/dafny_src-py.dtr
@@ -1,5 +1,5 @@
 file_format_version = "1.0"
-dafny_version = "4.8.0.0"
+dafny_version = "4.8.1.0"
 [options_by_module.AwsCryptographyPrimitivesTypes]
 legacy-module-names = false
 python-module-name = "aws_cryptography_primitives.internaldafny.generated"

diff --git a/ComAmazonawsDynamodb/Model/ComAmazonawsDynamodbTypes.dfy b/ComAmazonawsDynamodb/Model/ComAmazonawsDynamodbTypes.dfy
diff --git a/ComAmazonawsDynamodb/Model/dynamodb/model.json b/ComAmazonawsDynamodb/Model/dynamodb/model.json
diff --git a/ComAmazonawsDynamodb/codegen-patches/dotnet/dafny-4.8.0.patch b/ComAmazonawsDynamodb/codegen-patches/dotnet/dafny-4.8.0.patch
@@ -1,8 +1,25 @@
-diff --git a/ComAmazonawsDynamodb/runtimes/net/Generated/TypeConversion.cs b/ComAmazonawsDynamodb/runtimes/net/Generated/TypeConversion.cs
-index e35ad3d2..9f375b21 100644
---- a/ComAmazonawsDynamodb/runtimes/net/Generated/TypeConversion.cs
+unchanged:
+--- b/ComAmazonawsDynamodb/runtimes/net/Generated/TypeConversion.cs
 +++ b/ComAmazonawsDynamodb/runtimes/net/Generated/TypeConversion.cs
-@@ -5848,7 +5848,7 @@ namespace Com.Amazonaws.Dynamodb
+@@ -213,11 +213,12 @@
+         }
+         public static Amazon.DynamoDBv2.Model.ConditionalCheckFailedException FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S31_ConditionalCheckFailedException(software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_ConditionalCheckFailedException value)
+         {
+-            return new Amazon.DynamoDBv2.Model.ConditionalCheckFailedException(
+-            FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S31_ConditionalCheckFailedException__M7_message(value._message)
+-            ,
+-            FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S31_ConditionalCheckFailedException__M4_Item(value._Item)
+-            );
++            var conditionalCheckFailedException = new Amazon.DynamoDBv2.Model.ConditionalCheckFailedException(
++                FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S31_ConditionalCheckFailedException__M7_message(
++                    value._message));
++            conditionalCheckFailedException.Item =
++                FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S31_ConditionalCheckFailedException__M4_Item(value._Item);
++            return conditionalCheckFailedException;
+         }
+         public static software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_ConditionalCheckFailedException ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S31_ConditionalCheckFailedException(Amazon.DynamoDBv2.Model.ConditionalCheckFailedException value)
+         {
+@@ -5848,7 +5849,7 @@
          public static System.DateTime FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S18_LastUpdateDateTime(Dafny.ISequence<char> value)
          {
              string timestampString = new string(value.Elements);
@@ -11,7 +28,7 @@ index e35ad3d2..9f375b21 100644
 
          }
          public static Dafny.ISequence<char> ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S18_LastUpdateDateTime(System.DateTime value)
-@@ -6126,7 +6126,7 @@ namespace Com.Amazonaws.Dynamodb
+@@ -6126,7 +6127,7 @@
          public static System.DateTime FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S10_ExportTime(Dafny.ISequence<char> value)
          {
              string timestampString = new string(value.Elements);
@@ -20,7 +37,7 @@ index e35ad3d2..9f375b21 100644
 
          }
          public static Dafny.ISequence<char> ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S10_ExportTime(System.DateTime value)
-@@ -6252,7 +6252,7 @@ namespace Com.Amazonaws.Dynamodb
+@@ -6252,7 +6253,7 @@
          public static System.DateTime FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S19_TimeRangeLowerBound(Dafny.ISequence<char> value)
          {
              string timestampString = new string(value.Elements);
@@ -29,7 +46,7 @@ index e35ad3d2..9f375b21 100644
 
          }
          public static Dafny.ISequence<char> ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S19_TimeRangeLowerBound(System.DateTime value)
-@@ -6264,7 +6264,7 @@ namespace Com.Amazonaws.Dynamodb
+@@ -6264,7 +6265,7 @@
          public static System.DateTime FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S19_TimeRangeUpperBound(Dafny.ISequence<char> value)
          {
              string timestampString = new string(value.Elements);
@@ -38,7 +55,7 @@ index e35ad3d2..9f375b21 100644
 
          }
          public static Dafny.ISequence<char> ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S19_TimeRangeUpperBound(System.DateTime value)
-@@ -6450,7 +6450,7 @@ namespace Com.Amazonaws.Dynamodb
+@@ -6450,7 +6451,7 @@
          public static System.DateTime FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S4_Date(Dafny.ISequence<char> value)
          {
              string timestampString = new string(value.Elements);
@@ -47,7 +64,7 @@ index e35ad3d2..9f375b21 100644
 
          }
          public static Dafny.ISequence<char> ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S4_Date(System.DateTime value)
-@@ -8187,7 +8187,7 @@ namespace Com.Amazonaws.Dynamodb
+@@ -8187,7 +8188,7 @@
          public static System.DateTime FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S22_BackupCreationDateTime(Dafny.ISequence<char> value)
          {
              string timestampString = new string(value.Elements);
@@ -56,7 +73,7 @@ index e35ad3d2..9f375b21 100644
 
          }
          public static Dafny.ISequence<char> ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S22_BackupCreationDateTime(System.DateTime value)
-@@ -8595,7 +8595,7 @@ namespace Com.Amazonaws.Dynamodb
+@@ -8595,7 +8596,7 @@
          public static System.DateTime FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S15_ExportStartTime(Dafny.ISequence<char> value)
          {
              string timestampString = new string(value.Elements);
@@ -65,7 +82,7 @@ index e35ad3d2..9f375b21 100644
 
          }
          public static Dafny.ISequence<char> ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S15_ExportStartTime(System.DateTime value)
-@@ -8607,7 +8607,7 @@ namespace Com.Amazonaws.Dynamodb
+@@ -8607,7 +8608,7 @@
          public static System.DateTime FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S13_ExportEndTime(Dafny.ISequence<char> value)
          {
              string timestampString = new string(value.Elements);
@@ -74,7 +91,7 @@ index e35ad3d2..9f375b21 100644
 
          }
          public static Dafny.ISequence<char> ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S13_ExportEndTime(System.DateTime value)
-@@ -8700,7 +8700,7 @@ namespace Com.Amazonaws.Dynamodb
+@@ -8700,7 +8701,7 @@
          public static System.DateTime FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S15_ImportStartTime(Dafny.ISequence<char> value)
          {
              string timestampString = new string(value.Elements);
@@ -83,7 +100,7 @@ index e35ad3d2..9f375b21 100644
 
          }
          public static Dafny.ISequence<char> ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S15_ImportStartTime(System.DateTime value)
-@@ -8712,7 +8712,7 @@ namespace Com.Amazonaws.Dynamodb
+@@ -8712,7 +8713,7 @@
          public static System.DateTime FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S13_ImportEndTime(Dafny.ISequence<char> value)
          {
              string timestampString = new string(value.Elements);
@@ -92,7 +109,7 @@ index e35ad3d2..9f375b21 100644
 
          }
          public static Dafny.ISequence<char> ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S13_ImportEndTime(System.DateTime value)
-@@ -10522,7 +10522,7 @@ namespace Com.Amazonaws.Dynamodb
+@@ -10522,7 +10523,7 @@
          public static System.DateTime FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S21_TableCreationDateTime(Dafny.ISequence<char> value)
          {
              string timestampString = new string(value.Elements);
@@ -101,7 +118,7 @@ index e35ad3d2..9f375b21 100644
 
          }
          public static Dafny.ISequence<char> ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S21_TableCreationDateTime(System.DateTime value)
-@@ -10980,7 +10980,13 @@ namespace Com.Amazonaws.Dynamodb
+@@ -10980,7 +10981,13 @@
          }
          public static Wrappers_Compile._IOption<Dafny.ISequence<Dafny.ISequence<char>>> ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S10_Projection__M16_NonKeyAttributes(System.Collections.Generic.List<string> value)
          {
@@ -116,3 +133,24 @@ index e35ad3d2..9f375b21 100644
          }
          public static string FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S30_LocalSecondaryIndexDescription__M9_IndexName(Wrappers_Compile._IOption<Dafny.ISequence<char>> value)
          {
+diff -u b/ComAmazonawsDynamodb/runtimes/net/Generated/TypeConversion.cs b/ComAmazonawsDynamodb/runtimes/net/Generated/TypeConversion.cs
+--- b/ComAmazonawsDynamodb/runtimes/net/Generated/TypeConversion.cs
++++ b/ComAmazonawsDynamodb/runtimes/net/Generated/TypeConversion.cs
+@@ -9267,7 +9267,7 @@
+         public static System.DateTime FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_ExportFromTime(Dafny.ISequence<char> value)
+         {
+             string timestampString = new string(value.Elements);
+-            return System.DateTime.ParseExact(timestampString, new[] { ISO8601DateFormat, ISO8601DateFormatNoMS }, System.Globalization.CultureInfo.InvariantCulture);
++            return System.DateTime.ParseExact(timestampString, new[] { ISO8601DateFormat, ISO8601DateFormatNoMS }.ToString(), System.Globalization.CultureInfo.InvariantCulture);
+
+         }
+         public static Dafny.ISequence<char> ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_ExportFromTime(System.DateTime value)
+@@ -9279,7 +9279,7 @@
+         public static System.DateTime FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S12_ExportToTime(Dafny.ISequence<char> value)
+         {
+             string timestampString = new string(value.Elements);
+-            return System.DateTime.ParseExact(timestampString, new[] { ISO8601DateFormat, ISO8601DateFormatNoMS }, System.Globalization.CultureInfo.InvariantCulture);
++            return System.DateTime.ParseExact(timestampString, new[] { ISO8601DateFormat, ISO8601DateFormatNoMS }.ToString(), System.Globalization.CultureInfo.InvariantCulture);
+
+         }
+         public static Dafny.ISequence<char> ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S12_ExportToTime(System.DateTime value)