manual-verify.yml

name: Verification

# Run this workflow when manually triggered or when a PR with
# 'verification' label is created/updated
on:
  workflow_dispatch:
  pull_request:
    types: [opened, synchronize, reopened, labeled, unlabeled]

env:
  CARGO_TERM_COLOR: always

jobs:
  check:
    name: Verification Check
    runs-on: ubuntu-latest
    if: github.event_name == 'workflow_dispatch' || contains(github.event.pull_request.labels.*.name, 'verification')
    steps:
      - name: Checkout
        uses: actions/checkout@v3
        with:
          submodules: recursive

      - name: Install verus toolchains
        run: ./scripts/vinstall.sh --prebuilt-verusfmt

      - name: Format spec/proof code
        run: |
          verusfmt --check `find ./ -name *.verus.rs` --verus-only

      # cargo-v doesn't propagate the `cargo build` exit code, so we need
      # to check stderr for errors.
      # When https://github.com/microsoft/verismo/issues/23 will be fixed
      # we can remove it.
      - name: Verify svsm with verus
        run: |
          cargo verify 2>&1 | tee verify.log
          ! grep -q 'cargo build failed' verify.log
        working-directory: kernel

      - name: Verify extra proof libs with verus
        run: |
          cargo verify 2>&1 | tee verify.log
          ! grep -q 'cargo build failed' verify.log
        working-directory: verification/verify_proof