From fbde8291242ab46f892cc0a28deaa2011e0c94be Mon Sep 17 00:00:00 2001 From: leynos Date: Wed, 29 Jul 2026 00:35:01 +0200 Subject: [PATCH 01/10] Run the bounded Kani harness set in the kani-smoke PR job (#445) The `kani-smoke` job previously ran only `make kani-check` (a version check) because no proof harnesses existed when the lane shipped in `4.1.2`. The `4.2.*` work has since landed 13 `#[kani::proof]` harnesses, so wire them into the pull-request job: - Add a "Run Kani harnesses" step invoking `make kani-ir` after the version check, and guard the job with `timeout-minutes: 20` per the `4.1.2` execplan's cold-run ceiling. - Extend `behavioural_ci_workflow_wires_kani_smoke_job` to pin the new step and the timeout. - Update the developers' guide and roadmap so they no longer state that CI skips the harness suite. The `build-test` job and the isolated Kani cache are unchanged. --- .github/workflows/ci.yml | 3 +++ docs/developers-guide.md | 10 ++++++---- docs/roadmap.md | 9 ++++----- tests/workflow_ci.rs | 10 ++++++++++ 4 files changed, 23 insertions(+), 9 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index a9bd0057c..fbf9c5339 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -112,6 +112,7 @@ jobs: kani-smoke: if: github.event_name == 'pull_request' runs-on: ubuntu-latest + timeout-minutes: 20 permissions: contents: read env: @@ -140,3 +141,5 @@ jobs: run: make install-kani - name: Kani version check run: make kani-check + - name: Run Kani harnesses + run: make kani-ir diff --git a/docs/developers-guide.md b/docs/developers-guide.md index 057fd489f..95cfc3e60 100644 --- a/docs/developers-guide.md +++ b/docs/developers-guide.md @@ -845,10 +845,12 @@ 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 `uv`, installs the pinned Kani version -through `make install-kani`, and runs only `make kani-check`; it does not run -`make kani-full`, `make verus`, coverage, CodeScene upload, or the normal build -matrix. Its cache is intentionally separate from ordinary Cargo build -artefacts: the job uses a Kani-specific cache key derived from +through `make install-kani`, runs `make kani-check` as a version-drift guard, +and then runs the bounded harness suite through `make kani-ir` under a +20-minute job timeout; it does not run `make verus`, coverage, CodeScene +upload, or the normal build matrix. Its cache is intentionally separate from +ordinary Cargo build artefacts: the job uses a Kani-specific cache key derived +from `tools/kani/VERSION` and the Makefile, then caches the job-local Kani Cargo home plus Kani support-file home. diff --git a/docs/roadmap.md b/docs/roadmap.md index b2b92e2bd..44e74354f 100644 --- a/docs/roadmap.md +++ b/docs/roadmap.md @@ -355,11 +355,10 @@ and test workflow intact. See Requires 4.1.1. See [formal-verification-methods-in-netsuke.md §Continuous integration (CI)](formal-verification-methods-in-netsuke.md#continuous-integration-ci). - [x] Keep the existing `build-test` job unchanged. - - [x] Run the bounded smoke path on pull requests. As scoped for this item, - the `kani-smoke` job in `.github/workflows/ci.yml` runs `make install-kani` - and `make kani-check` (a Kani version check); the harness set was empty when - this lane shipped. Wiring the bounded harnesses since landed by `4.2.*` into - the pull-request job is tracked separately as + - [x] Run the bounded smoke path on pull requests. The `kani-smoke` job in + `.github/workflows/ci.yml` runs `make install-kani`, `make kani-check` (a + Kani version check), and `make kani-ir` (the bounded harnesses landed by + `4.2.*`). The harness wiring resolved the follow-up previously tracked as [issue #445](https://github.com/leynos/netsuke/issues/445). - [x] Cache Kani tool downloads separately from ordinary Cargo artefacts. - [x] 4.1.3. Record the phase-1 scope boundary for Verus and Stateright. See diff --git a/tests/workflow_ci.rs b/tests/workflow_ci.rs index 0425d9ee0..808b30ae7 100644 --- a/tests/workflow_ci.rs +++ b/tests/workflow_ci.rs @@ -266,5 +266,15 @@ fn behavioural_ci_workflow_wires_kani_smoke_job() -> Result<()> { .any(|step| step_has(step, StepField::Runs, "make kani-check")), "Kani smoke job should check Kani through the Make target" ); + ensure!( + steps + .iter() + .any(|step| step_has(step, StepField::Runs, "make kani-ir")), + "Kani smoke job should run the bounded Kani harnesses through the Make target" + ); + ensure!( + mapping_get(kani_job, YamlKey("timeout-minutes")).and_then(Value::as_u64) == Some(20), + "Kani smoke job should enforce the 20-minute cold-run ceiling" + ); Ok(()) } From ac595ce8e27e5ed1427f1f80a1597dd6895c07a7 Mon Sep 17 00:00:00 2001 From: leynos Date: Wed, 29 Jul 2026 00:57:33 +0200 Subject: [PATCH 02/10] Fix cfg(kani) compile errors in the cycle harnesses (#445) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Wiring `make kani-ir` into CI exposed two latent breakages in code that only compiles under `cfg(kani)`: - `src/ir/cycle_verification.rs` calls `rotate_index`, which lives in the private `support` module and was never in scope. Import it explicitly. - `cycle.rs` imported `path_cmp` unconditionally, but its only use is in the `#[cfg(not(kani))]` `detect_targets` path, producing an unused-import error under Kani. Gate the import to match. Nothing compiled the harness set in CI before, so these regressions went unnoticed — precisely the gap #445 closes. --- src/ir/cycle.rs | 4 +++- src/ir/cycle_verification.rs | 1 + 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/src/ir/cycle.rs b/src/ir/cycle.rs index 23a828372..cc82ba72b 100644 --- a/src/ir/cycle.rs +++ b/src/ir/cycle.rs @@ -28,7 +28,9 @@ mod cycle_property_tests; mod support; #[cfg(any(test, kani))] use support::canonicalize_cycle_by; -use support::{canonicalize_cycle, path_cmp, path_eq, state_for_path, target_entry_for_path}; +#[cfg(not(kani))] +use support::path_cmp; +use support::{canonicalize_cycle, path_eq, state_for_path, target_entry_for_path}; #[cfg(test)] #[path = "cycle_tests.rs"] diff --git a/src/ir/cycle_verification.rs b/src/ir/cycle_verification.rs index b13d2ead1..14e3883d9 100644 --- a/src/ir/cycle_verification.rs +++ b/src/ir/cycle_verification.rs @@ -1,5 +1,6 @@ //! Kani harnesses for bounded IR cycle-handling properties. +use super::support::rotate_index; use super::*; /// Prove a self-dependency reports a cycle and no missing dependency. From 8c37f7c89cc3153c44718c2aa83d5ebd4e2758cd Mon Sep 17 00:00:00 2001 From: leynos Date: Sat, 1 Aug 2026 16:21:00 +0200 Subject: [PATCH 03/10] Pass the Polonius flag through to cargo-kani (#445) The Polonius migration (ADR-006) enables `-Zpolonius=next` via `[build] rustflags` in `.cargo/config.toml` and assumed `cargo kani` would inherit it. It does not: cargo-kani sets `CARGO_ENCODED_RUSTFLAGS` itself, which bypasses the config table, so Kani builds borrow-check with plain NLL and fail on the tree's Polonius-dependent code (E0499 in the netsuke lib). Kani appends an inherited `RUSTFLAGS` environment variable to its own flag set, so have the `kani-full` recipe pass `POLONIUS_FLAGS` that way. The `${RUSTFLAGS:+...}` expansion avoids introducing an empty leading flag, which cargo-kani would otherwise forward to rustc as an empty input filename. Correct the ADR-006 bullet and the `.cargo/config.toml` comment that claimed the config table covers `cargo kani`. --- .cargo/config.toml | 8 +++++--- Makefile | 2 +- docs/adr-006-adopt-polonius-nightly-toolchain.md | 9 ++++++--- 3 files changed, 12 insertions(+), 7 deletions(-) diff --git a/.cargo/config.toml b/.cargo/config.toml index fba592bc3..e9e6b7002 100644 --- a/.cargo/config.toml +++ b/.cargo/config.toml @@ -1,10 +1,12 @@ # Enable the Polonius alpha borrow-checking analysis for every Cargo -# invocation, including rust-analyzer and `cargo kani`, so editors and -# verification tooling agree with CI about what borrows are legal. +# invocation, including rust-analyzer, so editors and verification tooling +# agree with CI about what borrows are legal. # # Note: an inherited `RUSTFLAGS` environment variable overrides this table. # Wrappers that set `RUSTFLAGS` (see the Makefile) must re-state -# `-Zpolonius=next` themselves. See +# `-Zpolonius=next` themselves. `cargo kani` sets `CARGO_ENCODED_RUSTFLAGS` +# itself, which also bypasses this table, so the `kani-full` recipe passes +# the flag via `RUSTFLAGS`. See # docs/adr-006-adopt-polonius-nightly-toolchain.md. [build] rustflags = ["-Zpolonius=next"] diff --git a/Makefile b/Makefile index 2ee022cb4..93df45546 100644 --- a/Makefile +++ b/Makefile @@ -146,7 +146,7 @@ kani-check: ## Check the installed Kani verifier version @$(PROVER_TOOLS) kani check-version --kani-command "$(KANI)" $(KANI_CHECK_FLAGS) || { status=$$?; printf 'prover-tools: target=kani-check failed exit=%s\n' "$$status" >&2; exit "$$status"; } kani-full: ## Run the full Kani verification suite - $(KANI) $(KANI_FLAGS) + RUSTFLAGS="$${RUSTFLAGS:+$$RUSTFLAGS }$(POLONIUS_FLAGS)" $(KANI) $(KANI_FLAGS) kani-ir: kani-full ## Run the IR Kani verification suite diff --git a/docs/adr-006-adopt-polonius-nightly-toolchain.md b/docs/adr-006-adopt-polonius-nightly-toolchain.md index de1374fc0..b9e7af7d8 100644 --- a/docs/adr-006-adopt-polonius-nightly-toolchain.md +++ b/docs/adr-006-adopt-polonius-nightly-toolchain.md @@ -39,9 +39,12 @@ Adopt Polonius now, as a nightly-only source tree: - Pin the dated toolchain `nightly-2026-06-25` in `rust-toolchain.toml` so builds stay reproducible. - Enable `-Zpolonius=next` in `.cargo/config.toml` under `[build] rustflags`, - so plain Cargo invocations, rust-analyzer, and `cargo kani` all borrow-check - with the same analysis. Makefile recipes that set `RUSTFLAGS` (which - overrides that table) re-state the flag via the `POLONIUS_FLAGS` variable. + so plain Cargo invocations and rust-analyzer borrow-check with the same + analysis. Makefile recipes that set `RUSTFLAGS` (which overrides that table) + re-state the flag via the `POLONIUS_FLAGS` variable. `cargo kani` sets + `CARGO_ENCODED_RUSTFLAGS` itself, which also bypasses the table, so the + `kani-full` recipe passes the flag through the `RUSTFLAGS` environment + variable, which Kani appends to its own flags. - Collapse the CI matrices in `ci.yml` and `netsukefile-test.yml` to the pinned nightly, and align `coverage-main.yml`. Stable and MSRV legs are removed because the tree no longer compiles without Polonius. From a69d2804bcf3c1cc7d8049ca7739398d1bd41e2f Mon Sep 17 00:00:00 2001 From: leynos Date: Sat, 1 Aug 2026 16:51:16 +0200 Subject: [PATCH 04/10] Assert Kani version check precedes the harness run (#445) Replace the presence-only assertions for `make kani-check` and `make kani-ir` in the kani-smoke contract test with position lookups, and require the version check to appear before the harness step so the fast drift guard keeps running first. --- tests/workflow_ci.rs | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/tests/workflow_ci.rs b/tests/workflow_ci.rs index 808b30ae7..9ef415435 100644 --- a/tests/workflow_ci.rs +++ b/tests/workflow_ci.rs @@ -260,17 +260,17 @@ fn behavioural_ci_workflow_wires_kani_smoke_job() -> Result<()> { .any(|step| step_has(step, StepField::Runs, "make install-kani")), "Kani smoke job should install Kani through the Make target" ); + let kani_check_index = steps + .iter() + .position(|step| step_has(step, StepField::Runs, "make kani-check")) + .context("Kani smoke job should check Kani through the Make target")?; + let kani_ir_index = steps + .iter() + .position(|step| step_has(step, StepField::Runs, "make kani-ir")) + .context("Kani smoke job should run the bounded Kani harnesses through the Make target")?; ensure!( - steps - .iter() - .any(|step| step_has(step, StepField::Runs, "make kani-check")), - "Kani smoke job should check Kani through the Make target" - ); - ensure!( - steps - .iter() - .any(|step| step_has(step, StepField::Runs, "make kani-ir")), - "Kani smoke job should run the bounded Kani harnesses through the Make target" + kani_check_index < kani_ir_index, + "Kani smoke job should check the Kani version before running the bounded harnesses" ); ensure!( mapping_get(kani_job, YamlKey("timeout-minutes")).and_then(Value::as_u64) == Some(20), From 95c98cca65fd5196a215ba238b1a54e80ddde1d6 Mon Sep 17 00:00:00 2001 From: leynos Date: Sun, 2 Aug 2026 09:32:09 +0200 Subject: [PATCH 05/10] Require install, check, run ordering in the kani-smoke test (#445) Replace the presence-only `make install-kani` assertion with a position lookup and extend the ordering assertion so installation precedes the version check, which precedes the bounded harness run. The missing-step error messages are unchanged. --- tests/workflow_ci.rs | 14 ++++++-------- 1 file changed, 6 insertions(+), 8 deletions(-) diff --git a/tests/workflow_ci.rs b/tests/workflow_ci.rs index 9ef415435..a73e07170 100644 --- a/tests/workflow_ci.rs +++ b/tests/workflow_ci.rs @@ -254,12 +254,10 @@ fn behavioural_ci_workflow_wires_kani_smoke_job() -> Result<()> { "Kani smoke job should cache tools using the Kani version and Makefile" ); - ensure!( - steps - .iter() - .any(|step| step_has(step, StepField::Runs, "make install-kani")), - "Kani smoke job should install Kani through the Make target" - ); + let install_kani_index = steps + .iter() + .position(|step| step_has(step, StepField::Runs, "make install-kani")) + .context("Kani smoke job should install Kani through the Make target")?; let kani_check_index = steps .iter() .position(|step| step_has(step, StepField::Runs, "make kani-check")) @@ -269,8 +267,8 @@ fn behavioural_ci_workflow_wires_kani_smoke_job() -> Result<()> { .position(|step| step_has(step, StepField::Runs, "make kani-ir")) .context("Kani smoke job should run the bounded Kani harnesses through the Make target")?; ensure!( - kani_check_index < kani_ir_index, - "Kani smoke job should check the Kani version before running the bounded harnesses" + install_kani_index < kani_check_index && kani_check_index < kani_ir_index, + "Kani smoke job should install Kani, check its version, then run the bounded harnesses" ); ensure!( mapping_get(kani_job, YamlKey("timeout-minutes")).and_then(Value::as_u64) == Some(20), From 2bc38a30e50b8b70dd9f84ce3dbe2b82b9993e53 Mon Sep 17 00:00:00 2001 From: leynos Date: Sun, 2 Aug 2026 09:32:09 +0200 Subject: [PATCH 06/10] Preserve inherited RUSTFLAGS in warning-denying recipes (#445) The nextest, doctest, clippy, whitaker, and typecheck recipes replaced any caller-supplied `RUSTFLAGS` with `-D warnings -Zpolonius=next`, silently dropping caller flags. Prepend the inherited value using the same `$${RUSTFLAGS:+$$RUSTFLAGS }` expansion the `kani-full` recipe uses, and update the `make test` contract test to pin the new shape. --- Makefile | 10 +++++----- tests/makefile_test_target.rs | 15 +++++++++------ 2 files changed, 14 insertions(+), 11 deletions(-) diff --git a/Makefile b/Makefile index 93df45546..c56203d07 100644 --- a/Makefile +++ b/Makefile @@ -80,10 +80,10 @@ clean: ## Remove build artefacts test: test-nextest doctest ## Run every Rust test with warnings treated as errors test-nextest: ## Run all non-doctest Rust tests through cargo-nextest - RUSTFLAGS="-D warnings $(POLONIUS_FLAGS)" $(CARGO) nextest run --all-targets --all-features $(NEXTEST_BUILD_JOBS) + RUSTFLAGS="$${RUSTFLAGS:+$$RUSTFLAGS }-D warnings $(POLONIUS_FLAGS)" $(CARGO) nextest run --all-targets --all-features $(NEXTEST_BUILD_JOBS) doctest: ## Run doctests, which cargo-nextest cannot execute - RUSTFLAGS="-D warnings $(POLONIUS_FLAGS)" $(CARGO) test --doc --all-features $(BUILD_JOBS) + RUSTFLAGS="$${RUSTFLAGS:+$$RUSTFLAGS }-D warnings $(POLONIUS_FLAGS)" $(CARGO) test --doc --all-features $(BUILD_JOBS) test-workflow-contracts: ## Validate the mutation-testing caller contract uv run --with 'pytest>=8' --with 'pyyaml>=6' pytest tests/workflow_contracts -q @@ -97,10 +97,10 @@ lint: lint-clippy lint-whitaker ## Run Clippy and the Whitaker Dylint suite with lint-clippy: ## Run rustdoc and Clippy with warnings denied RUSTDOCFLAGS="$(RUSTDOC_FLAGS)" RUSTFLAGS="$${RUSTFLAGS-} $(POLONIUS_FLAGS)" $(CARGO) doc --no-deps - RUSTFLAGS="-D warnings $(POLONIUS_FLAGS)" $(CARGO) clippy $(CLIPPY_FLAGS) + RUSTFLAGS="$${RUSTFLAGS:+$$RUSTFLAGS }-D warnings $(POLONIUS_FLAGS)" $(CARGO) clippy $(CLIPPY_FLAGS) lint-whitaker: ## Run the Whitaker Dylint suite with warnings denied - RUSTFLAGS="-D warnings $(POLONIUS_FLAGS)" $(WHITAKER) --all -- --all-targets --all-features + RUSTFLAGS="$${RUSTFLAGS:+$$RUSTFLAGS }-D warnings $(POLONIUS_FLAGS)" $(WHITAKER) --all -- --all-targets --all-features fmt: ## Format Rust and Markdown sources $(CARGO) fmt --all @@ -110,7 +110,7 @@ check-fmt: ## Verify formatting $(CARGO) fmt --all -- --check typecheck: ## Typecheck all targets and features - RUSTFLAGS="-D warnings $(POLONIUS_FLAGS)" $(CARGO) check --all-targets --all-features $(BUILD_JOBS) + RUSTFLAGS="$${RUSTFLAGS:+$$RUSTFLAGS }-D warnings $(POLONIUS_FLAGS)" $(CARGO) check --all-targets --all-features $(BUILD_JOBS) markdownlint: spelling ## Lint Markdown and enforce en-GB-oxendict spelling $(MDLINT) "**/*.md" diff --git a/tests/makefile_test_target.rs b/tests/makefile_test_target.rs index 26551f62f..81f6fbf47 100644 --- a/tests/makefile_test_target.rs +++ b/tests/makefile_test_target.rs @@ -3,10 +3,11 @@ //! `make test` is the single command local development and continuous //! integration (CI) both run. These tests pin the runner contract it encodes: //! non-doctest tests go through cargo-nextest, doctests run separately because -//! nextest cannot execute them, and both passes deny warnings and re-state -//! the Polonius flag that an inherited RUSTFLAGS would otherwise strip. They also assert -//! that the checked-in nextest configuration still declares the narrow -//! serialisation group the environment-mutating suites depend on. +//! nextest cannot execute them, and both passes preserve any inherited +//! RUSTFLAGS while denying warnings and re-stating the Polonius flag that +//! setting RUSTFLAGS would otherwise strip. They also assert that the +//! checked-in nextest configuration still declares the narrow serialisation +//! group the environment-mutating suites depend on. use anyhow::{Context, Result, ensure}; use camino::Utf8Path; @@ -125,7 +126,8 @@ fn behavioural_make_test_composes_the_nextest_and_doctest_passes() -> Result<()> "test-nextest should enable all features, found {nextest_recipe:?}" ); ensure!( - nextest_recipe.contains(r#"RUSTFLAGS="-D warnings $(POLONIUS_FLAGS)""#), + nextest_recipe + .contains(r#"RUSTFLAGS="$${RUSTFLAGS:+$$RUSTFLAGS }-D warnings $(POLONIUS_FLAGS)""#), "test-nextest should deny warnings and enable Polonius, found {nextest_recipe:?}" ); @@ -140,7 +142,8 @@ fn behavioural_make_test_composes_the_nextest_and_doctest_passes() -> Result<()> "doctests cannot run under nextest, found {doctest_recipe:?}" ); ensure!( - doctest_recipe.contains(r#"RUSTFLAGS="-D warnings $(POLONIUS_FLAGS)""#), + doctest_recipe + .contains(r#"RUSTFLAGS="$${RUSTFLAGS:+$$RUSTFLAGS }-D warnings $(POLONIUS_FLAGS)""#), "doctest should deny warnings and enable Polonius, found {doctest_recipe:?}" ); Ok(()) From 49160e1a0019ef71c8fc4144a18c15817da07b2b Mon Sep 17 00:00:00 2001 From: leynos Date: Sun, 2 Aug 2026 14:45:07 +0200 Subject: [PATCH 07/10] Use sentence case in the ADR-006 heading (#445) `docs/documentation-style-guide.md` requires headings in sentence case. Lower-case "Decision Record" in the title, keeping `ADR` and `Polonius` capitalized. --- docs/adr-006-adopt-polonius-nightly-toolchain.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/adr-006-adopt-polonius-nightly-toolchain.md b/docs/adr-006-adopt-polonius-nightly-toolchain.md index b9e7af7d8..1618dd215 100644 --- a/docs/adr-006-adopt-polonius-nightly-toolchain.md +++ b/docs/adr-006-adopt-polonius-nightly-toolchain.md @@ -1,4 +1,4 @@ -# Architecture Decision Record (ADR): Adopt the Polonius borrow checker on a pinned nightly toolchain +# Architecture decision record (ADR): Adopt the Polonius borrow checker on a pinned nightly toolchain ## Status From ff58913de1cef4e4007cbdb95da82126f28bf7cb Mon Sep 17 00:00:00 2001 From: leynos Date: Sun, 2 Aug 2026 14:51:58 +0200 Subject: [PATCH 08/10] Document the completed Kani smoke CI work (#445) Reconcile the formal-verification documentation with the state of the repository now that the bounded harness suite runs on pull requests. - Append a dated addendum to the completed `4.1.2` ExecPlan recording the follow-up work. The plan as executed is left byte-for-byte intact. - Update the living formal-verification design document: `kani-check` is no longer described as a placeholder "until substantive Kani harnesses exist", and the `kani-smoke` job entry now records that it is pull-request-only, runs `make kani-ir` after `make kani-check`, covers 13 harnesses, and is bounded by `timeout-minutes: 20`. - Document in the developers' guide that the recipes adding `-D warnings` and `$(POLONIUS_FLAGS)` prepend any caller-supplied `RUSTFLAGS` via `$${RUSTFLAGS:+$$RUSTFLAGS }`, replacing a stale literal that predated the preservation fix. The roadmap already records `4.1.2` accurately, so it is unchanged. No CI, Makefile, or source behaviour is affected. --- docs/developers-guide.md | 22 +++++++++++++------ docs/execplans/4-1-2-kani-smoke-ci-job.md | 16 ++++++++++++++ .../formal-verification-methods-in-netsuke.md | 16 +++++++++----- 3 files changed, 42 insertions(+), 12 deletions(-) diff --git a/docs/developers-guide.md b/docs/developers-guide.md index 95cfc3e60..f033aff83 100644 --- a/docs/developers-guide.md +++ b/docs/developers-guide.md @@ -82,10 +82,16 @@ Netsuke builds on the dated nightly toolchain pinned in `rust-toolchain.toml` with the Polonius alpha borrow-checking analysis (`-Zpolonius=next`) enabled. `rustup` provisions the toolchain automatically, and `.cargo/config.toml` supplies the flag by default, covering Cargo invocations such as rust-analyzer -and `cargo kani` that run without `RUSTFLAGS` in the environment. Makefile -recipes that set `RUSTFLAGS` re-state the flag through the `POLONIUS_FLAGS` -variable because an inherited `RUSTFLAGS` environment variable overrides -`.cargo/config.toml`. +that run without `RUSTFLAGS` in the environment. Makefile recipes that set +`RUSTFLAGS` re-state the flag through the `POLONIUS_FLAGS` variable because an +inherited `RUSTFLAGS` environment variable overrides `.cargo/config.toml`. The +recipes that add `-D warnings` and `$(POLONIUS_FLAGS)` build the value as +`RUSTFLAGS="$${RUSTFLAGS:+$$RUSTFLAGS }-D warnings $(POLONIUS_FLAGS)"`; the +`$${RUSTFLAGS:+$$RUSTFLAGS }` expansion prepends any `RUSTFLAGS` already set by +the caller (for example a CI wrapper), so those flags survive rather than being +silently discarded. `cargo kani` sets `CARGO_ENCODED_RUSTFLAGS` itself, which +also overrides the table, so `make kani-full` passes the flag through +`RUSTFLAGS` as well. [ADR-006](adr-006-adopt-polonius-nightly-toolchain.md) records the policy decision, and the [polonius migration notes](polonius.md) track every site @@ -860,9 +866,11 @@ home plus Kani support-file home. - `make test-nextest` — `cargo nextest run --all-targets --all-features`, with - `RUSTFLAGS="-D warnings $(POLONIUS_FLAGS)"` (the Makefile re-states the - Polonius flag because a set `RUSTFLAGS` overrides `.cargo/config.toml`). This - runs every unit, integration, `rstest`, and `rstest-bdd` test. + `RUSTFLAGS="$${RUSTFLAGS:+$$RUSTFLAGS }-D warnings $(POLONIUS_FLAGS)"` (the + Makefile re-states the Polonius flag because a set `RUSTFLAGS` overrides + `.cargo/config.toml`, and the `$${RUSTFLAGS:+$$RUSTFLAGS }` prefix preserves + any `RUSTFLAGS` inherited from the caller). This runs every unit, + integration, `rstest`, and `rstest-bdd` test. - `make doctest` — `cargo test --doc --all-features`, with the same `RUSTFLAGS`. nextest cannot execute doctests, so they need their own pass. Note that the previous `cargo test --all-targets` invocation never ran diff --git a/docs/execplans/4-1-2-kani-smoke-ci-job.md b/docs/execplans/4-1-2-kani-smoke-ci-job.md index d903256c7..62db234c9 100644 --- a/docs/execplans/4-1-2-kani-smoke-ci-job.md +++ b/docs/execplans/4-1-2-kani-smoke-ci-job.md @@ -569,3 +569,19 @@ The references section should include: - Lody session: ``` + +## Addendum: 2026-08-02 — bounded harness wiring completed + +The bounded Kani harness work deferred at the time of this ExecPlan's +execution has since been completed, in follow-up work tracked as +[issue #445](https://github.com/leynos/netsuke/issues/445). The pull-request +`kani-smoke` job now runs `make kani-check` (the pinned-version drift guard) +and then `make kani-ir` (the bounded harness suite), after +`make install-kani`. The `kani-smoke` job declares `timeout-minutes: 20`. The +bounded suite contains 13 `#[kani::proof]` harnesses: 4 in +`src/ir/from_manifest_verification.rs` and 9 in +`src/ir/cycle_verification.rs`. +[Pull request #470](https://github.com/leynos/netsuke/pull/470) carries the +implementation and declares `Closes #445`; the issue itself remains open at +the time of writing and closes on merge. This addendum records later work and +does not amend the plan as executed. diff --git a/docs/formal-verification-methods-in-netsuke.md b/docs/formal-verification-methods-in-netsuke.md index d6605ba05..41b0843fa 100644 --- a/docs/formal-verification-methods-in-netsuke.md +++ b/docs/formal-verification-methods-in-netsuke.md @@ -216,8 +216,10 @@ development and continuous integration. These pins serve several purposes: The first formal-verification commands should extend the existing `Makefile` without disturbing the current developer workflow.[^2] -- `make kani-check` should run the fast installed-version check suitable for - pull requests until substantive Kani harnesses exist. +- `make kani-check` should run the fast pinned-version drift guard suitable + for pull requests. +- The bounded Kani harness suite now also runs on pull requests through + `make kani-ir`. - `make kani-full` should run the full Kani suite. - `make install-kani` should install the pinned Kani version through `rust-prover-tools`. @@ -236,12 +238,16 @@ 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 first additional job should be a dedicated `kani-smoke` job that: +The `kani-smoke` job is a dedicated, pull-request-only job (it runs only when +`github.event_name == 'pull_request'`) that: - installs `uv` and then installs the pinned Kani toolchain through `make install-kani`, -- runs `make kani-check`, and -- caches tool downloads separately from the ordinary Rust build artefacts. +- runs `make kani-check` and then the bounded harness suite through + `make kani-ir` (13 harnesses across the manifest-verification and + cycle-verification modules), +- caches tool downloads separately from the ordinary Rust build artefacts, and +- is bounded by a 20-minute job timeout (`timeout-minutes: 20`). Any later Verus job should be added only after a stable proof kernel exists. From 2124851dbccb17f4b92a948f4a521983064f4265 Mon Sep 17 00:00:00 2001 From: leynos Date: Sun, 2 Aug 2026 21:43:39 +0200 Subject: [PATCH 09/10] Cover RUSTFLAGS composition in every changed recipe (#445) Preserving inherited `RUSTFLAGS` touched six recipes, but the only coverage was a literal text match in the `make test` contract test for `test-nextest` and `doctest`. That left `lint-clippy`, `lint-whitaker`, `typecheck`, and `kani-full` unguarded, and text matching cannot detect a broken expansion in any case. Add `tests/makefile_rustflags_tests.rs`, which runs each recipe with a stub standing in for the command it invokes (via the `CARGO`, `WHITAKER`, and `KANI` variables) and asserts on the `RUSTFLAGS` the stub actually observes. Two properties are checked per recipe: - an inherited `RUSTFLAGS` is prepended, and the Polonius flag (plus `-D warnings`, where the recipe adds it) still reaches the command; - an unset `RUSTFLAGS` produces no leading separator. Both are needed. Reverting a recipe to the clobbering form fails only the first; rewriting the expansion as a naive `$RUSTFLAGS ` prepend fails only the second. `kani-full` is covered too, and is the one case expected not to add `-D warnings`. The new crate stages its stub through an ambient tempdir, so it joins the sanctioned integration-test entries in `dylint.toml`. --- dylint.toml | 1 + tests/makefile_rustflags_tests.rs | 248 ++++++++++++++++++++++++++++++ 2 files changed, 249 insertions(+) create mode 100644 tests/makefile_rustflags_tests.rs diff --git a/dylint.toml b/dylint.toml index f0b565322..6ea6bd371 100644 --- a/dylint.toml +++ b/dylint.toml @@ -69,6 +69,7 @@ excluded_crates = [ "test_support", "advanced_usage_tests", "assert_cmd_tests", + "makefile_rustflags_tests", "manifest_glob_tests", "ninja_snapshot_tests", "novice_flow_smoke_tests", diff --git a/tests/makefile_rustflags_tests.rs b/tests/makefile_rustflags_tests.rs new file mode 100644 index 000000000..88f4d3b26 --- /dev/null +++ b/tests/makefile_rustflags_tests.rs @@ -0,0 +1,248 @@ +//! Behavioural tests for `RUSTFLAGS` composition in Makefile recipes. +//! +//! Several recipes set `RUSTFLAGS` so they can add `-D warnings` and the +//! Polonius flag. Setting `RUSTFLAGS` at all overrides the `[build] rustflags` +//! table in `.cargo/config.toml`, which is why each recipe re-states +//! `-Zpolonius=next`, and why each prepends any value the caller already +//! exported instead of discarding it. +//! +//! Matching the recipe text would only prove the Makefile still spells the +//! expansion the same way. These tests instead run each recipe with a stub +//! standing in for the command it invokes, and assert on the `RUSTFLAGS` that +//! stub actually observes, so a broken expansion fails here rather than in CI. + +#![cfg(unix)] + +use anyhow::{Context, Result, ensure}; +use rstest::rstest; +use std::fs; +use std::path::PathBuf; +use std::process::Command; +use tempfile::{TempDir, tempdir}; +use test_support::exec::write_exec_with_content; + +/// A `RUSTFLAGS`-setting recipe under test. +#[derive(Copy, Clone, Debug)] +struct RecipeCase { + /// The Make target to run. + target: &'static str, + /// The Make variable naming the command the recipe invokes, so the test + /// can substitute a stub for it. + command_variable: &'static str, + /// Substring selecting the invocation under test. `lint-clippy` drives + /// `$(CARGO)` twice, so its Clippy line must be picked out by argument. + /// An empty marker matches a recipe's sole invocation. + invocation_marker: &'static str, + /// Whether the recipe adds `-D warnings`. `kani-full` deliberately does + /// not: Kani compiles third-party crates that the workspace lints do not + /// govern. + denies_warnings: bool, +} + +impl RecipeCase { + const fn test_nextest() -> Self { + Self { + target: "test-nextest", + command_variable: "CARGO", + invocation_marker: "nextest run", + denies_warnings: true, + } + } + + const fn doctest() -> Self { + Self { + target: "doctest", + command_variable: "CARGO", + invocation_marker: "test --doc", + denies_warnings: true, + } + } + + const fn lint_clippy() -> Self { + Self { + target: "lint-clippy", + command_variable: "CARGO", + invocation_marker: "clippy", + denies_warnings: true, + } + } + + const fn lint_whitaker() -> Self { + Self { + target: "lint-whitaker", + command_variable: "WHITAKER", + invocation_marker: "--all", + denies_warnings: true, + } + } + + const fn typecheck() -> Self { + Self { + target: "typecheck", + command_variable: "CARGO", + invocation_marker: "check --all-targets", + denies_warnings: true, + } + } + + const fn kani_full() -> Self { + Self { + target: "kani-full", + command_variable: "KANI", + invocation_marker: "", + denies_warnings: false, + } + } +} + +/// A stub executable that records the `RUSTFLAGS` each invocation observes. +struct StubCommand { + _temp: TempDir, + executable: PathBuf, + log: PathBuf, +} + +impl StubCommand { + fn new() -> Result { + let temp = tempdir().context("create stub command directory")?; + let log = temp.path().join("invocations.log"); + // Each line is the invocation's arguments and its `RUSTFLAGS`, + // separated by a tab. + let script = format!( + r#"#!/bin/sh +printf '%s\t%s\n' "$*" "${{RUSTFLAGS-}}" >> '{log}' +exit 0 +"#, + log = log.display() + ); + let executable = write_exec_with_content(temp.path(), "stub-command", &script) + .context("write stub command")?; + + Ok(Self { + _temp: temp, + executable, + log, + }) + } + + /// Returns the `RUSTFLAGS` seen by the invocation matching `marker`. + fn observed_rustflags(&self, marker: &str) -> Result { + let log = fs::read_to_string(&self.log) + .with_context(|| format!("read {}", self.log.display()))?; + log.lines() + .filter_map(|line| line.split_once('\t')) + .find(|(arguments, _)| arguments.contains(marker)) + .map(|(_, flags)| flags.to_owned()) + .with_context(|| format!("no stub invocation matched {marker:?}, log was {log:?}")) + } +} + +const CALLER_FLAG: &str = "--cfg=caller_supplied_marker"; +const POLONIUS_FLAG: &str = "-Zpolonius=next"; +const DENY_WARNINGS: &str = "-D warnings"; + +/// Runs `case.target`, substituting the stub for the command it invokes. +/// +/// `inherited` is exported to `make` as the caller's `RUSTFLAGS`; `None` +/// removes the variable so the unset branch of the expansion is exercised. +fn run_recipe(stub: &StubCommand, case: RecipeCase, inherited: Option<&str>) -> Result<()> { + let mut command = Command::new("make"); + command + .arg("--no-print-directory") + .arg("-f") + .arg("Makefile") + .arg(format!( + "{}={}", + case.command_variable, + stub.executable.display() + )) + .arg(case.target) + .env_remove("RUSTFLAGS"); + if let Some(value) = inherited { + command.env("RUSTFLAGS", value); + } + + let output = command + .output() + .with_context(|| format!("run make {}", case.target))?; + ensure!( + output.status.success(), + "make {} should succeed: {}", + case.target, + String::from_utf8_lossy(&output.stderr) + ); + Ok(()) +} + +#[rstest] +#[case(RecipeCase::test_nextest())] +#[case(RecipeCase::doctest())] +#[case(RecipeCase::lint_clippy())] +#[case(RecipeCase::lint_whitaker())] +#[case(RecipeCase::typecheck())] +#[case(RecipeCase::kani_full())] +fn behavioural_recipes_prepend_inherited_rustflags(#[case] case: RecipeCase) -> Result<()> { + let stub = StubCommand::new()?; + run_recipe(&stub, case, Some(CALLER_FLAG))?; + let observed = stub.observed_rustflags(case.invocation_marker)?; + + ensure!( + observed.starts_with(&format!("{CALLER_FLAG} ")), + "make {} should prepend the caller's RUSTFLAGS, observed {observed:?}", + case.target + ); + ensure!( + observed.contains(POLONIUS_FLAG), + "make {} should re-state {POLONIUS_FLAG} because setting RUSTFLAGS \ + overrides .cargo/config.toml, observed {observed:?}", + case.target + ); + ensure!( + observed.contains(DENY_WARNINGS) == case.denies_warnings, + "make {} should {} deny warnings, observed {observed:?}", + case.target, + if case.denies_warnings { "" } else { "not" } + ); + Ok(()) +} + +#[rstest] +#[case(RecipeCase::test_nextest())] +#[case(RecipeCase::doctest())] +#[case(RecipeCase::lint_clippy())] +#[case(RecipeCase::lint_whitaker())] +#[case(RecipeCase::typecheck())] +#[case(RecipeCase::kani_full())] +fn behavioural_recipes_add_no_separator_without_inherited_rustflags( + #[case] case: RecipeCase, +) -> Result<()> { + let stub = StubCommand::new()?; + run_recipe(&stub, case, None)?; + let observed = stub.observed_rustflags(case.invocation_marker)?; + + // The `:+` expansion contributes the separator only alongside a value, so + // an unset `RUSTFLAGS` must not leave a leading space. + ensure!( + !observed.starts_with(' '), + "make {} should not emit a leading separator when RUSTFLAGS is unset, \ + observed {observed:?}", + case.target + ); + let expected_first = if case.denies_warnings { + DENY_WARNINGS + } else { + POLONIUS_FLAG + }; + ensure!( + observed.starts_with(expected_first), + "make {} should start with {expected_first:?} when RUSTFLAGS is unset, \ + observed {observed:?}", + case.target + ); + ensure!( + observed.contains(POLONIUS_FLAG), + "make {} should re-state {POLONIUS_FLAG}, observed {observed:?}", + case.target + ); + Ok(()) +} From 5c9d7357878e908e413d78c2f9e0741692f2feed Mon Sep 17 00:00:00 2001 From: leynos Date: Mon, 3 Aug 2026 00:34:14 +0200 Subject: [PATCH 10/10] Put every RUSTFLAGS-setting recipe under contract (#445) Preserving inherited `RUSTFLAGS` touched six recipes, but only `test-nextest` and `doctest` were covered, and only by matching the recipe text. Text matching proves the Makefile still spells the expansion a certain way, not that it behaves correctly. Extend `tests/makefile_test_target.rs` to cover all eight recipe lines that set `RUSTFLAGS`. Each case extracts the assignment, resolves the Make variables it names, and expands it in a shell with a caller value of `-C target-cpu=native`. Only the assignment is expanded; the command the recipe would run is never executed, so no Cargo, Kani, nextest, or Dylint invocation is involved. Every case asserts the caller's value survives and the Polonius flag is re-stated. `lint-clippy`'s Clippy line, `lint-whitaker`, and `typecheck` join `test-nextest` and `doctest` in asserting `-D warnings`; `kani-full` asserts its absence, matching the recipe. The binary-build recipe and `lint-clippy`'s rustdoc line preserve the caller's value through the `$${RUSTFLAGS-}` spelling and are covered too. A guard test fails if a recipe starts setting `RUSTFLAGS` without a matching case, so the coverage cannot silently fall behind. Assertions target flag semantics rather than whole recipe strings, so they survive unrelated changes to the command a recipe runs. The "separator only when set" property is declared by each case rather than read back from the Makefile: inferring it would let a rewrite to a bare `$RUSTFLAGS ` prefix delete the assertion along with the idiom. This replaces `tests/makefile_rustflags_tests.rs`, which drove `make` with stub commands, and with it the `dylint.toml` exclusion that test's ambient tempdir required. --- dylint.toml | 1 - tests/makefile_rustflags_tests.rs | 248 -------------------- tests/makefile_test_target.rs | 361 +++++++++++++++++++++++++++++- 3 files changed, 354 insertions(+), 256 deletions(-) delete mode 100644 tests/makefile_rustflags_tests.rs diff --git a/dylint.toml b/dylint.toml index 6ea6bd371..f0b565322 100644 --- a/dylint.toml +++ b/dylint.toml @@ -69,7 +69,6 @@ excluded_crates = [ "test_support", "advanced_usage_tests", "assert_cmd_tests", - "makefile_rustflags_tests", "manifest_glob_tests", "ninja_snapshot_tests", "novice_flow_smoke_tests", diff --git a/tests/makefile_rustflags_tests.rs b/tests/makefile_rustflags_tests.rs deleted file mode 100644 index 88f4d3b26..000000000 --- a/tests/makefile_rustflags_tests.rs +++ /dev/null @@ -1,248 +0,0 @@ -//! Behavioural tests for `RUSTFLAGS` composition in Makefile recipes. -//! -//! Several recipes set `RUSTFLAGS` so they can add `-D warnings` and the -//! Polonius flag. Setting `RUSTFLAGS` at all overrides the `[build] rustflags` -//! table in `.cargo/config.toml`, which is why each recipe re-states -//! `-Zpolonius=next`, and why each prepends any value the caller already -//! exported instead of discarding it. -//! -//! Matching the recipe text would only prove the Makefile still spells the -//! expansion the same way. These tests instead run each recipe with a stub -//! standing in for the command it invokes, and assert on the `RUSTFLAGS` that -//! stub actually observes, so a broken expansion fails here rather than in CI. - -#![cfg(unix)] - -use anyhow::{Context, Result, ensure}; -use rstest::rstest; -use std::fs; -use std::path::PathBuf; -use std::process::Command; -use tempfile::{TempDir, tempdir}; -use test_support::exec::write_exec_with_content; - -/// A `RUSTFLAGS`-setting recipe under test. -#[derive(Copy, Clone, Debug)] -struct RecipeCase { - /// The Make target to run. - target: &'static str, - /// The Make variable naming the command the recipe invokes, so the test - /// can substitute a stub for it. - command_variable: &'static str, - /// Substring selecting the invocation under test. `lint-clippy` drives - /// `$(CARGO)` twice, so its Clippy line must be picked out by argument. - /// An empty marker matches a recipe's sole invocation. - invocation_marker: &'static str, - /// Whether the recipe adds `-D warnings`. `kani-full` deliberately does - /// not: Kani compiles third-party crates that the workspace lints do not - /// govern. - denies_warnings: bool, -} - -impl RecipeCase { - const fn test_nextest() -> Self { - Self { - target: "test-nextest", - command_variable: "CARGO", - invocation_marker: "nextest run", - denies_warnings: true, - } - } - - const fn doctest() -> Self { - Self { - target: "doctest", - command_variable: "CARGO", - invocation_marker: "test --doc", - denies_warnings: true, - } - } - - const fn lint_clippy() -> Self { - Self { - target: "lint-clippy", - command_variable: "CARGO", - invocation_marker: "clippy", - denies_warnings: true, - } - } - - const fn lint_whitaker() -> Self { - Self { - target: "lint-whitaker", - command_variable: "WHITAKER", - invocation_marker: "--all", - denies_warnings: true, - } - } - - const fn typecheck() -> Self { - Self { - target: "typecheck", - command_variable: "CARGO", - invocation_marker: "check --all-targets", - denies_warnings: true, - } - } - - const fn kani_full() -> Self { - Self { - target: "kani-full", - command_variable: "KANI", - invocation_marker: "", - denies_warnings: false, - } - } -} - -/// A stub executable that records the `RUSTFLAGS` each invocation observes. -struct StubCommand { - _temp: TempDir, - executable: PathBuf, - log: PathBuf, -} - -impl StubCommand { - fn new() -> Result { - let temp = tempdir().context("create stub command directory")?; - let log = temp.path().join("invocations.log"); - // Each line is the invocation's arguments and its `RUSTFLAGS`, - // separated by a tab. - let script = format!( - r#"#!/bin/sh -printf '%s\t%s\n' "$*" "${{RUSTFLAGS-}}" >> '{log}' -exit 0 -"#, - log = log.display() - ); - let executable = write_exec_with_content(temp.path(), "stub-command", &script) - .context("write stub command")?; - - Ok(Self { - _temp: temp, - executable, - log, - }) - } - - /// Returns the `RUSTFLAGS` seen by the invocation matching `marker`. - fn observed_rustflags(&self, marker: &str) -> Result { - let log = fs::read_to_string(&self.log) - .with_context(|| format!("read {}", self.log.display()))?; - log.lines() - .filter_map(|line| line.split_once('\t')) - .find(|(arguments, _)| arguments.contains(marker)) - .map(|(_, flags)| flags.to_owned()) - .with_context(|| format!("no stub invocation matched {marker:?}, log was {log:?}")) - } -} - -const CALLER_FLAG: &str = "--cfg=caller_supplied_marker"; -const POLONIUS_FLAG: &str = "-Zpolonius=next"; -const DENY_WARNINGS: &str = "-D warnings"; - -/// Runs `case.target`, substituting the stub for the command it invokes. -/// -/// `inherited` is exported to `make` as the caller's `RUSTFLAGS`; `None` -/// removes the variable so the unset branch of the expansion is exercised. -fn run_recipe(stub: &StubCommand, case: RecipeCase, inherited: Option<&str>) -> Result<()> { - let mut command = Command::new("make"); - command - .arg("--no-print-directory") - .arg("-f") - .arg("Makefile") - .arg(format!( - "{}={}", - case.command_variable, - stub.executable.display() - )) - .arg(case.target) - .env_remove("RUSTFLAGS"); - if let Some(value) = inherited { - command.env("RUSTFLAGS", value); - } - - let output = command - .output() - .with_context(|| format!("run make {}", case.target))?; - ensure!( - output.status.success(), - "make {} should succeed: {}", - case.target, - String::from_utf8_lossy(&output.stderr) - ); - Ok(()) -} - -#[rstest] -#[case(RecipeCase::test_nextest())] -#[case(RecipeCase::doctest())] -#[case(RecipeCase::lint_clippy())] -#[case(RecipeCase::lint_whitaker())] -#[case(RecipeCase::typecheck())] -#[case(RecipeCase::kani_full())] -fn behavioural_recipes_prepend_inherited_rustflags(#[case] case: RecipeCase) -> Result<()> { - let stub = StubCommand::new()?; - run_recipe(&stub, case, Some(CALLER_FLAG))?; - let observed = stub.observed_rustflags(case.invocation_marker)?; - - ensure!( - observed.starts_with(&format!("{CALLER_FLAG} ")), - "make {} should prepend the caller's RUSTFLAGS, observed {observed:?}", - case.target - ); - ensure!( - observed.contains(POLONIUS_FLAG), - "make {} should re-state {POLONIUS_FLAG} because setting RUSTFLAGS \ - overrides .cargo/config.toml, observed {observed:?}", - case.target - ); - ensure!( - observed.contains(DENY_WARNINGS) == case.denies_warnings, - "make {} should {} deny warnings, observed {observed:?}", - case.target, - if case.denies_warnings { "" } else { "not" } - ); - Ok(()) -} - -#[rstest] -#[case(RecipeCase::test_nextest())] -#[case(RecipeCase::doctest())] -#[case(RecipeCase::lint_clippy())] -#[case(RecipeCase::lint_whitaker())] -#[case(RecipeCase::typecheck())] -#[case(RecipeCase::kani_full())] -fn behavioural_recipes_add_no_separator_without_inherited_rustflags( - #[case] case: RecipeCase, -) -> Result<()> { - let stub = StubCommand::new()?; - run_recipe(&stub, case, None)?; - let observed = stub.observed_rustflags(case.invocation_marker)?; - - // The `:+` expansion contributes the separator only alongside a value, so - // an unset `RUSTFLAGS` must not leave a leading space. - ensure!( - !observed.starts_with(' '), - "make {} should not emit a leading separator when RUSTFLAGS is unset, \ - observed {observed:?}", - case.target - ); - let expected_first = if case.denies_warnings { - DENY_WARNINGS - } else { - POLONIUS_FLAG - }; - ensure!( - observed.starts_with(expected_first), - "make {} should start with {expected_first:?} when RUSTFLAGS is unset, \ - observed {observed:?}", - case.target - ); - ensure!( - observed.contains(POLONIUS_FLAG), - "make {} should re-state {POLONIUS_FLAG}, observed {observed:?}", - case.target - ); - Ok(()) -} diff --git a/tests/makefile_test_target.rs b/tests/makefile_test_target.rs index 81f6fbf47..ce8029ec5 100644 --- a/tests/makefile_test_target.rs +++ b/tests/makefile_test_target.rs @@ -1,17 +1,34 @@ -//! Contract tests for the canonical `make test` entry point. +//! Contract tests for the canonical `make test` entry point and for every +//! Makefile recipe that overrides `RUSTFLAGS`. //! //! `make test` is the single command local development and continuous //! integration (CI) both run. These tests pin the runner contract it encodes: -//! non-doctest tests go through cargo-nextest, doctests run separately because -//! nextest cannot execute them, and both passes preserve any inherited -//! RUSTFLAGS while denying warnings and re-stating the Polonius flag that -//! setting RUSTFLAGS would otherwise strip. They also assert that the -//! checked-in nextest configuration still declares the narrow serialisation -//! group the environment-mutating suites depend on. +//! non-doctest tests go through cargo-nextest, and doctests run separately +//! because nextest cannot execute them. +//! +//! They also pin the `RUSTFLAGS` contract shared by every recipe that sets the +//! variable. Setting `RUSTFLAGS` at all overrides the `[build] rustflags` +//! table in `.cargo/config.toml`, so each such recipe re-states the Polonius +//! flag, and each prepends any value the caller already exported rather than +//! discarding it. `test-nextest`, `doctest`, `lint-clippy`'s Clippy line, +//! `lint-whitaker`, and `typecheck` additionally add `-D warnings`; +//! `kani-full` adds only the Polonius flag, because Kani compiles third-party +//! crates the workspace lint policy does not govern. The binary-build recipe +//! and `lint-clippy`'s rustdoc line preserve the caller's value through a +//! different expansion and add neither `-D warnings` nor anything else. +//! +//! The `RUSTFLAGS` tests extract each assignment from the Makefile, resolve +//! the Make variables it names, and expand the result in a shell. They assert +//! on the flags that expansion yields rather than on recipe text, so they stay +//! valid when the command a recipe runs changes. A guard test fails if a +//! recipe starts setting `RUSTFLAGS` without joining the covered set. use anyhow::{Context, Result, ensure}; use camino::Utf8Path; use cap_std::{ambient_authority, fs_utf8::Dir}; +use rstest::rstest; +use std::collections::BTreeSet; +use std::process::Command; use toml::Value; /// Opens the repository root as a capability-scoped directory handle. @@ -149,6 +166,336 @@ fn behavioural_make_test_composes_the_nextest_and_doctest_passes() -> Result<()> Ok(()) } +/// The prefix introducing a quoted `RUSTFLAGS` assignment in a recipe. +const RUSTFLAGS_PREFIX: &str = "RUSTFLAGS=\""; + +/// A value a caller might already have exported before invoking `make`. +const CALLER_RUSTFLAGS: &str = "-C target-cpu=native"; + +const DENY_WARNINGS: &str = "-D warnings"; + +/// A recipe line that overrides `RUSTFLAGS`, and the contract it must meet. +#[derive(Clone, Copy, Debug)] +struct RustflagsCase { + /// The Make target owning the recipe. + target: &'static str, + /// Substring selecting the recipe line. `lint-clippy` sets `RUSTFLAGS` on + /// two lines — one for rustdoc, one for Clippy — with different contracts. + line_marker: &'static str, + /// Whether the recipe adds `-D warnings`. + denies_warnings: bool, + /// Whether the recipe must contribute its separator only alongside an + /// inherited value, so an unset `RUSTFLAGS` leaves no leading space. + /// + /// This is the contract the case asserts, deliberately not read back from + /// the Makefile: inferring it from the assignment would let a rewrite to a + /// bare `$RUSTFLAGS ` prefix delete the assertion along with the idiom. + separator_only_when_set: bool, +} + +impl RustflagsCase { + const fn test_nextest() -> Self { + Self { + target: "test-nextest", + line_marker: "nextest run", + denies_warnings: true, + separator_only_when_set: true, + } + } + + const fn doctest() -> Self { + Self { + target: "doctest", + line_marker: "--doc", + denies_warnings: true, + separator_only_when_set: true, + } + } + + const fn binary_build() -> Self { + Self { + target: "target/%/$(APP)", + line_marker: "build", + denies_warnings: false, + separator_only_when_set: false, + } + } + + const fn lint_clippy_rustdoc() -> Self { + Self { + target: "lint-clippy", + line_marker: "doc --no-deps", + denies_warnings: false, + separator_only_when_set: false, + } + } + + const fn lint_clippy() -> Self { + Self { + target: "lint-clippy", + line_marker: "clippy", + denies_warnings: true, + separator_only_when_set: true, + } + } + + const fn lint_whitaker() -> Self { + Self { + target: "lint-whitaker", + line_marker: "$(WHITAKER)", + denies_warnings: true, + separator_only_when_set: true, + } + } + + const fn typecheck() -> Self { + Self { + target: "typecheck", + line_marker: "check", + denies_warnings: true, + separator_only_when_set: true, + } + } + + const fn kani_full() -> Self { + Self { + target: "kani-full", + line_marker: "$(KANI)", + denies_warnings: false, + separator_only_when_set: true, + } + } +} + +/// Every `RUSTFLAGS`-setting recipe line under contract. +const RUSTFLAGS_CASES: [RustflagsCase; 8] = [ + RustflagsCase::test_nextest(), + RustflagsCase::doctest(), + RustflagsCase::binary_build(), + RustflagsCase::lint_clippy_rustdoc(), + RustflagsCase::lint_clippy(), + RustflagsCase::lint_whitaker(), + RustflagsCase::typecheck(), + RustflagsCase::kani_full(), +]; + +/// Returns the value of a simple `NAME ?= value` or `NAME = value` variable. +fn make_variable(contents: &str, name: &str) -> Option { + contents.lines().find_map(|line| { + let rest = line.strip_prefix(name)?; + let value = rest + .strip_prefix(" ?= ") + .or_else(|| rest.strip_prefix(" = "))?; + Some(value.trim().to_owned()) + }) +} + +/// Extracts the double-quoted `RUSTFLAGS` assignment from a recipe line. +/// +/// `RUSTDOCFLAGS="…"` does not contain `RUSTFLAGS="`, so a line setting both +/// still yields the `RUSTFLAGS` value. +fn rustflags_assignment(line: &str) -> Option<&str> { + let start = line.find(RUSTFLAGS_PREFIX)? + RUSTFLAGS_PREFIX.len(); + let rest = line.get(start..)?; + let end = rest.find('"')?; + rest.get(..end) +} + +/// Returns the recipe line `case` selects. +fn recipe_line(makefile: &str, case: RustflagsCase) -> Result { + let recipe = target_recipe(makefile, case.target) + .with_context(|| format!("Makefile should declare a {} target", case.target))?; + recipe + .lines() + .find(|line| line.contains(RUSTFLAGS_PREFIX) && line.contains(case.line_marker)) + .map(str::trim) + .map(ToOwned::to_owned) + .with_context(|| { + format!( + "{} should set RUSTFLAGS on a line matching {:?}", + case.target, case.line_marker + ) + }) +} + +/// Returns `case`'s `RUSTFLAGS` assignment as a shell expression. +/// +/// Make variable references are resolved, and Make's `$$` escape is reduced to +/// the single `$` the shell receives. +fn shell_expression(makefile: &str, case: RustflagsCase) -> Result { + let line = recipe_line(makefile, case)?; + let assignment = rustflags_assignment(&line).with_context(|| { + format!( + "{} should assign a double-quoted RUSTFLAGS value", + case.target + ) + })?; + let polonius = make_variable(makefile, "POLONIUS_FLAGS") + .context("Makefile should define POLONIUS_FLAGS")?; + let resolved = assignment.replace("$(POLONIUS_FLAGS)", &polonius); + ensure!( + !resolved.contains("$("), + "{}: RUSTFLAGS assignment {resolved:?} names a Make variable this test cannot resolve", + case.target + ); + Ok(resolved.replace("$$", "$")) +} + +/// Expands `expression` in a shell, exporting `inherited` as `RUSTFLAGS`. +/// +/// Only the assignment is expanded; the command the recipe would run is never +/// executed, so no test here invokes Cargo, Kani, nextest, or Dylint. +#[cfg(unix)] +fn expand(expression: &str, inherited: Option<&str>) -> Result { + ensure!( + !expression.contains('"') && !expression.contains('`'), + "the expansion helper cannot safely embed {expression:?}" + ); + let mut command = Command::new("sh"); + command + .arg("-c") + .arg(format!("printf '%s' \"{expression}\"")) + .env_remove("RUSTFLAGS"); + if let Some(value) = inherited { + command.env("RUSTFLAGS", value); + } + + let output = command + .output() + .with_context(|| format!("expand {expression:?} with sh"))?; + ensure!( + output.status.success(), + "sh should expand {expression:?}: {}", + String::from_utf8_lossy(&output.stderr) + ); + String::from_utf8(output.stdout).context("expanded RUSTFLAGS should be UTF-8") +} + +#[test] +fn unit_extracts_the_rustflags_assignment_from_a_recipe_line() { + assert_eq!( + rustflags_assignment(r#" RUSTFLAGS="$${RUSTFLAGS:+$$RUSTFLAGS }-D warnings" $(CARGO) x"#), + Some(r"$${RUSTFLAGS:+$$RUSTFLAGS }-D warnings") + ); + // A line setting RUSTDOCFLAGS first still yields the RUSTFLAGS value. + assert_eq!( + rustflags_assignment(r#" RUSTDOCFLAGS="-D warnings" RUSTFLAGS="$${RUSTFLAGS-} -Z" x"#), + Some(r"$${RUSTFLAGS-} -Z") + ); + assert_eq!(rustflags_assignment("\tcargo build"), None); +} + +#[cfg(unix)] +#[rstest] +#[case(RustflagsCase::test_nextest())] +#[case(RustflagsCase::doctest())] +#[case(RustflagsCase::binary_build())] +#[case(RustflagsCase::lint_clippy_rustdoc())] +#[case(RustflagsCase::lint_clippy())] +#[case(RustflagsCase::lint_whitaker())] +#[case(RustflagsCase::typecheck())] +#[case(RustflagsCase::kani_full())] +fn behavioural_rustflags_recipes_preserve_inherited_flags( + #[case] case: RustflagsCase, +) -> Result<()> { + let makefile = read_repo_file(Utf8Path::new("Makefile"))?; + let polonius = make_variable(&makefile, "POLONIUS_FLAGS") + .context("Makefile should define POLONIUS_FLAGS")?; + let expanded = expand(&shell_expression(&makefile, case)?, Some(CALLER_RUSTFLAGS))?; + + ensure!( + expanded.contains(CALLER_RUSTFLAGS), + "{} should preserve the caller's RUSTFLAGS, expanded to {expanded:?}", + case.target + ); + ensure!( + expanded.contains(&polonius), + "{} should re-state {polonius} because setting RUSTFLAGS overrides \ + .cargo/config.toml, expanded to {expanded:?}", + case.target + ); + ensure!( + expanded.contains(DENY_WARNINGS) == case.denies_warnings, + "{} should {}deny warnings, expanded to {expanded:?}", + case.target, + if case.denies_warnings { "" } else { "not " } + ); + Ok(()) +} + +#[cfg(unix)] +#[rstest] +#[case(RustflagsCase::test_nextest())] +#[case(RustflagsCase::doctest())] +#[case(RustflagsCase::binary_build())] +#[case(RustflagsCase::lint_clippy_rustdoc())] +#[case(RustflagsCase::lint_clippy())] +#[case(RustflagsCase::lint_whitaker())] +#[case(RustflagsCase::typecheck())] +#[case(RustflagsCase::kani_full())] +fn behavioural_rustflags_recipes_are_well_formed_without_inherited_flags( + #[case] case: RustflagsCase, +) -> Result<()> { + let makefile = read_repo_file(Utf8Path::new("Makefile"))?; + let polonius = make_variable(&makefile, "POLONIUS_FLAGS") + .context("Makefile should define POLONIUS_FLAGS")?; + let expression = shell_expression(&makefile, case)?; + let expanded = expand(&expression, None)?; + + ensure!( + expanded.contains(&polonius), + "{} should re-state {polonius} even with no inherited RUSTFLAGS, \ + expanded to {expanded:?}", + case.target + ); + ensure!( + !expanded.contains(CALLER_RUSTFLAGS), + "{} should not invent flags the caller never set, expanded to {expanded:?}", + case.target + ); + // `${VAR:+VAR }` contributes its separator only alongside a value, so an + // unset RUSTFLAGS must not leave a leading space. Recipes spelling the + // expansion `${VAR-}` tolerate one, so the case declares which contract + // applies. This is what separates the idiom from a bare `$RUSTFLAGS ` + // prefix, which preserves the caller's flags but strands a separator. + if case.separator_only_when_set { + ensure!( + !expanded.starts_with(' '), + "{} should not emit a leading separator when RUSTFLAGS is unset, \ + expanded to {expanded:?}", + case.target + ); + } + Ok(()) +} + +#[test] +fn behavioural_every_rustflags_recipe_line_is_under_contract() -> Result<()> { + let makefile = read_repo_file(Utf8Path::new("Makefile"))?; + let declared: BTreeSet = makefile + .lines() + .filter(|line| line.starts_with('\t') && line.contains(RUSTFLAGS_PREFIX)) + .map(|line| line.trim().to_owned()) + .collect(); + let covered: BTreeSet = RUSTFLAGS_CASES + .iter() + .map(|case| recipe_line(&makefile, *case)) + .collect::>()?; + + let uncovered: Vec<&String> = declared.difference(&covered).collect(); + ensure!( + uncovered.is_empty(), + "every recipe setting RUSTFLAGS needs a RustflagsCase; uncovered: {uncovered:#?}" + ); + ensure!( + covered.len() == RUSTFLAGS_CASES.len(), + "each RustflagsCase should select a distinct recipe line, {} cases selected {} lines", + RUSTFLAGS_CASES.len(), + covered.len() + ); + Ok(()) +} + /// Returns the `[[profile.default.overrides]]` entries. fn profile_overrides(config: &Value) -> Option<&[Value]> { config