Run only the CI a pull request can affect

[jserv]

Every pull request paid for every workflow whatever it touched: seventeen macOS runners proving seventeen targets, three more analyzing a build, one building and testing, for a branch that edited a test script. The proofs are the bulk of that, and a target whose inputs a branch does not touch already has the verdict the base established.

scripts/proof-scope.py decides which proof targets a set of changed files can reach. It takes each proved source's include closure from the compiler's own -MM, preprocessed with that target's VERIFY_CPP_DEFS and unioned with its VERIFY_SCAN list, so the scan sees what the prover sees. Inputs no closure can see widen the scope to everything: the makefiles, the checkers the recipes run, the Frama-C stub headers, the workflow itself. So does every "cannot tell" answer, whether an unresolvable base ref or a compiler scan that cannot be trusted. Narrowing on a guess turns a speed-up into a correctness problem; proving something twice does not.

verify.yml builds its matrix from that answer on a pull request, so an untouched target gets no runner rather than a runner that skips its work. An empty scope is a verdict rather than a failure, and only the mutation gate decides what counts as a pass; the verify job mirrors it, so the rule lives in one place instead of two shell blocks that have to be edited together. A push to main and a merge queue run prove everything, so the guarantee on the branch a pull request merges into is never the narrowed one.

build.yml and static-analysis.yml take the cheaper mechanism their inputs allow, a paths-ignore list of what cannot reach them, on pull_request only so there is one list per file and nothing can drift. The analysis jobs analyze "make elfuse" and nothing else, which is why tests/ is inert for them. The failure directions differ from the proof scoping, and that is why one needs a self-test and the other does not: a stale entry there matches nothing and the workflow runs more, while a stale harness entry widens nothing and the proofs run less.

lint.yml loses its path filter entirely, which is what makes it the place the self-test can live. It had been ignoring markdown, and check-skill-refs.py validates nothing but the markdown under .claude, which the other two workflows treat as inert, so a documentation-only pull request ran no CI at all. That checker was also wired into no workflow until now, and it failed on its first run, naming two files the CI split had already removed.

---

Summary by cubic

Runs only the CI jobs a pull request can affect, widening to the full set on any uncertainty. Previously every PR ran all proofs, mutations, builds, and analysis; now proofs/mutations narrow to targets reachable from the diff, builds/analysis use path filters, and lint always runs to cover self-tests and docs checks.

• Proofs and mutations

  • Adds scripts/proof-scope.py to derive per-target reach from each source’s compiler include closure with VERIFY_<T>_CPP_DEFS unioned with VERIFY_<T>_SCAN; any “cannot tell” widens to all. Separates “scheduling-only” files and self-tests to forbid budgets or make in scheduling workflows.
  • verify.yml reads targets from mk/verify.mk, narrows matrices on PRs, and proves/mutates the full set on push and merge_group. Introduces verify-proofs to backfill anything mutation legs don’t prove; verify-mutants-gate stays the required aggregate and scripts/check-proof-targets.py asserts the matrix is derived and that macOS jobs are reachable from it.
  • Adds composite action ./.github/actions/framac for shared setup and moves to Frama-C 33.0. scripts/check-mutants.py delegates changed-only selection to proof-scope.py; scripts/verify-mk.py exposes targets/SCAN/CPP_DEFS, discovers proof workflows, and rejects multi-source VERIFY_<T>_SRC. scripts/check-char-signedness.py reads the shared table. mk/verify.mk corrects data-model notes (plain char is signed on arm64 macOS) and records why the macos_arm machdep cannot be used.

• CI and repo

  • build.yml and static-analysis.yml use paths-ignore on pull_request only (tests are inert for analysis). lint.yml drops its path filter, runs package-free checks first with if: !cancelled(), runs proof-scope.py --self-test, and wires scripts/check-skill-refs.py so docs-only PRs still run CI.
  • .ci/check-security.sh now flags “agent scratch markers”; removes one from src/syscall/asyncio.c. Updates SKILL.md to reference mk/verify.mk.
  • Required action: Install Frama-C 33.0. To reproduce CI scoping locally: make verify-mutants MUTANT_SINCE=<base>.

^{Written for commit 8993631. Summary will update on new commits.}