From fedc0ad2d490eaa853c103cae2cb7406c526a550 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jos=C3=A9=20Corella?=
 <39066999+josecorella@users.noreply.github.com>
Date: Mon, 16 Sep 2024 09:48:45 -0700
Subject: [PATCH] feat: bump to dafny 4.8.0 and mpl 1.6.0 (#1356)

* feat: move to dafny 4.8.0
---
 .../action.yml                                |  21 +++
 .github/workflows/ci_codegen.yml              |  12 +-
 DynamoDbEncryption/.gitignore                 |   2 +
 .../dotnet/dafny-4.8.0.patch                  |  51 +++++++
 .../dotnet/dafny-4.8.0.patch                  |  15 ++
 .../dotnet/dafny-4.8.0.patch                  |  15 ++
 .../dotnet/dafny-4.8.0.patch                  |  15 ++
 .../test/TestFixtures.dfy                     |  50 +++----
 .../DynamoDbKeyBranchKeyIdSupplier.java       |  12 +-
 .../dbencryptionsdk/dynamodb/ToDafny.java     | 134 ++++++++++++++----
 .../dynamodb/itemencryptor/ToDafny.java       |  51 +++++--
 .../dynamodb/transforms/ToDafny.java          |   5 +-
 .../BatchGetItemInputTransformInput.java      |  12 ++
 .../BatchGetItemInputTransformOutput.java     |  12 ++
 .../BatchGetItemOutputTransformInput.java     |  24 ++++
 .../BatchGetItemOutputTransformOutput.java    |  12 ++
 .../BatchWriteItemInputTransformInput.java    |  12 ++
 .../BatchWriteItemInputTransformOutput.java   |  12 ++
 .../BatchWriteItemOutputTransformInput.java   |  24 ++++
 .../BatchWriteItemOutputTransformOutput.java  |  12 ++
 .../model/DeleteItemInputTransformInput.java  |  12 ++
 .../model/DeleteItemInputTransformOutput.java |  12 ++
 .../model/DeleteItemOutputTransformInput.java |  24 ++++
 .../DeleteItemOutputTransformOutput.java      |  12 ++
 .../model/GetItemInputTransformInput.java     |  12 ++
 .../model/GetItemInputTransformOutput.java    |  12 ++
 .../model/GetItemOutputTransformInput.java    |  24 ++++
 .../model/GetItemOutputTransformOutput.java   |  12 ++
 .../model/PutItemInputTransformInput.java     |  12 ++
 .../model/PutItemInputTransformOutput.java    |  12 ++
 .../model/PutItemOutputTransformInput.java    |  24 ++++
 .../model/PutItemOutputTransformOutput.java   |  12 ++
 .../model/QueryInputTransformInput.java       |  12 ++
 .../model/QueryInputTransformOutput.java      |  12 ++
 .../model/QueryOutputTransformInput.java      |  24 ++++
 .../model/QueryOutputTransformOutput.java     |  12 ++
 .../model/ScanInputTransformInput.java        |  12 ++
 .../model/ScanInputTransformOutput.java       |  12 ++
 .../model/ScanOutputTransformInput.java       |  24 ++++
 .../model/ScanOutputTransformOutput.java      |  12 ++
 .../model/UpdateItemInputTransformInput.java  |  12 ++
 .../model/UpdateItemInputTransformOutput.java |  12 ++
 .../model/UpdateItemOutputTransformInput.java |  24 ++++
 .../UpdateItemOutputTransformOutput.java      |  12 ++
 .../structuredencryption/ToDafny.java         |  51 ++++++-
 SharedMakefile.mk                             |  11 ++
 TestVectors/project.properties                |   4 +
 .../wrapped/TestDynamoDbEncryption.java       |  24 +++-
 .../Generated/DDBEncryption/TypeConversion.cs |   4 +
 project.properties                            |   8 +-
 submodules/MaterialProviders                  |   2 +-
 submodules/smithy-dafny                       |   2 +-
 52 files changed, 881 insertions(+), 88 deletions(-)
 create mode 100644 .github/actions/install_smithy_dafny_codegen_dependencies/action.yml
 create mode 100644 DynamoDbEncryption/codegen-patches/DynamoDbEncryption/dotnet/dafny-4.8.0.patch
 create mode 100644 DynamoDbEncryption/codegen-patches/DynamoDbEncryptionTransforms/dotnet/dafny-4.8.0.patch
 create mode 100644 DynamoDbEncryption/codegen-patches/DynamoDbItemEncryptor/dotnet/dafny-4.8.0.patch
 create mode 100644 DynamoDbEncryption/codegen-patches/StructuredEncryption/dotnet/dafny-4.8.0.patch
 create mode 100644 TestVectors/project.properties

diff --git a/.github/actions/install_smithy_dafny_codegen_dependencies/action.yml b/.github/actions/install_smithy_dafny_codegen_dependencies/action.yml
new file mode 100644
index 000000000..d4df6ab8a
--- /dev/null
+++ b/.github/actions/install_smithy_dafny_codegen_dependencies/action.yml
@@ -0,0 +1,21 @@
+#
+# This local action sets up code dependencies
+# to run Smithy-Dafny CI in GitHub Actions workflows.
+#
+
+name: "Install Smithy-Dafny codegen dependencies"
+description: "Install Java package dependencies required to run Smithy-Dafny codegen"
+runs:
+  using: "composite"
+  steps:
+    - name: Install smithy-dafny-codegen Rust dependencies locally
+      uses: gradle/gradle-build-action@v2
+      with:
+        arguments: :codegen-client:pTML :codegen-core:pTML :rust-runtime:pTML
+        build-root-directory: submodules/smithy-dafny/smithy-dafny-codegen-modules/smithy-rs
+
+    - name: Install smithy-dafny-codegen Python dependencies locally
+      uses: gradle/gradle-build-action@v2
+      with:
+        arguments: :smithy-python-codegen:pTML
+        build-root-directory: submodules/smithy-dafny/codegen/smithy-dafny-codegen-modules/smithy-python/codegen
diff --git a/.github/workflows/ci_codegen.yml b/.github/workflows/ci_codegen.yml
index 5426d8777..092259a40 100644
--- a/.github/workflows/ci_codegen.yml
+++ b/.github/workflows/ci_codegen.yml
@@ -33,6 +33,7 @@ jobs:
       - uses: actions/checkout@v3
         with:
           submodules: recursive
+      - run: git submodule update --init --recursive submodules/smithy-dafny
 
       # Only used to format generated code
       # and to translate version strings such as "nightly-latest"
@@ -47,8 +48,17 @@ jobs:
         with:
           dotnet-version: ${{ matrix.dotnet-version }}
 
+      - name: Setup Java 17 for codegen
+        uses: actions/setup-java@v3
+        with:
+          distribution: "corretto"
+          java-version: "17"
+
+      - name: Install Smithy-Dafny codegen dependencies
+        uses: ./.github/actions/install_smithy_dafny_codegen_dependencies
+
       - uses: ./.github/actions/polymorph_codegen
         with:
-          dafny: ${{ env.DAFNY_VERSION }}
+          dafny: ${{ inputs.dafny }}
           library: ${{ matrix.library }}
           diff-generated-code: true
diff --git a/DynamoDbEncryption/.gitignore b/DynamoDbEncryption/.gitignore
index b8d4ccd01..e652cbedf 100644
--- a/DynamoDbEncryption/.gitignore
+++ b/DynamoDbEncryption/.gitignore
@@ -1,6 +1,8 @@
 TestResults
 ImplementationFromDafny.cs
 TestsFromDafny.cs
+ImplementationFromDafny-cs.dtr
+TestsFromDafny-cs.dtr
 **/bin
 **/obj
 node_modules
diff --git a/DynamoDbEncryption/codegen-patches/DynamoDbEncryption/dotnet/dafny-4.8.0.patch b/DynamoDbEncryption/codegen-patches/DynamoDbEncryption/dotnet/dafny-4.8.0.patch
new file mode 100644
index 000000000..4f80638b8
--- /dev/null
+++ b/DynamoDbEncryption/codegen-patches/DynamoDbEncryption/dotnet/dafny-4.8.0.patch
@@ -0,0 +1,51 @@
+diff --git b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs
+index 9601968..a2a04f8 100644
+--- b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs
++++ a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs
+@@ -7,10 +7,43 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb
+ {
+   public static class TypeConversion
+   {
+-    private const string ISO8601DateFormat = "yyyy-MM-dd\\THH:mm:ss.fff\\Z";
+-
+-    private const string ISO8601DateFormatNoMS = "yyyy-MM-dd\\THH:mm:ss\\Z";
++    // BEGIN MANUAL EDIT
++    public static AWS.Cryptography.KeyStore.KeyStore FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S17_KeyStoreReference(software.amazon.cryptography.keystore.internaldafny.types.IKeyStoreClient value)
++    {
++      if (value is software.amazon.cryptography.keystore.internaldafny.types.IKeyStoreClient dafnyValue)
++      {
++        return new AWS.Cryptography.KeyStore.KeyStore(dafnyValue);
++      }
++      throw new System.ArgumentException("Custom implementations of AWS.Cryptography.KeyStore.KeyStore are not supported yet");
++    }
++    public static software.amazon.cryptography.keystore.internaldafny.types.IKeyStoreClient ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S17_KeyStoreReference(AWS.Cryptography.KeyStore.KeyStore value)
++    {
++      if (value is AWS.Cryptography.KeyStore.KeyStore nativeValue)
++      {
++        return nativeValue.impl();
++      }
++      throw new System.ArgumentException("Custom implementations of AWS.Cryptography.KeyStore.KeyStore are not supported yet");
++    }
++    public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.ILegacyDynamoDbEncryptor FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S32_LegacyDynamoDbEncryptorReference(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.ILegacyDynamoDbEncryptor value)
++    {
++      if (value is NativeWrapper_LegacyDynamoDbEncryptor nativeWrapper) return nativeWrapper._impl;
++      return new LegacyDynamoDbEncryptor(value);
+ 
++    }
++    public static software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.ILegacyDynamoDbEncryptor ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S32_LegacyDynamoDbEncryptorReference(AWS.Cryptography.DbEncryptionSDK.DynamoDb.ILegacyDynamoDbEncryptor value)
++    {
++      switch (value)
++      {
++        case LegacyDynamoDbEncryptor valueWithImpl:
++          return valueWithImpl._impl;
++        case LegacyDynamoDbEncryptorBase nativeImpl:
++          return new NativeWrapper_LegacyDynamoDbEncryptor(nativeImpl);
++        default:
++          throw new System.ArgumentException(
++              "Custom implementations of LegacyDynamoDbEncryptor must extend LegacyDynamoDbEncryptorBase.");
++      }
++    }
++    // END MANUAL EDIT
+     public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.BeaconKeySource FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S15_BeaconKeySource(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IBeaconKeySource value)
+     {
+       software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.BeaconKeySource concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.BeaconKeySource)value;
diff --git a/DynamoDbEncryption/codegen-patches/DynamoDbEncryptionTransforms/dotnet/dafny-4.8.0.patch b/DynamoDbEncryption/codegen-patches/DynamoDbEncryptionTransforms/dotnet/dafny-4.8.0.patch
new file mode 100644
index 000000000..e4f743fff
--- /dev/null
+++ b/DynamoDbEncryption/codegen-patches/DynamoDbEncryptionTransforms/dotnet/dafny-4.8.0.patch
@@ -0,0 +1,15 @@
+diff --git b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs
+index 2f95341..36226d3 100644
+--- b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs
++++ a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs
+@@ -7,10 +7,6 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb.Transforms
+ {
+   public static class TypeConversion
+   {
+-    private const string ISO8601DateFormat = "yyyy-MM-dd\\THH:mm:ss.fff\\Z";
+-
+-    private const string ISO8601DateFormatNoMS = "yyyy-MM-dd\\THH:mm:ss\\Z";
+-
+     public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.DynamoDbTablesEncryptionConfig FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S30_DynamoDbTablesEncryptionConfig(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IDynamoDbTablesEncryptionConfig value)
+     {
+       software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.DynamoDbTablesEncryptionConfig concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.DynamoDbTablesEncryptionConfig)value; AWS.Cryptography.DbEncryptionSDK.DynamoDb.DynamoDbTablesEncryptionConfig converted = new AWS.Cryptography.DbEncryptionSDK.DynamoDb.DynamoDbTablesEncryptionConfig(); converted.TableEncryptionConfigs = (System.Collections.Generic.Dictionary<string, AWS.Cryptography.DbEncryptionSDK.DynamoDb.DynamoDbTableEncryptionConfig>)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S30_DynamoDbTablesEncryptionConfig__M22_tableEncryptionConfigs(concrete._tableEncryptionConfigs); return converted;
diff --git a/DynamoDbEncryption/codegen-patches/DynamoDbItemEncryptor/dotnet/dafny-4.8.0.patch b/DynamoDbEncryption/codegen-patches/DynamoDbItemEncryptor/dotnet/dafny-4.8.0.patch
new file mode 100644
index 000000000..5631d0784
--- /dev/null
+++ b/DynamoDbEncryption/codegen-patches/DynamoDbItemEncryptor/dotnet/dafny-4.8.0.patch
@@ -0,0 +1,15 @@
+diff --git b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs
+index da904fc..c5b0bed 100644
+--- b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs
++++ a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs
+@@ -7,10 +7,6 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor
+ {
+   public static class TypeConversion
+   {
+-    private const string ISO8601DateFormat = "yyyy-MM-dd\\THH:mm:ss.fff\\Z";
+-
+-    private const string ISO8601DateFormatNoMS = "yyyy-MM-dd\\THH:mm:ss\\Z";
+-
+     public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.DecryptItemInput FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S16_DecryptItemInput(software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types._IDecryptItemInput value)
+     {
+       software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.DecryptItemInput concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.DecryptItemInput)value; AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.DecryptItemInput converted = new AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.DecryptItemInput(); converted.EncryptedItem = (System.Collections.Generic.Dictionary<string, Amazon.DynamoDBv2.Model.AttributeValue>)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S16_DecryptItemInput__M13_encryptedItem(concrete._encryptedItem); return converted;
diff --git a/DynamoDbEncryption/codegen-patches/StructuredEncryption/dotnet/dafny-4.8.0.patch b/DynamoDbEncryption/codegen-patches/StructuredEncryption/dotnet/dafny-4.8.0.patch
new file mode 100644
index 000000000..4f5051d38
--- /dev/null
+++ b/DynamoDbEncryption/codegen-patches/StructuredEncryption/dotnet/dafny-4.8.0.patch
@@ -0,0 +1,15 @@
+diff --git b/DynamoDbEncryption/runtimes/net/Generated/StructuredEncryption/TypeConversion.cs a/DynamoDbEncryption/runtimes/net/Generated/StructuredEncryption/TypeConversion.cs
+index d0a4e58..4e9890c 100644
+--- b/DynamoDbEncryption/runtimes/net/Generated/StructuredEncryption/TypeConversion.cs
++++ a/DynamoDbEncryption/runtimes/net/Generated/StructuredEncryption/TypeConversion.cs
+@@ -7,10 +7,6 @@ namespace AWS.Cryptography.DbEncryptionSDK.StructuredEncryption
+ {
+   public static class TypeConversion
+   {
+-    private const string ISO8601DateFormat = "yyyy-MM-dd\\THH:mm:ss.fff\\Z";
+-
+-    private const string ISO8601DateFormatNoMS = "yyyy-MM-dd\\THH:mm:ss\\Z";
+-
+     public static AWS.Cryptography.DbEncryptionSDK.StructuredEncryption.AuthenticateAction FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N20_structuredEncryption__S18_AuthenticateAction(software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny.types._IAuthenticateAction value)
+     {
+       if (value.is_SIGN) return AWS.Cryptography.DbEncryptionSDK.StructuredEncryption.AuthenticateAction.SIGN;
diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/TestFixtures.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/TestFixtures.dfy
index 2667e361c..6a6a1ef7b 100644
--- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/TestFixtures.dfy
+++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/TestFixtures.dfy
@@ -237,31 +237,31 @@ module TestFixtures {
     assume {:axiom} fresh(encryption.Modifies);
   }
 
-  method GetDynamoDbEncryptionTransforms2(actions : AttributeActions, sortKey : Option<string>)
-    returns (encryption: DynamoDbEncryptionTransforms.DynamoDbEncryptionTransformsClient)
-    ensures encryption.ValidState()
-    ensures fresh(encryption)
-    ensures fresh(encryption.Modifies)
-  {
-    var keyring := GetKmsKeyring();
-    encryption :- expect DynamoDbEncryptionTransforms.DynamoDbEncryptionTransforms(
-      DynamoDbTablesEncryptionConfig(
-        tableEncryptionConfigs := map[
-          "foo" := DynamoDbTableEncryptionConfig(
-            logicalTableName := "foo",
-            partitionKeyName := "bar",
-            sortKeyName := sortKey,
-            attributeActionsOnEncrypt := actions,
-            allowedUnsignedAttributes := Some(["plain"]),
-            allowedUnsignedAttributePrefix := None(),
-            algorithmSuiteId := None(),
-            keyring := Some(keyring)
-          )
-        ]
-      )
-    );
-    assume {:axiom} fresh(encryption.Modifies);
-  }
+  // method GetDynamoDbEncryptionTransforms2(actions : AttributeActions, sortKey : Option<string>)
+  //   returns (encryption: DynamoDbEncryptionTransforms.DynamoDbEncryptionTransformsClient)
+  //   ensures encryption.ValidState()
+  //   ensures fresh(encryption)
+  //   ensures fresh(encryption.Modifies)
+  // {
+  //   var keyring := GetKmsKeyring();
+  //   encryption :- expect DynamoDbEncryptionTransforms.DynamoDbEncryptionTransforms(
+  //     DynamoDbTablesEncryptionConfig(
+  //       tableEncryptionConfigs := map[
+  //         "foo" := DynamoDbTableEncryptionConfig(
+  //           logicalTableName := "foo",
+  //           partitionKeyName := "bar",
+  //           sortKeyName := sortKey,
+  //           attributeActionsOnEncrypt := actions,
+  //           allowedUnsignedAttributes := Some(["plain"]),
+  //           allowedUnsignedAttributePrefix := None(),
+  //           algorithmSuiteId := None(),
+  //           keyring := Some(keyring)
+  //         )
+  //       ]
+  //     )
+  //   );
+  //   assume {:axiom} fresh(encryption.Modifies);
+  // }
 
   // type AttributeActions = map<ComAmazonawsDynamodbTypes.AttributeName, AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes.CryptoAction>
 
diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/DynamoDbKeyBranchKeyIdSupplier.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/DynamoDbKeyBranchKeyIdSupplier.java
index 9c0d33bbc..2e67b9012 100644
--- a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/DynamoDbKeyBranchKeyIdSupplier.java
+++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/DynamoDbKeyBranchKeyIdSupplier.java
@@ -103,9 +103,17 @@ > GetBranchKeyIdFromDdbKey(
           this._impl.GetBranchKeyIdFromDdbKey(nativeInput);
         software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetBranchKeyIdFromDdbKeyOutput dafnyOutput =
           ToDafny.GetBranchKeyIdFromDdbKeyOutput(nativeOutput);
-        return Result.create_Success(dafnyOutput);
+        return Result.create_Success(
+          software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetBranchKeyIdFromDdbKeyOutput._typeDescriptor(),
+          Error._typeDescriptor(),
+          dafnyOutput
+        );
       } catch (RuntimeException ex) {
-        return Result.create_Failure(ToDafny.Error(ex));
+        return Result.create_Failure(
+          software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetBranchKeyIdFromDdbKeyOutput._typeDescriptor(),
+          Error._typeDescriptor(),
+          ToDafny.Error(ex)
+        );
       }
     }
 
diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/ToDafny.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/ToDafny.java
index 88677a441..a20f1f9d3 100644
--- a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/ToDafny.java
+++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/ToDafny.java
@@ -6,6 +6,7 @@
 import Wrappers_Compile.Option;
 import dafny.DafnyMap;
 import dafny.DafnySequence;
+import dafny.TypeDescriptor;
 import java.lang.Boolean;
 import java.lang.Character;
 import java.lang.IllegalArgumentException;
@@ -129,31 +130,45 @@ public static BeaconVersion BeaconVersion(
       (Objects.nonNull(nativeValue.compoundBeacons()) &&
           nativeValue.compoundBeacons().size() > 0)
         ? Option.create_Some(
+          DafnySequence._typeDescriptor(CompoundBeacon._typeDescriptor()),
           ToDafny.CompoundBeaconList(nativeValue.compoundBeacons())
         )
-        : Option.create_None();
+        : Option.create_None(
+          DafnySequence._typeDescriptor(CompoundBeacon._typeDescriptor())
+        );
     Option<DafnySequence<? extends VirtualField>> virtualFields;
     virtualFields =
       (Objects.nonNull(nativeValue.virtualFields()) &&
           nativeValue.virtualFields().size() > 0)
         ? Option.create_Some(
+          DafnySequence._typeDescriptor(VirtualField._typeDescriptor()),
           ToDafny.VirtualFieldList(nativeValue.virtualFields())
         )
-        : Option.create_None();
+        : Option.create_None(
+          DafnySequence._typeDescriptor(VirtualField._typeDescriptor())
+        );
     Option<DafnySequence<? extends EncryptedPart>> encryptedParts;
     encryptedParts =
       (Objects.nonNull(nativeValue.encryptedParts()) &&
           nativeValue.encryptedParts().size() > 0)
         ? Option.create_Some(
+          DafnySequence._typeDescriptor(EncryptedPart._typeDescriptor()),
           ToDafny.EncryptedPartsList(nativeValue.encryptedParts())
         )
-        : Option.create_None();
+        : Option.create_None(
+          DafnySequence._typeDescriptor(EncryptedPart._typeDescriptor())
+        );
     Option<DafnySequence<? extends SignedPart>> signedParts;
     signedParts =
       (Objects.nonNull(nativeValue.signedParts()) &&
           nativeValue.signedParts().size() > 0)
-        ? Option.create_Some(ToDafny.SignedPartsList(nativeValue.signedParts()))
-        : Option.create_None();
+        ? Option.create_Some(
+          DafnySequence._typeDescriptor(SignedPart._typeDescriptor()),
+          ToDafny.SignedPartsList(nativeValue.signedParts())
+        )
+        : Option.create_None(
+          DafnySequence._typeDescriptor(SignedPart._typeDescriptor())
+        );
     return new BeaconVersion(
       version,
       keyStore,
@@ -184,22 +199,33 @@ public static CompoundBeacon CompoundBeacon(
       (Objects.nonNull(nativeValue.encrypted()) &&
           nativeValue.encrypted().size() > 0)
         ? Option.create_Some(
+          DafnySequence._typeDescriptor(EncryptedPart._typeDescriptor()),
           ToDafny.EncryptedPartsList(nativeValue.encrypted())
         )
-        : Option.create_None();
+        : Option.create_None(
+          DafnySequence._typeDescriptor(EncryptedPart._typeDescriptor())
+        );
     Option<DafnySequence<? extends SignedPart>> signed;
     signed =
       (Objects.nonNull(nativeValue.signed()) && nativeValue.signed().size() > 0)
-        ? Option.create_Some(ToDafny.SignedPartsList(nativeValue.signed()))
-        : Option.create_None();
+        ? Option.create_Some(
+          DafnySequence._typeDescriptor(SignedPart._typeDescriptor()),
+          ToDafny.SignedPartsList(nativeValue.signed())
+        )
+        : Option.create_None(
+          DafnySequence._typeDescriptor(SignedPart._typeDescriptor())
+        );
     Option<DafnySequence<? extends Constructor>> constructors;
     constructors =
       (Objects.nonNull(nativeValue.constructors()) &&
           nativeValue.constructors().size() > 0)
         ? Option.create_Some(
+          DafnySequence._typeDescriptor(Constructor._typeDescriptor()),
           ToDafny.ConstructorList(nativeValue.constructors())
         )
-        : Option.create_None();
+        : Option.create_None(
+          DafnySequence._typeDescriptor(Constructor._typeDescriptor())
+        );
     return new CompoundBeacon(name, split, encrypted, signed, constructors);
   }
 
@@ -273,16 +299,22 @@ public static DynamoDbTableEncryptionConfig DynamoDbTableEncryptionConfig(
     sortKeyName =
       Objects.nonNull(nativeValue.sortKeyName())
         ? Option.create_Some(
+          DafnySequence._typeDescriptor(TypeDescriptor.CHAR),
           software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence(
             nativeValue.sortKeyName()
           )
         )
-        : Option.create_None();
+        : Option.create_None(
+          DafnySequence._typeDescriptor(TypeDescriptor.CHAR)
+        );
     Option<SearchConfig> search;
     search =
       Objects.nonNull(nativeValue.search())
-        ? Option.create_Some(ToDafny.SearchConfig(nativeValue.search()))
-        : Option.create_None();
+        ? Option.create_Some(
+          SearchConfig._typeDescriptor(),
+          ToDafny.SearchConfig(nativeValue.search())
+        )
+        : Option.create_None(SearchConfig._typeDescriptor());
     DafnyMap<
       ? extends DafnySequence<? extends Character>,
       ? extends CryptoAction
@@ -296,61 +328,78 @@ public static DynamoDbTableEncryptionConfig DynamoDbTableEncryptionConfig(
       (Objects.nonNull(nativeValue.allowedUnsignedAttributes()) &&
           nativeValue.allowedUnsignedAttributes().size() > 0)
         ? Option.create_Some(
+          DafnySequence._typeDescriptor(
+            DafnySequence._typeDescriptor(TypeDescriptor.CHAR)
+          ),
           software.amazon.cryptography.services.dynamodb.internaldafny.ToDafny.AttributeNameList(
             nativeValue.allowedUnsignedAttributes()
           )
         )
-        : Option.create_None();
+        : Option.create_None(
+          DafnySequence._typeDescriptor(
+            DafnySequence._typeDescriptor(TypeDescriptor.CHAR)
+          )
+        );
     Option<DafnySequence<? extends Character>> allowedUnsignedAttributePrefix;
     allowedUnsignedAttributePrefix =
       Objects.nonNull(nativeValue.allowedUnsignedAttributePrefix())
         ? Option.create_Some(
+          DafnySequence._typeDescriptor(TypeDescriptor.CHAR),
           software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence(
             nativeValue.allowedUnsignedAttributePrefix()
           )
         )
-        : Option.create_None();
+        : Option.create_None(
+          DafnySequence._typeDescriptor(TypeDescriptor.CHAR)
+        );
     Option<DBEAlgorithmSuiteId> algorithmSuiteId;
     algorithmSuiteId =
       Objects.nonNull(nativeValue.algorithmSuiteId())
         ? Option.create_Some(
+          DBEAlgorithmSuiteId._typeDescriptor(),
           software.amazon.cryptography.materialproviders.ToDafny.DBEAlgorithmSuiteId(
             nativeValue.algorithmSuiteId()
           )
         )
-        : Option.create_None();
+        : Option.create_None(DBEAlgorithmSuiteId._typeDescriptor());
     Option<IKeyring> keyring;
     keyring =
       Objects.nonNull(nativeValue.keyring())
         ? Option.create_Some(
+          TypeDescriptor.reference(IKeyring.class),
           software.amazon.cryptography.materialproviders.ToDafny.Keyring(
             nativeValue.keyring()
           )
         )
-        : Option.create_None();
+        : Option.create_None(TypeDescriptor.reference(IKeyring.class));
     Option<ICryptographicMaterialsManager> cmm;
     cmm =
       Objects.nonNull(nativeValue.cmm())
         ? Option.create_Some(
+          TypeDescriptor.reference(ICryptographicMaterialsManager.class),
           software.amazon.cryptography.materialproviders.ToDafny.CryptographicMaterialsManager(
             nativeValue.cmm()
           )
         )
-        : Option.create_None();
+        : Option.create_None(
+          TypeDescriptor.reference(ICryptographicMaterialsManager.class)
+        );
     Option<LegacyOverride> legacyOverride;
     legacyOverride =
       Objects.nonNull(nativeValue.legacyOverride())
         ? Option.create_Some(
+          LegacyOverride._typeDescriptor(),
           ToDafny.LegacyOverride(nativeValue.legacyOverride())
         )
-        : Option.create_None();
+        : Option.create_None(LegacyOverride._typeDescriptor());
     Option<PlaintextOverride> plaintextOverride;
     plaintextOverride =
       Objects.nonNull(nativeValue.plaintextOverride())
         ? Option.create_Some(
+          PlaintextOverride._typeDescriptor(),
           ToDafny.PlaintextOverride(nativeValue.plaintextOverride())
         )
-        : Option.create_None();
+        : Option.create_None(PlaintextOverride._typeDescriptor());
     return new DynamoDbTableEncryptionConfig(
       logicalTableName,
       partitionKeyName,
@@ -393,29 +442,38 @@ public static EncryptedDataKeyDescription EncryptedDataKeyDescription(
     keyProviderInfo =
       Objects.nonNull(nativeValue.keyProviderInfo())
         ? Option.create_Some(
+          DafnySequence._typeDescriptor(TypeDescriptor.CHAR),
           software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence(
             nativeValue.keyProviderInfo()
           )
         )
-        : Option.create_None();
+        : Option.create_None(
+          DafnySequence._typeDescriptor(TypeDescriptor.CHAR)
+        );
     Option<DafnySequence<? extends Character>> branchKeyId;
     branchKeyId =
       Objects.nonNull(nativeValue.branchKeyId())
         ? Option.create_Some(
+          DafnySequence._typeDescriptor(TypeDescriptor.CHAR),
           software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence(
             nativeValue.branchKeyId()
           )
         )
-        : Option.create_None();
+        : Option.create_None(
+          DafnySequence._typeDescriptor(TypeDescriptor.CHAR)
+        );
     Option<DafnySequence<? extends Character>> branchKeyVersion;
     branchKeyVersion =
       Objects.nonNull(nativeValue.branchKeyVersion())
         ? Option.create_Some(
+          DafnySequence._typeDescriptor(TypeDescriptor.CHAR),
           software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence(
             nativeValue.branchKeyVersion()
           )
         )
-        : Option.create_None();
+        : Option.create_None(
+          DafnySequence._typeDescriptor(TypeDescriptor.CHAR)
+        );
     return new EncryptedDataKeyDescription(
       keyProviderId,
       keyProviderInfo,
@@ -570,11 +628,12 @@ public static LegacyOverride LegacyOverride(
     defaultAttributeFlag =
       Objects.nonNull(nativeValue.defaultAttributeFlag())
         ? Option.create_Some(
+          CryptoAction._typeDescriptor(),
           software.amazon.cryptography.dbencryptionsdk.structuredencryption.ToDafny.CryptoAction(
             nativeValue.defaultAttributeFlag()
           )
         )
-        : Option.create_None();
+        : Option.create_None(CryptoAction._typeDescriptor());
     return new LegacyOverride(
       policy,
       encryptor,
@@ -603,11 +662,12 @@ public static MultiKeyStore MultiKeyStore(
     cache =
       Objects.nonNull(nativeValue.cache())
         ? Option.create_Some(
+          CacheType._typeDescriptor(),
           software.amazon.cryptography.materialproviders.ToDafny.CacheType(
             nativeValue.cache()
           )
         )
-        : Option.create_None();
+        : Option.create_None(CacheType._typeDescriptor());
     return new MultiKeyStore(keyFieldName, cacheTTL, cache);
   }
 
@@ -666,11 +726,14 @@ public static SignedPart SignedPart(
     loc =
       Objects.nonNull(nativeValue.loc())
         ? Option.create_Some(
+          DafnySequence._typeDescriptor(TypeDescriptor.CHAR),
           software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence(
             nativeValue.loc()
           )
         )
-        : Option.create_None();
+        : Option.create_None(
+          DafnySequence._typeDescriptor(TypeDescriptor.CHAR)
+        );
     return new SignedPart(name, prefix, loc);
   }
 
@@ -701,16 +764,22 @@ public static StandardBeacon StandardBeacon(
     loc =
       Objects.nonNull(nativeValue.loc())
         ? Option.create_Some(
+          DafnySequence._typeDescriptor(TypeDescriptor.CHAR),
           software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence(
             nativeValue.loc()
           )
         )
-        : Option.create_None();
+        : Option.create_None(
+          DafnySequence._typeDescriptor(TypeDescriptor.CHAR)
+        );
     Option<BeaconStyle> style;
     style =
       Objects.nonNull(nativeValue.style())
-        ? Option.create_Some(ToDafny.BeaconStyle(nativeValue.style()))
-        : Option.create_None();
+        ? Option.create_Some(
+          BeaconStyle._typeDescriptor(),
+          ToDafny.BeaconStyle(nativeValue.style())
+        )
+        : Option.create_None(BeaconStyle._typeDescriptor());
     return new StandardBeacon(name, length, loc, style);
   }
 
@@ -744,8 +813,13 @@ public static VirtualPart VirtualPart(
     Option<DafnySequence<? extends VirtualTransform>> trans;
     trans =
       (Objects.nonNull(nativeValue.trans()) && nativeValue.trans().size() > 0)
-        ? Option.create_Some(ToDafny.VirtualTransformList(nativeValue.trans()))
-        : Option.create_None();
+        ? Option.create_Some(
+          DafnySequence._typeDescriptor(VirtualTransform._typeDescriptor()),
+          ToDafny.VirtualTransformList(nativeValue.trans())
+        )
+        : Option.create_None(
+          DafnySequence._typeDescriptor(VirtualTransform._typeDescriptor())
+        );
     return new VirtualPart(loc, trans);
   }
 
diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/itemencryptor/ToDafny.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/itemencryptor/ToDafny.java
index c0ea35b5a..37d593f32 100644
--- a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/itemencryptor/ToDafny.java
+++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/itemencryptor/ToDafny.java
@@ -6,6 +6,7 @@
 import Wrappers_Compile.Option;
 import dafny.DafnyMap;
 import dafny.DafnySequence;
+import dafny.TypeDescriptor;
 import java.lang.Byte;
 import java.lang.Character;
 import java.lang.RuntimeException;
@@ -92,8 +93,11 @@ public static DecryptItemOutput DecryptItemOutput(
     Option<ParsedHeader> parsedHeader;
     parsedHeader =
       Objects.nonNull(nativeValue.parsedHeader())
-        ? Option.create_Some(ToDafny.ParsedHeader(nativeValue.parsedHeader()))
-        : Option.create_None();
+        ? Option.create_Some(
+          ParsedHeader._typeDescriptor(),
+          ToDafny.ParsedHeader(nativeValue.parsedHeader())
+        )
+        : Option.create_None(ParsedHeader._typeDescriptor());
     return new DecryptItemOutput(plaintextItem, parsedHeader);
   }
 
@@ -114,11 +118,14 @@ public static DynamoDbItemEncryptorConfig DynamoDbItemEncryptorConfig(
     sortKeyName =
       Objects.nonNull(nativeValue.sortKeyName())
         ? Option.create_Some(
+          DafnySequence._typeDescriptor(TypeDescriptor.CHAR),
           software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence(
             nativeValue.sortKeyName()
           )
         )
-        : Option.create_None();
+        : Option.create_None(
+          DafnySequence._typeDescriptor(TypeDescriptor.CHAR)
+        );
     DafnyMap<
       ? extends DafnySequence<? extends Character>,
       ? extends CryptoAction
@@ -134,65 +141,82 @@ public static DynamoDbItemEncryptorConfig DynamoDbItemEncryptorConfig(
       (Objects.nonNull(nativeValue.allowedUnsignedAttributes()) &&
           nativeValue.allowedUnsignedAttributes().size() > 0)
         ? Option.create_Some(
+          DafnySequence._typeDescriptor(
+            DafnySequence._typeDescriptor(TypeDescriptor.CHAR)
+          ),
           software.amazon.cryptography.services.dynamodb.internaldafny.ToDafny.AttributeNameList(
             nativeValue.allowedUnsignedAttributes()
           )
         )
-        : Option.create_None();
+        : Option.create_None(
+          DafnySequence._typeDescriptor(
+            DafnySequence._typeDescriptor(TypeDescriptor.CHAR)
+          )
+        );
     Option<DafnySequence<? extends Character>> allowedUnsignedAttributePrefix;
     allowedUnsignedAttributePrefix =
       Objects.nonNull(nativeValue.allowedUnsignedAttributePrefix())
         ? Option.create_Some(
+          DafnySequence._typeDescriptor(TypeDescriptor.CHAR),
           software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence(
             nativeValue.allowedUnsignedAttributePrefix()
           )
         )
-        : Option.create_None();
+        : Option.create_None(
+          DafnySequence._typeDescriptor(TypeDescriptor.CHAR)
+        );
     Option<DBEAlgorithmSuiteId> algorithmSuiteId;
     algorithmSuiteId =
       Objects.nonNull(nativeValue.algorithmSuiteId())
         ? Option.create_Some(
+          DBEAlgorithmSuiteId._typeDescriptor(),
           software.amazon.cryptography.materialproviders.ToDafny.DBEAlgorithmSuiteId(
             nativeValue.algorithmSuiteId()
           )
         )
-        : Option.create_None();
+        : Option.create_None(DBEAlgorithmSuiteId._typeDescriptor());
     Option<IKeyring> keyring;
     keyring =
       Objects.nonNull(nativeValue.keyring())
         ? Option.create_Some(
+          TypeDescriptor.reference(IKeyring.class),
           software.amazon.cryptography.materialproviders.ToDafny.Keyring(
             nativeValue.keyring()
           )
         )
-        : Option.create_None();
+        : Option.create_None(TypeDescriptor.reference(IKeyring.class));
     Option<ICryptographicMaterialsManager> cmm;
     cmm =
       Objects.nonNull(nativeValue.cmm())
         ? Option.create_Some(
+          TypeDescriptor.reference(ICryptographicMaterialsManager.class),
           software.amazon.cryptography.materialproviders.ToDafny.CryptographicMaterialsManager(
             nativeValue.cmm()
           )
         )
-        : Option.create_None();
+        : Option.create_None(
+          TypeDescriptor.reference(ICryptographicMaterialsManager.class)
+        );
     Option<LegacyOverride> legacyOverride;
     legacyOverride =
       Objects.nonNull(nativeValue.legacyOverride())
         ? Option.create_Some(
+          LegacyOverride._typeDescriptor(),
           software.amazon.cryptography.dbencryptionsdk.dynamodb.ToDafny.LegacyOverride(
             nativeValue.legacyOverride()
           )
         )
-        : Option.create_None();
+        : Option.create_None(LegacyOverride._typeDescriptor());
     Option<PlaintextOverride> plaintextOverride;
     plaintextOverride =
       Objects.nonNull(nativeValue.plaintextOverride())
         ? Option.create_Some(
+          PlaintextOverride._typeDescriptor(),
           software.amazon.cryptography.dbencryptionsdk.dynamodb.ToDafny.PlaintextOverride(
             nativeValue.plaintextOverride()
           )
         )
-        : Option.create_None();
+        : Option.create_None(PlaintextOverride._typeDescriptor());
     return new DynamoDbItemEncryptorConfig(
       logicalTableName,
       partitionKeyName,
@@ -236,8 +260,11 @@ public static EncryptItemOutput EncryptItemOutput(
     Option<ParsedHeader> parsedHeader;
     parsedHeader =
       Objects.nonNull(nativeValue.parsedHeader())
-        ? Option.create_Some(ToDafny.ParsedHeader(nativeValue.parsedHeader()))
-        : Option.create_None();
+        ? Option.create_Some(
+          ParsedHeader._typeDescriptor(),
+          ToDafny.ParsedHeader(nativeValue.parsedHeader())
+        )
+        : Option.create_None(ParsedHeader._typeDescriptor());
     return new EncryptItemOutput(encryptedItem, parsedHeader);
   }
 
diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/ToDafny.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/ToDafny.java
index a2b9dc32a..b1d3deba6 100644
--- a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/ToDafny.java
+++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/ToDafny.java
@@ -6,6 +6,7 @@
 import Wrappers_Compile.Option;
 import dafny.DafnyMap;
 import dafny.DafnySequence;
+import dafny.TypeDescriptor;
 import java.lang.Character;
 import java.lang.Integer;
 import java.lang.RuntimeException;
@@ -596,8 +597,8 @@ public static ResolveAttributesInput ResolveAttributesInput(
     Option<Integer> version;
     version =
       Objects.nonNull(nativeValue.Version())
-        ? Option.create_Some((nativeValue.Version()))
-        : Option.create_None();
+        ? Option.create_Some(TypeDescriptor.INT, (nativeValue.Version()))
+        : Option.create_None(TypeDescriptor.INT);
     return new ResolveAttributesInput(tableName, item, version);
   }
 
diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/BatchGetItemInputTransformInput.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/BatchGetItemInputTransformInput.java
index 360c70c49..a0f0bd0e9 100644
--- a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/BatchGetItemInputTransformInput.java
+++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/BatchGetItemInputTransformInput.java
@@ -8,12 +8,18 @@
 
 public class BatchGetItemInputTransformInput {
 
+  /**
+   * <p>Represents the input of a <code>BatchGetItem</code> operation.</p>
+   */
   private final BatchGetItemRequest sdkInput;
 
   protected BatchGetItemInputTransformInput(BuilderImpl builder) {
     this.sdkInput = builder.sdkInput();
   }
 
+  /**
+   * @return <p>Represents the input of a <code>BatchGetItem</code> operation.</p>
+   */
   public BatchGetItemRequest sdkInput() {
     return this.sdkInput;
   }
@@ -27,8 +33,14 @@ public static Builder builder() {
   }
 
   public interface Builder {
+    /**
+     * @param sdkInput <p>Represents the input of a <code>BatchGetItem</code> operation.</p>
+     */
     Builder sdkInput(BatchGetItemRequest sdkInput);
 
+    /**
+     * @return <p>Represents the input of a <code>BatchGetItem</code> operation.</p>
+     */
     BatchGetItemRequest sdkInput();
 
     BatchGetItemInputTransformInput build();
diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/BatchGetItemInputTransformOutput.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/BatchGetItemInputTransformOutput.java
index ca9f10aa4..807674dd3 100644
--- a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/BatchGetItemInputTransformOutput.java
+++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/BatchGetItemInputTransformOutput.java
@@ -8,12 +8,18 @@
 
 public class BatchGetItemInputTransformOutput {
 
+  /**
+   * <p>Represents the input of a <code>BatchGetItem</code> operation.</p>
+   */
   private final BatchGetItemRequest transformedInput;
 
   protected BatchGetItemInputTransformOutput(BuilderImpl builder) {
     this.transformedInput = builder.transformedInput();
   }
 
+  /**
+   * @return <p>Represents the input of a <code>BatchGetItem</code> operation.</p>
+   */
   public BatchGetItemRequest transformedInput() {
     return this.transformedInput;
   }
@@ -27,8 +33,14 @@ public static Builder builder() {
   }
 
   public interface Builder {
+    /**
+     * @param transformedInput <p>Represents the input of a <code>BatchGetItem</code> operation.</p>
+     */
     Builder transformedInput(BatchGetItemRequest transformedInput);
 
+    /**
+     * @return <p>Represents the input of a <code>BatchGetItem</code> operation.</p>
+     */
     BatchGetItemRequest transformedInput();
 
     BatchGetItemInputTransformOutput build();
diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/BatchGetItemOutputTransformInput.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/BatchGetItemOutputTransformInput.java
index 5769cb985..c6afc9f5f 100644
--- a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/BatchGetItemOutputTransformInput.java
+++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/BatchGetItemOutputTransformInput.java
@@ -9,8 +9,14 @@
 
 public class BatchGetItemOutputTransformInput {
 
+  /**
+   * <p>Represents the output of a <code>BatchGetItem</code> operation.</p>
+   */
   private final BatchGetItemResponse sdkOutput;
 
+  /**
+   * <p>Represents the input of a <code>BatchGetItem</code> operation.</p>
+   */
   private final BatchGetItemRequest originalInput;
 
   protected BatchGetItemOutputTransformInput(BuilderImpl builder) {
@@ -18,10 +24,16 @@ protected BatchGetItemOutputTransformInput(BuilderImpl builder) {
     this.originalInput = builder.originalInput();
   }
 
+  /**
+   * @return <p>Represents the output of a <code>BatchGetItem</code> operation.</p>
+   */
   public BatchGetItemResponse sdkOutput() {
     return this.sdkOutput;
   }
 
+  /**
+   * @return <p>Represents the input of a <code>BatchGetItem</code> operation.</p>
+   */
   public BatchGetItemRequest originalInput() {
     return this.originalInput;
   }
@@ -35,12 +47,24 @@ public static Builder builder() {
   }
 
   public interface Builder {
+    /**
+     * @param sdkOutput <p>Represents the output of a <code>BatchGetItem</code> operation.</p>
+     */
     Builder sdkOutput(BatchGetItemResponse sdkOutput);
 
+    /**
+     * @return <p>Represents the output of a <code>BatchGetItem</code> operation.</p>
+     */
     BatchGetItemResponse sdkOutput();
 
+    /**
+     * @param originalInput <p>Represents the input of a <code>BatchGetItem</code> operation.</p>
+     */
     Builder originalInput(BatchGetItemRequest originalInput);
 
+    /**
+     * @return <p>Represents the input of a <code>BatchGetItem</code> operation.</p>
+     */
     BatchGetItemRequest originalInput();
 
     BatchGetItemOutputTransformInput build();
diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/BatchGetItemOutputTransformOutput.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/BatchGetItemOutputTransformOutput.java
index 551a85a67..efbb90723 100644
--- a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/BatchGetItemOutputTransformOutput.java
+++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/BatchGetItemOutputTransformOutput.java
@@ -8,12 +8,18 @@
 
 public class BatchGetItemOutputTransformOutput {
 
+  /**
+   * <p>Represents the output of a <code>BatchGetItem</code> operation.</p>
+   */
   private final BatchGetItemResponse transformedOutput;
 
   protected BatchGetItemOutputTransformOutput(BuilderImpl builder) {
     this.transformedOutput = builder.transformedOutput();
   }
 
+  /**
+   * @return <p>Represents the output of a <code>BatchGetItem</code> operation.</p>
+   */
   public BatchGetItemResponse transformedOutput() {
     return this.transformedOutput;
   }
@@ -27,8 +33,14 @@ public static Builder builder() {
   }
 
   public interface Builder {
+    /**
+     * @param transformedOutput <p>Represents the output of a <code>BatchGetItem</code> operation.</p>
+     */
     Builder transformedOutput(BatchGetItemResponse transformedOutput);
 
+    /**
+     * @return <p>Represents the output of a <code>BatchGetItem</code> operation.</p>
+     */
     BatchGetItemResponse transformedOutput();
 
     BatchGetItemOutputTransformOutput build();
diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/BatchWriteItemInputTransformInput.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/BatchWriteItemInputTransformInput.java
index 2b162ea90..eb493cc6d 100644
--- a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/BatchWriteItemInputTransformInput.java
+++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/BatchWriteItemInputTransformInput.java
@@ -8,12 +8,18 @@
 
 public class BatchWriteItemInputTransformInput {
 
+  /**
+   * <p>Represents the input of a <code>BatchWriteItem</code> operation.</p>
+   */
   private final BatchWriteItemRequest sdkInput;
 
   protected BatchWriteItemInputTransformInput(BuilderImpl builder) {
     this.sdkInput = builder.sdkInput();
   }
 
+  /**
+   * @return <p>Represents the input of a <code>BatchWriteItem</code> operation.</p>
+   */
   public BatchWriteItemRequest sdkInput() {
     return this.sdkInput;
   }
@@ -27,8 +33,14 @@ public static Builder builder() {
   }
 
   public interface Builder {
+    /**
+     * @param sdkInput <p>Represents the input of a <code>BatchWriteItem</code> operation.</p>
+     */
     Builder sdkInput(BatchWriteItemRequest sdkInput);
 
+    /**
+     * @return <p>Represents the input of a <code>BatchWriteItem</code> operation.</p>
+     */
     BatchWriteItemRequest sdkInput();
 
     BatchWriteItemInputTransformInput build();
diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/BatchWriteItemInputTransformOutput.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/BatchWriteItemInputTransformOutput.java
index 62014c5d1..317a931ba 100644
--- a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/BatchWriteItemInputTransformOutput.java
+++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/BatchWriteItemInputTransformOutput.java
@@ -8,12 +8,18 @@
 
 public class BatchWriteItemInputTransformOutput {
 
+  /**
+   * <p>Represents the input of a <code>BatchWriteItem</code> operation.</p>
+   */
   private final BatchWriteItemRequest transformedInput;
 
   protected BatchWriteItemInputTransformOutput(BuilderImpl builder) {
     this.transformedInput = builder.transformedInput();
   }
 
+  /**
+   * @return <p>Represents the input of a <code>BatchWriteItem</code> operation.</p>
+   */
   public BatchWriteItemRequest transformedInput() {
     return this.transformedInput;
   }
@@ -27,8 +33,14 @@ public static Builder builder() {
   }
 
   public interface Builder {
+    /**
+     * @param transformedInput <p>Represents the input of a <code>BatchWriteItem</code> operation.</p>
+     */
     Builder transformedInput(BatchWriteItemRequest transformedInput);
 
+    /**
+     * @return <p>Represents the input of a <code>BatchWriteItem</code> operation.</p>
+     */
     BatchWriteItemRequest transformedInput();
 
     BatchWriteItemInputTransformOutput build();
diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/BatchWriteItemOutputTransformInput.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/BatchWriteItemOutputTransformInput.java
index 711e59ed8..f720aa65e 100644
--- a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/BatchWriteItemOutputTransformInput.java
+++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/BatchWriteItemOutputTransformInput.java
@@ -9,8 +9,14 @@
 
 public class BatchWriteItemOutputTransformInput {
 
+  /**
+   * <p>Represents the output of a <code>BatchWriteItem</code> operation.</p>
+   */
   private final BatchWriteItemResponse sdkOutput;
 
+  /**
+   * <p>Represents the input of a <code>BatchWriteItem</code> operation.</p>
+   */
   private final BatchWriteItemRequest originalInput;
 
   protected BatchWriteItemOutputTransformInput(BuilderImpl builder) {
@@ -18,10 +24,16 @@ protected BatchWriteItemOutputTransformInput(BuilderImpl builder) {
     this.originalInput = builder.originalInput();
   }
 
+  /**
+   * @return <p>Represents the output of a <code>BatchWriteItem</code> operation.</p>
+   */
   public BatchWriteItemResponse sdkOutput() {
     return this.sdkOutput;
   }
 
+  /**
+   * @return <p>Represents the input of a <code>BatchWriteItem</code> operation.</p>
+   */
   public BatchWriteItemRequest originalInput() {
     return this.originalInput;
   }
@@ -35,12 +47,24 @@ public static Builder builder() {
   }
 
   public interface Builder {
+    /**
+     * @param sdkOutput <p>Represents the output of a <code>BatchWriteItem</code> operation.</p>
+     */
     Builder sdkOutput(BatchWriteItemResponse sdkOutput);
 
+    /**
+     * @return <p>Represents the output of a <code>BatchWriteItem</code> operation.</p>
+     */
     BatchWriteItemResponse sdkOutput();
 
+    /**
+     * @param originalInput <p>Represents the input of a <code>BatchWriteItem</code> operation.</p>
+     */
     Builder originalInput(BatchWriteItemRequest originalInput);
 
+    /**
+     * @return <p>Represents the input of a <code>BatchWriteItem</code> operation.</p>
+     */
     BatchWriteItemRequest originalInput();
 
     BatchWriteItemOutputTransformInput build();
diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/BatchWriteItemOutputTransformOutput.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/BatchWriteItemOutputTransformOutput.java
index cb6d0a66c..19bc50307 100644
--- a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/BatchWriteItemOutputTransformOutput.java
+++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/BatchWriteItemOutputTransformOutput.java
@@ -8,12 +8,18 @@
 
 public class BatchWriteItemOutputTransformOutput {
 
+  /**
+   * <p>Represents the output of a <code>BatchWriteItem</code> operation.</p>
+   */
   private final BatchWriteItemResponse transformedOutput;
 
   protected BatchWriteItemOutputTransformOutput(BuilderImpl builder) {
     this.transformedOutput = builder.transformedOutput();
   }
 
+  /**
+   * @return <p>Represents the output of a <code>BatchWriteItem</code> operation.</p>
+   */
   public BatchWriteItemResponse transformedOutput() {
     return this.transformedOutput;
   }
@@ -27,8 +33,14 @@ public static Builder builder() {
   }
 
   public interface Builder {
+    /**
+     * @param transformedOutput <p>Represents the output of a <code>BatchWriteItem</code> operation.</p>
+     */
     Builder transformedOutput(BatchWriteItemResponse transformedOutput);
 
+    /**
+     * @return <p>Represents the output of a <code>BatchWriteItem</code> operation.</p>
+     */
     BatchWriteItemResponse transformedOutput();
 
     BatchWriteItemOutputTransformOutput build();
diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/DeleteItemInputTransformInput.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/DeleteItemInputTransformInput.java
index 94f14a622..b459bc907 100644
--- a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/DeleteItemInputTransformInput.java
+++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/DeleteItemInputTransformInput.java
@@ -8,12 +8,18 @@
 
 public class DeleteItemInputTransformInput {
 
+  /**
+   * <p>Represents the input of a <code>DeleteItem</code> operation.</p>
+   */
   private final DeleteItemRequest sdkInput;
 
   protected DeleteItemInputTransformInput(BuilderImpl builder) {
     this.sdkInput = builder.sdkInput();
   }
 
+  /**
+   * @return <p>Represents the input of a <code>DeleteItem</code> operation.</p>
+   */
   public DeleteItemRequest sdkInput() {
     return this.sdkInput;
   }
@@ -27,8 +33,14 @@ public static Builder builder() {
   }
 
   public interface Builder {
+    /**
+     * @param sdkInput <p>Represents the input of a <code>DeleteItem</code> operation.</p>
+     */
     Builder sdkInput(DeleteItemRequest sdkInput);
 
+    /**
+     * @return <p>Represents the input of a <code>DeleteItem</code> operation.</p>
+     */
     DeleteItemRequest sdkInput();
 
     DeleteItemInputTransformInput build();
diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/DeleteItemInputTransformOutput.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/DeleteItemInputTransformOutput.java
index f4295e34b..e1668f03a 100644
--- a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/DeleteItemInputTransformOutput.java
+++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/DeleteItemInputTransformOutput.java
@@ -8,12 +8,18 @@
 
 public class DeleteItemInputTransformOutput {
 
+  /**
+   * <p>Represents the input of a <code>DeleteItem</code> operation.</p>
+   */
   private final DeleteItemRequest transformedInput;
 
   protected DeleteItemInputTransformOutput(BuilderImpl builder) {
     this.transformedInput = builder.transformedInput();
   }
 
+  /**
+   * @return <p>Represents the input of a <code>DeleteItem</code> operation.</p>
+   */
   public DeleteItemRequest transformedInput() {
     return this.transformedInput;
   }
@@ -27,8 +33,14 @@ public static Builder builder() {
   }
 
   public interface Builder {
+    /**
+     * @param transformedInput <p>Represents the input of a <code>DeleteItem</code> operation.</p>
+     */
     Builder transformedInput(DeleteItemRequest transformedInput);
 
+    /**
+     * @return <p>Represents the input of a <code>DeleteItem</code> operation.</p>
+     */
     DeleteItemRequest transformedInput();
 
     DeleteItemInputTransformOutput build();
diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/DeleteItemOutputTransformInput.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/DeleteItemOutputTransformInput.java
index 0147e9520..8cd44af88 100644
--- a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/DeleteItemOutputTransformInput.java
+++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/DeleteItemOutputTransformInput.java
@@ -9,8 +9,14 @@
 
 public class DeleteItemOutputTransformInput {
 
+  /**
+   * <p>Represents the output of a <code>DeleteItem</code> operation.</p>
+   */
   private final DeleteItemResponse sdkOutput;
 
+  /**
+   * <p>Represents the input of a <code>DeleteItem</code> operation.</p>
+   */
   private final DeleteItemRequest originalInput;
 
   protected DeleteItemOutputTransformInput(BuilderImpl builder) {
@@ -18,10 +24,16 @@ protected DeleteItemOutputTransformInput(BuilderImpl builder) {
     this.originalInput = builder.originalInput();
   }
 
+  /**
+   * @return <p>Represents the output of a <code>DeleteItem</code> operation.</p>
+   */
   public DeleteItemResponse sdkOutput() {
     return this.sdkOutput;
   }
 
+  /**
+   * @return <p>Represents the input of a <code>DeleteItem</code> operation.</p>
+   */
   public DeleteItemRequest originalInput() {
     return this.originalInput;
   }
@@ -35,12 +47,24 @@ public static Builder builder() {
   }
 
   public interface Builder {
+    /**
+     * @param sdkOutput <p>Represents the output of a <code>DeleteItem</code> operation.</p>
+     */
     Builder sdkOutput(DeleteItemResponse sdkOutput);
 
+    /**
+     * @return <p>Represents the output of a <code>DeleteItem</code> operation.</p>
+     */
     DeleteItemResponse sdkOutput();
 
+    /**
+     * @param originalInput <p>Represents the input of a <code>DeleteItem</code> operation.</p>
+     */
     Builder originalInput(DeleteItemRequest originalInput);
 
+    /**
+     * @return <p>Represents the input of a <code>DeleteItem</code> operation.</p>
+     */
     DeleteItemRequest originalInput();
 
     DeleteItemOutputTransformInput build();
diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/DeleteItemOutputTransformOutput.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/DeleteItemOutputTransformOutput.java
index 8c9f1d184..883df60bc 100644
--- a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/DeleteItemOutputTransformOutput.java
+++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/DeleteItemOutputTransformOutput.java
@@ -8,12 +8,18 @@
 
 public class DeleteItemOutputTransformOutput {
 
+  /**
+   * <p>Represents the output of a <code>DeleteItem</code> operation.</p>
+   */
   private final DeleteItemResponse transformedOutput;
 
   protected DeleteItemOutputTransformOutput(BuilderImpl builder) {
     this.transformedOutput = builder.transformedOutput();
   }
 
+  /**
+   * @return <p>Represents the output of a <code>DeleteItem</code> operation.</p>
+   */
   public DeleteItemResponse transformedOutput() {
     return this.transformedOutput;
   }
@@ -27,8 +33,14 @@ public static Builder builder() {
   }
 
   public interface Builder {
+    /**
+     * @param transformedOutput <p>Represents the output of a <code>DeleteItem</code> operation.</p>
+     */
     Builder transformedOutput(DeleteItemResponse transformedOutput);
 
+    /**
+     * @return <p>Represents the output of a <code>DeleteItem</code> operation.</p>
+     */
     DeleteItemResponse transformedOutput();
 
     DeleteItemOutputTransformOutput build();
diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/GetItemInputTransformInput.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/GetItemInputTransformInput.java
index 99808cc7d..9ab5e25f0 100644
--- a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/GetItemInputTransformInput.java
+++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/GetItemInputTransformInput.java
@@ -8,12 +8,18 @@
 
 public class GetItemInputTransformInput {
 
+  /**
+   * <p>Represents the input of a <code>GetItem</code> operation.</p>
+   */
   private final GetItemRequest sdkInput;
 
   protected GetItemInputTransformInput(BuilderImpl builder) {
     this.sdkInput = builder.sdkInput();
   }
 
+  /**
+   * @return <p>Represents the input of a <code>GetItem</code> operation.</p>
+   */
   public GetItemRequest sdkInput() {
     return this.sdkInput;
   }
@@ -27,8 +33,14 @@ public static Builder builder() {
   }
 
   public interface Builder {
+    /**
+     * @param sdkInput <p>Represents the input of a <code>GetItem</code> operation.</p>
+     */
     Builder sdkInput(GetItemRequest sdkInput);
 
+    /**
+     * @return <p>Represents the input of a <code>GetItem</code> operation.</p>
+     */
     GetItemRequest sdkInput();
 
     GetItemInputTransformInput build();
diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/GetItemInputTransformOutput.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/GetItemInputTransformOutput.java
index a94eb1600..b0b057d00 100644
--- a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/GetItemInputTransformOutput.java
+++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/GetItemInputTransformOutput.java
@@ -8,12 +8,18 @@
 
 public class GetItemInputTransformOutput {
 
+  /**
+   * <p>Represents the input of a <code>GetItem</code> operation.</p>
+   */
   private final GetItemRequest transformedInput;
 
   protected GetItemInputTransformOutput(BuilderImpl builder) {
     this.transformedInput = builder.transformedInput();
   }
 
+  /**
+   * @return <p>Represents the input of a <code>GetItem</code> operation.</p>
+   */
   public GetItemRequest transformedInput() {
     return this.transformedInput;
   }
@@ -27,8 +33,14 @@ public static Builder builder() {
   }
 
   public interface Builder {
+    /**
+     * @param transformedInput <p>Represents the input of a <code>GetItem</code> operation.</p>
+     */
     Builder transformedInput(GetItemRequest transformedInput);
 
+    /**
+     * @return <p>Represents the input of a <code>GetItem</code> operation.</p>
+     */
     GetItemRequest transformedInput();
 
     GetItemInputTransformOutput build();
diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/GetItemOutputTransformInput.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/GetItemOutputTransformInput.java
index 764fe7cdc..b11d9e391 100644
--- a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/GetItemOutputTransformInput.java
+++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/GetItemOutputTransformInput.java
@@ -9,8 +9,14 @@
 
 public class GetItemOutputTransformInput {
 
+  /**
+   * <p>Represents the output of a <code>GetItem</code> operation.</p>
+   */
   private final GetItemResponse sdkOutput;
 
+  /**
+   * <p>Represents the input of a <code>GetItem</code> operation.</p>
+   */
   private final GetItemRequest originalInput;
 
   protected GetItemOutputTransformInput(BuilderImpl builder) {
@@ -18,10 +24,16 @@ protected GetItemOutputTransformInput(BuilderImpl builder) {
     this.originalInput = builder.originalInput();
   }
 
+  /**
+   * @return <p>Represents the output of a <code>GetItem</code> operation.</p>
+   */
   public GetItemResponse sdkOutput() {
     return this.sdkOutput;
   }
 
+  /**
+   * @return <p>Represents the input of a <code>GetItem</code> operation.</p>
+   */
   public GetItemRequest originalInput() {
     return this.originalInput;
   }
@@ -35,12 +47,24 @@ public static Builder builder() {
   }
 
   public interface Builder {
+    /**
+     * @param sdkOutput <p>Represents the output of a <code>GetItem</code> operation.</p>
+     */
     Builder sdkOutput(GetItemResponse sdkOutput);
 
+    /**
+     * @return <p>Represents the output of a <code>GetItem</code> operation.</p>
+     */
     GetItemResponse sdkOutput();
 
+    /**
+     * @param originalInput <p>Represents the input of a <code>GetItem</code> operation.</p>
+     */
     Builder originalInput(GetItemRequest originalInput);
 
+    /**
+     * @return <p>Represents the input of a <code>GetItem</code> operation.</p>
+     */
     GetItemRequest originalInput();
 
     GetItemOutputTransformInput build();
diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/GetItemOutputTransformOutput.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/GetItemOutputTransformOutput.java
index 8ebf42a5b..814006edd 100644
--- a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/GetItemOutputTransformOutput.java
+++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/GetItemOutputTransformOutput.java
@@ -8,12 +8,18 @@
 
 public class GetItemOutputTransformOutput {
 
+  /**
+   * <p>Represents the output of a <code>GetItem</code> operation.</p>
+   */
   private final GetItemResponse transformedOutput;
 
   protected GetItemOutputTransformOutput(BuilderImpl builder) {
     this.transformedOutput = builder.transformedOutput();
   }
 
+  /**
+   * @return <p>Represents the output of a <code>GetItem</code> operation.</p>
+   */
   public GetItemResponse transformedOutput() {
     return this.transformedOutput;
   }
@@ -27,8 +33,14 @@ public static Builder builder() {
   }
 
   public interface Builder {
+    /**
+     * @param transformedOutput <p>Represents the output of a <code>GetItem</code> operation.</p>
+     */
     Builder transformedOutput(GetItemResponse transformedOutput);
 
+    /**
+     * @return <p>Represents the output of a <code>GetItem</code> operation.</p>
+     */
     GetItemResponse transformedOutput();
 
     GetItemOutputTransformOutput build();
diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/PutItemInputTransformInput.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/PutItemInputTransformInput.java
index 9bf02f0fe..094c9f629 100644
--- a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/PutItemInputTransformInput.java
+++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/PutItemInputTransformInput.java
@@ -8,12 +8,18 @@
 
 public class PutItemInputTransformInput {
 
+  /**
+   * <p>Represents the input of a <code>PutItem</code> operation.</p>
+   */
   private final PutItemRequest sdkInput;
 
   protected PutItemInputTransformInput(BuilderImpl builder) {
     this.sdkInput = builder.sdkInput();
   }
 
+  /**
+   * @return <p>Represents the input of a <code>PutItem</code> operation.</p>
+   */
   public PutItemRequest sdkInput() {
     return this.sdkInput;
   }
@@ -27,8 +33,14 @@ public static Builder builder() {
   }
 
   public interface Builder {
+    /**
+     * @param sdkInput <p>Represents the input of a <code>PutItem</code> operation.</p>
+     */
     Builder sdkInput(PutItemRequest sdkInput);
 
+    /**
+     * @return <p>Represents the input of a <code>PutItem</code> operation.</p>
+     */
     PutItemRequest sdkInput();
 
     PutItemInputTransformInput build();
diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/PutItemInputTransformOutput.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/PutItemInputTransformOutput.java
index cc06df561..574819d92 100644
--- a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/PutItemInputTransformOutput.java
+++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/PutItemInputTransformOutput.java
@@ -8,12 +8,18 @@
 
 public class PutItemInputTransformOutput {
 
+  /**
+   * <p>Represents the input of a <code>PutItem</code> operation.</p>
+   */
   private final PutItemRequest transformedInput;
 
   protected PutItemInputTransformOutput(BuilderImpl builder) {
     this.transformedInput = builder.transformedInput();
   }
 
+  /**
+   * @return <p>Represents the input of a <code>PutItem</code> operation.</p>
+   */
   public PutItemRequest transformedInput() {
     return this.transformedInput;
   }
@@ -27,8 +33,14 @@ public static Builder builder() {
   }
 
   public interface Builder {
+    /**
+     * @param transformedInput <p>Represents the input of a <code>PutItem</code> operation.</p>
+     */
     Builder transformedInput(PutItemRequest transformedInput);
 
+    /**
+     * @return <p>Represents the input of a <code>PutItem</code> operation.</p>
+     */
     PutItemRequest transformedInput();
 
     PutItemInputTransformOutput build();
diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/PutItemOutputTransformInput.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/PutItemOutputTransformInput.java
index 7e5afed34..a0b58c3f1 100644
--- a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/PutItemOutputTransformInput.java
+++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/PutItemOutputTransformInput.java
@@ -9,8 +9,14 @@
 
 public class PutItemOutputTransformInput {
 
+  /**
+   * <p>Represents the output of a <code>PutItem</code> operation.</p>
+   */
   private final PutItemResponse sdkOutput;
 
+  /**
+   * <p>Represents the input of a <code>PutItem</code> operation.</p>
+   */
   private final PutItemRequest originalInput;
 
   protected PutItemOutputTransformInput(BuilderImpl builder) {
@@ -18,10 +24,16 @@ protected PutItemOutputTransformInput(BuilderImpl builder) {
     this.originalInput = builder.originalInput();
   }
 
+  /**
+   * @return <p>Represents the output of a <code>PutItem</code> operation.</p>
+   */
   public PutItemResponse sdkOutput() {
     return this.sdkOutput;
   }
 
+  /**
+   * @return <p>Represents the input of a <code>PutItem</code> operation.</p>
+   */
   public PutItemRequest originalInput() {
     return this.originalInput;
   }
@@ -35,12 +47,24 @@ public static Builder builder() {
   }
 
   public interface Builder {
+    /**
+     * @param sdkOutput <p>Represents the output of a <code>PutItem</code> operation.</p>
+     */
     Builder sdkOutput(PutItemResponse sdkOutput);
 
+    /**
+     * @return <p>Represents the output of a <code>PutItem</code> operation.</p>
+     */
     PutItemResponse sdkOutput();
 
+    /**
+     * @param originalInput <p>Represents the input of a <code>PutItem</code> operation.</p>
+     */
     Builder originalInput(PutItemRequest originalInput);
 
+    /**
+     * @return <p>Represents the input of a <code>PutItem</code> operation.</p>
+     */
     PutItemRequest originalInput();
 
     PutItemOutputTransformInput build();
diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/PutItemOutputTransformOutput.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/PutItemOutputTransformOutput.java
index deec37efb..8961e2fee 100644
--- a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/PutItemOutputTransformOutput.java
+++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/PutItemOutputTransformOutput.java
@@ -8,12 +8,18 @@
 
 public class PutItemOutputTransformOutput {
 
+  /**
+   * <p>Represents the output of a <code>PutItem</code> operation.</p>
+   */
   private final PutItemResponse transformedOutput;
 
   protected PutItemOutputTransformOutput(BuilderImpl builder) {
     this.transformedOutput = builder.transformedOutput();
   }
 
+  /**
+   * @return <p>Represents the output of a <code>PutItem</code> operation.</p>
+   */
   public PutItemResponse transformedOutput() {
     return this.transformedOutput;
   }
@@ -27,8 +33,14 @@ public static Builder builder() {
   }
 
   public interface Builder {
+    /**
+     * @param transformedOutput <p>Represents the output of a <code>PutItem</code> operation.</p>
+     */
     Builder transformedOutput(PutItemResponse transformedOutput);
 
+    /**
+     * @return <p>Represents the output of a <code>PutItem</code> operation.</p>
+     */
     PutItemResponse transformedOutput();
 
     PutItemOutputTransformOutput build();
diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/QueryInputTransformInput.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/QueryInputTransformInput.java
index fe180f0d0..d1ee2f6e7 100644
--- a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/QueryInputTransformInput.java
+++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/QueryInputTransformInput.java
@@ -8,12 +8,18 @@
 
 public class QueryInputTransformInput {
 
+  /**
+   * <p>Represents the input of a <code>Query</code> operation.</p>
+   */
   private final QueryRequest sdkInput;
 
   protected QueryInputTransformInput(BuilderImpl builder) {
     this.sdkInput = builder.sdkInput();
   }
 
+  /**
+   * @return <p>Represents the input of a <code>Query</code> operation.</p>
+   */
   public QueryRequest sdkInput() {
     return this.sdkInput;
   }
@@ -27,8 +33,14 @@ public static Builder builder() {
   }
 
   public interface Builder {
+    /**
+     * @param sdkInput <p>Represents the input of a <code>Query</code> operation.</p>
+     */
     Builder sdkInput(QueryRequest sdkInput);
 
+    /**
+     * @return <p>Represents the input of a <code>Query</code> operation.</p>
+     */
     QueryRequest sdkInput();
 
     QueryInputTransformInput build();
diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/QueryInputTransformOutput.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/QueryInputTransformOutput.java
index 9d8b0c0b6..a869c8253 100644
--- a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/QueryInputTransformOutput.java
+++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/QueryInputTransformOutput.java
@@ -8,12 +8,18 @@
 
 public class QueryInputTransformOutput {
 
+  /**
+   * <p>Represents the input of a <code>Query</code> operation.</p>
+   */
   private final QueryRequest transformedInput;
 
   protected QueryInputTransformOutput(BuilderImpl builder) {
     this.transformedInput = builder.transformedInput();
   }
 
+  /**
+   * @return <p>Represents the input of a <code>Query</code> operation.</p>
+   */
   public QueryRequest transformedInput() {
     return this.transformedInput;
   }
@@ -27,8 +33,14 @@ public static Builder builder() {
   }
 
   public interface Builder {
+    /**
+     * @param transformedInput <p>Represents the input of a <code>Query</code> operation.</p>
+     */
     Builder transformedInput(QueryRequest transformedInput);
 
+    /**
+     * @return <p>Represents the input of a <code>Query</code> operation.</p>
+     */
     QueryRequest transformedInput();
 
     QueryInputTransformOutput build();
diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/QueryOutputTransformInput.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/QueryOutputTransformInput.java
index c645ff4fa..6b97fde68 100644
--- a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/QueryOutputTransformInput.java
+++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/QueryOutputTransformInput.java
@@ -9,8 +9,14 @@
 
 public class QueryOutputTransformInput {
 
+  /**
+   * <p>Represents the output of a <code>Query</code> operation.</p>
+   */
   private final QueryResponse sdkOutput;
 
+  /**
+   * <p>Represents the input of a <code>Query</code> operation.</p>
+   */
   private final QueryRequest originalInput;
 
   protected QueryOutputTransformInput(BuilderImpl builder) {
@@ -18,10 +24,16 @@ protected QueryOutputTransformInput(BuilderImpl builder) {
     this.originalInput = builder.originalInput();
   }
 
+  /**
+   * @return <p>Represents the output of a <code>Query</code> operation.</p>
+   */
   public QueryResponse sdkOutput() {
     return this.sdkOutput;
   }
 
+  /**
+   * @return <p>Represents the input of a <code>Query</code> operation.</p>
+   */
   public QueryRequest originalInput() {
     return this.originalInput;
   }
@@ -35,12 +47,24 @@ public static Builder builder() {
   }
 
   public interface Builder {
+    /**
+     * @param sdkOutput <p>Represents the output of a <code>Query</code> operation.</p>
+     */
     Builder sdkOutput(QueryResponse sdkOutput);
 
+    /**
+     * @return <p>Represents the output of a <code>Query</code> operation.</p>
+     */
     QueryResponse sdkOutput();
 
+    /**
+     * @param originalInput <p>Represents the input of a <code>Query</code> operation.</p>
+     */
     Builder originalInput(QueryRequest originalInput);
 
+    /**
+     * @return <p>Represents the input of a <code>Query</code> operation.</p>
+     */
     QueryRequest originalInput();
 
     QueryOutputTransformInput build();
diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/QueryOutputTransformOutput.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/QueryOutputTransformOutput.java
index 494b68583..8280489d4 100644
--- a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/QueryOutputTransformOutput.java
+++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/QueryOutputTransformOutput.java
@@ -8,12 +8,18 @@
 
 public class QueryOutputTransformOutput {
 
+  /**
+   * <p>Represents the output of a <code>Query</code> operation.</p>
+   */
   private final QueryResponse transformedOutput;
 
   protected QueryOutputTransformOutput(BuilderImpl builder) {
     this.transformedOutput = builder.transformedOutput();
   }
 
+  /**
+   * @return <p>Represents the output of a <code>Query</code> operation.</p>
+   */
   public QueryResponse transformedOutput() {
     return this.transformedOutput;
   }
@@ -27,8 +33,14 @@ public static Builder builder() {
   }
 
   public interface Builder {
+    /**
+     * @param transformedOutput <p>Represents the output of a <code>Query</code> operation.</p>
+     */
     Builder transformedOutput(QueryResponse transformedOutput);
 
+    /**
+     * @return <p>Represents the output of a <code>Query</code> operation.</p>
+     */
     QueryResponse transformedOutput();
 
     QueryOutputTransformOutput build();
diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/ScanInputTransformInput.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/ScanInputTransformInput.java
index 1c6ce9ae1..95c93a410 100644
--- a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/ScanInputTransformInput.java
+++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/ScanInputTransformInput.java
@@ -8,12 +8,18 @@
 
 public class ScanInputTransformInput {
 
+  /**
+   * <p>Represents the input of a <code>Scan</code> operation.</p>
+   */
   private final ScanRequest sdkInput;
 
   protected ScanInputTransformInput(BuilderImpl builder) {
     this.sdkInput = builder.sdkInput();
   }
 
+  /**
+   * @return <p>Represents the input of a <code>Scan</code> operation.</p>
+   */
   public ScanRequest sdkInput() {
     return this.sdkInput;
   }
@@ -27,8 +33,14 @@ public static Builder builder() {
   }
 
   public interface Builder {
+    /**
+     * @param sdkInput <p>Represents the input of a <code>Scan</code> operation.</p>
+     */
     Builder sdkInput(ScanRequest sdkInput);
 
+    /**
+     * @return <p>Represents the input of a <code>Scan</code> operation.</p>
+     */
     ScanRequest sdkInput();
 
     ScanInputTransformInput build();
diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/ScanInputTransformOutput.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/ScanInputTransformOutput.java
index 295b284a5..bbd53da9a 100644
--- a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/ScanInputTransformOutput.java
+++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/ScanInputTransformOutput.java
@@ -8,12 +8,18 @@
 
 public class ScanInputTransformOutput {
 
+  /**
+   * <p>Represents the input of a <code>Scan</code> operation.</p>
+   */
   private final ScanRequest transformedInput;
 
   protected ScanInputTransformOutput(BuilderImpl builder) {
     this.transformedInput = builder.transformedInput();
   }
 
+  /**
+   * @return <p>Represents the input of a <code>Scan</code> operation.</p>
+   */
   public ScanRequest transformedInput() {
     return this.transformedInput;
   }
@@ -27,8 +33,14 @@ public static Builder builder() {
   }
 
   public interface Builder {
+    /**
+     * @param transformedInput <p>Represents the input of a <code>Scan</code> operation.</p>
+     */
     Builder transformedInput(ScanRequest transformedInput);
 
+    /**
+     * @return <p>Represents the input of a <code>Scan</code> operation.</p>
+     */
     ScanRequest transformedInput();
 
     ScanInputTransformOutput build();
diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/ScanOutputTransformInput.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/ScanOutputTransformInput.java
index f2b693935..41a7149f7 100644
--- a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/ScanOutputTransformInput.java
+++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/ScanOutputTransformInput.java
@@ -9,8 +9,14 @@
 
 public class ScanOutputTransformInput {
 
+  /**
+   * <p>Represents the output of a <code>Scan</code> operation.</p>
+   */
   private final ScanResponse sdkOutput;
 
+  /**
+   * <p>Represents the input of a <code>Scan</code> operation.</p>
+   */
   private final ScanRequest originalInput;
 
   protected ScanOutputTransformInput(BuilderImpl builder) {
@@ -18,10 +24,16 @@ protected ScanOutputTransformInput(BuilderImpl builder) {
     this.originalInput = builder.originalInput();
   }
 
+  /**
+   * @return <p>Represents the output of a <code>Scan</code> operation.</p>
+   */
   public ScanResponse sdkOutput() {
     return this.sdkOutput;
   }
 
+  /**
+   * @return <p>Represents the input of a <code>Scan</code> operation.</p>
+   */
   public ScanRequest originalInput() {
     return this.originalInput;
   }
@@ -35,12 +47,24 @@ public static Builder builder() {
   }
 
   public interface Builder {
+    /**
+     * @param sdkOutput <p>Represents the output of a <code>Scan</code> operation.</p>
+     */
     Builder sdkOutput(ScanResponse sdkOutput);
 
+    /**
+     * @return <p>Represents the output of a <code>Scan</code> operation.</p>
+     */
     ScanResponse sdkOutput();
 
+    /**
+     * @param originalInput <p>Represents the input of a <code>Scan</code> operation.</p>
+     */
     Builder originalInput(ScanRequest originalInput);
 
+    /**
+     * @return <p>Represents the input of a <code>Scan</code> operation.</p>
+     */
     ScanRequest originalInput();
 
     ScanOutputTransformInput build();
diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/ScanOutputTransformOutput.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/ScanOutputTransformOutput.java
index bcf82a72d..33dbb173e 100644
--- a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/ScanOutputTransformOutput.java
+++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/ScanOutputTransformOutput.java
@@ -8,12 +8,18 @@
 
 public class ScanOutputTransformOutput {
 
+  /**
+   * <p>Represents the output of a <code>Scan</code> operation.</p>
+   */
   private final ScanResponse transformedOutput;
 
   protected ScanOutputTransformOutput(BuilderImpl builder) {
     this.transformedOutput = builder.transformedOutput();
   }
 
+  /**
+   * @return <p>Represents the output of a <code>Scan</code> operation.</p>
+   */
   public ScanResponse transformedOutput() {
     return this.transformedOutput;
   }
@@ -27,8 +33,14 @@ public static Builder builder() {
   }
 
   public interface Builder {
+    /**
+     * @param transformedOutput <p>Represents the output of a <code>Scan</code> operation.</p>
+     */
     Builder transformedOutput(ScanResponse transformedOutput);
 
+    /**
+     * @return <p>Represents the output of a <code>Scan</code> operation.</p>
+     */
     ScanResponse transformedOutput();
 
     ScanOutputTransformOutput build();
diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/UpdateItemInputTransformInput.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/UpdateItemInputTransformInput.java
index 8c9a6ffde..056f3cd96 100644
--- a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/UpdateItemInputTransformInput.java
+++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/UpdateItemInputTransformInput.java
@@ -8,12 +8,18 @@
 
 public class UpdateItemInputTransformInput {
 
+  /**
+   * <p>Represents the input of an <code>UpdateItem</code> operation.</p>
+   */
   private final UpdateItemRequest sdkInput;
 
   protected UpdateItemInputTransformInput(BuilderImpl builder) {
     this.sdkInput = builder.sdkInput();
   }
 
+  /**
+   * @return <p>Represents the input of an <code>UpdateItem</code> operation.</p>
+   */
   public UpdateItemRequest sdkInput() {
     return this.sdkInput;
   }
@@ -27,8 +33,14 @@ public static Builder builder() {
   }
 
   public interface Builder {
+    /**
+     * @param sdkInput <p>Represents the input of an <code>UpdateItem</code> operation.</p>
+     */
     Builder sdkInput(UpdateItemRequest sdkInput);
 
+    /**
+     * @return <p>Represents the input of an <code>UpdateItem</code> operation.</p>
+     */
     UpdateItemRequest sdkInput();
 
     UpdateItemInputTransformInput build();
diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/UpdateItemInputTransformOutput.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/UpdateItemInputTransformOutput.java
index 7b9635893..0d45bc38a 100644
--- a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/UpdateItemInputTransformOutput.java
+++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/UpdateItemInputTransformOutput.java
@@ -8,12 +8,18 @@
 
 public class UpdateItemInputTransformOutput {
 
+  /**
+   * <p>Represents the input of an <code>UpdateItem</code> operation.</p>
+   */
   private final UpdateItemRequest transformedInput;
 
   protected UpdateItemInputTransformOutput(BuilderImpl builder) {
     this.transformedInput = builder.transformedInput();
   }
 
+  /**
+   * @return <p>Represents the input of an <code>UpdateItem</code> operation.</p>
+   */
   public UpdateItemRequest transformedInput() {
     return this.transformedInput;
   }
@@ -27,8 +33,14 @@ public static Builder builder() {
   }
 
   public interface Builder {
+    /**
+     * @param transformedInput <p>Represents the input of an <code>UpdateItem</code> operation.</p>
+     */
     Builder transformedInput(UpdateItemRequest transformedInput);
 
+    /**
+     * @return <p>Represents the input of an <code>UpdateItem</code> operation.</p>
+     */
     UpdateItemRequest transformedInput();
 
     UpdateItemInputTransformOutput build();
diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/UpdateItemOutputTransformInput.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/UpdateItemOutputTransformInput.java
index 702b7c5fb..6046efe54 100644
--- a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/UpdateItemOutputTransformInput.java
+++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/UpdateItemOutputTransformInput.java
@@ -9,8 +9,14 @@
 
 public class UpdateItemOutputTransformInput {
 
+  /**
+   * <p>Represents the output of an <code>UpdateItem</code> operation.</p>
+   */
   private final UpdateItemResponse sdkOutput;
 
+  /**
+   * <p>Represents the input of an <code>UpdateItem</code> operation.</p>
+   */
   private final UpdateItemRequest originalInput;
 
   protected UpdateItemOutputTransformInput(BuilderImpl builder) {
@@ -18,10 +24,16 @@ protected UpdateItemOutputTransformInput(BuilderImpl builder) {
     this.originalInput = builder.originalInput();
   }
 
+  /**
+   * @return <p>Represents the output of an <code>UpdateItem</code> operation.</p>
+   */
   public UpdateItemResponse sdkOutput() {
     return this.sdkOutput;
   }
 
+  /**
+   * @return <p>Represents the input of an <code>UpdateItem</code> operation.</p>
+   */
   public UpdateItemRequest originalInput() {
     return this.originalInput;
   }
@@ -35,12 +47,24 @@ public static Builder builder() {
   }
 
   public interface Builder {
+    /**
+     * @param sdkOutput <p>Represents the output of an <code>UpdateItem</code> operation.</p>
+     */
     Builder sdkOutput(UpdateItemResponse sdkOutput);
 
+    /**
+     * @return <p>Represents the output of an <code>UpdateItem</code> operation.</p>
+     */
     UpdateItemResponse sdkOutput();
 
+    /**
+     * @param originalInput <p>Represents the input of an <code>UpdateItem</code> operation.</p>
+     */
     Builder originalInput(UpdateItemRequest originalInput);
 
+    /**
+     * @return <p>Represents the input of an <code>UpdateItem</code> operation.</p>
+     */
     UpdateItemRequest originalInput();
 
     UpdateItemOutputTransformInput build();
diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/UpdateItemOutputTransformOutput.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/UpdateItemOutputTransformOutput.java
index e7a5f5c83..ea8d8d5aa 100644
--- a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/UpdateItemOutputTransformOutput.java
+++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/UpdateItemOutputTransformOutput.java
@@ -8,12 +8,18 @@
 
 public class UpdateItemOutputTransformOutput {
 
+  /**
+   * <p>Represents the output of an <code>UpdateItem</code> operation.</p>
+   */
   private final UpdateItemResponse transformedOutput;
 
   protected UpdateItemOutputTransformOutput(BuilderImpl builder) {
     this.transformedOutput = builder.transformedOutput();
   }
 
+  /**
+   * @return <p>Represents the output of an <code>UpdateItem</code> operation.</p>
+   */
   public UpdateItemResponse transformedOutput() {
     return this.transformedOutput;
   }
@@ -27,8 +33,14 @@ public static Builder builder() {
   }
 
   public interface Builder {
+    /**
+     * @param transformedOutput <p>Represents the output of an <code>UpdateItem</code> operation.</p>
+     */
     Builder transformedOutput(UpdateItemResponse transformedOutput);
 
+    /**
+     * @return <p>Represents the output of an <code>UpdateItem</code> operation.</p>
+     */
     UpdateItemResponse transformedOutput();
 
     UpdateItemOutputTransformOutput build();
diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/structuredencryption/ToDafny.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/structuredencryption/ToDafny.java
index 3ec5e6a19..d3d49d587 100644
--- a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/structuredencryption/ToDafny.java
+++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/structuredencryption/ToDafny.java
@@ -6,6 +6,7 @@
 import Wrappers_Compile.Option;
 import dafny.DafnyMap;
 import dafny.DafnySequence;
+import dafny.TypeDescriptor;
 import java.lang.Byte;
 import java.lang.Character;
 import java.lang.IllegalArgumentException;
@@ -125,11 +126,20 @@ public static DecryptPathStructureInput DecryptPathStructureInput(
       (Objects.nonNull(nativeValue.encryptionContext()) &&
           nativeValue.encryptionContext().size() > 0)
         ? Option.create_Some(
+          DafnyMap._typeDescriptor(
+            DafnySequence._typeDescriptor(TypeDescriptor.BYTE),
+            DafnySequence._typeDescriptor(TypeDescriptor.BYTE)
+          ),
           software.amazon.cryptography.materialproviders.ToDafny.EncryptionContext(
             nativeValue.encryptionContext()
           )
         )
-        : Option.create_None();
+        : Option.create_None(
+          DafnyMap._typeDescriptor(
+            DafnySequence._typeDescriptor(TypeDescriptor.BYTE),
+            DafnySequence._typeDescriptor(TypeDescriptor.BYTE)
+          )
+        );
     return new DecryptPathStructureInput(
       tableName,
       encryptedStructure,
@@ -183,11 +193,20 @@ public static DecryptStructureInput DecryptStructureInput(
       (Objects.nonNull(nativeValue.encryptionContext()) &&
           nativeValue.encryptionContext().size() > 0)
         ? Option.create_Some(
+          DafnyMap._typeDescriptor(
+            DafnySequence._typeDescriptor(TypeDescriptor.BYTE),
+            DafnySequence._typeDescriptor(TypeDescriptor.BYTE)
+          ),
           software.amazon.cryptography.materialproviders.ToDafny.EncryptionContext(
             nativeValue.encryptionContext()
           )
         )
-        : Option.create_None();
+        : Option.create_None(
+          DafnyMap._typeDescriptor(
+            DafnySequence._typeDescriptor(TypeDescriptor.BYTE),
+            DafnySequence._typeDescriptor(TypeDescriptor.BYTE)
+          )
+        );
     return new DecryptStructureInput(
       tableName,
       encryptedStructure,
@@ -239,11 +258,12 @@ public static EncryptPathStructureInput EncryptPathStructureInput(
     algorithmSuiteId =
       Objects.nonNull(nativeValue.algorithmSuiteId())
         ? Option.create_Some(
+          DBEAlgorithmSuiteId._typeDescriptor(),
           software.amazon.cryptography.materialproviders.ToDafny.DBEAlgorithmSuiteId(
             nativeValue.algorithmSuiteId()
           )
         )
-        : Option.create_None();
+        : Option.create_None(DBEAlgorithmSuiteId._typeDescriptor());
     Option<
       DafnyMap<
         ? extends DafnySequence<? extends Byte>,
@@ -254,11 +274,20 @@ public static EncryptPathStructureInput EncryptPathStructureInput(
       (Objects.nonNull(nativeValue.encryptionContext()) &&
           nativeValue.encryptionContext().size() > 0)
         ? Option.create_Some(
+          DafnyMap._typeDescriptor(
+            DafnySequence._typeDescriptor(TypeDescriptor.BYTE),
+            DafnySequence._typeDescriptor(TypeDescriptor.BYTE)
+          ),
           software.amazon.cryptography.materialproviders.ToDafny.EncryptionContext(
             nativeValue.encryptionContext()
           )
         )
-        : Option.create_None();
+        : Option.create_None(
+          DafnyMap._typeDescriptor(
+            DafnySequence._typeDescriptor(TypeDescriptor.BYTE),
+            DafnySequence._typeDescriptor(TypeDescriptor.BYTE)
+          )
+        );
     return new EncryptPathStructureInput(
       tableName,
       plaintextStructure,
@@ -306,11 +335,12 @@ public static EncryptStructureInput EncryptStructureInput(
     algorithmSuiteId =
       Objects.nonNull(nativeValue.algorithmSuiteId())
         ? Option.create_Some(
+          DBEAlgorithmSuiteId._typeDescriptor(),
           software.amazon.cryptography.materialproviders.ToDafny.DBEAlgorithmSuiteId(
             nativeValue.algorithmSuiteId()
           )
         )
-        : Option.create_None();
+        : Option.create_None(DBEAlgorithmSuiteId._typeDescriptor());
     Option<
       DafnyMap<
         ? extends DafnySequence<? extends Byte>,
@@ -321,11 +351,20 @@ public static EncryptStructureInput EncryptStructureInput(
       (Objects.nonNull(nativeValue.encryptionContext()) &&
           nativeValue.encryptionContext().size() > 0)
         ? Option.create_Some(
+          DafnyMap._typeDescriptor(
+            DafnySequence._typeDescriptor(TypeDescriptor.BYTE),
+            DafnySequence._typeDescriptor(TypeDescriptor.BYTE)
+          ),
           software.amazon.cryptography.materialproviders.ToDafny.EncryptionContext(
             nativeValue.encryptionContext()
           )
         )
-        : Option.create_None();
+        : Option.create_None(
+          DafnyMap._typeDescriptor(
+            DafnySequence._typeDescriptor(TypeDescriptor.BYTE),
+            DafnySequence._typeDescriptor(TypeDescriptor.BYTE)
+          )
+        );
     return new EncryptStructureInput(
       tableName,
       plaintextStructure,
diff --git a/SharedMakefile.mk b/SharedMakefile.mk
index d93ba5857..37f18d5f6 100644
--- a/SharedMakefile.mk
+++ b/SharedMakefile.mk
@@ -12,3 +12,14 @@ GRADLEW := ./runtimes/java/gradlew
 include $(SMITHY_DAFNY_ROOT)/SmithyDafnyMakefile.mk
 
 VERIFY_TIMEOUT := 250
+
+verify:DAFNY_OPTIONS=--allow-warnings --allow-external-contracts --log-format csv
+verify_single:DAFNY_OPTIONS=--allow-warnings --allow-external-contracts --log-format csv
+verify_service:DAFNY_OPTIONS=--allow-warnings --allow-external-contracts --log-format csv
+
+transpile_implementation_net: DAFNY_OPTIONS=--allow-warnings --compile-suffix --legacy-module-names --allow-external-contracts
+transpile_test_net: DAFNY_OPTIONS=--allow-warnings --include-test-runner --compile-suffix --legacy-module-names --allow-external-contracts
+
+transpile_implementation_java: DAFNY_OPTIONS=--allow-warnings --compile-suffix --legacy-data-constructors --legacy-module-names --allow-external-contracts
+transpile_test_java: DAFNY_OPTIONS=--allow-warnings --include-test-runner --compile-suffix --legacy-data-constructors --legacy-module-names --allow-external-contracts
+
diff --git a/TestVectors/project.properties b/TestVectors/project.properties
new file mode 100644
index 000000000..02e193a7d
--- /dev/null
+++ b/TestVectors/project.properties
@@ -0,0 +1,4 @@
+# This file stores the top level dafny version information.
+# All elements of the project need to agree on this version.
+dafnyVersion=4.8.0
+dafnyRuntimeJavaVersion=4.8.0
diff --git a/TestVectors/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/wrapped/TestDynamoDbEncryption.java b/TestVectors/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/wrapped/TestDynamoDbEncryption.java
index acf30bd1e..d9df0b96e 100644
--- a/TestVectors/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/wrapped/TestDynamoDbEncryption.java
+++ b/TestVectors/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/wrapped/TestDynamoDbEncryption.java
@@ -42,9 +42,17 @@ > CreateDynamoDbEncryptionBranchKeyIdSupplier(
         this._impl.CreateDynamoDbEncryptionBranchKeyIdSupplier(nativeInput);
       CreateDynamoDbEncryptionBranchKeyIdSupplierOutput dafnyOutput =
         ToDafny.CreateDynamoDbEncryptionBranchKeyIdSupplierOutput(nativeOutput);
-      return Result.create_Success(dafnyOutput);
+      return Result.create_Success(
+        CreateDynamoDbEncryptionBranchKeyIdSupplierOutput._typeDescriptor(),
+        Error._typeDescriptor(),
+        dafnyOutput
+      );
     } catch (RuntimeException ex) {
-      return Result.create_Failure(ToDafny.Error(ex));
+      return Result.create_Failure(
+        CreateDynamoDbEncryptionBranchKeyIdSupplierOutput._typeDescriptor(),
+        Error._typeDescriptor(),
+        ToDafny.Error(ex)
+      );
     }
   }
 
@@ -61,9 +69,17 @@ > GetEncryptedDataKeyDescription(
         this._impl.GetEncryptedDataKeyDescription(nativeInput);
       GetEncryptedDataKeyDescriptionOutput dafnyOutput =
         ToDafny.GetEncryptedDataKeyDescriptionOutput(nativeOutput);
-      return Result.create_Success(dafnyOutput);
+      return Result.create_Success(
+        GetEncryptedDataKeyDescriptionOutput._typeDescriptor(),
+        Error._typeDescriptor(),
+        dafnyOutput
+      );
     } catch (RuntimeException ex) {
-      return Result.create_Failure(ToDafny.Error(ex));
+      return Result.create_Failure(
+        GetEncryptedDataKeyDescriptionOutput._typeDescriptor(),
+        Error._typeDescriptor(),
+        ToDafny.Error(ex)
+      );
     }
   }
 
diff --git a/TestVectors/runtimes/net/Generated/DDBEncryption/TypeConversion.cs b/TestVectors/runtimes/net/Generated/DDBEncryption/TypeConversion.cs
index 6a0902fa9..d517f861e 100644
--- a/TestVectors/runtimes/net/Generated/DDBEncryption/TypeConversion.cs
+++ b/TestVectors/runtimes/net/Generated/DDBEncryption/TypeConversion.cs
@@ -7,6 +7,10 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb.Wrapped
 {
     public static class TypeConversion
     {
+        private const string ISO8601DateFormat = "yyyy-MM-dd\\THH:mm:ss.fff\\Z";
+
+        private const string ISO8601DateFormatNoMS = "yyyy-MM-dd\\THH:mm:ss\\Z";
+
         public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.BeaconKeySource FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S15_BeaconKeySource(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IBeaconKeySource value)
         {
             software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.BeaconKeySource concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.BeaconKeySource)value;
diff --git a/project.properties b/project.properties
index 1a4050afc..4f9d620ce 100644
--- a/project.properties
+++ b/project.properties
@@ -1,6 +1,6 @@
 projectJavaVersion=3.6.2-SNAPSHOT
-mplDependencyJavaVersion=1.5.1
-dafnyVersion=4.2.0
-dafnyVerifyVersion=4.7.0
-dafnyRuntimeJavaVersion=4.2.0
+mplDependencyJavaVersion=1.6.0
+dafnyVersion=4.8.0
+dafnyVerifyVersion=4.8.0
+dafnyRuntimeJavaVersion=4.8.0
 smithyDafnyJavaConversionVersion=0.1
diff --git a/submodules/MaterialProviders b/submodules/MaterialProviders
index cdd4885cb..66a04bf31 160000
--- a/submodules/MaterialProviders
+++ b/submodules/MaterialProviders
@@ -1 +1 @@
-Subproject commit cdd4885cb22957b04167b11d8b40edbdf4301d8d
+Subproject commit 66a04bf31bcfd8fd514acea740d8e670ab565ed9
diff --git a/submodules/smithy-dafny b/submodules/smithy-dafny
index d9c596cb8..98939e130 160000
--- a/submodules/smithy-dafny
+++ b/submodules/smithy-dafny
@@ -1 +1 @@
-Subproject commit d9c596cb85ce55434efb57a5f88e6dd7fb68d505
+Subproject commit 98939e130695095386059967509a19299dfac320