Post-#381 audit of all 18 required contexts: 11 have a path to green without measuring

[avrabe]

#381 was a required status check that spent four months reading a path that never existed, scoring every run as 0 survivors, and reporting green. The property that made it invisible was not that it was wrong — it was that its failure mode produced the flattering reading. 0 is the best possible survivor count. Nothing about a broken run looked different from a good one.

That is not a property of mutation testing. It is a property of any gate whose "nothing happened" renders identically to "it worked". So all 18 required contexts were audited against one question:

Can this check report success without having measured the thing its name claims?

Three clean-room agents, no shared framing, each given a slice. Every verdict below was reached by executing the gate's own logic against constructed inputs — mutating each guard to a no-op and checking whether CI would notice. Where something was reasoned rather than executed, it says so.

Result

11 of 18 have a path to green without measuring. Four are live today.

#	Required context	Verdict	Mechanism
1	Bench compile smoke	✅ sound	declared [[bench]] targets make a missing file exit 101
2	Cargo Deny	⚠️ narrow	[bans] multiple-versions = "warn", wildcards = "allow" → check bans cannot fail; advisories skipped (documented, covered by RustSec job)
3	Clippy	⚠️ narrow	--workspace misses the 3 nested workspaces — see #383
4	Code Coverage	❌ vacuous	cargo llvm-cov with no --fail-under-*; upload is fail_ci_if_error: false. Cannot fail for a coverage reason — it duplicates Test
5	Codegen compile oracle	✅ sound	best-defended job here — real assert!(status.success()), per-field distinct sentinels, if n != 1 { bail! } on the source patch
6	Detect changed paths	⚠️ fails open	#384
7	Detect changed paths (proofs)	⚠️ fails open	#384 — byte-identical clone
8	Format	❌ live false-green	#383 — green right now over unformatted tracked code
9	Fuzz smoke (60s/target)	✅ sound	3 targets hard-coded; nothing asserts they match cargo fuzz list
10	Lean proof typecheck	❌ vacuous (sorry sub-gate)	#385 — 12 sorrys, 12 self-exempted, 0 enforced. lake build itself is sound
11	Miri	⚠️ misaimed	guards spar-hir-def, the one crate with zero unsafe; the 6 crates that have it are never Miri-checked. Filter -- instance:: exits 0 if renamed
12	Mutation Testing	❌ vacuous	#381 — fixed, pending merge
13	Proptest (extended)	✅ sound	10× cases is real; degrades silently to 100 on a bad env var. Incidentally the only job that runs doctests
14	Rivet validate (artifacts)	⚠️ narrow	passes on an empty artifact set (881 → 0 is indistinguishable); duplicate IDs, missing title, typo'd field names are all non-fatal in the pinned v0.4.3
15	Security Audit (RustSec)	✅ sound	engine mutation-proved; the rustsec/audit-check@v2 wrapper was reasoned, not executed
16	Supply Chain (cargo-vet)	✅ sound	mechanically fail-closed (exit 255 proved); 207 exemptions vs 4 audits + empty imports.lock is a policy weakness, not a gate defect
17	Test	❌ vacuous for doctests	cargo nextest has no doctest support at all; ~25 executable doctests never run under this name
18	Verification Gate	❌ vacuous on demand	skip-as-pass + author-controlled Verify-Filter: — see #358

The four that are live

• Format check is green on unformatted tracked code: cargo fmt --all covers 1 of the repo's 4 workspaces #383 Format — cargo fmt --all covers 1 of 4 workspaces; fuzz/fuzz_targets/fuzz_codegen_roundtrip.rs:32 is unformatted on main and the check is green.
• Lean 'Fail on sorry' gate enforces zero obligations: all 12 sorrys are self-exempted by '-- TODO' #385 Lean sorry gate — 12 bare sorrys, all exempted by a self-service -- TODO suffix. Prints "No sorrys — gate green."
• Instance model array support (subcomponent and feature arrays) #4 Code Coverage — no threshold anywhere. It runs for ~25 minutes and cannot fail for the reason it exists.
• LSP: code actions, formatting, and rename refactoring #17 Test doctests — covered only because Proptest (extended) happens to run cargo test --workspace. Switching that one job to nextest would silently delete doctest coverage with nothing noticing.

The recurring shapes

Four distinct mechanisms, one symptom:

1. Scope narrower than the name. --all ≠ the repo (Format check is green on unformatted tracked code: cargo fmt --all covers 1 of the repo's 4 workspaces #383). --workspace ≠ the repo. -p one-crate ≠ Miri coverage. cargo test <substring> exits 0 on zero matches — 13 of the 20 verification artifacts rely on exactly that.
2. The error path is the permissive path. || true + set -e being inert inside an if (Detect changed paths fails open two ways, skipping 11 of 18 required contexts (cloned into proofs.yml) #384). grep failing into a default. Mutation Testing gate reads a path cargo-mutants never writes — 4 months of vacuous green (210 survivors reported as 0) #381 itself.
3. Absence renders as success. Zero survivors, zero sorrys, zero artifacts, zero matched tests, an empty report — every one is the ideal reading.
4. A gate with no configured failure mode. multiple-versions = "warn". cargo llvm-cov with no threshold. A check that runs, costs money, and is structurally incapable of red.

The general fix

Every gate should print a positive count of what it examined, and fail when that count is implausible:

Surviving mutants: 210  (caught 603, unviable 793, timeout 2)   # not "0"
0 sorrys found, 0 allowlisted, 47 files scanned                 # not "gate green"
4 workspaces formatted                                          # not silence
881 artifacts validated                                         # not "PASS"

A count cannot be produced by a broken read. That is the whole trick, and it is what tools/check_mutants_report.py now does for #381 — including a cross-check of its own number against a second, independent derivation.

The second half is the tools/check_*.py convention already in use: put the logic in a script with a --self-test decision table, run the self-test as a step before the real check, and include the historical regression as a table row. Inline workflow shell is only testable by pushing, and a log cannot distinguish "0 findings" from "0 files read".

Remaining work (split into issues as they are picked up)

• Format check is green on unformatted tracked code: cargo fmt --all covers 1 of the repo's 4 workspaces #383 — Format / Clippy workspace scope
• Detect changed paths fails open two ways, skipping 11 of 18 required contexts (cloned into proofs.yml) #384 — change-filter fails open (both copies)
• Lean 'Fail on sorry' gate enforces zero obligations: all 12 sorrys are self-exempted by '-- TODO' #385 — Lean sorry gate + MinPlusPwa.lean in no build target
• Mutation Testing gate reads a path cargo-mutants never writes — 4 months of vacuous green (210 survivors reported as 0) #381 — mutation gate path (fix written, pending merge)
• Code Coverage: add --fail-under-lines at the measured floor, or stop requiring it
• Test: add cargo test --workspace --doc
• Miri: point at the 6 crates that contain unsafe; assert a test count
• Verification gate: return 1 when passed_count == 0; drop author-controlled scope (Verification Gate scope is stale: 20 of 161 feature artifacts checked, per-PR override never used #358)
• cargo test <substring> in 13 of 20 verification artifacts → --exact or assert a count
• Rivet validate: artifact-count floor; duplicate-ID check until the rivet pin can advance
• Cargo Deny: decide whether multiple-versions should be deny (6 duplicates today) or drop the pretence
• Fuzz smoke: assert the hard-coded target list equals cargo fuzz list
• Codegen compile oracle / Miri: assert -- --ignored --list and -- <filter> --list are non-empty

Honest scope

This audit covers the 18 required contexts on main. It does not cover nightly workflows, release workflows, or the release-tag path — #366 and #372 came from the same species of question and are already filed. Nothing here says the code is bad; it says the evidence is thinner than the green ticks imply. Several gates (Codegen compile oracle in particular) were actively hardened against exactly this and held up under attack.

Refs #381, #382, #358, #366, #372.

[avrabe]

Measured: the Miri item, and a correction to this issue's own count

Two of the checklist items are measurable without a build, so I measured them
before writing the fix. One of them contradicts a number in the table above.

Miri: point at the 6 crates that contain unsafe — there are not 6

git grep -w unsafe origin/main, every hit classified by hand:

Memory-safety unsafe — 5 sites across 4 crates. All five are the identical
rowan round-trip:

site	expression
crates/spar-annex/src/ba/syntax_kind.rs:314	transmute::<u16, BaKind>(raw.0)
crates/spar-annex/src/emv2/syntax_kind.rs:338	transmute::<u16, Emv2Kind>(raw.0)
crates/spar-cli/src/assertion/syntax.rs:101	transmute::<u16, ExprSyntaxKind>(raw.0)
crates/spar-syntax/src/language.rs:16	transmute::<u16, SyntaxKind>(raw.0)
crates/spar-sysml2/src/language.rs:16	transmute::<u16, SyntaxKind>(raw.0)

Edition-2024 unsafe — 2 sites, 1 crate, tests only.
crates/spar-mcp/tests/in_process_tests.rs:270,282 — env::set_var /
env::remove_var. That is a thread-safety obligation, not a layout one; it is
not the hazard class Miri's borrow-stack checker is pointed at.

Grep false positives — 2. crates/spar-codegen/src/lib.rs:261 is the string
"unsafe" inside the Rust reserved-word list used for identifier escaping, and
rust_gen.rs:415 is a comment. spar-codegen contains no unsafe code. That is
the most likely origin of the "6".

Not a big error, but this issue's whole thesis is that unverified numbers read as
green, so its own numbers should be re-derived rather than carried.

Confirmed separately: spar-hir-def — Miri's only target — contains zero
unsafe. git grep -c -w unsafe -- crates/spar-hir-def returns nothing. That
part of the table is exactly right.

The retarget is not as cheap as the checklist implies

All five transmute sites are in crates that depend on rowan, and the current
job comment says the -- instance:: filter exists specifically to dodge
rust-analyzer/rowan#192 (a retag issue in rowan's custom Arc, upstream, not
ours). So the filter is not incidental — it is load-bearing avoidance, and
"just point Miri at the crates with unsafe" will very likely trip the same
upstream UB on day one and turn a required context red for a reason we cannot fix.

That makes the honest options:

1. -Zmiri-tree-borrows instead of the default stacked-borrows. Tree Borrows
   accepts several patterns stacked borrows rejects, and rowan#192 is a retag
   complaint — plausibly passes, but this is a guess and must be measured, not
   asserted.
2. Leave rowan out of the process entirely: the transmute's real precondition is
   "raw.0 is a valid discriminant". Give each SyntaxKind impl a unit test that
   walks the full 0..=LAST range plus a deliberately out-of-range value, and run
   that under Miri. It exercises the actual UB without constructing a rowan tree.
3. Concede it: if neither works, the required context should say what it really
   covers rather than carry a name it does not earn.

I lean 2 — it is the only one that tests the obligation directly, and it is a
detector in this issue's own preferred shape: a valid discriminant and an invalid
one must render differently.

The count assertion has a floor now

cargo test -p spar-hir-def --lib -- instance:: --list → 33 tests, 0 benchmarks.
So the --list non-empty assertion on the last checklist line has a concrete
number to assert against rather than merely "non-empty".

Fuzz smoke: the two lists agree today, and nothing holds them there

fuzz/Cargo.toml declares exactly three [[bin]] targets — fuzz_aadl_parse,
fuzz_scheduler_solver, fuzz_codegen_roundtrip. ci.yml:356-361 runs those
same three. They match right now.

The shape is worth naming though: they are three separately named steps, not a
loop over a list. A fourth target added to fuzz/Cargo.toml is simply never
fuzzed, and there is no step that could fail to say so. Nothing regresses; it just
silently never starts. Same species as everything else in the table — absence
renders as success.

[avrabe]

Second measured pass — three more numbers moved, and one item is now its own issue

Same method: re-derive rather than carry.

cargo test <substring> → filed as #388, and it is worse than "narrow"

The checklist says "13 of 20 verification artifacts". Measured:
artifacts/verification.yaml holds 149 cargo test invocations, 105 of
which carry a name filter.

And it is not a latent risk. Seven of them cite test names that have never
existed in this repository — git log -S across all refs finds zero commits
ever adding or removing them. Five are VAL-R1–VAL-R5, marked
implemented, closing the V for six RENDER-REQ-* and four ARCH-R*.

Executed: cargo test -p spar-wasm -- topology → 0 passed; 0 failed; 7 filtered out, exit 0. run_verification.py:74 scores a step by returncode == 0, so
that is recorded as a pass.

Full evidence in #388. Moving that checklist line there.

Cargo Deny: multiple-versions — 18 duplicates, not 6

From Cargo.lock on main (214 distinct crates):

bitflags 1.3.2, 2.11.0            petgraph 0.6.5, 0.7.1
fixedbitset 0.4.2, 0.5.7          r-efi 5.3.0, 6.0.0
foldhash 0.1.5, 0.2.0             rustc-hash 1.1.0, 2.1.2
getrandom 0.3.4, 0.4.2            wasm-encoder 0.244.0, 0.245.1
hashbrown 0.14.5, 0.15.5, 0.16.1  wasm-metadata 0.244.0, 0.245.1
itertools 0.10.5, 0.13.0          wasmparser 0.244.0, 0.245.1, 0.246.2
wit-bindgen{,-core,-rust,-rust-macro} 0.51.0, 0.53.1
wit-component 0.244.0, 0.245.1    wit-parser 0.244.0, 0.245.1, 0.246.2

Ten of the eighteen are one cluster: spar-wasm pins wit-bindgen = "0.53"
directly while the 0.51 line arrives transitively, dragging three generations of
wasmparser/wit-parser with it. So "flip it to deny" is not a config change —
it is a dependency-unification task with a real cost. Worth knowing before the
decision, since the issue currently prices it at 6.

deny.toml has no [graph] section, so cargo-deny includes dev-dependencies and
its own count should land close to this. I have not run cargo-deny itself.

Incidentally [licenses] is fail-closed (cargo-deny v2 denies anything outside
allow). [bans] is the only section in that file with no configured failure mode.

Code Coverage — floor measured, plus a defect the audit did not record

codecov, branch main: 89.03 % lines — 78 288 / 87 930, 9 642 misses, 182
files, branches: 0.

Two things beyond "no --fail-under-*":

1. The percentage never appears in the job log at all. ci.yml:236-237 is
   --lcov --output-path and --html --output-dir; neither prints a summary. The
   number above had to be fetched from outside the gate.
2. It runs the full instrumented test suite twice — once per output format.

One restructure fixes cost, visibility and the gate together:

cargo llvm-cov --workspace --no-report
cargo llvm-cov report --lcov --output-path lcov.info
cargo llvm-cov report --html --output-dir coverage-html
cargo llvm-cov report --summary-only --fail-under-lines <N>

<N> must not be taken from codecov's 89.03. Codecov applies its own path
fixes and ignores, so a threshold calibrated on it would be enforcing against a
different denominator than the one it measures. First PR prints the summary and
reads N off cargo-llvm-cov's own output.

Rivet validate: the artifact-count floor

984 artifacts exist across all tracked YAML; rivet.yaml sources: covers
artifacts/ (432) + safety/stpa/ (458) ≈ 890. The remaining 94 live in
safety/analysis.yaml (71) and safety/requirements.yaml (23), which are outside
sources: — both are frozen 2026-03-10 snapshots and strict subsets of their
safety/stpa/ counterparts. Measured in detail on #375; the answer there is
delete, not add.

So the floor for the count assertion is ~890, and it should be asserted against
what rivet reports, not against a file-walk — the two differ by exactly the 94.

Running tally of numbers in this issue that moved on re-derivation

claim	as written	measured
Miri: crates containing unsafe	6	4 in src (+1 in tests); 2 grep false positives
cargo test <substring> artifacts	13 of 20	105 filtered of 149; 7 provably vacuous
Cargo Deny duplicates	6	18

None of these weakens the issue — every one makes its own case stronger. But the
thesis here is that unverified numbers read as green, so the tally belongs on the
record.