From f43a2853e0a6cf3b60dfd6fdca34381539dd18fa Mon Sep 17 00:00:00 2001 From: Jose Corella Date: Thu, 15 Aug 2024 17:26:41 -0700 Subject: [PATCH 1/2] chore(GHA): add backwards interop dafny tests --- .github/workflows/dafny-interop.yml | 60 ++++++++++++++++ .github/workflows/dafny_interop_java.yml | 87 ++++++++++++++++++++++++ 2 files changed, 147 insertions(+) create mode 100644 .github/workflows/dafny-interop.yml create mode 100644 .github/workflows/dafny_interop_java.yml diff --git a/.github/workflows/dafny-interop.yml b/.github/workflows/dafny-interop.yml new file mode 100644 index 000000000..bbc375903 --- /dev/null +++ b/.github/workflows/dafny-interop.yml @@ -0,0 +1,60 @@ + +# This workflow is for testing backwards compatibility of a dafny version +# and tests if a project that consumes the mpl will be backwards compatible with +# a newer version of Dafny +name: Dafny Interoperability Test + +on: + workflow_dispatch: + inputs: + mpl-dafny: + description: "The Dafny version to compile the MPL with (4.2.0, dafny-nightly, etc..)" + required: true + type: string + mpl-commit: + description: "The MPL commit to use" + required: false + default: "HEAD" + type: string + dbesdk-dafny: + description: "The Dafny version to compile the DBESDK with (4.2.0, dafny-nightly, etc..)" + required: true + type: string + +jobs: + dafny-interop-java: + uses: ./.github/workflows/dafny_interop_java.yml + with: + mpl-dafny: ${{inputs.mpl-dafny}} + mpl-commit: ${{inputs.mpl-commit}} + dbesdk-dafny: ${{inputs.dbesdk-dafny}} + # dafny-interop-java-test-vectors: + # uses: ./.github/workflows/ci_test_vector_java.yml + # with: + # mpl-dafny: ${{inputs.mpl-dafny}} + # mpl-commit: ${{inputs.mpl-commit}} + # dbsesdk-dafny: ${{inputs.dbesdk-dafny}} + # dafny-interop-java-examples: + # uses: ./.github/workflows/ci_examples_java.yml + # with: + # mpl-dafny: ${{inputs.mpl-dafny}} + # mpl-commit: ${{inputs.mpl-commit}} + # dbsesdk-dafny: ${{inputs.dbesdk-dafny}} + # dafny-interop-net: + # uses: ./.github/workflows/ci_test_net.yml + # with: + # mpl-dafny: ${{inputs.mpl-dafny}} + # mpl-commit: ${{inputs.mpl-commit}} + # dbsesdk-dafny: ${{inputs.dbesdk-dafny}} + # dafny-interop-net-test-vectors: + # uses: ./.github/workflows/ci_test_vector_net.yml + # with: + # mpl-dafny: ${{inputs.mpl-dafny}} + # mpl-commit: ${{inputs.mpl-commit}} + # dbsesdk-dafny: ${{inputs.dbesdk-dafny}} + # dafny-interop-net-examples: + # uses: ./.github/workflows/ci_examples_net.yml + # with: + # mpl-dafny: ${{inputs.mpl-dafny}} + # mpl-commit: ${{inputs.mpl-commit}} + # dbsesdk-dafny: ${{inputs.dbesdk-dafny}} diff --git a/.github/workflows/dafny_interop_java.yml b/.github/workflows/dafny_interop_java.yml new file mode 100644 index 000000000..5d35ef59b --- /dev/null +++ b/.github/workflows/dafny_interop_java.yml @@ -0,0 +1,87 @@ +# This workflow performs tests in Java. +name: Library Java tests + +on: + workflow_call: + inputs: + mpl-dafny: + description: "The Dafny version to compile the MPL with (4.2.0, dafny-nightly, etc..)" + required: true + type: string + mpl-commit: + description: "The MPL commit to use" + required: false + default: "main" + type: string + dbesdk-dafny: + description: "The Dafny version to compile the DBESDK with (4.2.0, dafny-nightly, etc..)" + required: true + type: string + +jobs: + testJava: + strategy: + matrix: + library: [DynamoDbEncryption] + java-version: [8, 11, 16, 17] + os: [macos-12] + runs-on: ${{ matrix.os }} + permissions: + id-token: write + contents: read + steps: + - name: Configure AWS Credentials + uses: aws-actions/configure-aws-credentials@v4 + with: + aws-region: us-west-2 + role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-DDBEC-Dafny-Role-us-west-2 + role-session-name: DDBEC-Dafny-Java-Tests + + - uses: actions/checkout@v3 + with: + submodules: recursive + fetch-depth: 0 + + - name: Setup MPL Dafny + uses: dafny-lang/setup-dafny-action@v1.7.2 + with: + dafny-version: ${{ inputs.mpl-dafny }} + + - name: Update MPL submodule if using MPL HEAD + working-directory: submodules/MaterialProviders + run: | + git fetch + git checkout ${{inputs.mpl-commit}} + git pull + git submodule update --init --recursive + git rev-parse HEAD + + - name: Setup Java ${{ matrix.java-version }} + uses: actions/setup-java@v4 + with: + distribution: "corretto" + java-version: ${{ matrix.java-version }} + + - name: Build MPL with Dafny ${{inputs.mpl-dafny}} + working-directory: submodules/MaterialProviders/submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders + run: | + # This works because `node` is installed by default on GHA runners + CORES=$(node -e 'console.log(os.cpus().length)') + make build_java CORES=$CORES + + - name: Setup DBESDK Dafny + uses: dafny-lang/setup-dafny-action@v1.7.2 + with: + dafny-version: ${{ inputs.dbesdk-dafny}} + + - name: Build ${{ matrix.library }} implementation + shell: bash + working-directory: ./${{ matrix.library }} + run: | + make transpile_implementation_java + make transpile_test_java + + - name: Test ${{ matrix.library }} + working-directory: ./${{ matrix.library }} + run: | + make test_java From e9220410b23d27816ddcdc6846fb4b7e1c41b9b1 Mon Sep 17 00:00:00 2001 From: Jose Corella Date: Fri, 16 Aug 2024 11:20:16 -0700 Subject: [PATCH 2/2] format --- .github/workflows/dafny-interop.yml | 5 ++--- .github/workflows/dafny_interop_java.yml | 6 +++--- 2 files changed, 5 insertions(+), 6 deletions(-) diff --git a/.github/workflows/dafny-interop.yml b/.github/workflows/dafny-interop.yml index bbc375903..3db81b28c 100644 --- a/.github/workflows/dafny-interop.yml +++ b/.github/workflows/dafny-interop.yml @@ -1,7 +1,6 @@ - # This workflow is for testing backwards compatibility of a dafny version # and tests if a project that consumes the mpl will be backwards compatible with -# a newer version of Dafny +# a newer version of Dafny name: Dafny Interoperability Test on: @@ -20,7 +19,7 @@ on: description: "The Dafny version to compile the DBESDK with (4.2.0, dafny-nightly, etc..)" required: true type: string - + jobs: dafny-interop-java: uses: ./.github/workflows/dafny_interop_java.yml diff --git a/.github/workflows/dafny_interop_java.yml b/.github/workflows/dafny_interop_java.yml index 5d35ef59b..3eda6dc07 100644 --- a/.github/workflows/dafny_interop_java.yml +++ b/.github/workflows/dafny_interop_java.yml @@ -61,19 +61,19 @@ jobs: with: distribution: "corretto" java-version: ${{ matrix.java-version }} - + - name: Build MPL with Dafny ${{inputs.mpl-dafny}} working-directory: submodules/MaterialProviders/submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders run: | # This works because `node` is installed by default on GHA runners CORES=$(node -e 'console.log(os.cpus().length)') make build_java CORES=$CORES - + - name: Setup DBESDK Dafny uses: dafny-lang/setup-dafny-action@v1.7.2 with: dafny-version: ${{ inputs.dbesdk-dafny}} - + - name: Build ${{ matrix.library }} implementation shell: bash working-directory: ./${{ matrix.library }}