Summary
The core-proof harness's component-A pilot (branch feat/coreproof-pilot-a, R60/R61 pass-bar
round 3) cannot re-find the #645 stale-per-CPU-identity-capture defect class through its
coreproof_mut_cpu_identity mutation. This is a harness predicate/site-labelling gap, not a
claim that #645 (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):
#645 stale per-CPU identity capture | MISSED | 194s, 15/15 clean, cov=cpu_identity nonzero (23474) — a real, non-vacuous miss
The mutation site executes 23,474 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_cpu_identity*.log,
round3/leg1_progress.log on the pilot branch (not committed — pass-bar working evidence).
Root cause, as diagnosed in fix3-notes.md
The mutated field is read once at boot, before any concurrent scheduling activity exists on
this tree. The harness's perturbation/adversarial peers only begin operating after that read
has already happened, so there is no window in which a race on the mutated field can be
observed by any predicate this harness currently declares.
What's needed
Either:
- A different mutation-injection point for this defect class — one sited where a concurrent
scheduling event can actually observe the corrupted identity (i.e., a read that happens
after peers are live, not only at boot), or
- An explicit, documented acknowledgment that this defect class's current site is inert under
this harness's stimulus shape, with the mutation feature scoped accordingly (e.g. excluded
from the "6 mutations, all catchable" pass-bar count until re-sited).
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 #645 fix (already closed, merged in PR #645).
Summary
The core-proof harness's component-A pilot (branch
feat/coreproof-pilot-a, R60/R61 pass-barround 3) cannot re-find the #645 stale-per-CPU-identity-capture defect class through its
coreproof_mut_cpu_identitymutation. This is a harness predicate/site-labelling gap, not aclaim that #645 (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):The mutation site executes 23,474 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_cpu_identity*.log,round3/leg1_progress.logon the pilot branch (not committed — pass-bar working evidence).Root cause, as diagnosed in
fix3-notes.mdThe mutated field is read once at boot, before any concurrent scheduling activity exists on
this tree. The harness's perturbation/adversarial peers only begin operating after that read
has already happened, so there is no window in which a race on the mutated field can be
observed by any predicate this harness currently declares.
What's needed
Either:
scheduling event can actually observe the corrupted identity (i.e., a read that happens
after peers are live, not only at boot), or
this harness's stimulus shape, with the mutation feature scoped accordingly (e.g. excluded
from the "6 mutations, all catchable" pass-bar count until re-sited).
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 #645 fix (already closed, merged in PR #645).