diff --git a/HANDOFF-x86-guards.md b/HANDOFF-x86-guards.md index a6fa101..b083540 100644 --- a/HANDOFF-x86-guards.md +++ b/HANDOFF-x86-guards.md @@ -137,6 +137,26 @@ has for the case, and the corpus simply had no program that started a transfer f `lib/emit.ml`, `lib/check.ml` and `runtime/flan_rt.c` were not modified; no change to any of them was needed. +## The survey + +`bash spike/x86/survey.sh p9 p10` — the two new probes, both sides, built and run: + +``` +MATCH 2 +DIFFER 0 +REFUSED 0 +``` + +Worth saying what that second row proves for `p10`, because it is not obvious: the survey hands the compiler an +**absolute** `$src`, so the location string in the stderr both binaries print is the absolute path, not the +`spike/x86/…` seen by hand. The two are byte-identical anyway, which is the comparison that matters — a +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. + ## What this leaves Items 1, 2, 3, 6 and 7 of `HANDOFF-x86-rt.md` are untouched and still stand. Two smaller things this lane turned up