JosephFerano/flan
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

The targeted survey: both probes match, and what p10 proves

Browse Source
This commit is contained in:
Joseph Ferano 2026-09-13 22:46:55 +07:00
parent 624a94af7b
commit 4b9a6c0852
1 changed files with 20 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

20
HANDOFF-x86-guards.md
View File

@ -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