From b3c0a7b5d0562f1c916a772b3c2c4c89f6679f5c Mon Sep 17 00:00:00 2001
From: Andy Jewell <ajewell@amazon.com>
Date: Thu, 2 Oct 2025 10:15:30 -0400
Subject: [PATCH 1/8] chore(dotnet): release 4.1.1

---
 AwsEncryptionSDK/runtimes/net/ESDK.csproj | 8 +++-----
 mpl                                       | 2 +-
 2 files changed, 4 insertions(+), 6 deletions(-)

diff --git a/AwsEncryptionSDK/runtimes/net/ESDK.csproj b/AwsEncryptionSDK/runtimes/net/ESDK.csproj
index d0332e517..6cd2adfa3 100644
--- a/AwsEncryptionSDK/runtimes/net/ESDK.csproj
+++ b/AwsEncryptionSDK/runtimes/net/ESDK.csproj
@@ -8,7 +8,7 @@
       <EnableDefaultCompileItems>false</EnableDefaultCompileItems>
       <IsPackable>true</IsPackable>
       
-      <Version>4.1.0</Version>
+      <Version>4.1.1</Version>
 
       <AssemblyName>AWS.Cryptography.EncryptionSDK</AssemblyName>
       <PackageId>AWS.Cryptography.EncryptionSDK</PackageId>
@@ -29,11 +29,9 @@
   </PropertyGroup>
 
   <ItemGroup>
-      <!-- TODO: manually upgraded to match the latest from MPL, is that reasonable? -->
-      <PackageReference Include="AWSSDK.Core" Version="3.7.300.2" />
-      <PackageReference Include="DafnyRuntime" Version="4.2.0" />
+      <PackageReference Include="DafnyRuntime" Version="[4.2.0,4.8.0]" />
       <PackageReference Include="BouncyCastle.Cryptography" Version="2.2.1" />
-      <PackageReference Include="AWS.Cryptography.MaterialProviders" Version="1.3.0" />
+      <PackageReference Include="AWS.Cryptography.MaterialProviders" Version="[1.7.6]" />
       <!--
         System.Collections.Immutable can be removed once dafny.msbuild is updated with
         https://github.com/dafny-lang/dafny.msbuild/pull/10 and versioned
diff --git a/mpl b/mpl
index 6d0f00dfa..df37a708c 160000
--- a/mpl
+++ b/mpl
@@ -1 +1 @@
-Subproject commit 6d0f00dfa8c31d490d89399cc104e7d4eac5b9b4
+Subproject commit df37a708cae023ae88a7d0dd0f3ecb59753be5f5

From f1b5e32c44f070b54a96b3e4fd132e8b8f964ffb Mon Sep 17 00:00:00 2001
From: Andy Jewell <ajewell@amazon.com>
Date: Fri, 3 Oct 2025 13:24:00 -0400
Subject: [PATCH 2/8] m

---
 AwsEncryptionSDK/runtimes/net/CHANGELOG.md | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/AwsEncryptionSDK/runtimes/net/CHANGELOG.md b/AwsEncryptionSDK/runtimes/net/CHANGELOG.md
index bf9b9eb6a..741db3da1 100644
--- a/AwsEncryptionSDK/runtimes/net/CHANGELOG.md
+++ b/AwsEncryptionSDK/runtimes/net/CHANGELOG.md
@@ -1,5 +1,9 @@
 # Changelog
 
+## 4.1.1
+
+Update .csproj files to prevent use of AWS-SDK-NET V4
+
 ## 4.1.0
 
 ### Notes

From 361ab91a232f1d189d50789148dd5824269d2b79 Mon Sep 17 00:00:00 2001
From: Andy Jewell <ajewell@amazon.com>
Date: Mon, 6 Oct 2025 12:57:31 -0400
Subject: [PATCH 3/8] m

---
 AwsEncryptionSDK/runtimes/net/ESDK.csproj | 1 -
 1 file changed, 1 deletion(-)

diff --git a/AwsEncryptionSDK/runtimes/net/ESDK.csproj b/AwsEncryptionSDK/runtimes/net/ESDK.csproj
index 6cd2adfa3..9e8ac6774 100644
--- a/AwsEncryptionSDK/runtimes/net/ESDK.csproj
+++ b/AwsEncryptionSDK/runtimes/net/ESDK.csproj
@@ -30,7 +30,6 @@
 
   <ItemGroup>
       <PackageReference Include="DafnyRuntime" Version="[4.2.0,4.8.0]" />
-      <PackageReference Include="BouncyCastle.Cryptography" Version="2.2.1" />
       <PackageReference Include="AWS.Cryptography.MaterialProviders" Version="[1.7.6]" />
       <!--
         System.Collections.Immutable can be removed once dafny.msbuild is updated with

From 374e81c7d9e779b1873f6b7c1bed3f4fd566ee85 Mon Sep 17 00:00:00 2001
From: Andy Jewell <ajewell@amazon.com>
Date: Mon, 6 Oct 2025 16:30:13 -0400
Subject: [PATCH 4/8] rename Primitives

---
 .../dafny/AwsEncryptionSdk/src/AwsEncryptionSdkOperations.dfy   | 2 +-
 AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/EncryptDecrypt.dfy  | 2 +-
 AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Index.dfy           | 2 +-
 AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/KeyDerivation.dfy   | 2 +-
 AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/MessageBody.dfy     | 2 +-
 AwsEncryptionSDK/dafny/AwsEncryptionSdk/test/Fixtures.dfy       | 2 +-
 6 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/AwsEncryptionSdkOperations.dfy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/AwsEncryptionSdkOperations.dfy
index 695b3379d..1a89973e7 100644
--- a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/AwsEncryptionSdkOperations.dfy
+++ b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/AwsEncryptionSdkOperations.dfy
@@ -17,7 +17,7 @@ include "Serialize/EncryptionContext.dfy"
 
 module AwsEncryptionSdkOperations refines AbstractAwsCryptographyEncryptionSdkOperations {
 
-  import Aws.Cryptography.Primitives
+  import Primitives = AtomicPrimitives
   import MPL = AwsCryptographyMaterialProvidersTypes
   import MaterialProviders
   import EncryptDecryptHelpers
diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/EncryptDecrypt.dfy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/EncryptDecrypt.dfy
index 6a3762abe..5825b02cf 100644
--- a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/EncryptDecrypt.dfy
+++ b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/EncryptDecrypt.dfy
@@ -15,7 +15,7 @@ module EncryptDecryptHelpers {
   import Types = AwsCryptographyEncryptionSdkTypes
   import MPL = AwsCryptographyMaterialProvidersTypes
   import MaterialProviders
-  import Aws.Cryptography.Primitives
+  import Primitives = AtomicPrimitives
   import MessageBody
   import SerializableTypes
   import opened SerializeFunctions
diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Index.dfy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Index.dfy
index cf46c3714..ab851b1a8 100644
--- a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Index.dfy
+++ b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Index.dfy
@@ -7,7 +7,7 @@ module
   {:extern "software.amazon.cryptography.encryptionsdk.internaldafny" }
   EncryptionSdk refines AbstractAwsCryptographyEncryptionSdkService {
   import Operations = AwsEncryptionSdkOperations
-  import Aws.Cryptography.Primitives
+  import Primitives = AtomicPrimitives
   import MaterialProviders
   import AwsCryptographyMaterialProvidersTypes
 
diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/KeyDerivation.dfy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/KeyDerivation.dfy
index 2607f528c..2456f756e 100644
--- a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/KeyDerivation.dfy
+++ b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/KeyDerivation.dfy
@@ -12,7 +12,7 @@ module KeyDerivation {
   import Types = AwsCryptographyEncryptionSdkTypes
   import MPL = AwsCryptographyMaterialProvidersTypes
   import AwsCryptographyPrimitivesTypes
-  import Aws.Cryptography.Primitives
+  import Primitives = AtomicPrimitives
   import HeaderTypes
   import SerializableTypes
 
diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/MessageBody.dfy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/MessageBody.dfy
index ca62a4d66..794c22838 100644
--- a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/MessageBody.dfy
+++ b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/MessageBody.dfy
@@ -22,7 +22,7 @@ module MessageBody {
   import opened UInt = StandardLibrary.UInt
   import Types = AwsCryptographyEncryptionSdkTypes
   import MPL = AwsCryptographyMaterialProvidersTypes
-  import Aws.Cryptography.Primitives
+  import Primitives = AtomicPrimitives
   import Streams
   import UTF8
   import SerializableTypes
diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/test/Fixtures.dfy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/test/Fixtures.dfy
index b7edf42a6..a7d7d5652 100644
--- a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/test/Fixtures.dfy
+++ b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/test/Fixtures.dfy
@@ -9,7 +9,7 @@ module Fixtures {
   import primitivesTypes = AwsCryptographyPrimitivesTypes
   import mplTypes = AwsCryptographyMaterialProvidersTypes
   import opened UInt = StandardLibrary.UInt
-  import Aws.Cryptography.Primitives
+  import Primitives = AtomicPrimitives
   
   // The following are test resources that exist in tests accounts:
 

From f195e471f789081b21fda68977aa9713a8adca50 Mon Sep 17 00:00:00 2001
From: Andy Jewell <ajewell@amazon.com>
Date: Mon, 6 Oct 2025 16:34:08 -0400
Subject: [PATCH 5/8] m

---
 .github/workflows/pull.yml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/.github/workflows/pull.yml b/.github/workflows/pull.yml
index ad9a6d9ca..03f6e18c3 100644
--- a/.github/workflows/pull.yml
+++ b/.github/workflows/pull.yml
@@ -8,20 +8,20 @@ jobs:
   pr-ci-codegen:
     uses: ./.github/workflows/library_codegen.yml
     with:
-      dafny: '4.2.0'
+      dafny: '4.9.0'
   pr-ci-verification:
     uses: ./.github/workflows/library_dafny_verification.yml
     with:
-      dafny: '4.2.0'
+      dafny: '4.9.0'
   # pr-ci-java:
   #   uses: ./.github/workflows/library_java_tests.yml
   #   with:
-  #     dafny: '4.2.0'
+  #     dafny: '4.9.0'
   pr-ci-net:
     uses: ./.github/workflows/library_net_tests.yml
     with:
-      dafny: '4.2.0'
+      dafny: '4.9.0'
   pr-test-vectors:
     uses: ./.github/workflows/library_interop_tests.yml
     with:
-      dafny: '4.2.0'
+      dafny: '4.9.0'

From 1742498b24836060a949dd750502fd3c1ba83a59 Mon Sep 17 00:00:00 2001
From: Andy Jewell <ajewell@amazon.com>
Date: Mon, 6 Oct 2025 16:48:53 -0400
Subject: [PATCH 6/8] m

---
 libraries | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/libraries b/libraries
index 05beef6e2..fabf44d71 160000
--- a/libraries
+++ b/libraries
@@ -1 +1 @@
-Subproject commit 05beef6e25a5583abdd4c70c6b09404dfe2fb4cb
+Subproject commit fabf44d71c6d5065b0021cb4e5e96b5128c87d39

From 9f38f8082aa8cee813f467443de7724333666fdd Mon Sep 17 00:00:00 2001
From: Andy Jewell <ajewell@amazon.com>
Date: Mon, 6 Oct 2025 18:18:36 -0400
Subject: [PATCH 7/8] m

---
 SharedMakefileV2.mk | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

diff --git a/SharedMakefileV2.mk b/SharedMakefileV2.mk
index 94138dfc6..66d54cf49 100644
--- a/SharedMakefileV2.mk
+++ b/SharedMakefileV2.mk
@@ -6,9 +6,19 @@
 # that are shared by all libraries in this repo.
 PROJECT_ROOT := $(abspath $(dir $(abspath $(lastword $(MAKEFILE_LIST)))))
 
-SMITHY_DAFNY_ROOT := $(PROJECT_ROOT)/smithy-dafny
+SMITHY_DAFNY_ROOT := $(PROJECT_ROOT)/mpl/smithy-dafny
 GRADLEW := ./runtimes/java/gradlew
 
 VERIFY_TIMEOUT := 150
 
 include $(SMITHY_DAFNY_ROOT)/SmithyDafnyMakefile.mk
+
+verify:DAFNY_OPTIONS=--allow-deprecation --allow-external-contracts
+verify_single:DAFNY_OPTIONS=--allow-deprecation --allow-external-contracts
+verify_service:DAFNY_OPTIONS=--allow-deprecation --allow-external-contracts
+
+transpile_implementation_net: DAFNY_OPTIONS=--allow-warnings --compile-suffix --legacy-module-names --allow-external-contracts
+transpile_test_net: DAFNY_OPTIONS=--allow-warnings --include-test-runner --compile-suffix --legacy-module-names --allow-external-contracts
+
+transpile_implementation_java: DAFNY_OPTIONS=--allow-warnings --compile-suffix --legacy-data-constructors --legacy-module-names --allow-external-contracts
+transpile_test_java: DAFNY_OPTIONS=--allow-warnings --include-test-runner --compile-suffix --legacy-data-constructors --legacy-module-names --allow-external-contracts

From 1b1091ea84f0d70e67961af4e302aa89c0c6dee6 Mon Sep 17 00:00:00 2001
From: Darwin Chowdary <39110935+imabhichow@users.noreply.github.com>
Date: Sun, 12 Oct 2025 23:04:04 -0700
Subject: [PATCH 8/8] branch key id

---
 AwsEncryptionSDK/dafny/AwsEncryptionSdk/test/Fixtures.dfy | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/test/Fixtures.dfy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/test/Fixtures.dfy
index a7d7d5652..f73045a5a 100644
--- a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/test/Fixtures.dfy
+++ b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/test/Fixtures.dfy
@@ -20,7 +20,7 @@ module Fixtures {
   
   const branchKeyStoreName := "KeyStoreDdbTable"
   const logicalKeyStoreName := branchKeyStoreName
-  const branchKeyId := "75789115-1deb-4fe3-a2ec-be9e885d1945"
+  const branchKeyId := "3f43a9af-08c5-4317-b694-3d3e883dcaef"
   
   // UTF-8 encoded "aws-crypto-"
   const RESERVED_ENCRYPTION_CONTEXT: UTF8.ValidUTF8Bytes :=