From e6d3d101265722a9fa4721f72c68f6176cdad81d Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Mon, 28 Oct 2024 09:09:02 -0700 Subject: [PATCH 01/12] Java 17 and install dependencies --- .../action.yml | 21 ------------------- .github/actions/polymorph_codegen/action.yml | 11 ++++++++++ 2 files changed, 11 insertions(+), 21 deletions(-) delete mode 100644 .github/actions/install_smithy_dafny_codegen_dependencies/action.yml diff --git a/.github/actions/install_smithy_dafny_codegen_dependencies/action.yml b/.github/actions/install_smithy_dafny_codegen_dependencies/action.yml deleted file mode 100644 index d4df6ab8a..000000000 --- a/.github/actions/install_smithy_dafny_codegen_dependencies/action.yml +++ /dev/null @@ -1,21 +0,0 @@ -# -# This local action sets up code dependencies -# to run Smithy-Dafny CI in GitHub Actions workflows. -# - -name: "Install Smithy-Dafny codegen dependencies" -description: "Install Java package dependencies required to run Smithy-Dafny codegen" -runs: - using: "composite" - steps: - - name: Install smithy-dafny-codegen Rust dependencies locally - uses: gradle/gradle-build-action@v2 - with: - arguments: :codegen-client:pTML :codegen-core:pTML :rust-runtime:pTML - build-root-directory: submodules/smithy-dafny/smithy-dafny-codegen-modules/smithy-rs - - - name: Install smithy-dafny-codegen Python dependencies locally - uses: gradle/gradle-build-action@v2 - with: - arguments: :smithy-python-codegen:pTML - build-root-directory: submodules/smithy-dafny/codegen/smithy-dafny-codegen-modules/smithy-python/codegen diff --git a/.github/actions/polymorph_codegen/action.yml b/.github/actions/polymorph_codegen/action.yml index 302523dae..193be9dda 100644 --- a/.github/actions/polymorph_codegen/action.yml +++ b/.github/actions/polymorph_codegen/action.yml @@ -66,6 +66,17 @@ runs: git pull git submodule update --init --recursive + - name: Setup Java 17 for smithy-dafny + uses: actions/setup-java@v3 + with: + distribution: "corretto" + java-version: 17 + + - name: Install smithy-dafny dependencies locally + shell: bash + run: | + make -C submodules/smithy-dafny mvn_local_deploy_polymorph_dependencies + - name: Update top-level project.properties file in MPL if: inputs.update-and-regenerate-mpl == 'true' shell: bash From b60430e8f61ecf347235389560b5a2b58fd8f41d Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Mon, 28 Oct 2024 09:09:30 -0700 Subject: [PATCH 02/12] Update smithy-dafny --- submodules/smithy-dafny | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/submodules/smithy-dafny b/submodules/smithy-dafny index 98939e130..1ac83f584 160000 --- a/submodules/smithy-dafny +++ b/submodules/smithy-dafny @@ -1 +1 @@ -Subproject commit 98939e130695095386059967509a19299dfac320 +Subproject commit 1ac83f584f7ffd7016360fd4367cf4864d9b3a29 From 6b9a9481217e0e9c3cbc2ca684ca53daa1d01bb8 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Tue, 29 Oct 2024 14:07:29 -0700 Subject: [PATCH 03/12] Verification fixes --- .../DynamoDbGetEncryptedDataKeyDescriptionTest.dfy | 2 +- .../dafny/StructuredEncryption/src/Canonize.dfy | 11 +++++++++++ 2 files changed, 12 insertions(+), 1 deletion(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoDbGetEncryptedDataKeyDescriptionTest.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoDbGetEncryptedDataKeyDescriptionTest.dfy index 2f5cb02a8..67d315ad3 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoDbGetEncryptedDataKeyDescriptionTest.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoDbGetEncryptedDataKeyDescriptionTest.dfy @@ -156,7 +156,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 85c6f93f9..51027dcdc 100644 --- a/DynamoDbEncryption/dafny/StructuredEncryption/src/Canonize.dfy +++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/Canonize.dfy @@ -663,6 +663,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) @@ -693,6 +701,9 @@ module {:options "/functionSyntax:4" } Canonize { assert forall val <- input :: exists x :: x in origData && Updated2(x, val, DoDecrypt); 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); } From 495d520687c6b3d2326a620371bda6e6cc5752ed Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Tue, 29 Oct 2024 14:22:09 -0700 Subject: [PATCH 04/12] =?UTF-8?q?don=E2=80=99t=20regenerate=20code=20in=20?= =?UTF-8?q?nightly=20any=20more?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .github/workflows/nightly.yml | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/.github/workflows/nightly.yml b/.github/workflows/nightly.yml index 408eefe62..7ecd3ba9d 100644 --- a/.github/workflows/nightly.yml +++ b/.github/workflows/nightly.yml @@ -19,45 +19,45 @@ 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-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-latest From b2a68a83a3961041b0bd5db67ffa20845f283c93 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Tue, 29 Oct 2024 14:48:13 -0700 Subject: [PATCH 05/12] Fix codegen workflow --- .github/workflows/ci_codegen.yml | 9 --------- 1 file changed, 9 deletions(-) diff --git a/.github/workflows/ci_codegen.yml b/.github/workflows/ci_codegen.yml index 6bbee248d..c7d6cf6cd 100644 --- a/.github/workflows/ci_codegen.yml +++ b/.github/workflows/ci_codegen.yml @@ -51,15 +51,6 @@ jobs: - name: Create temporary global.json run: echo '{"sdk":{"rollForward":"latestFeature","version":"6.0.0"}}' > ./global.json - - name: Setup Java 17 for codegen - uses: actions/setup-java@v3 - with: - distribution: "corretto" - java-version: "17" - - - name: Install Smithy-Dafny codegen dependencies - uses: ./.github/actions/install_smithy_dafny_codegen_dependencies - - uses: ./.github/actions/polymorph_codegen with: dafny: ${{ inputs.dafny }} From 31f1b605aa93496f9cd0857ef60ea4400b77eac3 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Tue, 29 Oct 2024 14:57:31 -0700 Subject: [PATCH 06/12] Revert smithy-dafny --- submodules/smithy-dafny | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/submodules/smithy-dafny b/submodules/smithy-dafny index 1ac83f584..98939e130 160000 --- a/submodules/smithy-dafny +++ b/submodules/smithy-dafny @@ -1 +1 @@ -Subproject commit 1ac83f584f7ffd7016360fd4367cf4864d9b3a29 +Subproject commit 98939e130695095386059967509a19299dfac320 From 21e832e1c78e22a0c0788ea0612c50ca690a8352 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Fri, 23 May 2025 12:34:43 -0700 Subject: [PATCH 07/12] Revert "Java 17 and install dependencies" This reverts commit e6d3d101265722a9fa4721f72c68f6176cdad81d. --- .../action.yml | 21 +++++++++++++++++++ .github/actions/polymorph_codegen/action.yml | 11 ---------- 2 files changed, 21 insertions(+), 11 deletions(-) create mode 100644 .github/actions/install_smithy_dafny_codegen_dependencies/action.yml diff --git a/.github/actions/install_smithy_dafny_codegen_dependencies/action.yml b/.github/actions/install_smithy_dafny_codegen_dependencies/action.yml new file mode 100644 index 000000000..d4df6ab8a --- /dev/null +++ b/.github/actions/install_smithy_dafny_codegen_dependencies/action.yml @@ -0,0 +1,21 @@ +# +# This local action sets up code dependencies +# to run Smithy-Dafny CI in GitHub Actions workflows. +# + +name: "Install Smithy-Dafny codegen dependencies" +description: "Install Java package dependencies required to run Smithy-Dafny codegen" +runs: + using: "composite" + steps: + - name: Install smithy-dafny-codegen Rust dependencies locally + uses: gradle/gradle-build-action@v2 + with: + arguments: :codegen-client:pTML :codegen-core:pTML :rust-runtime:pTML + build-root-directory: submodules/smithy-dafny/smithy-dafny-codegen-modules/smithy-rs + + - name: Install smithy-dafny-codegen Python dependencies locally + uses: gradle/gradle-build-action@v2 + with: + arguments: :smithy-python-codegen:pTML + build-root-directory: submodules/smithy-dafny/codegen/smithy-dafny-codegen-modules/smithy-python/codegen diff --git a/.github/actions/polymorph_codegen/action.yml b/.github/actions/polymorph_codegen/action.yml index 193be9dda..302523dae 100644 --- a/.github/actions/polymorph_codegen/action.yml +++ b/.github/actions/polymorph_codegen/action.yml @@ -66,17 +66,6 @@ runs: git pull git submodule update --init --recursive - - name: Setup Java 17 for smithy-dafny - uses: actions/setup-java@v3 - with: - distribution: "corretto" - java-version: 17 - - - name: Install smithy-dafny dependencies locally - shell: bash - run: | - make -C submodules/smithy-dafny mvn_local_deploy_polymorph_dependencies - - name: Update top-level project.properties file in MPL if: inputs.update-and-regenerate-mpl == 'true' shell: bash From 80b1575fd94ba590bc9ef8d440aa675e8eb1f818 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Fri, 23 May 2025 12:37:49 -0700 Subject: [PATCH 08/12] m --- .../action.yml | 12 ++++++++++++ submodules/smithy-dafny | 2 +- 2 files changed, 13 insertions(+), 1 deletion(-) diff --git a/.github/actions/install_smithy_dafny_codegen_dependencies/action.yml b/.github/actions/install_smithy_dafny_codegen_dependencies/action.yml index d4df6ab8a..c643fb2fb 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 StandardLibrary setup_net 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 From 2625de8b2517911485c7d8893b15ed6a215c94ed Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Fri, 23 May 2025 12:45:14 -0700 Subject: [PATCH 09/12] m --- .../install_smithy_dafny_codegen_dependencies/action.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/actions/install_smithy_dafny_codegen_dependencies/action.yml b/.github/actions/install_smithy_dafny_codegen_dependencies/action.yml index c643fb2fb..cbb9af5f8 100644 --- a/.github/actions/install_smithy_dafny_codegen_dependencies/action.yml +++ b/.github/actions/install_smithy_dafny_codegen_dependencies/action.yml @@ -30,4 +30,4 @@ runs: - name: Arbitrary makefile target to force downloading Gradle shell: bash run: | - make -C StandardLibrary setup_net + make -C DynamoDbEncryption setup_net From dff2f5d3ac6b2b2d396f7c473fded1d1a9d268b4 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Fri, 23 May 2025 15:56:48 -0700 Subject: [PATCH 10/12] Always install codegen CLI dependencies --- .github/workflows/ci_examples_java.yml | 1 - .github/workflows/ci_test_java.yml | 1 - .github/workflows/ci_test_vector_java.yml | 1 - .github/workflows/ci_test_vector_net.yml | 1 - .github/workflows/library_dafny_verification.yml | 1 - .github/workflows/test_vector_verification.yml | 1 - 6 files changed, 6 deletions(-) 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..93950b935 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/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/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 From 24b5b4851596948ff13c699afad6964a878783e0 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Fri, 23 May 2025 16:20:23 -0700 Subject: [PATCH 11/12] Missed one --- .github/workflows/ci_test_vector_net.yml | 1 - 1 file changed, 1 deletion(-) diff --git a/.github/workflows/ci_test_vector_net.yml b/.github/workflows/ci_test_vector_net.yml index 93950b935..5dd90d031 100644 --- a/.github/workflows/ci_test_vector_net.yml +++ b/.github/workflows/ci_test_vector_net.yml @@ -70,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 From e48dfc4230580d91089308f8293ed94a27b13af2 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Sat, 24 May 2025 10:39:39 -0700 Subject: [PATCH 12/12] Explicit type for resolution regression --- .../dafny/DynamoDbEncryption/src/DynamoToStruct.dfy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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);