From 939417446d6463a02a09a4852ae1b719e66f5f09 Mon Sep 17 00:00:00 2001
From: Joseph Ferano <joseph@ferano.io>
Date: Sun, 13 Sep 2026 22:42:42 +0700
Subject: [PATCH] Item 5's guard dropped, item 4's reached and correct

---
 lib/x86.ml                                 | 21 ++++++---
 spike/x86/p10-defer-transfer.flan          | 53 ++++++++++++++++++++++
 spike/x86/{g5.flan => p9-dead-defers.flan} |  0
 3 files changed, 68 insertions(+), 6 deletions(-)
 create mode 100644 spike/x86/p10-defer-transfer.flan
 rename spike/x86/{g5.flan => p9-dead-defers.flan} (100%)

diff --git a/lib/x86.ml b/lib/x86.ml
index 1e264fe..07dbbcb 100644
--- a/lib/x86.ml
+++ b/lib/x86.ml
@@ -2231,12 +2231,21 @@ let emit_fn (md : Emit.m) ~externs ~fns (fn : Tast.fn) : string * string =
     end
     else begin zero_return (); jmp_lbl f.b f.retlbl end
   end
-  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;
+  (* And if [f.unwound] is false there is nothing to emit: the defers on the
+     transfer exit are dead because no path names that exit. This used to be a
+     refusal, on the theory that a function with a defer and no transfer exit
+     was a sign the reasoning had gone wrong. It is not — it is every leaf
+     function with a defer, and [spike/x86/p9-dead-defers.flan] is ten lines
+     of it. [emit.ml]'s [emit_fn] writes the whole exit under the same
+     [if f.unwound], and so drops them too.
+
+     What makes the drop safe is that [unwound] is not an approximation.
+     Every site that can leave a transfer in the channel and keep going either
+     emits [guard] — [Signal], [bounds_call], the two [rt_signals] entry
+     points, and every call by name or by pointer — or jumps to [current_pad]
+     outright, which is [invoke-restart] and the three re-propagating pads. So
+     [unwound] is false exactly when no transfer can arrive. *)
+  ;
 
   (* The prologue, now that the frame size is known. *)
   let pb = create () in
diff --git a/spike/x86/p10-defer-transfer.flan b/spike/x86/p10-defer-transfer.flan
new file mode 100644
index 0000000..d7b295b
--- /dev/null
+++ b/spike/x86/p10-defer-transfer.flan
@@ -0,0 +1,53 @@
+;;;; The second transfer, which the checker can only half refuse.
+;;;;
+;;;; spec-conditions.md §5 says a defer is the cleanup a transfer runs on its
+;;;; way out. Starting a *second* transfer from inside one would leave this
+;;;; frame's defers half run with two targets and no way to choose, so both
+;;;; backends emit a branch into `flan_transfer_fail` for it and the runtime
+;;;; dies there with the frame's location.
+;;;;
+;;;; `check.ml`'s `Ast.InvokeRestart` arm refuses the *lexical* case -- an
+;;;; `invoke-restart` written inside the `defer` form itself -- with the same
+;;;; reasoning. What it cannot see is a defer that *calls* a function that
+;;;; invokes a restart, because the callee is ordinary code and knows nothing
+;;;; about who called it. That is the case below, and it is the only way to
+;;;; reach the branch.
+;;;;
+;;;; The order matters and is what makes this a real second transfer rather
+;;;; than a first one: `outer` establishes both restart-cases, calls `middle`,
+;;;; `deep` signals, `outer`'s handler aims at `esc-one`, and 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
+;;;; transfer at `esc-two`. Both restart frames are still pushed: `outer`'s
+;;;; pad is what pops them, and `outer` has not been reached yet.
+;;;;
+;;;; Exits 134 with the message on stderr, both ways.
+
+(defstruct Blip [n i32])
+
+(defvar log i64)
+
+(defn deep [n i32] i32
+  (signal (Blip {.n n}))
+  0)
+
+;;; Ordinary code. The checker has nothing to object to here, because from
+;;; where it stands this is a function like any other.
+(defn second [] i64
+  (invoke-restart 'esc-two))
+
+(defn middle [n i32] i32
+  (defer (set log (second)))
+  (deep n))
+
+(defn outer [n i32] i32
+  (restart-case
+    (restart-case
+      (handler-bind [(Blip [c] (invoke-restart 'esc-one))]
+        (middle n))
+      (esc-one [] 11))
+    (esc-two [] 22)))
+
+(defn main [] i32
+  (print (outer 1)) (println "")
+  0)
diff --git a/spike/x86/g5.flan b/spike/x86/p9-dead-defers.flan
similarity index 100%
rename from spike/x86/g5.flan
rename to spike/x86/p9-dead-defers.flan