flan/HANDOFF-x86-guards.md

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 the same way — a guard that exists so that if the reasoning behind it is wrong it says so, and that no program in the corpus reaches. The question this lane was given is whether each is correct or merely untested.

The two answers are different, and that is the whole of the result. Item 4's guard is correct, and it is now reached by a program and the two backends agree about it byte for byte. Item 5's guard is wrong — not the reasoning behind it, which is sound, but the guard itself, which fires on the most ordinary function in the language.

Item 5 — "defers on a transfer path nothing reaches" is reachable in ten lines

The refusal stood at lib/x86.ml:2234. It fired when a function had function-level defers (fn.Tast.fdefers <> []) and f.unwound was false — that is, when nothing in the body ever named the function's own transfer exit as its landing pad. f.unwound is set in exactly one place, current_pad (lib/x86.ml:757), when the pad stack is empty, and the caller that matters here is 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. It is any leaf function with a defer. spike/x86/p9-dead-defers.flan is ten lines:

(defn quiet [n i32] i32
  (defer (set log (+ log 1)))
  (* n 2))

and before the fix it produced, at exit status 3,

x86: quiet has defers on a transfer path nothing reaches

The same program compiles and runs under LLVM and prints 42 then 1. lib/emit.ml's emit_fn (the block at ~2283) has no counterpart to the 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 agreed about the reasoning — the defers on that path are dead — and disagreed only about what to do with the observation. So this was a genuine gap of exactly the kind the survey is meant to catch, and the corpus missed it only because every test/programs function with a defer also happens to call something.

What made the fix safe rather than assumed

Dropping the defers is right only if unwound is not an under-approximation — if a function could transfer while unwound stayed false, the transfer exit would never be emitted and the unwinding frame would fall through its epilogue, which is far worse than a spurious refusal. So every site in lib/x86.ml that can leave a transfer in the channel and then continue was enumerated, by grepping the two writers (xfer_store, and chan_into for the calls that signal through it):

line	site	what it does about the pad
1098	Signal (Ssignal, …) → flan_signal	guard f
1110	Signal (Serror, …) → flan_error	guard f, then ud2
1619	bounds_call — every bounds and slice check	guard f, then ud2
1777	call_flan — every call, by name or by pointer	guard f
1822	call_native ~chan — flan_vec_at, flan_vec_as_slice	if chan then guard f
1433	emit_invoke_restart	jmp (current_pad f)
1184, 1214, 1358	the handler-bind, with-allocator and restart-case pads re-propagating	jmp (current_pad f)

Every one of them either calls guard or jumps to current_pad outright, and both touch current_pad. An ordinary foreign call gets neither, correctly: a transfer cannot cross a C frame, because the channel is not in the SysV signature C sees. So unwound is false exactly when no transfer can arrive, and the defers on that exit are dead in fact and not merely by assumption.

The one shape that looks like a counterexample and is not: a function whose every call sits inside a restart-case, so that no guard ever finds an empty pad stack. It still sets unwound, because the guard sets that pad's used, which is what causes the pad to be emitted at all, and the pad's tail — line 1358, the transfer aimed further out than any clause it offers — re-propagates through current_pad with its own frame already popped off f.pads.

The edit, for the merge

lib/x86.ml, in emit_fn, the tail of the transfer-exit block. The six lines that were

  else if fn.Tast.fdefers <> [] then
    (* Nothing in this function can transfer, so the second exit has no path
       to it and the defers on it are dead. Left as a refusal rather than
       quietly dropped: if that reasoning is ever wrong, this says so. *)
    unsupported "%s has defers on a transfer path nothing reaches"
      fn.Tast.name;

are gone, replaced by a comment and a bare ; closing the preceding if f.unwound then begin … end. That is the only change to lib/x86.ml in this lane — nothing else in the file was touched, and the concurrent redefinition lane should need to resolve nothing but this one hunk. The comment records the table above so the next reader does not have to rebuild the argument.

Item 4 — the flan_transfer_fail branch is reachable, and it is correct

lib/x86.ml:2229, inside the transfer exit: while the function's defers run with the channel cleared, a fresh pad named cleanup is the innermost one, and anything that finds the channel set again lands there and dies in flan_transfer_fail. Two separate questions, and both now answered by a program.

Is the block emitted? Yes, whenever a defer body contains a guarded call in a function that can unwind. used is a bool ref set by current_pad, so a defer that only assigns — which is what p6-transfer.flan's middle does — never emits it. objdump -d over spike/x86/p10-defer-transfer.flan built with --x86 finds two references to flan_transfer_fail.

Does anything arrive there? Yes. The thing that makes this hard to construct is that lib/check.ml's Ast.InvokeRestart arm (~line 1636) refuses an invoke-restart written lexically inside a defer, with the same reasoning the runtime's message carries. The runtime's own comment at runtime/flan_rt.c:449 says exactly where the remaining case lives: "this is the one that reaches a function through a call, where nothing static could see it." So the probe puts the invoke-restart in an ordinary defn and has the defer call it. The checker has nothing to object to, because from where it stands second is a function like any other.

spike/x86/p10-defer-transfer.flan is that program. outer establishes two nested restart-cases and a handler-bind and calls middle; deep signals; the handler aims a transfer at esc-one; the transfer unwinds deep and then middle; middle's transfer exit clears the channel and runs its defers; and the defer calls second, which aims a second transfer at esc-two. The restart frames are both still pushed at that moment — it is outer's own pad that pops them, and outer has not been reached — so the second transfer really is created rather than failing an unarmed-restart or no-such-restart check first. That was the thing worth checking before writing the probe, and it is why the second restart-case has to be established outside the first.

Both backends, verbatim and identical, at exit status 134:

spike/x86/p10-defer-transfer.flan:39:7: a defer invoked a restart, which a defer may not do — it is the cleanup a transfer runs on its way out

The location is Loc.to_string fn.Tast.floc — middle's own defer form — on both sides, which is the part a hand-written backend can get wrong silently: the string is a .rodata label and a length in a register here and a string_bytes constant there, and a wrong one looks exactly like a match to anything that only compares exit statuses. survey.sh compares stderr for this reason, and this is the program that makes that comparison earn its keep.

So item 4's guard is not a guess that happened to be unexercised. It is right, it is the only branch either backend has for the case, and the corpus simply had no program that started a transfer from a defer.

Files

file	state	what
lib/x86.ml — emit_fn, tail of the transfer exit	working	the item-5 refusal removed; one hunk, six lines out, a comment in. Nothing else in the file
spike/x86/p9-dead-defers.flan	working, MATCH	a leaf function with a defer and no call. Was the refusal
spike/x86/p10-defer-transfer.flan	working, MATCH at 134	a defer that calls a function that invokes a restart, while a first transfer unwinds

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.

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, and the SKIP 36 is the same 28 / 6 / 2 as before. Read it as a sanity check and not as the verification of the fix, for two reasons the honest version has to name: it does not include p10, whose file did not exist when the run globbed the directory, and lib/x86.ml was rebuilt twice while it was in flight — the end; fold and the comment — so some rows were built with the binary before that tidy-up and some after. Both rebuilds were semantically identical, so the counts are not wrong, but they are not one measurement. A clean run of the final binary, which includes p10, should report 99 / 0 / 0.

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

Items 1, 2, 3, 6 and 7 of HANDOFF-x86-rt.md are untouched and still stand. Two smaller things this lane turned up and did not do:

• emit.ml drops the dead defers silently and now so does x86.ml, but neither says so. The defers on an unreachable transfer exit are dead code the user wrote and that never runs, which is fine and is what the spec implies, but it is the kind of thing a --verbose build could reasonably mention. Not a correctness item.
• The survey's blind spot is real and is not about these two guards. Item 5 sat behind a ten-line program for as long as it existed, and was reachable the whole time, because every function with a defer in test/programs also calls something. HANDOFF-x86-rt.md already asks for survey.sh in CI; the stronger version of that request is that spike/x86 is where the shapes the corpus does not have belong, and it is worth adding them deliberately rather than when a lane happens to need one.