core-proof harness: #609 masked-reclaim-lock mutation only reintroduces half the original defect (companion bare-Mutex hazard already closed by #632)

[ryanbreen]

Summary

The core-proof harness's component-A pilot (branch feat/coreproof-pilot-a, R60/R61 pass-bar
round 3) cannot re-find the #609 non-irqsave-lock-in-masked-reclaim defect class through its
coreproof_mut_masked_lock mutation. This is a harness predicate/site-labelling gap, not a
claim that #609 (already fixed on main) has regressed.

Trial evidence

Leg 1 (per-mutation hunt, cortex-a72, mode=adversarial, 15 seeds, --require-cov,
docker/qemu/run-coreproof-gate.sh):

#609 non-irqsave lock in masked reclaim | MISSED | 192s, 15/15 clean, cov=masked_lock nonzero (77) — a real, non-vacuous miss

The mutation site executes 77 times inside the measured window (nonzero coverage, so this is
not a vacuous "site never reached" miss) but never raises a [COREPROOF:VIOLATION:...] record
across 15 fresh seeds. Leg 2's single-boot arm shows the same result (NO, consistent with leg 1 miss). Full logs: round3/leg1_coreproof_mut_masked_lock*.log, round3/leg1_progress.log
on the pilot branch (not committed — pass-bar working evidence).

Build-notes.md's pre-registered prediction, made before this mutation was ever booted, called
this outcome: "coreproof_mut_masked_lock (#609) historically presented as a hang, not a
marker. If it hangs the boot it will show up as a missing RUN record — a gate failure, but not
a [COREPROOF:VIOLATION:...] naming a predicate, which is what the pass bar requires." In
this run it did not hang, and instead landed as a clean, non-vacuous miss.

Root cause, as diagnosed in fix3-notes.md

The originally planted mutation only reintroduces half of the real-world #609 defect. The
other half — a bare-spin::Mutex orphan-lock hazard on the bitmap — was independently fixed
by PR #632 already merged on this tree, ahead of this pilot's baseline. The planted mutation
therefore reopens a window that nothing on this tree can actually race, since the companion
hazard PR #632 closed is gone.

What's needed

The bare-spin::Mutex half of the original #609 defect needs to be faithfully reintroduced
under this mutation's own feature flag, as a deliberate scoping decision — noting that once
reintroduced, this mutation would likely present as a hang (a missing RUN record) rather than
a violation predicate, meaning the harness's missing-RUN leg, not its predicate set, is what
would need to catch it. That's a different gate shape than the other five mutations and should
be scoped explicitly rather than continuing to probe the half PR #632 already closed.

Not in scope

This issue is about the core-proof harness's predicate/site coverage only. It makes no claim
about the production state of the underlying #609 fix (already closed by PR #632).