diff --git a/DISCUSS.md b/DISCUSS.md
index 854460a..a2cd5f0 100644
--- a/DISCUSS.md
+++ b/DISCUSS.md
@@ -704,3 +704,201 @@ 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`**. C's psABI would classify that single eightbyte as
+  INTEGER and pack both into `rax`. **LLVM's lowering of a first-class aggregate in IR is per-field, and it is not
+  the C ABI.**
+- `%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.**
+
+So **the internal calling convention 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/jit_stubs.c b/spike/backend/jit_stubs.c
index 76395b0..f53b516 100644
--- a/spike/backend/jit_stubs.c
+++ b/spike/backend/jit_stubs.c
@@ -91,15 +91,12 @@ int64_t spike_probe_align(int64_t x) {
   return x + (int64_t)(v[0] + v[1]);
 }
 
-/* A double in xmm0 alongside integers, and al = number of vector registers
- * used is *not* required here because this is not variadic -- which is itself
- * the thing to record. */
-double spike_probe_f(int64_t a, double x, int64_t b, double y) {
-  return (double)a + x * 2.0 + (double)b * 100.0 + y * 200.0;
-}
-
-/* A small struct by value. BUILT.md's "Why the FFI goes through a C shim"
- * says Flan never emits one of these -- the shim flattens it. This is here to
- * measure what the shim is saving us from, not because the backend needs it. */
-typedef struct { float x, y; } spike_vec2;
-float spike_probe_struct(spike_vec2 v, float s) { return v.x * s + v.y; }
+/* 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. */