From ef41e45e60b12f667be116f82e37040afd283b5a Mon Sep 17 00:00:00 2001 From: Jose Corella Date: Tue, 9 Jul 2024 15:06:09 -0700 Subject: [PATCH] refactor(GHA): make workflows reusable --- .github/workflows/check-files.yml | 68 ++++++++++++++ .github/workflows/ci_codegen.yml | 12 +-- .github/workflows/ci_examples_java.yml | 31 ++----- .github/workflows/ci_examples_net.yml | 25 ++++-- .github/workflows/ci_test_java.yml | 32 +++---- .github/workflows/ci_test_net.yml | 32 ++----- .github/workflows/ci_test_vector_java.yml | 31 +++++-- .github/workflows/ci_test_vector_net.yml | 31 +++++-- .github/workflows/ci_tv_verification.yml | 60 ------------- .github/workflows/ci_verification.yml | 76 ---------------- .github/workflows/dafny_verify_version.yml | 3 + .github/workflows/dafny_version.yml | 25 ++++++ .github/workflows/daily_ci.yml | 46 ++++++++++ .../workflows/library_dafny_verification.yml | 70 +++++++++++++++ .github/workflows/library_format.yml | 16 ++-- .github/workflows/manual.yml | 59 ++++++++++++ .github/workflows/nightly.yml | 90 +++++++++++++++++++ .github/workflows/pull.yml | 54 +++++++++++ .github/workflows/push.yml | 56 ++++++++++++ project.properties | 1 + 20 files changed, 586 insertions(+), 232 deletions(-) create mode 100644 .github/workflows/check-files.yml delete mode 100644 .github/workflows/ci_tv_verification.yml delete mode 100644 .github/workflows/ci_verification.yml create mode 100644 .github/workflows/dafny_verify_version.yml create mode 100644 .github/workflows/dafny_version.yml create mode 100644 .github/workflows/daily_ci.yml create mode 100644 .github/workflows/library_dafny_verification.yml create mode 100644 .github/workflows/manual.yml create mode 100644 .github/workflows/nightly.yml create mode 100644 .github/workflows/pull.yml create mode 100644 .github/workflows/push.yml diff --git a/.github/workflows/check-files.yml b/.github/workflows/check-files.yml new file mode 100644 index 000000000..420fbf87d --- /dev/null +++ b/.github/workflows/check-files.yml @@ -0,0 +1,68 @@ +# This workflow checks if specfic files were modified, +# if they were they require more than one approval from CODEOWNERS +name: Check Release Files + +on: + pull_request: + +jobs: + require-approvals: + runs-on: ubuntu-latest + permissions: + issues: write + pull-requests: write + env: + # unfortunately we can't check if the approver is part of the CODEOWNERS. This is a subset of aws/aws-crypto-tools-team + # to add more allowlisted approvers just modify this env variable + maintainers: seebees, texastony, ShubhamChaturvedi7, lucasmcdonald3, josecorella, imabhichow, rishav-karanjit, antonf-amzn, justplaz, ajewellamz + steps: + - uses: actions/checkout@v3 + with: + fetch-depth: 0 + + - name: Get Files changed + id: file-changes + shell: bash + run: + # *release.yml files are responsible for releasing builds + # we require multiple approvers if any of those files change + # when adding any release file, it must be appended with *release + # we also want to check if there are changes to this file + echo "FILES=$(git diff --name-only origin/main origin/${GITHUB_HEAD_REF} .github/workflows/*release.yml .github/workflows/check-files.yml | tr '\n' ' ')" >> "$GITHUB_OUTPUT" + + - name: Check if FILES is not empty + id: comment + env: + PR_NUMBER: ${{ github.event.number }} + GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} + FILES: ${{ steps.file-changes.outputs.FILES }} + if: ${{env.FILES != ''}} + run: | + COMMENT="Detected changes to the release files or to the check-files action" + COMMENT_URL="https://api.github.com/repos/${{ github.repository }}/issues/${PR_NUMBER}/comments" + curl -s -H "Authorization: token ${GITHUB_TOKEN}" -X POST $COMMENT_URL -d "{\"body\":\"$COMMENT\"}" + + - name: Check Approvers + id: approvers + if: steps.comment.outcome == 'success' + # if this step fails we want to continue to post a message on the PR. + continue-on-error: true + # we are using this action because it does the heavy lifting for us, it uses the github_token enabled + # for github actions, this is ok because tokens are created for every workflow run and they expire at the end + # of the job + uses: peternied/required-approval@v1.3 + with: + token: ${{ secrets.GITHUB_TOKEN }} + min-required: 2 + required-approvers-list: ${{env.maintainers}} + + - name: Post Approvers Result + if: steps.approvers.outcome == 'failure' + env: + PR_NUMBER: ${{ github.event.number }} + GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} + run: | + COMMENT="Changes to the release files or the check-files action requires 2 approvals from CODEOWNERS" + COMMENT_URL="https://api.github.com/repos/${{ github.repository }}/issues/${PR_NUMBER}/comments" + curl -s -H "Authorization: token ${GITHUB_TOKEN}" -X POST $COMMENT_URL -d "{\"body\":\"$COMMENT\"}" + exit 1 diff --git a/.github/workflows/ci_codegen.yml b/.github/workflows/ci_codegen.yml index ee88f5286..fdb869d7f 100644 --- a/.github/workflows/ci_codegen.yml +++ b/.github/workflows/ci_codegen.yml @@ -1,10 +1,12 @@ # This workflow regenerates code using smithy-dafny and checks that the output matches what's checked in. name: Library Code Generation on: - pull_request: - push: - branches: - - main + workflow_call: + inputs: + dafny: + description: "The dafny version to run" + required: true + type: string jobs: code-generation: @@ -38,7 +40,7 @@ jobs: - name: Setup Dafny uses: dafny-lang/setup-dafny-action@v1.7.0 with: - dafny-version: 4.2.0 + dafny-version: ${{ inputs.dafny }} - name: Setup .NET Core SDK ${{ matrix.dotnet-version }} uses: actions/setup-dotnet@v4 diff --git a/.github/workflows/ci_examples_java.yml b/.github/workflows/ci_examples_java.yml index 15f849ee9..f3354fbdf 100644 --- a/.github/workflows/ci_examples_java.yml +++ b/.github/workflows/ci_examples_java.yml @@ -2,31 +2,20 @@ name: Java Examples on: - pull_request: - push: - branches: - - main - workflow_dispatch: - # Manual trigger for this workflow, either the normal version - # or the nightly build that uses the latest Dafny prerelease - # (accordingly to the "nightly" parameter). + workflow_call: inputs: - nightly: - description: "Run the nightly build" + dafny: + description: "The Dafny version to run" + required: true + type: string + regenerate-code: + description: "Regenerate code using smithy-dafny" required: false + default: false type: boolean - schedule: - # Nightly build against Dafny's nightly prereleases, - # for early warning of verification issues or regressions. - # Timing chosen to be adequately after Dafny's own nightly build, - # but this might need to be tweaked: - # https://github.com/dafny-lang/dafny/blob/master/.github/workflows/deep-tests.yml#L16 - - cron: "30 16 * * *" jobs: testJava: - # Don't run the nightly build on forks - if: github.event_name != 'schedule' || github.repository_owner == 'aws' strategy: max-parallel: 1 matrix: @@ -57,11 +46,9 @@ jobs: - name: Setup Dafny uses: dafny-lang/setup-dafny-action@v1.7.0 with: - # A && B || C is the closest thing to an if .. then ... else ... or ?: expression the GitHub Actions syntax supports. - dafny-version: ${{ (github.event_name == 'schedule' || inputs.nightly) && 'nightly-latest' || '4.2.0' }} + dafny-version: ${{ inputs.dafny }} - name: Regenerate code using smithy-dafny if necessary - if: ${{ github.event_name == 'schedule' || inputs.nightly }} uses: ./.github/actions/polymorph_codegen with: dafny: ${{ env.DAFNY_VERSION }} diff --git a/.github/workflows/ci_examples_net.yml b/.github/workflows/ci_examples_net.yml index 5e70ce483..76958d564 100644 --- a/.github/workflows/ci_examples_net.yml +++ b/.github/workflows/ci_examples_net.yml @@ -2,10 +2,17 @@ name: dotnet examples on: - pull_request: - push: - branches: - - main + workflow_call: + inputs: + dafny: + description: "The Dafny version to run" + required: true + type: string + regenerate-code: + description: "Regenerate code using smithy-dafny" + required: false + default: false + type: boolean jobs: dotNetExamples: @@ -36,7 +43,15 @@ jobs: - name: Setup Dafny uses: dafny-lang/setup-dafny-action@v1.7.0 with: - dafny-version: ${{ '4.2.0' }} + dafny-version: ${{ inputs.dafny }} + + - name: Regenerate code using smithy-dafny if necessary + uses: ./.github/actions/polymorph_codegen + with: + dafny: ${{ env.DAFNY_VERSION }} + library: DynamoDbEncryption + diff-generated-code: false + update-and-regenerate-mpl: true - name: Download Dependencies working-directory: ./${{ matrix.library }} diff --git a/.github/workflows/ci_test_java.yml b/.github/workflows/ci_test_java.yml index 4a9b44de0..a4e9a26be 100644 --- a/.github/workflows/ci_test_java.yml +++ b/.github/workflows/ci_test_java.yml @@ -2,31 +2,20 @@ name: Library Java tests on: - pull_request: - push: - branches: - - main - workflow_dispatch: - # Manual trigger for this workflow, either the normal version - # or the nightly build that uses the latest Dafny prerelease - # (accordingly to the "nightly" parameter). + workflow_call: inputs: - nightly: - description: "Run the nightly build" + dafny: + description: "The Dafny version to run" + required: true + type: string + regenerate-code: + description: "Regenerate code using smithy-dafny" required: false + default: false type: boolean - schedule: - # Nightly build against Dafny's nightly prereleases, - # for early warning of verification issues or regressions. - # Timing chosen to be adequately after Dafny's own nightly build, - # but this might need to be tweaked: - # https://github.com/dafny-lang/dafny/blob/master/.github/workflows/deep-tests.yml#L16 - - cron: "30 16 * * *" jobs: testJava: - # Don't run the nightly build on forks - if: github.event_name != 'schedule' || github.repository_owner == 'aws' strategy: matrix: library: [DynamoDbEncryption] @@ -51,11 +40,10 @@ jobs: - name: Setup Dafny uses: dafny-lang/setup-dafny-action@v1.7.0 with: - # A && B || C is the closest thing to an if .. then ... else ... or ?: expression the GitHub Actions syntax supports. - dafny-version: ${{ (github.event_name == 'schedule' || inputs.nightly) && 'nightly-latest' || '4.2.0' }} + dafny-version: ${{ inputs.dafny }} - name: Regenerate code using smithy-dafny if necessary - if: ${{ github.event_name == 'schedule' || inputs.nightly }} + if: ${{ inputs.regenerate-code }} uses: ./.github/actions/polymorph_codegen with: dafny: ${{ env.DAFNY_VERSION }} diff --git a/.github/workflows/ci_test_net.yml b/.github/workflows/ci_test_net.yml index a697f596d..96cf3d9e0 100644 --- a/.github/workflows/ci_test_net.yml +++ b/.github/workflows/ci_test_net.yml @@ -2,32 +2,20 @@ name: test dotnet on: - pull_request: - push: - branches: - - main - workflow_dispatch: - # Manual trigger for this workflow, either the normal version - # or the nightly build that uses the latest Dafny prerelease - # (accordingly to the "nightly" parameter). + workflow_call: inputs: - nightly: - description: "Run the nightly build" + dafny: + description: "The Dafny version to run" + required: true + type: string + regenerate-code: + description: "Regenerate code using smithy-dafny" required: false + default: false type: boolean - schedule: - # Nightly build against Dafny's nightly prereleases, - # for early warning of verification issues or regressions. - # Timing chosen to be adequately after Dafny's own nightly build, - # but this might need to be tweaked: - # https://github.com/dafny-lang/dafny/blob/master/.github/workflows/deep-tests.yml#L16 - - cron: "30 16 * * *" jobs: testDotNet: - # Don't run the nightly build on forks - # Disabled until we reintroduce DynamoDbEncryption, since a matrix vector cannot be empty - if: (github.event_name != 'schedule' || github.repository_owner == 'aws') strategy: matrix: library: [DynamoDbEncryption] @@ -56,11 +44,9 @@ jobs: - name: Setup Dafny uses: dafny-lang/setup-dafny-action@v1.7.0 with: - # A && B || C is the closest thing to an if .. then ... else ... or ?: expression the GitHub Actions syntax supports. - dafny-version: ${{ (github.event_name == 'schedule' || inputs.nightly) && 'nightly-latest' || '4.2.0' }} + dafny-version: ${{ inputs.dafny }} - name: Regenerate code using smithy-dafny if necessary - if: ${{ github.event_name == 'schedule' || inputs.nightly }} uses: ./.github/actions/polymorph_codegen with: dafny: ${{ env.DAFNY_VERSION }} diff --git a/.github/workflows/ci_test_vector_java.yml b/.github/workflows/ci_test_vector_java.yml index e148f3703..e1607eb88 100644 --- a/.github/workflows/ci_test_vector_java.yml +++ b/.github/workflows/ci_test_vector_java.yml @@ -2,15 +2,23 @@ name: Library Java Test Vectors on: - pull_request: - push: - branches: - - main + workflow_call: + inputs: + dafny: + description: "The Dafny version to run" + required: true + type: string + regenerate-code: + description: "Regenerate code using smithy-dafny" + required: false + default: false + type: boolean jobs: testJava: strategy: matrix: + library: [TestVectors] java-version: [8, 11, 16, 17] os: [ # Run on ubuntu image that comes pre-configured with docker @@ -41,7 +49,16 @@ jobs: - name: Setup Dafny uses: dafny-lang/setup-dafny-action@v1.7.0 with: - dafny-version: "4.2.0" + dafny-version: ${{ inputs.dafny }} + + - name: Regenerate code using smithy-dafny if necessary + if: ${{ inputs.regenerate-code }} + uses: ./.github/actions/polymorph_codegen + with: + dafny: ${{ env.DAFNY_VERSION }} + library: ${{ matrix.library }} + diff-generated-code: false + update-and-regenerate-mpl: true - name: Setup Java ${{ matrix.java-version }} uses: actions/setup-java@v4 @@ -51,13 +68,13 @@ jobs: - name: Build TestVectors implementation shell: bash - working-directory: ./TestVectors + 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 build_java CORES=$CORES - name: Test TestVectors - working-directory: ./TestVectors + working-directory: ${{matrix.library}} run: | make test_java diff --git a/.github/workflows/ci_test_vector_net.yml b/.github/workflows/ci_test_vector_net.yml index e3b75f47d..8552edd35 100644 --- a/.github/workflows/ci_test_vector_net.yml +++ b/.github/workflows/ci_test_vector_net.yml @@ -2,15 +2,23 @@ name: Library DotNet Test Vectors on: - pull_request: - push: - branches: - - main + workflow_call: + inputs: + dafny: + description: "The Dafny version to run" + required: true + type: string + regenerate-code: + description: "Regenerate code using smithy-dafny" + required: false + default: false + type: boolean jobs: testDotNet: strategy: matrix: + library: [TestVectors] dotnet-version: ["6.0.x"] os: [ # Run on ubuntu image that comes pre-configured with docker @@ -41,7 +49,16 @@ jobs: - name: Setup Dafny uses: dafny-lang/setup-dafny-action@v1.7.0 with: - dafny-version: "4.2.0" + dafny-version: ${{ inputs.dafny }} + + - name: Regenerate code using smithy-dafny if necessary + if: ${{ inputs.regenerate-code }} + uses: ./.github/actions/polymorph_codegen + with: + dafny: ${{ env.DAFNY_VERSION }} + library: ${{ matrix.library }} + diff-generated-code: false + update-and-regenerate-mpl: true - name: Setup .NET Core SDK ${{ matrix.dotnet-version }} uses: actions/setup-dotnet@v4 @@ -50,13 +67,13 @@ jobs: - name: Build TestVectors implementation shell: bash - working-directory: ./TestVectors + working-directory: ${{matrix.library}} run: | # This works because `node` is installed by default on GHA runners make transpile_net - name: Test TestVectors on .NET 6.0 - working-directory: ./TestVectors/runtimes/net + working-directory: ./${{matrix.library}}/runtimes/net run: | cp ../java/decrypt_java_*.json ../java/decrypt_dotnet_*.json . dotnet run diff --git a/.github/workflows/ci_tv_verification.yml b/.github/workflows/ci_tv_verification.yml deleted file mode 100644 index c4a4a6591..000000000 --- a/.github/workflows/ci_tv_verification.yml +++ /dev/null @@ -1,60 +0,0 @@ -# This workflow performs verification checks -name: test vector verification - -on: - pull_request: - push: - branches: - - main - workflow_dispatch: - # Manual trigger for this workflow, either the normal version - # or the nightly build that uses the latest Dafny prerelease - # (accordingly to the "nightly" parameter). - inputs: - nightly: - description: "Run the nightly build" - required: false - type: boolean - schedule: - # Nightly build against Dafny's nightly prereleases, - # for early warning of verification issues or regressions. - # Timing chosen to be adequately after Dafny's own nightly build, - # but this might need to be tweaked: - # https://github.com/dafny-lang/dafny/blob/master/.github/workflows/deep-tests.yml#L16 - - cron: "30 16 * * *" - -jobs: - verification: - # Don't run the nightly build on forks - if: github.event_name != 'schedule' || github.repository_owner == 'aws' - strategy: - matrix: - # Break up verification between namespaces over multiple - # actions to take advantage of parallelization - service: [DDBEncryption] - os: [macos-12] - runs-on: ${{ matrix.os }} - steps: - - uses: actions/checkout@v3 - with: - submodules: recursive - - - name: Setup Dafny - uses: dafny-lang/setup-dafny-action@v1.7.0 - with: - # A && B || C is the closest thing to an if .. then ... else ... or ?: expression the GitHub Actions syntax supports. - dafny-version: ${{ (github.event_name == 'schedule' || inputs.nightly) && 'nightly-latest' || '4.2.0' }} - - - name: Verify ${{ matrix.library }} Dafny code - shell: bash - working-directory: ./TestVectors - run: | - # This works because `node` is installed by default on GHA runners - CORES=$(node -e 'console.log(os.cpus().length)') - make verify_service CORES=$CORES SERVICE=${{ matrix.service }} - - - name: Check solver resource use - shell: bash - working-directory: ./TestVectors - run: | - make dafny-reportgenerator diff --git a/.github/workflows/ci_verification.yml b/.github/workflows/ci_verification.yml deleted file mode 100644 index 27ebac75a..000000000 --- a/.github/workflows/ci_verification.yml +++ /dev/null @@ -1,76 +0,0 @@ -# This workflow performs verification checks -name: verification - -on: - pull_request: - push: - branches: - - main - workflow_dispatch: - # Manual trigger for this workflow, either the normal version - # or the nightly build that uses the latest Dafny prerelease - # (accordingly to the "nightly" parameter). - inputs: - nightly: - description: "Run the nightly build" - required: false - type: boolean - schedule: - # Nightly build against Dafny's nightly prereleases, - # for early warning of verification issues or regressions. - # Timing chosen to be adequately after Dafny's own nightly build, - # but this might need to be tweaked: - # https://github.com/dafny-lang/dafny/blob/master/.github/workflows/deep-tests.yml#L16 - - cron: "30 16 * * *" - -jobs: - verification: - # Don't run the nightly build on forks - if: github.event_name != 'schedule' || github.repository_owner == 'aws' - strategy: - fail-fast: false - matrix: - # Break up verification between namespaces over multiple - # actions to take advantage of parallelization - service: - [ - DynamoDbEncryption, - DynamoDbEncryptionTransforms, - DynamoDbItemEncryptor, - StructuredEncryption, - ] - os: [macos-12] - runs-on: ${{ matrix.os }} - steps: - - uses: actions/checkout@v3 - with: - submodules: recursive - - - name: Setup Dafny - uses: dafny-lang/setup-dafny-action@v1.7.0 - with: - # A && B || C is the closest thing to an if .. then ... else ... or ?: expression the GitHub Actions syntax supports. - dafny-version: ${{ (github.event_name == 'schedule' || inputs.nightly) && 'nightly-latest' || '4.7.0' }} - - - name: Regenerate code using smithy-dafny if necessary - if: ${{ github.event_name == 'schedule' || inputs.nightly }} - uses: ./.github/actions/polymorph_codegen - with: - dafny: ${{ env.DAFNY_VERSION }} - library: DynamoDbEncryption - diff-generated-code: false - update-and-regenerate-mpl: true - - - name: Verify ${{ matrix.service }} Dafny code - shell: bash - working-directory: ./DynamoDbEncryption - run: | - # This works because `node` is installed by default on GHA runners - CORES=$(node -e 'console.log(os.cpus().length)') - make verify_service CORES=$CORES SERVICE=${{ matrix.service }} - - - name: Check solver resource use - shell: bash - working-directory: ./DynamoDbEncryption - run: | - make dafny-reportgenerator diff --git a/.github/workflows/dafny_verify_version.yml b/.github/workflows/dafny_verify_version.yml new file mode 100644 index 000000000..c90950bd5 --- /dev/null +++ b/.github/workflows/dafny_verify_version.yml @@ -0,0 +1,3 @@ +# This workflow reads the project.properties +# into the enviornment variables +# and then creates an output variable for `dafnyVerifyVersion` diff --git a/.github/workflows/dafny_version.yml b/.github/workflows/dafny_version.yml new file mode 100644 index 000000000..80ca46bdc --- /dev/null +++ b/.github/workflows/dafny_version.yml @@ -0,0 +1,25 @@ +# This workflow reads the project.properties +# into the environment variables +# and then creates an output variable for `dafnyVersion` +name: Dafny Version + +on: + workflow_call: + outputs: + version: + description: "The dafny version" + value: ${{ jobs.getDafnyVersion.outputs.version }} + +jobs: + getDafnyVersion: + runs-on: ubuntu-latest + outputs: + version: ${{ steps.read_property.outputs.dafnyVersion }} + steps: + - uses: actions/checkout@v4 + - name: Read version from Properties-file + id: read_property + uses: christian-draeger/read-properties@1.1.1 + with: + path: "./project.properties" + properties: "dafnyVersion" diff --git a/.github/workflows/daily_ci.yml b/.github/workflows/daily_ci.yml new file mode 100644 index 000000000..07ae283a0 --- /dev/null +++ b/.github/workflows/daily_ci.yml @@ -0,0 +1,46 @@ +# This workflow runs every weekday at 16:00 UTC (9AM PDT) +name: Daily CI + +on: + schedule: + - cron: "00 16 * * 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.yaml + getVerifyVersion: + if: github.event_name != 'schedule' || github.repository_owner == 'aws' + uses: ./.github/workflows/dafny_verify_version.yaml + daily-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}} + daily-ci-codegen: + needs: getVersion + if: github.event_name != 'schedule' || github.repository_owner == 'aws' + uses: ./.github/workflows/library_codegen.yml + with: + dafny: ${{needs.getVersion.outputs.version}} + daily-ci-verification: + needs: getVerifyVersion + if: github.event_name != 'schedule' || github.repository_owner == 'aws' + uses: ./.github/workflows/library_dafny_verification.yml + with: + dafny: ${{needs.getVerifyVersion.outputs.version}} + daily-ci-java: + needs: getVersion + if: github.event_name != 'schedule' || github.repository_owner == 'aws' + uses: ./.github/workflows/library_java_tests.yml + with: + dafny: ${{needs.getVersion.outputs.version}} + daily-ci-net: + needs: getVersion + if: github.event_name != 'schedule' || github.repository_owner == 'aws' + uses: ./.github/workflows/library_net_tests.yml + with: + dafny: ${{needs.getVersion.outputs.version}} + diff --git a/.github/workflows/library_dafny_verification.yml b/.github/workflows/library_dafny_verification.yml new file mode 100644 index 000000000..f21e11437 --- /dev/null +++ b/.github/workflows/library_dafny_verification.yml @@ -0,0 +1,70 @@ +# This workflow performs static analysis checks. +name: Library Dafny verification + +on: + workflow_call: + inputs: + dafny: + description: "The Dafny version to run" + required: true + type: string + regenerate-code: + description: "Regenerate code using smithy-dafny" + required: false + default: false + type: boolean + +jobs: + verification: + # Don't run the nightly build on forks + if: github.event_name != 'schedule' || github.repository_owner == 'aws' + strategy: + matrix: + # Break up verification between namespaces over multiple + # actions to take advantage of parallelization + library: [DDBEncryption, TestVectors] + os: [macos-12] + runs-on: ${{ matrix.os }} + defaults: + run: + shell: bash + env: + DOTNET_CLI_TELEMETRY_OPTOUT: 1 + DOTNET_NOLOGO: 1 + steps: + - uses: actions/checkout@v3 + with: + submodules: recursive + + - name: Setup Dafny + uses: dafny-lang/setup-dafny-action@v1.7.0 + with: + dafny-version: ${{ inputs.dafny }} + + # dafny-reportgenerator requires next6 + # but only 7.0 is installed on macos-12-large + - name: Setup .NET Core SDK '6.0.x' + uses: actions/setup-dotnet@v3 + with: + dotnet-version: "6.0.x" + + - name: Regenerate code using smithy-dafny if necessary + if: ${{ inputs.regenerate-code }} + uses: ./.github/actions/polymorph_codegen + with: + dafny: ${{ env.DAFNY_VERSION }} + library: ${{ matrix.library }} + diff-generated-code: false + + - name: Verify ${{ matrix.library }} Dafny code + 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 verify CORES=$CORES + + - name: Check solver resource use + if: success() || failure() + working-directory: ./${{ matrix.library }} + run: | + make dafny-reportgenerator \ No newline at end of file diff --git a/.github/workflows/library_format.yml b/.github/workflows/library_format.yml index bbefa84de..7a7cf3259 100644 --- a/.github/workflows/library_format.yml +++ b/.github/workflows/library_format.yml @@ -2,11 +2,17 @@ name: Library format check on: - pull_request: - push: - branches: - - main - + workflow_call: + inputs: + dafny: + description: "The Dafny version to run" + required: true + type: string + regenerate-code: + description: "Regenerate code using smithy-dafny" + required: false + default: false + type: boolean jobs: format_projects: # Don't run the nightly build on forks diff --git a/.github/workflows/manual.yml b/.github/workflows/manual.yml new file mode 100644 index 000000000..ea03bc2bf --- /dev/null +++ b/.github/workflows/manual.yml @@ -0,0 +1,59 @@ +# This workflow invokes other workflows with the requested Dafny build. +# It is primarily meant for manual compatibility testing, +# such as trying out what the next pending nightly build will do ahead of time. +name: Manual CI + +on: + workflow_dispatch: + inputs: + dafny: + description: "The Dafny version to use" + required: true + type: string + regenerate-code: + description: "Regenerate code using smithy-dafny" + required: false + default: true + type: boolean + +jobs: + manual-ci-format: + uses: ./.github/workflows/library_format.yml + with: + dafny: ${{ inputs.dafny }} + regenerate-code: ${{ inputs.regenerate-code }} + manual-ci-verification: + uses: ./.github/workflows/library_dafny_verification.yml + with: + dafny: ${{ inputs.dafny }} + regenerate-code: ${{ inputs.regenerate-code }} + manual-ci-java: + uses: ./.github/workflows/ci_test_java.yml + with: + dafny: ${{ inputs.dafny }} + regenerate-code: ${{ inputs.regenerate-code }} + manual-ci-java-test-vectors: + uses: ./.github/workflows/ci_test_vector_java.yml + with: + dafny: ${{ inputs.dafny }} + regenerate-code: ${{ inputs.regenerate-code }} + manual-ci-java-examples: + uses: ./.github/workflows/ci_examples_java.yml + with: + dafny: ${{ inputs.dafny }} + regenerate-code: ${{ inputs.regenerate-code }} + manual-ci-net: + uses: ./.github/workflows/ci_test_net.yml + with: + dafny: ${{ inputs.dafny }} + regenerate-code: ${{ inputs.regenerate-code }} + manual-ci-net-test-vectors: + uses: ./.github/workflows/ci_test_vector_net.yml + with: + dafny: ${{ inputs.dafny }} + regenerate-code: ${{ inputs.regenerate-code }} + manual-ci-net-examples: + uses: ./.github/workflows/ci_examples_net.yml + with: + dafny: ${{ inputs.dafny }} + regenerate-code: ${{ inputs.regenerate-code }} \ No newline at end of file diff --git a/.github/workflows/nightly.yml b/.github/workflows/nightly.yml new file mode 100644 index 000000000..9f6ae9e39 --- /dev/null +++ b/.github/workflows/nightly.yml @@ -0,0 +1,90 @@ +# This workflow invokes other workflows with the nightly Dafny build +name: Dafny Nightly + +on: + schedule: + # Nightly build against Dafny's nightly prereleases, + # for early warning of verification issues or regressions. + # Timing chosen to be adequately after Dafny's own nightly build, + # but this might need to be tweaked: + # https://github.com/dafny-lang/dafny/blob/master/.github/workflows/deep-tests.yml#L16 + - cron: "30 16 * * *" + +jobs: + dafny-nightly-format: + # Don't run the cron builds on forks + if: github.event_name != 'schedule' || github.repository_owner == 'aws' + uses: ./.github/workflows/library_format.yml + with: + dafny: "nightly-latest" + regenerate-code: true + 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 + 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 + 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 + 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 + 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 + + cut-issue-on-failure: + runs-on: ubuntu-latest + permissions: + id-token: write + contents: read + needs: + [ + dafny-nightly-format, + dafny-nightly-verification, + dafny-nightly-java, + dafny-nightly-net, + ] + if: ${{ always() && contains(needs.*.result, 'failure') }} + steps: + # We need access to the role that is able to get CI Bot Creds + - name: Configure AWS Credentials for Release + uses: aws-actions/configure-aws-credentials@v2 + with: + aws-region: us-west-2 + role-to-assume: arn:aws:iam::587316601012:role/GitHub-CI-CI-Bot-Credential-Access-Role-us-west-2 + role-session-name: Dafny_Issue_Blocker + + # Use AWS Secrets Manger GHA to retrieve CI Bot Creds + - name: Get CI Bot Creds Secret + uses: aws-actions/aws-secretsmanager-get-secrets@v2 + with: + secret-ids: Github/aws-crypto-tools-ci-bot + parse-json-secrets: true + + - name: Create release blocker on dafny-lang/dafny + env: + GH_TOKEN: ${{ env.GITHUB_AWS_CRYPTO_TOOLS_CI_BOT_ESDK_RELEASE_TOKEN }} + run: | + gh issue create \ + --repo "dafny-lang/dafny" \ + --title "[PRERELEASE REGRESSION] Dafny prerelease regression from ${{ github.repository }}" \ + --body "Failure in ${{ github.workflow_ref }}. \ + See ${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}" \ No newline at end of file diff --git a/.github/workflows/pull.yml b/.github/workflows/pull.yml new file mode 100644 index 000000000..6f65ae33c --- /dev/null +++ b/.github/workflows/pull.yml @@ -0,0 +1,54 @@ +# This workflow runs for every pull request +name: PR CI + +on: + pull_request: + +jobs: + getVersion: + uses: ./.github/workflows/dafny_version.yml + pr-ci-format: + needs: getVersion + uses: ./.github/workflows/library_format.yml + with: + dafny: ${{needs.getVersion.outputs.version}} + pr-ci-codegen: + needs: getVersion + uses: ./.github/workflows/ci_codegen.yml + with: + dafny: ${{needs.getVersion.outputs.version}} + pr-ci-verification: + needs: getVersion + uses: ./.github/workflows/library_dafny_verification.yml + with: + dafny: ${{needs.getVersion.outputs.version}} + pr-ci-java: + needs: getVersion + uses: ./.github/workflows/ci_test_java.yml + with: + dafny: ${{needs.getVersion.outputs.version}} + pr-ci-java-test-vectors: + needs: getVersion + uses: ./.github/workflows/ci_test_vector_java.yml + with: + dafny: ${{needs.getVersion.outputs.version}} + pr-ci-java-examples: + needs: getVersion + uses: ./.github/workflows/ci_examples_java.yml + with: + dafny: ${{needs.getVersion.outputs.version}} + pr-ci-net: + needs: getVersion + uses: ./.github/workflows/ci_test_net.yml + with: + dafny: ${{needs.getVersion.outputs.version}} + pr-ci-net-test-vectors: + needs: getVersion + uses: ./.github/workflows/ci_test_vector_net.yml + with: + dafny: ${{needs.getVersion.outputs.version}} + pr-ci-net-examples: + needs: getVersion + uses: ./.github/workflows/ci_examples_net.yml + with: + dafny: ${{needs.getVersion.outputs.version}} diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml new file mode 100644 index 000000000..86f2875fd --- /dev/null +++ b/.github/workflows/push.yml @@ -0,0 +1,56 @@ +# This workflow runs for every push to main +name: Push CI + +on: + push: + branches: + - main + +jobs: + getVersion: + uses: ./.github/workflows/dafny_version.yml + push-ci-format: + needs: getVersion + uses: ./.github/workflows/library_format.yml + with: + dafny: ${{needs.getVersion.outputs.version}} + push-ci-codegen: + needs: getVersion + uses: ./.github/workflows/ci_codegen.yml + with: + dafny: ${{needs.getVersion.outputs.version}} + push-ci-verification: + needs: getVersion + uses: ./.github/workflows/library_dafny_verification.yml + with: + dafny: ${{needs.getVersion.outputs.version}} + pr-ci-java: + needs: getVersion + uses: ./.github/workflows/ci_test_java.yml + with: + dafny: ${{needs.getVersion.outputs.version}} + pr-ci-java-test-vectors: + needs: getVersion + uses: ./.github/workflows/ci_test_vector_java.yml + with: + dafny: ${{needs.getVersion.outputs.version}} + pr-ci-java-examples: + needs: getVersion + uses: ./.github/workflows/ci_examples_java.yml + with: + dafny: ${{needs.getVersion.outputs.version}} + pr-ci-net: + needs: getVersion + uses: ./.github/workflows/ci_test_net.yml + with: + dafny: ${{needs.getVersion.outputs.version}} + pr-ci-net-test-vectors: + needs: getVersion + uses: ./.github/workflows/ci_test_vector_net.yml + with: + dafny: ${{needs.getVersion.outputs.version}} + pr-ci-net-examples: + needs: getVersion + uses: ./.github/workflows/ci_examples_net.yml + with: + dafny: ${{needs.getVersion.outputs.version}} diff --git a/project.properties b/project.properties index e35812981..aef7c7f86 100644 --- a/project.properties +++ b/project.properties @@ -1,5 +1,6 @@ projectJavaVersion=3.5.0-SNAPSHOT mplDependencyJavaVersion=1.4.0 dafnyVersion=4.2.0 +dafnyVerifyVersion=4.7.0 dafnyRuntimeJavaVersion=4.2.0 smithyDafnyJavaConversionVersion=0.1