diff --git a/.github/actions/install_smithy_dafny_codegen_dependencies/action.yml b/.github/actions/install_smithy_dafny_codegen_dependencies/action.yml index d4df6ab8a..cbb9af5f8 100644 --- a/.github/actions/install_smithy_dafny_codegen_dependencies/action.yml +++ b/.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 diff --git a/.github/workflows/ci_codegen.yml b/.github/workflows/ci_codegen.yml index 38f11beb0..311559b04 100644 --- a/.github/workflows/ci_codegen.yml +++ b/.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 }} diff --git a/.github/workflows/ci_examples_java.yml b/.github/workflows/ci_examples_java.yml index 13fc60abb..2499ac6ae 100644 --- a/.github/workflows/ci_examples_java.yml +++ b/.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 diff --git a/.github/workflows/ci_test_java.yml b/.github/workflows/ci_test_java.yml index fd701c52a..34d8c1d08 100644 --- a/.github/workflows/ci_test_java.yml +++ b/.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 diff --git a/.github/workflows/ci_test_vector_java.yml b/.github/workflows/ci_test_vector_java.yml index 54bf63ca3..d0396f2b4 100644 --- a/.github/workflows/ci_test_vector_java.yml +++ b/.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 diff --git a/.github/workflows/ci_test_vector_net.yml b/.github/workflows/ci_test_vector_net.yml index 91663fea8..5dd90d031 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 @@ -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 diff --git a/.github/workflows/library_dafny_verification.yml b/.github/workflows/library_dafny_verification.yml index 30915f103..1759804e1 100644 --- a/.github/workflows/library_dafny_verification.yml +++ b/.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 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/.github/workflows/test_vector_verification.yml b/.github/workflows/test_vector_verification.yml index 7170063d6..d00b1fdc2 100644 --- a/.github/workflows/test_vector_verification.yml +++ b/.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 diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy index e15763cb6..9d3d8aecf 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy +++ b/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); 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