Run the Kani proofs on a pull request only when inputs change

.github/workflows/ci.yml

@@ -8,6 +8,11 @@ on:
   # publish, so without this trigger no generation would ever be written.
   push:
     branches: [main]
+  # Nightly at 04:41 UTC, clear of the 03:05 mutation-testing run, so every
+  # Kani harness is verified even on a day with no push to `main`. Only
+  # `kani-smoke` runs on it; see docs/adr-039-change-scoped-kani-gate.md.
+  schedule:
+    - cron: '41 4 * * *'
   workflow_dispatch:
 
 # Start every job from an empty token and let each one opt in. Both jobs
@@ -54,6 +59,8 @@ jobs:
     runs-on: >-
       ${{ github.event.pull_request.head.repo.fork
       && 'ubuntu-latest' || 'ubicloud-standard-4-ubuntu-2404' }}
+    # The nightly schedule exists for the Kani proofs alone.
+    if: github.event_name != 'schedule'
     # Ninety minutes, not sixty. The coverage step below passes
     # `doctests: 'true'`, so the shared action runs `cargo llvm-cov nextest`
     # and then an uninstrumented `cargo test --doc`, each arming the 1,800 s
@@ -348,6 +355,8 @@ jobs:
     # inside the repository's 400-line limit. Version pins stay here, so the
     # documented `sed` extraction still finds exactly one of each.
     name: Windows
+    # The nightly schedule exists for the Kani proofs alone.
+    if: github.event_name != 'schedule'
     permissions:
       contents: read
     uses: ./.github/workflows/ci-windows.yml
@@ -360,7 +369,16 @@ jobs:
       python-baseline: '3.14'
 
   kani-smoke:
-    # Runs on every trigger, dispatch included. A dispatch cannot publish a
+    # A required check, so it runs and reports on every trigger; it is never
+    # skipped by a `paths` filter or a job-level `if:`, since a required check
+    # that never reports blocks the pull request. An early step decides
+    # whether the proofs can differ from `main`'s: on a pull request whose
+    # changed paths match no entry in either list of
+    # tools/kani/proof-scope.toml (an edit to the TOML file itself is a
+    # change to `tools/kani/`, which is an entry) every later step skips and
+    # the job ends green, saying why in its summary. A push to `main`, the
+    # nightly schedule and a dispatch always run every harness. See
+    # docs/adr-039-change-scoped-kani-gate.md. A dispatch cannot publish a
     # generation, since the save gates on a push to `main`, so all it can do
     # here is measure a warm restore, which is the one the exit gate needs.
     # A pull request from a fork cannot obtain a Ubicloud runner, so the
@@ -444,15 +462,31 @@ jobs:
       - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1  # v7.0.1
         with:
           persist-credentials: false
+          # The pull-request merge commit and its first parent, the base tip,
+          # whose diff is the change set the scope decision reads.
+          fetch-depth: 2
+      - name: Setup uv
+        uses: astral-sh/setup-uv@bec219d24cd3e171d82865faccec33120bb574f4
+        with:
+          python-version: ${{ env.PYTHON_BASELINE }}
+          # Nothing here is worth a cache entry; the job owns only the Kani key.
+          enable-cache: 'false'
+      - name: Decide Kani proof scope
+        id: scope
+        env:
+          INPUT_EVENT_NAME: ${{ github.event_name }}
+        run: uv run --script scripts/kani_proof_scope.py
       - name: Restore Kani payloads
         id: kani_cache
+        if: steps.scope.outputs.run-proofs == 'true'
         # Restored before every installer, so a warm run finds the front-end,
         # bundle and Kani toolchain in place.
         uses: ./.github/actions/kani-cache
         with:
           mode: restore
           runner-image: ${{ env.NETSUKE_RUNNER_IMAGE }}
       - name: Setup Rust
+        if: steps.scope.outputs.run-proofs == 'true'
         uses: leynos/shared-actions/.github/actions/setup-rust@4fb8eb7ad52454678a0662865d81d3cd17aa6e0e
         with:
           # Resolved from the job's own `env`, which declares the pinned
@@ -470,6 +504,7 @@ jobs:
           install-binstall: 'false'
           use-sccache: 'false'
       - name: Install prebuilt Kani
+        if: steps.scope.outputs.run-proofs == 'true'
         # Two payloads from pinned checksummed archives under
         # version-qualified directories, so a bump cannot reuse a stale one.
         run: |
@@ -511,8 +546,10 @@ jobs:
             cargo kani setup --use-local-bundle "${bundle}"
           fi
       - name: Kani version check
+        if: steps.scope.outputs.run-proofs == 'true'
         run: cargo kani --version | grep --fixed-strings "0.67.0"
       - name: Start the user manager
+        if: steps.scope.outputs.run-proofs == 'true'
         # A hosted runner's job does not run inside a login session, so the
         # per-user systemd manager that `systemd-run --user --scope` needs is
         # absent until lingering is on; without it every scenario in the next
@@ -528,6 +565,7 @@ jobs:
             sleep 1
           done
       - name: Install the build standard
+        if: steps.scope.outputs.run-proofs == 'true'
         # Not because the wrapper's suite needs the pinned linker: its recipe is
         # a single `cargo nextest run` whose `RUSTFLAGS` displace the
         # configuration's `-Zthreads`/`mold` tables, and the target declares no
@@ -537,6 +575,7 @@ jobs:
         # tests/workflow_contracts/nextest_lane_mold_test.py is that contract.
         run: make install-build-tools
       - name: Install cargo-nextest
+        if: steps.scope.outputs.run-proofs == 'true'
         # The wrapper's own suite is an ordinary test binary run through the
         # standard runner, and this job installs none of the test tooling the
         # `build-test` lane does. Pinned to the same action revision and the
@@ -545,6 +584,7 @@ jobs:
         with:
           tool: nextest@${{ env.NEXTEST_VERSION }}
       - name: Verify the scope wrapper end to end
+        if: steps.scope.outputs.run-proofs == 'true'
         # Runs before the harness suite so a broken wrapper is reported as
         # itself rather than as a Kani failure. Not a `make test` invocation:
         # the wrapper's own suite is one test binary, and `kani-smoke` is
@@ -554,8 +594,10 @@ jobs:
         # that skipped every scenario would otherwise read as green.
         run: make test-kani-scope-wrapper
       - name: Run Kani harnesses
+        if: steps.scope.outputs.run-proofs == 'true'
         run: make kani-ir
       - name: Mutation patch compile gate
+        if: steps.scope.outputs.run-proofs == 'true'
         # Applies each patch under docs/verification/mutations/ and compiles the
         # patched tree under `-D warnings`. `#[ignore]`-gated and run from its
         # own target: one Kani codegen per patch is too costly for the default
@@ -584,6 +626,7 @@ jobs:
         # it as a second workspace-suite execution.
         run: make test-kani-mutations
       - name: Save Kani payloads
+        if: steps.scope.outputs.run-proofs == 'true'
         # This job owns the Kani key and nothing else; the action restricts
         # the save to a push on `main`.
         uses: ./.github/actions/kani-cache

Makefile

@@ -241,7 +241,7 @@ test-kani-mutations: check-build-tools ## Compile each mutation patch's patched
 	$(GATE_RUSTFLAGS) $(CARGO) nextest run --test kani_mutation_evidence_tests --all-features --run-ignored ignored-only $(NEXTEST_BUILD_JOBS) $(NEXTEST_TEST_JOBS)
 
 test-workflow-contracts: ## Validate GitHub Actions workflow contracts
-	$(UV_ENV) $(UV) run --no-project --python $(PYTHON_BASELINE) --with 'pytest>=8' --with 'pyyaml>=6' --with 'hypothesis>=6' --with 'cmd-mox==0.2.0' pytest tests/workflow_contracts -q --doctest-modules
+	$(UV_ENV) $(UV) run --no-project --python $(PYTHON_BASELINE) --with 'pytest>=8' --with 'pyyaml>=6' --with 'hypothesis>=6' --with 'cmd-mox==0.2.0' --with 'cuprum==0.1.0' --with 'cyclopts==4.25.3' pytest tests/workflow_contracts -q --doctest-modules
 
 test-windows-msi-release-rank: ## Validate Windows MSI release-rank parsing
 	@PYTHONPATH=scripts $(UV_ENV) $(UV) run --no-project --python $(PYTHON_BASELINE) \
@@ -374,6 +374,7 @@ typecheck-python: ## Typecheck the Python sources with ty
 	$(UV_ENV) $(UV) tool run --python $(PYTHON_BASELINE) \
 		--from ty==$(TY_VERSION) --with pytest==9.0.2 --with pytest-cov==7.0.0 \
 		--with 'pyyaml>=6' --with 'hypothesis>=6' --with 'cmd-mox==0.2.0' \
+		--with 'cuprum==0.1.0' --with 'cyclopts==4.25.3' \
 		ty check --python-version $(PYTHON_BASELINE) \
 		--extra-search-path scripts --extra-search-path .github/scripts \
 		$(PYTHON_SOURCES)

docs/adr-039-change-scoped-kani-gate.md

@@ -0,0 +1,169 @@
+# Architecture decision record (ADR) 039: Run the Kani proofs on a pull request only when their inputs change
+
+## Status
+
+Accepted.
+
+## Date
+
+2026-09-23
+
+## Context and problem statement
+
+The `kani-smoke` job in `.github/workflows/ci.yml` runs `make kani-ir`, the 15
+bounded Kani harnesses in `src/ir/from_manifest_verification.rs`,
+`src/ir/cycle_verification.rs` and `src/ir/cmd_interpolate/verification.rs` (see
+[ADR-004](adr-004-bound-kani-ir-harnesses-to-small-n.md)). Until this decision
+it ran them on every pull request. From 1 to 21 September 2026 that was 534
+runs and 3,696 runner minutes, about seven minutes a run, and most of those
+pull requests changed nothing a proof reads: documentation, workflows for other
+jobs, the command-line interface, the runner.
+
+`kani-smoke` is a required check on the repository ruleset. GitHub treats a
+required check that never reports as pending, so a pull request that skips the
+job never becomes mergeable. The usual ways of skipping work, a `paths` filter
+on the trigger or an `if:` on the job, therefore cannot be used.
+
+The proofs must stay trustworthy. A pull request that could change a proof's
+outcome must run it before it merges, and anything the pull-request decision
+misses must still be verified soon after.
+
+## Decision drivers
+
+- `kani-smoke` must report on every pull request, since it is required.
+- A pull request touching any proof input must run every harness.
+- The set of proof inputs must be derived from the source, not written down
+  once and trusted, and adding a harness anywhere must fail a contract until
+  the set covers it.
+- `main` must be verified in full on every push and at least nightly.
+- The mechanism must be reusable by other repositories adopting Kani.
+
+## Options considered
+
+- **Keep running every harness on every pull request.** Correct, and costs
+  about seven minutes on every run of every pull request.
+- **A `paths` filter on the trigger, or a job-level `if:`.** Refused: the
+  required check would never report on a skipped pull request.
+- **A path-filter action inside the job.** Works, but adds a third-party
+  action to a required job and moves the path set into workflow YAML where no
+  contract can derive it from the source.
+- **An in-repository decision step reading a derived, contract-held scope.**
+  Chosen.
+
+## Decision
+
+`kani-smoke` always runs and always reports. Its steps are, in order: the
+checkout (with `fetch-depth: 2`), `astral-sh/setup-uv`, and **Decide Kani proof
+scope**, which runs `uv run --script scripts/kani_proof_scope.py` with
+`INPUT_EVENT_NAME` set from `github.event_name`. The script writes
+`run-proofs=true` or `run-proofs=false` to the step outputs, and every later
+step carries `if: steps.scope.outputs.run-proofs == 'true'`. That includes the
+job's two other checks, the scope wrapper's end-to-end suite and the mutation
+patch compile gate, together with the build standard and runner they install.
+The gate compiles through the Kani front-end that only a proof run installs,
+and both checks read inputs the scope names, so they run and skip with the
+proofs. When the proofs are skipped the job ends green, and the script says why
+in the job summary and as a `::notice::` annotation.
+
+**What runs in full, and when.**
+
+- Every push to `main` runs every harness, whatever it changed.
+- A nightly `schedule` trigger at 04:41 UTC runs every harness, clear of the
+  03:05 UTC mutation-testing run. `build-test` and `windows` carry
+  `if: github.event_name != 'schedule'`, so the nightly run is the Kani job
+  alone. The release dry-run smoke contract admits that one condition on the
+  Windows gate, since it is true on every pull request.
+- A manual `workflow_dispatch` runs every harness.
+- On a pull request the change set is the diff between the merge commit
+  `actions/checkout` checks out and its first parent, the base branch tip, read
+  with `--no-renames` so that a file moved out of the scope counts under both
+  paths. When HEAD is not a two-parent merge, or git fails, the change set is
+  unreadable and every harness runs. The proofs run when any changed path falls
+  in the scope, and skip otherwise.
+- A scope file that is missing or malformed fails the step, rather than
+  deciding from it.
+
+**The scope.** `tools/kani/proof-scope.toml` holds two lists. An entry ending in
+`/` covers a directory; any other entry names one file.
+
+- `sources` is the module closure of the harnesses. The contract
+  `tests/workflow_contracts/kani_proof_scope_test.py` recomputes it from the
+  Rust source on every run, reading the library's module tree
+  (`tests/workflow_contracts/rust_module_graph.py`) and closing over it
+  (`tests/workflow_contracts/rust_module_closure.py`). It seeds from every
+  compiled file whose code names `kani` (a `#[kani::proof]` harness, a
+  `cfg(kani)` site or a `kani::` call) or declares a `#[global_allocator]`, and
+  follows:
+
+  - `crate::`, `super::`, `self::` and `$crate::` paths, and `{…}` use groups,
+    to the module named and every compiled module beneath it;
+  - bare `child::` paths to a module declared in the same file;
+  - `name!` invocations to every file defining `macro_rules! name`;
+  - `impl` items whose header names a type or trait the closure defines, since
+    coherence lets an impl live anywhere in the crate;
+  - `include_str!`, `include_bytes!` and `include!` to the file a literal names,
+    or to the directory of a `concat!`'s leading literal;
+  - and, at the end, each reached module's declaring ancestors, whose `mod`
+    attributes decide whether and how it compiles.
+
+  Every rule over-approximates. `#[cfg(test)]` modules and inline
+  `#[cfg(test)] mod … { … }` bodies are left out because `cargo kani` compiles
+  without `cfg(test)`; a contract refuses `--tests` in the Makefile's Kani
+  invocation and a `tests` key in `[package.metadata.kani.flags]`, which is the
+  change that would make that unsound. A `mod name;` nested in an inline module
+  body, a missing module file, and an include whose path is not a literal are
+  refused, so a layout the reader does not model fails the contract instead of
+  shrinking the scope.
+
+- `infrastructure` names what builds and runs the proofs, which no source
+  closure can find: `Cargo.toml`, `Cargo.lock`, `rust-toolchain.toml`,
+  `build.rs`, `.cargo/`, `tools/kani/`, `.github/actions/kani-cache/`, the
+  `Makefile`, `.github/workflows/ci.yml`, and the decision script itself. It
+  also names the inputs of the job's two other checks, which the same decision
+  gates: the scope wrapper's suite (`tests/kani_scope_wrapper_e2e_tests.rs`)
+  and the mutation compile gate (`tests/kani_mutation_evidence_tests.rs`, its
+  module directory, and the patches under `docs/verification/mutations/`).
+  Every file a patch edits must lie in `sources`, since the gate applies the
+  patch before compiling. The contract requires each of them.
+
+The contract fails when the closure reaches a path the scope does not cover,
+when any `#[kani::proof]` file anywhere in the repository is outside the scope,
+when a required infrastructure entry is dropped, and when a `sources` entry
+covers a compiled file the closure does not reach or covers nothing it reaches.
+The last two keep the scope from quietly widening to the whole crate, which
+would satisfy every sufficiency check and run the proofs on every pull request
+again. At adoption the closure is 44 files, listed as 18 `sources` entries:
+`src/ir/`, `src/ast/`, `src/ninja_gen/` and six of its sibling
+`src/ninja_gen_*.rs` modules, the localization modules and `locales/`,
+`src/hasher.rs`, `src/hex.rs`, `src/recipe_shell.rs`, `src/shell_word.rs` (which
+`recipe_shell` imports), and the crate root.
+
+## Consequences
+
+- A pull request that touches no proof input finishes `kani-smoke` in the time
+  it takes to check out, install uv and run the script, and reports success. Of
+  the 300 most recent merges to `main` before adoption, 129 (43%) touched no
+  path in the scope.
+- `Cargo.lock`, `Cargo.toml`, `ci.yml` and the `Makefile` are in the scope as
+  whole files, so a dependency bump or a CI change runs the proofs even when it
+  cannot affect them. That is the conservative side of the trade and the
+  largest source of full runs.
+- The pull-request decision covers what a proof verifies, not every way the
+  crate can fail to compile under Kani's bundled toolchain
+  (`nightly-2025-11-21` for Kani 0.67.0). A pull request outside the scope that
+  uses a language feature newer than that toolchain would still pass
+  `build-test` and skip the proofs, and the failure would appear on the push to
+  `main` that follows it. The push-to-`main` and nightly runs exist to bound
+  that window.
+- Adding a harness, or a `cfg(kani)` site, outside the current closure fails
+  the contract and prints the paths to add. Moving code so that a harness no
+  longer reaches a file fails it too, and prints the entry to remove.
+
+## Reuse in other repositories
+
+The mechanism is repository-independent apart from the scope file. A step by
+step adoption guide lives outside this repository, in the estate's
+`kani-change-scoped-gate.md` note; the parts to copy are
+`scripts/kani_proof_scope.py`, the two module readers and their tests, the
+scope contract with its `REQUIRED_INFRASTRUCTURE` list rewritten for the
+adopting repository, and the job shape above.

docs/contents.md

@@ -235,6 +235,9 @@ operator, user, and contributor references are easier to find.
   Runtime annotation introspection declared unsupported for the workflow
   contract tests, with the loader gate's stale `TYPE_CHECKING` claim corrected
   and a revisit gate that reopens on a real consumer.
+- [ADR-039](adr-039-change-scoped-kani-gate.md): Change-scoped Kani proofs,
+  running the required `kani-smoke` harnesses on a pull request only when a
+  derived proof input changes, and in full on `main` and nightly.
 - [ADR-040](adr-040-focused-child-rfcs-for-survey-rfcs.md): Splitting a survey
   RFC into focused child RFCs, each owning one or more capability groups, with
   the accepted set partitioned by a coverage map and guarded by a