diff --git a/.github/workflows/verify-std-check.yml b/.github/workflows/verify-std-check.yml new file mode 100644 index 000000000000..667be6b340c5 --- /dev/null +++ b/.github/workflows/verify-std-check.yml @@ -0,0 +1,86 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +# +# This workflow will try to build and run the `verify-rust-std` repository. +# +# This check should be optional, but it has been added to help provide +# visibility to when a PR may break the `verify-rust-std` repository. +# +# We expect toolchain updates to potentially break this workflow in cases where +# the version tracked in the `verify-rust-std` is not compatible with newer +# versions of the Rust toolchain. +# +# Changes unrelated to the toolchain should match the current status of main. + +name: Check Std Verification +on: + pull_request: + workflow_call: + +env: + RUST_BACKTRACE: 1 + +jobs: + verify-std: + runs-on: ${{ matrix.os }} + strategy: + matrix: + # Kani does not support windows. + os: [ ubuntu-22.04, macos-14 ] + steps: + - name: Checkout Library + uses: actions/checkout@v4 + with: + repository: model-checking/verify-rust-std + path: verify-rust-std + submodules: true + + - name: Checkout `Kani` + uses: actions/checkout@v4 + with: + path: kani + + - name: Setup Kani Dependencies + uses: ./kani/.github/actions/setup + with: + os: ${{ matrix.os }} + kani_dir: kani + + - name: Build Kani + working-directory: kani + run: | + cargo build-dev + echo "$(pwd)/scripts" >> $GITHUB_PATH + + - name: Run verification with HEAD + id: check-head + working-directory: verify-rust-std + continue-on-error: true + run: | + kani verify-std -Z unstable-options ./library --target-dir ${{ runner.temp }} -Z function-contracts \ + -Z mem-predicates -Z ptr-to-ref-cast-checks + + # If the head failed, check if it's a new failure. + - name: Checkout base + working-directory: kani + if: steps.check-head.outcome != 'success' && github.event_name == 'pull_request' + run: | + BASE_REF=${{ github.event.pull_request.base.sha }} + git checkout ${BASE_REF} + cargo build-dev + + - name: Run verification with BASE + id: check-base + if: steps.check-head.outcome != 'success' && github.event_name == 'pull_request' + working-directory: verify-rust-std + continue-on-error: true + run: | + kani verify-std -Z unstable-options ./library --target-dir ${{ runner.temp }} -Z function-contracts \ + -Z mem-predicates -Z ptr-to-ref-cast-checks + + - name: Compare PR results + if: steps.check-head.outcome != 'success' && steps.check-head.output != github.check-base.output + run: | + echo "New failure introduced by this change" + exit 1 + diff --git a/.github/workflows/verify-std-update.yml b/.github/workflows/verify-std-update.yml new file mode 100644 index 000000000000..518f80ecd1b8 --- /dev/null +++ b/.github/workflows/verify-std-update.yml @@ -0,0 +1,35 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +# +# This workflow will try to update the verify std branch. + +name: Update "features/verify-rust-std" +on: + schedule: + - cron: "30 3 * * *" # Run this every day at 03:30 UTC + workflow_dispatch: # Allow manual dispatching. + +env: + RUST_BACKTRACE: 1 + +jobs: + # First ensure the HEAD is compatible with the `verify-rust-std` repository. + verify-std: + name: Verify Std + permissions: { } + uses: ./.github/workflows/verify-std-check.yml + + # Push changes to the features branch. + update-branch: + needs: verify-std + permissions: + contents: write + runs-on: ubuntu-latest + steps: + - name: Checkout Kani + uses: actions/checkout@v4 + + - name: Update feature branch + run: | + git push origin HEAD:features/verify-rust-std +