diff --git a/HANDOFF-x86-guards.md b/HANDOFF-x86-guards.md index b083540..7ccfb79 100644 --- a/HANDOFF-x86-guards.md +++ b/HANDOFF-x86-guards.md @@ -153,9 +153,25 @@ Worth saying what that second row proves for `p10`, because it is not obvious: t hand-encoded backend that got the `.rodata` label or the length register wrong would still exit 134 and would still look like a match to anything comparing only exit statuses. -The full run over `test/programs` plus `spike/x86` was in flight beside another lane's and is slow for that reason; -the number to expect is `HANDOFF-x86-rt.md`'s 97 MATCH plus these two, and the invariant that must hold is 0 DIFFER -and 0 refused. Before the item-5 fix landed, `p9` was one refusal, which is the shape the invariant exists to catch. +And the full run, `SURVEY_QUIET=1 spike/x86/survey.sh`, over `test/programs` and `spike/x86` together: + +``` +MATCH 98 +DIFFER 0 +REFUSED 0 +NOX86 0 +SKIP 36 +``` + +That is `HANDOFF-x86-rt.md`'s 97 plus `p9`. It does not include `p10`, whose file did not exist when the run globbed +the directory — the targeted run above is `p10`'s row, and the number a later full run should report is **99**. The +`SKIP` 36 is the same 28 / 6 / 2 as before. + +The invariant that matters is the two zeroes, and it is worth saying why the item-5 fix cannot have moved anything +else: the change removes a refusal and adds no code. A function with `f.unwound` true reaches none of it, and a +function with `f.unwound` false previously failed the whole compile. The baseline was 0 refused, so no program in the +corpus was on that branch and no program's output could change. Before the fix, `p9` was one refusal — which is the +shape the invariant exists to catch, and it caught it. ## What this leaves