diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index a88e2e87d..d0399cec2 100644 --- a/.github/workflows/ci.yml +++ b/.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,8 +462,23 @@ 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 @@ -453,6 +486,7 @@ jobs: 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 diff --git a/Makefile b/Makefile index e4452262a..4f5c16ebe 100644 --- a/Makefile +++ b/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) diff --git a/docs/adr-039-change-scoped-kani-gate.md b/docs/adr-039-change-scoped-kani-gate.md new file mode 100644 index 000000000..a7a012c4a --- /dev/null +++ b/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. diff --git a/docs/contents.md b/docs/contents.md index 0cd15077b..722a1d78c 100644 --- a/docs/contents.md +++ b/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 diff --git a/docs/developers-guide.md b/docs/developers-guide.md index 9c9dd03ed..e637fb2a7 100644 --- a/docs/developers-guide.md +++ b/docs/developers-guide.md @@ -1666,8 +1666,11 @@ The disjunct can only make the job run more often. `tests/workflow_contracts/release_dry_run_smoke_test.py` holds four things. The condition is compared whole, so a tagged release still runs the job. `release` -still needs it. The pull-request gate runs the same smoke unconditionally, with -the same invocation token for token. And the dry run's event types outside +still needs it. The pull-request gate runs the same smoke, with the same +invocation token for token. `ci.yml` calls the Windows gate on every event but +the nightly Kani schedule (ADR-039), so the contract admits exactly +`if: github.event_name != 'schedule'` on that call, which is true on every pull +request, and refuses any other condition. And the dry run's event types outside `ci.yml`'s set are exactly the ones the condition exempts. ## Release-admission observability @@ -3300,8 +3303,11 @@ links with it, but the suite does not only build: its tests drive `make` recipes gated on `check-build-tools`, which refuses to run without the pinned `mold` on `PATH`. The rule is general. Every Linux job that runs the nextest suite, whether through the coverage action, `cargo nextest run`, or a Make goal -whose recipe reaches it, runs `make install-build-tools` in an unguarded step -of its own before the suite. `tests/workflow_contracts/nextest_lane_rules.py` +whose recipe reaches it, runs `make install-build-tools` in a step of its own +before the suite. That step carries no `if:` unless every suite step in the job +carries the identical one, so the install runs whenever the suite does. +`kani-smoke` is the case this admits: its proof-scope decision gates every +later step alike (ADR-039). `tests/workflow_contracts/nextest_lane_rules.py` derives those jobs from the workflows and the Makefile rather than listing them, and `tests/workflow_contracts/nextest_lane_mold_test.py` proves each clause by mutation. @@ -3535,11 +3541,12 @@ them. during `cargo kani setup`, and drives `rustc` through `kani-compiler`. Reading the compiler invocations a `cargo kani` run produces shows `-Zthreads` never reaching `kani-compiler`, so the harnesses need no override - and none is added; CI's `kani-smoke` job runs `make kani-ir` on every pull - request, which is where that continues to be checked. Verus drives its own - toolchain the same way. If a proof tool ever does inherit a flag it cannot - take, the remedy is an override scoped to that one target with the reason - recorded, not a change to the shared configuration. + and none is added; CI's `kani-smoke` job runs `make kani-ir` on every push to + `main`, nightly, and on each pull request that changes a proof input, which + is where that continues to be checked. Verus drives its own toolchain the + same way. If a proof tool ever does inherit a flag it cannot take, the remedy + is an override scoped to that one target with the reason recorded, not a + change to the shared configuration. - **Dylint and Whitaker.** `make lint-whitaker` execs `cargo dylint`, which re-invokes Cargo under Whitaker's own pinned nightly with a driver as `RUSTC_WORKSPACE_WRAPPER`. That older Cargo reads this configuration without @@ -4146,15 +4153,72 @@ long-lived mutable control-plane state. See for the design rationale and re-entry criteria. Pull requests run a dedicated `kani-smoke` CI job alongside the ordinary -`build-test` job. The job installs the pinned, checksummed `cargo-kani` -front-end and Kani release bundle, checks the reported version, and then runs -the bounded harness suite through `make kani-ir` and the mutation compile gate -through `make test-kani-mutations`, both under a 30-minute job timeout; it does -not run `make verus`, coverage, CodeScene upload, or the normal build matrix. -Its cache entry owns the job-local Kani Cargo, support-file, and Rust toolchain -homes separately from ordinary Cargo build artefacts. The job runs on every -pull request, on a push to `main`, and on a manual dispatch, which is what lets -a dispatch measure a warm restore of those homes. +`build-test` job. When the proofs run, the job installs the pinned, checksummed +`cargo-kani` front-end and Kani release bundle, checks the reported version, +and then runs the bounded harness suite through `make kani-ir` and the mutation +compile gate through `make test-kani-mutations`, both under a 30-minute job +timeout; it does not run `make verus`, coverage, CodeScene upload, or the +normal build matrix. Its cache entry owns the job-local Kani Cargo, +support-file, and Rust toolchain homes separately from ordinary Cargo build +artefacts. The job runs on every pull request, on a push to `main`, on the +nightly schedule and on a manual dispatch, which is what lets a dispatch +measure a warm restore of those homes. + +### Change-scoped Kani proofs + +`kani-smoke` is a required check, so it runs and reports on every trigger, but +on a pull request it runs the harnesses only when the pull request changes a +proof input. [ADR-039](adr-039-change-scoped-kani-gate.md) records the +decision; this section is the working reference. + +- **The decision.** The job's third step, `Decide Kani proof scope`, runs + `uv run --script scripts/kani_proof_scope.py` and writes `run-proofs` to its + outputs. Every later step carries + `if: steps.scope.outputs.run-proofs == 'true'`. A push to `main`, the nightly + `schedule` (04:41 UTC) and a `workflow_dispatch` always run every harness. A + pull request runs them when its merge commit's diff against the base tip + touches the scope, or when that diff cannot be read. A skipped job is green + and says why in its summary. +- **The scope.** `tools/kani/proof-scope.toml` lists `sources`, the harnesses' + module closure, and `infrastructure`, what builds and runs them. Entries + ending in `/` cover a directory. +- **Never skip the job itself.** No `paths` filter on the workflow trigger and + no job-level `if:` on `kani-smoke`: a required check that never reports + blocks the pull request. `kani_smoke_scope_wiring_test.py` refuses both, and + requires the decision condition, exactly, on every step after the decision. +- **Keeping the scope right.** `kani_proof_scope_test.py` recomputes the + closure from the source and fails when the scope misses a reached path or a + `#[kani::proof]` file anywhere in the repository, when a `sources` entry + covers a compiled file no harness reaches, or when a required infrastructure + entry is dropped. Its failure message names the paths; copy them into the + scope rather than widening an entry. `rust_module_closure_test.py` drives + each closure rule over a synthetic crate. + `rust_module_closure_property_test.py` generates small flat crates and checks + the closure against graph reachability over the generating edge list, never a + second parse of the source: every required dependency is reached, nothing + test-only is, the answer is stable under declaration and line order, and + adding a reference or seed never shrinks it. Unsupported layouts must raise + `ModuleGraphError`. The generated crates omit `impl` headers, which + over-approximate by design and stay pinned by the synthetic crate. + `kani_proof_scope_property_test.py` does the same for scope-entry matching + (exact file, directory boundary) and the decision (order independence, an + unreadable diff runs the proofs). +- **Adding a harness.** Put it beside the module it verifies, under + `#[cfg(kani)] mod verification`, as the existing harnesses are. Run + `make test-workflow-contracts`; if the harness reaches code outside the + scope, the contract prints what to add. +- **Local check.** With a pull request's merge commit checked out, + `uv run --script scripts/kani_proof_scope.py --event-name pull_request` + prints the decision the job would make. +- **What the pull-request decision does not cover.** Kani compiles the whole + crate on its bundled toolchain, so a pull request outside the scope that uses + a language feature newer than that toolchain skips the proofs and breaks the + next push-to-`main` run instead. That run, and the nightly one, are the + backstop. + +The decision script's `cuprum` and `cyclopts` pins are repeated in the +`test-workflow-contracts` and `typecheck-python` recipes, and +`kani_proof_scope_decision_test.py` holds them equal. ## Test execution @@ -9592,7 +9656,9 @@ The contract also pins the condition each lane carries. A skipped step runs no `if: false` on the step or on its job would leave a lane that looks bounded and is not. `ci.yml` also runs on pushes, which the trunk lane covers, so its coverage step is conditional on the pull request; that condition is pinned -rather than tolerated. +rather than tolerated. Its job also skips on the nightly `schedule`, which +exists for the Kani proofs alone (see "Change-scoped Kani proofs"); that job +condition is pinned beside the step's. The ceiling is judged per job rather than per lane. A lane is one watchdog window, and the ceiling belongs to the job, so the job's lanes are summed diff --git a/docs/formal-verification-methods-in-netsuke.md b/docs/formal-verification-methods-in-netsuke.md index ba557a3a3..a272c9385 100644 --- a/docs/formal-verification-methods-in-netsuke.md +++ b/docs/formal-verification-methods-in-netsuke.md @@ -245,8 +245,11 @@ Formal verification should not be folded into the existing `build-test` job. The current `CI` workflow already performs formatting, linting, tests, and coverage, and those checks should remain intact.[^3] -The `kani-smoke` job is a dedicated job that runs on every trigger: a pull -request, a push to `main`, and a manual dispatch. It: +The `kani-smoke` job is a dedicated, required job that runs on every trigger. +It verifies every harness on each push to `main`, nightly, and on a manual +dispatch; on a pull request it runs them only when the pull request changes a +proof input (see [ADR-039](adr-039-change-scoped-kani-gate.md)). When the +proofs run, it: - installs the pinned Kani front-end and release bundle from checksummed archives, then checks the reported version against `tools/kani/VERSION`, diff --git a/docs/repository-layout.md b/docs/repository-layout.md index 2f3510a8c..e06d2a60e 100644 --- a/docs/repository-layout.md +++ b/docs/repository-layout.md @@ -149,7 +149,9 @@ output and some leaf files so the long-lived structure remains visible. - `tests/features_unix/`: Unix-specific behavioural feature files. - `tests/snapshots/`: Checked-in integration-test snapshots. - `tools/kani/`: Kani formal-verification harness configuration and related - local tooling. + local tooling, including `proof-scope.toml`, the paths whose change runs the + Kani proofs on a pull request (see + [ADR-039](adr-039-change-scoped-kani-gate.md)). - `tools/mold/`: Pinned `mold` linker release version and the SHA-256 checksums used to verify the downloaded release artefacts. diff --git a/scripts/kani_proof_scope.py b/scripts/kani_proof_scope.py new file mode 100755 index 000000000..99b13a67f --- /dev/null +++ b/scripts/kani_proof_scope.py @@ -0,0 +1,287 @@ +#!/usr/bin/env -S uv run --script +# /// script +# requires-python = ">=3.14" +# dependencies = [ +# "cuprum==0.1.0", +# "cyclopts==4.25.3", +# ] +# /// +"""Decide whether the `kani-smoke` job must run its proofs. + +`kani-smoke` is a required check, so it must report on every pull request. +Running every harness on every pull request costs about seven minutes a run, +although most pull requests change nothing a proof depends on. This script is +the job's first step: it reads the proof scope in `tools/kani/proof-scope.toml` +and writes `run-proofs=true` or `run-proofs=false` to the step's outputs, +which every later step of the job is conditioned on. A skipped job still ends +green and says why in the job summary. + +The decision is conservative in both directions it can fail: + +- Any event other than `pull_request` (a push to `main`, the nightly + `schedule`, a manual dispatch) runs every harness, whatever it changes. +- On a pull request, the change set is the diff between the merge commit + GitHub checks out and its first parent, the base branch tip. When that diff + cannot be read (the checkout is not a two-parent merge, or git fails), the + proofs run. + +A malformed scope file is an error rather than a decision, so a broken scope +fails the step loudly instead of silently running, or skipping, everything. + +Usage +----- +In the workflow, with ``INPUT_EVENT_NAME`` set from ``github.event_name``: + +``` +uv run --script scripts/kani_proof_scope.py +``` + +Locally, with a pull request's merge commit checked out, to see what it would +decide: + +``` +uv run --script scripts/kani_proof_scope.py --event-name pull_request +``` +""" + +import dataclasses +import tomllib +import typing as typ +from pathlib import Path + +from cuprum import ExecutionContext, Program, ProgramCatalogue, ProjectSettings +from cuprum import sh as cuprum_sh + +import cyclopts +from cyclopts import App, Parameter + +REPO_ROOT = Path(__file__).resolve().parents[1] +DEFAULT_SCOPE_FILE = REPO_ROOT / "tools" / "kani" / "proof-scope.toml" +SCOPE_KEYS = ("sources", "infrastructure") +#: How many matching paths the summary names before eliding the rest. +SUMMARY_PATH_LIMIT = 10 +#: `git rev-list --parents` prints a merge commit followed by its two parents. +MERGE_COMMIT_FIELDS = 3 +GIT = Program("git") +CATALOGUE = ProgramCatalogue( + projects=[ + ProjectSettings( + name="git", + programs=(GIT,), + documentation_locations=("https://git-scm.com/docs",), + noise_rules=(), + ) + ] +) + +app = App(help=__doc__, config=cyclopts.config.Env("INPUT_", command=False)) + + +class ScopeFileError(Exception): + """Report a proof-scope file the decision cannot trust.""" + + +@dataclasses.dataclass(frozen=True, slots=True) +class Decision: + """Whether the proofs run, and the sentence explaining why.""" + + run_proofs: bool + reason: str + + +@Parameter(name="*") +@dataclasses.dataclass(frozen=True, slots=True) +class StepFiles: + """The files GitHub Actions reads a step's outputs and job summary from.""" + + output: typ.Annotated[Path | None, Parameter(env_var="GITHUB_OUTPUT")] = None + summary: typ.Annotated[Path | None, Parameter(env_var="GITHUB_STEP_SUMMARY")] = None + + +def read_scope(scope_file: Path) -> tuple[str, ...]: + """Return every path in the scope file, sources first. + + An entry ending in `/` names a directory and matches everything beneath + it; any other entry names one file exactly. + + Returns + ------- + tuple[str, ...] + The `sources` entries followed by the `infrastructure` entries. + + Raises + ------ + ScopeFileError + When the file is missing, is not TOML, or lacks a non-empty list of + strings under either key of its `[scope]` table. + """ + try: + document = tomllib.loads(scope_file.read_text(encoding="utf-8")) + except (OSError, tomllib.TOMLDecodeError) as error: + msg = f"cannot read the proof scope {scope_file}: {error}" + raise ScopeFileError(msg) from error + scope = document.get("scope") + table = scope if isinstance(scope, dict) else {} + return tuple( + path for key in SCOPE_KEYS for path in _scope_paths(table, key, scope_file) + ) + + +def _scope_paths(table: dict[str, object], key: str, scope_file: Path) -> list[str]: + """Return the paths under one key of the `[scope]` table. + + Returns + ------- + list[str] + The key's entries, in file order. + + Raises + ------ + ScopeFileError + When the key does not hold a non-empty list of non-empty strings. + """ + values = table.get(key) + if not _is_path_list(values): + msg = f"{scope_file}: [scope] {key} must be a non-empty list of paths" + raise ScopeFileError(msg) + return typ.cast("list[str]", values) + + +def _is_path_list(values: object) -> bool: + """Return whether ``values`` is a non-empty list of non-empty strings.""" + if not isinstance(values, list) or not values: + return False + return all(isinstance(value, str) and value for value in values) + + +def is_in_scope(path: str, scope: tuple[str, ...]) -> bool: + """Return whether a repository-relative ``path`` falls under ``scope``. + + Returns + ------- + bool + Whether a directory entry is a whole-segment prefix of ``path``, or a + file entry equals it. + + Examples + -------- + >>> is_in_scope("src/ir/graph.rs", ("src/ir/", "Cargo.toml")) + True + >>> is_in_scope("src/irony.rs", ("src/ir/",)) + False + """ + return any( + path.startswith(entry) if entry.endswith("/") else path == entry + for entry in scope + ) + + +def _git(repository: Path, *arguments: str) -> str | None: + """Return a git command's standard output, or `None` when it fails.""" + command = cuprum_sh.make(GIT, catalogue=CATALOGUE)(*arguments) + result = command.run_sync(context=ExecutionContext(cwd=repository)) + return ( + result.stdout if result.exit_code == 0 and result.stdout is not None else None + ) + + +def pull_request_changes(repository: Path) -> list[str] | None: + """Return the paths a pull request's merge commit changes. + + `actions/checkout` checks out the merge commit `refs/pull/N/merge`, whose + first parent is the base branch tip, so the diff against that parent is + exactly what merging would change. `--no-renames` reports a rename as a + deletion and an addition, so a file moved out of the scope still counts. + + Returns + ------- + list[str] | None + The changed paths, or `None` when HEAD is not a two-parent merge or + git fails, so that the caller runs the proofs. + """ + parents = _git(repository, "rev-list", "--parents", "--max-count=1", "HEAD") + if parents is None or len(parents.split()) != MERGE_COMMIT_FIELDS: + return None + changed = _git(repository, "diff", "--name-only", "--no-renames", "HEAD^1", "HEAD") + return None if changed is None else [line for line in changed.splitlines() if line] + + +def decide( + event_name: str, scope: tuple[str, ...], changes: list[str] | None +) -> Decision: + """Return the decision for one event and its change set. + + Returns + ------- + Decision + Run on every event but a pull request, and on a pull request whose + change set is unreadable or touches the scope; skip otherwise. + + Examples + -------- + >>> decide("push", ("src/ir/",), None).run_proofs + True + >>> decide("pull_request", ("src/ir/",), ["README.md"]).run_proofs + False + """ + if event_name != "pull_request": + return Decision( + run_proofs=True, reason=f"A `{event_name}` run verifies every harness." + ) + if changes is None: + return Decision( + run_proofs=True, + reason="The pull request's change set could not be read, so every " + "harness runs.", + ) + matched = [path for path in changes if is_in_scope(path, scope)] + if matched: + named = ", ".join(f"`{path}`" for path in matched[:SUMMARY_PATH_LIMIT]) + more = len(matched) - SUMMARY_PATH_LIMIT + elided = f" and {more} more" if more > 0 else "" + return Decision( + run_proofs=True, + reason=f"This pull request changes proof inputs: {named}{elided}.", + ) + return Decision( + run_proofs=False, + reason=f"This pull request changes {len(changes)} path(s), none of them among " + f"the {len(scope)} proof inputs in `tools/kani/proof-scope.toml`, so the " + "harnesses would verify the same inputs as on `main`. Every push to " + "`main` and the nightly schedule run them in full.", + ) + + +def publish(decision: Decision, files: StepFiles) -> None: + """Write the decision to the step outputs, the job summary and the log.""" + value = "true" if decision.run_proofs else "false" + if files.output is not None: + with files.output.open("a", encoding="utf-8") as stream: + stream.write(f"run-proofs={value}\n") + heading = "Kani proofs run" if decision.run_proofs else "Kani proofs skipped" + if files.summary is not None: + with files.summary.open("a", encoding="utf-8") as stream: + stream.write(f"### {heading}\n\n{decision.reason}\n") + print(f"::notice title={heading}::{decision.reason}") + + +@app.default +def main( + *, + event_name: typ.Annotated[str, Parameter(required=True)], + repository: Path = REPO_ROOT, + scope_file: Path = DEFAULT_SCOPE_FILE, + files: StepFiles | None = None, +) -> None: + """Decide whether the proofs run and publish the decision. + + A scope file that cannot be trusted raises out of here, which fails the + step rather than deciding from it. + """ + scope = read_scope(scope_file) + changes = pull_request_changes(repository) if event_name == "pull_request" else None + publish(decide(event_name, scope, changes), files or StepFiles()) + + +if __name__ == "__main__": + app() diff --git a/tests/workflow_contracts/kani_proof_scope_decision_test.py b/tests/workflow_contracts/kani_proof_scope_decision_test.py new file mode 100644 index 000000000..400cf1e7a --- /dev/null +++ b/tests/workflow_contracts/kani_proof_scope_decision_test.py @@ -0,0 +1,273 @@ +"""Behavioural tests for ``scripts/kani_proof_scope.py``. + +The script decides whether `kani-smoke` runs its proofs, so each way it can +be wrong is tested: a non-pull-request event that skips, a pull request whose +change set cannot be read and skips, a path matched by prefix rather than by +directory, and a scope file whose damage turns into a decision instead of an +error. The git half runs against real repositories built in a temporary +directory, and the command-line half runs the script as a child process with +its environment passed to that child alone. + +Run via ``make test-workflow-contracts``. +""" + +import os +import subprocess # ruff: ignore[suspicious-subprocess-import] - the tests drive git and the script as children. +import sys +import typing as typ + +import pytest +from workflow_loading import MAKEFILE_PATH, REPO_ROOT + +sys.path.insert(0, str(REPO_ROOT / "scripts")) + +# The module under test lives in scripts/, outside any package, so the import +# cannot precede the sys.path insertion above. +import kani_proof_scope as scope_mod + +if typ.TYPE_CHECKING: + from pathlib import Path + +SCRIPT = REPO_ROOT / "scripts" / "kani_proof_scope.py" +SCOPE = ("src/ir/", "Cargo.toml") +VALID_SCOPE = '[scope]\nsources = ["src/ir/"]\ninfrastructure = ["Cargo.toml"]\n' +#: A child environment for git that ignores the developer's own configuration, +#: so a signing hook or a default branch name cannot change what is built. +GIT_ENVIRONMENT = { + "PATH": os.environ.get("PATH", ""), + "HOME": "/nonexistent", + "GIT_CONFIG_GLOBAL": os.devnull, + "GIT_CONFIG_NOSYSTEM": "1", + "GIT_AUTHOR_NAME": "Test", + "GIT_AUTHOR_EMAIL": "test@example.invalid", + "GIT_COMMITTER_NAME": "Test", + "GIT_COMMITTER_EMAIL": "test@example.invalid", +} + + +def _git(repository: Path, *arguments: str) -> None: + """Run one git command in ``repository`` and require it to succeed.""" + # The argv is fixed by the test; no untrusted input reaches the child. + subprocess.run( # ruff: ignore[subprocess-without-shell-equals-true] - shell is False. + ["git", *arguments], # ruff: ignore[start-process-with-partial-path] - git from the test PATH. + cwd=repository, + env=GIT_ENVIRONMENT, + check=True, + capture_output=True, + ) + + +def _commit(repository: Path, path: str, message: str) -> None: + """Write ``path`` and commit it.""" + target = repository / path + target.parent.mkdir(parents=True, exist_ok=True) + target.write_text(message, encoding="utf-8") + _git(repository, "add", path) + _git(repository, "commit", "--quiet", "--message", message) + + +def _merge_commit_repository(tmp_path: Path, changed: str) -> Path: + """Return a repository whose HEAD merges a branch that changed ``changed``.""" + # The shape `actions/checkout` produces for a pull request: HEAD is the + # merge commit and its first parent is the base branch tip. + repository = tmp_path / "repository" + repository.mkdir() + _git(repository, "init", "--quiet", "--initial-branch=main") + _commit(repository, "README.md", "base") + _git(repository, "switch", "--quiet", "--create", "topic") + _commit(repository, changed, "topic") + _git(repository, "switch", "--quiet", "main") + _commit(repository, "CHANGELOG.md", "main moved on") + _git(repository, "merge", "--quiet", "--no-ff", "--no-edit", "topic") + return repository + + +@pytest.mark.parametrize("event_name", ["push", "schedule", "workflow_dispatch"]) +def test_every_other_event_runs_the_proofs(event_name: str) -> None: + """Run in full on every event but a pull request, whatever changed.""" + assert scope_mod.decide(event_name, SCOPE, []).run_proofs, event_name + assert scope_mod.decide(event_name, SCOPE, None).run_proofs, event_name + + +def test_unreadable_change_set_runs_the_proofs() -> None: + """Fail closed when the pull request's change set could not be read.""" + assert scope_mod.decide("pull_request", SCOPE, None).run_proofs, ( + "an unreadable change set must run the proofs" + ) + + +@pytest.mark.parametrize( + ("changes", "expected"), + [ + (["src/ir/graph.rs"], True), + (["docs/users-guide.md", "Cargo.toml"], True), + (["src/irony.rs", "Cargo.toml.orig"], False), + (["docs/users-guide.md"], False), + ([], False), + ], +) +def test_pull_request_runs_only_when_a_proof_input_changes( + changes: list[str], *, expected: bool +) -> None: + """Match directories by whole segment and files exactly.""" + decision = scope_mod.decide("pull_request", SCOPE, changes) + assert decision.run_proofs is expected, decision.reason + assert ("none of them" in decision.reason) is not expected, decision.reason + + +def test_matched_paths_are_named_and_elided() -> None: + """Name the first matched paths and count the rest.""" + changes = [f"src/ir/file_{index}.rs" for index in range(12)] + reason = scope_mod.decide("pull_request", SCOPE, changes).reason + assert "`src/ir/file_0.rs`" in reason, reason + assert "`src/ir/file_10.rs`" not in reason, reason + assert "and 2 more" in reason, reason + + +@pytest.mark.parametrize( + "text", + [ + "not toml [", + "[other]\n", + '[scope]\nsources = ["src/ir/"]\n', + '[scope]\nsources = []\ninfrastructure = ["Cargo.toml"]\n', + '[scope]\nsources = ["src/ir/", 3]\ninfrastructure = ["Cargo.toml"]\n', + '[scope]\nsources = ["src/ir/", ""]\ninfrastructure = ["Cargo.toml"]\n', + '[scope]\nsources = "src/ir/"\ninfrastructure = ["Cargo.toml"]\n', + "scope = 3\n", + ], +) +def test_damaged_scope_is_an_error(tmp_path: Path, text: str) -> None: + """Refuse a scope file rather than decide from a damaged one.""" + scope_file = tmp_path / "proof-scope.toml" + scope_file.write_text(text, encoding="utf-8") + with pytest.raises(scope_mod.ScopeFileError): + scope_mod.read_scope(scope_file) + + +def test_missing_scope_is_an_error(tmp_path: Path) -> None: + """Refuse a scope file that does not exist.""" + with pytest.raises(scope_mod.ScopeFileError): + scope_mod.read_scope(tmp_path / "absent.toml") + + +def test_checked_in_scope_reads() -> None: + """Read the repository's own scope, sources first.""" + entries = scope_mod.read_scope(scope_mod.DEFAULT_SCOPE_FILE) + assert "src/ir/" in entries, entries + assert entries.index("src/ir/") < entries.index("Cargo.toml"), entries + + +def test_merge_commit_change_set_is_the_pull_request_diff(tmp_path: Path) -> None: + """Read the merge commit's diff against the base tip, not the whole branch.""" + repository = _merge_commit_repository(tmp_path, "src/ir/graph.rs") + changes = scope_mod.pull_request_changes(repository) + assert changes == ["src/ir/graph.rs"], changes + + +def test_rename_reports_both_paths(tmp_path: Path) -> None: + """Report a file moved out of the scope under its old path as well.""" + repository = _merge_commit_repository(tmp_path, "src/ir/graph.rs") + _git(repository, "switch", "--quiet", "--create", "rename", "HEAD") + (repository / "docs").mkdir() + _git(repository, "mv", "src/ir/graph.rs", "docs/graph.rs") + _git(repository, "commit", "--quiet", "--message", "move") + _git(repository, "switch", "--quiet", "--detach", "main") + _git(repository, "merge", "--quiet", "--no-ff", "--no-edit", "rename") + changes = sorted(scope_mod.pull_request_changes(repository) or []) + assert changes == ["docs/graph.rs", "src/ir/graph.rs"], changes + + +def test_single_parent_head_is_unreadable(tmp_path: Path) -> None: + """Treat a HEAD that is not a merge commit as an unreadable change set.""" + repository = _merge_commit_repository(tmp_path, "src/ir/graph.rs") + _commit(repository, "docs/after.md", "a plain commit on top") + assert scope_mod.pull_request_changes(repository) is None, "HEAD is not a merge" + + +def test_git_failure_is_unreadable(tmp_path: Path) -> None: + """Treat a failing git command, here in a repository with no HEAD, as unreadable.""" + _git(tmp_path, "init", "--quiet") + assert scope_mod.pull_request_changes(tmp_path) is None, "git must have failed" + + +def _run_script( + tmp_path: Path, + repository: Path, + scope_text: str, + event_name: str = "pull_request", +) -> subprocess.CompletedProcess[str]: + """Run the script as the workflow does, with inputs in the child's environment.""" + scope_file = tmp_path / "proof-scope.toml" + scope_file.write_text(scope_text, encoding="utf-8") + environment = { + **GIT_ENVIRONMENT, + "INPUT_EVENT_NAME": event_name, + "INPUT_REPOSITORY": str(repository), + "INPUT_SCOPE_FILE": str(scope_file), + "GITHUB_OUTPUT": str(tmp_path / "output"), + "GITHUB_STEP_SUMMARY": str(tmp_path / "summary.md"), + } + return subprocess.run( # ruff: ignore[subprocess-without-shell-equals-true] - fixed argv, no shell. + [sys.executable, str(SCRIPT)], + env=environment, + capture_output=True, + text=True, + check=False, + ) + + +@pytest.mark.parametrize( + ("changed", "expected"), [("src/ir/graph.rs", "true"), ("docs/guide.md", "false")] +) +def test_script_publishes_the_decision( + tmp_path: Path, changed: str, expected: str +) -> None: + """Write the step output and a summary from the workflow's environment.""" + repository = _merge_commit_repository(tmp_path, changed) + completed = _run_script(tmp_path, repository, VALID_SCOPE) + assert completed.returncode == 0, completed.stderr + output = (tmp_path / "output").read_text(encoding="utf-8") + assert output == f"run-proofs={expected}\n", output + heading = "Kani proofs run" if expected == "true" else "Kani proofs skipped" + summary = (tmp_path / "summary.md").read_text(encoding="utf-8") + assert f"### {heading}" in summary, summary + assert f"::notice title={heading}::" in completed.stdout, completed.stdout + + +@pytest.mark.parametrize("event_name", ["push", "schedule", "workflow_dispatch"]) +def test_script_runs_every_other_event_in_full(tmp_path: Path, event_name: str) -> None: + """Publish a full run for every event but a pull request, whatever changed. + + The merge commit changes only a path outside the scope, which a pull + request would skip, so a run here comes from the event alone. + """ + repository = _merge_commit_repository(tmp_path, "docs/guide.md") + completed = _run_script(tmp_path, repository, VALID_SCOPE, event_name) + assert completed.returncode == 0, completed.stderr + output = (tmp_path / "output").read_text(encoding="utf-8") + assert output == "run-proofs=true\n", output + summary = (tmp_path / "summary.md").read_text(encoding="utf-8") + assert "### Kani proofs run" in summary, summary + assert f"`{event_name}`" in summary, summary + + +def test_script_fails_on_a_damaged_scope(tmp_path: Path) -> None: + """Fail the step, writing no decision, when the scope cannot be trusted.""" + repository = _merge_commit_repository(tmp_path, "docs/guide.md") + completed = _run_script(tmp_path, repository, "[scope]\n") + assert completed.returncode != 0, "a damaged scope must fail the step" + assert not (tmp_path / "output").exists(), "a failed step must decide nothing" + + +def test_dependency_pins_match_the_makefile() -> None: + """Hold the script's inline pins equal to the test and typecheck recipes.""" + header = SCRIPT.read_text(encoding="utf-8").split("# ///", 2)[1] + pins = [line.strip().strip('#", ') for line in header.splitlines() if "==" in line] + makefile = MAKEFILE_PATH.read_text(encoding="utf-8") + assert len(pins) == 2, f"expected the cuprum and cyclopts pins, found {pins}" + for pin in pins: + assert makefile.count(f"--with '{pin}'") == 2, ( + f"`make test-workflow-contracts` and `make typecheck-python` must " + f"both install {pin}, the version the script declares" + ) diff --git a/tests/workflow_contracts/kani_proof_scope_property_test.py b/tests/workflow_contracts/kani_proof_scope_property_test.py new file mode 100644 index 000000000..c3d0fb8d1 --- /dev/null +++ b/tests/workflow_contracts/kani_proof_scope_property_test.py @@ -0,0 +1,99 @@ +"""Generated tests for the proof-scope matching and decision rules. + +``kani_proof_scope_decision_test.py`` drives the script over real repositories +and named cases. This module generates scope entries and changed paths and +checks ``is_in_scope`` and ``decide`` against an oracle that compares path +segments by hand, so a prefix test that matches `src/irony.rs` against +`src/ir/` fails here whatever the examples happen to name. + +Run via ``make test-workflow-contracts``. +""" + +import sys + +from hypothesis import given, settings +from hypothesis import strategies as st +from workflow_loading import REPO_ROOT + +sys.path.insert(0, str(REPO_ROOT / "scripts")) + +# The module under test lives in scripts/, outside any package, so the import +# cannot precede the sys.path insertion above. +import kani_proof_scope as scope_mod + +PROPERTY = settings(max_examples=200, deadline=None) +#: A small alphabet makes a generated path collide with an entry's prefix, or +#: share a stem with its directory name, often enough to exercise the boundary. +SEGMENT = st.sampled_from(["src", "ir", "irony", "a", "b", "Cargo.toml"]) +PATHS = st.lists(SEGMENT, min_size=1, max_size=4).map("/".join) +ENTRIES = st.one_of( + PATHS, + st.lists(SEGMENT, min_size=1, max_size=3).map(lambda s: "/".join(s) + "/"), +) +SCOPES = st.lists(ENTRIES, min_size=1, max_size=5).map(tuple) +EVENTS = st.sampled_from(["push", "schedule", "workflow_dispatch", "anything"]) + + +def matches(path: str, entry: str) -> bool: + """Match by whole segments: a directory entry is a proper segment prefix.""" + if not entry.endswith("/"): + return path == entry + directory = entry.rstrip("/").split("/") + parts = path.split("/") + return len(parts) > len(directory) and parts[: len(directory)] == directory + + +@PROPERTY +@given(path=PATHS, scope=SCOPES) +def test_scope_matching_agrees_with_segment_comparison( + path: str, scope: tuple[str, ...] +) -> None: + """Match a file entry exactly and a directory entry on a segment boundary.""" + expected = any(matches(path, entry) for entry in scope) + assert scope_mod.is_in_scope(path, scope) is expected, f"{path} against {scope}" + + +@PROPERTY +@given(directory=st.lists(SEGMENT, min_size=1, max_size=3), tail=SEGMENT) +def test_a_directory_entry_never_matches_a_sibling_sharing_its_stem( + directory: list[str], tail: str +) -> None: + """Refuse `src/irony.rs` for `src/ir/`: the boundary is the slash, not a prefix.""" + entry = "/".join(directory) + "/" + sibling = "/".join(directory) + tail + inside = "/".join(directory) + "/" + tail + assert not scope_mod.is_in_scope(sibling, (entry,)), f"{sibling} matched {entry}" + assert scope_mod.is_in_scope(inside, (entry,)), f"{inside} missed {entry}" + + +@PROPERTY +@given(scope=SCOPES, changes=st.lists(PATHS, max_size=6), data=st.data()) +def test_a_pull_request_runs_exactly_when_a_change_is_in_scope( + scope: tuple[str, ...], changes: list[str], data: st.DataObject +) -> None: + """Run the proofs on a pull request iff a change matches, in any order.""" + expected = any(matches(path, entry) for path in changes for entry in scope) + shuffled = data.draw(st.permutations(changes)) + reordered = tuple(data.draw(st.permutations(scope))) + decision = scope_mod.decide("pull_request", scope, changes) + assert decision.run_proofs is expected, f"{changes} against {scope}" + again = scope_mod.decide("pull_request", reordered, shuffled) + assert again.run_proofs is expected, f"order changed the decision for {scope}" + + +@PROPERTY +@given(scope=SCOPES) +def test_an_unreadable_change_set_runs_the_proofs(scope: tuple[str, ...]) -> None: + """Run every harness when the diff is unreadable, never skip on a guess.""" + decision = scope_mod.decide("pull_request", scope, None) + assert decision.run_proofs is True, f"an unreadable diff skipped for {scope}" + + +@PROPERTY +@given(event=EVENTS, scope=SCOPES, changes=st.one_of(st.none(), st.lists(PATHS))) +def test_every_event_but_a_pull_request_runs_the_proofs( + event: str, scope: tuple[str, ...], changes: list[str] | None +) -> None: + """Run every harness on a push, schedule or dispatch whatever it changes.""" + decision = scope_mod.decide(event, scope, changes) + assert decision.run_proofs is True, f"a `{event}` run skipped the proofs" diff --git a/tests/workflow_contracts/kani_proof_scope_test.py b/tests/workflow_contracts/kani_proof_scope_test.py new file mode 100644 index 000000000..556bd2410 --- /dev/null +++ b/tests/workflow_contracts/kani_proof_scope_test.py @@ -0,0 +1,236 @@ +"""Hold `tools/kani/proof-scope.toml` to what the Kani harnesses depend on. + +`kani-smoke` skips its proofs on a pull request that changes nothing in the +proof scope, so a scope missing one input lets a pull request that breaks a +proof merge green. These contracts recompute the harnesses' module closure +from the Rust source (see ``rust_module_closure``) and fail when the scope +misses any of it, when a `#[kani::proof]` file anywhere in the repository is +outside it, or when a toolchain input is dropped. They also fail when the +scope grows past the closure, since a scope covering the whole crate would +satisfy sufficiency and quietly run the proofs on every pull request again. + +Run via ``make test-workflow-contracts``. +""" + +import re +import tomllib +import typing as typ + +import pytest +from rust_module_closure import kani_seeds, reachable_files +from rust_module_graph import CrateSource, read_crate +from rust_source_scan import mask_non_code +from workflow_loading import MAKEFILE_PATH, REPO_ROOT + +if typ.TYPE_CHECKING: + from pathlib import Path + +SCOPE_FILE = REPO_ROOT / "tools" / "kani" / "proof-scope.toml" +CRATE_ROOT = REPO_ROOT / "src" / "lib.rs" +#: What builds and runs the proofs, which no source closure can find: each is +#: an input `cargo kani` or the `kani-smoke` job reads. ADR-039 records why. +REQUIRED_INFRASTRUCTURE = ( + ".cargo/", # Cargo configuration read by every cargo invocation + ".github/actions/kani-cache/", # the cached verifier payloads + ".github/workflows/ci.yml", # the job, its installer and its pins + "Cargo.lock", # the resolved dependencies the harnesses compile against + "Cargo.toml", # features, dependencies and `[package.metadata.kani]` + "Makefile", # the `kani-ir` and `kani-full` targets and their flags + "build.rs", # the build script `cargo kani` runs before compiling + "docs/verification/mutations/", # the patches the mutation gate compiles + "rust-toolchain.toml", # the toolchain pin + "scripts/kani_proof_scope.py", # the decision itself + "tests/kani_mutation_evidence_tests.rs", # the mutation compile gate + "tests/kani_mutation_evidence_tests/", # its modules + "tests/kani_scope_wrapper_e2e_tests.rs", # the scope wrapper's own suite + "tools/kani/", # the verifier version and this scope +) +MUTATIONS_DIR = REPO_ROOT / "docs" / "verification" / "mutations" +PROOF_ATTRIBUTE = re.compile(r"#\[\s*kani\s*::\s*proof\s*\]") +SKIPPED_DIRECTORIES = frozenset({"target", "node_modules"}) + + +def _scope() -> dict[str, list[str]]: + """Return the `[scope]` table of the proof-scope file.""" + return tomllib.loads(SCOPE_FILE.read_text(encoding="utf-8"))["scope"] + + +def _relative(path: Path) -> str: + """Return ``path`` relative to the repository root, POSIX-style.""" + return path.relative_to(REPO_ROOT).as_posix() + + +def _covers(entry: str, path: str) -> bool: + """Return whether one scope entry covers a repository-relative path.""" + if entry.endswith("/"): + return path == entry.removesuffix("/") or path.startswith(entry) + return path == entry + + +def _covered_files(entry: str) -> list[Path]: + """Return every file on disk one scope entry covers.""" + target = REPO_ROOT / entry + if entry.endswith("/"): + return sorted(path for path in target.rglob("*") if path.is_file()) + return [target] if target.is_file() else [] + + +def _repository_rust_files() -> list[Path]: + """Return every Rust source in the repository outside build and hidden trees.""" + return sorted( + path + for path in REPO_ROOT.rglob("*.rs") + if not any( + part in SKIPPED_DIRECTORIES or part.startswith(".") + for part in path.relative_to(REPO_ROOT).parts + ) + ) + + +@pytest.fixture(scope="module") +def crate() -> CrateSource: + """Return the library crate's module tree.""" + return read_crate(CRATE_ROOT) + + +@pytest.fixture(scope="module") +def closure(crate: CrateSource) -> set[str]: + """Return the harness closure as repository-relative paths.""" + return {_relative(path) for path in reachable_files(crate, kani_seeds(crate))} + + +def test_every_proof_harness_file_is_in_scope() -> None: + """Require every file declaring `#[kani::proof]` to be a proof input. + + The search covers the whole repository, not just the library, so a + harness added to a test tree or another crate fails here until the scope + and the Kani invocation are extended to it. Comments and string literals + are masked, so prose quoting the attribute does not count. + """ + harnesses = [ + _relative(path) + for path in _repository_rust_files() + if PROOF_ATTRIBUTE.search( + mask_non_code(path.read_text(encoding="utf-8"), set()) + ) + ] + assert harnesses, "no `#[kani::proof]` harness found; the discovery is broken" + sources = _scope()["sources"] + outside = [path for path in harnesses if not any(_covers(e, path) for e in sources)] + assert not outside, ( + f"these harness files are outside tools/kani/proof-scope.toml " + f"`sources`: {outside}" + ) + + +def test_scope_covers_the_harness_closure(closure: set[str]) -> None: + """Require every file the harnesses can reach to be a proof input.""" + sources = _scope()["sources"] + missing = sorted( + path for path in closure if not any(_covers(e, path) for e in sources) + ) + assert not missing, ( + f"the harnesses reach these paths, which tools/kani/proof-scope.toml " + f"`sources` does not cover: {missing}" + ) + + +def _is_beneath(path: str, directories: set[str]) -> bool: + """Return whether ``path`` lies inside one of ``directories``.""" + return any(path.startswith(f"{directory}/") for directory in directories) + + +def _unreached_files(entry: str, allowed: set[str], directories: set[str]) -> list[str]: + """Return the files one scope entry covers that no harness reaches. + + A file is reached when ``allowed`` names it or it lies beneath one of the + ``directories`` the closure reaches (an include target). + + Returns + ------- + list[str] + The covered files outside the closure, repository-relative. + """ + return [ + path + for path in map(_relative, _covered_files(entry)) + if path not in allowed and not _is_beneath(path, directories) + ] + + +def test_scope_reaches_no_further_than_the_closure( + crate: CrateSource, closure: set[str] +) -> None: + """Require each source entry to cover only the closure and its test modules. + + A test-only module is compiled out under `cargo kani`, so a directory + entry may cover one harmlessly. Anything else means the entry is broader + than what the proofs depend on. + """ + test_only = {_relative(m.file) for m in crate.modules.values() if m.is_test_only} + directories = {path for path in closure if (REPO_ROOT / path).is_dir()} + broad = { + entry: unreached + for entry in _scope()["sources"] + if (unreached := _unreached_files(entry, closure | test_only, directories)) + } + assert not broad, f"these entries cover files no harness reaches: {broad}" + + +def test_every_scope_entry_covers_the_closure(closure: set[str]) -> None: + """Require every source entry to cover at least one path in the closure. + + An entry covering nothing a harness reaches is stale, so it is removed + rather than kept. + """ + dead = [ + e for e in _scope()["sources"] if not any(_covers(e, path) for path in closure) + ] + assert not dead, f"these entries cover nothing a harness reaches: {dead}" + + +def test_every_mutation_patch_target_is_in_scope() -> None: + """Require every file a mutation patch edits to be a proof input. + + The mutation compile gate applies each patch before compiling, so a pull + request that changes a patched file can break the gate even where no + harness reaches that file. + """ + targets = sorted({ + line.removeprefix("+++ b/").strip() + for patch in sorted(MUTATIONS_DIR.glob("*.patch")) + for line in patch.read_text(encoding="utf-8").splitlines() + if line.startswith("+++ b/") + }) + assert targets, "no mutation patch target found; the discovery is broken" + sources = _scope()["sources"] + outside = [path for path in targets if not any(_covers(e, path) for e in sources)] + assert not outside, f"these patched files are outside the scope: {outside}" + + +def test_scope_names_every_toolchain_input() -> None: + """Require the inputs no source closure can find, each present on disk.""" + infrastructure = _scope()["infrastructure"] + missing = [ + entry for entry in REQUIRED_INFRASTRUCTURE if entry not in infrastructure + ] + assert not missing, f"the proof scope must name these inputs: {missing}" + absent = [entry for entry in infrastructure if not (REPO_ROOT / entry).exists()] + assert not absent, f"these proof-scope entries do not exist: {absent}" + + +def test_kani_compiles_without_the_test_configuration() -> None: + """Require `cargo kani` to stay off `--tests`. + + The closure leaves out `#[cfg(test)]` modules because `cargo kani` does + not compile them. Passing `--tests` would compile them, so the closure + would silently miss every test module a harness could then reach. + """ + makefile = MAKEFILE_PATH.read_text(encoding="utf-8") + kani_lines = [line for line in makefile.splitlines() if "KANI" in line] + assert not [line for line in kani_lines if "--tests" in line], ( + "the Makefile's Kani invocation must not pass `--tests`" + ) + manifest = tomllib.loads((REPO_ROOT / "Cargo.toml").read_text(encoding="utf-8")) + flags = manifest["package"]["metadata"]["kani"]["flags"] + assert "tests" not in flags, "`[package.metadata.kani.flags]` must not set `tests`" diff --git a/tests/workflow_contracts/kani_smoke_scope_wiring_test.py b/tests/workflow_contracts/kani_smoke_scope_wiring_test.py new file mode 100644 index 000000000..bf589b312 --- /dev/null +++ b/tests/workflow_contracts/kani_smoke_scope_wiring_test.py @@ -0,0 +1,144 @@ +"""Hold `kani-smoke` to the change-scoped shape ADR-039 records. + +`kani-smoke` is a required check on the ruleset, so a pull request cannot +merge until it reports. Skipping the job itself, with a trigger `paths` +filter or a job-level `if:`, leaves a required check that never reports and a +pull request that can never merge. The job therefore always runs, its first +real step decides whether the proofs can differ from `main`'s, and every step +after the decision is conditioned on it. These contracts pin that shape: the +decision's position and command, the condition on every later step, the +absence of a job condition and trigger filters, and the nightly schedule that +runs the proofs in full. + +Run via ``make test-workflow-contracts``. +""" + +import pytest +from workflow_loading import ( + job_steps, + load_workflow, + require_list, + require_mapping, + workflow_job, +) + +JOB = "kani-smoke" +DECISION_STEP = "Decide Kani proof scope" +DECISION_COMMAND = "uv run --script scripts/kani_proof_scope.py" +#: The output the script writes; `kani_proof_scope_decision_test.py` runs the +#: script and reads this exact key back from `GITHUB_OUTPUT`. +PROOF_CONDITION = "steps.scope.outputs.run-proofs == 'true'" +#: The jobs other than `kani-smoke`, which the nightly schedule must not run. +SCHEDULE_EXCLUDED_JOBS = ("build-test", "windows") +NOT_ON_SCHEDULE = "github.event_name != 'schedule'" + + +@pytest.fixture(scope="module") +def workflow() -> dict[str, object]: + """Return the CI workflow.""" + return load_workflow() + + +@pytest.fixture(scope="module") +def steps(workflow: dict[str, object]) -> list[dict[str, object]]: + """Return the `kani-smoke` steps.""" + return job_steps(workflow, JOB) + + +def _decision_index(steps: list[dict[str, object]]) -> int: + """Return the position of the one decision step.""" + positions = [ + index for index, step in enumerate(steps) if step.get("name") == DECISION_STEP + ] + assert len(positions) == 1, f"`{JOB}` must have exactly one `{DECISION_STEP}` step" + return positions[0] + + +def test_job_always_runs_and_reports(workflow: dict[str, object]) -> None: + """Refuse a job condition, which would stop a required check reporting.""" + assert "if" not in workflow_job(workflow, JOB), ( + f"`{JOB}` is a required check; a job-level `if:` can leave it unreported" + ) + + +def test_triggers_carry_no_path_filters(workflow: dict[str, object]) -> None: + """Refuse trigger path filters, which skip the whole workflow's checks.""" + triggers = require_mapping(workflow.get("on"), "ci.yml triggers") + filtered = { + event: key + for event, settings in triggers.items() + if isinstance(settings, dict) + for key in ("paths", "paths-ignore") + if key in settings + } + assert not filtered, f"ci.yml triggers must not filter paths: {filtered}" + + +def test_nightly_schedule_runs_only_the_proofs(workflow: dict[str, object]) -> None: + """Require one nightly cron and every other job excluded from it.""" + triggers = require_mapping(workflow.get("on"), "ci.yml triggers") + schedule = require_list(triggers.get("schedule"), "ci.yml schedule") + crons = [require_mapping(entry, "schedule entry").get("cron") for entry in schedule] + assert crons == ["41 4 * * *"], f"expected the one nightly cron, found {crons}" + for job in SCHEDULE_EXCLUDED_JOBS: + assert workflow_job(workflow, job).get("if") == NOT_ON_SCHEDULE, ( + f"`{job}` must skip the nightly schedule, which exists for `{JOB}` alone" + ) + + +def test_decision_reads_the_merge_commit(steps: list[dict[str, object]]) -> None: + """Require the checkout to fetch the merge commit's first parent.""" + checkout = steps[0] + assert str(checkout.get("uses", "")).startswith("actions/checkout@"), ( + f"`{JOB}` must start with the checkout" + ) + assert ( + require_mapping(checkout.get("with"), "checkout inputs").get("fetch-depth") == 2 + ), "the scope decision diffs HEAD against HEAD^1, which needs `fetch-depth: 2`" + + +def test_decision_step_is_unconditional_and_runs_the_script( + steps: list[dict[str, object]], +) -> None: + """Require the decision to run on every trigger, as its step's sole command.""" + index = _decision_index(steps) + decision = steps[index] + assert decision.get("id") == "scope", "later steps read `steps.scope.outputs`" + assert "if" not in decision, "the decision must run on every trigger" + assert decision.get("run") == DECISION_COMMAND, ( + f"the decision must run `{DECISION_COMMAND}` as its sole command" + ) + env = require_mapping(decision.get("env"), "decision env") + assert env == {"INPUT_EVENT_NAME": "${{ github.event_name }}"}, ( + f"the decision must read the triggering event and nothing else: {env}" + ) + before = [str(step.get("uses", "")).split("@", 1)[0] for step in steps[:index]] + assert before == ["actions/checkout", "astral-sh/setup-uv"], ( + "only the checkout and uv may precede the decision, so a skipped run " + f"pays for nothing else; found {before}" + ) + assert all("if" not in step for step in steps[:index]), ( + "the steps the decision needs must run unconditionally" + ) + + +def test_every_later_step_is_conditioned_on_the_decision( + steps: list[dict[str, object]], +) -> None: + """Require the exact decision condition on every step after it. + + A later step without it runs its work on a skipped pull request; a step + with any other condition may skip on a push to `main`, where the proofs + must always run. The presence half requires the harness step itself, so + that deleting it cannot satisfy the condition check vacuously. + """ + later = steps[_decision_index(steps) + 1 :] + assert any(step.get("run") == "make kani-ir" for step in later), ( + f"`{JOB}` must run `make kani-ir` after the decision" + ) + unconditioned = [ + step.get("name") for step in later if step.get("if") != PROOF_CONDITION + ] + assert not unconditioned, ( + f"these `{JOB}` steps do not carry `if: {PROOF_CONDITION}`: {unconditioned}" + ) diff --git a/tests/workflow_contracts/nextest_lane_mold_test.py b/tests/workflow_contracts/nextest_lane_mold_test.py index 96d8cf976..8c44dd87b 100644 --- a/tests/workflow_contracts/nextest_lane_mold_test.py +++ b/tests/workflow_contracts/nextest_lane_mold_test.py @@ -125,6 +125,32 @@ def test_the_install_cannot_be_guarded(documents: Documents, makefile: str) -> N _reports(documents, makefile, "must not carry an `if:`") +KANI_LANE = ("ci.yml", "kani-smoke") + + +def test_a_guard_every_suite_step_shares_is_allowed( + documents: Documents, makefile: str +) -> None: + """`kani-smoke` gates its install and its suite steps on one decision.""" + steps = _steps(documents, *KANI_LANE) + guard = _install(steps).get("if") + assert guard, "kani-smoke's install must carry the decision guard" + assert "ci.yml:kani-smoke" in suite_lanes(documents, makefile), ( + "kani-smoke must be derived as a suite lane for this case to mean anything" + ) + _clean(documents, makefile) + + +def test_a_guard_one_suite_step_lacks_is_refused( + documents: Documents, makefile: str +) -> None: + """The install is skipped while an unguarded suite step still runs.""" + steps = _steps(documents, *KANI_LANE) + gate = next(s for s in steps if s.get("run") == "make test-kani-mutations") + del gate["if"] + _reports(documents, makefile, "must not carry an `if:`") + + def test_the_install_cannot_continue_on_error( documents: Documents, makefile: str ) -> None: diff --git a/tests/workflow_contracts/nextest_lane_rules.py b/tests/workflow_contracts/nextest_lane_rules.py index 33c037372..2f22dd65b 100644 --- a/tests/workflow_contracts/nextest_lane_rules.py +++ b/tests/workflow_contracts/nextest_lane_rules.py @@ -5,7 +5,8 @@ measured build never links with ``mold``: the coverage lanes assign ``RUSTFLAGS`` and so displace the linker flag, yet their tests still reach the preflight. So every Linux job that runs the suite must run -``make install-build-tools`` in a step of its own, unguarded, before the suite. +``make install-build-tools`` in a step of its own, before the suite, and +unguarded unless every suite step carries the same guard. Which jobs those are is derived, not listed. A job runs the suite when a step calls the shared coverage action, runs ``cargo nextest run`` itself, or invokes @@ -233,6 +234,31 @@ def suite_lanes(documents: dict[str, dict[str, object]], makefile: str) -> list[ return [where for where, _ in _suite_jobs(documents, nextest_goals(makefile))] +def _guard_is_shared(steps: Steps, install: int, goals: frozenset[str]) -> bool: + """Return whether the install runs whenever any suite step does. + + An unguarded install always does. A guarded one does only when every + suite step carries the identical guard, as in `kani-smoke`, where one + decision step gates every later step alike (ADR-039). + + Guards are compared as written, so the same condition spelled with and + without `${{ }}` counts as different and is refused: the rule fails loud + rather than open. The quantifier is never vacuous here, since + ``_lane_violations`` runs only for jobs with at least one suite step, and + ``test_a_guard_every_suite_step_shares_is_allowed`` pins `kani-smoke` as + such a job. + + Returns + ------- + bool + Whether the install is unguarded, or every suite step shares its guard. + """ + if "if" not in steps[install]: + return True + guard = steps[install]["if"] + return all(step.get("if") == guard for step in steps if runs_suite(step, goals)) + + def _lane_violations(where: str, steps: Steps, goals: frozenset[str]) -> list[str]: """Check one suite lane's install step against the rule.""" first_suite = next(i for i, step in enumerate(steps) if runs_suite(step, goals)) @@ -248,8 +274,11 @@ def _lane_violations(where: str, steps: Steps, goals: frozenset[str]) -> list[st f"{where}: installs the build standard only after " f"{step_name(steps[first_suite])!r} runs the suite" ) - if "if" in steps[install]: - problems.append(f"{where}: `make install-build-tools` must not carry an `if:`") + if not _guard_is_shared(steps, install, goals): + problems.append( + f"{where}: `make install-build-tools` must not carry an `if:` " + "that every suite step does not carry too" + ) if steps[install].get("continue-on-error") not in {None, False}: problems.append( f"{where}: `make install-build-tools` must not continue on error" diff --git a/tests/workflow_contracts/release_dry_run_smoke_test.py b/tests/workflow_contracts/release_dry_run_smoke_test.py index 7a2eb627c..2c89d357f 100644 --- a/tests/workflow_contracts/release_dry_run_smoke_test.py +++ b/tests/workflow_contracts/release_dry_run_smoke_test.py @@ -14,8 +14,9 @@ answer (`ready_for_review`), where no gate run would cover it. 2. `release` still needs it, so publication cannot proceed without it. 3. The pull request still runs the same smoke: `ci.yml` calls the Windows gate - unconditionally, `build-test-windows` carries no condition of its own, and - its smoke invocation is the release job's, token for token. + on every event but the nightly Kani schedule, `build-test-windows` carries + no condition of its own, and its smoke invocation is the release job's, + token for token. Run via ``make test-workflow-contracts``. """ @@ -50,6 +51,12 @@ "|| github.event.action == 'ready_for_review'" ) +#: The only condition `ci.yml` may put on its Windows gate. The nightly +#: schedule exists for the Kani proofs alone (ADR-039), and this expression is +#: true on every other event, so every pull request still calls the gate. +#: Compared whole, so any other condition fails. +WINDOWS_GATE_CONDITION = "github.event_name != 'schedule'" + #: The pull-request event types the dry run answers that `ci.yml` does not. #: The smoke must run for each of them, because no gate run covers it. UNCOVERED_BY_CI = frozenset({"ready_for_review"}) @@ -140,15 +147,16 @@ def test_publication_still_needs_the_smoke() -> None: def test_the_pull_request_runs_the_same_smoke() -> None: """Hold the pull-request gate to the smoke the dry run no longer runs. - Unconditional at both levels, and the same invocation token for token. If - any of these drifted, a pull request would reach its merge without the - smoke the dry run used to give it. + Called on every pull request, unconditional inside the gate, and the same + invocation token for token. If any of these drifted, a pull request would + reach its merge without the smoke the dry run used to give it. """ windows_call = workflow_job(load_workflow(CI_WORKFLOW_PATH), "windows") condition, called = windows_call.get("if"), windows_call.get("uses") - # Key absence, not a null value: GitHub reads an empty `if` as false. - assert "if" not in windows_call, ( - f"ci.yml must call the Windows gate on every run, got {condition!r}" + # Key absence, or the schedule exclusion exactly: GitHub reads an empty + # `if` as false, so a null value is refused like any other condition. + assert "if" not in windows_call or condition == WINDOWS_GATE_CONDITION, ( + f"ci.yml must call the Windows gate on every pull request, got {condition!r}" ) assert called == "./.github/workflows/ci-windows.yml", ( f"ci.yml's windows job must call ci-windows.yml, got {called!r}" diff --git a/tests/workflow_contracts/rust_module_closure.py b/tests/workflow_contracts/rust_module_closure.py new file mode 100644 index 000000000..1013d3fdd --- /dev/null +++ b/tests/workflow_contracts/rust_module_closure.py @@ -0,0 +1,312 @@ +"""Close over the source files a set of Rust files can depend on. + +`kani-smoke` skips its proofs on a pull request that changes none of their +inputs, so the proof-scope contract must know every file a harness can depend +on. Starting from the files ``kani_seeds`` names, this module follows the +references each reached file makes, over the tree ``rust_module_graph`` reads: + +- a `crate::`, `super::`, `self::` or `$crate::` path reaches the module it + names, together with every compiled module nested beneath it, and a `{…}` + use group reaches each module it names; +- a bare `child::` path reaches a module declared in the same file; +- a `name!` invocation reaches every file defining `macro_rules! name`; +- an `impl` item whose header names a type or trait the closure defines + reaches the file holding it, since coherence lets an impl live anywhere in + the crate; +- `include_str!`, `include_bytes!` and `include!` reach the file a literal + argument names, or the directory of a `concat!`'s leading literal. + +A reached module's declaring ancestors are added at the end, since the +attributes on a `mod` line decide whether and how it is compiled. Every rule +over-approximates; the crate root alone is reached as a file rather than a +subtree, because every module sits beneath it. + +Test-only: production code and workflows must not import this module. +""" + +import re +import typing as typ + +from rust_module_graph import STRING_LITERAL, ModuleGraphError, closing_bracket + +if typ.TYPE_CHECKING: + from pathlib import Path + + from rust_module_graph import CrateSource, RustModule + +ROOTED_PATH = re.compile(r"(?\$crate|crate|super|self)\s*::") +PATH_SEGMENT = re.compile(r"\s*(?P[A-Za-z_]\w*)\s*::") +GROUP_OPEN = re.compile(r"\s*\{") +FINAL_SEGMENT = re.compile(r"\s*(?P[A-Za-z_]\w*)") +GROUP_NAME = re.compile(r"(?:^|[{,])\s*(?P[A-Za-z_]\w*)") +BARE_PATH = re.compile(r"(?[A-Za-z_]\w*)\s*::") +MACRO_DEFINITION = re.compile(r"\bmacro_rules!\s*(?P[A-Za-z_]\w*)") +MACRO_CALL = re.compile(r"(?[A-Za-z_]\w*)!") +TYPE_DEFINITION = re.compile( + r"\b(?:struct|enum|union|trait|type)\s+(?P[A-Za-z_]\w*)" +) +#: An `impl` item at the start of a line; `impl Trait` in argument or return +#: position is a type, not an item, and never starts a line. +IMPL_HEADER = re.compile(r"(?m)^[ \t]*(?:unsafe\s+)?impl\b(?P
[^{;]*)\{") +IDENTIFIER = re.compile(r"[A-Za-z_]\w*") +INCLUDE_CALL = re.compile(r"\binclude(?:_str|_bytes)?!\s*\(") +ASSEMBLED_PATH = re.compile(r'concat!\s*\(\s*"(?P[^"\\]*)"') +KANI_MARKER = re.compile(r"\bkani\b|#\[\s*global_allocator\s*\]") + + +def _rooted_targets( + crate: CrateSource, module: RustModule, code: str +) -> set[tuple[str, ...]]: + """Return the modules the rooted paths in ``code`` name.""" + targets = set() + for match in ROOTED_PATH.finditer(code): + base, index = _walk_path(code, match.end(), _path_base(module, match["head"])) + prefix = crate.resolve(base) + targets.add(prefix) + targets.add(_final_target(crate, base, code, index)) + if group := GROUP_OPEN.match(code, index): + targets |= _grouped_targets(crate, prefix, code, group.end()) + return targets + + +def _final_target( + crate: CrateSource, base: tuple[str, ...], code: str, index: int +) -> tuple[str, ...]: + """Return the module a path's final segment names, or ``base`` itself. + + `use crate::hasher;` names the module `hasher` in a segment no `::` + follows, and the file then reaches it through a bare `hasher::` path that + ``_bare_targets`` cannot see from a nested module. When the final segment + is an item rather than a module, resolving falls back to ``base``. + + Returns + ------- + tuple[str, ...] + The longest module prefix of the path including its final segment. + """ + final = FINAL_SEGMENT.match(code, index) + return crate.resolve((*base, final["name"]) if final else base) + + +def _path_base(module: RustModule, head: str) -> tuple[str, ...]: + """Return the module a rooted path's ``head`` keyword starts from.""" + match head: + case "self": + return module.path + case "super": + return module.path[:-1] + case _: + return () + + +def _walk_path( + code: str, index: int, base: tuple[str, ...] +) -> tuple[tuple[str, ...], int]: + """Return the module a path names from ``base``, and where the walk stopped. + + The walk consumes further `super::` hops and module names, stopping at a + brace group, a glob or an item. + + Returns + ------- + tuple[tuple[str, ...], int] + The named module path and the offset just past its last segment. + """ + while segment := PATH_SEGMENT.match(code, index): + base = base[:-1] if segment["name"] == "super" else (*base, segment["name"]) + index = segment.end() + return base, index + + +def _grouped_targets( + crate: CrateSource, prefix: tuple[str, ...], code: str, start: int +) -> set[tuple[str, ...]]: + """Return the modules a `{a::b, c}` use group names beneath ``prefix``. + + Nested groups are flattened to their first segment beneath ``prefix``, + which reaches the whole subtree and so over-approximates. + + Returns + ------- + set[tuple[str, ...]] + The longest module prefix of each name the group starts with. + """ + group = code[start : closing_bracket(code, start) - 1] + names = {match["name"] for match in GROUP_NAME.finditer(group)} + return {crate.resolve((*prefix, name)) for name in names - {"self"}} + + +def _bare_targets( + crate: CrateSource, module: RustModule, code: str +) -> set[tuple[str, ...]]: + """Return the child modules of ``module`` named by a bare `child::` path.""" + children = {child.path[-1]: child.path for child in crate.children(module.path)} + return { + children[match["name"]] + for match in BARE_PATH.finditer(code) + if match["name"] in children + } + + +def _include_targets(file: Path, code: str, text: str) -> set[Path]: + """Return the files and directories the `include*!` calls in a file read. + + The argument list is delimited on the fully masked ``code``, so a + parenthesis inside a literal cannot end it early, and read from ``text`` + at the same offsets. A literal argument names one file. A `concat!` whose + first argument is a literal names the directory of that literal, which + covers every file the assembled path can name there. Any other argument is + refused by ``_include_target``. + + Returns + ------- + set[Path] + The resolved file and directory targets. + """ + return { + _include_target( + file, text[match.end() : closing_bracket(code, match.end(), "()") - 1] + ) + for match in INCLUDE_CALL.finditer(code) + } + + +def _include_target(file: Path, arguments: str) -> Path: + """Return the file or directory one include's ``arguments`` name. + + Returns + ------- + Path + The resolved target. + + Raises + ------ + ModuleGraphError + When the path is neither a literal nor a `concat!` led by one. + """ + if whole := STRING_LITERAL.fullmatch(arguments.strip()): + return (file.parent / whole["value"]).resolve() + if assembled := ASSEMBLED_PATH.match(arguments.strip()): + directory = assembled["value"].rpartition("/")[0] or "." + return (file.parent / directory).resolve() + msg = f"{file}: an include without a literal path cannot be resolved" + raise ModuleGraphError(msg) + + +def _defined_names(crate: CrateSource, files: set[Path]) -> set[str]: + """Return every type and trait name defined in ``files``.""" + return { + name for file in files for name in TYPE_DEFINITION.findall(crate.code[file]) + } + + +def _implementing_files(crate: CrateSource, names: set[str]) -> set[Path]: + """Return every compiled file with an `impl` header naming one of ``names``.""" + return { + module.file + for module in crate.modules.values() + if not module.is_test_only + and any( + names & set(IDENTIFIER.findall(match["header"])) + for match in IMPL_HEADER.finditer(crate.code[module.file]) + ) + } + + +def _macro_files(crate: CrateSource) -> dict[str, set[Path]]: + """Return the files defining each `macro_rules!` name in the crate.""" + definitions: dict[str, set[Path]] = {} + for module in crate.modules.values(): + for name in MACRO_DEFINITION.findall(crate.code[module.file]): + definitions.setdefault(name, set()).add(module.file) + return definitions + + +def _file_references( + crate: CrateSource, file: Path, macros: dict[str, set[Path]] +) -> set[Path]: + """Return the files one reached file references directly.""" + module = crate.module_of(file) + code = crate.code[file] + modules = _rooted_targets(crate, module, code) | _bare_targets(crate, module, code) + # The crate root names the root file alone: every module sits beneath it, + # so reaching its subtree would reach the whole crate for any root item. + referenced = {crate.modules[()].file for path in modules if not path} + referenced |= { + nested.file + for path in modules + if path + for nested in crate.subtree(path) + if not nested.is_test_only + } + return referenced | { + definition + for call in MACRO_CALL.findall(code) + for definition in macros.get(call, set()) + } + + +def reachable_files(crate: CrateSource, seeds: set[Path]) -> set[Path]: + """Return the source files and include targets ``seeds`` can depend on. + + Each reached module's declaring ancestors are included too, since the + attributes on a `mod` line (`cfg`, `path`) decide whether and how the + module is compiled at all. + + Returns + ------- + set[Path] + The reached files, their declaring ancestors, and include targets. + """ + macros = _macro_files(crate) + reached: set[Path] = set() + pending = set(seeds) + while pending: + reached |= pending + frontier = { + reference + for file in pending + for reference in _file_references(crate, file, macros) + } + frontier |= _implementing_files(crate, _defined_names(crate, reached)) + pending = frontier - reached + ancestors = _declaring_ancestors(crate, reached) + return reached | ancestors | _all_includes(crate, reached) + + +def _declaring_ancestors(crate: CrateSource, files: set[Path]) -> set[Path]: + """Return the files declaring each module on the way down to ``files``.""" + return { + crate.modules[crate.module_of(file).path[:length]].file + for file in files + for length in range(len(crate.module_of(file).path)) + } + + +def _all_includes(crate: CrateSource, files: set[Path]) -> set[Path]: + """Return every include target the `include*!` calls in ``files`` read.""" + return { + target + for file in files + for target in _include_targets(file, crate.code[file], crate.text[file]) + } + + +def kani_seeds(crate: CrateSource) -> set[Path]: + """Return every compiled file whose code names Kani or a global allocator. + + A `#[kani::proof]` harness is a seed, and so is any `cfg(kani)` or + `kani::` site, since it changes what the verifier compiles even where no + harness reaches it by path. A `#[global_allocator]` changes every + allocation a harness makes. + + Returns + ------- + set[Path] + The seed files. + """ + return { + module.file + for module in crate.modules.values() + if not module.is_test_only and KANI_MARKER.search(crate.code[module.file]) + } diff --git a/tests/workflow_contracts/rust_module_closure_property_test.py b/tests/workflow_contracts/rust_module_closure_property_test.py new file mode 100644 index 000000000..fd9b8ceb3 --- /dev/null +++ b/tests/workflow_contracts/rust_module_closure_property_test.py @@ -0,0 +1,259 @@ +"""Generated tests for the Rust module reader and its closure rules. + +The example-based tests in ``rust_module_closure_test.py`` pin one synthetic +crate. This module generates small file-backed crates instead and checks the +closure against an oracle that never reads Rust text: each crate is rendered +from an explicit edge list, so the expected reached set is a plain graph +reachability over that list, not a second parse of the source. + +The generated crates are flat (every module is a child of the root) and avoid +`impl` headers, because the closure documents both as over-approximating +where the oracle would have to guess; the rules that over-approximate are +pinned by the example-based tests. Within that space the closure must be +exact: every required dependency reached, and nothing test-only. + +Run via ``make test-workflow-contracts``. +""" + +import dataclasses +import tempfile +from pathlib import Path + +import pytest +from hypothesis import given, settings +from hypothesis import strategies as st +from rust_module_closure import kani_seeds, reachable_files +from rust_module_graph import ModuleGraphError, read_crate + +#: How a module refers to another: a rooted path, a final-segment `use`, a +#: `use` group, or a call of the macro the other module defines. +EDGE_KINDS = ("rooted", "final", "group", "macro") +MAX_MODULES = 6 +MAX_EDGES = 10 +MAX_INCLUDES = 3 +#: Generated crates are tiny, so a modest budget explores them well and keeps +#: each example, which writes files, cheap. +PROPERTY = settings(max_examples=60, deadline=None) + + +@dataclasses.dataclass(frozen=True, slots=True) +class Spec: + """A generated crate: which modules exist and how they refer to each other.""" + + count: int + is_test_only: tuple[bool, ...] + is_seed: tuple[bool, ...] + edges: frozenset[tuple[int, str, int]] + includes: frozenset[tuple[int, int]] + + +@st.composite +def specs(draw: st.DrawFn) -> Spec: + """Draw a small crate specification.""" + count = draw(st.integers(min_value=1, max_value=MAX_MODULES)) + index = st.integers(min_value=0, max_value=count - 1) + flags = st.tuples(*[st.booleans()] * count) + edge = st.tuples(index, st.sampled_from(EDGE_KINDS), index) + include = st.tuples(index, st.integers(min_value=0, max_value=MAX_INCLUDES)) + return Spec( + count, + draw(flags), + draw(flags), + frozenset(draw(st.lists(edge, max_size=MAX_EDGES))), + frozenset(draw(st.lists(include, max_size=MAX_INCLUDES))), + ) + + +def _module_lines(spec: Spec, index: int) -> list[str]: + """Return the source lines of module ``index``, one construct per line.""" + lines = [] + if spec.is_seed[index]: + lines.append("#[kani::proof] fn proof() {}") + if not spec.is_test_only[index]: + lines.append(f"macro_rules! mac{index} {{ () => {{}}; }}") + for n, (source, kind, target) in enumerate(sorted(spec.edges)): + if source != index: + continue + lines.append( + { + "rooted": f"fn r{n}() {{ crate::m{target}::f(); }}", + "final": f"use crate::m{target};", + "group": f"use crate::{{m{target}, m{target}}};", + "macro": f"fn c{n}() {{ mac{target}!(); }}", + }[kind] + ) + lines.extend( + f'const D{n}: &str = include_str!("../data/d{data}.txt");' + for n, (source, data) in enumerate(sorted(spec.includes)) + if source == index + ) + return lines + + +def render(spec: Spec, *, declaration_order: list[int], rotation: int = 0) -> dict: + """Return the crate's files, declaring modules and lines in a chosen order.""" + files = { + "src/lib.rs": "\n".join( + ("#[cfg(test)]\n" if spec.is_test_only[i] else "") + f"mod m{i};" + for i in declaration_order + ) + + "\n" + } + for index in range(spec.count): + lines = _module_lines(spec, index) + shift = rotation % len(lines) if lines else 0 + files[f"src/m{index}.rs"] = "\n".join(lines[shift:] + lines[:shift]) + "\n" + return files + + +def oracle(spec: Spec) -> set[str]: + """Return the files the closure must reach, by graph reachability alone.""" + compiled = {i for i in range(spec.count) if not spec.is_test_only[i]} + reached = {i for i in compiled if spec.is_seed[i]} + pending = set(reached) + while pending: + pending = { + target + for source, _, target in spec.edges + if source in pending and target in compiled + } - reached + reached |= pending + # The root declares every module, so it joins whenever any module does. + files = {f"src/m{i}.rs" for i in reached} | ({"src/lib.rs"} if reached else set()) + return files | {f"data/d{data}.txt" for i, data in spec.includes if i in reached} + + +def closure( + spec: Spec, *, declaration_order: list[int] | None = None, rotation: int = 0 +) -> set[str]: + """Write the crate, run the production closure, and return relative paths.""" + order = list(range(spec.count)) if declaration_order is None else declaration_order + with tempfile.TemporaryDirectory() as directory: + root = Path(directory).resolve() + for relative, text in render( + spec, declaration_order=order, rotation=rotation + ).items(): + (root / relative).parent.mkdir(parents=True, exist_ok=True) + (root / relative).write_text(text, encoding="utf-8") + crate = read_crate(root / "src" / "lib.rs") + return { + path.relative_to(root).as_posix() + for path in reachable_files(crate, kani_seeds(crate)) + } + + +@PROPERTY +@given(spec=specs()) +def test_closure_equals_graph_reachability(spec: Spec) -> None: + """Reach exactly the modules the edge list reaches from the compiled seeds. + + Every required dependency must be present, and a test-only module, or + anything only a test-only module refers to, must be absent. + """ + assert closure(spec) == oracle(spec), f"closure differs from oracle for {spec}" + + +@PROPERTY +@given(spec=specs(), data=st.data()) +def test_closure_is_stable_under_declaration_and_line_order( + spec: Spec, data: st.DataObject +) -> None: + """Return the same set however the modules and their lines are ordered.""" + order = data.draw(st.permutations(range(spec.count))) + rotation = data.draw(st.integers(min_value=0, max_value=MAX_EDGES)) + reordered = closure(spec, declaration_order=order, rotation=rotation) + assert reordered == closure(spec), f"order {order}/{rotation} changed {spec}" + + +@PROPERTY +@given(spec=specs(), data=st.data()) +def test_adding_a_reference_or_seed_never_shrinks_the_closure( + spec: Spec, data: st.DataObject +) -> None: + """Keep every reached file when a supported reference or a seed is added.""" + index = st.integers(min_value=0, max_value=spec.count - 1) + extra = data.draw(st.tuples(index, st.sampled_from(EDGE_KINDS), index)) + seed = data.draw(index) + seeds = tuple(is_seed or i == seed for i, is_seed in enumerate(spec.is_seed)) + grown = dataclasses.replace(spec, edges=spec.edges | {extra}, is_seed=seeds) + assert closure(spec) <= closure(grown), f"{grown} lost a file of {spec}" + + +@PROPERTY +@given(spec=specs(), data=st.data()) +def test_a_test_only_module_never_seeds_or_joins_the_closure( + spec: Spec, data: st.DataObject +) -> None: + """Ignore a test-only module even when it carries the Kani marker.""" + index = data.draw(st.integers(min_value=0, max_value=spec.count - 1)) + flagged = tuple(flag or i == index for i, flag in enumerate(spec.is_test_only)) + marked = tuple(flag or i == index for i, flag in enumerate(spec.is_seed)) + hidden = dataclasses.replace(spec, is_test_only=flagged, is_seed=marked) + assert f"src/m{index}.rs" not in closure(hidden), "a test-only module was reached" + + +def _refusal(spec: Spec, path: str, appended: str) -> None: + """Append ``appended`` to one generated file and run the closure.""" + with tempfile.TemporaryDirectory() as directory: + root = Path(directory).resolve() + files = render(spec, declaration_order=list(range(spec.count))) + files[path] += appended + for relative, text in files.items(): + (root / relative).parent.mkdir(parents=True, exist_ok=True) + (root / relative).write_text(text, encoding="utf-8") + crate = read_crate(root / "src" / "lib.rs") + reachable_files(crate, kani_seeds(crate)) + + +@PROPERTY +@given(spec=specs(), name=st.from_regex(r"[a-z]{1,8}", fullmatch=True)) +def test_a_module_declared_inside_a_block_is_refused(spec: Spec, name: str) -> None: + """Raise rather than guess where an inline module's `mod x;` resolves.""" + with pytest.raises(ModuleGraphError, match="nested in a block"): + _refusal(spec, "src/m0.rs", f"\nmod block_{name} {{ mod hidden_{name}; }}\n") + + +@PROPERTY +@given(spec=specs(), name=st.from_regex(r"[a-z]{1,8}", fullmatch=True)) +def test_a_declared_module_without_a_file_is_refused(spec: Spec, name: str) -> None: + """Raise when a `mod x;` names a file that does not exist.""" + with pytest.raises(ModuleGraphError, match="has no file"): + _refusal(spec, "src/lib.rs", f"mod absent_{name};\n") + + +@PROPERTY +@given(spec=specs()) +def test_a_non_literal_include_in_a_reached_file_is_refused(spec: Spec) -> None: + """Raise when a reached file's include names no literal path.""" + marked = dataclasses.replace( + spec, + is_test_only=(False, *spec.is_test_only[1:]), + is_seed=(True, *spec.is_seed[1:]), + ) + with pytest.raises(ModuleGraphError, match="without a literal path"): + _refusal(marked, "src/m0.rs", '\nconst X: &str = include_str!(env!("X"));\n') + + +@PROPERTY +@given( + kinds=st.lists(st.sampled_from(EDGE_KINDS), min_size=1, max_size=MAX_MODULES - 1) +) +def test_a_chain_of_any_reference_forms_is_followed_to_its_end( + kinds: list[str], +) -> None: + """Follow a seed through a chain where each link uses one reference form. + + A general crate rarely draws a module whose only way in is one particular + form, so this family makes each link the sole route to the next module and + fails if any reference form stops being followed. + """ + count = len(kinds) + 1 + chain = Spec( + count, + (False,) * count, + (True, *(False,) * len(kinds)), + frozenset((i, kind, i + 1) for i, kind in enumerate(kinds)), + frozenset(), + ) + expected = {"src/lib.rs", *(f"src/m{i}.rs" for i in range(count))} + assert closure(chain) == oracle(chain) == expected, f"chain {kinds} broke" diff --git a/tests/workflow_contracts/rust_module_closure_test.py b/tests/workflow_contracts/rust_module_closure_test.py new file mode 100644 index 000000000..3b0674525 --- /dev/null +++ b/tests/workflow_contracts/rust_module_closure_test.py @@ -0,0 +1,185 @@ +"""Drive the Rust module-closure rules over a synthetic crate. + +The proof-scope contract passes over this repository's source whether or not +a given rule works, since the checked-in scope already covers what the rules +find. These tests build a small crate in which each rule, and each exclusion, +decides exactly one file, and pin the reached set, so that breaking any rule +changes the answer here. + +Run via ``make test-workflow-contracts``. +""" + +import typing as typ + +import pytest +from rust_module_closure import kani_seeds, reachable_files +from rust_module_graph import ModuleGraphError, read_crate + +if typ.TYPE_CHECKING: + from pathlib import Path + +#: One file per rule. The comment on each says why it is, or is not, reached. +SYNTHETIC_CRATE: dict[str, str] = { + "src/lib.rs": """ +pub mod harness; +pub mod model; +pub mod unrelated; +mod inherent; +mod macros; +mod argument_position; +mod sibling; +mod echo; +mod tail; +#[cfg(test)] +mod test_only; +""", + # The seed: reaches `model` by a rooted path, `macros` by a call, and + # `data/fixture.txt` by an include followed by a method call. The comment + # and the inline test module name `unrelated` and must not reach it, and + # the test module's unresolvable include must not be read at all. + "src/harness.rs": """ +// crate::unrelated::helper() is prose, not a reference. +#[kani::proof] +fn proof() { + let value = crate::model::Model::new(); + checked!(value); + let _ = include_str!("../data/fixture.txt").contains(")"); +} + +#[cfg(test)] +mod tests { + use crate::unrelated::helper; + const OUTSIDE: &str = include_str!(env!("NOT_A_LITERAL")); +} +""", + # Reached by path; its compiled subtree comes with it, including a + # `#[path]` child, but not its test-only child. + "src/model.rs": """ +pub struct Model; +pub mod nested; +#[path = "custom/located.rs"] +pub mod located; +#[cfg(test)] +mod model_tests; +""", + # Imports the crate-root `tail` by its final segment, then uses it bare. + "src/model/nested.rs": "use crate::tail;\npub fn nested() { tail::wag(); }\n", + "src/tail.rs": "pub fn wag() {}\n", + "src/model/model_tests.rs": "use crate::unrelated::helper;\n", + # Reached through `super::super::sibling` from inside the model subtree. + "src/custom/located.rs": "pub fn located() { super::super::sibling::touch(); }\n", + # Its `self::echo` names its own child, not the crate's `echo`. + "src/sibling.rs": "pub mod echo;\npub fn touch() { self::echo::ring(); }\n", + "src/sibling/echo.rs": "pub fn ring() {}\n", + # Not reached: only a `self::` path inside `sibling` spells its name. + "src/echo.rs": "pub fn ring() {}\n", + # Reached because its `impl` header names `Model`, a type the closure defines. + "src/inherent.rs": """ +impl crate::model::Model { + pub fn new() -> Self { Self } +} +""", + # Reached because the harness invokes `checked!`. + "src/macros.rs": "macro_rules! checked { ($value:expr) => {}; }\n", + # Not reached: `impl` in argument position is a type, not an impl item. + "src/argument_position.rs": "pub fn take(_: impl AsRef) {}\n", + # Not reached: nothing names it outside comments and test code. + "src/unrelated.rs": "pub fn helper() {}\n", + # Not reached, and compiled out under `cargo kani`. + "src/test_only.rs": "use crate::harness;\n", + "data/fixture.txt": "fixture\n", +} + +EXPECTED_REACHED = { + "src/lib.rs", + "src/harness.rs", + "src/model.rs", + "src/model/nested.rs", + "src/tail.rs", + "src/custom/located.rs", + "src/sibling.rs", + "src/sibling/echo.rs", + "src/inherent.rs", + "src/macros.rs", + "data/fixture.txt", +} + + +def _write_crate(root: Path, files: dict[str, str]) -> Path: + """Write ``files`` beneath ``root`` and return the crate root file.""" + for relative, text in files.items(): + path = root / relative + path.parent.mkdir(parents=True, exist_ok=True) + path.write_text(text, encoding="utf-8") + return root / "src" / "lib.rs" + + +def _reached(root: Path) -> set[str]: + """Return the synthetic crate's harness closure, relative to ``root``.""" + crate = read_crate(root / "src" / "lib.rs") + return { + path.relative_to(root.resolve()).as_posix() + for path in reachable_files(crate, kani_seeds(crate)) + } + + +def test_closure_follows_every_rule_and_no_further(tmp_path: Path) -> None: + """Pin the reached set of a crate where each rule decides one file.""" + _write_crate(tmp_path, SYNTHETIC_CRATE) + reached = _reached(tmp_path) + assert reached == EXPECTED_REACHED, ( + f"unexpected closure: extra {sorted(reached - EXPECTED_REACHED)}, " + f"missing {sorted(EXPECTED_REACHED - reached)}" + ) + + +def test_test_only_modules_are_marked(tmp_path: Path) -> None: + """Mark a `#[cfg(test)]` module, and only that one, as test-only.""" + crate = read_crate(_write_crate(tmp_path, SYNTHETIC_CRATE)) + test_only = {path for path, module in crate.modules.items() if module.is_test_only} + assert test_only == {("test_only",), ("model", "model_tests")}, ( + f"test-only modules: {test_only}" + ) + + +def test_seeds_include_cfg_kani_sites(tmp_path: Path) -> None: + """Treat a `cfg(kani)` site as a seed even when no harness reaches it.""" + files = { + **SYNTHETIC_CRATE, + "src/unrelated.rs": "#[cfg(kani)]\npub fn helper() {}\n", + } + _write_crate(tmp_path, files) + assert "src/unrelated.rs" in _reached(tmp_path), "a `cfg(kani)` site must seed" + + +def test_assembled_include_reaches_the_literal_directory(tmp_path: Path) -> None: + """Reach the directory of an assembled include's literal prefix.""" + harness = SYNTHETIC_CRATE["src/harness.rs"].replace( + 'include_str!("../data/fixture.txt")', + 'include_str!(concat!("../data/", "fixture.txt"))', + ) + _write_crate(tmp_path, {**SYNTHETIC_CRATE, "src/harness.rs": harness}) + reached = _reached(tmp_path) + assert "data" in reached, "the literal prefix's directory must be reached" + assert "data/fixture.txt" not in reached, "an assembled path names no one file" + + +@pytest.mark.parametrize( + ("relative", "text", "message"), + [ + ("src/unrelated.rs", "mod inline {\n mod hidden;\n}\n", "nested in a block"), + ("src/unrelated.rs", "mod absent;\n", "has no file"), + ( + "src/harness.rs", + '#[kani::proof]\nfn proof() { include_str!(env!("X")); }\n', + "without a literal path", + ), + ], +) +def test_unsupported_layouts_are_refused( + tmp_path: Path, relative: str, text: str, message: str +) -> None: + """Refuse a layout the reader would otherwise resolve by guessing.""" + _write_crate(tmp_path, {**SYNTHETIC_CRATE, relative: text}) + with pytest.raises(ModuleGraphError, match=message): + _reached(tmp_path) diff --git a/tests/workflow_contracts/rust_module_graph.py b/tests/workflow_contracts/rust_module_graph.py new file mode 100644 index 000000000..218fdd2bc --- /dev/null +++ b/tests/workflow_contracts/rust_module_graph.py @@ -0,0 +1,243 @@ +"""Read a Rust crate's module tree from its source text. + +The Kani proof-scope contract needs each file-backed module of the library +crate: its path from the crate root, the file that backs it, and whether it +is compiled only under `cfg(test)`. This module reads that tree from the crate +root, following `mod name;` declarations and `#[path]` attributes, and keeps +each file's text twice: fully masked, for code queries, and with only comments +masked, where string literals such as `#[path]` values must stay readable. +``rust_module_closure`` closes over the references in that text. + +A module declared under `#[cfg(test)]`, and an inline `#[cfg(test)] mod … { +… }` body, are marked or masked because `cargo kani` compiles without +`cfg(test)`. A `mod name;` nested inside an inline module body is refused +rather than resolved by guesswork, so an unsupported layout fails the contract +instead of silently shrinking the scope. + +Test-only: production code and workflows must not import this module. +""" + +import dataclasses +import functools +import re +import typing as typ + +from rust_source_scan import mask_non_code + +if typ.TYPE_CHECKING: + from pathlib import Path + +#: A file-backed `mod name;` declaration with the attribute block before it. +MOD_DECLARATION = re.compile( + r"(?P(?:#\[[^\]]*\]\s*)*)" + r"(?:pub(?:\s*\([^)]*\))?\s+)?mod\s+(?P[A-Za-z_]\w*)\s*(?P[;{])" +) +PATH_ATTRIBUTE = re.compile(r'#\[\s*path\s*=\s*"(?P[^"]+)"\s*\]') +TEST_ONLY_CFG = re.compile(r"#\[\s*cfg\s*\(\s*(?:test\s*\)|all\s*\(\s*test\b)") +STRING_LITERAL = re.compile(r'"(?P[^"\\]*)"') +STRING_PREFIXES = ('"', 'r"', "r#", 'b"', "br") +MOD_RS_NAMES = frozenset({"lib.rs", "main.rs", "mod.rs"}) + + +class ModuleGraphError(Exception): + """Report a module layout the reader refuses to guess about.""" + + +@dataclasses.dataclass(frozen=True, slots=True) +class RustModule: + """One file-backed module: its path from the crate root and its file.""" + + path: tuple[str, ...] + file: Path + is_test_only: bool + + +@dataclasses.dataclass(frozen=True) +class CrateSource: + """The module tree of one crate and two views of each file's text. + + ``code`` masks comments and literals, so every brace and path in it is + real, and blanks inline `#[cfg(test)]` module bodies; ``text`` masks only + comments, so literals stay readable at the same offsets. Every query finds + its match in ``code`` and reads literals from ``text`` at that offset, so + nothing in a blanked body is ever read. + """ + + modules: dict[tuple[str, ...], RustModule] + code: dict[Path, str] + text: dict[Path, str] + + @functools.cached_property + def _by_file(self) -> dict[Path, RustModule]: + """Index the modules by the file that backs each.""" + return {module.file: module for module in self.modules.values()} + + def module_of(self, file: Path) -> RustModule: + """Return the module a file backs.""" + return self._by_file[file] + + def children(self, path: tuple[str, ...]) -> list[RustModule]: + """Return the modules declared directly inside ``path``.""" + return [m for m in self.modules.values() if m.path[:-1] == path and m.path] + + def subtree(self, path: tuple[str, ...]) -> list[RustModule]: + """Return ``path`` and every module nested beneath it.""" + return [m for m in self.modules.values() if m.path[: len(path)] == path] + + def resolve(self, path: tuple[str, ...]) -> tuple[str, ...]: + """Return the longest prefix of ``path`` that names a module.""" + for length in range(len(path), -1, -1): + if path[:length] in self.modules: + return path[:length] + return () + + +def closing_bracket(code: str, start: int, pair: str = "{}") -> int: + """Return the offset just past the bracket closing the one before ``start``. + + ``code`` must be fully masked, so that no bracket inside a literal or a + comment is counted. + + Returns + ------- + int + The offset after the matching closing bracket, or the end of ``code`` + when the brackets never balance. + """ + depth, index = 1, start + while depth and index < len(code): + depth += {pair[0]: 1, pair[1]: -1}.get(code[index], 0) + index += 1 + return index + + +def _test_only_spans(code: str) -> list[tuple[int, int]]: + """Return the span of every inline `#[cfg(test)] mod … { … }` in ``code``.""" + return [ + (match.start(), closing_bracket(code, match.end())) + for match in MOD_DECLARATION.finditer(code) + if match["end"] == "{" and TEST_ONLY_CFG.search(match["attributes"]) + ] + + +def _blank(text: str, spans: list[tuple[int, int]]) -> str: + """Replace each span of ``text`` with spaces, keeping its line breaks.""" + characters = list(text) + for start, end in spans: + characters[start:end] = ( + "\n" if character == "\n" else " " for character in text[start:end] + ) + return "".join(characters) + + +def _declared_file( + parent: Path, name: str, path_attribute: str | None, *, is_mod_rs: bool +) -> Path: + """Return the file a `mod name;` declared in ``parent`` loads.""" + if path_attribute is not None: + return (parent.parent / path_attribute).resolve() + directory = parent.parent if is_mod_rs else parent.parent / parent.stem + flat = directory / f"{name}.rs" + return flat if flat.is_file() else directory / name / "mod.rs" + + +def _file_declarations( + file: Path, code: str, text: str +) -> list[tuple[str, str | None, bool]]: + """Return each file-backed module declared in ``file``, refusing nested ones. + + ``code`` is the fully masked source, whose braces are all real, and + ``text`` the same source with only comments masked, from which the + `#[path]` literal is read at the same offsets. + + Returns + ------- + list[tuple[str, str | None, bool]] + Each module's name, its `#[path]` value if any, and whether it is + declared under `#[cfg(test)]`. + + Raises + ------ + ModuleGraphError + When a `mod name;` sits inside a brace block, where its file would + resolve relative to an inline module the reader does not model. + """ + declarations = [] + for match in MOD_DECLARATION.finditer(code): + if match["end"] != ";": + continue + if code[: match.start()].count("{") != code[: match.start()].count("}"): + msg = f"{file}: `mod {match['name']};` is nested in a block" + raise ModuleGraphError(msg) + attributes = text[match.start("attributes") : match.end("attributes")] + path_match = PATH_ATTRIBUTE.search(attributes) + declarations.append(( + match["name"], + path_match["path"] if path_match else None, + bool(TEST_ONLY_CFG.search(attributes)), + )) + return declarations + + +class _EveryStringLiteral(set[str]): + """Claim to contain every string literal, so masking keeps them all. + + ``mask_non_code`` retains the literals its caller names; naming them in + advance would need a second tokenizer, and a regular expression pairing + quotes falls out of step at the first escaped quote. + """ + + def __contains__(self, literal: object) -> bool: + """Return whether ``literal`` is a string rather than a comment.""" + return isinstance(literal, str) and literal.startswith(STRING_PREFIXES) + + +def comment_free(source: str) -> str: + """Mask Rust comments while keeping every string literal readable.""" + return mask_non_code(source, _EveryStringLiteral()) + + +def _file_views(file: Path) -> tuple[str, str]: + """Return a file's masked code, test bodies blanked, and comment-free text.""" + raw = file.read_text(encoding="utf-8") + masked = mask_non_code(raw, set()) + return _blank(masked, _test_only_spans(masked)), comment_free(raw) + + +def read_crate(crate_root: Path) -> CrateSource: + """Read every file-backed module reachable from ``crate_root``. + + Returns + ------- + CrateSource + The module tree with each file's masked views. + + Raises + ------ + ModuleGraphError + When a declared module's file is missing or the layout is refused. + """ + modules: dict[tuple[str, ...], RustModule] = {} + code: dict[Path, str] = {} + text: dict[Path, str] = {} + pending = [(RustModule((), crate_root.resolve(), is_test_only=False), True)] + while pending: + module, is_mod_rs = pending.pop() + if not module.file.is_file(): + msg = f"module {'::'.join(module.path)} has no file at {module.file}" + raise ModuleGraphError(msg) + modules[module.path] = module + code[module.file], text[module.file] = _file_views(module.file) + for name, path_attribute, is_test_only in _file_declarations( + module.file, code[module.file], text[module.file] + ): + child = _declared_file( + module.file, name, path_attribute, is_mod_rs=is_mod_rs + ) + pending.append(( + RustModule( + (*module.path, name), child, module.is_test_only or is_test_only + ), + path_attribute is not None or child.name in MOD_RS_NAMES, + )) + return CrateSource(modules, code, text) diff --git a/tests/workflow_contracts/timeout_ordering_test.py b/tests/workflow_contracts/timeout_ordering_test.py index 21d32a975..f4501b0d3 100644 --- a/tests/workflow_contracts/timeout_ordering_test.py +++ b/tests/workflow_contracts/timeout_ordering_test.py @@ -72,7 +72,9 @@ #: changing a condition changes when it runs at all. #: #: `ci.yml` also runs on pushes, where the trunk lane covers the same -#: ground, so its coverage step is conditional on the pull request. +#: ground, so its coverage step is conditional on the pull request. Its +#: nightly schedule exists for the Kani proofs alone, so the job skips on +#: that trigger, which never reaches the pull-request step anyway. #: Keyed by workflow, job and step, because a job may run the coverage #: action twice and the steps need not carry the same condition; keying #: by job alone let the second overwrite the first. The entry pins a step @@ -81,7 +83,7 @@ REQUIRED_CONDITIONS: typ.Final[dict[tuple[str, str, str], tuple[object, object]]] = { ("ci.yml", "build-test", "Test and Measure Coverage"): ( "github.event_name == 'pull_request'", - None, + "github.event_name != 'schedule'", ), ("coverage-main.yml", "coverage-upload", "Test and Measure Coverage"): ( None, diff --git a/tools/kani/proof-scope.toml b/tools/kani/proof-scope.toml new file mode 100644 index 000000000..83accff32 --- /dev/null +++ b/tools/kani/proof-scope.toml @@ -0,0 +1,56 @@ +# The paths a Kani proof in this repository can depend on. +# +# `scripts/kani_proof_scope.py` skips the `kani-smoke` proofs on a pull request +# that changes none of these paths; every push to `main` and the nightly +# schedule run them in full. An entry ending in `/` names a directory and +# covers everything beneath it; any other entry names one file. +# +# Do not edit `sources` by guesswork. It is the module closure of the +# `#[kani::proof]` harnesses, which tests/workflow_contracts/kani_proof_scope_test.py +# recomputes from the source on every run: the contract fails when a file the +# harnesses reach is missing here, and when an entry covers a file they cannot +# reach. When it fails, it prints the files to add or remove. See +# docs/adr-039-change-scoped-kani-gate.md for the derivation rules. + +[scope] +sources = [ + "locales/", + "src/ast/", + "src/cli_localization.rs", + "src/hasher.rs", + "src/hex.rs", + "src/ir/", + "src/lib.rs", + "src/locale_catalogues.rs", + "src/localization/", + "src/ninja_gen/", + "src/ninja_gen_command_list.rs", + "src/ninja_gen_command_list_scanner.rs", + "src/ninja_gen_error.rs", + "src/ninja_gen_escape.rs", + "src/ninja_gen_recipe_shell.rs", + "src/ninja_gen_validation.rs", + "src/recipe_shell.rs", + "src/shell_word.rs", +] + +# What builds and runs the proofs rather than what they prove, and the inputs of +# the job's other steps (the scope wrapper's suite and the mutation compile +# gate), which the same decision gates. The contract requires each of these, +# since none can be derived from the Rust source. +infrastructure = [ + ".cargo/", + ".github/actions/kani-cache/", + ".github/workflows/ci.yml", + "Cargo.lock", + "Cargo.toml", + "Makefile", + "build.rs", + "docs/verification/mutations/", + "rust-toolchain.toml", + "scripts/kani_proof_scope.py", + "tests/kani_mutation_evidence_tests.rs", + "tests/kani_mutation_evidence_tests/", + "tests/kani_scope_wrapper_e2e_tests.rs", + "tools/kani/", +]