From 76856694812d3254c24b50bfd17816880aa3df00 Mon Sep 17 00:00:00 2001 From: texastony <5892063+texastony@users.noreply.github.com> Date: Tue, 10 Sep 2024 10:48:00 -0700 Subject: [PATCH 1/3] fix(DDB-Model): DDB Supports 100 actions per Transaction See: https://aws.amazon.com/about-aws/whats-new/2022/09/amazon-dynamodb-supports-100-actions-per-transaction/ Note: We cannot use the latest DDB Model due to https://github.com/smithy-lang/smithy-dafny/issues/105 Thus, I manually bumped the relevant values from 25 to 100. --- ComAmazonawsDynamodb/Model/dynamodb/model.json | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/ComAmazonawsDynamodb/Model/dynamodb/model.json b/ComAmazonawsDynamodb/Model/dynamodb/model.json index 079590e39..7b3d3302a 100644 --- a/ComAmazonawsDynamodb/Model/dynamodb/model.json +++ b/ComAmazonawsDynamodb/Model/dynamodb/model.json @@ -1208,7 +1208,7 @@ "traits": { "smithy.api#length": { "min": 1, - "max": 25 + "max": 100 } } }, @@ -5147,7 +5147,7 @@ "traits": { "smithy.api#length": { "min": 1, - "max": 25 + "max": 100 } } }, @@ -6179,7 +6179,7 @@ "traits": { "smithy.api#length": { "min": 1, - "max": 25 + "max": 100 } } }, @@ -9008,7 +9008,7 @@ "traits": { "smithy.api#length": { "min": 1, - "max": 25 + "max": 100 } } }, @@ -9122,7 +9122,7 @@ "traits": { "smithy.api#length": { "min": 1, - "max": 25 + "max": 100 } } }, @@ -10128,4 +10128,4 @@ } } } -} \ No newline at end of file +} From c1ce7f4c2a6b380b33463f416d0ccb837693ac18 Mon Sep 17 00:00:00 2001 From: texastony <5892063+texastony@users.noreply.github.com> Date: Tue, 10 Sep 2024 10:53:14 -0700 Subject: [PATCH 2/3] fix(DDB-Model): re-polymorph --- .../codegen-patches/dafny/dafny-4.2.0.patch | 49 +++++++++++++++++++ .../codegen-patches/java/dafny-4.2.0.patch | 6 +-- 2 files changed, 52 insertions(+), 3 deletions(-) create mode 100644 ComAmazonawsDynamodb/codegen-patches/dafny/dafny-4.2.0.patch diff --git a/ComAmazonawsDynamodb/codegen-patches/dafny/dafny-4.2.0.patch b/ComAmazonawsDynamodb/codegen-patches/dafny/dafny-4.2.0.patch new file mode 100644 index 000000000..cb387f238 --- /dev/null +++ b/ComAmazonawsDynamodb/codegen-patches/dafny/dafny-4.2.0.patch @@ -0,0 +1,49 @@ +diff --git b/ComAmazonawsDynamodb/Model/ComAmazonawsDynamodbTypes.dfy a/ComAmazonawsDynamodb/Model/ComAmazonawsDynamodbTypes.dfy +index 95fbec3f..16030b6c 100644 +--- b/ComAmazonawsDynamodb/Model/ComAmazonawsDynamodbTypes.dfy ++++ a/ComAmazonawsDynamodb/Model/ComAmazonawsDynamodbTypes.dfy +@@ -237,7 +237,7 @@ module {:extern "software.amazon.cryptography.services.dynamodb.internaldafny.ty + ) + type CancellationReasonList = x: seq | IsValid_CancellationReasonList(x) witness * + predicate method IsValid_CancellationReasonList(x: seq) { +- ( 1 <= |x| <= 100 ) ++ ( 1 <= |x| <= 25 ) + } + datatype Capacity = | Capacity ( + nameonly ReadCapacityUnits: Option := Option.None , +@@ -1781,7 +1781,7 @@ module {:extern "software.amazon.cryptography.services.dynamodb.internaldafny.ty + ) + type ItemResponseList = x: seq | IsValid_ItemResponseList(x) witness * + predicate method IsValid_ItemResponseList(x: seq) { +- ( 1 <= |x| <= 100 ) ++ ( 1 <= |x| <= 25 ) + } + type Key = map + type KeyConditions = map +@@ -1955,7 +1955,7 @@ module {:extern "software.amazon.cryptography.services.dynamodb.internaldafny.ty + ) + type ParameterizedStatements = x: seq | IsValid_ParameterizedStatements(x) witness * + predicate method IsValid_ParameterizedStatements(x: seq) { +- ( 1 <= |x| <= 100 ) ++ ( 1 <= |x| <= 25 ) + } + type PartiQLBatchRequest = x: seq | IsValid_PartiQLBatchRequest(x) witness * + predicate method IsValid_PartiQLBatchRequest(x: seq) { +@@ -2474,7 +2474,7 @@ module {:extern "software.amazon.cryptography.services.dynamodb.internaldafny.ty + ) + type TransactGetItemList = x: seq | IsValid_TransactGetItemList(x) witness * + predicate method IsValid_TransactGetItemList(x: seq) { +- ( 1 <= |x| <= 100 ) ++ ( 1 <= |x| <= 25 ) + } + datatype TransactGetItemsInput = | TransactGetItemsInput ( + nameonly TransactItems: TransactGetItemList , +@@ -2492,7 +2492,7 @@ module {:extern "software.amazon.cryptography.services.dynamodb.internaldafny.ty + ) + type TransactWriteItemList = x: seq | IsValid_TransactWriteItemList(x) witness * + predicate method IsValid_TransactWriteItemList(x: seq) { +- ( 1 <= |x| <= 100 ) ++ ( 1 <= |x| <= 25 ) + } + datatype TransactWriteItemsInput = | TransactWriteItemsInput ( + nameonly TransactItems: TransactWriteItemList , diff --git a/ComAmazonawsDynamodb/codegen-patches/java/dafny-4.2.0.patch b/ComAmazonawsDynamodb/codegen-patches/java/dafny-4.2.0.patch index 7ed7a98c4..99079e516 100644 --- a/ComAmazonawsDynamodb/codegen-patches/java/dafny-4.2.0.patch +++ b/ComAmazonawsDynamodb/codegen-patches/java/dafny-4.2.0.patch @@ -1,7 +1,7 @@ -diff --git a/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToNative.java b/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToNative.java +diff --git b/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToNative.java a/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToNative.java index c30e7cdf..3964b7cb 100644 ---- a/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToNative.java -+++ b/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToNative.java +--- b/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToNative.java ++++ a/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToNative.java @@ -8040,6 +8040,126 @@ public class ToNative { return builder.build(); } From 854d7acc273b7344c55dac71b34601133f083308 Mon Sep 17 00:00:00 2001 From: texastony <5892063+texastony@users.noreply.github.com> Date: Tue, 10 Sep 2024 11:00:40 -0700 Subject: [PATCH 3/3] fix(DDB-Model): re-polymorph --- .../Model/ComAmazonawsDynamodbTypes.dfy | 10 ++-- .../codegen-patches/dafny/dafny-4.2.0.patch | 49 ------------------- 2 files changed, 5 insertions(+), 54 deletions(-) delete mode 100644 ComAmazonawsDynamodb/codegen-patches/dafny/dafny-4.2.0.patch diff --git a/ComAmazonawsDynamodb/Model/ComAmazonawsDynamodbTypes.dfy b/ComAmazonawsDynamodb/Model/ComAmazonawsDynamodbTypes.dfy index 16030b6ce..95fbec3f3 100644 --- a/ComAmazonawsDynamodb/Model/ComAmazonawsDynamodbTypes.dfy +++ b/ComAmazonawsDynamodb/Model/ComAmazonawsDynamodbTypes.dfy @@ -237,7 +237,7 @@ module {:extern "software.amazon.cryptography.services.dynamodb.internaldafny.ty ) type CancellationReasonList = x: seq | IsValid_CancellationReasonList(x) witness * predicate method IsValid_CancellationReasonList(x: seq) { - ( 1 <= |x| <= 25 ) + ( 1 <= |x| <= 100 ) } datatype Capacity = | Capacity ( nameonly ReadCapacityUnits: Option := Option.None , @@ -1781,7 +1781,7 @@ module {:extern "software.amazon.cryptography.services.dynamodb.internaldafny.ty ) type ItemResponseList = x: seq | IsValid_ItemResponseList(x) witness * predicate method IsValid_ItemResponseList(x: seq) { - ( 1 <= |x| <= 25 ) + ( 1 <= |x| <= 100 ) } type Key = map type KeyConditions = map @@ -1955,7 +1955,7 @@ module {:extern "software.amazon.cryptography.services.dynamodb.internaldafny.ty ) type ParameterizedStatements = x: seq | IsValid_ParameterizedStatements(x) witness * predicate method IsValid_ParameterizedStatements(x: seq) { - ( 1 <= |x| <= 25 ) + ( 1 <= |x| <= 100 ) } type PartiQLBatchRequest = x: seq | IsValid_PartiQLBatchRequest(x) witness * predicate method IsValid_PartiQLBatchRequest(x: seq) { @@ -2474,7 +2474,7 @@ module {:extern "software.amazon.cryptography.services.dynamodb.internaldafny.ty ) type TransactGetItemList = x: seq | IsValid_TransactGetItemList(x) witness * predicate method IsValid_TransactGetItemList(x: seq) { - ( 1 <= |x| <= 25 ) + ( 1 <= |x| <= 100 ) } datatype TransactGetItemsInput = | TransactGetItemsInput ( nameonly TransactItems: TransactGetItemList , @@ -2492,7 +2492,7 @@ module {:extern "software.amazon.cryptography.services.dynamodb.internaldafny.ty ) type TransactWriteItemList = x: seq | IsValid_TransactWriteItemList(x) witness * predicate method IsValid_TransactWriteItemList(x: seq) { - ( 1 <= |x| <= 25 ) + ( 1 <= |x| <= 100 ) } datatype TransactWriteItemsInput = | TransactWriteItemsInput ( nameonly TransactItems: TransactWriteItemList , diff --git a/ComAmazonawsDynamodb/codegen-patches/dafny/dafny-4.2.0.patch b/ComAmazonawsDynamodb/codegen-patches/dafny/dafny-4.2.0.patch deleted file mode 100644 index cb387f238..000000000 --- a/ComAmazonawsDynamodb/codegen-patches/dafny/dafny-4.2.0.patch +++ /dev/null @@ -1,49 +0,0 @@ -diff --git b/ComAmazonawsDynamodb/Model/ComAmazonawsDynamodbTypes.dfy a/ComAmazonawsDynamodb/Model/ComAmazonawsDynamodbTypes.dfy -index 95fbec3f..16030b6c 100644 ---- b/ComAmazonawsDynamodb/Model/ComAmazonawsDynamodbTypes.dfy -+++ a/ComAmazonawsDynamodb/Model/ComAmazonawsDynamodbTypes.dfy -@@ -237,7 +237,7 @@ module {:extern "software.amazon.cryptography.services.dynamodb.internaldafny.ty - ) - type CancellationReasonList = x: seq | IsValid_CancellationReasonList(x) witness * - predicate method IsValid_CancellationReasonList(x: seq) { -- ( 1 <= |x| <= 100 ) -+ ( 1 <= |x| <= 25 ) - } - datatype Capacity = | Capacity ( - nameonly ReadCapacityUnits: Option := Option.None , -@@ -1781,7 +1781,7 @@ module {:extern "software.amazon.cryptography.services.dynamodb.internaldafny.ty - ) - type ItemResponseList = x: seq | IsValid_ItemResponseList(x) witness * - predicate method IsValid_ItemResponseList(x: seq) { -- ( 1 <= |x| <= 100 ) -+ ( 1 <= |x| <= 25 ) - } - type Key = map - type KeyConditions = map -@@ -1955,7 +1955,7 @@ module {:extern "software.amazon.cryptography.services.dynamodb.internaldafny.ty - ) - type ParameterizedStatements = x: seq | IsValid_ParameterizedStatements(x) witness * - predicate method IsValid_ParameterizedStatements(x: seq) { -- ( 1 <= |x| <= 100 ) -+ ( 1 <= |x| <= 25 ) - } - type PartiQLBatchRequest = x: seq | IsValid_PartiQLBatchRequest(x) witness * - predicate method IsValid_PartiQLBatchRequest(x: seq) { -@@ -2474,7 +2474,7 @@ module {:extern "software.amazon.cryptography.services.dynamodb.internaldafny.ty - ) - type TransactGetItemList = x: seq | IsValid_TransactGetItemList(x) witness * - predicate method IsValid_TransactGetItemList(x: seq) { -- ( 1 <= |x| <= 100 ) -+ ( 1 <= |x| <= 25 ) - } - datatype TransactGetItemsInput = | TransactGetItemsInput ( - nameonly TransactItems: TransactGetItemList , -@@ -2492,7 +2492,7 @@ module {:extern "software.amazon.cryptography.services.dynamodb.internaldafny.ty - ) - type TransactWriteItemList = x: seq | IsValid_TransactWriteItemList(x) witness * - predicate method IsValid_TransactWriteItemList(x: seq) { -- ( 1 <= |x| <= 100 ) -+ ( 1 <= |x| <= 25 ) - } - datatype TransactWriteItemsInput = | TransactWriteItemsInput ( - nameonly TransactItems: TransactWriteItemList ,