diff --git a/.github/workflows/ci_examples_java.yml b/.github/workflows/ci_examples_java.yml index 48d51d356..558b2b583 100644 --- a/.github/workflows/ci_examples_java.yml +++ b/.github/workflows/ci_examples_java.yml @@ -13,6 +13,15 @@ on: required: false default: false type: boolean + mpl-version: + description: "MPL version to use" + required: false + type: string + mpl-head: + description: "Running on MPL HEAD" + required: false + default: false + type: boolean jobs: testJava: @@ -48,6 +57,20 @@ jobs: with: 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 + git pull + git submodule update --init --recursive + git rev-parse HEAD + + - name: Update project.properties if using MPL HEAD + if: ${{ inputs.mpl-head == true }} + run: | + sed "s/mplDependencyJavaVersion=.*/mplDependencyJavaVersion=${{inputs.mpl-version}}/g" project.properties > project.properties2; mv project.properties2 project.properties + - name: Regenerate code using smithy-dafny if necessary if: ${{ inputs.regenerate-code }} uses: ./.github/actions/polymorph_codegen diff --git a/.github/workflows/ci_examples_net.yml b/.github/workflows/ci_examples_net.yml index 5c5f47a0f..9d6d7eef6 100644 --- a/.github/workflows/ci_examples_net.yml +++ b/.github/workflows/ci_examples_net.yml @@ -13,6 +13,11 @@ on: required: false default: false type: boolean + mpl-head: + description: "Running on MPL HEAD" + required: false + default: false + type: boolean jobs: dotNetExamples: @@ -45,6 +50,15 @@ jobs: with: 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 + git pull + git submodule update --init --recursive + git rev-parse HEAD + - name: Regenerate code using smithy-dafny if necessary if: ${{ inputs.regenerate-code }} uses: ./.github/actions/polymorph_codegen diff --git a/.github/workflows/ci_test_java.yml b/.github/workflows/ci_test_java.yml index a4e9a26be..f96748878 100644 --- a/.github/workflows/ci_test_java.yml +++ b/.github/workflows/ci_test_java.yml @@ -13,6 +13,15 @@ on: required: false default: false type: boolean + mpl-version: + description: "MPL version to use" + required: false + type: string + mpl-head: + description: "Running on MPL HEAD" + required: false + default: false + type: boolean jobs: testJava: @@ -42,6 +51,20 @@ jobs: with: 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 + git pull + git submodule update --init --recursive + git rev-parse HEAD + + - name: Update project.properties if using MPL HEAD + if: ${{ inputs.mpl-head == true }} + run: | + sed "s/mplDependencyJavaVersion=.*/mplDependencyJavaVersion=${{inputs.mpl-version}}/g" project.properties > project.properties2; mv project.properties2 project.properties + - name: Regenerate code using smithy-dafny if necessary if: ${{ inputs.regenerate-code }} uses: ./.github/actions/polymorph_codegen diff --git a/.github/workflows/ci_test_net.yml b/.github/workflows/ci_test_net.yml index 5e0bf8d39..8ead30d1f 100644 --- a/.github/workflows/ci_test_net.yml +++ b/.github/workflows/ci_test_net.yml @@ -13,6 +13,11 @@ on: required: false default: false type: boolean + mpl-head: + description: "Running on MPL HEAD" + required: false + default: false + type: boolean jobs: testDotNet: @@ -46,6 +51,15 @@ jobs: with: 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 + git pull + git submodule update --init --recursive + git rev-parse HEAD + - name: Regenerate code using smithy-dafny if necessary if: ${{ inputs.regenerate-code }} uses: ./.github/actions/polymorph_codegen diff --git a/.github/workflows/ci_test_vector_java.yml b/.github/workflows/ci_test_vector_java.yml index 707fd1a16..13549d90d 100644 --- a/.github/workflows/ci_test_vector_java.yml +++ b/.github/workflows/ci_test_vector_java.yml @@ -13,6 +13,15 @@ on: required: false default: false type: boolean + mpl-version: + description: "MPL version to use" + required: false + type: string + mpl-head: + description: "Running on MPL HEAD" + required: false + default: false + type: boolean jobs: testJava: @@ -51,6 +60,20 @@ jobs: with: 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 + git pull + git submodule update --init --recursive + git rev-parse HEAD + + - name: Update project.properties if using MPL HEAD + if: ${{ inputs.mpl-head == true }} + run: | + sed "s/mplDependencyJavaVersion=.*/mplDependencyJavaVersion=${{inputs.mpl-version}}/g" project.properties > project.properties2; mv project.properties2 project.properties + - name: Regenerate code using smithy-dafny if necessary if: ${{ inputs.regenerate-code }} uses: ./.github/actions/polymorph_codegen diff --git a/.github/workflows/ci_test_vector_net.yml b/.github/workflows/ci_test_vector_net.yml index c39ab9e96..e2fdff24e 100644 --- a/.github/workflows/ci_test_vector_net.yml +++ b/.github/workflows/ci_test_vector_net.yml @@ -13,6 +13,11 @@ on: required: false default: false type: boolean + mpl-head: + description: "Running on MPL HEAD" + required: false + default: false + type: boolean jobs: testDotNet: @@ -51,6 +56,15 @@ jobs: with: 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 + git pull + git submodule update --init --recursive + git rev-parse HEAD + - name: Regenerate code using smithy-dafny if necessary if: ${{ inputs.regenerate-code }} uses: ./.github/actions/polymorph_codegen diff --git a/.github/workflows/daily_ci.yml b/.github/workflows/daily_ci.yml index 2edd6273a..cc047fcab 100644 --- a/.github/workflows/daily_ci.yml +++ b/.github/workflows/daily_ci.yml @@ -36,6 +36,11 @@ jobs: uses: ./.github/workflows/test_vector_verification.yml with: dafny: ${{needs.getVerifyVersion.outputs.version}} + daily-ci-java: + needs: getVersion + uses: ./.github/workflows/ci_test_java.yml + with: + dafny: ${{needs.getVersion.outputs.version}} daily-ci-java-test-vectors: needs: getVersion uses: ./.github/workflows/ci_test_vector_java.yml diff --git a/.github/workflows/library_dafny_verification.yml b/.github/workflows/library_dafny_verification.yml index dda360ec6..f25a216b2 100644 --- a/.github/workflows/library_dafny_verification.yml +++ b/.github/workflows/library_dafny_verification.yml @@ -13,6 +13,15 @@ on: required: false default: false type: boolean + mpl-version: + description: "MPL version to use" + required: false + type: string + mpl-head: + description: "Running on MPL HEAD" + required: false + default: false + type: boolean jobs: verification: @@ -47,6 +56,20 @@ jobs: with: 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 + git pull + git submodule update --init --recursive + git rev-parse HEAD + + - name: Update project.properties if using MPL HEAD + if: ${{ inputs.mpl-head == true }} + run: | + sed "s/mplDependencyJavaVersion=.*/mplDependencyJavaVersion=${{inputs.mpl-version}}/g" project.properties > project.properties2; mv project.properties2 project.properties + # dafny-reportgenerator requires next6 # but only 7.0 is installed on macos-12-large - name: Setup .NET Core SDK '6.0.x' @@ -63,7 +86,7 @@ jobs: diff-generated-code: false - name: Verify ${{ matrix.library }} Dafny code - working-directory: ./DynamoDbEncryption + working-directory: DynamoDbEncryption run: | # This works because `node` is installed by default on GHA runners CORES=$(node -e 'console.log(os.cpus().length)') @@ -71,6 +94,6 @@ jobs: - name: Check solver resource use if: success() || failure() - working-directory: ./DynamoDbEncryption + working-directory: DynamoDbEncryption run: | make dafny-reportgenerator diff --git a/.github/workflows/mpl-head.yml b/.github/workflows/mpl-head.yml new file mode 100644 index 000000000..6bb7e1b7c --- /dev/null +++ b/.github/workflows/mpl-head.yml @@ -0,0 +1,78 @@ +# This workflow invokes other workflows with the latest MPL head at 14:00 UTC (7am PDT) +name: CI MPL HEAD + +on: + schedule: + - cron: "00 14 * * 1-5" + +jobs: + getVersion: + # Don't run the cron builds on forks + if: github.event_name != 'schedule' || github.repository_owner == 'aws' + uses: ./.github/workflows/dafny_version.yml + getVerifyVersion: + if: github.event_name != 'schedule' || github.repository_owner == 'aws' + uses: ./.github/workflows/dafny_verify_version.yml + getMplHeadVersion: + if: github.event_name != 'schedule' || github.repository_owner == 'aws' + uses: ./.github/workflows/mpl_head_version.yml + mpl-head-ci-format: + needs: getVersion + if: github.event_name != 'schedule' || github.repository_owner == 'aws' + uses: ./.github/workflows/library_format.yml + with: + dafny: ${{needs.getVersion.outputs.version}} + mpl-head-ci-verification: + needs: [getVerifyVersion, getMplHeadVersion] + if: github.event_name != 'schedule' || github.repository_owner == 'aws' + uses: ./.github/workflows/library_dafny_verification.yml + with: + dafny: ${{needs.getVerifyVersion.outputs.version}} + mpl-version: ${{needs.getMplHeadVersion.outputs.version}} + mpl-head: true + mpl-head-ci-test-vector-verification: + needs: [getVerifyVersion, getMplHeadVersion] + uses: ./.github/workflows/test_vector_verification.yml + with: + dafny: ${{needs.getVerifyVersion.outputs.version}} + mpl-version: ${{needs.getMplHeadVersion.outputs.version}} + mpl-head: true + mpl-head-ci-java: + needs: [getVersion, getMplHeadVersion] + uses: ./.github/workflows/ci_test_java.yml + with: + dafny: ${{needs.getVersion.outputs.version}} + mpl-version: ${{needs.getMplHeadVersion.outputs.version}} + mpl-head: true + mpl-head-ci-java-test-vectors: + needs: [getVersion, getMplHeadVersion] + uses: ./.github/workflows/ci_test_vector_java.yml + with: + dafny: ${{needs.getVersion.outputs.version}} + mpl-version: ${{needs.getMplHeadVersion.outputs.version}} + mpl-head: true + mpl-head-ci-java-examples: + needs: [getVersion, getMplHeadVersion] + uses: ./.github/workflows/ci_examples_java.yml + with: + dafny: ${{needs.getVersion.outputs.version}} + mpl-version: ${{needs.getMplHeadVersion.outputs.version}} + mpl-head: true + mpl-head-ci-net: + needs: getVersion + uses: ./.github/workflows/ci_test_net.yml + with: + dafny: ${{needs.getVersion.outputs.version}} + mpl-head: true + mpl-head-ci-net-test-vectors: + needs: getVersion + uses: ./.github/workflows/ci_test_vector_net.yml + with: + dafny: ${{needs.getVersion.outputs.version}} + mpl-head: true + mpl-head-ci-net-examples: + needs: getVersion + uses: ./.github/workflows/ci_examples_net.yml + with: + dafny: ${{needs.getVersion.outputs.version}} + mpl-head: true diff --git a/.github/workflows/mpl_head_version.yml b/.github/workflows/mpl_head_version.yml new file mode 100644 index 000000000..094825a9a --- /dev/null +++ b/.github/workflows/mpl_head_version.yml @@ -0,0 +1,36 @@ +# This workflow reads the project.properties +# into the environment variables +# and then creates an output variable for `dafnyVerifyVersion ` +name: MPL HEAD Version + +on: + workflow_call: + outputs: + version: + description: "The dafny version for verify" + value: ${{ jobs.getMplHeadVersion.outputs.version }} + +jobs: + getMplHeadVersion: + runs-on: ubuntu-latest + outputs: + version: ${{ steps.read_property.outputs.mplVersion }} + steps: + - uses: actions/checkout@v4 + with: + submodules: recursive + - name: Update MPL submodule locally if requested + working-directory: submodules/MaterialProviders + shell: bash + run: | + git checkout main + git pull + git submodule update --init --recursive + git rev-parse HEAD + + - name: Get the MPL version from the MPL submodule + id: read_property + uses: christian-draeger/read-properties@1.1.1 + with: + path: "submodules/MaterialProviders/project.properties" + properties: "mplVersion" diff --git a/.github/workflows/test_vector_verification.yml b/.github/workflows/test_vector_verification.yml index e6de4b5f6..118808829 100644 --- a/.github/workflows/test_vector_verification.yml +++ b/.github/workflows/test_vector_verification.yml @@ -13,6 +13,15 @@ on: required: false default: false type: boolean + mpl-version: + description: "MPL version to use" + required: false + type: string + mpl-head: + description: "Running on MPL HEAD" + required: false + default: false + type: boolean jobs: verification: @@ -38,6 +47,20 @@ jobs: with: 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 + git pull + git submodule update --init --recursive + git rev-parse HEAD + + - name: Update project.properties if using MPL HEAD + if: ${{ inputs.mpl-head == true }} + run: | + sed "s/mplDependencyJavaVersion=.*/mplDependencyJavaVersion=${{inputs.mpl-version}}/g" project.properties > project.properties2; mv project.properties2 project.properties + # dafny-reportgenerator requires next6 # but only 7.0 is installed on macos-12-large - name: Setup .NET Core SDK '6.0.x' diff --git a/TestVectors/runtimes/java/build.gradle.kts b/TestVectors/runtimes/java/build.gradle.kts index ee1439b90..ae608f1a9 100644 --- a/TestVectors/runtimes/java/build.gradle.kts +++ b/TestVectors/runtimes/java/build.gradle.kts @@ -28,6 +28,7 @@ var dafnyRuntimeJavaVersion = props.getProperty("dafnyRuntimeJavaVersion") var smithyDafnyJavaConversionVersion = props.getProperty("smithyDafnyJavaConversionVersion") group = "software.amazon.cryptography" +// change to ${mplVersion} for next MPL update version = "1.0-SNAPSHOT" description = "TestVectorsDynamoDbEncryption" @@ -90,6 +91,7 @@ dependencies { implementation("software.amazon.smithy.dafny:conversion:${smithyDafnyJavaConversionVersion}") implementation("software.amazon.cryptography:aws-cryptographic-material-providers:${mplVersion}") implementation("software.amazon.cryptography:aws-database-encryption-sdk-dynamodb:${ddbecVersion}") + // change to ${mplVersion} for next MPL update implementation("software.amazon.cryptography:TestAwsCryptographicMaterialProviders:1.0-SNAPSHOT") implementation(platform("software.amazon.awssdk:bom:2.24.2"))