diff --git a/.github/workflows/ci_test_vector_net.yml b/.github/workflows/ci_test_vector_net.yml
index c98fb33ed..0432d1cb9 100644
--- a/.github/workflows/ci_test_vector_net.yml
+++ b/.github/workflows/ci_test_vector_net.yml
@@ -62,7 +62,6 @@ jobs:
           dafny-version: ${{ inputs.dafny }}
 
       - name: Update MPL submodule if using MPL HEAD
-        if: ${{ inputs.mpl-head == true }}
         working-directory: submodules/MaterialProviders
         run: |
           git checkout main
diff --git a/.github/workflows/nightly.yml b/.github/workflows/nightly.yml
index eb4bc6e20..530f2f12b 100644
--- a/.github/workflows/nightly.yml
+++ b/.github/workflows/nightly.yml
@@ -19,51 +19,51 @@ jobs:
     uses: ./.github/workflows/library_format.yml
     with:
       dafny: "nightly-latest"
-      regenerate-code: true
+      regenerate-code: false
   dafny-nightly-verification:
     # Don't run the cron builds on forks
     if: github.event_name != 'schedule' || github.repository_owner == 'aws'
     uses: ./.github/workflows/library_dafny_verification.yml
     with:
       dafny: "nightly-latest"
-      regenerate-code: true
+      regenerate-code: false
   dafny-nightly-test-vector-verification:
     # Don't run the cron builds on forks
     if: github.event_name != 'schedule' || github.repository_owner == 'aws'
     uses: ./.github/workflows/test_vector_verification.yml
     with:
       dafny: "nightly-latest"
-      regenerate-code: true
+      regenerate-code: false
   dafny-nightly-java:
     if: github.event_name != 'schedule' || github.repository_owner == 'aws'
     uses: ./.github/workflows/ci_test_java.yml
     with:
       dafny: "nightly-latest"
-      regenerate-code: true
+      regenerate-code: false
   dafny-nightly-test-vectors-java:
     if: github.event_name != 'schedule' || github.repository_owner == 'aws'
     uses: ./.github/workflows/ci_test_vector_java.yml
     with:
       dafny: "nightly-latest"
-      regenerate-code: true
+      regenerate-code: false
   dafny-nightly-net:
     if: github.event_name != 'schedule' || github.repository_owner == 'aws'
     uses: ./.github/workflows/ci_test_net.yml
     with:
       dafny: "nightly-latest"
-      regenerate-code: true
+      regenerate-code: false
   dafny-nightly-rust:
     if: github.event_name != 'schedule' || github.repository_owner == 'aws'
     uses: ./.github/workflows/library_rust_tests.yml
     with:
       dafny: "nightly-latest"
-      regenerate-code: true
+      regenerate-code: false
   dafny-nightly-test-vectors-net:
     if: github.event_name != 'schedule' || github.repository_owner == 'aws'
     uses: ./.github/workflows/ci_test_vector_net.yml
     with:
       dafny: "nightly-latest"
-      regenerate-code: true
+      regenerate-code: false
 
   cut-issue-on-failure:
     runs-on: ubuntu-22.04
diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoDbGetEncryptedDataKeyDescriptionTest.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoDbGetEncryptedDataKeyDescriptionTest.dfy
index ee74a7383..84f9dd09c 100644
--- a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoDbGetEncryptedDataKeyDescriptionTest.dfy
+++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoDbGetEncryptedDataKeyDescriptionTest.dfy
@@ -191,7 +191,7 @@ module DynamoDbGetEncryptedDataKeyDescriptionTest {
     expect actualDataKeyDescription.EncryptedDataKeyDescriptionOutput[0].keyProviderInfo.value == "keyproviderInfo";
   }
 
-  method {:test} TestDDBItemInputAwsKmsHDataKeyCase()
+  method {:test} {:isolate_assertions} TestDDBItemInputAwsKmsHDataKeyCase()
   {
     var expectedHead := CreatePartialHeader(testVersion, testFlavor0, testMsgID, testLegend, testEncContext, [testAwsKmsHDataKey]);
     var serializedHeader := expectedHead.serialize() + expectedHead.msgID;
diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Canonize.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Canonize.dfy
index 8a2531579..140f8f77a 100644
--- a/DynamoDbEncryption/dafny/StructuredEncryption/src/Canonize.dfy
+++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/Canonize.dfy
@@ -671,6 +671,14 @@ module {:options "/functionSyntax:4" } Canonize {
     exists x :: x in origData && Updated2(x, item, DoDecrypt)
   }
 
+  ghost function Updated2Item(origData : AuthList, item : CanonCryptoItem) : (result : AuthItem)
+    requires Updated2Exists(origData, item)
+    ensures Updated2(result, item, DoDecrypt)
+  {
+    var r :| Updated2(r, item, DoDecrypt);
+    r
+  }
+
   ghost predicate Updated5Exists(origData : CryptoList, item : CanonCryptoItem)
   {
     exists x :: x in origData && Updated5(x, item, DoEncrypt)
@@ -698,11 +706,12 @@ module {:options "/functionSyntax:4" } Canonize {
     reveal CryptoUpdatedAuth();
     assert forall k <- output :: exists x :: x in origData && Updated3(x, k, DoDecrypt) by {
       Update2ImpliesUpdate3();
-      assert forall val <- input :: exists x :: x in origData && Updated2(x, val, DoDecrypt);
-      assume {:axiom} forall i | 0 <= i < |input| :: exists x :: x in origData && Updated2(x, input[i], DoDecrypt);
-      // assert forall i | 0 <= i < |input| :: exists x :: x in origData && Updated2(x, input[i], DoDecrypt) by {
-      //   InputIsInput(origData, input);
-      // }
+      assert forall i | 0 <= i < |input| :: exists x :: x in origData && Updated2(x, input[i], DoDecrypt) by {
+        InputIsInput(origData, input);
+        forall i | 0 <= i < |input| ensures exists x :: x in origData && Updated2(x, input[i], DoDecrypt) {
+          var x := Updated2Item(origData, input[i]);
+        }
+      }
       assert forall newVal <- output :: exists x :: x in origData && Updated3(x, newVal, DoDecrypt);
     }
   }
diff --git a/submodules/smithy-dafny b/submodules/smithy-dafny
index 2f83e28ad..36a8c87ec 160000
--- a/submodules/smithy-dafny
+++ b/submodules/smithy-dafny
@@ -1 +1 @@
-Subproject commit 2f83e28ad9532b24c93d2229476c9a268355d338
+Subproject commit 36a8c87ec0a02b9f095f805d550461a7654831f9