Item 5's guard is reachable in ten lines, and a stub handoff

This commit is contained in:
Joseph Ferano 2026-09-13 22:36:14 +07:00
parent b1cc67b36f
commit b0f21ae513
2 changed files with 59 additions and 0 deletions

49
HANDOFF-x86-guards.md Normal file
View File

@ -0,0 +1,49 @@
# Handoff — the two unreached guards in `lib/x86.ml`
Branch `dev-loop`, worktree `agent-ab6daf83988bee428`, on top of `b1cc67b`. This lane is items 4 and 5 of
`HANDOFF-x86-rt.md`'s "What remains": the `flan_transfer_fail` branch in the transfer exit, and the
`"defers on a transfer path nothing reaches"` refusal beside it. Both were described as guards that exist so that
if the reasoning behind them is wrong they say so, and that no program in the corpus reaches. The question this
lane was given is whether they are correct or merely untested.
**Status: in progress.** Item 5 is answered and the answer is that the guard is wrong. Item 4 is being probed.
## Item 5 — `"%s has defers on a transfer path nothing reaches"` is reachable, and it is a real hole
`lib/x86.ml:2234`. It fires when a function has function-level defers (`fn.Tast.fdefers <> []`) and `f.unwound` is
false — that is, when nothing in the body ever named the function's own transfer exit as a landing pad. `f.unwound`
is set in exactly one place, `current_pad` (`lib/x86.ml:757`), when the pad stack is empty, and `current_pad` has
exactly one caller that matters here: `guard`, the two-load-and-branch check emitted after every Flan call. So the
condition reads, in source terms: **a function that has a defer and makes no guarded call at all** — neither in the
body nor in the defers, which are spliced onto the normal exit path and so are lowered as part of the body.
That is not an exotic shape. `spike/x86/g5.flan` is ten lines and reaches it:
```
x86: quiet has defers on a transfer path nothing reaches
```
exit status 3, from
```flan
(defn quiet [n i32] i32
(defer (set log (+ log 1)))
(* n 2))
```
The same program compiles and runs under LLVM. `lib/emit.ml`'s `emit_fn` (~line 2283) has no counterpart to this
refusal: it writes the whole transfer exit under `if f.unwound then`, so when nothing can unwind the block and the
defers on it are simply not emitted. The two backends agree about the *reasoning* — the defers on that path are
dead — and disagree only about what to do with the observation. `x86.ml` refuses; `emit.ml` drops them.
**The correct lowering is to drop them,** matching `emit.ml`. The reasoning behind the guard is sound; the guard
itself is not, because "nothing reaches that path" is the ordinary case for any leaf function with a defer, not a
sign that something has gone wrong.
## Item 4 — the `flan_transfer_fail` branch
(being probed; see below)
## Files
(to be filled in)

10
spike/x86/g5.flan Normal file
View File

@ -0,0 +1,10 @@
(defvar log i64)
(defn quiet [n i32] i32
(defer (set log (+ log 1)))
(* n 2))
(defn main [] i32
(print (quiet 21)) (println "")
(print log) (println "")
0)