plan: pick the replace unit by its write set, not its name (lane CR's lesson)
This commit is contained in:
parent
d12459d1e1
commit
3bfde5a70d
1 changed files with 9 additions and 0 deletions
|
|
@ -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).
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue