formal-verification.yml

# formal-verification — Kani proof enforcement for the `pr_gate = true` suites in
# ci/formal-verification.toml (bead sq-63ups).
#
# WHEN: nightly (01:53 UTC) and on manual dispatch. It does not run on pull requests;
# the one required PR check is ci-fast (docs/branch-protection.md). To re-check proofs
# on a branch that touches a verified path: `gh workflow run formal-verification.yml
# --ref <branch>`.
#
# TWO JOBS (sq-6vshe.20):
#   * fv-select — scripts/fv_select.py emits the suite matrix. Outside a
#     pull_request/merge_group event there is no diff pair, so it fails closed to
#     EVERY `pr_gate = true` suite. Then fv-manifest (scripts/check-fv-manifest.py), the
#     completeness + drift gate: REDs when a `#[cfg(kani)]` module is uncovered by the
#     manifest, when the source `#[kani::proof]` inventory and the manifest harness lists
#     disagree, or when kani.yml's matrix drifts from the `nightly = true` suites.
#   * kani — the selected suites' bounded proofs, with the same per-harness timeout +
#     step-summary machinery as the nightly kani.yml lane; a counterexample OR a
#     per-harness timeout is red.
#
# WHICH SUITES RUN: `pr_gate = true` suites only. The two mmap-validator totality
# suites are `pr_gate = false` (owner sq-og8u8): their harnesses exceed the 20m
# per-harness CBMC budget on this runner class and have never completed in CI. They
# stay on the nightly kani.yml lane (honest red there)
# and flip to pr_gate = true when sq-og8u8 bounds them. This is recorded in the
# manifest itself (`pr_gate_blocked_by`), enforced by the D4 manifest rule.
#
# Third-party actions are pinned by full commit SHA (supply-chain hardening); the
# trailing `# vX.Y.Z` comment is what Dependabot follows to bump the pin. Toolchain
# pin + install flow match kani.yml so a bump moves them together.
name: formal-verification

on:
  workflow_dispatch:
  schedule:
    - cron: "53 1 * * *"

permissions:
  contents: read

concurrency:
  group: formal-verification-${{ github.ref }}
  cancel-in-progress: true

env:
  CARGO_TERM_COLOR: always
  RUST_BACKTRACE: 1
  # Same per-harness wall-clock ceiling as the nightly kani.yml lane: a runaway proof
  # is cut with a clean red TIMEOUT record instead of exhausting the runner.
  KANI_HARNESS_TIMEOUT: "20m"
  # sq-ko0jt — SUITE-LEVEL budget; see kani.yml's identical block for the full
  # rationale. The biggest pr_gate suite (compare ORDER laws) has 26 harnesses, so its
  # worst case is 26 × 20m = 520m against a `timeout-minutes: 120` backstop. A backstop
  # hit CANCELS the job with no attribution at all. With the budget the
  # loop always emits a per-harness table naming exactly what ran, timed out, was cut, or
  # never started. Sized as the 120m backstop − the same ~15m setup allowance − reserve;
  # the relation is pinned by rule D5 in scripts/check-fv-manifest.py.
  KANI_STEP_BUDGET: "100m"

jobs:
  # The selector + the manifest gate (two former sub-minute jobs on one runner). The
  # selector step-group runs FIRST so the `any`/`suites` outputs are emitted before the
  # manifest gate can fail.
  fv-select:
    name: fv-select (change-based test selection) + fv-manifest (proof inventory)
    runs-on: ubuntu-latest
    permissions:
      contents: read
    outputs:
      any: ${{ steps.sel.outputs.any }}
      suites: ${{ steps.sel.outputs.suites }}
    steps:
      - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
        with:
          persist-credentials: false

      # ---- former job: fv-select (change-based test selection) ----
      # The selector's own fixtures run first so a broken selector cannot silently
      # mis-select.
      - name: Self-test the FV selector (hermetic fixtures)
        run: python3 scripts/fv_select.py --self-test
      - name: Select proof suites for this diff (scripts/fv_select.py)
        id: sel
        env:
          EVENT: ${{ github.event_name }}
        run: |
          set -euo pipefail
          # schedule/workflow_dispatch carry no diff pair => every pr_gate suite.
          python3 scripts/fv_select.py --event "$EVENT"

      # ---- former job: fv-manifest (proof inventory completeness + drift) ----
      # Seconds-cheap (a comment-aware source scan + two
      # config parses — no cargo, no build).
      - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 # v7.0.0
        with:
          python-version: "3.12"
      - name: Install PyYAML (hash-pinned)
        # Needed only to parse kani.yml's matrix. HASH-pinned (Scorecard
        # PinnedDependenciesID) against the same requirements file the docs-quality
        # YAML jobs use — one pin to bump.
        run: pip install --require-hashes -r .github/requirements/docs-quality.txt
      - name: Self-test the drift gate (all drift classes must red)
        run: python3 scripts/check-fv-manifest.py --self-test
      - name: Manifest / source-inventory / kani.yml agreement — GATING
        run: python3 scripts/check-fv-manifest.py

  # The change-coupled bounded proofs. Mirrors the nightly kani.yml job mechanics
  # (per-harness `--harness` invocation under a wall-clock timeout, solver reap,
  # step-summary table) — see kani.yml's RUNNER/STRUCTURE header for the rationale.
  # Skipped when fv-select selected nothing.
  kani:
    name: kani ${{ matrix.suite.name }} (change-coupled proofs)
    needs: fv-select
    if: needs.fv-select.outputs.any == 'true'
    runs-on: ubuntu-latest
    # Cold Kani install + per-harness codegen + the slowest measured suite (the
    # vectorized reducers: slowest harness ~10 min on the work box, six harnesses)
    # need generous headroom; a hung harness is cut by KANI_HARNESS_TIMEOUT long
    # before this backstop fires.
    timeout-minutes: 120
    strategy:
      # One suite's timeout must not cancel another suite's verdict.
      fail-fast: false
      matrix:
        suite: ${{ fromJSON(needs.fv-select.outputs.suites) }}
    # PINNED-TOOLCHAIN ESCAPE — REQUIRED here, not belt-and-braces, and this lane
    # GATES the merge. The repo root carries a `rust-toolchain.toml` pinning STABLE, and
    # rustup resolves that file (precedence 4) ABOVE the `rustup default <toolchain>` that
    # `dtolnay/rust-toolchain` performs (precedence 5). Every cargo call in this job
    # (`cargo install --locked kani-verifier`, `cargo kani setup`, `cargo kani --harness`)
    # is a plain invocation with no `+<toolchain>`, so without this env var they would all
    # silently move off the declared nightly onto pinned stable. `RUSTUP_TOOLCHAIN` is
    # precedence 2 and beats the file, preserving exactly the toolchain this lane resolved
    # to before the pin existed. Keep in sync with the `toolchain:` input below and with
    # kani.yml's identical escape.
    env:
      RUSTUP_TOOLCHAIN: nightly-2026-06-11
    steps:
      - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
        with:
          persist-credentials: false
      # Same pinned nightly as kani.yml / miri.yml / asan.yml so a toolchain bump
      # moves every formal lane together.
      - name: Install Rust (nightly, pinned)
        uses: dtolnay/rust-toolchain@29eef336d9b2848a0b548edc03f92a220660cdb8 # nightly via toolchain input
        with:
          toolchain: nightly-2026-06-11
      - name: Cache cargo + target
        uses: Swatinem/rust-cache@e18b497796c12c097a38f9edb9d0641fb99eee32 # v2
        with:
          # Distinct from kani.yml's `kani-<crate>` keys so a dispatch on a branch never
          # poisons that lane's warm cache.
          key: kani-pr-${{ matrix.suite.crate }}
          # sq-3sbrr save-if discipline: SAVE only from main; a branch-scoped save is
          # unreachable from main and only churns the shared 10 GB Actions-cache budget.
          save-if: ${{ github.ref == 'refs/heads/main' }}
      - name: Install Kani
        run: |
          cargo install --locked kani-verifier
          cargo kani setup
      # Identical loop to kani.yml (see that header for why per-harness + timeout +
      # summary): every harness's PASS / FAIL / TIMEOUT is recorded before the job
      # reds, so one cut proof cannot hide another's counterexample.
      - name: Kani bounded proofs (per-harness, timeout, summary)
        env:
          SUITE_NAME: ${{ matrix.suite.name }}
          SUITE_CRATE: ${{ matrix.suite.crate }}
          SUITE_FEATURES: ${{ matrix.suite.features }}
          SUITE_HARNESSES: ${{ matrix.suite.harnesses }}
        run: |
          set -u
          summary="${GITHUB_STEP_SUMMARY:-/dev/stdout}"
          tmo="${KANI_HARNESS_TIMEOUT:-20m}"
          budget="${KANI_STEP_BUDGET:-100m}"
          # `timeout(1)` duration syntax -> seconds (h/m/s suffix; bare number = seconds).
          to_seconds() {
            case "$1" in
              *h) echo $(( ${1%h} * 3600 )) ;;
              *m) echo $(( ${1%m} * 60 )) ;;
              *s) echo "${1%s}" ;;
              *)  echo "$1" ;;
            esac
          }
          tmo_s=$(to_seconds "$tmo")
          budget_s=$(to_seconds "$budget")
          step_start=$(date +%s)
          {
            echo "### Kani proof results — ${SUITE_NAME}"
            echo ""
            echo "This suite's bounded proofs (ci/formal-verification.toml) are re-checked here."
            echo "Each harness runs as its"
            echo "own \`cargo kani --harness\` invocation under a \`${tmo}\` wall-clock ceiling."
            echo ""
            echo "The suite as a whole is bounded by a \`${budget}\` step budget, so this table is"
            echo "always produced — a slow suite reds the run with a named harness rather than"
            echo "being CANCELLED at the job backstop and telling you nothing."
            echo ""
            echo "| Harness | Result | Wall time |"
            echo "| --- | --- | --- |"
          } >> "$summary"

          had_fail=0
          had_timeout=0
          had_unrun=0
          for h in $SUITE_HARNESSES; do
            # STEP-BUDGET GUARD — see kani.yml. Never start a harness we cannot record a verdict
            # for; a job cancellation would erase this whole table on a GATING check.
            left=$(( budget_s - ($(date +%s) - step_start) ))
            if [ "$left" -le 60 ]; then
              had_unrun=1
              echo "::error title=Kani harness NOT RUN::${SUITE_CRATE}::${h} never ran — the ${budget} step budget was exhausted by earlier harnesses in this suite, so the proved source is UNVERIFIED in this run."
              echo "| \`${h}\` | ⏭️ NOT RUN (\`${budget}\` step budget exhausted) | — |" >> "$summary"
              continue
            fi
            this_tmo=$tmo_s
            if [ "$left" -lt "$this_tmo" ]; then
              this_tmo=$left
            fi
            log="kani-${SUITE_CRATE}-${h}.log"
            start=$(date +%s)
            # shellcheck disable=SC2086  # SUITE_FEATURES is an intentional word-split arg list.
            # `&& ec=0 || ec=$?` — capture exit code without triggering `set -e` (bash -e {0}).
            timeout -k 30s "${this_tmo}s" cargo kani -p "$SUITE_CRATE" $SUITE_FEATURES --harness "$h" \
              > "$log" 2>&1 && ec=0 || ec=$?
            # Anti-OOM invariant: reap any orphaned solver before the next harness starts.
            pkill -9 -x cbmc 2>/dev/null || true
            end=$(date +%s)
            dur=$((end - start))
            wall=$(printf '%dm%02ds' $((dur / 60)) $((dur % 60)))

            case "$ec" in
              0)
                res="✅ PASS"
                ;;
              124 | 137)
                # CUT (clamped by the remaining step budget) vs TIMEOUT (full ${tmo} spent) are
                # different findings and get different messages — on a gating leg the author
                # needs to know whether THEIR change blew the proof budget or the suite simply
                # no longer fits the runner. Both are red here (this leg has no debt tier).
                if [ "$this_tmo" -lt "$tmo_s" ]; then
                  res="⏱️ CUT (only ${this_tmo}s of the \`${budget}\` step budget left)"
                  had_unrun=1
                  echo "::error title=Kani harness cut by the step budget::${SUITE_CRATE}::${h} was cut after ${this_tmo}s — earlier harnesses consumed the ${budget} step budget, so this proof has NO verdict in this run."
                else
                  res="⏱️ TIMEOUT (>${tmo})"
                  had_timeout=1
                  echo "::error title=Kani timeout::${SUITE_CRATE}::${h} exceeded ${tmo} — the proof no longer fits its budget (see step summary)."
                fi
                ;;
              *)
                res="❌ FAIL (exit ${ec})"
                had_fail=1
                echo "::error title=Kani proof failed::${SUITE_CRATE}::${h} failed (exit ${ec}) — a reachable panic/OOB/UB counterexample or a build error (see step summary)."
                ;;
            esac
            echo "| \`${h}\` | ${res} | ${wall} |" >> "$summary"

            if [ "$ec" -ne 0 ]; then
              {
                echo ""
                echo "<details><summary>Log tail — <code>${h}</code> (${res})</summary>"
                echo ""
                echo '```'
                tail -n 40 "$log" 2>/dev/null || true
                echo '```'
                echo ""
                echo "</details>"
              } >> "$summary"
            fi
          done

          {
            echo ""
            if [ "$had_fail" -eq 1 ]; then
              echo "**Overall: ❌ FAIL** — a bounded proof is broken; fix the code or re-derive the harness honestly (never weaken the property to pass)."
            elif [ "$had_unrun" -eq 1 ]; then
              echo "**Overall: ❌ NO VERDICT for part of this suite** — the \`${budget}\` step budget ran out, so the harnesses marked **NOT RUN** / **CUT** above did not re-prove the source. Every harness that DID run is recorded above, so if none of them failed this is a suite-cost problem rather than a code defect — re-bound the slow harnesses or split the suite."
            elif [ "$had_timeout" -eq 1 ]; then
              echo "**Overall: ⏱️ TIMEOUT** — every harness that finished passed, but one or more proofs went past the \`${tmo}\` budget; re-bound the harness or simplify the code."
            else
              echo "**Overall: ✅ PASS** — every re-obligated proof verified within budget."
            fi
          } >> "$summary"

          if [ "$had_fail" -eq 1 ] || [ "$had_unrun" -eq 1 ] || [ "$had_timeout" -eq 1 ]; then
            exit 1
          fi