plan: pick the replace unit by its write set, not its name (lane CR's lesson)

This commit is contained in:
alex 2026-09-09 10:39:09 -04:00
parent d12459d1e1
commit 3bfde5a70d

View file

@ -148,6 +148,15 @@ it fails if a corpus test skips.
### Track 1 — displacement: `compared → replaced`, then `modelled → compared`
**Pick the replace unit by its WRITE SET, not by its name.** Lane CR's failure is the rule's
source: our code replaced `ProcessResearch` and produced **all 13** tech-tree leaves the turn moves
— the model was right — and the oracle still missed by 16, every one written by
`OnTechResearched`, a neighbouring function. A replace boundary that splits a write set cannot
pass an oracle no matter how correct the model is. So before attempting one, enumerate the leaves
the turn moves in that area and ask which functions write them; if the answer is more than one,
the unit is the union or the attempt is wasted. The compare mode's guard spans already name the
write set — CR's five spans predicted exactly the five fields the oracle later billed.
Only `replaced` means the original's code did not run. The bar, written once: an un-instrumented
oracle first (`certified-pairs.md` format), then the same procedure with the hook in `replace`
mode and the **same hashes**, with a count from the hook proving the path executed (rule 1).