From ecf1b5bc60fcba8cb7b6222c1da0b230c237d566 Mon Sep 17 00:00:00 2001
From: Jose Corella <jocorell@amazon.com>
Date: Thu, 19 Mar 2026 14:45:10 -0700
Subject: [PATCH 01/13] chore: upadte mpl

---
 submodules/MaterialProviders | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/submodules/MaterialProviders b/submodules/MaterialProviders
index 734c1a31fc..e6bdbae3b5 160000
--- a/submodules/MaterialProviders
+++ b/submodules/MaterialProviders
@@ -1 +1 @@
-Subproject commit 734c1a31fc4521dc0653433565d5d6171e61d1ac
+Subproject commit e6bdbae3b57ba227434f196b80d8c26e5baaaf4f

From ae475470229e2483ef4f13709d8b0e54f60f062f Mon Sep 17 00:00:00 2001
From: Jose Corella <jocorell@amazon.com>
Date: Thu, 19 Mar 2026 16:04:27 -0700
Subject: [PATCH 02/13] update patch files

---
 .../dotnet/dafny-4.9.0.patch                  | 23 +++++++++++++++----
 .../dotnet/dafny-4.9.0.patch                  | 23 +++++++++++++++----
 .../dotnet/dafny-4.9.0.patch                  | 23 +++++++++++++++----
 .../runtimes/net/DynamoDbEncryption.csproj    |  3 ---
 .../DynamoDbEncryption/TypeConversion.cs      |  6 ++---
 .../TypeConversion.cs                         |  6 ++---
 .../DynamoDbItemEncryptor/TypeConversion.cs   |  6 ++---
 Examples/runtimes/net/Examples.csproj         |  2 +-
 8 files changed, 67 insertions(+), 25 deletions(-)

diff --git a/DynamoDbEncryption/codegen-patches/DynamoDbEncryption/dotnet/dafny-4.9.0.patch b/DynamoDbEncryption/codegen-patches/DynamoDbEncryption/dotnet/dafny-4.9.0.patch
index 31f95b6309..a33e07381e 100644
--- a/DynamoDbEncryption/codegen-patches/DynamoDbEncryption/dotnet/dafny-4.9.0.patch
+++ b/DynamoDbEncryption/codegen-patches/DynamoDbEncryption/dotnet/dafny-4.9.0.patch
@@ -1,7 +1,7 @@
-diff --git b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs
-index 82bbffe6a..87ae5c0e9 100644
---- b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs
-+++ a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs
+diff --git a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs
+index 82bbffe6..708467da 100644
+--- a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs
++++ b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs
 @@ -7,10 +7,6 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb
  {
    public static class TypeConversion
@@ -13,3 +13,18 @@ index 82bbffe6a..87ae5c0e9 100644
      public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.AsSet FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S5_AsSet(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IAsSet value)
      {
        software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.AsSet concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.AsSet)value; AWS.Cryptography.DbEncryptionSDK.DynamoDb.AsSet converted = new AWS.Cryptography.DbEncryptionSDK.DynamoDb.AsSet(); return converted;
+@@ -2258,11 +2254,11 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb
+       }
+       if (value.NULL == true)
+       {
+-        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL(value.NULL));
++        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL((bool)value.NULL));
+       }
+-      if (value.IsBOOLSet)
++      if (value.BOOL != null)
+       {
+-        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL(value.BOOL));
++        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL((bool)value.BOOL));
+       }
+       throw new System.ArgumentException("Invalid Amazon.DynamoDBv2.Model.AttributeValue state");
+     }
diff --git a/DynamoDbEncryption/codegen-patches/DynamoDbEncryptionTransforms/dotnet/dafny-4.9.0.patch b/DynamoDbEncryption/codegen-patches/DynamoDbEncryptionTransforms/dotnet/dafny-4.9.0.patch
index 97fcc23806..76383851bb 100644
--- a/DynamoDbEncryption/codegen-patches/DynamoDbEncryptionTransforms/dotnet/dafny-4.9.0.patch
+++ b/DynamoDbEncryption/codegen-patches/DynamoDbEncryptionTransforms/dotnet/dafny-4.9.0.patch
@@ -1,7 +1,7 @@
-diff --git b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs
-index 08aa59190..fa42225e6 100644
---- b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs
-+++ a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs
+diff --git a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs
+index 08aa5919..02ad044e 100644
+--- a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs
++++ b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs
 @@ -7,10 +7,6 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb.Transforms
  {
    public static class TypeConversion
@@ -13,3 +13,18 @@ index 08aa59190..fa42225e6 100644
      public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.AsSet FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S5_AsSet(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IAsSet value)
      {
        software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.AsSet concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.AsSet)value; AWS.Cryptography.DbEncryptionSDK.DynamoDb.AsSet converted = new AWS.Cryptography.DbEncryptionSDK.DynamoDb.AsSet(); return converted;
+@@ -3222,11 +3218,11 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb.Transforms
+       }
+       if (value.NULL == true)
+       {
+-        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL(value.NULL));
++        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL((bool)value.NULL));
+       }
+-      if (value.IsBOOLSet)
++      if (value.BOOL != null)
+       {
+-        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL(value.BOOL));
++        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL((bool)value.BOOL));
+       }
+       throw new System.ArgumentException("Invalid Amazon.DynamoDBv2.Model.AttributeValue state");
+     }
diff --git a/DynamoDbEncryption/codegen-patches/DynamoDbItemEncryptor/dotnet/dafny-4.9.0.patch b/DynamoDbEncryption/codegen-patches/DynamoDbItemEncryptor/dotnet/dafny-4.9.0.patch
index bfffccb499..ffc431be09 100644
--- a/DynamoDbEncryption/codegen-patches/DynamoDbItemEncryptor/dotnet/dafny-4.9.0.patch
+++ b/DynamoDbEncryption/codegen-patches/DynamoDbItemEncryptor/dotnet/dafny-4.9.0.patch
@@ -1,7 +1,7 @@
-diff --git b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs
-index b4a90d1b4..b5d5046a4 100644
---- b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs
-+++ a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs
+diff --git a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs
+index b4a90d1b..004fe3ed 100644
+--- a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs
++++ b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs
 @@ -7,10 +7,6 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor
  {
    public static class TypeConversion
@@ -13,3 +13,18 @@ index b4a90d1b4..b5d5046a4 100644
      public static System.Collections.Generic.Dictionary<string, AWS.Cryptography.DbEncryptionSDK.StructuredEncryption.CryptoAction> FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S16_AttributeActions(Dafny.IMap<Dafny.ISequence<char>, software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny.types._ICryptoAction> value)
      {
        return value.ItemEnumerable.ToDictionary(pair => FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S16_AttributeActions__M3_key(pair.Car), pair => FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S16_AttributeActions__M5_value(pair.Cdr));
+@@ -724,11 +720,11 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor
+       }
+       if (value.NULL == true)
+       {
+-        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL(value.NULL));
++        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL((bool)value.NULL));
+       }
+-      if (value.IsBOOLSet)
++      if (value.BOOL != null)
+       {
+-        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL(value.BOOL));
++        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL((bool)value.BOOL));
+       }
+       throw new System.ArgumentException("Invalid Amazon.DynamoDBv2.Model.AttributeValue state");
+     }
diff --git a/DynamoDbEncryption/runtimes/net/DynamoDbEncryption.csproj b/DynamoDbEncryption/runtimes/net/DynamoDbEncryption.csproj
index bddba56f62..1b5db20bc1 100644
--- a/DynamoDbEncryption/runtimes/net/DynamoDbEncryption.csproj
+++ b/DynamoDbEncryption/runtimes/net/DynamoDbEncryption.csproj
@@ -58,9 +58,6 @@
 
   <ItemGroup>
     <PackageReference Include="DafnyRuntime" Version="$(DafnyVersion)" />
-    <!-- See https://learn.microsoft.com/en-us/nuget/concepts/package-versioning?tabs=semver20sort#version-ranges   -->
-    <PackageReference Include="AWSSDK.Core" Version="[3.7.*, 4.0)" />
-    <PackageReference Include="AWSSDK.DynamoDBv2" Version="[3.7.*, 4.0)" />
     <!-- Before releasing a new DBESDK version ensure to pin the MPL -->
     <ProjectReference Include="../../../submodules/MaterialProviders/AwsCryptographicMaterialProviders/runtimes/net/MPL.csproj"/>
     <!--
diff --git a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs
index 87ae5c0e95..708467da12 100644
--- a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs
+++ b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs
@@ -2254,11 +2254,11 @@ public static software.amazon.cryptography.services.dynamodb.internaldafny.types
       }
       if (value.NULL == true)
       {
-        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL(value.NULL));
+        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL((bool)value.NULL));
       }
-      if (value.IsBOOLSet)
+      if (value.BOOL != null)
       {
-        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL(value.BOOL));
+        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL((bool)value.BOOL));
       }
       throw new System.ArgumentException("Invalid Amazon.DynamoDBv2.Model.AttributeValue state");
     }
diff --git a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs
index fa42225e63..02ad044e52 100644
--- a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs
+++ b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs
@@ -3218,11 +3218,11 @@ public static software.amazon.cryptography.services.dynamodb.internaldafny.types
       }
       if (value.NULL == true)
       {
-        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL(value.NULL));
+        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL((bool)value.NULL));
       }
-      if (value.IsBOOLSet)
+      if (value.BOOL != null)
       {
-        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL(value.BOOL));
+        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL((bool)value.BOOL));
       }
       throw new System.ArgumentException("Invalid Amazon.DynamoDBv2.Model.AttributeValue state");
     }
diff --git a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs
index b5d5046a47..004fe3ed1a 100644
--- a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs
+++ b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs
@@ -720,11 +720,11 @@ public static software.amazon.cryptography.services.dynamodb.internaldafny.types
       }
       if (value.NULL == true)
       {
-        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL(value.NULL));
+        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL((bool)value.NULL));
       }
-      if (value.IsBOOLSet)
+      if (value.BOOL != null)
       {
-        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL(value.BOOL));
+        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL((bool)value.BOOL));
       }
       throw new System.ArgumentException("Invalid Amazon.DynamoDBv2.Model.AttributeValue state");
     }
diff --git a/Examples/runtimes/net/Examples.csproj b/Examples/runtimes/net/Examples.csproj
index f57bdb388b..98be03fbf1 100644
--- a/Examples/runtimes/net/Examples.csproj
+++ b/Examples/runtimes/net/Examples.csproj
@@ -10,7 +10,7 @@
 
   <ItemGroup>
     <ProjectReference Include="../../../DynamoDbEncryption/runtimes/net/DynamoDbEncryption.csproj" />
-    <PackageReference Include="AWSSDK.SecurityToken" Version="3.7.202.5"/>
+    <PackageReference Include="AWSSDK.SecurityToken" Version="4.*"/>
     <PackageReference Include="xunit" Version="2.4.0" />
     <PackageReference Include="xunit.runner.visualstudio" Version="2.4.0" />
     <PackageReference Include="Microsoft.NET.Test.Sdk" Version="16.11.0" />

From 125f55895309fb46bc5dd607f1b0dfb1de6eb047 Mon Sep 17 00:00:00 2001
From: Jose Corella <jocorell@amazon.com>
Date: Fri, 20 Mar 2026 11:34:52 -0700
Subject: [PATCH 03/13] test vector patches

---
 TestVectors/Makefile                          |  2 ++
 .../DDBEncryption/dotnet/dafny-4.9.0.patch    | 19 +++++++++++++++++++
 .../dotnet/dafny-4.9.0.patch                  | 19 +++++++++++++++++++
 .../Generated/DDBEncryption/TypeConversion.cs |  6 +++---
 .../TypeConversion.cs                         |  6 +++---
 5 files changed, 46 insertions(+), 6 deletions(-)
 create mode 100644 TestVectors/codegen-patches/DDBEncryption/dotnet/dafny-4.9.0.patch
 create mode 100644 TestVectors/codegen-patches/WrappedDynamoDbItemEncryptor/dotnet/dafny-4.9.0.patch

diff --git a/TestVectors/Makefile b/TestVectors/Makefile
index 9a65a42094..5fe3c632a9 100644
--- a/TestVectors/Makefile
+++ b/TestVectors/Makefile
@@ -7,6 +7,8 @@ TRANSPILE_TESTS_IN_RUST=1
 
 include ../SharedMakefile.mk
 
+DIR_STRUCTURE_V2=V2
+
 PROJECT_SERVICES := \
 	DDBEncryption \
 	WrappedDynamoDbItemEncryptor
diff --git a/TestVectors/codegen-patches/DDBEncryption/dotnet/dafny-4.9.0.patch b/TestVectors/codegen-patches/DDBEncryption/dotnet/dafny-4.9.0.patch
new file mode 100644
index 0000000000..bc63e8c02c
--- /dev/null
+++ b/TestVectors/codegen-patches/DDBEncryption/dotnet/dafny-4.9.0.patch
@@ -0,0 +1,19 @@
+diff --git a/TestVectors/runtimes/net/Generated/DDBEncryption/TypeConversion.cs b/TestVectors/runtimes/net/Generated/DDBEncryption/TypeConversion.cs
+index 1ff2d1b4..5e46a9aa 100644
+--- a/TestVectors/runtimes/net/Generated/DDBEncryption/TypeConversion.cs
++++ b/TestVectors/runtimes/net/Generated/DDBEncryption/TypeConversion.cs
+@@ -2236,11 +2236,11 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb.Wrapped
+             }
+             if (value.NULL == true)
+             {
+-                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL(value.NULL));
++                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL((bool)value.NULL));
+             }
+-            if (value.IsBOOLSet)
++            if (value.BOOL != null)
+             {
+-                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL(value.BOOL));
++                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL((bool)value.BOOL));
+             }
+             throw new System.ArgumentException("Invalid Amazon.DynamoDBv2.Model.AttributeValue state");
+         }
diff --git a/TestVectors/codegen-patches/WrappedDynamoDbItemEncryptor/dotnet/dafny-4.9.0.patch b/TestVectors/codegen-patches/WrappedDynamoDbItemEncryptor/dotnet/dafny-4.9.0.patch
new file mode 100644
index 0000000000..321f0b1032
--- /dev/null
+++ b/TestVectors/codegen-patches/WrappedDynamoDbItemEncryptor/dotnet/dafny-4.9.0.patch
@@ -0,0 +1,19 @@
+diff --git a/TestVectors/runtimes/net/Generated/WrappedDynamoDbItemEncryptor/TypeConversion.cs b/TestVectors/runtimes/net/Generated/WrappedDynamoDbItemEncryptor/TypeConversion.cs
+index dc216416..f4ffbb58 100644
+--- a/TestVectors/runtimes/net/Generated/WrappedDynamoDbItemEncryptor/TypeConversion.cs
++++ b/TestVectors/runtimes/net/Generated/WrappedDynamoDbItemEncryptor/TypeConversion.cs
+@@ -716,11 +716,11 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.Wrapped
+             }
+             if (value.NULL == true)
+             {
+-                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL(value.NULL));
++                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL((bool)value.NULL));
+             }
+-            if (value.IsBOOLSet)
++            if (value.BOOL != null)
+             {
+-                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL(value.BOOL));
++                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL((bool)value.BOOL));
+             }
+             throw new System.ArgumentException("Invalid Amazon.DynamoDBv2.Model.AttributeValue state");
+         }
diff --git a/TestVectors/runtimes/net/Generated/DDBEncryption/TypeConversion.cs b/TestVectors/runtimes/net/Generated/DDBEncryption/TypeConversion.cs
index 1ff2d1b401..5e46a9aa1b 100644
--- a/TestVectors/runtimes/net/Generated/DDBEncryption/TypeConversion.cs
+++ b/TestVectors/runtimes/net/Generated/DDBEncryption/TypeConversion.cs
@@ -2236,11 +2236,11 @@ public static software.amazon.cryptography.services.dynamodb.internaldafny.types
             }
             if (value.NULL == true)
             {
-                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL(value.NULL));
+                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL((bool)value.NULL));
             }
-            if (value.IsBOOLSet)
+            if (value.BOOL != null)
             {
-                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL(value.BOOL));
+                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL((bool)value.BOOL));
             }
             throw new System.ArgumentException("Invalid Amazon.DynamoDBv2.Model.AttributeValue state");
         }
diff --git a/TestVectors/runtimes/net/Generated/WrappedDynamoDbItemEncryptor/TypeConversion.cs b/TestVectors/runtimes/net/Generated/WrappedDynamoDbItemEncryptor/TypeConversion.cs
index dc216416e2..f4ffbb586d 100644
--- a/TestVectors/runtimes/net/Generated/WrappedDynamoDbItemEncryptor/TypeConversion.cs
+++ b/TestVectors/runtimes/net/Generated/WrappedDynamoDbItemEncryptor/TypeConversion.cs
@@ -716,11 +716,11 @@ public static software.amazon.cryptography.services.dynamodb.internaldafny.types
             }
             if (value.NULL == true)
             {
-                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL(value.NULL));
+                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL((bool)value.NULL));
             }
-            if (value.IsBOOLSet)
+            if (value.BOOL != null)
             {
-                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL(value.BOOL));
+                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL((bool)value.BOOL));
             }
             throw new System.ArgumentException("Invalid Amazon.DynamoDBv2.Model.AttributeValue state");
         }

From 01c84f8d6f5cf2837535a11f4a9c8b11cd81563a Mon Sep 17 00:00:00 2001
From: Jose Corella <jocorell@amazon.com>
Date: Fri, 20 Mar 2026 12:04:57 -0700
Subject: [PATCH 04/13] update releaserc files

---
 .releaserc-net.cjs | 234 +++++++++++++++++++++++++++++++++++++++++++++
 .releaserc.cjs     | 149 ++++++++++++++++++++---------
 Makefile           |  14 +++
 project.properties |   2 +-
 4 files changed, 353 insertions(+), 46 deletions(-)
 create mode 100644 .releaserc-net.cjs

diff --git a/.releaserc-net.cjs b/.releaserc-net.cjs
new file mode 100644
index 0000000000..86feee0074
--- /dev/null
+++ b/.releaserc-net.cjs
@@ -0,0 +1,234 @@
+// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0
+
+/*
+  First run `make setup_semantic_release` to install the required dependencies.
+
+  Using this config semantic-release will search for the latest tag
+  evaluate all commits after that tag
+  generate release notes and a version bump.
+  It will commit these changes, push these changes, and publish a new version tag.
+
+  This file requires a `--branches` option to function.
+  This is to facilitate point releases if needed.
+
+  `npx semantic-release --branches main`
+*/
+
+const fs = require("fs");
+
+/**
+ * Function to parse a simple properties file
+ * @param {string} filePath - Path to the properties file
+ * @returns {Object} Parsed properties as key-value pairs
+ */
+function parsePropertiesFile(filePath) {
+  const content = fs.readFileSync(filePath, "utf8");
+  const properties = {};
+
+  content.split("\n").forEach((line) => {
+    if (line && !line.startsWith("#") && line.includes("=")) {
+      const [key, ...valueParts] = line.split("=");
+      properties[key.trim()] = valueParts.join("=").trim();
+    }
+  });
+
+  return properties;
+}
+
+// Read your project.properties file
+const props = parsePropertiesFile("./project.properties");
+
+// This project has several runtimes
+// each one has files that need to be updated.
+// We model all the files and the runtimes here in this structure
+const Runtimes = {
+  net: {
+    "DynamoDbEncryption/runtimes/net/DynamoDbEncryption.csproj": {
+      dependencies: [],
+      assemblyInfo: "DynamoDbEncryption/runtimes/net/AssemblyInfo.cs",
+    },
+  },
+};
+
+/**
+ * @type {import('semantic-release').GlobalConfig}
+ */
+module.exports = {
+  branches: ["main"],
+  repositoryUrl: "git@github.com:aws/aws-database-encryption-sdk-dynamodb.git",
+  tagFormat: "v${version}-net",
+  plugins: [
+    // Check the commits since the last release
+    [
+      "@semantic-release/commit-analyzer",
+      {
+        preset: "conventionalcommits",
+        parserOpts: {
+          noteKeywords: ["DOTNET-BREAKING-CHANGE", "DOTNET-BREAKING-CHANGES"],
+        },
+        presetConfig: {
+          types: [
+            { type: "feat", section: "Features" },
+            { type: "fix", section: "Fixes" },
+            { type: "chore", section: "Maintenance" },
+            { type: "docs", section: "Maintenance" },
+            { type: "revert", section: "Fixes" },
+            { type: "style", hidden: true },
+            { type: "refactor", hidden: true },
+            { type: "perf", hidden: true },
+            { type: "test", hidden: true },
+          ],
+        },
+        releaseRules: [
+          { type: "docs", release: "patch" },
+          { type: "revert", release: "patch" },
+          { type: "chore", release: "patch" },
+        ],
+      },
+    ],
+    // Based on the commits generate release notes
+    [
+      "@semantic-release/release-notes-generator",
+      {
+        preset: "conventionalcommits",
+        parserOpts: {
+          noteKeywords: ["DOTNET-BREAKING-CHANGE", "DOTNET-BREAKING-CHANGES"],
+        },
+        presetConfig: {
+          types: [
+            {
+              type: "feat",
+              scope: "dafny",
+              section: "Features -- All Languages",
+              hidden: false,
+            },
+            {
+              type: "feat",
+              scope: "dotnet",
+              section: "Features -- DotNet",
+              hidden: false,
+            },
+            {
+              type: "fix",
+              scope: "dafny",
+              section: "Fixes -- All Languages",
+              hidden: false,
+            },
+            {
+              type: "fix",
+              scope: "dotnet",
+              section: "Fixes -- DotNet",
+              hidden: false,
+            },
+            {
+              type: "chore",
+              scope: "dafny",
+              section: "Maintenance -- All Languages",
+              hidden: false,
+            },
+            {
+              type: "chore",
+              scope: "dotnet",
+              section: "Maintenance -- DotNet",
+              hidden: false,
+            },
+            {
+              type: "docs",
+              scope: "dafny",
+              section: "Maintenance -- All Languages",
+              hidden: false,
+            },
+            {
+              type: "docs",
+              scope: "dotnet",
+              section: "Maintenance -- DotNet",
+              hidden: false,
+            },
+            {
+              type: "revert",
+              scope: "dafny",
+              section: "Fixes -- All Languages",
+              hidden: false,
+            },
+            {
+              type: "revert",
+              scope: "dotnet",
+              section: "Fixes -- DotNet",
+              hidden: false,
+            },
+            { type: "style", section: "Miscellaneous", hidden: false },
+            { type: "refactor", section: "Miscellaneous", hidden: false },
+            { type: "perf", section: "Miscellaneous", hidden: false },
+            { type: "test", section: "Miscellaneous", hidden: false },
+          ],
+        },
+      },
+    ],
+    // Update the change log with the generated release notes
+    [
+      "@semantic-release/changelog",
+      {
+        changelogFile: "CHANGELOG.md",
+        changelogTitle: "# Changelog",
+      },
+    ],
+
+    // Bump the various versions
+    [
+      "semantic-release-replace-plugin",
+      {
+        replacements: [
+          // Update the version for all DotNet projects
+          // Does not update the dependencies
+          {
+            files: Object.keys(Runtimes.net),
+            from: "<Version>.*</Version>",
+            to: "<Version>${nextRelease.version}</Version>",
+            results: Object.keys(Runtimes.net).map(CheckResults),
+            countMatches: true,
+          },
+          {
+            files: Object.keys(Runtimes.net),
+            from: '<ProjectReference Include="../../../submodules/MaterialProviders/AwsCryptographicMaterialProviders/runtimes/net/MPL.csproj"/>',
+            to: `<PackageReference Include="AWS.Cryptography.MaterialProviders" Version="[${props.mplDependencyNetVersion}]" />`,
+            results: Object.keys(Runtimes.net).map(CheckResults),
+            countMatches: true,
+          },
+          // Update the AssmeblyInfo.cs file of the DotNet projects
+          ...Object.entries(Runtimes.net).flatMap(
+            ([file, { assemblyInfo }]) => ({
+              files: assemblyInfo,
+              from: "assembly: AssemblyVersion(.*)",
+              to: 'assembly: AssemblyVersion("${nextRelease.version}")]',
+              results: [CheckResults(assemblyInfo)],
+              countMatches: true,
+            }),
+          ),
+        ],
+      },
+    ],
+    // Commit and push changes the changelog and versions bumps
+    [
+      "@semantic-release/git",
+      {
+        assets: [
+          "CHANGELOG.md",
+          ...Object.values(Runtimes).flatMap((r) => Object.keys(r)),
+          ...Object.values(Runtimes.net).flatMap((r) => r.assemblyInfo),
+        ],
+        message:
+          "chore(release): ${nextRelease.version} \n\n${nextRelease.notes}",
+      },
+    ],
+  ],
+};
+
+function CheckResults(file) {
+  return {
+    file,
+    hasChanged: true,
+    numMatches: 1,
+    numReplacements: 1,
+  };
+}
diff --git a/.releaserc.cjs b/.releaserc.cjs
index 21f6d9af3e..25db26cbc4 100644
--- a/.releaserc.cjs
+++ b/.releaserc.cjs
@@ -48,12 +48,6 @@ const Runtimes = {
       dependencies: [],
     },
   },
-  net: {
-    "DynamoDbEncryption/runtimes/net/DynamoDbEncryption.csproj": {
-      dependencies: [],
-      assemblyInfo: "DynamoDbEncryption/runtimes/net/AssemblyInfo.cs",
-    },
-  },
 };
 
 /**
@@ -69,7 +63,7 @@ module.exports = {
       {
         preset: "conventionalcommits",
         parserOpts: {
-          noteKeywords: ["BREAKING CHANGE", "BREAKING CHANGES"],
+          noteKeywords: ["BREAKING-CHANGE", "BREAKING-CHANGES"],
         },
         presetConfig: {
           types: [
@@ -97,19 +91,111 @@ module.exports = {
       {
         preset: "conventionalcommits",
         parserOpts: {
-          noteKeywords: ["BREAKING CHANGE", "BREAKING CHANGES"],
+          noteKeywords: ["BREAKING-CHANGE", "BREAKING-CHANGES"],
         },
         presetConfig: {
           types: [
-            { type: "feat", section: "Features" },
-            { type: "fix", section: "Fixes" },
-            { type: "chore", section: "Maintenance" },
-            { type: "docs", section: "Maintenance" },
-            { type: "revert", section: "Fixes" },
-            { type: "style", hidden: true },
-            { type: "refactor", hidden: true },
-            { type: "perf", hidden: true },
-            { type: "test", hidden: true },
+            {
+              type: "feat",
+              scope: "dafny",
+              section: "Features -- All Languages",
+              hidden: false,
+            },
+            {
+              type: "feat",
+              scope: "java",
+              section: "Features -- Java",
+              hidden: false,
+            },
+            {
+              type: "feat",
+              scope: "rust",
+              section: "Features -- Rust",
+              hidden: false,
+            },
+
+            {
+              type: "fix",
+              scope: "dafny",
+              section: "Fixes -- All Languages",
+              hidden: false,
+            },
+            {
+              type: "fix",
+              scope: "java",
+              section: "Fixes -- Java",
+              hidden: false,
+            },
+            {
+              type: "fix",
+              scope: "rust",
+              section: "Fixes -- Rust",
+              hidden: false,
+            },
+
+            {
+              type: "chore",
+              scope: "dafny",
+              section: "Maintenance -- All Languages",
+              hidden: false,
+            },
+            {
+              type: "chore",
+              scope: "java",
+              section: "Maintenance -- Java",
+              hidden: false,
+            },
+            {
+              type: "chore",
+              scope: "rust",
+              section: "Maintenance -- Rust",
+              hidden: false,
+            },
+            {
+              type: "chore",
+              section: "Miscellaneous",
+              hidden: false,
+            },
+            {
+              type: "docs",
+              scope: "dafny",
+              section: "Maintenance -- All Languages",
+              hidden: false,
+            },
+            {
+              type: "docs",
+              scope: "java",
+              section: "Maintenance -- Java",
+              hidden: false,
+            },
+            {
+              type: "docs",
+              scope: "rust",
+              section: "Maintenance -- Rust",
+              hidden: false,
+            },
+            {
+              type: "revert",
+              scope: "dafny",
+              section: "Fixes -- All Languages",
+              hidden: false,
+            },
+            {
+              type: "revert",
+              scope: "java",
+              section: "Fixes -- Java",
+              hidden: false,
+            },
+            {
+              type: "revert",
+              scope: "rust",
+              section: "Fixes -- Rust",
+              hidden: false,
+            },
+            { type: "style", section: "Miscellaneous", hidden: false },
+            { type: "refactor", section: "Miscellaneous", hidden: false },
+            { type: "perf", section: "Miscellaneous", hidden: false },
+            { type: "test", section: "Miscellaneous", hidden: false },
           ],
         },
       },
@@ -137,32 +223,6 @@ module.exports = {
             results: Object.keys(Runtimes.java).map(CheckResults),
             countMatches: true,
           },
-          // Update the version for all DotNet projects
-          // Does not update the dependencies
-          {
-            files: Object.keys(Runtimes.net),
-            from: "<Version>.*</Version>",
-            to: "<Version>${nextRelease.version}</Version>",
-            results: Object.keys(Runtimes.net).map(CheckResults),
-            countMatches: true,
-          },
-          {
-            files: Object.keys(Runtimes.net),
-            from: '<ProjectReference Include="../../../submodules/MaterialProviders/AwsCryptographicMaterialProviders/runtimes/net/MPL.csproj"/>',
-            to: `<PackageReference Include="AWS.Cryptography.MaterialProviders" Version="[${props.mplDependencyNetVersion}]" />`,
-            results: Object.keys(Runtimes.net).map(CheckResults),
-            countMatches: true,
-          },
-          // Update the AssmeblyInfo.cs file of the DotNet projects
-          ...Object.entries(Runtimes.net).flatMap(
-            ([file, { assemblyInfo }]) => ({
-              files: assemblyInfo,
-              from: "assembly: AssemblyVersion(.*)",
-              to: 'assembly: AssemblyVersion("${nextRelease.version}")]',
-              results: [CheckResults(assemblyInfo)],
-              countMatches: true,
-            }),
-          ),
         ],
       },
     ],
@@ -173,10 +233,9 @@ module.exports = {
         assets: [
           "CHANGELOG.md",
           ...Object.values(Runtimes).flatMap((r) => Object.keys(r)),
-          ...Object.values(Runtimes.net).flatMap((r) => r.assemblyInfo),
         ],
         message:
-          "chore(release): ${nextRelease.version} [skip ci]\n\n${nextRelease.notes}",
+          "chore(release): ${nextRelease.version} \n\n${nextRelease.notes}",
       },
     ],
   ],
diff --git a/Makefile b/Makefile
index 7bede0e44d..30ec89950b 100644
--- a/Makefile
+++ b/Makefile
@@ -82,5 +82,19 @@ setup_semantic_release:
 run_semantic_release:
 	npx semantic-release --no-ci
 
+run_net_semantic_release:
+	mv .releaserc.cjs .releaserc-main.cjs
+	mv .releaserc-net.cjs .releaserc.cjs
+	npx semantic-release --no-ci
+	mv .releaserc.cjs .releaserc-net.cjs
+	mv .releaserc-main.cjs .releaserc.cjs
+
 dry_run_semantic_release:
 	npx semantic-release --dry-run
+
+dry_run_net_semantic_release:
+	mv .releaserc.cjs .releaserc-main.cjs
+	mv .releaserc-net.cjs .releaserc.cjs
+	npx semantic-release --dry-run
+	mv .releaserc.cjs .releaserc-net.cjs
+	mv .releaserc-main.cjs .releaserc.cjs
\ No newline at end of file
diff --git a/project.properties b/project.properties
index d0eda36016..5e471a9ddd 100644
--- a/project.properties
+++ b/project.properties
@@ -1,6 +1,6 @@
 projectJavaVersion=3.9.1-SNAPSHOT
 mplDependencyJavaVersion=1.11.2-SNAPSHOT
-mplDependencyNetVersion=1.11.2
+mplDependencyNetVersion=2.0.0
 dafnyVersion=4.9.0
 dafnyVerifyVersion=4.9.1
 dafnyRuntimeJavaVersion=4.9.0

From 13cc2927d93386d9961b8408e8e042292ac91e3e Mon Sep 17 00:00:00 2001
From: Jose Corella <jocorell@amazon.com>
Date: Fri, 20 Mar 2026 16:48:23 -0700
Subject: [PATCH 05/13] m

---
 .../Generated/DynamoDbEncryption/TypeConversion.cs   | 10 +++++++---
 Examples/runtimes/net/src/TestUtils.cs               | 12 ++++++------
 2 files changed, 13 insertions(+), 9 deletions(-)

diff --git a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs
index 708467da12..82bbffe6a0 100644
--- a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs
+++ b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs
@@ -7,6 +7,10 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb
 {
   public static class TypeConversion
   {
+    private const string ISO8601DateFormat = "yyyy-MM-dd\\THH:mm:ss.fff\\Z";
+
+    private const string ISO8601DateFormatNoMS = "yyyy-MM-dd\\THH:mm:ss\\Z";
+
     public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.AsSet FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S5_AsSet(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IAsSet value)
     {
       software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.AsSet concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.AsSet)value; AWS.Cryptography.DbEncryptionSDK.DynamoDb.AsSet converted = new AWS.Cryptography.DbEncryptionSDK.DynamoDb.AsSet(); return converted;
@@ -2254,11 +2258,11 @@ public static software.amazon.cryptography.services.dynamodb.internaldafny.types
       }
       if (value.NULL == true)
       {
-        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL((bool)value.NULL));
+        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL(value.NULL));
       }
-      if (value.BOOL != null)
+      if (value.IsBOOLSet)
       {
-        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL((bool)value.BOOL));
+        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL(value.BOOL));
       }
       throw new System.ArgumentException("Invalid Amazon.DynamoDBv2.Model.AttributeValue state");
     }
diff --git a/Examples/runtimes/net/src/TestUtils.cs b/Examples/runtimes/net/src/TestUtils.cs
index 2ad5c4a26c..3ad2592b13 100644
--- a/Examples/runtimes/net/src/TestUtils.cs
+++ b/Examples/runtimes/net/src/TestUtils.cs
@@ -61,9 +61,9 @@ public static String AttributeType(AttributeValue value)
         if (value.S != null) return "S";
         if (value.N != null) return "N";
         if (value.B != null) return "B";
-        if (value.SS.Any()) return "SS";
-        if (value.NS.Any()) return "NS";
-        if (value.BS.Any()) return "BS";
+        if (value.SS != null && value.SS.Any()) return "SS";
+        if (value.NS != null && value.NS.Any()) return "NS";
+        if (value.BS != null && value.BS.Any()) return "BS";
         if (value.IsMSet) return "M";
         if (value.IsLSet) return "L";
         if (value.NULL == true) return "NULL";
@@ -76,9 +76,9 @@ public static void PrintAttributeValue(AttributeValue value)
         if (value.S != null) Console.Write($"S {value.S}\n");
         if (value.N != null) Console.Write($"N {value.N}\n");
         if (value.B != null) Console.Write($"B {value.B}\n");
-        if (value.SS.Any()) Console.Write($"SS {value.SS}\n");
-        if (value.NS.Any()) Console.Write($"NS {value.NS}\n");
-        if (value.BS.Any()) Console.Write($"BS {value.BS}\n");
+        if (value.SS != null && value.SS.Any()) Console.Write($"SS {value.SS}\n");
+        if (value.NS != null && value.NS.Any()) Console.Write($"NS {value.NS}\n");
+        if (value.BS != null && value.BS.Any()) Console.Write($"BS {value.BS}\n");
         if (value.IsMSet) Console.Write($"M {value.M}\n");
         if (value.IsLSet) Console.Write($"L {value.L}\n");
         if (value.NULL == true) Console.Write($"NULL {value.NULL}\n");

From 8767fd6f66dca3214d25cb22868e227e0fe1c7ab Mon Sep 17 00:00:00 2001
From: Jose Corella <jocorell@amazon.com>
Date: Fri, 20 Mar 2026 16:54:38 -0700
Subject: [PATCH 06/13] m

---
 .../dotnet/dafny-4.9.0.patch                  | 30 -------------------
 .../dotnet/dafny-4.9.0.patch                  | 30 -------------------
 .../dotnet/dafny-4.9.0.patch                  | 30 -------------------
 .../DDBEncryption/dotnet/dafny-4.9.0.patch    | 19 ------------
 .../dotnet/dafny-4.9.0.patch                  | 19 ------------
 5 files changed, 128 deletions(-)
 delete mode 100644 DynamoDbEncryption/codegen-patches/DynamoDbEncryption/dotnet/dafny-4.9.0.patch
 delete mode 100644 DynamoDbEncryption/codegen-patches/DynamoDbEncryptionTransforms/dotnet/dafny-4.9.0.patch
 delete mode 100644 DynamoDbEncryption/codegen-patches/DynamoDbItemEncryptor/dotnet/dafny-4.9.0.patch
 delete mode 100644 TestVectors/codegen-patches/DDBEncryption/dotnet/dafny-4.9.0.patch
 delete mode 100644 TestVectors/codegen-patches/WrappedDynamoDbItemEncryptor/dotnet/dafny-4.9.0.patch

diff --git a/DynamoDbEncryption/codegen-patches/DynamoDbEncryption/dotnet/dafny-4.9.0.patch b/DynamoDbEncryption/codegen-patches/DynamoDbEncryption/dotnet/dafny-4.9.0.patch
deleted file mode 100644
index a33e07381e..0000000000
--- a/DynamoDbEncryption/codegen-patches/DynamoDbEncryption/dotnet/dafny-4.9.0.patch
+++ /dev/null
@@ -1,30 +0,0 @@
-diff --git a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs
-index 82bbffe6..708467da 100644
---- a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs
-+++ b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs
-@@ -7,10 +7,6 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb
- {
-   public static class TypeConversion
-   {
--    private const string ISO8601DateFormat = "yyyy-MM-dd\\THH:mm:ss.fff\\Z";
--
--    private const string ISO8601DateFormatNoMS = "yyyy-MM-dd\\THH:mm:ss\\Z";
--
-     public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.AsSet FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S5_AsSet(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IAsSet value)
-     {
-       software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.AsSet concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.AsSet)value; AWS.Cryptography.DbEncryptionSDK.DynamoDb.AsSet converted = new AWS.Cryptography.DbEncryptionSDK.DynamoDb.AsSet(); return converted;
-@@ -2258,11 +2254,11 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb
-       }
-       if (value.NULL == true)
-       {
--        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL(value.NULL));
-+        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL((bool)value.NULL));
-       }
--      if (value.IsBOOLSet)
-+      if (value.BOOL != null)
-       {
--        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL(value.BOOL));
-+        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL((bool)value.BOOL));
-       }
-       throw new System.ArgumentException("Invalid Amazon.DynamoDBv2.Model.AttributeValue state");
-     }
diff --git a/DynamoDbEncryption/codegen-patches/DynamoDbEncryptionTransforms/dotnet/dafny-4.9.0.patch b/DynamoDbEncryption/codegen-patches/DynamoDbEncryptionTransforms/dotnet/dafny-4.9.0.patch
deleted file mode 100644
index 76383851bb..0000000000
--- a/DynamoDbEncryption/codegen-patches/DynamoDbEncryptionTransforms/dotnet/dafny-4.9.0.patch
+++ /dev/null
@@ -1,30 +0,0 @@
-diff --git a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs
-index 08aa5919..02ad044e 100644
---- a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs
-+++ b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs
-@@ -7,10 +7,6 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb.Transforms
- {
-   public static class TypeConversion
-   {
--    private const string ISO8601DateFormat = "yyyy-MM-dd\\THH:mm:ss.fff\\Z";
--
--    private const string ISO8601DateFormatNoMS = "yyyy-MM-dd\\THH:mm:ss\\Z";
--
-     public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.AsSet FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S5_AsSet(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IAsSet value)
-     {
-       software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.AsSet concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.AsSet)value; AWS.Cryptography.DbEncryptionSDK.DynamoDb.AsSet converted = new AWS.Cryptography.DbEncryptionSDK.DynamoDb.AsSet(); return converted;
-@@ -3222,11 +3218,11 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb.Transforms
-       }
-       if (value.NULL == true)
-       {
--        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL(value.NULL));
-+        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL((bool)value.NULL));
-       }
--      if (value.IsBOOLSet)
-+      if (value.BOOL != null)
-       {
--        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL(value.BOOL));
-+        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL((bool)value.BOOL));
-       }
-       throw new System.ArgumentException("Invalid Amazon.DynamoDBv2.Model.AttributeValue state");
-     }
diff --git a/DynamoDbEncryption/codegen-patches/DynamoDbItemEncryptor/dotnet/dafny-4.9.0.patch b/DynamoDbEncryption/codegen-patches/DynamoDbItemEncryptor/dotnet/dafny-4.9.0.patch
deleted file mode 100644
index ffc431be09..0000000000
--- a/DynamoDbEncryption/codegen-patches/DynamoDbItemEncryptor/dotnet/dafny-4.9.0.patch
+++ /dev/null
@@ -1,30 +0,0 @@
-diff --git a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs
-index b4a90d1b..004fe3ed 100644
---- a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs
-+++ b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs
-@@ -7,10 +7,6 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor
- {
-   public static class TypeConversion
-   {
--    private const string ISO8601DateFormat = "yyyy-MM-dd\\THH:mm:ss.fff\\Z";
--
--    private const string ISO8601DateFormatNoMS = "yyyy-MM-dd\\THH:mm:ss\\Z";
--
-     public static System.Collections.Generic.Dictionary<string, AWS.Cryptography.DbEncryptionSDK.StructuredEncryption.CryptoAction> FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S16_AttributeActions(Dafny.IMap<Dafny.ISequence<char>, software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny.types._ICryptoAction> value)
-     {
-       return value.ItemEnumerable.ToDictionary(pair => FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S16_AttributeActions__M3_key(pair.Car), pair => FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S16_AttributeActions__M5_value(pair.Cdr));
-@@ -724,11 +720,11 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor
-       }
-       if (value.NULL == true)
-       {
--        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL(value.NULL));
-+        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL((bool)value.NULL));
-       }
--      if (value.IsBOOLSet)
-+      if (value.BOOL != null)
-       {
--        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL(value.BOOL));
-+        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL((bool)value.BOOL));
-       }
-       throw new System.ArgumentException("Invalid Amazon.DynamoDBv2.Model.AttributeValue state");
-     }
diff --git a/TestVectors/codegen-patches/DDBEncryption/dotnet/dafny-4.9.0.patch b/TestVectors/codegen-patches/DDBEncryption/dotnet/dafny-4.9.0.patch
deleted file mode 100644
index bc63e8c02c..0000000000
--- a/TestVectors/codegen-patches/DDBEncryption/dotnet/dafny-4.9.0.patch
+++ /dev/null
@@ -1,19 +0,0 @@
-diff --git a/TestVectors/runtimes/net/Generated/DDBEncryption/TypeConversion.cs b/TestVectors/runtimes/net/Generated/DDBEncryption/TypeConversion.cs
-index 1ff2d1b4..5e46a9aa 100644
---- a/TestVectors/runtimes/net/Generated/DDBEncryption/TypeConversion.cs
-+++ b/TestVectors/runtimes/net/Generated/DDBEncryption/TypeConversion.cs
-@@ -2236,11 +2236,11 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb.Wrapped
-             }
-             if (value.NULL == true)
-             {
--                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL(value.NULL));
-+                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL((bool)value.NULL));
-             }
--            if (value.IsBOOLSet)
-+            if (value.BOOL != null)
-             {
--                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL(value.BOOL));
-+                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL((bool)value.BOOL));
-             }
-             throw new System.ArgumentException("Invalid Amazon.DynamoDBv2.Model.AttributeValue state");
-         }
diff --git a/TestVectors/codegen-patches/WrappedDynamoDbItemEncryptor/dotnet/dafny-4.9.0.patch b/TestVectors/codegen-patches/WrappedDynamoDbItemEncryptor/dotnet/dafny-4.9.0.patch
deleted file mode 100644
index 321f0b1032..0000000000
--- a/TestVectors/codegen-patches/WrappedDynamoDbItemEncryptor/dotnet/dafny-4.9.0.patch
+++ /dev/null
@@ -1,19 +0,0 @@
-diff --git a/TestVectors/runtimes/net/Generated/WrappedDynamoDbItemEncryptor/TypeConversion.cs b/TestVectors/runtimes/net/Generated/WrappedDynamoDbItemEncryptor/TypeConversion.cs
-index dc216416..f4ffbb58 100644
---- a/TestVectors/runtimes/net/Generated/WrappedDynamoDbItemEncryptor/TypeConversion.cs
-+++ b/TestVectors/runtimes/net/Generated/WrappedDynamoDbItemEncryptor/TypeConversion.cs
-@@ -716,11 +716,11 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.Wrapped
-             }
-             if (value.NULL == true)
-             {
--                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL(value.NULL));
-+                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL((bool)value.NULL));
-             }
--            if (value.IsBOOLSet)
-+            if (value.BOOL != null)
-             {
--                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL(value.BOOL));
-+                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL((bool)value.BOOL));
-             }
-             throw new System.ArgumentException("Invalid Amazon.DynamoDBv2.Model.AttributeValue state");
-         }

From c25b21b348705349acff489674a625d263f6e475 Mon Sep 17 00:00:00 2001
From: Jose Corella <jocorell@amazon.com>
Date: Fri, 20 Mar 2026 17:02:00 -0700
Subject: [PATCH 07/13] m

---
 .../Generated/DynamoDbItemEncryptor/TypeConversion.cs  | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

diff --git a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs
index 004fe3ed1a..b4a90d1b44 100644
--- a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs
+++ b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs
@@ -7,6 +7,10 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor
 {
   public static class TypeConversion
   {
+    private const string ISO8601DateFormat = "yyyy-MM-dd\\THH:mm:ss.fff\\Z";
+
+    private const string ISO8601DateFormatNoMS = "yyyy-MM-dd\\THH:mm:ss\\Z";
+
     public static System.Collections.Generic.Dictionary<string, AWS.Cryptography.DbEncryptionSDK.StructuredEncryption.CryptoAction> FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S16_AttributeActions(Dafny.IMap<Dafny.ISequence<char>, software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny.types._ICryptoAction> value)
     {
       return value.ItemEnumerable.ToDictionary(pair => FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S16_AttributeActions__M3_key(pair.Car), pair => FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S16_AttributeActions__M5_value(pair.Cdr));
@@ -720,11 +724,11 @@ public static software.amazon.cryptography.services.dynamodb.internaldafny.types
       }
       if (value.NULL == true)
       {
-        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL((bool)value.NULL));
+        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL(value.NULL));
       }
-      if (value.BOOL != null)
+      if (value.IsBOOLSet)
       {
-        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL((bool)value.BOOL));
+        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL(value.BOOL));
       }
       throw new System.ArgumentException("Invalid Amazon.DynamoDBv2.Model.AttributeValue state");
     }

From e265fb7c338a68bb3de6346883f86da16b12e4bd Mon Sep 17 00:00:00 2001
From: Jose Corella <jocorell@amazon.com>
Date: Fri, 20 Mar 2026 17:07:40 -0700
Subject: [PATCH 08/13] m

---
 .../DynamoDbEncryptionTransforms/TypeConversion.cs     | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

diff --git a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs
index 02ad044e52..08aa591908 100644
--- a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs
+++ b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs
@@ -7,6 +7,10 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb.Transforms
 {
   public static class TypeConversion
   {
+    private const string ISO8601DateFormat = "yyyy-MM-dd\\THH:mm:ss.fff\\Z";
+
+    private const string ISO8601DateFormatNoMS = "yyyy-MM-dd\\THH:mm:ss\\Z";
+
     public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.AsSet FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S5_AsSet(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IAsSet value)
     {
       software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.AsSet concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.AsSet)value; AWS.Cryptography.DbEncryptionSDK.DynamoDb.AsSet converted = new AWS.Cryptography.DbEncryptionSDK.DynamoDb.AsSet(); return converted;
@@ -3218,11 +3222,11 @@ public static software.amazon.cryptography.services.dynamodb.internaldafny.types
       }
       if (value.NULL == true)
       {
-        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL((bool)value.NULL));
+        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL(value.NULL));
       }
-      if (value.BOOL != null)
+      if (value.IsBOOLSet)
       {
-        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL((bool)value.BOOL));
+        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL(value.BOOL));
       }
       throw new System.ArgumentException("Invalid Amazon.DynamoDBv2.Model.AttributeValue state");
     }

From 6fe230d80e2aed2f3950a0edfa61f22809abda5f Mon Sep 17 00:00:00 2001
From: Jose Corella <jocorell@amazon.com>
Date: Fri, 20 Mar 2026 17:13:20 -0700
Subject: [PATCH 09/13] m

---
 .../dotnet/dafny-4.9.0.patch                  | 49 +++++++++++++++++++
 .../dotnet/dafny-4.9.0.patch                  | 49 +++++++++++++++++++
 .../dotnet/dafny-4.9.0.patch                  | 49 +++++++++++++++++++
 .../DynamoDbEncryption/TypeConversion.cs      | 16 +++---
 .../TypeConversion.cs                         | 16 +++---
 .../DynamoDbItemEncryptor/TypeConversion.cs   | 16 +++---
 6 files changed, 165 insertions(+), 30 deletions(-)
 create mode 100644 DynamoDbEncryption/codegen-patches/DynamoDbEncryption/dotnet/dafny-4.9.0.patch
 create mode 100644 DynamoDbEncryption/codegen-patches/DynamoDbEncryptionTransforms/dotnet/dafny-4.9.0.patch
 create mode 100644 DynamoDbEncryption/codegen-patches/DynamoDbItemEncryptor/dotnet/dafny-4.9.0.patch

diff --git a/DynamoDbEncryption/codegen-patches/DynamoDbEncryption/dotnet/dafny-4.9.0.patch b/DynamoDbEncryption/codegen-patches/DynamoDbEncryption/dotnet/dafny-4.9.0.patch
new file mode 100644
index 0000000000..957ff09b1d
--- /dev/null
+++ b/DynamoDbEncryption/codegen-patches/DynamoDbEncryption/dotnet/dafny-4.9.0.patch
@@ -0,0 +1,49 @@
+diff --git a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs
+index 82bbffe6..90bdb825 100644
+--- a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs
++++ b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs
+@@ -7,10 +7,6 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb
+ {
+   public static class TypeConversion
+   {
+-    private const string ISO8601DateFormat = "yyyy-MM-dd\\THH:mm:ss.fff\\Z";
+-
+-    private const string ISO8601DateFormatNoMS = "yyyy-MM-dd\\THH:mm:ss\\Z";
+-
+     public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.AsSet FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S5_AsSet(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IAsSet value)
+     {
+       software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.AsSet concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.AsSet)value; AWS.Cryptography.DbEncryptionSDK.DynamoDb.AsSet converted = new AWS.Cryptography.DbEncryptionSDK.DynamoDb.AsSet(); return converted;
+@@ -2236,15 +2232,15 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb
+       {
+         return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_B(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M1_B(value.B));
+       }
+-      if (value.SS.Any())
++      if (value.SS != null && value.SS.Any())
+       {
+         return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_SS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_SS(value.SS));
+       }
+-      if (value.NS.Any())
++      if (value.NS != null && value.NS.Any())
+       {
+         return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_NS(value.NS));
+       }
+-      if (value.BS.Any())
++      if (value.BS != null && value.BS.Any())
+       {
+         return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_BS(value.BS));
+       }
+@@ -2258,11 +2254,11 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb
+       }
+       if (value.NULL == true)
+       {
+-        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL(value.NULL));
++        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL((bool)value.NULL));
+       }
+-      if (value.IsBOOLSet)
++      if (value.BOOL != null)
+       {
+-        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL(value.BOOL));
++        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL((bool)value.BOOL));
+       }
+       throw new System.ArgumentException("Invalid Amazon.DynamoDBv2.Model.AttributeValue state");
+     }
diff --git a/DynamoDbEncryption/codegen-patches/DynamoDbEncryptionTransforms/dotnet/dafny-4.9.0.patch b/DynamoDbEncryption/codegen-patches/DynamoDbEncryptionTransforms/dotnet/dafny-4.9.0.patch
new file mode 100644
index 0000000000..657c859159
--- /dev/null
+++ b/DynamoDbEncryption/codegen-patches/DynamoDbEncryptionTransforms/dotnet/dafny-4.9.0.patch
@@ -0,0 +1,49 @@
+diff --git a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs
+index 08aa5919..afcaa92c 100644
+--- a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs
++++ b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs
+@@ -7,10 +7,6 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb.Transforms
+ {
+   public static class TypeConversion
+   {
+-    private const string ISO8601DateFormat = "yyyy-MM-dd\\THH:mm:ss.fff\\Z";
+-
+-    private const string ISO8601DateFormatNoMS = "yyyy-MM-dd\\THH:mm:ss\\Z";
+-
+     public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.AsSet FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S5_AsSet(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IAsSet value)
+     {
+       software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.AsSet concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.AsSet)value; AWS.Cryptography.DbEncryptionSDK.DynamoDb.AsSet converted = new AWS.Cryptography.DbEncryptionSDK.DynamoDb.AsSet(); return converted;
+@@ -3200,15 +3196,15 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb.Transforms
+       {
+         return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_B(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M1_B(value.B));
+       }
+-      if (value.SS.Any())
++      if (value.SS != null && value.SS.Any())
+       {
+         return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_SS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_SS(value.SS));
+       }
+-      if (value.NS.Any())
++      if (value.NS != null && value.NS.Any())
+       {
+         return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_NS(value.NS));
+       }
+-      if (value.BS.Any())
++      if (value.BS != null && value.BS.Any())
+       {
+         return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_BS(value.BS));
+       }
+@@ -3222,11 +3218,11 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb.Transforms
+       }
+       if (value.NULL == true)
+       {
+-        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL(value.NULL));
++        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL((bool)value.NULL));
+       }
+-      if (value.IsBOOLSet)
++      if (value.BOOL != null)
+       {
+-        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL(value.BOOL));
++        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL((bool)value.BOOL));
+       }
+       throw new System.ArgumentException("Invalid Amazon.DynamoDBv2.Model.AttributeValue state");
+     }
diff --git a/DynamoDbEncryption/codegen-patches/DynamoDbItemEncryptor/dotnet/dafny-4.9.0.patch b/DynamoDbEncryption/codegen-patches/DynamoDbItemEncryptor/dotnet/dafny-4.9.0.patch
new file mode 100644
index 0000000000..8e47a1219d
--- /dev/null
+++ b/DynamoDbEncryption/codegen-patches/DynamoDbItemEncryptor/dotnet/dafny-4.9.0.patch
@@ -0,0 +1,49 @@
+diff --git a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs
+index b4a90d1b..7f4207c2 100644
+--- a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs
++++ b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs
+@@ -7,10 +7,6 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor
+ {
+   public static class TypeConversion
+   {
+-    private const string ISO8601DateFormat = "yyyy-MM-dd\\THH:mm:ss.fff\\Z";
+-
+-    private const string ISO8601DateFormatNoMS = "yyyy-MM-dd\\THH:mm:ss\\Z";
+-
+     public static System.Collections.Generic.Dictionary<string, AWS.Cryptography.DbEncryptionSDK.StructuredEncryption.CryptoAction> FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S16_AttributeActions(Dafny.IMap<Dafny.ISequence<char>, software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny.types._ICryptoAction> value)
+     {
+       return value.ItemEnumerable.ToDictionary(pair => FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S16_AttributeActions__M3_key(pair.Car), pair => FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S16_AttributeActions__M5_value(pair.Cdr));
+@@ -702,15 +698,15 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor
+       {
+         return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_B(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M1_B(value.B));
+       }
+-      if (value.SS.Any())
++      if (value.SS != null && value.SS.Any())
+       {
+         return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_SS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_SS(value.SS));
+       }
+-      if (value.NS.Any())
++      if (value.NS != null && value.NS.Any())
+       {
+         return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_NS(value.NS));
+       }
+-      if (value.BS.Any())
++      if (value.BS != null && value.BS.Any())
+       {
+         return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_BS(value.BS));
+       }
+@@ -724,11 +720,11 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor
+       }
+       if (value.NULL == true)
+       {
+-        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL(value.NULL));
++        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL((bool)value.NULL));
+       }
+-      if (value.IsBOOLSet)
++      if (value.BOOL != null)
+       {
+-        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL(value.BOOL));
++        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL((bool)value.BOOL));
+       }
+       throw new System.ArgumentException("Invalid Amazon.DynamoDBv2.Model.AttributeValue state");
+     }
diff --git a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs
index 82bbffe6a0..90bdb825b4 100644
--- a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs
+++ b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs
@@ -7,10 +7,6 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb
 {
   public static class TypeConversion
   {
-    private const string ISO8601DateFormat = "yyyy-MM-dd\\THH:mm:ss.fff\\Z";
-
-    private const string ISO8601DateFormatNoMS = "yyyy-MM-dd\\THH:mm:ss\\Z";
-
     public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.AsSet FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S5_AsSet(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IAsSet value)
     {
       software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.AsSet concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.AsSet)value; AWS.Cryptography.DbEncryptionSDK.DynamoDb.AsSet converted = new AWS.Cryptography.DbEncryptionSDK.DynamoDb.AsSet(); return converted;
@@ -2236,15 +2232,15 @@ public static software.amazon.cryptography.services.dynamodb.internaldafny.types
       {
         return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_B(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M1_B(value.B));
       }
-      if (value.SS.Any())
+      if (value.SS != null && value.SS.Any())
       {
         return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_SS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_SS(value.SS));
       }
-      if (value.NS.Any())
+      if (value.NS != null && value.NS.Any())
       {
         return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_NS(value.NS));
       }
-      if (value.BS.Any())
+      if (value.BS != null && value.BS.Any())
       {
         return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_BS(value.BS));
       }
@@ -2258,11 +2254,11 @@ public static software.amazon.cryptography.services.dynamodb.internaldafny.types
       }
       if (value.NULL == true)
       {
-        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL(value.NULL));
+        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL((bool)value.NULL));
       }
-      if (value.IsBOOLSet)
+      if (value.BOOL != null)
       {
-        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL(value.BOOL));
+        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL((bool)value.BOOL));
       }
       throw new System.ArgumentException("Invalid Amazon.DynamoDBv2.Model.AttributeValue state");
     }
diff --git a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs
index 08aa591908..afcaa92cd6 100644
--- a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs
+++ b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs
@@ -7,10 +7,6 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb.Transforms
 {
   public static class TypeConversion
   {
-    private const string ISO8601DateFormat = "yyyy-MM-dd\\THH:mm:ss.fff\\Z";
-
-    private const string ISO8601DateFormatNoMS = "yyyy-MM-dd\\THH:mm:ss\\Z";
-
     public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.AsSet FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S5_AsSet(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IAsSet value)
     {
       software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.AsSet concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.AsSet)value; AWS.Cryptography.DbEncryptionSDK.DynamoDb.AsSet converted = new AWS.Cryptography.DbEncryptionSDK.DynamoDb.AsSet(); return converted;
@@ -3200,15 +3196,15 @@ public static software.amazon.cryptography.services.dynamodb.internaldafny.types
       {
         return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_B(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M1_B(value.B));
       }
-      if (value.SS.Any())
+      if (value.SS != null && value.SS.Any())
       {
         return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_SS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_SS(value.SS));
       }
-      if (value.NS.Any())
+      if (value.NS != null && value.NS.Any())
       {
         return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_NS(value.NS));
       }
-      if (value.BS.Any())
+      if (value.BS != null && value.BS.Any())
       {
         return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_BS(value.BS));
       }
@@ -3222,11 +3218,11 @@ public static software.amazon.cryptography.services.dynamodb.internaldafny.types
       }
       if (value.NULL == true)
       {
-        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL(value.NULL));
+        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL((bool)value.NULL));
       }
-      if (value.IsBOOLSet)
+      if (value.BOOL != null)
       {
-        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL(value.BOOL));
+        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL((bool)value.BOOL));
       }
       throw new System.ArgumentException("Invalid Amazon.DynamoDBv2.Model.AttributeValue state");
     }
diff --git a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs
index b4a90d1b44..7f4207c213 100644
--- a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs
+++ b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs
@@ -7,10 +7,6 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor
 {
   public static class TypeConversion
   {
-    private const string ISO8601DateFormat = "yyyy-MM-dd\\THH:mm:ss.fff\\Z";
-
-    private const string ISO8601DateFormatNoMS = "yyyy-MM-dd\\THH:mm:ss\\Z";
-
     public static System.Collections.Generic.Dictionary<string, AWS.Cryptography.DbEncryptionSDK.StructuredEncryption.CryptoAction> FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S16_AttributeActions(Dafny.IMap<Dafny.ISequence<char>, software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny.types._ICryptoAction> value)
     {
       return value.ItemEnumerable.ToDictionary(pair => FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S16_AttributeActions__M3_key(pair.Car), pair => FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S16_AttributeActions__M5_value(pair.Cdr));
@@ -702,15 +698,15 @@ public static software.amazon.cryptography.services.dynamodb.internaldafny.types
       {
         return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_B(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M1_B(value.B));
       }
-      if (value.SS.Any())
+      if (value.SS != null && value.SS.Any())
       {
         return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_SS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_SS(value.SS));
       }
-      if (value.NS.Any())
+      if (value.NS != null && value.NS.Any())
       {
         return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_NS(value.NS));
       }
-      if (value.BS.Any())
+      if (value.BS != null && value.BS.Any())
       {
         return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_BS(value.BS));
       }
@@ -724,11 +720,11 @@ public static software.amazon.cryptography.services.dynamodb.internaldafny.types
       }
       if (value.NULL == true)
       {
-        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL(value.NULL));
+        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL((bool)value.NULL));
       }
-      if (value.IsBOOLSet)
+      if (value.BOOL != null)
       {
-        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL(value.BOOL));
+        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL((bool)value.BOOL));
       }
       throw new System.ArgumentException("Invalid Amazon.DynamoDBv2.Model.AttributeValue state");
     }

From 79ab4506d6cb98d6b53196f54c8ac239bac38da5 Mon Sep 17 00:00:00 2001
From: Jose Corella <jocorell@amazon.com>
Date: Fri, 20 Mar 2026 17:19:40 -0700
Subject: [PATCH 10/13] m

---
 .../runtimes/net/Generated/DDBEncryption/TypeConversion.cs  | 6 +++---
 .../WrappedDynamoDbItemEncryptor/TypeConversion.cs          | 6 +++---
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/TestVectors/runtimes/net/Generated/DDBEncryption/TypeConversion.cs b/TestVectors/runtimes/net/Generated/DDBEncryption/TypeConversion.cs
index 5e46a9aa1b..1ff2d1b401 100644
--- a/TestVectors/runtimes/net/Generated/DDBEncryption/TypeConversion.cs
+++ b/TestVectors/runtimes/net/Generated/DDBEncryption/TypeConversion.cs
@@ -2236,11 +2236,11 @@ public static software.amazon.cryptography.services.dynamodb.internaldafny.types
             }
             if (value.NULL == true)
             {
-                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL((bool)value.NULL));
+                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL(value.NULL));
             }
-            if (value.BOOL != null)
+            if (value.IsBOOLSet)
             {
-                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL((bool)value.BOOL));
+                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL(value.BOOL));
             }
             throw new System.ArgumentException("Invalid Amazon.DynamoDBv2.Model.AttributeValue state");
         }
diff --git a/TestVectors/runtimes/net/Generated/WrappedDynamoDbItemEncryptor/TypeConversion.cs b/TestVectors/runtimes/net/Generated/WrappedDynamoDbItemEncryptor/TypeConversion.cs
index f4ffbb586d..dc216416e2 100644
--- a/TestVectors/runtimes/net/Generated/WrappedDynamoDbItemEncryptor/TypeConversion.cs
+++ b/TestVectors/runtimes/net/Generated/WrappedDynamoDbItemEncryptor/TypeConversion.cs
@@ -716,11 +716,11 @@ public static software.amazon.cryptography.services.dynamodb.internaldafny.types
             }
             if (value.NULL == true)
             {
-                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL((bool)value.NULL));
+                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL(value.NULL));
             }
-            if (value.BOOL != null)
+            if (value.IsBOOLSet)
             {
-                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL((bool)value.BOOL));
+                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL(value.BOOL));
             }
             throw new System.ArgumentException("Invalid Amazon.DynamoDBv2.Model.AttributeValue state");
         }

From 98d7c33f17c92d685e63af182b8d8c5fdd37bd02 Mon Sep 17 00:00:00 2001
From: Jose Corella <jocorell@amazon.com>
Date: Fri, 20 Mar 2026 17:25:48 -0700
Subject: [PATCH 11/13] m

---
 .../DDBEncryption/dotnet/dafny-4.9.0.patch    | 49 +++++++++++++++++++
 .../dotnet/dafny-4.9.0.patch                  | 49 +++++++++++++++++++
 .../Generated/DDBEncryption/TypeConversion.cs | 16 +++---
 .../TypeConversion.cs                         | 16 +++---
 4 files changed, 110 insertions(+), 20 deletions(-)
 create mode 100644 TestVectors/codegen-patches/DDBEncryption/dotnet/dafny-4.9.0.patch
 create mode 100644 TestVectors/codegen-patches/WrappedDynamoDbItemEncryptor/dotnet/dafny-4.9.0.patch

diff --git a/TestVectors/codegen-patches/DDBEncryption/dotnet/dafny-4.9.0.patch b/TestVectors/codegen-patches/DDBEncryption/dotnet/dafny-4.9.0.patch
new file mode 100644
index 0000000000..8dc0f341e2
--- /dev/null
+++ b/TestVectors/codegen-patches/DDBEncryption/dotnet/dafny-4.9.0.patch
@@ -0,0 +1,49 @@
+diff --git a/TestVectors/runtimes/net/Generated/DDBEncryption/TypeConversion.cs b/TestVectors/runtimes/net/Generated/DDBEncryption/TypeConversion.cs
+index 1ff2d1b4..b2cef8b4 100644
+--- a/TestVectors/runtimes/net/Generated/DDBEncryption/TypeConversion.cs
++++ b/TestVectors/runtimes/net/Generated/DDBEncryption/TypeConversion.cs
+@@ -7,10 +7,6 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb.Wrapped
+ {
+     public static class TypeConversion
+     {
+-        private const string ISO8601DateFormat = "yyyy-MM-dd\\THH:mm:ss.fff\\Z";
+-
+-        private const string ISO8601DateFormatNoMS = "yyyy-MM-dd\\THH:mm:ss\\Z";
+-
+         public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.AsSet FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S5_AsSet(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IAsSet value)
+         {
+             software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.AsSet concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.AsSet)value; AWS.Cryptography.DbEncryptionSDK.DynamoDb.AsSet converted = new AWS.Cryptography.DbEncryptionSDK.DynamoDb.AsSet(); return converted;
+@@ -2214,15 +2210,15 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb.Wrapped
+             {
+                 return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_B(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M1_B(value.B));
+             }
+-            if (value.SS.Any())
++            if (value.SS != null && value.SS.Any())
+             {
+                 return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_SS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_SS(value.SS));
+             }
+-            if (value.NS.Any())
++            if (value.NS != null && value.NS.Any())
+             {
+                 return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_NS(value.NS));
+             }
+-            if (value.BS.Any())
++            if (value.BS != null && value.BS.Any())
+             {
+                 return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_BS(value.BS));
+             }
+@@ -2236,11 +2232,11 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb.Wrapped
+             }
+             if (value.NULL == true)
+             {
+-                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL(value.NULL));
++                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL((bool)value.NULL));
+             }
+-            if (value.IsBOOLSet)
++            if (value.BOOL != null)
+             {
+-                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL(value.BOOL));
++                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL((bool)value.BOOL));
+             }
+             throw new System.ArgumentException("Invalid Amazon.DynamoDBv2.Model.AttributeValue state");
+         }
diff --git a/TestVectors/codegen-patches/WrappedDynamoDbItemEncryptor/dotnet/dafny-4.9.0.patch b/TestVectors/codegen-patches/WrappedDynamoDbItemEncryptor/dotnet/dafny-4.9.0.patch
new file mode 100644
index 0000000000..e93f6db636
--- /dev/null
+++ b/TestVectors/codegen-patches/WrappedDynamoDbItemEncryptor/dotnet/dafny-4.9.0.patch
@@ -0,0 +1,49 @@
+diff --git a/TestVectors/runtimes/net/Generated/WrappedDynamoDbItemEncryptor/TypeConversion.cs b/TestVectors/runtimes/net/Generated/WrappedDynamoDbItemEncryptor/TypeConversion.cs
+index dc216416..51ad0d43 100644
+--- a/TestVectors/runtimes/net/Generated/WrappedDynamoDbItemEncryptor/TypeConversion.cs
++++ b/TestVectors/runtimes/net/Generated/WrappedDynamoDbItemEncryptor/TypeConversion.cs
+@@ -7,10 +7,6 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.Wrapped
+ {
+     public static class TypeConversion
+     {
+-        private const string ISO8601DateFormat = "yyyy-MM-dd\\THH:mm:ss.fff\\Z";
+-
+-        private const string ISO8601DateFormatNoMS = "yyyy-MM-dd\\THH:mm:ss\\Z";
+-
+         public static System.Collections.Generic.Dictionary<string, AWS.Cryptography.DbEncryptionSDK.StructuredEncryption.CryptoAction> FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S16_AttributeActions(Dafny.IMap<Dafny.ISequence<char>, software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny.types._ICryptoAction> value)
+         {
+             return value.ItemEnumerable.ToDictionary(pair => FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S16_AttributeActions__M3_key(pair.Car), pair => FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S16_AttributeActions__M5_value(pair.Cdr));
+@@ -694,15 +690,15 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.Wrapped
+             {
+                 return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_B(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M1_B(value.B));
+             }
+-            if (value.SS.Any())
++            if (value.SS != null && value.SS.Any())
+             {
+                 return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_SS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_SS(value.SS));
+             }
+-            if (value.NS.Any())
++            if (value.NS != null && value.NS.Any())
+             {
+                 return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_NS(value.NS));
+             }
+-            if (value.BS.Any())
++            if (value.BS != null && value.BS.Any())
+             {
+                 return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_BS(value.BS));
+             }
+@@ -716,11 +712,11 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.Wrapped
+             }
+             if (value.NULL == true)
+             {
+-                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL(value.NULL));
++                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL((bool)value.NULL));
+             }
+-            if (value.IsBOOLSet)
++            if (value.BOOL != null)
+             {
+-                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL(value.BOOL));
++                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL((bool)value.BOOL));
+             }
+             throw new System.ArgumentException("Invalid Amazon.DynamoDBv2.Model.AttributeValue state");
+         }
diff --git a/TestVectors/runtimes/net/Generated/DDBEncryption/TypeConversion.cs b/TestVectors/runtimes/net/Generated/DDBEncryption/TypeConversion.cs
index 1ff2d1b401..b2cef8b42a 100644
--- a/TestVectors/runtimes/net/Generated/DDBEncryption/TypeConversion.cs
+++ b/TestVectors/runtimes/net/Generated/DDBEncryption/TypeConversion.cs
@@ -7,10 +7,6 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb.Wrapped
 {
     public static class TypeConversion
     {
-        private const string ISO8601DateFormat = "yyyy-MM-dd\\THH:mm:ss.fff\\Z";
-
-        private const string ISO8601DateFormatNoMS = "yyyy-MM-dd\\THH:mm:ss\\Z";
-
         public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.AsSet FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S5_AsSet(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IAsSet value)
         {
             software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.AsSet concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.AsSet)value; AWS.Cryptography.DbEncryptionSDK.DynamoDb.AsSet converted = new AWS.Cryptography.DbEncryptionSDK.DynamoDb.AsSet(); return converted;
@@ -2214,15 +2210,15 @@ public static software.amazon.cryptography.services.dynamodb.internaldafny.types
             {
                 return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_B(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M1_B(value.B));
             }
-            if (value.SS.Any())
+            if (value.SS != null && value.SS.Any())
             {
                 return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_SS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_SS(value.SS));
             }
-            if (value.NS.Any())
+            if (value.NS != null && value.NS.Any())
             {
                 return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_NS(value.NS));
             }
-            if (value.BS.Any())
+            if (value.BS != null && value.BS.Any())
             {
                 return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_BS(value.BS));
             }
@@ -2236,11 +2232,11 @@ public static software.amazon.cryptography.services.dynamodb.internaldafny.types
             }
             if (value.NULL == true)
             {
-                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL(value.NULL));
+                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL((bool)value.NULL));
             }
-            if (value.IsBOOLSet)
+            if (value.BOOL != null)
             {
-                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL(value.BOOL));
+                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL((bool)value.BOOL));
             }
             throw new System.ArgumentException("Invalid Amazon.DynamoDBv2.Model.AttributeValue state");
         }
diff --git a/TestVectors/runtimes/net/Generated/WrappedDynamoDbItemEncryptor/TypeConversion.cs b/TestVectors/runtimes/net/Generated/WrappedDynamoDbItemEncryptor/TypeConversion.cs
index dc216416e2..51ad0d43a3 100644
--- a/TestVectors/runtimes/net/Generated/WrappedDynamoDbItemEncryptor/TypeConversion.cs
+++ b/TestVectors/runtimes/net/Generated/WrappedDynamoDbItemEncryptor/TypeConversion.cs
@@ -7,10 +7,6 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.Wrapped
 {
     public static class TypeConversion
     {
-        private const string ISO8601DateFormat = "yyyy-MM-dd\\THH:mm:ss.fff\\Z";
-
-        private const string ISO8601DateFormatNoMS = "yyyy-MM-dd\\THH:mm:ss\\Z";
-
         public static System.Collections.Generic.Dictionary<string, AWS.Cryptography.DbEncryptionSDK.StructuredEncryption.CryptoAction> FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S16_AttributeActions(Dafny.IMap<Dafny.ISequence<char>, software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny.types._ICryptoAction> value)
         {
             return value.ItemEnumerable.ToDictionary(pair => FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S16_AttributeActions__M3_key(pair.Car), pair => FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S16_AttributeActions__M5_value(pair.Cdr));
@@ -694,15 +690,15 @@ public static software.amazon.cryptography.services.dynamodb.internaldafny.types
             {
                 return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_B(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M1_B(value.B));
             }
-            if (value.SS.Any())
+            if (value.SS != null && value.SS.Any())
             {
                 return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_SS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_SS(value.SS));
             }
-            if (value.NS.Any())
+            if (value.NS != null && value.NS.Any())
             {
                 return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_NS(value.NS));
             }
-            if (value.BS.Any())
+            if (value.BS != null && value.BS.Any())
             {
                 return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_BS(value.BS));
             }
@@ -716,11 +712,11 @@ public static software.amazon.cryptography.services.dynamodb.internaldafny.types
             }
             if (value.NULL == true)
             {
-                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL(value.NULL));
+                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL((bool)value.NULL));
             }
-            if (value.IsBOOLSet)
+            if (value.BOOL != null)
             {
-                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL(value.BOOL));
+                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL((bool)value.BOOL));
             }
             throw new System.ArgumentException("Invalid Amazon.DynamoDBv2.Model.AttributeValue state");
         }

From 0998b5081caea240015c4e4dfe5c5dc8161f341c Mon Sep 17 00:00:00 2001
From: Jose Corella <jocorell@amazon.com>
Date: Mon, 30 Mar 2026 14:05:45 -0700
Subject: [PATCH 12/13] point to wip branch of smithy-dafny

---
 submodules/smithy-dafny | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/submodules/smithy-dafny b/submodules/smithy-dafny
index 351cff6fbc..d0f6d61d3b 160000
--- a/submodules/smithy-dafny
+++ b/submodules/smithy-dafny
@@ -1 +1 @@
-Subproject commit 351cff6fbcf94de451dd24b1f69de51f2ed20ffb
+Subproject commit d0f6d61d3b030bb9cc7b93cee5e69fb591a246b6

From c827939b077a6008ccd2c7ae8b43bc2e9328cd23 Mon Sep 17 00:00:00 2001
From: Jose Corella <jocorell@amazon.com>
Date: Mon, 30 Mar 2026 15:22:06 -0700
Subject: [PATCH 13/13] update

---
 .../dotnet/dafny-4.9.0.patch                  | 42 ++--------------
 .../dotnet/dafny-4.9.0.patch                  | 42 ++--------------
 .../dotnet/dafny-4.9.0.patch                  | 42 ++--------------
 .../DynamoDbEncryption/TypeConversion.cs      | 10 ++--
 .../TypeConversion.cs                         | 18 +++----
 .../DynamoDbItemEncryptor/TypeConversion.cs   | 10 ++--
 .../DDBEncryption/dotnet/dafny-4.9.0.patch    | 49 -------------------
 .../dotnet/dafny-4.9.0.patch                  | 49 -------------------
 .../Generated/DDBEncryption/TypeConversion.cs | 14 ++++--
 .../TypeConversion.cs                         | 14 ++++--
 10 files changed, 49 insertions(+), 241 deletions(-)
 delete mode 100644 TestVectors/codegen-patches/DDBEncryption/dotnet/dafny-4.9.0.patch
 delete mode 100644 TestVectors/codegen-patches/WrappedDynamoDbItemEncryptor/dotnet/dafny-4.9.0.patch

diff --git a/DynamoDbEncryption/codegen-patches/DynamoDbEncryption/dotnet/dafny-4.9.0.patch b/DynamoDbEncryption/codegen-patches/DynamoDbEncryption/dotnet/dafny-4.9.0.patch
index 957ff09b1d..31f95b6309 100644
--- a/DynamoDbEncryption/codegen-patches/DynamoDbEncryption/dotnet/dafny-4.9.0.patch
+++ b/DynamoDbEncryption/codegen-patches/DynamoDbEncryption/dotnet/dafny-4.9.0.patch
@@ -1,7 +1,7 @@
-diff --git a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs
-index 82bbffe6..90bdb825 100644
---- a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs
-+++ b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs
+diff --git b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs
+index 82bbffe6a..87ae5c0e9 100644
+--- b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs
++++ a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs
 @@ -7,10 +7,6 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb
  {
    public static class TypeConversion
@@ -13,37 +13,3 @@ index 82bbffe6..90bdb825 100644
      public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.AsSet FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S5_AsSet(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IAsSet value)
      {
        software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.AsSet concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.AsSet)value; AWS.Cryptography.DbEncryptionSDK.DynamoDb.AsSet converted = new AWS.Cryptography.DbEncryptionSDK.DynamoDb.AsSet(); return converted;
-@@ -2236,15 +2232,15 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb
-       {
-         return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_B(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M1_B(value.B));
-       }
--      if (value.SS.Any())
-+      if (value.SS != null && value.SS.Any())
-       {
-         return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_SS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_SS(value.SS));
-       }
--      if (value.NS.Any())
-+      if (value.NS != null && value.NS.Any())
-       {
-         return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_NS(value.NS));
-       }
--      if (value.BS.Any())
-+      if (value.BS != null && value.BS.Any())
-       {
-         return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_BS(value.BS));
-       }
-@@ -2258,11 +2254,11 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb
-       }
-       if (value.NULL == true)
-       {
--        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL(value.NULL));
-+        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL((bool)value.NULL));
-       }
--      if (value.IsBOOLSet)
-+      if (value.BOOL != null)
-       {
--        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL(value.BOOL));
-+        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL((bool)value.BOOL));
-       }
-       throw new System.ArgumentException("Invalid Amazon.DynamoDBv2.Model.AttributeValue state");
-     }
diff --git a/DynamoDbEncryption/codegen-patches/DynamoDbEncryptionTransforms/dotnet/dafny-4.9.0.patch b/DynamoDbEncryption/codegen-patches/DynamoDbEncryptionTransforms/dotnet/dafny-4.9.0.patch
index 657c859159..97fcc23806 100644
--- a/DynamoDbEncryption/codegen-patches/DynamoDbEncryptionTransforms/dotnet/dafny-4.9.0.patch
+++ b/DynamoDbEncryption/codegen-patches/DynamoDbEncryptionTransforms/dotnet/dafny-4.9.0.patch
@@ -1,7 +1,7 @@
-diff --git a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs
-index 08aa5919..afcaa92c 100644
---- a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs
-+++ b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs
+diff --git b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs
+index 08aa59190..fa42225e6 100644
+--- b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs
++++ a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs
 @@ -7,10 +7,6 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb.Transforms
  {
    public static class TypeConversion
@@ -13,37 +13,3 @@ index 08aa5919..afcaa92c 100644
      public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.AsSet FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S5_AsSet(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IAsSet value)
      {
        software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.AsSet concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.AsSet)value; AWS.Cryptography.DbEncryptionSDK.DynamoDb.AsSet converted = new AWS.Cryptography.DbEncryptionSDK.DynamoDb.AsSet(); return converted;
-@@ -3200,15 +3196,15 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb.Transforms
-       {
-         return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_B(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M1_B(value.B));
-       }
--      if (value.SS.Any())
-+      if (value.SS != null && value.SS.Any())
-       {
-         return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_SS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_SS(value.SS));
-       }
--      if (value.NS.Any())
-+      if (value.NS != null && value.NS.Any())
-       {
-         return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_NS(value.NS));
-       }
--      if (value.BS.Any())
-+      if (value.BS != null && value.BS.Any())
-       {
-         return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_BS(value.BS));
-       }
-@@ -3222,11 +3218,11 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb.Transforms
-       }
-       if (value.NULL == true)
-       {
--        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL(value.NULL));
-+        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL((bool)value.NULL));
-       }
--      if (value.IsBOOLSet)
-+      if (value.BOOL != null)
-       {
--        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL(value.BOOL));
-+        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL((bool)value.BOOL));
-       }
-       throw new System.ArgumentException("Invalid Amazon.DynamoDBv2.Model.AttributeValue state");
-     }
diff --git a/DynamoDbEncryption/codegen-patches/DynamoDbItemEncryptor/dotnet/dafny-4.9.0.patch b/DynamoDbEncryption/codegen-patches/DynamoDbItemEncryptor/dotnet/dafny-4.9.0.patch
index 8e47a1219d..bfffccb499 100644
--- a/DynamoDbEncryption/codegen-patches/DynamoDbItemEncryptor/dotnet/dafny-4.9.0.patch
+++ b/DynamoDbEncryption/codegen-patches/DynamoDbItemEncryptor/dotnet/dafny-4.9.0.patch
@@ -1,7 +1,7 @@
-diff --git a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs
-index b4a90d1b..7f4207c2 100644
---- a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs
-+++ b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs
+diff --git b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs
+index b4a90d1b4..b5d5046a4 100644
+--- b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs
++++ a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs
 @@ -7,10 +7,6 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor
  {
    public static class TypeConversion
@@ -13,37 +13,3 @@ index b4a90d1b..7f4207c2 100644
      public static System.Collections.Generic.Dictionary<string, AWS.Cryptography.DbEncryptionSDK.StructuredEncryption.CryptoAction> FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S16_AttributeActions(Dafny.IMap<Dafny.ISequence<char>, software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny.types._ICryptoAction> value)
      {
        return value.ItemEnumerable.ToDictionary(pair => FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S16_AttributeActions__M3_key(pair.Car), pair => FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S16_AttributeActions__M5_value(pair.Cdr));
-@@ -702,15 +698,15 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor
-       {
-         return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_B(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M1_B(value.B));
-       }
--      if (value.SS.Any())
-+      if (value.SS != null && value.SS.Any())
-       {
-         return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_SS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_SS(value.SS));
-       }
--      if (value.NS.Any())
-+      if (value.NS != null && value.NS.Any())
-       {
-         return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_NS(value.NS));
-       }
--      if (value.BS.Any())
-+      if (value.BS != null && value.BS.Any())
-       {
-         return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_BS(value.BS));
-       }
-@@ -724,11 +720,11 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor
-       }
-       if (value.NULL == true)
-       {
--        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL(value.NULL));
-+        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL((bool)value.NULL));
-       }
--      if (value.IsBOOLSet)
-+      if (value.BOOL != null)
-       {
--        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL(value.BOOL));
-+        return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL((bool)value.BOOL));
-       }
-       throw new System.ArgumentException("Invalid Amazon.DynamoDBv2.Model.AttributeValue state");
-     }
diff --git a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs
index 90bdb825b4..8e4b720906 100644
--- a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs
+++ b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs
@@ -2232,23 +2232,23 @@ public static software.amazon.cryptography.services.dynamodb.internaldafny.types
       {
         return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_B(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M1_B(value.B));
       }
-      if (value.SS != null && value.SS.Any())
+      if (value.SS != null)
       {
         return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_SS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_SS(value.SS));
       }
-      if (value.NS != null && value.NS.Any())
+      if (value.NS != null)
       {
         return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_NS(value.NS));
       }
-      if (value.BS != null && value.BS.Any())
+      if (value.BS != null)
       {
         return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_BS(value.BS));
       }
-      if (value.IsMSet)
+      if (value.M != null)
       {
         return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_M(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M1_M(value.M));
       }
-      if (value.IsLSet)
+      if (value.L != null)
       {
         return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_L(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M1_L(value.L));
       }
diff --git a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs
index afcaa92cd6..cc9a449929 100644
--- a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs
+++ b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs
@@ -3196,23 +3196,23 @@ public static software.amazon.cryptography.services.dynamodb.internaldafny.types
       {
         return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_B(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M1_B(value.B));
       }
-      if (value.SS != null && value.SS.Any())
+      if (value.SS != null)
       {
         return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_SS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_SS(value.SS));
       }
-      if (value.NS != null && value.NS.Any())
+      if (value.NS != null)
       {
         return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_NS(value.NS));
       }
-      if (value.BS != null && value.BS.Any())
+      if (value.BS != null)
       {
         return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_BS(value.BS));
       }
-      if (value.IsMSet)
+      if (value.M != null)
       {
         return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_M(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M1_M(value.M));
       }
-      if (value.IsLSet)
+      if (value.L != null)
       {
         return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_L(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M1_L(value.L));
       }
@@ -5693,7 +5693,7 @@ public static software.amazon.cryptography.services.dynamodb.internaldafny.types
       string var_indexName = value.IndexName != null ? value.IndexName : (string)null;
       Amazon.DynamoDBv2.Select var_select = value.Select != null ? value.Select : (Amazon.DynamoDBv2.Select)null;
       System.Collections.Generic.List<string> var_attributesToGet = value.AttributesToGet != null ? value.AttributesToGet : (System.Collections.Generic.List<string>)null;
-      int? var_limit = value.IsLimitSet ? value.Limit : (int?)null;
+      int? var_limit = value.Limit != null ? value.Limit : (int?)null;
       bool? var_consistentRead = value.ConsistentRead != null ? value.ConsistentRead : (bool?)null;
       System.Collections.Generic.Dictionary<string, Amazon.DynamoDBv2.Model.Condition> var_keyConditions = value.KeyConditions != null ? value.KeyConditions : (System.Collections.Generic.Dictionary<string, Amazon.DynamoDBv2.Model.Condition>)null;
       System.Collections.Generic.Dictionary<string, Amazon.DynamoDBv2.Model.Condition> var_queryFilter = value.QueryFilter != null ? value.QueryFilter : (System.Collections.Generic.Dictionary<string, Amazon.DynamoDBv2.Model.Condition>)null;
@@ -5982,14 +5982,14 @@ public static software.amazon.cryptography.services.dynamodb.internaldafny.types
 
       string var_indexName = value.IndexName != null ? value.IndexName : (string)null;
       System.Collections.Generic.List<string> var_attributesToGet = value.AttributesToGet != null ? value.AttributesToGet : (System.Collections.Generic.List<string>)null;
-      int? var_limit = value.IsLimitSet ? value.Limit : (int?)null;
+      int? var_limit = value.Limit != null ? value.Limit : (int?)null;
       Amazon.DynamoDBv2.Select var_select = value.Select != null ? value.Select : (Amazon.DynamoDBv2.Select)null;
       System.Collections.Generic.Dictionary<string, Amazon.DynamoDBv2.Model.Condition> var_scanFilter = value.ScanFilter != null ? value.ScanFilter : (System.Collections.Generic.Dictionary<string, Amazon.DynamoDBv2.Model.Condition>)null;
       Amazon.DynamoDBv2.ConditionalOperator var_conditionalOperator = value.ConditionalOperator != null ? value.ConditionalOperator : (Amazon.DynamoDBv2.ConditionalOperator)null;
       System.Collections.Generic.Dictionary<string, Amazon.DynamoDBv2.Model.AttributeValue> var_exclusiveStartKey = value.ExclusiveStartKey != null ? value.ExclusiveStartKey : (System.Collections.Generic.Dictionary<string, Amazon.DynamoDBv2.Model.AttributeValue>)null;
       Amazon.DynamoDBv2.ReturnConsumedCapacity var_returnConsumedCapacity = value.ReturnConsumedCapacity != null ? value.ReturnConsumedCapacity : (Amazon.DynamoDBv2.ReturnConsumedCapacity)null;
-      int? var_totalSegments = value.IsTotalSegmentsSet ? value.TotalSegments : (int?)null;
-      int? var_segment = value.IsSegmentSet ? value.Segment : (int?)null;
+      int? var_totalSegments = value.TotalSegments != null ? value.TotalSegments : (int?)null;
+      int? var_segment = value.Segment != null ? value.Segment : (int?)null;
       string var_projectionExpression = value.ProjectionExpression != null ? value.ProjectionExpression : (string)null;
       string var_filterExpression = value.FilterExpression != null ? value.FilterExpression : (string)null;
       System.Collections.Generic.Dictionary<string, string> var_expressionAttributeNames = value.ExpressionAttributeNames != null ? value.ExpressionAttributeNames : (System.Collections.Generic.Dictionary<string, string>)null;
diff --git a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs
index 7f4207c213..ae5eb4f825 100644
--- a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs
+++ b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs
@@ -698,23 +698,23 @@ public static software.amazon.cryptography.services.dynamodb.internaldafny.types
       {
         return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_B(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M1_B(value.B));
       }
-      if (value.SS != null && value.SS.Any())
+      if (value.SS != null)
       {
         return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_SS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_SS(value.SS));
       }
-      if (value.NS != null && value.NS.Any())
+      if (value.NS != null)
       {
         return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_NS(value.NS));
       }
-      if (value.BS != null && value.BS.Any())
+      if (value.BS != null)
       {
         return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_BS(value.BS));
       }
-      if (value.IsMSet)
+      if (value.M != null)
       {
         return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_M(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M1_M(value.M));
       }
-      if (value.IsLSet)
+      if (value.L != null)
       {
         return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_L(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M1_L(value.L));
       }
diff --git a/TestVectors/codegen-patches/DDBEncryption/dotnet/dafny-4.9.0.patch b/TestVectors/codegen-patches/DDBEncryption/dotnet/dafny-4.9.0.patch
deleted file mode 100644
index 8dc0f341e2..0000000000
--- a/TestVectors/codegen-patches/DDBEncryption/dotnet/dafny-4.9.0.patch
+++ /dev/null
@@ -1,49 +0,0 @@
-diff --git a/TestVectors/runtimes/net/Generated/DDBEncryption/TypeConversion.cs b/TestVectors/runtimes/net/Generated/DDBEncryption/TypeConversion.cs
-index 1ff2d1b4..b2cef8b4 100644
---- a/TestVectors/runtimes/net/Generated/DDBEncryption/TypeConversion.cs
-+++ b/TestVectors/runtimes/net/Generated/DDBEncryption/TypeConversion.cs
-@@ -7,10 +7,6 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb.Wrapped
- {
-     public static class TypeConversion
-     {
--        private const string ISO8601DateFormat = "yyyy-MM-dd\\THH:mm:ss.fff\\Z";
--
--        private const string ISO8601DateFormatNoMS = "yyyy-MM-dd\\THH:mm:ss\\Z";
--
-         public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.AsSet FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S5_AsSet(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IAsSet value)
-         {
-             software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.AsSet concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.AsSet)value; AWS.Cryptography.DbEncryptionSDK.DynamoDb.AsSet converted = new AWS.Cryptography.DbEncryptionSDK.DynamoDb.AsSet(); return converted;
-@@ -2214,15 +2210,15 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb.Wrapped
-             {
-                 return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_B(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M1_B(value.B));
-             }
--            if (value.SS.Any())
-+            if (value.SS != null && value.SS.Any())
-             {
-                 return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_SS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_SS(value.SS));
-             }
--            if (value.NS.Any())
-+            if (value.NS != null && value.NS.Any())
-             {
-                 return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_NS(value.NS));
-             }
--            if (value.BS.Any())
-+            if (value.BS != null && value.BS.Any())
-             {
-                 return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_BS(value.BS));
-             }
-@@ -2236,11 +2232,11 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb.Wrapped
-             }
-             if (value.NULL == true)
-             {
--                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL(value.NULL));
-+                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL((bool)value.NULL));
-             }
--            if (value.IsBOOLSet)
-+            if (value.BOOL != null)
-             {
--                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL(value.BOOL));
-+                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL((bool)value.BOOL));
-             }
-             throw new System.ArgumentException("Invalid Amazon.DynamoDBv2.Model.AttributeValue state");
-         }
diff --git a/TestVectors/codegen-patches/WrappedDynamoDbItemEncryptor/dotnet/dafny-4.9.0.patch b/TestVectors/codegen-patches/WrappedDynamoDbItemEncryptor/dotnet/dafny-4.9.0.patch
deleted file mode 100644
index e93f6db636..0000000000
--- a/TestVectors/codegen-patches/WrappedDynamoDbItemEncryptor/dotnet/dafny-4.9.0.patch
+++ /dev/null
@@ -1,49 +0,0 @@
-diff --git a/TestVectors/runtimes/net/Generated/WrappedDynamoDbItemEncryptor/TypeConversion.cs b/TestVectors/runtimes/net/Generated/WrappedDynamoDbItemEncryptor/TypeConversion.cs
-index dc216416..51ad0d43 100644
---- a/TestVectors/runtimes/net/Generated/WrappedDynamoDbItemEncryptor/TypeConversion.cs
-+++ b/TestVectors/runtimes/net/Generated/WrappedDynamoDbItemEncryptor/TypeConversion.cs
-@@ -7,10 +7,6 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.Wrapped
- {
-     public static class TypeConversion
-     {
--        private const string ISO8601DateFormat = "yyyy-MM-dd\\THH:mm:ss.fff\\Z";
--
--        private const string ISO8601DateFormatNoMS = "yyyy-MM-dd\\THH:mm:ss\\Z";
--
-         public static System.Collections.Generic.Dictionary<string, AWS.Cryptography.DbEncryptionSDK.StructuredEncryption.CryptoAction> FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S16_AttributeActions(Dafny.IMap<Dafny.ISequence<char>, software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny.types._ICryptoAction> value)
-         {
-             return value.ItemEnumerable.ToDictionary(pair => FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S16_AttributeActions__M3_key(pair.Car), pair => FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S16_AttributeActions__M5_value(pair.Cdr));
-@@ -694,15 +690,15 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.Wrapped
-             {
-                 return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_B(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M1_B(value.B));
-             }
--            if (value.SS.Any())
-+            if (value.SS != null && value.SS.Any())
-             {
-                 return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_SS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_SS(value.SS));
-             }
--            if (value.NS.Any())
-+            if (value.NS != null && value.NS.Any())
-             {
-                 return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_NS(value.NS));
-             }
--            if (value.BS.Any())
-+            if (value.BS != null && value.BS.Any())
-             {
-                 return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_BS(value.BS));
-             }
-@@ -716,11 +712,11 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.Wrapped
-             }
-             if (value.NULL == true)
-             {
--                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL(value.NULL));
-+                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL((bool)value.NULL));
-             }
--            if (value.IsBOOLSet)
-+            if (value.BOOL != null)
-             {
--                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL(value.BOOL));
-+                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL((bool)value.BOOL));
-             }
-             throw new System.ArgumentException("Invalid Amazon.DynamoDBv2.Model.AttributeValue state");
-         }
diff --git a/TestVectors/runtimes/net/Generated/DDBEncryption/TypeConversion.cs b/TestVectors/runtimes/net/Generated/DDBEncryption/TypeConversion.cs
index b2cef8b42a..1a1ce70140 100644
--- a/TestVectors/runtimes/net/Generated/DDBEncryption/TypeConversion.cs
+++ b/TestVectors/runtimes/net/Generated/DDBEncryption/TypeConversion.cs
@@ -7,6 +7,10 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb.Wrapped
 {
     public static class TypeConversion
     {
+        private const string ISO8601DateFormat = "yyyy-MM-dd\\THH:mm:ss.fff\\Z";
+
+        private const string ISO8601DateFormatNoMS = "yyyy-MM-dd\\THH:mm:ss\\Z";
+
         public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.AsSet FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S5_AsSet(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IAsSet value)
         {
             software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.AsSet concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.AsSet)value; AWS.Cryptography.DbEncryptionSDK.DynamoDb.AsSet converted = new AWS.Cryptography.DbEncryptionSDK.DynamoDb.AsSet(); return converted;
@@ -2210,23 +2214,23 @@ public static software.amazon.cryptography.services.dynamodb.internaldafny.types
             {
                 return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_B(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M1_B(value.B));
             }
-            if (value.SS != null && value.SS.Any())
+            if (value.SS != null)
             {
                 return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_SS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_SS(value.SS));
             }
-            if (value.NS != null && value.NS.Any())
+            if (value.NS != null)
             {
                 return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_NS(value.NS));
             }
-            if (value.BS != null && value.BS.Any())
+            if (value.BS != null)
             {
                 return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_BS(value.BS));
             }
-            if (value.IsMSet)
+            if (value.M != null)
             {
                 return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_M(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M1_M(value.M));
             }
-            if (value.IsLSet)
+            if (value.L != null)
             {
                 return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_L(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M1_L(value.L));
             }
diff --git a/TestVectors/runtimes/net/Generated/WrappedDynamoDbItemEncryptor/TypeConversion.cs b/TestVectors/runtimes/net/Generated/WrappedDynamoDbItemEncryptor/TypeConversion.cs
index 51ad0d43a3..7af856cea3 100644
--- a/TestVectors/runtimes/net/Generated/WrappedDynamoDbItemEncryptor/TypeConversion.cs
+++ b/TestVectors/runtimes/net/Generated/WrappedDynamoDbItemEncryptor/TypeConversion.cs
@@ -7,6 +7,10 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.Wrapped
 {
     public static class TypeConversion
     {
+        private const string ISO8601DateFormat = "yyyy-MM-dd\\THH:mm:ss.fff\\Z";
+
+        private const string ISO8601DateFormatNoMS = "yyyy-MM-dd\\THH:mm:ss\\Z";
+
         public static System.Collections.Generic.Dictionary<string, AWS.Cryptography.DbEncryptionSDK.StructuredEncryption.CryptoAction> FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S16_AttributeActions(Dafny.IMap<Dafny.ISequence<char>, software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny.types._ICryptoAction> value)
         {
             return value.ItemEnumerable.ToDictionary(pair => FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S16_AttributeActions__M3_key(pair.Car), pair => FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S16_AttributeActions__M5_value(pair.Cdr));
@@ -690,23 +694,23 @@ public static software.amazon.cryptography.services.dynamodb.internaldafny.types
             {
                 return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_B(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M1_B(value.B));
             }
-            if (value.SS != null && value.SS.Any())
+            if (value.SS != null)
             {
                 return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_SS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_SS(value.SS));
             }
-            if (value.NS != null && value.NS.Any())
+            if (value.NS != null)
             {
                 return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_NS(value.NS));
             }
-            if (value.BS != null && value.BS.Any())
+            if (value.BS != null)
             {
                 return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_BS(value.BS));
             }
-            if (value.IsMSet)
+            if (value.M != null)
             {
                 return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_M(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M1_M(value.M));
             }
-            if (value.IsLSet)
+            if (value.L != null)
             {
                 return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_L(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M1_L(value.L));
             }