Skip to content

Commit f01b7a6

Browse files
Merge pull request #917 from aws/DDBv2_Upgrade
feat: DDB v2 upgrade
2 parents 2926609 + 0b2702f commit f01b7a6

File tree

22 files changed

+8940
-2266
lines changed

22 files changed

+8940
-2266
lines changed

AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/CreateKeyStoreTable.dfy

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -46,6 +46,7 @@ module CreateKeyStoreTable {
4646
requires DDB.IsValid_TableName(tableName)
4747
modifies ddbClient.Modifies
4848
ensures ddbClient.ValidState()
49+
ensures res.Success? ==> DDB.IsValid_TableArn(res.Extract())
4950

5051
//= aws-encryption-sdk-specification/framework/branch-key-store.md#createkeystore
5152
//= type=implication
@@ -86,6 +87,7 @@ module CreateKeyStoreTable {
8687
&& Seq.Last(ddbClient.History.CreateTable).output.Success?
8788
&& Seq.Last(ddbClient.History.CreateTable).output.value.TableDescription.Some?
8889
&& keyStoreHasExpectedConstruction?(Seq.Last(ddbClient.History.CreateTable).output.value.TableDescription.value)
90+
&& DDB.IsValid_TableArn(Seq.Last(ddbClient.History.CreateTable).output.value.TableDescription.value.TableArn.value)
8991
==>
9092
&& res.Success?
9193
&& res.value == Seq.Last(ddbClient.History.CreateTable).output.value.TableDescription.value.TableArn.value
@@ -154,7 +156,8 @@ module CreateKeyStoreTable {
154156
} else {
155157
:- Need(
156158
&& maybeCreateTableResponse.value.TableDescription.Some?
157-
&& keyStoreHasExpectedConstruction?(maybeCreateTableResponse.value.TableDescription.value),
159+
&& keyStoreHasExpectedConstruction?(maybeCreateTableResponse.value.TableDescription.value)
160+
&& DDB.IsValid_TableArn(maybeCreateTableResponse.value.TableDescription.value.TableArn.value),
158161
E("Configured table name does not conform to expected Key Store construction.")
159162
);
160163
//= aws-encryption-sdk-specification/framework/branch-key-store.md#createkeystore
@@ -173,7 +176,8 @@ module CreateKeyStoreTable {
173176
//# this operation MUST yield an error.
174177
:- Need(
175178
&& maybeDescribeTableResponse.value.Table.Some?
176-
&& keyStoreHasExpectedConstruction?(maybeDescribeTableResponse.value.Table.value),
179+
&& keyStoreHasExpectedConstruction?(maybeDescribeTableResponse.value.Table.value)
180+
&& DDB.IsValid_TableArn(maybeDescribeTableResponse.value.Table.value.TableArn.value),
177181
E("Configured table name does not conform to expected Key Store construction.")
178182
);
179183
res := Success(maybeDescribeTableResponse.value.Table.value.TableArn.value);

AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/keystore/model/CreateKeyStoreOutput.java

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -73,6 +73,16 @@ public CreateKeyStoreOutput build() {
7373
"Missing value for required field `tableArn`"
7474
);
7575
}
76+
if (Objects.nonNull(this.tableArn()) && this.tableArn().length() < 1) {
77+
throw new IllegalArgumentException(
78+
"The size of `tableArn` must be greater than or equal to 1"
79+
);
80+
}
81+
if (Objects.nonNull(this.tableArn()) && this.tableArn().length() > 1024) {
82+
throw new IllegalArgumentException(
83+
"The size of `tableArn` must be less than or equal to 1024"
84+
);
85+
}
7686
return new CreateKeyStoreOutput(this);
7787
}
7888
}

AwsCryptographicMaterialProviders/runtimes/python/src/aws_cryptographic_material_providers/smithygenerated/aws_cryptography_keystore/models.py

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -292,6 +292,12 @@ def __init__(
292292
:param table_arn: The ARN of the DynamoDB table that backs this
293293
Key Store.
294294
"""
295+
if (table_arn is not None) and (len(table_arn) < 1):
296+
raise ValueError("The size of table_arn must be greater than or equal to 1")
297+
298+
if (table_arn is not None) and (len(table_arn) > 1024):
299+
raise ValueError("The size of table_arn must be less than or equal to 1024")
300+
295301
self.table_arn = table_arn
296302

297303
def as_dict(self) -> Dict[str, Any]:

AwsCryptographyPrimitives/runtimes/net/Extern/RSAEncryption.cs

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -99,7 +99,6 @@ private static IAsymmetricBlockCipher GetEngineForPadding(_IRSAPaddingMode paddi
9999
// key and returns the AsymmetricKeyParameter for that public key, encoded using UTF-8
100100
private static AsymmetricKeyParameter GetPublicKeyFromByteSeq(ibyteseq key)
101101
{
102-
AsymmetricKeyParameter keyParam;
103102
using (var stringReader = new StringReader(Encoding.UTF8.GetString(key.CloneAsArray())))
104103
{
105104
return (AsymmetricKeyParameter)new PemReader(stringReader).ReadObject();

AwsCryptographyPrimitives/runtimes/python/src/aws_cryptography_primitives/internaldafny/generated/dafny_src-py.dtr

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
file_format_version = "1.0"
2-
dafny_version = "4.8.0.0"
2+
dafny_version = "4.8.1.0"
33
[options_by_module.AwsCryptographyPrimitivesTypes]
44
legacy-module-names = false
55
python-module-name = "aws_cryptography_primitives.internaldafny.generated"

ComAmazonawsDynamodb/Model/ComAmazonawsDynamodbTypes.dfy

Lines changed: 313 additions & 71 deletions
Large diffs are not rendered by default.

ComAmazonawsDynamodb/Model/dynamodb/model.json

Lines changed: 3704 additions & 1149 deletions
Large diffs are not rendered by default.

ComAmazonawsDynamodb/codegen-patches/dotnet/dafny-4.8.0.patch

Lines changed: 53 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,25 @@
1-
diff --git a/ComAmazonawsDynamodb/runtimes/net/Generated/TypeConversion.cs b/ComAmazonawsDynamodb/runtimes/net/Generated/TypeConversion.cs
2-
index e35ad3d2..9f375b21 100644
3-
--- a/ComAmazonawsDynamodb/runtimes/net/Generated/TypeConversion.cs
1+
unchanged:
2+
--- b/ComAmazonawsDynamodb/runtimes/net/Generated/TypeConversion.cs
43
+++ b/ComAmazonawsDynamodb/runtimes/net/Generated/TypeConversion.cs
5-
@@ -5848,7 +5848,7 @@ namespace Com.Amazonaws.Dynamodb
4+
@@ -213,11 +213,12 @@
5+
}
6+
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)
7+
{
8+
- return new Amazon.DynamoDBv2.Model.ConditionalCheckFailedException(
9+
- FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S31_ConditionalCheckFailedException__M7_message(value._message)
10+
- ,
11+
- FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S31_ConditionalCheckFailedException__M4_Item(value._Item)
12+
- );
13+
+ var conditionalCheckFailedException = new Amazon.DynamoDBv2.Model.ConditionalCheckFailedException(
14+
+ FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S31_ConditionalCheckFailedException__M7_message(
15+
+ value._message));
16+
+ conditionalCheckFailedException.Item =
17+
+ FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S31_ConditionalCheckFailedException__M4_Item(value._Item);
18+
+ return conditionalCheckFailedException;
19+
}
20+
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)
21+
{
22+
@@ -5848,7 +5849,7 @@
623
public static System.DateTime FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S18_LastUpdateDateTime(Dafny.ISequence<char> value)
724
{
825
string timestampString = new string(value.Elements);
@@ -11,7 +28,7 @@ index e35ad3d2..9f375b21 100644
1128

1229
}
1330
public static Dafny.ISequence<char> ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S18_LastUpdateDateTime(System.DateTime value)
14-
@@ -6126,7 +6126,7 @@ namespace Com.Amazonaws.Dynamodb
31+
@@ -6126,7 +6127,7 @@
1532
public static System.DateTime FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S10_ExportTime(Dafny.ISequence<char> value)
1633
{
1734
string timestampString = new string(value.Elements);
@@ -20,7 +37,7 @@ index e35ad3d2..9f375b21 100644
2037

2138
}
2239
public static Dafny.ISequence<char> ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S10_ExportTime(System.DateTime value)
23-
@@ -6252,7 +6252,7 @@ namespace Com.Amazonaws.Dynamodb
40+
@@ -6252,7 +6253,7 @@
2441
public static System.DateTime FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S19_TimeRangeLowerBound(Dafny.ISequence<char> value)
2542
{
2643
string timestampString = new string(value.Elements);
@@ -29,7 +46,7 @@ index e35ad3d2..9f375b21 100644
2946

3047
}
3148
public static Dafny.ISequence<char> ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S19_TimeRangeLowerBound(System.DateTime value)
32-
@@ -6264,7 +6264,7 @@ namespace Com.Amazonaws.Dynamodb
49+
@@ -6264,7 +6265,7 @@
3350
public static System.DateTime FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S19_TimeRangeUpperBound(Dafny.ISequence<char> value)
3451
{
3552
string timestampString = new string(value.Elements);
@@ -38,7 +55,7 @@ index e35ad3d2..9f375b21 100644
3855

3956
}
4057
public static Dafny.ISequence<char> ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S19_TimeRangeUpperBound(System.DateTime value)
41-
@@ -6450,7 +6450,7 @@ namespace Com.Amazonaws.Dynamodb
58+
@@ -6450,7 +6451,7 @@
4259
public static System.DateTime FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S4_Date(Dafny.ISequence<char> value)
4360
{
4461
string timestampString = new string(value.Elements);
@@ -47,7 +64,7 @@ index e35ad3d2..9f375b21 100644
4764

4865
}
4966
public static Dafny.ISequence<char> ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S4_Date(System.DateTime value)
50-
@@ -8187,7 +8187,7 @@ namespace Com.Amazonaws.Dynamodb
67+
@@ -8187,7 +8188,7 @@
5168
public static System.DateTime FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S22_BackupCreationDateTime(Dafny.ISequence<char> value)
5269
{
5370
string timestampString = new string(value.Elements);
@@ -56,7 +73,7 @@ index e35ad3d2..9f375b21 100644
5673

5774
}
5875
public static Dafny.ISequence<char> ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S22_BackupCreationDateTime(System.DateTime value)
59-
@@ -8595,7 +8595,7 @@ namespace Com.Amazonaws.Dynamodb
76+
@@ -8595,7 +8596,7 @@
6077
public static System.DateTime FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S15_ExportStartTime(Dafny.ISequence<char> value)
6178
{
6279
string timestampString = new string(value.Elements);
@@ -65,7 +82,7 @@ index e35ad3d2..9f375b21 100644
6582

6683
}
6784
public static Dafny.ISequence<char> ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S15_ExportStartTime(System.DateTime value)
68-
@@ -8607,7 +8607,7 @@ namespace Com.Amazonaws.Dynamodb
85+
@@ -8607,7 +8608,7 @@
6986
public static System.DateTime FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S13_ExportEndTime(Dafny.ISequence<char> value)
7087
{
7188
string timestampString = new string(value.Elements);
@@ -74,7 +91,7 @@ index e35ad3d2..9f375b21 100644
7491

7592
}
7693
public static Dafny.ISequence<char> ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S13_ExportEndTime(System.DateTime value)
77-
@@ -8700,7 +8700,7 @@ namespace Com.Amazonaws.Dynamodb
94+
@@ -8700,7 +8701,7 @@
7895
public static System.DateTime FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S15_ImportStartTime(Dafny.ISequence<char> value)
7996
{
8097
string timestampString = new string(value.Elements);
@@ -83,7 +100,7 @@ index e35ad3d2..9f375b21 100644
83100

84101
}
85102
public static Dafny.ISequence<char> ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S15_ImportStartTime(System.DateTime value)
86-
@@ -8712,7 +8712,7 @@ namespace Com.Amazonaws.Dynamodb
103+
@@ -8712,7 +8713,7 @@
87104
public static System.DateTime FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S13_ImportEndTime(Dafny.ISequence<char> value)
88105
{
89106
string timestampString = new string(value.Elements);
@@ -92,7 +109,7 @@ index e35ad3d2..9f375b21 100644
92109

93110
}
94111
public static Dafny.ISequence<char> ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S13_ImportEndTime(System.DateTime value)
95-
@@ -10522,7 +10522,7 @@ namespace Com.Amazonaws.Dynamodb
112+
@@ -10522,7 +10523,7 @@
96113
public static System.DateTime FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S21_TableCreationDateTime(Dafny.ISequence<char> value)
97114
{
98115
string timestampString = new string(value.Elements);
@@ -101,7 +118,7 @@ index e35ad3d2..9f375b21 100644
101118

102119
}
103120
public static Dafny.ISequence<char> ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S21_TableCreationDateTime(System.DateTime value)
104-
@@ -10980,7 +10980,13 @@ namespace Com.Amazonaws.Dynamodb
121+
@@ -10980,7 +10981,13 @@
105122
}
106123
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)
107124
{
@@ -116,3 +133,24 @@ index e35ad3d2..9f375b21 100644
116133
}
117134
public static string FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S30_LocalSecondaryIndexDescription__M9_IndexName(Wrappers_Compile._IOption<Dafny.ISequence<char>> value)
118135
{
136+
diff -u b/ComAmazonawsDynamodb/runtimes/net/Generated/TypeConversion.cs b/ComAmazonawsDynamodb/runtimes/net/Generated/TypeConversion.cs
137+
--- b/ComAmazonawsDynamodb/runtimes/net/Generated/TypeConversion.cs
138+
+++ b/ComAmazonawsDynamodb/runtimes/net/Generated/TypeConversion.cs
139+
@@ -9267,7 +9267,7 @@
140+
public static System.DateTime FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_ExportFromTime(Dafny.ISequence<char> value)
141+
{
142+
string timestampString = new string(value.Elements);
143+
- return System.DateTime.ParseExact(timestampString, new[] { ISO8601DateFormat, ISO8601DateFormatNoMS }, System.Globalization.CultureInfo.InvariantCulture);
144+
+ return System.DateTime.ParseExact(timestampString, new[] { ISO8601DateFormat, ISO8601DateFormatNoMS }.ToString(), System.Globalization.CultureInfo.InvariantCulture);
145+
146+
}
147+
public static Dafny.ISequence<char> ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_ExportFromTime(System.DateTime value)
148+
@@ -9279,7 +9279,7 @@
149+
public static System.DateTime FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S12_ExportToTime(Dafny.ISequence<char> value)
150+
{
151+
string timestampString = new string(value.Elements);
152+
- return System.DateTime.ParseExact(timestampString, new[] { ISO8601DateFormat, ISO8601DateFormatNoMS }, System.Globalization.CultureInfo.InvariantCulture);
153+
+ return System.DateTime.ParseExact(timestampString, new[] { ISO8601DateFormat, ISO8601DateFormatNoMS }.ToString(), System.Globalization.CultureInfo.InvariantCulture);
154+
155+
}
156+
public static Dafny.ISequence<char> ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S12_ExportToTime(System.DateTime value)

0 commit comments

Comments
 (0)