diff --git a/DISCUSS.md b/DISCUSS.md
index 854460a..e1c391b 100644
--- a/DISCUSS.md
+++ b/DISCUSS.md
@@ -704,3 +704,212 @@ measurement.
    and the render-thunk-per-inspection all get deleted. It is the bulk of the work and the whole of the prize.
 5. **Keep `llc` + `ld` + `dlopen` exactly as they are.** Item 13's third option. Nothing here argues against it.
 6. **Measure what is left.** Then, and only then, item 13 step 4.
+
+## 15. The backend spike, answered: feasible, and the obstacle is not the one anyone expected
+
+Item 13's step 4, run early and deliberately out of order, as a spike rather than as a decision. **Feasible.** A
+function written in Flan goes through the ordinary frontend, is lowered to x86-64 by hand, is written into an `mmap`
+and is called, and it answers correctly. That took an afternoon and no reference material beyond `objdump`.
+
+The apparatus is `spike/backend/`: `x86.ml` (an instruction selector), `jit_stubs.c` (three calls OCaml cannot make
+for itself, plus the C side of the ABI probes), `probe.flan`, `driver.ml` and `run.sh`. `bash spike/backend/run.sh`
+reproduces everything below. There is no dune file under `spike/`, nothing is wired into the build, and
+`dune test --root . -j 1` is green either side of it.
+
+**The headline is not the arithmetic.** Ten checks pass, and one of them failed first and mattered: a C callee that
+does a 16-byte aligned spill and reports whether it was entered aligned. Called plainly it passed; called from inside
+a binary operator it returned `-1`. The evaluator spills its left operand across the right operand's evaluation, so a
+call written in the right operand runs with `rsp` 8 bytes out. **That is the raylib crash, reproduced on day one of a
+backend that does almost nothing.** It is fixed with a depth counter and an assertion, and it is the clearest single
+argument that this work is *tractable but unforgiving*: nothing about the wrong version looked wrong, and only a probe
+built to catch it caught it.
+
+### Question 1 — does one function work end to end
+
+Yes. The frontend is the real one — `Reader`, `Parse`, `Load`, `Check` — so what is lowered is the same `Tast.fn`
+`emit.ml` gets, not a literal typed to make the exercise come out. Eleven of the 83 functions in a trivial program
+(the prelude is most of them) lower with no special handling, including `space?`, `digit?` and `upper-ascii`, which
+nobody wrote for this.
+
+The emitter is the trivial one the brief allows: every slot is a stack slot at `rbp - 8(i+1)`, every value is computed
+into `rax`, a binary operator spills its left operand. Two registers, no allocator, no liveness. `spike-add` is 58
+bytes where clang `-O0` would spend about 20, and that is the correct trade for a debug build.
+
+Proved by comparing numbers, not by reading bytes. `SPIKE_DISASM=1` disassembles the buffers that ran, and that is a
+debugging aid kept out of the pass/fail path on purpose: a disassembly that reads correctly beside a function
+answering 656 when it should answer 650 is the normal outcome of hand-encoding.
+
+### Question 2 — the real shape of the work
+
+**Layout is already owned, and this is the best news in the report.** `emit.ml`'s `lay` / `lay_fields` /
+`payload_lay` compute C struct layout — offsets, padding, tail padding, the union payload blob — because DWARF needs
+member offsets as integer literals and `getelementptr` cannot supply one. They are acceptance-tested against LLVM's
+own answer for the same struct type. So the drift risk item 10 fears most, *two backends disagreeing silently about
+where a field is*, does not arise: there is one layout calculator and a new backend calls it.
+
+Against `tast.ml`'s `expr_kind`, in four buckets:
+
+| | nodes |
+|---|---|
+| **Done in the spike** | `Int` `Bool` `Local` `Do` `Let` `If` `Return` `Set`/`Plocal`, arithmetic, comparison, bitwise, `Call`, `Rt` |
+| **Mechanical** | `While` `Break` `Continue` (the jump patching exists), `Global` `Str` `Zero` `Uninit`, the rest of `place`, `Field` `Deref` `Addr`, `Arr`, `Some_` `None_` `UnwrapSome`, `Match` on a tag |
+| **Bulky, not hard** | floats — a second register file, SSE encodings, `Cast`'s eight conversions, and the SSE half of the calling convention. Perhaps a third of the total instruction work for a small fraction of the programs |
+| **Fiddly** | aggregate copy on assignment (a struct `store` *is* the copy `spec-memory.md` requires), `Make` `MakeCase` `CaseField` over the payload blob, `CallPtr`, `FnAddr`'s three cases and the cell load behind `Fnval` |
+| **No plan** | `Handled` `Signal` `RestartCase` `InvokeRestart` `WithAlloc`, the transfer-channel guard after every call, the landing pad, and `fdefers` on the transfer exit path |
+
+The last row is the one to take seriously. The spike never emitted a guard or a pad, and the guard is on *every call
+site* in the real thing — `emit.ml`'s `guard`, `current_pad`, `emit_restart_case` and `emit_with_alloc` are several
+hundred lines of control flow that a second backend reimplements from the spec rather than copies. Conditions are not
+an advanced feature to defer: `spec-conditions.md` is load-bearing in the prelude already.
+
+### Question 3 — the SysV boundary, and the obstacle nobody named
+
+**The C boundary is the easy half, and `BUILT.md` is why.** `check.ml` rejects an aggregate in a `declare` signature
+and the generated shim flattens every struct, so no Flan-emitted call ever passes one to C. A string or slice crosses
+as `ptr`+`len` — two arguments, which is the only counting subtlety. The spike calls an eight-argument C function
+correctly, including the two that go on the stack, and sets `al` for the variadic case. **No aggregate classifier is
+needed for raylib. That is a large piece of `plan.org`'s "three classifiers to write and keep correct forever" that
+simply does not apply.**
+
+**The hard half is Flan calling Flan, and it was found by reading `signature`.** That function spells each parameter
+with `ll ty` and flattens nothing. Emitting a trivial program and looking at the `define` lines:
+
+```
+define i64            @"flan.take-slice"(%slice %p0, i64 %p1, ptr %xfer)
+define { i8, i32 }    @"flan.index-of-i32"(%slice %p0, i32 %p1, ptr %xfer)
+define { i8, float }  @"flan.min-f32"(%slice %p0, ptr %xfer)
+define { i8, %slice } @"flan.split-next!"(ptr %p0, ptr %xfer)
+define %vec           @"flan.filter-i32"(%slice %p0, ptr %p1, ptr %xfer)
+```
+
+The prelude is wall to wall aggregates by value. And what LLVM does with them, measured by `objdump` on clang's own
+output rather than read off a table:
+
+- `%slice` argument → `rdi`:`rsi`, two registers, and the next argument shifts along.
+- `{ i8, i64 }` return → tag in `al`, value in `rdx`.
+- `{ i8, float }` return → tag in `al`, value in **`xmm0`**.
+- `%vec` return (six words) → a hidden `sret` pointer in `rdi`, the real arguments shifted along behind it, and the
+  pointer returned in `rax`. **That pointer does not appear in the `define` line at all.**
+
+The last two are not the C ABI, and that was checked against a control rather than asserted — the same three shapes
+written in C, compiled by the same clang at `-O2`, beside the same shapes written as first-class IR aggregates:
+
+| shape | from C | from IR |
+|---|---|---|
+| `{ i8, i64 }` | `al` + `rdx` | `al` + `rdx` — agree |
+| `{ i8, float }` | **packed into `rax`** (`movd`/`shl`/`or`) | `al` + `xmm0` |
+| `{ i64, i64, i64 }` | **`sret` pointer in `rdi`** | **`rax` + `rdx` + `rcx`** |
+
+The 24-byte case is the striking one: C spills to memory through a hidden pointer, and the IR form returns it in three
+registers, one of which — `rcx` — the SysV ABI never uses for a return value at all. Somewhere past that, LLVM does
+switch to `sret`, which is what `%vec` gets.
+
+So **the internal calling convention is not the C ABI and is not specified anywhere. It is whatever LLVM's backend
+does with a first-class struct, discoverable only by disassembling.** That is the sharpest obstacle in this report,
+and it is sharper than raylib for three reasons: the reference is an implementation rather than a document; the
+failure mode is a garbage field rather than a link error; and it is not stable by contract across LLVM versions, which
+is exactly the coupling `plan.org` chose text IR to avoid.
+
+It also forces the decision that determines everything else:
+
+1. **Redefinitions only** — the custom backend emits a new body into an LLVM-built host. Incremental, testable one
+   function at a time, and the path that fits the dev loop. It requires matching LLVM's aggregate convention
+   bit-exactly, including the mixed integer/SSE case above.
+2. **The whole dev build** — the custom backend owns both sides and *picks* the convention: every aggregate by
+   pointer, nothing classified, done. No matching problem at all. But it needs complete node coverage on day one,
+   conditions included, and there is no partial version that runs.
+
+The spike leaned on option 1 without noticing, because the probe called C and C is the flattened half. A real attempt
+has to choose deliberately.
+
+### Question 4 — where the language leans on LLVM instead of defining itself
+
+The audit, which stands on its own whatever happens to the backend. Each row is drift you do not get if the language
+answers it.
+
+| | today | defined? |
+|---|---|---|
+| Integer overflow | no `nsw`/`nuw`, "arithmetic wraps (plan.org, Types)" | **yes** |
+| Shift count | masked to the operand width; a literal out of range is rejected by `check` | **yes** |
+| Evaluation order | `map_lr`, and the comment says left-to-right is *required, not a preference* | **yes** |
+| Division by zero | nothing. `prelude.ml` calls a remainder by zero "immediate undefined behaviour" and routes around it | **no** |
+| `INT64_MIN / -1` | nothing, and it is a separate case. LLVM says undefined; x86 `idiv` raises `SIGFPE` | **no** |
+| `f64` → `i64` out of range | `fptosi`, undefined in LLVM; x86 `cvttsd2si` answers the "integer indefinite" value | **no** |
+| `Uninit` | emitted as `poison` | **no**, and see below |
+| `unreachable` | after a `noreturn` call, and after an exhaustive `match` | **no** |
+| Alignment | no explicit `align` on loads and stores; LLVM uses the type's ABI alignment | implicitly, via `lay` |
+
+Two are worth more than a table row.
+
+**`Uninit` → `poison` is the one that actually bites, and it bites in the direction item 10 fears.** A hand backend
+gives a stable garbage value: whatever the stack slot held. LLVM's optimiser may reason from poison and delete the
+code that reads it. So `(uninit)` is the one construct where the two backends are *supposed* to differ and where
+"works in dev, breaks when shipped" is the expected outcome rather than a bug. The language should say what reading an
+uninitialised value means before a second backend exists, not after.
+
+**`unreachable` is the cheap one.** The spike emits `ud2`: a defined `SIGILL` at the instruction that fell through.
+LLVM's `unreachable` is undefined behaviour and licenses the optimiser to delete the path. Defining it as a trap costs
+two bytes and turns a class of miscompile into a crash with an address.
+
+None of this needs a backend. It is a session with `plan.org` and six `check.ml` cases.
+
+### Question 5 — unloading code, which is the prize
+
+**The shadow stack is better than expected and still not sufficient, and the two halves of that are separate
+questions.**
+
+*The running half — and the shadow stack does answer it.* The frame push in `emit_fn` is inside a plain `if m.dev`
+and is **not** gated: only the *slot table* is gated on `named && n > 0`, and a function with no named slot still
+pushes a frame with a null `slots`. So every active Flan function in a dev build is on the chain, lifted handler
+clauses included, and each frame points at the `flan_fninfo` belonging to the module it was compiled into — so the
+pointer identifies not just the function but *which body*. "No frame on the chain names this body" is answerable
+today, with no DWARF and no unwinder.
+
+Two caveats on that half. The pop happens before `leave; ret`, so a body is briefly executing with no record —
+irrelevant if reclamation happens at a safe point on the same thread, fatal if another thread reclaims while the game
+thread is returning. And the chain is a plain global, not thread-local, which `flan_dev.c` states and justifies.
+
+*The pointed-into half, which the shadow stack cannot see and which is the actual reason nothing is `dlclose`d today.*
+`BUILT.md` is explicit, and it is not the reason the brief assumed: "a cell holds an address inside a module's text;
+unloading it leaves every call site pointing at unmapped memory. The rule is about being *pointed into*." Owning the
+code object answers most of this — you own the cells, so redefinition drops the old body's last cell reference — but
+not all of it:
+
+- `FnAddr (Fnval n)` **loads the cell and yields a raw body address**, which can then be stored in a struct, a `Vec`
+  or a global. Nothing records that it happened.
+- `FnAddr (Flanfn _)` and `(Rtfn _)` bypass the cell *by design* — `tast.ml` says they "must never take that path" —
+  so a `Map`'s hash and equality pair and a handler-bind clause's address are raw pointers into a specific body, held
+  in data.
+
+So: **frames are tracked, escaped code pointers are not.** Unloading needs a rule the language does not have yet. The
+cheapest honest one is deferred reclamation — retire a body when no frame names it *and* an epoch has passed with no
+new capture — and the cleanest is to make a function value a cell pointer rather than a body pointer, which costs one
+indirection on `CallPtr` in dev builds and makes the whole question go away. That second option is worth writing down
+now whatever happens to the backend, because it is a change to what a `Fn` value *is*.
+
+### The verdict
+
+**Feasible, unforgiving, and not the next thing to do.**
+
+Feasible: the instruction selection is easy, layout is already owned and tested, the C boundary is already flattened,
+and one function ran on day one. Nothing here argues the way item 10 feared — the divergence hazard is real but it is
+concentrated in three named places (`Uninit`, division, the float cast), not spread through the whole of arithmetic.
+
+Unforgiving: the internal aggregate convention is defined by LLVM's implementation and not by any document, the
+alignment rule is invisible until raylib crashes somewhere else, and conditions are a second full implementation of
+`spec-conditions.md` rather than a port.
+
+Not next: item 13's order still holds, and the spike does not disturb it. Transport is 41µs of a 21ms redefinition and
+code generation is 19 of the 21, so the *speed* case remains what item 13 said it was. What this spike adds is that
+the **introspection** case is also not free — unloading needs a rule about escaped function values that nothing in the
+language has, and that rule is worth having whether or not a backend is ever written.
+
+**What to do first if it went ahead**, in order, and the first two are worth doing regardless:
+
+1. **Define the six undefined cases** (question 4). No backend required, and every one is drift avoided rather than
+   drift managed.
+2. **Decide what a `Fn` value is** — body pointer or cell pointer — and write it down. This is the unloading question
+   and it is a language question, not a backend one.
+3. **Choose option 1 or option 2 from question 3**, deliberately. Everything else follows from it.
+4. **Only then**, and only if 3 says so, grow `spike/backend/x86.ml` from the node table in question 2 — floats
+   first, because they gate most of the prelude, and conditions last, because they are the only row with no plan.
diff --git a/spike/backend/driver.ml b/spike/backend/driver.ml
new file mode 100644
index 0000000..fde8ce4
--- /dev/null
+++ b/spike/backend/driver.ml
@@ -0,0 +1,177 @@
+(* The spike's harness: run the real frontend, lower the functions it produced
+   with [X86], put the bytes in executable memory, call them, and compare with
+   what the language says they should answer.
+
+   The comparison is the whole point. Reading the bytes proves nothing -- a
+   disassembly that looks right and a program that returns the wrong number is
+   the normal outcome of hand-encoding, which is why the oracle here is the
+   arithmetic and not objdump. [oracle.sh] disassembles the same buffer, and
+   that is a debugging aid, not the evidence. *)
+
+external jit_alloc : int -> nativeint = "spike_jit_alloc"
+external jit_write : nativeint -> string -> unit = "spike_jit_write"
+external jit_protect : nativeint -> int -> unit = "spike_jit_protect"
+external call1 : nativeint -> int64 -> int64 = "spike_call1"
+external call2 : nativeint -> int64 -> int64 -> int64 = "spike_call2"
+external sym : string -> nativeint = "spike_sym"
+
+let failures = ref 0
+let checks = ref 0
+
+let check name got want =
+  incr checks;
+  if got = want then Printf.printf "  ok    %-28s = %Ld\n" name got
+  else begin
+    incr failures;
+    Printf.printf "  FAIL  %-28s = %Ld, want %Ld\n" name got want
+  end
+
+(* One page per function, so that a function that runs off its own end lands in
+   an unmapped page and segfaults at the fault rather than in the middle of the
+   next function. This is the crudest possible version of the code-object
+   question the whole exercise is really about. *)
+let page = 4096
+
+let install (code : string) : nativeint =
+  if String.length code > page then failwith "function exceeds one page";
+  let p = jit_alloc page in
+  jit_write p code;
+  jit_protect p page;
+  p
+
+let run src =
+  let decls =
+    Flan.Load.program ~file:src (Flan.Parse.program_all (Flan.Reader.read_file src))
+  in
+  let prog = Flan.Check.program_all decls.Flan.Load.decls in
+  Printf.printf "frontend: %d fns, %d globals, %d structs, %d externs\n"
+    (List.length prog.Flan.Tast.fns) (List.length prog.Flan.Tast.globals)
+    (List.length prog.Flan.Tast.structs) (List.length prog.Flan.Tast.externs);
+
+  (* Two passes, because [spike-calls] calls functions whose addresses are not
+     known until they are installed. Pass one installs every function at a
+     fixed page; pass two emits the real code into it. A real backend does this
+     with relocations; the spike does it by emitting twice, which is the same
+     answer with none of the machinery. *)
+  let addrs : (string, nativeint) Hashtbl.t = Hashtbl.create 16 in
+  let unsupported = ref [] in
+  let lowerable =
+    List.filter
+      (fun (fd : Flan.Tast.fn) ->
+         try
+           ignore (X86.fn ~resolve:(fun _ -> 0L) fd);
+           true
+         with X86.Unsupported m ->
+           unsupported := (fd.Flan.Tast.name, m) :: !unsupported;
+           false)
+      prog.Flan.Tast.fns
+  in
+  List.iter
+    (fun (fd : Flan.Tast.fn) ->
+       Hashtbl.replace addrs fd.Flan.Tast.name (jit_alloc page))
+    lowerable;
+  let resolve name =
+    match Hashtbl.find_opt addrs name with
+    | Some p -> Int64.of_nativeint p
+    | None ->
+      (* Not a Flan function: a runtime entry point, looked up the way a dev
+         build already reaches the host's symbols -- through the dynamic symbol
+         table, which --dev links with -rdynamic. *)
+      Int64.of_nativeint (sym name)
+  in
+  let bytes = Hashtbl.create 16 in
+  List.iter
+    (fun (fd : Flan.Tast.fn) ->
+       let code = X86.fn ~resolve fd in
+       Hashtbl.replace bytes fd.Flan.Tast.name code;
+       let p = Hashtbl.find addrs fd.Flan.Tast.name in
+       jit_write p code;
+       jit_protect p page)
+    lowerable;
+
+  Printf.printf "lowered: %d of %d functions\n"
+    (List.length lowerable) (List.length prog.Flan.Tast.fns);
+  List.iter (fun (n, m) -> Printf.printf "  skipped %-20s %s\n" n m)
+    (List.rev !unsupported);
+  Hashtbl.iter (fun n c -> Printf.printf "  %-20s %4d bytes at %nx\n"
+                   n (String.length c) (Hashtbl.find addrs n)) bytes;
+
+  (* The bytes that actually ran, dumped where run.sh can objdump them.
+     A debugging aid and not the evidence: a disassembly that reads correctly
+     next to a function that answers 656 when it should answer 650 is the
+     normal outcome of hand-encoding, which is why the checks below compare
+     numbers. *)
+  (match Sys.getenv_opt "SPIKE_DUMP" with
+   | None -> ()
+   | Some dir ->
+     Hashtbl.iter
+       (fun n c ->
+          let oc = open_out_bin (Filename.concat dir (n ^ ".bin")) in
+          output_string oc c; close_out oc)
+       bytes);
+
+  (* ── The SysV boundary ──────────────────────────────────────────────
+     Three synthetic functions, built as Tast by hand rather than written in
+     Flan, because the surface language has no way to spell a call to an
+     arbitrary C symbol with eight arguments. [Tast.Rt] is the node a runtime
+     call already uses and the one a [declare-c] shim lands on, so this is the
+     real path with a made-up callee. *)
+  let loc = Flan.Loc.unknown in
+  let i64 = Flan.Types.Int Flan.Types.I64 in
+  let ex e = { Flan.Tast.e; ty = i64; loc } in
+  let lit n = ex (Flan.Tast.Int (Int64.of_int n, Flan.Types.I64)) in
+  let probe name params body =
+    { Flan.Tast.name; params; slots = Array.make (List.length params) i64;
+      snames = Array.make (List.length params) None; ret = i64;
+      body = [ body ]; fdefers = []; fparent = None; floc = loc }
+  in
+  let arg0 = ex (Flan.Tast.Local 0) in
+  let probes = [
+    (* Eight integers: six in registers and two on the stack, which is the case
+       a register-only convention gets silently wrong. *)
+    probe "abi-8" [ i64 ]
+      (ex (Flan.Tast.Prim (Flan.Tast.Rt "spike_probe8",
+         [ arg0; lit 2; lit 3; lit 4; lit 5; lit 6; lit 7; lit 8 ])));
+    (* rsp % 16 == 0 at the call. The callee does an aligned 16-byte spill and
+       answers -1 if it was entered misaligned. *)
+    probe "abi-align" [ i64 ]
+      (ex (Flan.Tast.Prim (Flan.Tast.Rt "spike_probe_align", [ arg0 ])));
+    (* The same call, but underneath a binary operator -- so it is evaluated
+       with the left operand spilled on the stack. This is the one that matters:
+       alignment at a call site is not a property of the prologue, it is a
+       property of how much the expression evaluator has pushed. *)
+    probe "abi-align-nested" [ i64 ]
+      (ex (Flan.Tast.Prim (Flan.Tast.Add,
+         [ lit 0;
+           ex (Flan.Tast.Prim (Flan.Tast.Rt "spike_probe_align", [ arg0 ])) ])));
+  ] in
+  List.iter
+    (fun (fd : Flan.Tast.fn) ->
+       let code = X86.fn ~resolve fd in
+       let p = jit_alloc page in
+       jit_write p code; jit_protect p page;
+       Hashtbl.replace addrs fd.Flan.Tast.name p)
+    probes;
+
+  print_endline "results:";
+  let at n = Hashtbl.find addrs n in
+  check "spike-add 3 4" (call2 (at "spike-add") 3L 4L) 7L;
+  check "spike-add -5 2" (call2 (at "spike-add") (-5L) 2L) (-3L);
+  check "spike-arith 10 4" (call2 (at "spike-arith") 10L 4L) 19L;
+  check "spike-let 6" (call1 (at "spike-let") 6L) 1332L;
+  check "spike-if 1 2" (call2 (at "spike-if") 1L 2L) 1L;
+  check "spike-if 9 2" (call2 (at "spike-if") 9L 2L) 7L;
+  check "spike-calls 5" (call1 (at "spike-calls") 5L) 656L;
+  check "abi-8 1" (call1 (at "abi-8") 1L) 87654321L;
+  check "abi-align 10" (call1 (at "abi-align") 10L) 13L;
+  check "abi-align-nested 10" (call1 (at "abi-align-nested") 10L) 13L;
+
+  Printf.printf "\n%d checks, %d failures\n" !checks !failures;
+  exit (if !failures = 0 then 0 else 1)
+
+(* The frontend's diagnostics printed rather than swallowed: a spike that says
+   [Fatal error: exception Errors(_)] costs an hour. *)
+let () =
+  try run Sys.argv.(1) with
+  | Flan.Loc.Error d -> prerr_endline (Flan.Loc.report d); exit 2
+  | Flan.Loc.Errors ds -> prerr_endline (Flan.Loc.report_all ds); exit 2
diff --git a/spike/backend/jit_stubs.c b/spike/backend/jit_stubs.c
new file mode 100644
index 0000000..6726793
--- /dev/null
+++ b/spike/backend/jit_stubs.c
@@ -0,0 +1,98 @@
+/* The three things OCaml cannot do for itself: get executable memory, put
+ * bytes in it, and jump to them. Everything interesting is in x86.ml; this
+ * file is deliberately dumb.
+ *
+ * Shaped after lib/dynload_stubs.c's rule, which spike/embed took verbatim for
+ * the same reason: the boundary passes pointers and scalars, never an OCaml
+ * [value] into foreign storage. Nothing here keeps anything.
+ *
+ * RW then mprotect to R+X, never RWX in one mmap: a hardened kernel may refuse
+ * a writable-executable anonymous mapping outright, and a policy denial that
+ * comes back as a null pointer reads exactly like an encoding bug. */
+
+#include <caml/mlvalues.h>
+#include <caml/memory.h>
+#include <caml/alloc.h>
+#include <caml/fail.h>
+
+#include <sys/mman.h>
+#include <string.h>
+#include <stdint.h>
+#include <stdio.h>
+#include <dlfcn.h>
+
+value spike_jit_alloc(value vlen) {
+  size_t len = (size_t)Long_val(vlen);
+  void *p = mmap(NULL, len, PROT_READ | PROT_WRITE,
+                 MAP_PRIVATE | MAP_ANONYMOUS, -1, 0);
+  if (p == MAP_FAILED) caml_failwith("spike_jit_alloc: mmap failed");
+  return caml_copy_nativeint((intnat)p);
+}
+
+value spike_jit_write(value vp, value vbytes) {
+  char *p = (char *)Nativeint_val(vp);
+  memcpy(p, String_val(vbytes), caml_string_length(vbytes));
+  return Val_unit;
+}
+
+value spike_jit_protect(value vp, value vlen) {
+  void *p = (void *)Nativeint_val(vp);
+  if (mprotect(p, (size_t)Long_val(vlen), PROT_READ | PROT_EXEC) != 0)
+    caml_failwith("spike_jit_protect: mprotect failed");
+  return Val_unit;
+}
+
+/* Every Flan function's emitted signature is its parameters followed by the
+ * transfer channel (emit.ml, [signature]), so the trampolines below all pass a
+ * trailing pointer. Nothing in the spike transfers, so it is NULL. */
+typedef int64_t (*fn1)(int64_t, void *);
+typedef int64_t (*fn2)(int64_t, int64_t, void *);
+
+value spike_call1(value vp, value a) {
+  return caml_copy_int64(((fn1)Nativeint_val(vp))(Int64_val(a), NULL));
+}
+value spike_call2(value vp, value a, value b) {
+  return caml_copy_int64(((fn2)Nativeint_val(vp))(Int64_val(a), Int64_val(b), NULL));
+}
+
+value spike_sym(value vname) {
+  void *h = dlsym(RTLD_DEFAULT, String_val(vname));
+  if (h == NULL) caml_failwith("spike_sym: not found");
+  return caml_copy_nativeint((intnat)h);
+}
+
+/* ── The C side of the ABI probes ──────────────────────────────────── */
+
+/* Eight integers: six in registers, two on the stack, which is the case a
+ * register-only convention silently gets wrong. The answer is positional so a
+ * swapped pair cannot pass. */
+int64_t spike_probe8(int64_t a, int64_t b, int64_t c, int64_t d,
+                     int64_t e, int64_t f, int64_t g, int64_t h) {
+  return a * 1 + b * 10 + c * 100 + d * 1000 + e * 10000 + f * 100000
+       + g * 1000000 + h * 10000000;
+}
+
+/* The alignment check, and it has to be done with an aligned load rather than
+ * by reading rsp, because that is how raylib finds out: the SysV ABI promises
+ * rsp % 16 == 0 at the call instruction, so on entry rsp+8 is aligned, and a
+ * callee that spills an __m128 to its frame faults when it is not. -O2 is what
+ * turns this into an actual movaps; without it the bug hides. */
+__attribute__((noinline))
+int64_t spike_probe_align(int64_t x) {
+  volatile double v[2] __attribute__((aligned(16))) = { 1.0, 2.0 };
+  /* Reading rsp as well, so a failure says which of the two it was. */
+  uintptr_t sp;
+  __asm__ volatile ("mov %%rsp, %0" : "=r"(sp));
+  if ((sp % 16) != 8) return -1;   /* entry rsp is call-site rsp minus 8 */
+  return x + (int64_t)(v[0] + v[1]);
+}
+
+/* No float probe either, for a plainer reason: this emitter has no SSE, so
+ * there is nothing here that could call one. Floats are counted as work in
+ * item 15 rather than claimed as done.
+ *
+ * And no struct-by-value probe, and that is a finding rather than an
+ * omission: check.ml rejects an aggregate in a [declare] signature and the
+ * generated shim flattens every one, so no Flan-emitted call ever passes a
+ * struct to C. The aggregate problem is real but it is on the Flan-to-Flan
+ * side, which is measured in DISCUSS.md item 15 and not from here. */
diff --git a/spike/backend/probe.flan b/spike/backend/probe.flan
new file mode 100644
index 0000000..0fab0e6
--- /dev/null
+++ b/spike/backend/probe.flan
@@ -0,0 +1,24 @@
+;; The spike's input. Ordinary Flan, run through the ordinary frontend --
+;; Reader, Parse, Load, Check -- so that what the emitter below lowers is the
+;; same Tast.fn the LLVM backend gets and not a literal someone typed to make
+;; the exercise come out.
+
+(defn spike-add [a i64  b i64] i64
+  (+ a b))
+
+(defn spike-arith [a i64  b i64] i64
+  (- (* a 3) (+ b 7)))
+
+(defn spike-let [a i64] i64
+  (let [x (* a a)
+        y (+ x 1)]
+    (* x y)))
+
+(defn spike-if [a i64  b i64] i64
+  (if (< a b) (- b a) (- a b)))
+
+(defn spike-calls [a i64] i64
+  (spike-add (spike-arith a 2) (spike-let a)))
+
+(defn main [] i32
+  0)
diff --git a/spike/backend/run.sh b/spike/backend/run.sh
new file mode 100644
index 0000000..bdef39b
--- /dev/null
+++ b/spike/backend/run.sh
@@ -0,0 +1,48 @@
+#!/usr/bin/env bash
+# The spike, end to end: the real frontend produces a Tast, x86.ml turns it
+# into bytes, the bytes go into an mmap, and the mmap gets called.
+#
+# Driven by hand with ocamlfind and clang against the flan.cmxa dune already
+# builds, exactly as spike/embed does and for the same reason: nothing under
+# spike/ is wired into the build, so there is no dune file here and `dune test`
+# cannot see any of it.
+set -u
+here=$(cd "$(dirname "$0")" && pwd)
+root=$(cd "$here/../.." && pwd)
+cd "$root" || exit 1
+
+dune build --root . lib/flan.cmxa 2>&1 | head -20
+
+out=$(mktemp -d); trap 'rm -rf "$out"' EXIT
+
+# The C stubs. -O2 on purpose: spike_probe_align's aligned load only becomes a
+# real movaps with optimisation on, and an alignment bug that only shows up in
+# a release build is the one this is looking for.
+clang -O2 -c -I"$(ocamlopt -where)" "$here/jit_stubs.c" -o "$out/jit_stubs.o" || exit 1
+
+ocamlfind ocamlopt -thread -package unix,threads.posix -linkpkg \
+  -I "$root/_build/default/lib/.flan.objs/byte" \
+  -I "$root/_build/default/lib/.flan.objs/native" \
+  -I "$out" -I "$here" \
+  -o "$out/spike" \
+  "$root/_build/default/lib/flan.cmxa" \
+  -cclib -rdynamic -ccopt -L"$root/_build/default/lib" \
+  "$out/jit_stubs.o" \
+  "$here/x86.ml" "$here/driver.ml" 2>&1 | head -40
+
+test -x "$out/spike" || { echo "build failed"; exit 1; }
+
+SPIKE_DUMP=$out "$out/spike" "$here/probe.flan"
+rc=$?
+
+# Disassembly on request. objdump over the raw buffer, which is what to reach
+# for when a function answers the wrong number -- not what proves it answers
+# the right one.
+if [ "${SPIKE_DISASM:-}" = 1 ]; then
+  for f in "$out"/*.bin; do
+    echo; echo "== $(basename "$f" .bin)"
+    objdump -D -b binary -m i386:x86-64 -M intel "$f" | tail -n +7
+  done
+fi
+echo "exit: $rc"
+exit $rc
diff --git a/spike/backend/x86.ml b/spike/backend/x86.ml
new file mode 100644
index 0000000..9f486fe
--- /dev/null
+++ b/spike/backend/x86.ml
@@ -0,0 +1,379 @@
+(* A spike: Tast -> x86-64 machine code, in memory, called. Not a backend.
+   The point is to find out what breaks, so the subset is deliberately tiny
+   and every case it cannot do raises with the node that defeated it -- an
+   honest [Unsupported] is the measurement, and a silently wrong answer is
+   the one outcome that would waste the exercise.
+
+   Register allocation is the trivial one the brief allows: every slot is a
+   stack slot at [rbp - 8*(i+1)], every value is computed into rax, and a
+   binary operator pushes its left operand. Two registers are enough for
+   everything below and nothing is kept live across a statement. That is what
+   makes an instruction selector tractable in an afternoon; it is also why the
+   code it produces is four times the size of clang -O0's.
+
+   Conventions, all of them SysV's, because raylib is called from this code:
+     - integer arguments in rdi rsi rdx rcx r8 r9, then right-to-left on the
+       stack; integer result in rax.
+     - rsp % 16 == 0 at the [call] instruction. raylib spills xmm registers
+       with movaps and faults far from the cause when this is wrong.
+     - rbx rbp r12-r15 are callee-saved. This emitter touches none of them
+       except rbp, which it saves.
+     - every Flan function takes the transfer channel as a trailing ptr
+       (emit.ml, [signature]), so a Flan function of n parameters is an n+1
+       argument C function. *)
+
+exception Unsupported of string
+
+let unsupported fmt = Printf.ksprintf (fun s -> raise (Unsupported s)) fmt
+
+(* ── Bytes ───────────────────────────────────────────────────────────── *)
+
+type buf = { mutable bytes : Buffer.t }
+
+let create () = { bytes = Buffer.create 256 }
+let len b = Buffer.length b.bytes
+let contents b = Buffer.contents b.bytes
+let u8 b n = Buffer.add_char b.bytes (Char.chr (n land 0xff))
+
+let u32 b n =
+  for i = 0 to 3 do u8 b ((n asr (i * 8)) land 0xff) done
+
+let i32 b (n : int) =
+  if n < -0x80000000 || n > 0x7fffffff then unsupported "displacement %d" n;
+  u32 b n
+
+let u64 b (n : int64) =
+  for i = 0 to 7 do
+    u8 b (Int64.to_int (Int64.logand (Int64.shift_right_logical n (i * 8)) 0xffL))
+  done
+
+(* ── Registers and modrm ─────────────────────────────────────────────── *)
+
+(* The encoding order, not the ABI order: this numbering *is* the three bits
+   the modrm byte wants, which is why rsp is 4 and rbp is 5 rather than
+   anything more memorable. *)
+let rax = 0 and rcx = 1 and rdx = 2 and _rbx = 3
+let rsp = 4 and rbp = 5 and rsi = 6 and rdi = 7
+let r8 = 8 and r9 = 9
+
+(* REX.W is always set: everything here is 64-bit. R extends the reg field and
+   B the r/m field, which is the whole of what r8-r15 need. *)
+let rex b ~r ~m = u8 b (0x48 lor (if r >= 8 then 4 else 0) lor (if m >= 8 then 1 else 0))
+let modrm b ~md ~r ~m = u8 b ((md lsl 6) lor ((r land 7) lsl 3) lor (m land 7))
+
+(* reg, reg *)
+let rr b op ~r ~m = rex b ~r ~m; u8 b op; modrm b ~md:3 ~r ~m
+
+(* reg, [rbp + disp32]. Always disp32 rather than the shorter disp8 form: a
+   frame can outgrow 128 bytes and a one-byte displacement that silently wraps
+   is exactly the bug this spike would not find. *)
+let rm_rbp b op ~r ~disp =
+  rex b ~r ~m:rbp; u8 b op; modrm b ~md:2 ~r ~m:rbp; i32 b disp
+
+let mov_rr b ~dst ~src = rr b 0x89 ~r:src ~m:dst          (* mov dst, src *)
+let mov_load b ~dst ~disp = rm_rbp b 0x8b ~r:dst ~disp    (* mov dst, [rbp+d] *)
+let mov_store b ~src ~disp = rm_rbp b 0x89 ~r:src ~disp   (* mov [rbp+d], src *)
+
+let movabs b ~dst (n : int64) =
+  rex b ~r:0 ~m:dst; u8 b (0xb8 lor (dst land 7)); u64 b n
+
+let push b r = if r >= 8 then u8 b 0x41; u8 b (0x50 lor (r land 7))
+let pop b r = if r >= 8 then u8 b 0x41; u8 b (0x58 lor (r land 7))
+
+let add_rr b ~dst ~src = rr b 0x01 ~r:src ~m:dst
+let sub_rr b ~dst ~src = rr b 0x29 ~r:src ~m:dst
+let and_rr b ~dst ~src = rr b 0x21 ~r:src ~m:dst
+let or_rr  b ~dst ~src = rr b 0x09 ~r:src ~m:dst
+let xor_rr b ~dst ~src = rr b 0x31 ~r:src ~m:dst
+let imul_rr b ~dst ~src =                                  (* 0f af /r *)
+  rex b ~r:dst ~m:src; u8 b 0x0f; u8 b 0xaf; modrm b ~md:3 ~r:dst ~m:src
+let cmp_rr b ~a ~bb = rr b 0x39 ~r:bb ~m:a                 (* cmp a, b *)
+
+let add_imm32 b ~dst n = rex b ~r:0 ~m:dst; u8 b 0x81; modrm b ~md:3 ~r:0 ~m:dst; i32 b n
+let sub_imm32 b ~dst n = rex b ~r:0 ~m:dst; u8 b 0x81; modrm b ~md:3 ~r:5 ~m:dst; i32 b n
+
+let call_r b r = if r >= 8 then u8 b 0x41; u8 b 0xff; modrm b ~md:3 ~r:2 ~m:r
+let leave b = u8 b 0xc9
+let ret b = u8 b 0xc3
+let ud2 b = u8 b 0x0f; u8 b 0x0b
+
+(* setcc al, then movzx rax, al -- a compare's result is a bool, which is one
+   byte in Flan's layout (i1 in LLVM, and the ABI zero-extends it). *)
+let setcc b cc = u8 b 0x0f; u8 b (0x90 lor cc); modrm b ~md:3 ~r:0 ~m:rax
+let movzx_al b = u8 b 0x48; u8 b 0x0f; u8 b 0xb6; modrm b ~md:3 ~r:rax ~m:rax
+
+(* jcc rel32 and jmp rel32, patched once the target is known. *)
+let jcc b cc = u8 b 0x0f; u8 b (0x80 lor cc); let at = len b in u32 b 0; at
+let jmp b = u8 b 0xe9; let at = len b in u32 b 0; at
+
+let patch b ~at ~target =
+  let rel = target - (at + 4) in
+  let s = Buffer.contents b.bytes in
+  let s = Bytes.of_string s in
+  for i = 0 to 3 do
+    Bytes.set s (at + i) (Char.chr ((rel asr (i * 8)) land 0xff))
+  done;
+  let nb = Buffer.create (Bytes.length s) in
+  Buffer.add_bytes nb s;
+  b.bytes <- nb
+
+(* ── Lowering ────────────────────────────────────────────────────────── *)
+
+type fnctx = {
+  b : buf;
+  nslots : int;
+  (* How many 8-byte words this expression's evaluation has pushed since the
+     prologue. rsp is 16-aligned at the end of the prologue, so [depth] even
+     means rsp is aligned and [depth] odd means it is 8 out.
+
+     This counter is the answer to the one bug the ABI probe found. Alignment
+     is not a property of the prologue: the evaluator spills the left operand
+     across the right one's evaluation, so a call written in the right operand
+     runs with one word outstanding. Deriving it from a count kept here is the
+     only way that stays correct as the evaluator grows cases, and it is what
+     clang's [sub rsp, 8] before a call is doing. *)
+  mutable depth : int;
+  (* A symbol the code calls, resolved to an absolute address by the driver
+     before emission. movabs + call r is what a JIT does anyway: a rel32 call
+     cannot reach an arbitrary mmap, and the 2-byte indirect call is cheaper
+     than the relocation machinery a real backend would grow here. *)
+  resolve : string -> int64;
+}
+
+let slot_disp i = -8 * (i + 1)
+
+(* Every stack movement goes through these two, so that nothing can move rsp
+   without the counter noticing. *)
+let pushv f r = push f.b r; f.depth <- f.depth + 1
+let popv f r = pop f.b r; f.depth <- f.depth - 1
+
+(* Every type this spike handles is one 8-byte integer register. Everything
+   else is the real backend's problem and is enumerated in the verdict rather
+   than guessed at here. *)
+let word_ty (t : Flan.Types.t) =
+  match t with
+  | Flan.Types.Int _ | Flan.Types.Bool | Flan.Types.Ptr _ -> true
+  | _ -> false
+
+let check_word what (t : Flan.Types.t) =
+  if not (word_ty t) then
+    unsupported "%s of type %s: not a single integer register" what
+      (Flan.Types.to_string t)
+
+let cc_of signed (p : Flan.Tast.prim) =
+  match p, signed with
+  | Flan.Tast.Eq, _ -> 0x4 | Flan.Tast.Ne, _ -> 0x5
+  | Flan.Tast.Lt, true -> 0xc | Flan.Tast.Lt, false -> 0x2
+  | Flan.Tast.Le, true -> 0xe | Flan.Tast.Le, false -> 0x6
+  | Flan.Tast.Gt, true -> 0xf | Flan.Tast.Gt, false -> 0x7
+  | Flan.Tast.Ge, true -> 0xd | Flan.Tast.Ge, false -> 0x3
+  | _ -> assert false
+
+let arg_regs = [| rdi; rsi; rdx; rcx; r8; r9 |]
+
+(* Value into rax. Everything is a subexpression of something that will
+   immediately consume rax, so nothing is kept live and no allocator is
+   needed. *)
+let rec value f (e : Flan.Tast.expr) : unit =
+  let b = f.b in
+  match e.Flan.Tast.e with
+  | Flan.Tast.Int (n, _) -> movabs b ~dst:rax n
+  | Flan.Tast.Bool v -> movabs b ~dst:rax (if v then 1L else 0L)
+  | Flan.Tast.Local i ->
+    check_word "local" e.Flan.Tast.ty;
+    if i >= f.nslots then unsupported "slot %d out of range" i;
+    mov_load b ~dst:rax ~disp:(slot_disp i)
+  | Flan.Tast.Do body -> block f body
+  | Flan.Tast.Let (binds, body) ->
+    List.iter
+      (fun (i, e) ->
+         value f e;
+         check_word "binding" e.Flan.Tast.ty;
+         mov_store b ~src:rax ~disp:(slot_disp i))
+      binds;
+    block f body
+  | Flan.Tast.Set (Flan.Tast.Plocal i, rhs) ->
+    value f rhs;
+    check_word "assignment" rhs.Flan.Tast.ty;
+    mov_store b ~src:rax ~disp:(slot_disp i)
+  | Flan.Tast.If (c, t, e') -> emit_if f c t e'
+  | Flan.Tast.Return (Some x) ->
+    value f x;
+    leave b; ret b
+  | Flan.Tast.Return None -> leave b; ret b
+  | Flan.Tast.Prim (p, args) -> prim f e p args
+  | Flan.Tast.Call (name, args) -> call f (f.resolve name) args ~xfer:true
+  | Flan.Tast.Unit -> ()
+  | k -> unsupported "expression: %s" (node_name k)
+
+and block f body =
+  match body with
+  | [] -> ()
+  | [ last ] -> value f last
+  | x :: rest -> value f x; block f rest
+
+and prim f e (p : Flan.Tast.prim) args =
+  let b = f.b in
+  match p, args with
+  | (Flan.Tast.Add | Flan.Tast.Sub | Flan.Tast.Mul
+    | Flan.Tast.BitAnd | Flan.Tast.BitOr | Flan.Tast.BitXor), [ x; y ] ->
+    check_word "arithmetic" x.Flan.Tast.ty;
+    binop f x y;
+    (* left in rax, right in rcx *)
+    (match p with
+     | Flan.Tast.Add -> add_rr b ~dst:rax ~src:rcx
+     | Flan.Tast.Sub -> sub_rr b ~dst:rax ~src:rcx
+     | Flan.Tast.Mul -> imul_rr b ~dst:rax ~src:rcx
+     | Flan.Tast.BitAnd -> and_rr b ~dst:rax ~src:rcx
+     | Flan.Tast.BitOr -> or_rr b ~dst:rax ~src:rcx
+     | _ -> xor_rr b ~dst:rax ~src:rcx)
+  | (Flan.Tast.Eq | Flan.Tast.Ne | Flan.Tast.Lt | Flan.Tast.Le
+    | Flan.Tast.Gt | Flan.Tast.Ge), [ x; y ] ->
+    let signed =
+      match x.Flan.Tast.ty with
+      | Flan.Types.Int k -> Flan.Types.signed k
+      | Flan.Types.Bool -> false
+      | t -> unsupported "comparison on %s" (Flan.Types.to_string t)
+    in
+    binop f x y;
+    cmp_rr b ~a:rax ~bb:rcx;
+    setcc b (cc_of signed p);
+    movzx_al b
+  | Flan.Tast.Rt sym, args -> call f (f.resolve sym) args ~xfer:false
+  | _ -> unsupported "primitive in %s" (Flan.Types.to_string e.Flan.Tast.ty)
+
+(* Left into rax, right into rcx, with the left spilled across the right's
+   evaluation. Left-to-right, which emit.ml's [map_lr] is explicit about being
+   required rather than a preference -- a call in either operand has effects.
+   The push/pop pair keeps rsp 16-aligned in pairs, which matters only because
+   [call] below re-derives alignment from a counter rather than tracking rsp. *)
+and binop f x y =
+  let b = f.b in
+  value f x;
+  pushv f rax;
+  value f y;
+  mov_rr b ~dst:rcx ~src:rax;
+  popv f rax
+
+and emit_if f c t e =
+  let b = f.b in
+  value f c;
+  (* cmp rax, 0: 48 83 f8 00 -- written out because the helper above takes
+     registers only and a zero-compare is the one immediate form worth having. *)
+  u8 b 0x48; u8 b 0x83; modrm b ~md:3 ~r:7 ~m:rax; u8 b 0x00;
+  let to_else = jcc b 0x4 in     (* je *)
+  value f t;
+  let to_end = jmp b in
+  patch b ~at:to_else ~target:(len b);
+  value f e;
+  patch b ~at:to_end ~target:(len b)
+
+(* A call, and this is the part that has to be exactly right.
+
+   [xfer] appends the transfer channel, which every Flan function's signature
+   carries and a C entry point does not. The spike passes NULL: nothing here
+   signals, and a real backend would pass the caller's own channel pointer.
+
+   Alignment: rsp is 16-aligned at function entry minus the 8 the [call]
+   pushed, so after [push rbp] it is aligned again, and the frame is rounded to
+   a multiple of 16. Every push here is paired with a pop before the next call
+   can happen, so rsp is aligned at every call site by construction. Stack
+   arguments are pushed in pairs to keep it that way -- an odd count gets a
+   dummy push, which is what clang's [sub rsp, 8] is doing when you see it. *)
+and call f (addr : int64) args ~xfer =
+  let b = f.b in
+  let n = List.length args + (if xfer then 1 else 0) in
+  (* Bring rsp to 16 first, so everything below can count in pairs. *)
+  let pad = f.depth land 1 = 1 in
+  if pad then (sub_imm32 b ~dst:rsp 8; f.depth <- f.depth + 1);
+  let stacked = List.filteri (fun i _ -> i >= 6) args in
+  let nstack = List.length stacked + (if xfer && n > 6 then 1 else 0) in
+  (* The stack half, evaluated right to left so that the seventh argument ends
+     up at [rsp] and the eighth above it. The transfer channel is the last
+     argument of all, so it is pushed first. *)
+  if nstack land 1 = 1 then (sub_imm32 b ~dst:rsp 8; f.depth <- f.depth + 1);
+  if xfer && n > 6 then (movabs b ~dst:rax 0L; pushv f rax);
+  List.iter (fun a -> value f a; pushv f rax) (List.rev stacked);
+  (* The register half needs a spill of its own: rdi..r9 are argument registers
+     and rax is where every value lands, so an earlier argument would be
+     clobbered by a later one's evaluation. Push each, then pop them into their
+     registers in reverse. *)
+  let inreg = List.filteri (fun i _ -> i < 6) args in
+  List.iter (fun a -> value f a; pushv f rax) inreg;
+  let nreg = List.length inreg in
+  List.iteri (fun i _ -> popv f arg_regs.(nreg - 1 - i)) inreg;
+  if xfer && n <= 6 then movabs b ~dst:arg_regs.(nreg) 0L;
+  (* al = the number of vector registers used. Required only for a variadic
+     callee and set unconditionally because it is two bytes: a wrong al on a
+     printf-shaped entry point -- raylib's TraceLog is one -- is a crash that
+     looks like anything else. After the argument registers, since al is rax's
+     low byte. *)
+  u8 b 0xb0; u8 b 0x00;          (* mov al, 0 *)
+  (* r11 always, never r9: r11 is the scratch register SysV reserves and is the
+     one register guaranteed not to be carrying an argument. Choosing the
+     target conditionally is how a six-argument call gets quietly wrong. *)
+  u8 b 0x49; u8 b 0xbb; u64 b addr;   (* movabs r11, addr *)
+  assert (f.depth land 1 = 0);
+  call_r b 11;
+  let back = 8 * (nstack + (nstack land 1)) in
+  if back > 0 then (add_imm32 b ~dst:rsp back; f.depth <- f.depth - (back / 8));
+  if pad then (add_imm32 b ~dst:rsp 8; f.depth <- f.depth - 1)
+
+and node_name (k : Flan.Tast.expr_kind) =
+  match k with
+  | Flan.Tast.Int _ -> "Int" | Flan.Tast.Float _ -> "Float"
+  | Flan.Tast.Bool _ -> "Bool" | Flan.Tast.Str _ -> "Str"
+  | Flan.Tast.Unit -> "Unit" | Flan.Tast.Zero _ -> "Zero"
+  | Flan.Tast.Uninit _ -> "Uninit" | Flan.Tast.Local _ -> "Local"
+  | Flan.Tast.Global _ -> "Global" | Flan.Tast.Prim _ -> "Prim"
+  | Flan.Tast.Call _ -> "Call" | Flan.Tast.FnAddr _ -> "FnAddr"
+  | Flan.Tast.CallPtr _ -> "CallPtr" | Flan.Tast.Do _ -> "Do"
+  | Flan.Tast.Let _ -> "Let" | Flan.Tast.If _ -> "If"
+  | Flan.Tast.While _ -> "While" | Flan.Tast.Return _ -> "Return"
+  | Flan.Tast.Break _ -> "Break" | Flan.Tast.Continue _ -> "Continue"
+  | Flan.Tast.Set _ -> "Set" | Flan.Tast.Field _ -> "Field"
+  | Flan.Tast.Addr _ -> "Addr" | Flan.Tast.Deref _ -> "Deref"
+  | Flan.Tast.Make _ -> "Make" | Flan.Tast.MakeCase _ -> "MakeCase"
+  | Flan.Tast.CaseField _ -> "CaseField" | Flan.Tast.Arr _ -> "Arr"
+  | Flan.Tast.Some_ _ -> "Some" | Flan.Tast.None_ -> "None"
+  | Flan.Tast.Match _ -> "Match" | Flan.Tast.UnwrapSome _ -> "UnwrapSome"
+  | Flan.Tast.Signal _ -> "Signal" | Flan.Tast.Handled _ -> "Handled"
+  | Flan.Tast.RestartCase _ -> "RestartCase"
+  | Flan.Tast.WithAlloc _ -> "WithAlloc"
+  | Flan.Tast.InvokeRestart _ -> "InvokeRestart"
+
+(* ── A whole function ────────────────────────────────────────────────── *)
+
+let fn ~resolve (fd : Flan.Tast.fn) : string =
+  let b = create () in
+  let nslots = Array.length fd.Flan.Tast.slots in
+  let f = { b; nslots; resolve; depth = 0 } in
+  push b rbp;
+  mov_rr b ~dst:rbp ~src:rsp;
+  (* Round the frame to 16 so that rsp is aligned at every call site. One
+     extra word for the transfer channel's slot, which is not a Flan slot and
+     has no index -- the spike never reads it, but a real backend must, and
+     leaving no room for it is the kind of thing that is cheap now and
+     expensive later. *)
+  let frame = (nslots + 1) * 8 in
+  let frame = (frame + 15) land lnot 15 in
+  if frame > 0 then sub_imm32 b ~dst:rsp frame;
+  (* Parameters arrive in registers and are stored into their slots at once,
+     which is also emit.ml's rule: slots 0..n-1 are the parameters, in order. *)
+  let np = List.length fd.Flan.Tast.params in
+  if np > 6 then unsupported "more than six parameters";
+  List.iteri
+    (fun i ty ->
+       check_word "parameter" ty;
+       mov_store b ~src:arg_regs.(i) ~disp:(slot_disp i))
+    fd.Flan.Tast.params;
+  (* The transfer channel is the last argument and goes just past the slots. *)
+  if np < 6 then mov_store b ~src:arg_regs.(np) ~disp:(slot_disp nslots);
+  block f fd.Flan.Tast.body;
+  leave b; ret b;
+  (* Anything that falls off the end of a Never-returning body lands here and
+     traps rather than running into the next function. LLVM's [unreachable] is
+     undefined behaviour; ud2 is a defined SIGILL, and the difference is one of
+     the audit's findings. *)
+  ud2 b;
+  contents b