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:

```flan
(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. The preceding `if f.unwound then begin … end` gained its `;` and a comment took the deleted arm's place. **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   99
DIFFER  0
REFUSED 0
NOX86   0
SKIP    36
```

That is `HANDOFF-x86-rt.md`'s 97 plus the two probes this lane added, and the `SKIP` 36 is the same 28 / 6 / 2 as
before. It is one clean measurement of the final binary: `lib/x86.ml` was not rebuilt while it ran, and both `p9`
and `p10` were on disk when it globbed the directory. An earlier full run reported 98, and that number should be
ignored rather than reconciled — it predated `p10` and straddled two rebuilds, so it was a sanity check and not a
verification.

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.