From fbb713cf35ff61d3368e7283d2bd57dbe1ebe6a6 Mon Sep 17 00:00:00 2001 From: leynos Date: Mon, 22 Jun 2026 19:05:08 +0200 Subject: [PATCH] Add execplan for formal-verification Makefile targets (15.1.4) Draft an execution plan for roadmap item 15.1.4, which adds the `test-verification`, `kani`, `kani-full`, `verus`, `formal-pr`, and `formal-nightly` Makefile targets. The plan resolves the central tension that three targets have no harnesses or proofs to run yet (those land in roadmap 15.3.x and 15.5.x) against the success criterion that each target returns exit 0 on a clean tree. After a Logisphere design-review panel, the design uses explicit stubs via a shared `scripts/formal-stub.sh` helper rather than self-activating skip guards: each stub prints a structured `FORMAL-SKIP:` marker and exits 0, or exits non-zero under `FORMAL_STRICT=1` so later CI work can assert a target is no longer skipping. The owning roadmap item replaces each stub recipe in a loud, reviewable edit. The plan extends the existing formal-tooling test harness, adding a `target_prerequisites` helper and hardening `.PHONY` parsing so the prerequisite-only aggregate targets can be asserted. This commit adds the plan document only; implementation awaits approval. Co-Authored-By: Claude Opus 4.8 (1M context) --- ...-4-formal-verification-makefile-targets.md | 696 ++++++++++++++++++ 1 file changed, 696 insertions(+) create mode 100644 docs/execplans/15-1-4-formal-verification-makefile-targets.md diff --git a/docs/execplans/15-1-4-formal-verification-makefile-targets.md b/docs/execplans/15-1-4-formal-verification-makefile-targets.md new file mode 100644 index 00000000..c696d255 --- /dev/null +++ b/docs/execplans/15-1-4-formal-verification-makefile-targets.md @@ -0,0 +1,696 @@ +# Add formal-verification Makefile targets (15.1.4) + +This ExecPlan (execution plan) is a living document. The sections +`Constraints`, `Tolerances`, `Risks`, `Progress`, `Surprises & Discoveries`, +`Decision Log`, and `Outcomes & Retrospective` must be kept up to date as work +proceeds. + +Status: DRAFT (awaiting user approval) + +## Purpose / big picture + +Wireframe is adopting formal verification (roadmap section 15). The tool +installation plumbing already exists: `make install-kani`, +`make check-kani-version`, `make install-verus`, and `make run-verus` delegate to +the pinned `rust-prover-tools` entry point. What is missing is the *execution +surface* a contributor or CI job uses to run verification work. + +Roadmap item 15.1.4 adds six Makefile targets that form that surface: + +1. `make test-verification` runs the Stateright model tests in + `crates/wireframe-verification`. +2. `make kani` runs the fast Kani smoke harnesses. +3. `make kani-full` runs every Kani harness. +4. `make verus` runs the Verus proof entry point. +5. `make formal-pr` is the fast gate intended for every pull request. +6. `make formal-nightly` is the deeper gate intended for scheduled runs. + +After this change a contributor can type `make formal-pr` on a freshly checked +out, clean tree and watch it complete with exit code `0`, today, even though no +Kani harnesses and no Verus proofs exist yet. `make test-verification` runs for +real immediately, because the verification crate already contains a Stateright +model and roughly twenty test items. The three tool-driven targets (`kani`, +`kani-full`, `verus`) are **explicit stubs** until the later roadmap items that +own them land their harnesses and proofs. + +You can observe success three ways: + +1. `mbake validate Makefile` reports `Valid syntax` and exits `0`. +2. Each of the six targets exits `0` on a clean tree. The three stub targets + print a single structured `FORMAL-SKIP:` notice to standard error explaining + which roadmap item will replace the stub. +3. `make test` passes, including new regression tests in + `tests/formal_tooling.rs` and a new behavioural scenario in + `tests/features/formal_tooling.feature` that assert the targets exist, + delegate correctly, and behave as specified (skip-by-default, fail under + `FORMAL_STRICT=1`). + +## Design rationale: explicit stubs, not self-activating guards + +This is the single most important decision in this plan, so it is stated up +front. It was revised after a Logisphere design-review panel (see "Design review +summary" below); the rejected first approach is recorded in the Decision Log. + +The roadmap success criterion for 15.1.4 is: + +> each target is accepted by `mbake validate Makefile` and returns exit `0` on a +> clean tree. + +Three of the six targets have nothing to run yet: + +- `make kani` (smoke) would name specific harnesses that arrive in roadmap + 15.3.1 (`src/frame/*`). +- `make kani-full` would run `cargo kani -p wireframe`, but there are zero + `#[kani::proof]` harnesses in the tree today. +- `make verus` would run `verus/wireframe_proofs.rs`, which does not exist; the + `verus/` directory is absent. The developers' guide already documents that + `make run-verus` is *expected to fail* with a missing-proof diagnostic until + roadmap 15.5.2. + +A target cannot both "run the real Verus proof" and "return exit `0` on a clean +tree" while the proof file is absent. The plan resolves this with **explicit +stubs**: `kani`, `kani-full`, and `verus` invoke a single tiny shared helper, +`scripts/formal-stub.sh`, which prints a structured `FORMAL-SKIP:` line naming +the roadmap item that will replace the stub, and exits `0`. There is no +filesystem `grep`, no `[ -f ]` test, no empty-variable loop, and no recursive +sub-make. When roadmap 15.3.x and 15.5.x land their harnesses and proofs, the +PR that adds them *replaces that target's one-line stub recipe* with the real +tool invocation — a loud, reviewable edit made in the same change that is +already touching that part of the tree. + +Why explicit stubs rather than guards that self-activate when artefacts appear: + +1. The guarded "self-activating" design is an outlier — none of the sibling + repos (`netsuke`, `chutoro`, `mxd`) ship readiness oracles in their + Makefiles. A Makefile is read far more often than it is run; optimise for the + reader. +2. Self-activation fails *silently*: a harness gated behind a feature the grep + does not see, or a smoke list a human forgets to populate, leaves a target + printing "skipping" forever while everyone believes verification runs. An + explicit stub fails *loudly*: the activating PR must edit the recipe, and the + reviewer sees it. +3. The most-run gate (`formal-pr` → `kani`) was, in the guarded design, the most + fragile (hand-maintained smoke list), while the least-run gate + (`formal-nightly` → `kani-full`) self-healed. That is backwards. Explicit + stubs make both tiers equally honest. + +To keep the future activation safe, the plan adds `FORMAL_STRICT=1`: an opt-in +environment switch that turns every stub's skip into a non-zero exit. Roadmap +15.1.5 (CI jobs) can then run a strict job that fails if any `FORMAL-SKIP:` +marker appears once a target is supposed to be real, giving the team a tripwire +against a forgotten activation. + +This design deliberately diverges from the literal Makefile snippet in +`docs/formal-verification-methods-in-wireframe.md` §"Recommended Makefile +changes", which assumes harnesses and proofs already exist. The six target names +and the aggregate composition match the doc; only the interim recipe bodies +differ, and only until 15.3.x/15.5.x fill them in. + +## Constraints + +Hard invariants that must hold throughout implementation. Violation requires +escalation, not a workaround. + +1. Do not modify production crate source (`src/**`), the public API, or + `Cargo.toml` dependency or feature tables. This item is build-and-test + plumbing only. Adding `cfg(kani)` to `check-cfg` belongs to roadmap 15.3.1, + alongside the first harness. +2. Keep the existing `run-verus`, `install-kani`, `check-kani-version`, and + `install-verus` targets byte-for-byte unchanged. The regression suite in + `tests/formal_tooling.rs` pins their exact recipes, and the developers' guide + documents `run-verus` as the raw, fail-loud proof runner. +3. The Makefile must continue to pass `mbake validate Makefile` with exit `0`. +4. Recipes must use real tab indentation (Make requires tabs). Editors that + convert tabs to spaces will break the build and `mbake`. +5. New formal targets must not be pulled into `make test`, `make lint`, or the + default `all` target. They are a separate surface, consistent with the CI + guidance that formal jobs stay independent of `build-test`. +6. The targets must exit `0` on a clean tree *without* Kani or Verus installed. + Plumbing validation must not depend on a multi-minute toolchain install. By + corollary, `formal-pr` must not depend on `check-kani-version` (which needs + Kani installed); it composes only tool-free targets. +7. No test in the default `make test` suite may invoke `cargo kani`, `verus`, or + `run-verus`, before or after 15.3.x/15.5.x. The stub targets are safe to + execute in tests because they only run `scripts/formal-stub.sh`. When a + future item replaces a stub recipe with a real tool invocation, that same PR + must relocate or guard the corresponding execution test so the default suite + stays tool-free. This invariant is documented in the developers' guide. +8. Recipes and `scripts/formal-stub.sh` must be POSIX-sh clean (no bashisms such + as `[[ ]]` or `local`); the script must pass `shellcheck`. +9. `.PHONY` handling: the test helper is hardened to follow backslash + continuations, so `.PHONY` may wrap; recipe blocks are separated by exactly + one blank line. +10. All prose in changed Markdown wraps at 80 columns; fenced code blocks wrap at + 120 columns; use `-` for list bullets; follow + `docs/documentation-style-guide.md`. + +## Tolerances (exception triggers) + +Stop and escalate (do not improvise) when any threshold is crossed: + +1. Scope: this change legitimately spans the Makefile, a small shell helper, the + formal-tooling test harness (integration test, shared helper, BDD fixture, + feature file, step definitions), and two docs. If it grows beyond roughly 12 + files or 400 net lines, stop and escalate. +2. Source/API: if any change to `src/**`, the public API, or `Cargo.toml` + `[dependencies]`/`[features]` appears necessary, stop and escalate. +3. Existing targets: if any change to the four existing prover-tools targets + appears necessary, stop and escalate. +4. Tooling: if `mbake validate Makefile` cannot pass without restructuring + unrelated parts of the Makefile, stop and escalate. +5. Test design: if making `make test` cover the new targets would require Kani + or Verus to be installed, stop and escalate (Constraints 6 and 7). +6. Iterations: if the gates (`mbake`, `check-fmt`, `lint`, `test`) still fail + after 3 fix attempts on the same milestone, stop and escalate. +7. Ambiguity: if a reviewer rejects the explicit-stub design, stop and present + the trade-offs rather than choosing unilaterally. + +## Risks + +1. Risk: an automated "exit `0`" test that *really executes* `make formal-pr` + would recurse into `cargo test -p wireframe-verification` from inside + `cargo test`, inflating `make test` runtime. + Severity: medium. Likelihood: high if done naively. + Mitigation: real-execute only the stub targets (`kani`, `kani-full`, `verus`), + which merely run `scripts/formal-stub.sh`; assert `test-verification`, + `formal-pr`, and `formal-nightly` via `make --dry-run`, which does not execute + recipes. Validate the full real run once, manually, recorded as evidence. +2. Risk: the existing test helpers cannot assert what the plan needs. + `MakefileContent::target_recipe` discards the rule line, so it returns + `Some("")` for the prerequisite-only aggregates (`formal-pr`, + `formal-nightly`) and cannot see their prerequisites; `has_phony_target` + breaks if `.PHONY` is wrapped onto a continuation line. + Severity: high (would give false confidence). Likelihood: high. + Mitigation: add a `target_prerequisites` helper that parses the rule line, and + harden `has_phony_target` to join `\`-continued `.PHONY` lines. Assert the + aggregates via both the new helper and `make --dry-run` content. Do not rely + on `target_recipe` being `Some` for the aggregates (that proves nothing). +3. Risk: tab/space corruption in new recipes breaks Make and `mbake`. + Severity: medium. Likelihood: medium. + Mitigation: after editing, run `mbake validate Makefile` and `make --dry-run` + for each new target before the wider gates. +4. Risk: a forgotten activation — a future item adds a harness or proof but does + not replace the stub recipe — leaves a target skipping while looking green. + Severity: medium. Likelihood: medium. + Mitigation: explicit stubs make activation a visible recipe edit in the + owning PR; `FORMAL_STRICT=1` lets 15.1.5 add a CI tripwire that fails on any + `FORMAL-SKIP:` marker; the developers' guide records the activation contract + and the tool-free-test invariant (Constraint 7) so 15.3.x/15.5.x authors know + what to change. +5. Risk: when 15.3.x replaces the `kani` stub with a real recipe, it must invoke + the *pinned* Kani (resolved through `rust-prover-tools` / the `KANI_ENV` + `LD_LIBRARY_PATH` pattern used by `chutoro`), not an arbitrary `cargo kani` on + `PATH`. + Severity: low (future item). Likelihood: low. + Mitigation: note this requirement in the developers' guide activation + contract so the owning item gets it right; out of scope for 15.1.4. + +## Progress + +- [x] (2026-06-22) Research: studied roadmap 15.1.4, the formal-verification + methods doc, prior-art Makefiles (`netsuke`, `chutoro`, `mxd`), the + existing formal-tooling test harness, and current repo state. +- [x] (2026-06-22) Drafted the initial plan (self-activating skip guards). +- [x] (2026-06-22) Logisphere design-review panel; pivoted to explicit stubs and + revised the plan accordingly. +- [ ] (pending) User approval of this plan (required before implementation). +- [ ] (pending) Stage A: confirm orientation and baseline. +- [ ] (pending) Stage B: red regression and behavioural tests. +- [ ] (pending) Stage C: implement the helper script and six Makefile targets. +- [ ] (pending) Stage D: documentation and roadmap tick. +- [ ] (pending) Stage E: full gate run and CodeRabbit review. + +## Surprises & discoveries + +- Observation: a complete formal-tooling test harness already exists. + Evidence: `tests/formal_tooling.rs`, `tests/common/formal_tooling_support.rs`, + `tests/fixtures/formal_tooling.rs`, and + `tests/features/formal_tooling.feature` already assert the four existing + prover-tools targets via recipe inspection and `make --dry-run`. + Impact: 15.1.4 extends this harness rather than inventing a test approach. +- Observation: the shared helpers cannot assert prerequisite-only rules and + break on a wrapped `.PHONY`. + Evidence: `tests/common/formal_tooling_support.rs:16-39` — + `target_recipe` discards the rule line; `has_phony_target` splits a single + line only. + Impact: the test plan must add a `target_prerequisites` helper and harden + `has_phony_target` (Risk 2). +- Observation: the developers' guide already states `run-verus` is expected to + fail until `verus/wireframe_proofs.rs` exists. + Evidence: `docs/developers-guide.md` §"Formal verification tooling". + Impact: confirms `run-verus` stays fail-loud; the new `verus` target is a + separate stub, not a wrapper around `run-verus`. + +## Decision log + +- Decision: use explicit stubs (`scripts/formal-stub.sh`) for `kani`, + `kani-full`, and `verus`, replaced by the owning roadmap items; add + `FORMAL_STRICT=1` to turn skips into failures. + Rationale: satisfies the exit-`0` criterion while keeping harnesses (15.3.x) + and proofs (15.5.x) in their own items, keeps plumbing tool-free, and makes + activation a loud, reviewable edit. Endorsed by the Logisphere panel. + Date/Author: 2026-06-22, planning agent + design-review panel. +- Decision (superseded): the first draft used self-activating guards + (`grep -rq 'kani::proof' src`, an empty `KANI_SMOKE_HARNESSES` loop, and + `$(MAKE) run-verus` gated on `[ -f ]`). + Rationale for reversal: three different readiness idioms in ~14 lines is too + clever for plumbing; it is an outlier versus sibling repos; and its failure + mode is a *silent* forever-skip (false green), worst on the most-run PR gate. + Date/Author: 2026-06-22, design-review panel (Wafflecat, Dinolump, Doggylump). +- Decision: `make test-verification` uses `cargo test -p wireframe-verification` + (not `cargo nextest`). + Rationale: the formal-verification methods document recommends `cargo test` to + minimise the delta from current Wireframe practice; switch to nextest only if + the whole repo migrates. + Date/Author: 2026-06-22, planning agent. +- Decision: do not introduce `KANI`/`KANI_*` Makefile variables in 15.1.4. + Rationale: with stub recipes they would be dead config; 15.3.x introduces them + with the real recipes (and must use the pinned Kani — Risk 5). + Date/Author: 2026-06-22, design-review panel (Dinolump). +- Decision: keep the `formal` alias (`formal: formal-pr`); drop the `stateright` + alias. + Rationale: `formal` is a discoverable default with no semantic trap; + `stateright` is a misleading synonym for `test-verification` (the CI job is + named `stateright-models` but runs `cargo test`), inviting the belief that it + runs the Stateright tool directly. + Date/Author: 2026-06-22, design-review panel (Dinolump). +- Decision: do not add `cfg(kani)` to `check-cfg` or otherwise touch + `Cargo.toml` in 15.1.4. + Rationale: there is no `cfg(kani)` code yet; that wiring belongs to 15.3.1. + Date/Author: 2026-06-22, planning agent. + +## Outcomes & retrospective + +To be completed at the end of implementation. Compare the delivered targets +against the six required names and the exit-`0` criterion; confirm the +`FORMAL_STRICT` tripwire works and the activation contract is documented for +15.3.x/15.5.x. + +## Design review summary + +A Logisphere pre-implementation panel reviewed the first draft. Key outcomes, +all folded into this revision: + +- Pandalump/Telefono (structure and contracts): the *test plan* was the weak + point — the existing helpers cannot assert the prerequisite-only aggregates + and break on a wrapped `.PHONY`. Fixed by Risk 2's mitigations. +- Wafflecat (alternatives) and Dinolump (viability): the self-activating guards + were too clever and an outlier versus sibling repos; recommended explicit + stubs that the owning PRs replace, plus dropping the `stateright` alias and the + premature `KANI_*` variables. Adopted. +- Doggylump (pre-mortem): the worst case is a silent "false green" (a target + that skips forever) and a "time bomb" test that detonates inside `make test` + once guards flip. Addressed by explicit stubs (loud activation), Constraint 7 + (tool-free default suite), and the `FORMAL_STRICT=1` tripwire with a greppable + `FORMAL-SKIP:` marker. + +## Context and orientation + +The reader is assumed to know nothing about this repository. + +This is the `wireframe` Rust library. The repository root holds the primary +crate; `crates/wireframe-verification` is an internal (unpublished) workspace +member holding Stateright models; `wireframe_testing` is a test-support crate. +The workspace: + +```toml +[workspace] +members = [".", "crates/wireframe-verification", "wireframe_testing"] +default-members = ["."] +resolver = "3" +``` + +Key files for this task, by full path: + +1. `Makefile` — the file to edit. Today it ends with the four prover-tools + targets (`install-kani`, `check-kani-version`, `install-verus`, `run-verus`) + and a `help` target. Relevant existing variables: `CRATE ?= wireframe`, + `CARGO ?= cargo`, `BUILD_JOBS ?=`, `PROVER_TOOLS ?= ...`, and + `VERUS_PROOF_FILE ?= verus/wireframe_proofs.rs`. The first line is the single + `.PHONY` declaration. +2. `scripts/formal-stub.sh` — new. A small POSIX-sh helper that prints a + `FORMAL-SKIP:` notice and exits `0`, or exits non-zero under + `FORMAL_STRICT`. The repo already keeps helpers under `scripts/` (for example + `scripts/doctest-benchmark.sh`). +3. `tests/formal_tooling.rs` — integration regression tests. Uses `rstest`, + `proptest`, and helpers from `tests/common/formal_tooling_support.rs`. It + already verifies targets are `.PHONY`, that recipes contain expected + substrings, and that `make --dry-run ` emits the expected command. + New red tests go here. +4. `tests/common/formal_tooling_support.rs` — shared helpers: + `MakefileContent { has_phony_target, target_recipe }`, `makefile()`, + `MAKEFILE_PATH`, version readers, and `run_make_dry_run`. This file gains a + `target_prerequisites` helper, a hardened `has_phony_target` (follows `\` + continuations), and a `run_make` helper (real execution, capturing status and + stderr) beside `run_make_dry_run`. +5. `tests/fixtures/formal_tooling.rs` — the BDD world `FormalToolingWorld`. Gains + `verify_formal_execution_targets(&self) -> TestResult`. +6. `tests/features/formal_tooling.feature` — the Gherkin feature. Gains a + scenario for the execution targets. The matching step definitions live in the + BDD module wired through `tests/bdd.rs`; locate the existing formal-tooling + steps (search `tests/` for the step text "the Makefile exposes the formal + verification tool entry points", or use + `leta grep "formal" -k function`) and add steps beside them. +7. `docs/developers-guide.md` — §"Formal verification tooling" (around line 259) + documents the four install targets. The six execution targets, the + `FORMAL_STRICT` switch, the activation contract, and the tool-free-test + invariant (Constraint 7) are documented here. +8. `docs/roadmap.md` — item 15.1.4 (line 603) is ticked on completion. + +Reference material (read for rationale; do not edit): +`docs/formal-verification-methods-in-wireframe.md` §"Recommended Makefile +changes" and §"Recommended CI changes"; prior-art Makefiles in `leynos/netsuke` +(cheap `formal-pr`), `leynos/chutoro` (explicit Kani harness names plus a +`KANI_ENV` `LD_LIBRARY_PATH` wrapper), and `leynos/mxd` +(`test-verification` runs the verification crate). + +Relevant skills to load while implementing: `execplans` (this document), `kani` +and `verus` (tool semantics; needed when the stubs are later replaced), +`rust-verification` (selection context), `rust-unit-testing` and `proptest` +(the existing tests in `formal_tooling.rs`), and `leta` for navigation; +`rust-router` routes deeper Rust questions. + +## Plan of work + +Proceed in stages with a validation gate at the end of each. Do not advance past +a failing gate. Do not begin Stage A until the user has approved this plan. + +### Stage A: understand and propose (no code changes) + +1. Run `git branch --show-current`; confirm + `15-1-4-formal-verification-makefile-targets`. +2. Run `mbake validate Makefile`; expect `Valid syntax`, exit `0`. +3. Re-read the tail of the `Makefile` and the cases in `tests/formal_tooling.rs` + that drive `makefile_declares_prover_tools_targets` and + `make_targets_dry_run_to_expected_prover_tools_command`. Confirm the helper + API in `tests/common/formal_tooling_support.rs`, in particular how + `target_recipe` and `has_phony_target` parse lines. + +Gate A: orientation notes recorded; no diffs. + +### Stage B: red regression and behavioural tests + +Add the smallest tests that specify the missing behaviour and watch them fail +for the right reason before touching the Makefile or the helper script. + +1. Extend `tests/common/formal_tooling_support.rs`: + - harden `has_phony_target` to join backslash-continued `.PHONY` lines; + - add `target_prerequisites(&self, target) -> Option>` that finds + the rule line and returns the tokens after the colon; + - add `run_make(target) -> FormalToolingResult<(ExitStatus, String, String)>` + (real execution, returning status, stdout, stderr) and an + `env`-aware variant or argument for `FORMAL_STRICT`. +2. In `tests/formal_tooling.rs`, add: + - `formal_execution_targets_are_declared` (`rstest` cases over all six + targets): each is `has_phony_target` true and present. + - `direct_recipe_targets_have_expected_content` (`rstest` over + `test-verification`, `kani`, `kani-full`, `verus`): `test-verification` + recipe contains `test -p wireframe-verification`; each stub recipe contains + `formal-stub.sh` and its own target name. + - `aggregate_targets_declare_expected_prerequisites` (`rstest`): `formal-pr` + prerequisites are exactly `test-verification kani verus`; `formal-nightly` + are `test-verification kani-full verus` (via the new + `target_prerequisites`). + - `stub_targets_skip_and_exit_zero` (`rstest` over `kani`, `kani-full`, + `verus`): `run_make` exits `0` and stderr contains `FORMAL-SKIP:` and the + target name. + - `stub_targets_fail_under_formal_strict` (`rstest` over the three stubs): + with `FORMAL_STRICT=1`, `run_make` exits non-zero and stderr contains + `FORMAL-SKIP:`. + - `aggregate_targets_dry_run_zero` (`rstest` over `test-verification`, + `formal-pr`, `formal-nightly`): `make --dry-run` exits `0`; + `formal-pr`/`formal-nightly` dry-run output mentions `wireframe-verification` + and `formal-stub.sh`. +3. In `tests/features/formal_tooling.feature`, add: + + ```gherkin + Scenario: The repository exposes formal-verification execution targets + Given the formal verification tooling metadata is loaded + Then the Makefile exposes the formal verification execution targets + And the formal execution stubs skip cleanly on a clean tree + ``` + + Add `verify_formal_execution_targets` to `FormalToolingWorld` and matching + step definitions beside the existing formal-tooling steps. + +Gate B (Red): run +`cargo test --test formal_tooling 2>&1 | tee /tmp/red-wireframe-$(git branch --show-current).out` +and `make test-bdd 2>&1 | tee -a /tmp/red-wireframe-$(git branch --show-current).out`. +Expect the new cases to fail because the targets and the stub script do not exist +yet. Record the failure text as evidence. + +### Stage C: implement the helper and the six targets + +1. Create `scripts/formal-stub.sh` (POSIX sh, executable, `shellcheck`-clean). + Behaviour: argument 1 is the target name, the rest is a human message; print + `FORMAL-SKIP: not yet implemented — ` to stderr; if + `FORMAL_STRICT` is non-empty, exit `1`, else exit `0`. Do not interpolate + untrusted values into a `printf` format string (pass them as arguments). +2. Edit `Makefile`: + - extend `.PHONY` with + `test-verification kani kani-full verus formal-pr formal-nightly formal`; + - add `VERIFICATION_CRATE ?= wireframe-verification`, + `FORMAL_STUB ?= ./scripts/formal-stub.sh`, and `FORMAL_STRICT ?=` near the + other tool variables (exporting `FORMAL_STRICT` so the script sees it, or + passing it explicitly — see "Interfaces"); + - add the six targets and the `formal` alias (recipes in "Interfaces"). + Keep one blank line between target blocks; use real tabs. + +Gate C (Green): + +1. `mbake validate Makefile` → `Valid syntax`, exit `0`. +2. `shellcheck scripts/formal-stub.sh` → clean. +3. `make --dry-run` for each of the six targets exits `0`. +4. Re-run the Stage B tests; they pass. Tee to + `/tmp/green-wireframe-$(git branch --show-current).out`. + +### Stage D: documentation and roadmap + +1. Expand `docs/developers-guide.md` §"Formal verification tooling" with a + subsection covering the six targets, the `FORMAL_STRICT` switch and + `FORMAL-SKIP:` marker, the activation contract (which roadmap item replaces + each stub, and that the replacement must use the pinned Kani and keep the + default test suite tool-free per Constraint 7). Wrap prose at 80 columns. +2. Run `make fmt`, then `make markdownlint`, and `make nixie` if the changed + Markdown contains Mermaid. +3. Tick roadmap item 15.1.4 in `docs/roadmap.md` only after every gate passes. + +Gate D: `make check-fmt` and `make markdownlint` pass. + +### Stage E: full gates and review + +1. Run sequentially (never in parallel; caching is shared), teeing each to + `/tmp`: `make check-fmt`, `make lint`, `make test`. +2. Run `mbake validate Makefile` once more. +3. Manually run all six targets for real on a clean tree; capture a transcript + proving each exits `0`, and run the three stubs with `FORMAL_STRICT=1` to show + they exit non-zero. +4. Commit, then run `coderabbit review --agent`; resolve every concern before + declaring the milestone complete. + +Gate E: all gates green; CodeRabbit concerns cleared. + +## Concrete steps + +Run everything from the repository root. + +Baseline: + +```bash +git branch --show-current +mbake validate Makefile +``` + +Expected: + +```plaintext +15-1-4-formal-verification-makefile-targets +✓ Makefile: Valid syntax +``` + +Red stage: + +```bash +cargo test --test formal_tooling \ + 2>&1 | tee /tmp/red-wireframe-$(git branch --show-current).out +``` + +Expect failures naming the missing targets and the missing stub script. + +Green stage (after Stage C): + +```bash +mbake validate Makefile +shellcheck scripts/formal-stub.sh +for t in test-verification kani kani-full verus formal-pr formal-nightly; do + echo "== dry-run $t =="; make --dry-run "$t"; echo "exit=$?"; +done +cargo test --test formal_tooling \ + 2>&1 | tee /tmp/green-wireframe-$(git branch --show-current).out +``` + +Stub behaviour proof on a clean tree: + +```bash +for t in kani kani-full verus; do + make "$t"; echo "$t exit=$?"; + FORMAL_STRICT=1 make "$t"; echo "$t strict exit=$?"; +done +``` + +Expected (abbreviated): + +```plaintext +FORMAL-SKIP: kani not yet implemented — roadmap 15.3.1 adds src/frame Kani smoke harnesses +kani exit=0 +FORMAL-SKIP: kani not yet implemented — roadmap 15.3.1 adds src/frame Kani smoke harnesses +kani strict exit=1 +... +``` + +Wider gates (sequential): + +```bash +make check-fmt 2>&1 | tee /tmp/check-fmt-wireframe-$(git branch --show-current).out +make lint 2>&1 | tee /tmp/lint-wireframe-$(git branch --show-current).out +make test 2>&1 | tee /tmp/test-wireframe-$(git branch --show-current).out +``` + +## Validation and acceptance + +Acceptance is behavioural: + +1. Plumbing valid: `mbake validate Makefile` prints `✓ Makefile: Valid syntax` + and exits `0`; `shellcheck scripts/formal-stub.sh` is clean. +2. Each of the six targets exits `0` on a clean tree. `kani`, `kani-full`, and + `verus` print a `FORMAL-SKIP:` notice; `test-verification`, `formal-pr`, and + `formal-nightly` run the verification crate tests and pass. +3. `FORMAL_STRICT=1 make kani` (and `kani-full`, `verus`) exits non-zero — the + tripwire works. +4. Red-Green evidence: the new cases in `tests/formal_tooling.rs` fail before the + implementation (target/script missing) and pass after. +5. `make test` passes overall, including the new behavioural scenario. +6. Activation contract documented: the developers' guide states which roadmap + item replaces each stub, that the replacement must use the pinned Kani, and + that the default test suite must stay tool-free (Constraint 7). + +Quality criteria ("done" means): + +- Tests: `make test` passes; new `formal_tooling` cases and BDD scenario pass. +- Lint/format: `make check-fmt`, `make lint`, `make markdownlint` exit `0`; + `shellcheck` clean. +- Makefile: `mbake validate Makefile` exits `0`. +- Review: `coderabbit review --agent` reports no outstanding concerns. + +Quality method: run the gates sequentially from the repository root, teeing each +to `/tmp`, and review the logs. Run CodeRabbit only after the deterministic gates +are green. + +## Idempotence and recovery + +All steps are re-runnable. The Makefile edits are additive (new targets, a few +variables, an extended `.PHONY` line); re-applying them is a no-op once present. +The stub script and the stub recipes have no side effects beyond a stderr line. +If a recipe breaks `mbake`, revert the Makefile hunk with +`git checkout -- Makefile` and re-apply carefully, watching for tab/space +corruption. The test additions are independent and can be reverted in isolation. +No destructive operations are involved. + +## Artifacts and notes + +Record, on completion: the baseline and red/green transcripts; the clean-tree +stub transcript including the `FORMAL_STRICT=1` non-zero exits; and the final +`make test` summary line (counts passed). + +## Interfaces and dependencies + +Dependencies (roadmap): 15.1.2 (the `wireframe-verification` crate, present) and +15.1.3 (pinned tool metadata and the four prover-tools targets, present). No new +external crates. No `Cargo.toml` changes. + +`scripts/formal-stub.sh` (new; leading spaces shown for readability): + +```sh +#!/bin/sh +# Placeholder runner for formal-verification Make targets whose real harnesses +# or proofs arrive in later roadmap items. Prints a structured skip marker and +# exits 0, or exits non-zero when FORMAL_STRICT is set so CI can assert that a +# target which should now be real is not still skipping. +set -eu + +target="${1:?target name required}" +shift +message="$*" + +printf 'FORMAL-SKIP: %s not yet implemented — %s\n' "$target" "$message" >&2 + +if [ -n "${FORMAL_STRICT:-}" ]; then + exit 1 +fi +exit 0 +``` + +Proposed Makefile additions (authoritative for this milestone; the six target +names, the aggregate composition, and the `FORMAL_STRICT` semantics are the +contract). Recipes shown with leading spaces — they MUST be real tabs: + +```make +VERIFICATION_CRATE ?= wireframe-verification +FORMAL_STUB ?= ./scripts/formal-stub.sh +FORMAL_STRICT ?= +export FORMAL_STRICT + +test-verification: ## Run the Stateright verification crate tests + RUSTFLAGS="-D warnings" $(CARGO) test -p $(VERIFICATION_CRATE) $(BUILD_JOBS) + +kani: ## Run Kani smoke harnesses (stub until roadmap 15.3.1) + @$(FORMAL_STUB) kani "roadmap 15.3.1 adds src/frame Kani smoke harnesses" + +kani-full: ## Run every Kani harness (stub until roadmap 15.3.x) + @$(FORMAL_STUB) kani-full "roadmap 15.3.x adds the full Kani harness set" + +verus: ## Run Verus proofs (stub until roadmap 15.5.2) + @$(FORMAL_STUB) verus "roadmap 15.5.2 adds verus/wireframe_proofs.rs" + +formal-pr: test-verification kani verus ## Fast pull-request formal gate + +formal-nightly: test-verification kani-full verus ## Deeper scheduled formal gate + +formal: formal-pr ## Default formal suite (alias for the PR gate) +``` + +Notes: + +- `formal-pr` deliberately does not depend on `check-kani-version`; that target + needs Kani installed and would violate the tool-free clean-tree criterion + (Constraint 6). +- The aggregates assume serial execution; `make -j formal-pr` would race + `test-verification` against the stubs harmlessly, but the documented contract + is serial. + +Test interfaces that must exist at the end of the milestone: + +- `tests/common/formal_tooling_support.rs`: hardened `has_phony_target`; new + `target_prerequisites`; new `run_make` (real execution capturing status and + stderr, honouring `FORMAL_STRICT`). +- `tests/formal_tooling.rs`: the six new `rstest` case sets described in Stage B. +- `tests/fixtures/formal_tooling.rs`: + `FormalToolingWorld::verify_formal_execution_targets(&self) -> TestResult`. +- `tests/features/formal_tooling.feature`: the execution-targets scenario with + matching step definitions. + +## Revision note + +- Change: pivoted from self-activating skip guards (grep/file-existence/sub-make) + to explicit stubs via `scripts/formal-stub.sh`, added `FORMAL_STRICT=1` and the + `FORMAL-SKIP:` marker, dropped the premature `KANI_*` variables and the + `stateright` alias, kept the `formal` alias, and rewrote the test strategy to + add a `target_prerequisites` helper and harden `has_phony_target`. +- Why: a Logisphere design-review panel found the guarded design too clever, an + outlier versus sibling repos, and silently failure-prone (false green), and + found the existing test helpers unable to assert the prerequisite-only + aggregates or a wrapped `.PHONY`. +- Effect on remaining work: implementation is simpler and tool-free; activation + becomes an explicit recipe edit owned by 15.3.x/15.5.x, guarded by the + `FORMAL_STRICT` tripwire and Constraint 7. Awaiting user approval before + Stage A.