From 622dca58e2fd82b1a6ccd4e117a6a57237946df3 Mon Sep 17 00:00:00 2001 From: Jose Corella Date: Mon, 19 Aug 2024 16:11:54 -0700 Subject: [PATCH] chore(GHA): update nightlies for interop and interop action --- .github/workflows/dafny-interop.yml | 60 ++++----- .../workflows/dafny_interop_examples_java.yml | 92 +++++++++++++ .../workflows/dafny_interop_examples_net.yml | 100 ++++++++++++++ .github/workflows/dafny_interop_java.yml | 6 +- .github/workflows/dafny_interop_test_net.yml | 124 ++++++++++++++++++ .../dafny_interop_test_vector_java.yml | 101 ++++++++++++++ .../dafny_interop_test_vector_net.yml | 102 ++++++++++++++ .github/workflows/nightly.yml | 36 +++++ 8 files changed, 588 insertions(+), 33 deletions(-) create mode 100644 .github/workflows/dafny_interop_examples_java.yml create mode 100644 .github/workflows/dafny_interop_examples_net.yml create mode 100644 .github/workflows/dafny_interop_test_net.yml create mode 100644 .github/workflows/dafny_interop_test_vector_java.yml create mode 100644 .github/workflows/dafny_interop_test_vector_net.yml diff --git a/.github/workflows/dafny-interop.yml b/.github/workflows/dafny-interop.yml index 8ea19e432..93f81b012 100644 --- a/.github/workflows/dafny-interop.yml +++ b/.github/workflows/dafny-interop.yml @@ -27,33 +27,33 @@ jobs: 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}} + dafny-interop-java-test-vectors: + uses: ./.github/workflows/dafny_interop_test_vector_java.yml + with: + mpl-dafny: ${{inputs.mpl-dafny}} + mpl-commit: ${{inputs.mpl-commit}} + dbesdk-dafny: ${{inputs.dbesdk-dafny}} + dafny-interop-java-examples: + uses: ./.github/workflows/dafny_interop_examples_java.yml + with: + mpl-dafny: ${{inputs.mpl-dafny}} + mpl-commit: ${{inputs.mpl-commit}} + dbesdk-dafny: ${{inputs.dbesdk-dafny}} + dafny-interop-net: + uses: ./.github/workflows/dafny_interop_test_net.yml + with: + mpl-dafny: ${{inputs.mpl-dafny}} + mpl-commit: ${{inputs.mpl-commit}} + dbesdk-dafny: ${{inputs.dbesdk-dafny}} + dafny-interop-net-test-vectors: + uses: ./.github/workflows/dafny_interop_test_vector_net.yml + with: + mpl-dafny: ${{inputs.mpl-dafny}} + mpl-commit: ${{inputs.mpl-commit}} + dbesdk-dafny: ${{inputs.dbesdk-dafny}} + dafny-interop-net-examples: + uses: ./.github/workflows/dafny_interop_examples_net.yml + with: + mpl-dafny: ${{inputs.mpl-dafny}} + mpl-commit: ${{inputs.mpl-commit}} + dbesdk-dafny: ${{inputs.dbesdk-dafny}} diff --git a/.github/workflows/dafny_interop_examples_java.yml b/.github/workflows/dafny_interop_examples_java.yml new file mode 100644 index 000000000..92aea2202 --- /dev/null +++ b/.github/workflows/dafny_interop_examples_java.yml @@ -0,0 +1,92 @@ +# This workflow performs tests in Java with MPL nightly latest. +name: Library Java Backwards Example 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: + testExamplesJava: + strategy: + max-parallel: 1 + matrix: + 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 + 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/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 implementation + shell: bash + working-directory: ./DynamoDbEncryption + run: | + make transpile_implementation_java + make transpile_test_java + make mvn_local_deploy + + - name: Test Examples + working-directory: ./Examples + run: | + # Run simple examples + gradle -p runtimes/java/DynamoDbEncryption test + # Run migration examples + gradle -p runtimes/java/Migration/PlaintextToAWSDBE test + gradle -p runtimes/java/Migration/DDBECToAWSDBE test diff --git a/.github/workflows/dafny_interop_examples_net.yml b/.github/workflows/dafny_interop_examples_net.yml new file mode 100644 index 000000000..5fcc96ece --- /dev/null +++ b/.github/workflows/dafny_interop_examples_net.yml @@ -0,0 +1,100 @@ +# This workflow performs tests in DotNet with MPL nightly latest. +name: Library DotNet Backwards Interop Example 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: + dotNetExamples: + strategy: + matrix: + library: [DynamoDbEncryption] + dotnet-version: ["6.0.x"] + os: [macos-12] + runs-on: ${{ matrix.os }} + permissions: + id-token: write + contents: read + env: + DOTNET_CLI_TELEMETRY_OPTOUT: 1 + DOTNET_NOLOGO: 1 + steps: + - name: Support longpaths on Git checkout + run: | + git config --global core.longpaths true + - uses: actions/checkout@v3 + with: + submodules: recursive + fetch-depth: 0 + + - name: Setup .NET Core SDK ${{ matrix.dotnet-version }} + uses: actions/setup-dotnet@v4 + with: + dotnet-version: ${{ matrix.dotnet-version }} + + - name: Setup MPL Dafny + uses: dafny-lang/setup-dafny-action@v1.7.2 + with: + dafny-version: ${{ inputs.mpl-dafny }} + + - name: Update MPL submodule + working-directory: submodules/MaterialProviders + run: | + git fetch + git checkout ${{inputs.mpl-commit}} + git pull + git submodule update --init --recursive + git rev-parse HEAD + + - name: Download Dependencies + working-directory: ./${{ matrix.library }} + run: make setup_net + + - 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-Net-Tests + + - name: Compile MPL with Dafny ${{inputs.mpl-dafny}} + shell: bash + working-directory: submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders + run: | + make setup_net + # This works because `node` is installed by default on GHA runners + CORES=$(node -e 'console.log(os.cpus().length)') + make transpile_net CORES=$CORES + + - name: Setup DBESDK Dafny + uses: dafny-lang/setup-dafny-action@v1.7.2 + with: + dafny-version: ${{ inputs.dbesdk-dafny}} + + - name: Compile ${{ matrix.library }} implementation + shell: bash + working-directory: ./${{ matrix.library }} + run: | + # This works because `node` is installed by default on GHA runners + CORES=$(node -e 'console.log(os.cpus().length)') + make transpile_implementation_net CORES=$CORES + make transpile_test_net CORES=$CORES + - name: Run Examples + working-directory: ./Examples/runtimes/net + shell: bash + run: | + dotnet run diff --git a/.github/workflows/dafny_interop_java.yml b/.github/workflows/dafny_interop_java.yml index 98ad044cf..457f64d1d 100644 --- a/.github/workflows/dafny_interop_java.yml +++ b/.github/workflows/dafny_interop_java.yml @@ -1,5 +1,5 @@ -# This workflow performs tests in Java. -name: Library Java tests +# This workflow performs tests in Java with MPL nightly latest. +name: Library Java Backwards Interop Tests on: workflow_call: @@ -47,7 +47,7 @@ jobs: with: dafny-version: ${{ inputs.mpl-dafny }} - - name: Update MPL submodule if using MPL HEAD + - name: Update MPL submodule working-directory: submodules/MaterialProviders run: | git fetch diff --git a/.github/workflows/dafny_interop_test_net.yml b/.github/workflows/dafny_interop_test_net.yml new file mode 100644 index 000000000..276db70a7 --- /dev/null +++ b/.github/workflows/dafny_interop_test_net.yml @@ -0,0 +1,124 @@ +# This workflow performs tests in DotNet with MPL nightly latest. +name: Library DotNet Backwards Interop 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: + testDotNet: + strategy: + matrix: + library: [DynamoDbEncryption] + dotnet-version: ["6.0.x"] + os: [macos-12, ubuntu-latest, windows-latest] + runs-on: ${{ matrix.os }} + permissions: + id-token: write + contents: read + env: + DOTNET_CLI_TELEMETRY_OPTOUT: 1 + DOTNET_NOLOGO: 1 + steps: + - name: Support longpaths on Git checkout + run: | + git config --global core.longpaths true + - uses: actions/checkout@v3 + with: + submodules: recursive + fetch-depth: 0 + + - name: Setup .NET Core SDK ${{ matrix.dotnet-version }} + uses: actions/setup-dotnet@v4 + with: + dotnet-version: ${{ matrix.dotnet-version }} + + - name: Setup MPL Dafny + uses: dafny-lang/setup-dafny-action@v1.7.2 + with: + dafny-version: ${{ inputs.mpl-dafny }} + + - name: Update MPL submodule + working-directory: submodules/MaterialProviders + run: | + git fetch + git checkout ${{inputs.mpl-commit}} + git pull + git submodule update --init --recursive + git rev-parse HEAD + + - name: Download Dependencies + working-directory: ./${{ matrix.library }} + run: make setup_net + + - 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-Net-Tests + + - name: Compile MPL with Dafny ${{inputs.mpl-dafny}} + shell: bash + working-directory: submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders + run: | + make setup_net + # This works because `node` is installed by default on GHA runners + CORES=$(node -e 'console.log(os.cpus().length)') + make transpile_net CORES=$CORES + + - name: Setup DBESDK Dafny + uses: dafny-lang/setup-dafny-action@v1.7.2 + with: + dafny-version: ${{ inputs.dbesdk-dafny}} + + - name: Compile ${{ matrix.library }} implementation + shell: bash + working-directory: ./${{ matrix.library }} + run: | + # This works because `node` is installed by default on GHA runners + CORES=$(node -e 'console.log(os.cpus().length)') + make transpile_implementation_net CORES=$CORES + make transpile_test_net CORES=$CORES + + - name: Test ${{ matrix.library }} net48 + if: matrix.os == 'windows-latest' + working-directory: ./${{ matrix.library }} + shell: bash + run: | + dotnet restore runtimes/net/tests + dotnet build runtimes/net/tests + make test_net FRAMEWORK=net48 + + - name: Test ${{ matrix.library }} net6.0 + working-directory: ./${{ matrix.library }} + shell: bash + run: | + dotnet restore runtimes/net/tests + dotnet build runtimes/net/tests + if [ "$RUNNER_OS" == "macOS" ]; then + make test_net_mac_intel + else + make test_net FRAMEWORK=net6.0 + fi + + - name: Test Build and Pack ${{ matrix.library}} + shell: bash + if: matrix.os != 'windows-latest' + working-directory: ./${{ matrix.library }} + run: | + dotnet build runtimes/net /p:Configuration=Release -nowarn:CS0162,CS0168 + dotnet pack runtimes/net/DynamoDbEncryption.csproj --no-build /p:Configuration=Release --output build diff --git a/.github/workflows/dafny_interop_test_vector_java.yml b/.github/workflows/dafny_interop_test_vector_java.yml new file mode 100644 index 000000000..a90478e8c --- /dev/null +++ b/.github/workflows/dafny_interop_test_vector_java.yml @@ -0,0 +1,101 @@ +# This workflow performs test vectors in Java with MPL nightly latest. +name: Library Java Test Vectors Backwards Interop 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, TestVectors] + java-version: [8, 11, 16, 17] + os: [ + # Run on ubuntu image that comes pre-configured with docker + ubuntu-latest, + ] + runs-on: ${{ matrix.os }} + permissions: + id-token: write + contents: read + steps: + - name: Setup DynamoDB Local + uses: rrainn/dynamodb-action@v4.0.0 + with: + port: 8000 + cors: "*" + + - 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: Setup Dafny + uses: dafny-lang/setup-dafny-action@v1.7.2 + with: + dafny-version: ${{ inputs.dafny }} + + - name: Update MPL submodule + 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/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 TestVectors implementation + shell: bash + working-directory: ${{matrix.library}} + run: | + make transpile_implementation_java + make transpile_test_java + + - name: Test TestVectors + working-directory: ./TestVectors + run: | + make test_java diff --git a/.github/workflows/dafny_interop_test_vector_net.yml b/.github/workflows/dafny_interop_test_vector_net.yml new file mode 100644 index 000000000..1d26e5798 --- /dev/null +++ b/.github/workflows/dafny_interop_test_vector_net.yml @@ -0,0 +1,102 @@ +# This workflow performs tests in DotNet with MPL nightly latest. +name: Library DotNet Backwards Interop Test Vectors + +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: + testDotNet: + strategy: + matrix: + library: [DynamoDbEncryption, TestVectors] + dotnet-version: ["6.0.x"] + os: [macos-12, ubuntu-latest, windows-latest] + runs-on: ${{ matrix.os }} + permissions: + id-token: write + contents: read + env: + DOTNET_CLI_TELEMETRY_OPTOUT: 1 + DOTNET_NOLOGO: 1 + steps: + - name: Support longpaths on Git checkout + run: | + git config --global core.longpaths true + - uses: actions/checkout@v3 + with: + submodules: recursive + fetch-depth: 0 + + - name: Setup .NET Core SDK ${{ matrix.dotnet-version }} + uses: actions/setup-dotnet@v4 + with: + dotnet-version: ${{ matrix.dotnet-version }} + + - name: Setup MPL Dafny + uses: dafny-lang/setup-dafny-action@v1.7.2 + with: + dafny-version: ${{ inputs.mpl-dafny }} + + - name: Update MPL submodule + working-directory: submodules/MaterialProviders + run: | + git fetch + git checkout ${{inputs.mpl-commit}} + git pull + git submodule update --init --recursive + git rev-parse HEAD + + - name: Download Dependencies + working-directory: ./${{ matrix.library }} + run: make setup_net + + - 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-Net-Tests + + - name: Compile MPL with Dafny ${{inputs.mpl-dafny}} + shell: bash + working-directory: submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders + run: | + make setup_net + # This works because `node` is installed by default on GHA runners + CORES=$(node -e 'console.log(os.cpus().length)') + make transpile_net CORES=$CORES + + - name: Setup DBESDK Dafny + uses: dafny-lang/setup-dafny-action@v1.7.2 + with: + dafny-version: ${{ inputs.dbesdk-dafny}} + + - name: Build TestVectors implementation + shell: bash + working-directory: ${{matrix.library}} + run: | + # This works because `node` is installed by default on GHA runners + make transpile_implementation_net CORES=$CORES + make transpile_test_net CORES=$CORES + + - name: Test TestVectors on .NET 6.0 + working-directory: ./${{matrix.library}}/runtimes/net + run: | + cp ../java/decrypt_java_*.json ../java/decrypt_dotnet_*.json . + dotnet run + cp ../java/*.json . + dotnet run --framework net6.0 diff --git a/.github/workflows/nightly.yml b/.github/workflows/nightly.yml index 47122a905..74c95075c 100644 --- a/.github/workflows/nightly.yml +++ b/.github/workflows/nightly.yml @@ -11,6 +11,8 @@ on: - cron: "30 16 * * *" jobs: + getVersion: + uses: ./.github/workflows/dafny_version.yml dafny-nightly-format: # Don't run the cron builds on forks if: github.event_name != 'schedule' || github.repository_owner == 'aws' @@ -57,6 +59,40 @@ jobs: dafny: "nightly-latest" regenerate-code: true + # Interop nightly tests use nighly tests and the current dafnyversion for the DBESDK. + dafny-nightly-java-interop: + if: github.event_name != 'schedule' || github.repository_owner == 'aws' + needs: getVersion + uses: ./.github/workflows/dafny_interop_java.yml + with: + mpl-dafny: "nightly-latest" + mpl-commit: main + dbesdk-dafny: ${{needs.getVersion.outputs.version}} + dafny-nightly-test-vectors-java-interop: + if: github.event_name != 'schedule' || github.repository_owner == 'aws' + needs: getVersion + uses: ./.github/workflows/dafny_interop_test_vector_java.yml + with: + mpl-dafny: "nightly-latest" + mpl-commit: main + dbesdk-dafny: ${{needs.getVersion.outputs.version}} + dafny-nightly-net-interop: + if: github.event_name != 'schedule' || github.repository_owner == 'aws' + needs: getVersion + uses: ./.github/workflows/dafny_interop_test_net.yml + with: + mpl-dafny: "nightly-latest" + mpl-commit: main + dbesdk-dafny: ${{needs.getVersion.outputs.version}} + dafny-nightly-test-vectors-net-interop: + if: github.event_name != 'schedule' || github.repository_owner == 'aws' + needs: getVersion + uses: ./.github/workflows/dafny_interop_test_vector_net.yml + with: + mpl-dafny: "nightly-latest" + mpl-commit: main + dbesdk-dafny: ${{needs.getVersion.outputs.version}} + cut-issue-on-failure: runs-on: ubuntu-latest permissions: