diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/DynamoDbEncryption.smithy b/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/DynamoDbEncryption.smithy
index b4fa422a0..64b4c82ac 100644
--- a/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/DynamoDbEncryption.smithy
+++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/DynamoDbEncryption.smithy
@@ -873,7 +873,6 @@ structure CreateDynamoDbEncryptionBranchKeyIdSupplierOutput {
   branchKeyIdSupplier: BranchKeyIdSupplierReference 
 }
 
-/////////////
 // Errors
 
 @error("client")
diff --git a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/Model/DynamoDbItemEncryptor.smithy b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/Model/DynamoDbItemEncryptor.smithy
index d128547b4..ae11f9361 100644
--- a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/Model/DynamoDbItemEncryptor.smithy
+++ b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/Model/DynamoDbItemEncryptor.smithy
@@ -224,7 +224,6 @@ structure AtomicPrimitivesReference {}
 @aws.polymorph#reference(service: aws.cryptography.dbEncryptionSdk.structuredEncryption#StructuredEncryption)
 structure StructuredEncryptionReference {}
 
-/////////////
 // Errors
 
 @error("client")
diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/Model/StructuredEncryption.smithy b/DynamoDbEncryption/dafny/StructuredEncryption/Model/StructuredEncryption.smithy
index c44a6bc00..a8e2fff5d 100644
--- a/DynamoDbEncryption/dafny/StructuredEncryption/Model/StructuredEncryption.smithy
+++ b/DynamoDbEncryption/dafny/StructuredEncryption/Model/StructuredEncryption.smithy
@@ -405,7 +405,6 @@ list AuthList {
 @aws.polymorph#reference(service: aws.cryptography.primitives#AwsCryptographicPrimitives)
 structure AtomicPrimitivesReference {}
 
-/////////////
 // Errors
 
 @error("client")
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/DynamoDbEncryption/runtimes/net/ImplementationFromDafny-cs.dtr b/DynamoDbEncryption/runtimes/net/ImplementationFromDafny-cs.dtr
new file mode 100644
index 000000000..2e5553f2e
--- /dev/null
+++ b/DynamoDbEncryption/runtimes/net/ImplementationFromDafny-cs.dtr
@@ -0,0 +1,63 @@
+file_format_version = "1.0"
+dafny_version = "4.7.0.0"
+[options_by_module.AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes]
+[options_by_module.AbstractAwsCryptographyDbEncryptionSdkStructuredEncryptionOperations]
+[options_by_module.AbstractAwsCryptographyDbEncryptionSdkStructuredEncryptionService]
+[options_by_module.StructuredEncryptionUtil]
+[options_by_module.Sets]
+[options_by_module.StructuredEncryptionPaths]
+[options_by_module.StructuredEncryptionHeader]
+[options_by_module.StructuredEncryptionFooter]
+[options_by_module.SortCanon]
+[options_by_module.Canonize]
+[options_by_module.StructuredEncryptionCrypt]
+[options_by_module.Maps]
+[options_by_module.AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations]
+[options_by_module.StructuredEncryption]
+[options_by_module.AwsCryptographyDbEncryptionSdkDynamoDbTypes]
+[options_by_module.AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes]
+[options_by_module.AbstractAwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations]
+[options_by_module.AbstractAwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorService]
+[options_by_module.DynamoDbEncryptionUtil]
+[options_by_module.DynamoDbNormalizeNumber]
+[options_by_module.DynamoToStruct]
+[options_by_module.DynamoDbItemEncryptorUtil]
+[options_by_module.InternalLegacyOverride]
+[options_by_module.AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations]
+[options_by_module.DynamoDbItemEncryptor]
+[options_by_module.AbstractAwsCryptographyDbEncryptionSdkDynamoDbOperations]
+[options_by_module.AbstractAwsCryptographyDbEncryptionSdkDynamoDbService]
+[options_by_module.DynamoDbEncryptionBranchKeyIdSupplier]
+[options_by_module.AwsCryptographyDbEncryptionSdkDynamoDbOperations]
+[options_by_module.DynamoDbEncryption]
+[options_by_module.TermLoc]
+[options_by_module.DdbVirtualFields]
+[options_by_module.DynamoDbUpdateExpr]
+[options_by_module.BaseBeacon]
+[options_by_module.CompoundBeacon]
+[options_by_module.SearchableEncryptionInfo]
+[options_by_module.DynamoDBFilterExpr]
+[options_by_module.DynamoDBSupport]
+[options_by_module.SearchConfigToInfo]
+[options_by_module.AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes]
+[options_by_module.AbstractAwsCryptographyDbEncryptionSdkDynamoDbTransformsOperations]
+[options_by_module.AbstractAwsCryptographyDbEncryptionSdkDynamoDbTransformsService]
+[options_by_module.DdbMiddlewareConfig]
+[options_by_module.DdbStatement]
+[options_by_module.DynamoDbMiddlewareSupport]
+[options_by_module.PutItemTransform]
+[options_by_module.GetItemTransform]
+[options_by_module.UpdateItemTransform]
+[options_by_module.BatchWriteItemTransform]
+[options_by_module.TransactWriteItemsTransform]
+[options_by_module.BatchGetItemTransform]
+[options_by_module.ScanTransform]
+[options_by_module.QueryTransform]
+[options_by_module.TransactGetItemsTransform]
+[options_by_module.DeleteItemTransform]
+[options_by_module.ExecuteStatementTransform]
+[options_by_module.BatchExecuteStatementTransform]
+[options_by_module.ExecuteTransactionTransform]
+[options_by_module.AttributeResolver]
+[options_by_module.AwsCryptographyDbEncryptionSdkDynamoDbTransformsOperations]
+[options_by_module.DynamoDbEncryptionTransforms]
diff --git a/DynamoDbEncryption/runtimes/net/tests/TestsFromDafny-cs.dtr b/DynamoDbEncryption/runtimes/net/tests/TestsFromDafny-cs.dtr
new file mode 100644
index 000000000..13f4d0690
--- /dev/null
+++ b/DynamoDbEncryption/runtimes/net/tests/TestsFromDafny-cs.dtr
@@ -0,0 +1,34 @@
+file_format_version = "1.0"
+dafny_version = "4.7.0.0"
+[options_by_module.StructuredDataTestFixtures]
+[options_by_module.HappyCaseTests]
+[options_by_module.PathsTests]
+[options_by_module.TestHeader]
+[options_by_module.TestStructuredEncryptionCrypt]
+[options_by_module.TestFixtures]
+[options_by_module.DynamoDbItemEncryptorTest]
+[options_by_module.GetItemTransformTest]
+[options_by_module.DdbStatementTest]
+[options_by_module.ExecuteTransactionTransformTest]
+[options_by_module.BatchWriteItemTransformTest]
+[options_by_module.TransactGetItemsTransformTest]
+[options_by_module.BatchExecuteStatementTransformTest]
+[options_by_module.BatchGetItemTransformTest]
+[options_by_module.ScanTransformTest]
+[options_by_module.UpdateItemTransformTest]
+[options_by_module.ExecuteStatementTransformTest]
+[options_by_module.TransactWriteItemsTransformTest]
+[options_by_module.PutItemTransformTest]
+[options_by_module.DeleteItemTransformTest]
+[options_by_module.QueryTransformTest]
+[options_by_module.BeaconTestFixtures]
+[options_by_module.TestDynamoDBFilterExpr]
+[options_by_module.TestBaseBeacon]
+[options_by_module.DynamoToStructTest]
+[options_by_module.TestUpdateExpr]
+[options_by_module.TestDdbVirtualFields]
+[options_by_module.TestDynamoDBConfigToInfo]
+[options_by_module.TestDDBSupport]
+[options_by_module.TestNormalizeNumber]
+[options_by_module.DynamoDbEncryptionBranchKeyIdSupplierTest]
+[options_by_module.DynamoDbGetEncryptedDataKeyDescriptionTest]
diff --git a/TestVectors/project.properties b/TestVectors/project.properties
new file mode 100644
index 000000000..a80e08198
--- /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.7.0
+dafnyRuntimeJavaVersion=4.7.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/project.properties b/project.properties
index 479454a16..7d5cccab7 100644
--- a/project.properties
+++ b/project.properties
@@ -1,6 +1,6 @@
 projectJavaVersion=3.5.0-SNAPSHOT
-mplDependencyJavaVersion=1.5.1
-dafnyVersion=4.2.0
+mplDependencyJavaVersion=1.5.1-SNAPSHOT
+dafnyVersion=4.7.0
 dafnyVerifyVersion=4.7.0
-dafnyRuntimeJavaVersion=4.2.0
+dafnyRuntimeJavaVersion=4.7.0
 smithyDafnyJavaConversionVersion=0.1
diff --git a/submodules/MaterialProviders b/submodules/MaterialProviders
index cdd4885cb..8a732bdc7 160000
--- a/submodules/MaterialProviders
+++ b/submodules/MaterialProviders
@@ -1 +1 @@
-Subproject commit cdd4885cb22957b04167b11d8b40edbdf4301d8d
+Subproject commit 8a732bdc71942bf77050bf9b4d2440d41176506d
diff --git a/submodules/smithy-dafny b/submodules/smithy-dafny
index d9c596cb8..a0fd2c595 160000
--- a/submodules/smithy-dafny
+++ b/submodules/smithy-dafny
@@ -1 +1 @@
-Subproject commit d9c596cb85ce55434efb57a5f88e6dd7fb68d505
+Subproject commit a0fd2c595fe7d16f0a18a7bbdcb056bdcb695192