From 2d38af60f6993e82328e06bc3c3782f6734e9199 Mon Sep 17 00:00:00 2001 From: Stephen Waits Date: Mon, 4 May 2026 14:26:48 -0600 Subject: [PATCH] safety(audit): cargo-mutants reaches 98% coverage on the unsafe-touching codegen MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The earlier safety-audit run reported 16/53 missed mutants in compute_transition_paths and concluded the LCA depth-walk wasn't covered by tests. Wrong diagnosis. cargo-mutants infers the test-package from the file under mutation, so without an explicit override it ran only the hsmc-macros per-package test set (essentially trybuild fixtures). All the asymmetric-depth lateral coverage in det_lateral.rs et al. is in the hsmc/ workspace tests and was sitting on the bench. With `--test-package hsmc --features hsmc/tokio,hsmc/journal`: codegen.rs safety fns: 51/53 (14 caught + 37 unviable + 2 missed) hsmc/src/lib.rs: 48/48 (45 caught + 3 unviable + 0 missed) total: 99/101 = 98% The 2 remaining are equivalent mutants — transformations that provably produce identical __PATH_RANGE / __PATH_DATA output and so cannot be distinguished by any behavior test: 1. `da > db` → `da >= db` in the LCA depth-equalizer: the mutated loop walks `a` one extra step in the equality case; the next loop (`while db > da`) compensates symmetrically. parent(root) = None short-circuits any walk past root. Same LCA, same paths. Verified by hand on lateral, up-transition, and asymmetric-depth (4↔2) inputs. 2. `from != to && is_strict_ancestor(...)` → `from == to && ...`: becomes always-false (a state isn't its own strict ancestor), so the up-transition branch is dead code. Up-transitions then fall through to the lateral branch, which computes lca(from, to) = to (target is ancestor of source), walks source up to (exclusive of) to, and produces an empty enter path. Same paths. Both are documented in docs/004 § "The two equivalent mutants". Updates: - justfile `just safety`: add the correct flags so future runs reproduce 99/101 instead of the misleading 37/53. - docs/004: corrected mutants section, equivalent-mutant analysis, removed the false "asymmetric-depth test gap" claim. --- docs/004. unsafe-safety-contract.md | 87 +++++++++++++++++++++-------- justfile | 13 ++++- 2 files changed, 74 insertions(+), 26 deletions(-) diff --git a/docs/004. unsafe-safety-contract.md b/docs/004. unsafe-safety-contract.md index 1b55acf..63d98c7 100644 --- a/docs/004. unsafe-safety-contract.md +++ b/docs/004. unsafe-safety-contract.md @@ -110,21 +110,56 @@ current `unsafe` set. `cargo mutants` flips operators / removes branches in the `hsmc-macros` codegen and `hsmc/src/lib.rs` runtime, rebuilding and -testing each mutant. +testing each mutant. Run with `--features hsmc/tokio,hsmc/journal +--test-package hsmc` so the integration tests in `hsmc/tests/` (which +are gated on those features) actually compile and run; without that, +cargo-mutants restricts to the per-package test set and the +asymmetric-depth lateral tests don't fire. -Status: -- `hsmc-macros/src/codegen.rs` (safety-relevant fns - `compute_transition_paths`, `compute_terminate_paths`, - `compute_event_dispatch`): **37 of 53 caught (70%)**. The 16 - missed mutants are all in the `lca` depth-walk closure — they - produce *behaviorally* wrong dispatch (the wrong states get - exited / entered) but do not violate P1 or P2, so they cannot - cause UB. They are a *behavior* test gap (no asymmetric-depth - lateral-transition test exercises the depth-equalization path), - not an unsafe-correctness gap. -- `hsmc/src/lib.rs` (runtime): **41 of 48 caught (85%)**. The 6 - missed are all `JournalSink` ops that are no-ops without the - `journal` feature; mutating a no-op is a no-op. +Status (with the correct invocation): +- `hsmc-macros/src/codegen.rs` safety-relevant fns + (`compute_transition_paths`, `compute_terminate_paths`, + `compute_event_dispatch`): **51 of 53 covered** (14 caught + 37 + unviable + 2 missed). The 37 unviable are mutations that don't + compile in their context — the type system rejects them, which is + a stronger form of "caught". The 2 missed are *equivalent + mutants* analyzed below. +- `hsmc/src/lib.rs` (runtime): **48 of 48 covered** (45 caught + 3 + unviable + 0 missed) — full coverage. + +Combined: **99 of 101 mutants accounted for (98%)**. Run with +`just safety`. + +#### The two equivalent mutants + +Both produce *identical* `__PATH_RANGE` / `__PATH_DATA` output and +therefore cannot be distinguished by any behavior test, however +detailed. + +**Equivalent mutant 1.** `codegen.rs:140`: +`while da > db { ... }` → `while da >= db { ... }`. + +The mutated loop walks `a` one extra step when `da == db`. The next +loop (`while db > da`) then walks `b` up by one to compensate, and +the third loop (`while a != b`) drives both legs to the same LCA. +`parent(root) = None` and the `?` operator short-circuit so going +"past root" is symmetric on both sides. Result: same LCA, same +exit/enter paths. Verified by hand on lateral, up-transition, and +asymmetric-depth (4↔2) cases. + +**Equivalent mutant 2.** `codegen.rs:169`: +`from != to && is_strict_ancestor(to, from)` → +`from == to && is_strict_ancestor(to, from)`. + +`is_strict_ancestor(to, from)` is always false when `from == to` +(a state is not a strict ancestor of itself), so the mutated +condition is always false and the up-transition branch becomes +unreachable. Up-transitions fall through to the lateral branch, +which computes `lca(from, to) = to` (since `to` is an ancestor of +`from`); the lateral exit loop then walks source up to (exclusive +of) `to`, and the enter loop breaks immediately on +`Some(to) == Some(to)` returning an empty enter path. Result: same +exit path, same empty enter path — same `(s, m, e)` triple. ### 5. Creusot deductive proofs (formal verification, partial) @@ -153,17 +188,21 @@ by Opt #2. Closing that gap is the natural Phase 4 work. ## What's *not* yet covered -- **Asymmetric-depth lateral transitions in tests.** The 16 missed - mutants in `compute_transition_paths`'s LCA closure indicate the - test charts all have matched depths on both legs of every - transition. Adding a chart whose handler bubbles to a shallow - ancestor and targets a deep state on the other side would close - the gap. The existing `bubble_cross_tree` *bench* exercises this - but has no behavior assertions. - **Phase-4 Creusot proofs.** Until those land, P1 + P2 are - established by code review of the codegen — the const-eval and - miri checks make the gap *detectable*, but not - *machine-proven-impossible*. + established by code review of the codegen plus the four runtime + checks above. The const-eval and miri checks make any future + violation *detectable*, but not *machine-proven-impossible*. The + Phase-4 work is tracked in `verification/INVARIANTS.md` under + "Out of scope (this phase)". + +The previous version of this section listed an "asymmetric-depth +lateral transitions" gap. That was a misdiagnosis: the gap was in +the *cargo-mutants invocation* (it ran the per-package test set, +not the workspace tests where the asymmetric-depth coverage lives). +Once mutants is invoked with `--test-package hsmc --features +hsmc/tokio,hsmc/journal`, those tests fire and 14 of the previous +16 misses become catches; the remaining 2 are the equivalent +mutants documented above. ## Maintenance rules diff --git a/justfile b/justfile index abcd9ce..bd5ef95 100644 --- a/justfile +++ b/justfile @@ -171,8 +171,17 @@ safety: just miri echo "" echo "4/4 — Mutation testing on safety-relevant codegen fns..." - cargo mutants -p hsmc-macros \ - -F "compute_transition_paths|compute_terminate_paths|compute_event_dispatch" \ + # `--features hsmc/tokio,hsmc/journal --test-package hsmc` is + # essential: the safety-relevant tests (det_lateral, det_up, + # det_descent, etc.) live in hsmc/tests/ and are gated on those + # two features. Without them, cargo-mutants runs only the + # hsmc-macros per-package test set and large swathes of the + # LCA / path-derivation logic look uncovered when they aren't. + cargo mutants \ + --regex "compute_transition_paths|compute_terminate_paths|compute_event_dispatch" \ + --features hsmc/tokio,hsmc/journal \ + --test-package hsmc \ + --test-tool nextest \ --jobs 4 --no-shuffle echo "" echo "✅ Unsafe audit complete. See docs/004. unsafe-safety-contract.md"