chore(ci): Fix nightly build

.github/actions/install_smithy_dafny_codegen_dependencies/action.yml

@@ -8,6 +8,12 @@ description: "Install Java package dependencies required to run Smithy-Dafny cod
 runs:
   using: "composite"
   steps:
+    - name: Setup Java 17 for smithy-dafny
+      uses: actions/setup-java@v3
+      with:
+        distribution: "corretto"
+        java-version: 17
+
     - name: Install smithy-dafny-codegen Rust dependencies locally
       uses: gradle/gradle-build-action@v2
       with:
@@ -19,3 +25,9 @@ runs:
       with:
         arguments: :smithy-python-codegen:pTML
         build-root-directory: submodules/smithy-dafny/codegen/smithy-dafny-codegen-modules/smithy-python/codegen
+
+    # Without this the if-dafny-at-least command includes "Downloading ..." output
+    - name: Arbitrary makefile target to force downloading Gradle
+      shell: bash
+      run: |
+        make -C DynamoDbEncryption setup_net

.github/workflows/ci_codegen.yml

@@ -60,9 +60,6 @@ jobs:
       - name: Install Smithy-Dafny codegen dependencies
         uses: ./.github/actions/install_smithy_dafny_codegen_dependencies
 
-      - name: Install Smithy-Dafny codegen dependencies
-        uses: ./.github/actions/install_smithy_dafny_codegen_dependencies
-
       - uses: ./.github/actions/polymorph_codegen
         with:
           dafny: ${{ inputs.dafny }}

.github/workflows/ci_examples_java.yml

@@ -72,7 +72,6 @@ jobs:
           sed "s/mplDependencyJavaVersion=.*/mplDependencyJavaVersion=${{inputs.mpl-version}}/g" project.properties > project.properties2; mv project.properties2 project.properties
 
       - name: Install Smithy-Dafny codegen dependencies
-        if: ${{ inputs.regenerate-code }}
         uses: ./.github/actions/install_smithy_dafny_codegen_dependencies
 
       - name: Regenerate code using smithy-dafny if necessary

.github/workflows/ci_test_java.yml

@@ -66,7 +66,6 @@ jobs:
           sed "s/mplDependencyJavaVersion=.*/mplDependencyJavaVersion=${{inputs.mpl-version}}/g" project.properties > project.properties2; mv project.properties2 project.properties
 
       - name: Install Smithy-Dafny codegen dependencies
-        if: ${{ inputs.regenerate-code }}
         uses: ./.github/actions/install_smithy_dafny_codegen_dependencies
 
       - name: Regenerate code using smithy-dafny if necessary

.github/workflows/ci_test_vector_java.yml

@@ -80,7 +80,6 @@ jobs:
           sed "s/mplDependencyJavaVersion=.*/mplDependencyJavaVersion=${{inputs.mpl-version}}/g" project.properties > project.properties2; mv project.properties2 project.properties
 
       - name: Install Smithy-Dafny codegen dependencies
-        if: ${{ inputs.regenerate-code }}
         uses: ./.github/actions/install_smithy_dafny_codegen_dependencies
 
       - name: Regenerate code using smithy-dafny if necessary

.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
@@ -71,7 +70,6 @@ jobs:
           git rev-parse HEAD
 
       - name: Install Smithy-Dafny codegen dependencies
-        if: ${{ inputs.regenerate-code }}
         uses: ./.github/actions/install_smithy_dafny_codegen_dependencies
 
       - name: Regenerate code using smithy-dafny if necessary

.github/workflows/library_dafny_verification.yml

@@ -79,7 +79,6 @@ jobs:
           dotnet-version: "6.0.x"
 
       - name: Install Smithy-Dafny codegen dependencies
-        if: ${{ inputs.regenerate-code }}
         uses: ./.github/actions/install_smithy_dafny_codegen_dependencies
 
       - name: Regenerate code using smithy-dafny if necessary

.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

.github/workflows/test_vector_verification.yml

@@ -69,7 +69,6 @@ jobs:
           dotnet-version: "6.0.x"
 
       - name: Install Smithy-Dafny codegen dependencies
-        if: ${{ inputs.regenerate-code }}
         uses: ./.github/actions/install_smithy_dafny_codegen_dependencies
 
       - name: Regenerate code using smithy-dafny if necessary

DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy

@@ -657,7 +657,7 @@ module DynamoToStruct {
     var len := |attrNames| as uint64;
     var output :- U32ToBigEndian64(len);
     for i : uint64 := 0 to len {
-      var k := attrNames[i];
+      var k: AttributeName := attrNames[i];
       var val := AttrToBytes(m[k], true, depth+1);
       if val.Failure? {
         var result := Failure(val.error);

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;

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);
     }
   }