Both comments predated the marker, and now neither does

NEXT.md contradicted itself about the raylib header: two entries said the check
runs on every build and a third, further down, still explained why it is opt-in.
It gets the strikethrough its siblings have, with the reason the argument
dissolved -- the commit, not a change of mind about the property.

plan.org's list of what the dev runtime answers over nREPL had gained a member it
never listed. And the page quotes a program so that the line numbers in the output
beside it resolve, so both new examples are now pasted from their files rather than
trimmed, and cast.flan gets the source block every other example has.

NEXT.md

@@ -18,8 +18,17 @@ IEEE already answers it.
 
 # Where this is — end of 2026-09-13, second handoff
 
+**This section is the record of that evening and is no longer where the tree is.** It is kept because the
+reasoning in it is still the reasoning, but read the section above this one first, and take the state below
+as a snapshot: it pins `dev-loop` at `e725a5a`, and since then the arithmetic-condition lane, the
+redefinition emitter, the aggregate case across the reload boundary, the two unreached guards, DWARF for
+`--x86`, the cost measurements, the last two raylib ports and the `dune test` noise have all landed. The
+x86 survey it quotes at 97 now reports **103 MATCH, 0 DIFFER, 0 refused by name, 38 skipped**, and of the
+seven remaining items it lists from `docs/handoffs/HANDOFF-x86-rt.md`, items 1, 3, 4, 5, 6 and 7 are done —
+each has a `docs/handoffs/HANDOFF-x86-*.md` of its own.
+
 **Branch `dev-loop` at `e725a5a`, working tree clean, `dune test` green, every lane merged.**
-Nothing is running and nothing is half-built. Read this first.
+Nothing is running and nothing is half-built.
 
 ## The x86 backend is correct, and is not yet the dev backend
 
@@ -466,13 +475,14 @@ clause tells the abstract pass what it may assume, so the body checks at the def
 - The clause is written as a **Clojure-style map at the head of the body**, `{:where (ordered? $t)}`, chosen by
   the author over a bare keyword. It disambiguates because a bare `{}` in expression position is already refused
   (`parse.ml:110`), so a `{}` there can be nothing else, and Clojure's `{:pre [...] :post [...]}` is the
-  precedent. It leaves room for further keys without new syntax. **One catch to settle first:** `{K V}` is
+  precedent. It leaves room for further keys without new syntax. ~~**One catch to settle first:** `{K V}` is
   currently a legal return type, so `(defn f [...] {string i32} {:where ...} body)` puts two braces in a row
-  meaning different things. That resolves itself if `{K V}` goes in favour of `(Map K V)`, which is a separate
-  open question in this file.
-- A `where` clause over **compile-time type predicates** admits the operators the body needs. Four are wanted —
-  `ordered?`, `equal?`, `hashable?`, `numeric?` — against Odin's forty-one. The prelude's nine non-collapsing
-  functions need only the first two.
+  meaning different things.~~ — resolved the way this predicted: `{K V}` went in favour of `(Map K V)`,
+  braces in type position are refused by name, and the two-braces-in-a-row case cannot arise.
+- A `where` clause over **compile-time type predicates** admits the operators the body needs. ~~Four are
+  wanted — `ordered?`, `equal?`, `hashable?`, `numeric?`~~ — against Odin's forty-one. Five landed: `copyable?`
+  is the fifth, and it has no Odin counterpart because a `$T` there never has to answer whether it moves. The
+  prelude's nine non-collapsing functions need only the first two.
 - Each instantiation checks the concrete type satisfies the predicates and refuses **that call site** if not.
 
 **This is not a type class, and the distinction is the one to keep straight.** A type class carries
@@ -1046,9 +1056,12 @@ header is now cached in the session as well as on disk, so a repeat import (a `C
 `import` line) costs nothing, and a header edited mid-session is not picked up until the session restarts — the same
 rule a changed `.c` file follows.
 
-**Opt-in on purpose.** `vendor/raylib/headers` is `?${FLAN_RAYLIB_H}`. "A build needs libraylib linkable and not
+~~**Opt-in on purpose.** `vendor/raylib/headers` is `?${FLAN_RAYLIB_H}`. "A build needs libraylib linkable and not
 raylib-devel installed" is a property chosen deliberately, and requiring a header would take it from everyone to give
-the check to whoever has one. Unset means off; set-and-wrong is an error naming the path.
+the check to whoever has one. Unset means off; set-and-wrong is an error naming the path.~~ — no longer so, and what
+dissolved the argument was the commit rather than a change of mind about the property: `vendor/raylib/raylib-5.5.h` is
+tracked, `headers` names that path with no `${...}` in front of it, `FLAN_RAYLIB_H` is gone, and the check runs on
+every build. The `?` marker still means what it says here; this package is simply not using it any more.
 
 Worth knowing before touching it:
 

conditions.org

@@ -102,6 +102,19 @@ the agent's socket instead.
   ~BoundsError~ rather than ending the process, abandoning a frame and retrying
   it is a real thing to do, and a non-idempotent mutation is what makes it go
   wrong.
+- *Four conditions come from below your program*, all with ~error~:
+  ~StorageExhausted~ when an allocator cannot satisfy a request, ~FileError~
+  when a file operation fails, ~BoundsError~ for an index or slice outside its
+  container, and ~ArithError~ for arithmetic with no answer — a divide or
+  remainder by zero, ~INT64_MIN / -1~, and a float-to-integer cast that does not
+  fit, each of which used to be a bare ~SIGFPE~ with no message and no location.
+  The first two offer a ~retry~ at the failing site, because freeing something
+  or supplying another path makes the same operation succeed. The last two offer
+  *nothing*: no handler makes index 51 valid for a length-50 array or gives a
+  division by zero a quotient, so there is nothing to resume into. The restart
+  that answers those is the one your program already established — the frame
+  loop's ~continue~ — and it is on the stack and reachable without anything
+  being pushed at the failure.
 - *An unknown restart name is a hard stop.* No ~find-restart~ to test with.
 - *So are the wrong arguments*, and for the same reason: nothing static can
   know what a name will find. The message names both signatures.

docs/BUILT.md

@@ -2615,6 +2615,12 @@ allocation guard, so a `retry` re-attempts the allocation and not the expression
 literal's field list, and giving the same braces two meanings is what the colon-to-dot change was for. A map is built
 with `map-new` and filled with `put`.
 
+*(Superseded on the first half only. `(Map K V)` is the type spelling and `{K V}` was withdrawn — braces in type
+position are refused by name, because the brace's value and type meanings never corresponded the way the bracket's do
+and `{}` in type position is wanted for anonymous struct types. The paragraph's actual subject is unchanged: there is
+still no map literal, and a bare map form in expression position is still a struct literal's field list. See
+`lib/parse.ml:68`.)*
+
 ### The refusals, each by name
 
 - A **float key** — not a milestone question, which is why it is said separately. NaN is not equal to itself, and
@@ -3847,6 +3853,11 @@ raylib to open. Pointing raylib at embedded bytes needs `LoadImageFromMemory` an
 `LoadTexture` — a raylib binding question, not an embedding one — so the flagship program is not yet asset-free on the
 web. The mechanism it needs is in.
 
+*(Superseded by the cut. `sand.flan` was taken back from 765 lines to 206, to parity with the Clojure, Common Lisp and
+jank ports, and the texture went with it — there is no `load-texture` call and no asset left to embed, only a
+`brush-size` integer that kept the name. The binding question is still open for whatever wants it next; this program is
+no longer the one asking it, and `brush.png` is now unreferenced.)*
+
 ## `slurp`, `barf`, and the two ways they fail
 
 NEXT.md decisions 2 and 5. `(slurp path)` and `(slurp path allocator)` read a whole file into a `(Vec u8)`;

docs/SPIKE-GENERICS.md

@@ -1,5 +1,16 @@
 # The generics spike, answered: it runs, and the bill lands on the dev loop rather than on the checker
 
+> **This is the spike report and it stopped being current when generics landed for real, on 2026-09-13.**
+> It is kept because the measurements and the reasoning behind the design are still the ones that were
+> acted on, but it describes a branch where `lib/prelude.ml` and the backends were untouched, and they
+> are not any more: the prelude's per-type families collapsed into one function each. Two things it says
+> have since been overtaken and would mislead anyone writing code from it. Its account of plan.org is out
+> of date — plan.org now specifies `$t` itself rather than lowercase-with-no-sigil. And the spelling rule
+> below is narrower than what shipped: `$t` is written wherever a *type* goes, including in a return type
+> and nested inside `[$t]` or `(Option $t)`, and bare `t` only where a type's *name* is an argument in
+> expression position, as in `(vec-new t)` and the cast `(t x)`. `(Option t)` does not compile.
+> plan.org's Types section and spec-memory.md's Generics section are the current account.
+
 Milestone 5's parametric polymorphism, run early and deliberately out of order, as a spike rather than as a
 decision. **Feasible, and smaller than expected.** A generic function written in Flan goes through the ordinary
 frontend, is instantiated at each concrete type its call sites ask for, is emitted as real functions and runs,

lib/ast.ml

@@ -16,7 +16,7 @@ and texpr_kind =
   | Tname  of string                  (* i32  bool  Cursor  string *)
   | Tslice of texpr                   (* [u8]                      ptr+len *)
   | Tarray of len * texpr             (* [4 f32]  [rows [cols u32]]        *)
-  | Tmap   of texpr * texpr           (* {string i32}                      *)
+  | Tmap   of texpr * texpr           (* (Map string i32)                  *)
   | Tapp   of string * texpr list     (* (Ptr Cursor)  (Option f64)        *)
   | Tfn    of texpr list * texpr      (* (Fn [a a] bool)                   *)
 

lib/build.ml

@@ -744,18 +744,20 @@ let executable ?(opts = default) ?(csrcs = []) ?(lflags = []) ?(pnames = [])
      by this backend — and the module that would redefine through them arrives
      with the lane that writes it.
 
-     That lane inherits one thing this comment should say out loud rather than
-     leave for it to find. [x86.ml]'s header licenses its own calling
-     convention on the grounds that a dev build is compiled entirely by it and
-     a release build entirely by LLVM, so the two never meet in one process.
-     Publishing a cell an LLVM-built module can store into is the first thing
-     that could make that false: the two conventions agree on scalars and
-     disagree on every aggregate, so an [Emit.redefinition] module dlopened
-     into an [--x86] host would be correct until the first redefined function
-     took or returned a struct. Nothing in the toolchain does that today —
-     [flan reload] and [flan dev] both build host and module through LLVM —
-     and the fix when something does is to emit the module through this
-     backend too, not to grow a classifier. *)
+     [X86.redefinition] is that lane, and it has landed, so the paragraph this
+     comment used to end with — that no counterpart existed — is no longer
+     true. What remains true is why it had to be written here rather than
+     borrowed from LLVM. [x86.ml]'s header licenses its own calling convention
+     on the grounds that a dev build is compiled entirely by it and a release
+     build entirely by LLVM, so the two never meet in one process. Publishing
+     a cell an LLVM-built module can store into is the first thing that could
+     make that false: the two conventions agree on scalars and disagree on
+     every aggregate, so an [Emit.redefinition] module dlopened into an
+     [--x86] host is correct until the first redefined function takes or
+     returns a struct. That pair is now refused at [dlopen] by a marker symbol
+     each backend defines and each backend's module references — see [shared]
+     below — rather than left to die at the call. The answer was to emit the
+     module through this backend too, and never to grow a classifier. *)
   (* [--debug] used to be in this list too. It is not any more: [x86.ml] emits
      a compile unit, a subprogram per function and a line table, all written
      out as bytes because [.loc] cannot work against a file whose instructions
@@ -911,12 +913,17 @@ let shared ?(opts = default) ~ir ~out () : timing =
      than it is is worse than none. It catches a caller holding one option
      record and reaching for the wrong builder. It does not catch a caller
      holding two and picking the wrong one — the crossed pair that was measured
-     segfaulting passes this check and still segfaults, because it hands an
-     LLVM record to the LLVM builder and simply loads the result into an x86
-     host. [flan reload] is precisely that caller. The complete answer is a
-     marker symbol the host defines and a module references, so the loader
-     refuses the pair at dlopen rather than the processor refusing it at a
-     call. See docs/handoffs/HANDOFF-x86-aggregates.md. *)
+     segfaulting passes this check, because it hands an LLVM record to the LLVM
+     builder and simply loads the result into an x86 host. [flan reload] is
+     precisely that caller, and it is why this guard was never the whole
+     answer. The whole answer is the marker symbol: a dev build defines
+     [flan.abi.x86] or [flan.abi.llvm] according to which backend emitted it,
+     each backend's redefinition module holds a pointer to its own, and the
+     loader has to resolve that pointer while it maps the object — so a crossed
+     pair is refused at [dlopen], naming both backends, before any new body
+     runs. That landed; this check is the cheap first line rather than the only
+     one. See docs/handoffs/HANDOFF-x86-aggregates.md and
+     docs/handoffs/HANDOFF-x86-abi-marker.md. *)
   if opts.x86 then
     failwith
       "--x86: Build.shared is the LLVM redefinition path, and an --x86 host \

lib/form.ml

@@ -17,7 +17,9 @@ and value =
   | Byte  of int           (* \space  \0  \(                   (0..255) *)
   | List  of t list        (* (f x) *)
   | Vec   of t list        (* [1 2 3]  and every binding/type bracket *)
-  | Map   of t list        (* {.field v} a struct value, {K V} a type. The
+  | Map   of t list        (* {.field v} a struct value, and a defn's
+                              {:where ...} clause. Braces are not a type: the
+                              {K V} spelling was withdrawn for (Map K V). The
                               colon spelling is left for map literals. *)
 
 let make v loc = { v; loc }

lib/tast.ml

@@ -1,8 +1,9 @@
 (** The typed IR: what the checker produces and what every backend consumes.
 
-    Three backends share this — the tree-walking interpreter, dev redefinition
-    and the release AOT build (plan.org, Compilation) — so everything a backend
-    would otherwise have to re-derive is resolved here and nowhere else:
+    Every backend shares this — the LLVM emitter and the hand-written x86-64
+    one, each of them under dev redefinition and under the release AOT build
+    (plan.org, Compilation) — so everything a backend would otherwise have to
+    re-derive is resolved here and nowhere else:
 
     - names are gone. A local is a slot index into the frame, a global is a
       name, and a call names its callee directly. No environment lookup.

lib/types.ml

@@ -28,7 +28,7 @@ type t =
   | Enum   of string
   | Slice  of t                       (* [T]     ptr+len, non-owning *)
   | Array  of int64 * t               (* [n T]   inline, a value, copies *)
-  | Map    of t * t                   (* {K V} *)
+  | Map    of t * t                   (* (Map K V) *)
   | Ptr    of t                       (* (Ptr T) *)
   (* [Allocator]: a builtin opaque type, the way [string] is a builtin
      ptr+len. It is a [Types.t] case with no user-writable constructor, which

plan.org

@@ -101,7 +101,7 @@ world.
 - Map keys initially use compiler-provided structural equality and hashing for
   integers, enums, strings, fixed arrays and value structs; pointers, slices and
   owning containers are excluded. A map is homogeneous, and empty construction
-  is type-directed: ~(defvar enemies (Map string Enemy) (map-new))~. ~get~
+  names its types: ~(let [enemies (map-new string Enemy)] ...)~. ~get~
   returns ~(Option V)~; ~put~ is the ~()~-returning upsert. See
   spec-memory.md for the deferred move-aware operations.
 - Operations: ~get~, ~put~, ~remove~, ~push~, ~pop~, ~at~, ~len~, ~update~.
@@ -194,8 +194,10 @@ and on a managed ~class~ instance. An ordinary ~struct~ never carries one.
 
 - Types are mandatory; *inference* makes them feel optional. Annotate function
   signatures, infer locals — Odin/Zig/Rust ergonomics.
-- Signatures are annotated as inline name/type pairs, as in ~let~ and
-  ~defstruct~: ~(defn area [s Shape] f32 ...)~. No separate ~declare~ form —
+- Signatures are annotated as inline name/type pairs, as in ~defstruct~ and a
+  ~restart-case~ clause: ~(defn area [s Shape] f32 ...)~. A ~let~ is not one of
+  them — a local is inferred from its initialiser and takes no annotation at
+  all. No separate ~declare~ form —
   ~declare~ is kept only where there is no body (forward declarations, FFI).
 - Annotations at function boundaries are unavoidable, because compile-time
   overloading is incompatible with full inference. Locals are inferred.
@@ -401,8 +403,8 @@ primitives, and are never bootstrapped away.
 The LLVM question does not bear on this: the release backend emits LLVM IR *as
 text* and shells out to ~clang~, so no language needs LLVM bindings, and C++ or
 Rust buy nothing here. What the choice actually turns on is that milestones 2–5
-are a reader, a typed IR, a checker and a tree-walking interpreter — variants and
-exhaustive pattern matching, which is the one domain where OCaml is not a
+are a reader, a typed IR, a checker and the code generators behind it — variants
+and exhaustive pattern matching, which is the one domain where OCaml is not a
 preference but a clear win. There is also a menhir lexer/parser already started
 in ~old-ocaml/~.
 
@@ -415,7 +417,7 @@ build sequence. For a game language it buys dogfooding at the price of a second
 compiler to maintain forever. Choose as if the host language is permanent.
 
 * Milestone-2 primitives
-The interpreter provides these; everything else is written in Flan. Keeping the
+The runtime provides these; everything else is written in Flan. Keeping the
 list short is the whole strategy — it is what makes the LLVM backend and the
 wasm32 target cheap, because a primitive is the only thing implemented twice.
 
@@ -477,33 +479,54 @@ is Clojure's ~ns~ form: no path that must mirror the directory, no
   root-directory aliases.
 
 * Compilation
-*Two backends and three paths.* The split is not dev-vs-release; it is
-/does this code have a frame budget/.
+*One evaluator and three paths.* The split is not dev-vs-release; it is
+/does this code have a frame budget/. There is no interpreter: open decision #7
+is settled the other way from how this section was first written, and docs/BUILT.md's
+"Why there is no interpreter" carries the reasoning. Compiling is the only way a
+form is ever run, so there is no second evaluator that could disagree with the
+first about what a program means.
 
 #+begin_src
-expression eval:    flan → typed IR → interpreter                      ~1ms
-dev redefinition:   flan → typed IR → .ll → llc → ld -shared → dlopen → cell store
-                                                                       ~16ms  (MEASURED)
+expression eval:    flan → typed IR → .ll → llc → ld -shared → dlopen → call
+                                                                       ~19ms  (MEASURED)
+dev redefinition:   the same path, ending in a cell store rather than a call
 release build:      flan → typed IR → .ll → clang --target={native,wasm32}
 #+end_src
 
 *Hard requirement: eval is immediate.* Not "fast enough for a build" — immediate,
-because the whole point of the live loop is that you see the result. 16ms is one
-frame at 60fps and under the ~50ms threshold where a response stops feeling
-instantaneous. The rule that buys it: *never invoke the ~clang~ driver on the dev
-path.*
+because the whole point of the live loop is that you see the result. 19ms is
+around one frame at 60fps and under the ~50ms threshold where a response stops
+feeling instantaneous. The rule that buys it: *never invoke the ~clang~ driver on
+the dev path.*
 
-*Expression eval* — ~C-c C-e~, calling a function, inspecting a var, running a
-test — goes to the tree-walking interpreter. Sub-millisecond, no subprocess. This
-is the permanent REPL backend, not a milestone-2 scaffold.
+*Expression eval* — ~C-x C-e~, calling a function, inspecting a var, running a
+test — is compiled like everything else, into its own shared object, which is
+then loaded and called. What made an interpreter look necessary was the
+assumption that this had to be sub-millisecond; the measurement below is that
+the compiled route is already inside the threshold, and the one thing an
+interpreter would have bought is an oracle the hand-written acceptance table
+supplies instead.
 
-*Dev redefinition* — ~C-c C-c~ on a function inside a running game — cannot use
-the interpreter, because that code has an 8ms frame budget. It recompiles the one
-function, links it, and does the atomic indirection-cell store. This is what the
-Hot reload section has always described; the interpreter does not replace it.
+*Dev redefinition* — ~C-c C-c~ on a function inside a running game — has an 8ms
+frame budget to respect. It recompiles the one function, links it, and does the
+atomic indirection-cell store. This is what the Hot reload section has always
+described, and it is the same machinery expression eval uses, one step further
+on.
 
 *Release* is whole-program AOT with direct calls and no cells.
 
+*A second code generator, not a second evaluator.* ~lib/x86.ml~ emits x86-64
+machine code directly and is selected with ~--x86~; it exists because ~llc~ is
+most of the 19ms above. It is a different route from the same typed IR to the
+same observable behaviour, not a different semantics, and what holds it to that
+is ~spike/x86/survey.sh~: every program in the corpus is built both ways and
+byte-compared on stdout, stderr and exit status. At the time of writing that is
+103 MATCH, 0 DIFFER, 0 refused by name. It handles conditions, bounds checks,
+indirection cells, redefinition modules and DWARF line tables; what it does not
+have, and must not grow, is an aggregate classifier — an ~--x86~ host therefore
+takes ~--x86~ modules and an LLVM host takes LLVM ones, and ~lib/build.ml~
+refuses the crossed pair by name.
+
 ** Measured redefinition latency
 Single function, x86-64, clang 20.1.8, 20 iterations each:
 
@@ -563,9 +586,10 @@ This is why *the dev runtime is multithreaded* — it needs the reload thread. T
 is settled, and is independent of whether the /language/ exposes threads, which
 is still open decision #4.
 
-It also bears on whether the interpreter survives: if the agent can ~dlopen~ and
-call anything in 16ms, then even "eval this expression against live game state"
-can be a compiled ~.so~, and no interpreter is needed inside the game process.
+This is also what settled the interpreter question: if the agent can ~dlopen~ and
+call anything in under 20ms, then even "eval this expression against live game
+state" is a compiled ~.so~, and no interpreter is needed inside the game process.
+That is the route ~C-x C-e~ actually takes.
 
 ** Why LLVM IR as text
 | | text ~.ll~ → ~clang~ | libLLVM bindings | emit C |
@@ -580,32 +604,36 @@ The only column text loses is the JIT one, and the measurement above shows the
 loss is ~13ms — below perception. ORC remains addable later behind the same typed
 IR without touching the language, but nothing currently argues for it.
 
-** The interpreter cannot run sand
-Do not plan around it. 200 × 280 = 56,000 cells, scanned by ~game-update~ and
-again by ~game-draw~ — ~112,000 interpreted cell-visits per frame against an
-8.3ms budget at 120fps. At an optimistic 100ns per visit (environment
-allocation, argument binding, two index computations, a compare) that is 11ms
-before ~settle~, ~paint~, or a single raylib call. Expect 20–30fps.
+** The interpreter, and why there is not one
+An interpreter could never have run sand, and that was the first half of the
+argument. 200 × 280 = 56,000 cells, scanned by ~game-update~ and again by
+~game-draw~ — ~112,000 interpreted cell-visits per frame against an 8.3ms budget
+at 120fps. At an optimistic 100ns per visit (environment allocation, argument
+binding, two index computations, a compare) that is 11ms before ~settle~,
+~paint~, or a single raylib call. Expect 20–30fps. Milestone 4's interactive
+acceptance test was always going to run on the compiled dev build.
 
-This is an estimate, not a measurement, which is why *milestone 2 exits with a
-measured interpreter throughput number* — before milestone 4 depends on it.
-Milestone 4's interactive acceptance test runs on the compiled dev build; the
-interpreter is not in that loop.
+*** Settled: the compiled path is the only backend
+This was open decision #7 and it is closed. Compiled redefinition measured at
+~19ms is perceptually instant for expression eval too, so the one thing an
+interpreter was still wanted for went away; the instrumentation-based step
+debugger that wanted it is cut (see Tooling); and milestone 3 did not need it as
+an oracle either, because the acceptance table is hand-written and the table /is/
+the oracle. What is bought by dropping it is the standing obligation: two
+evaluators must agree on observable behaviour forever, and every divergence is a
+bug that reproduces in only one of them. docs/BUILT.md's "Why there is no interpreter"
+records the decision; ~lib/expand.ml~ states it at the top of the file, because
+macros are where the absence stopped being free — a macro has to run at compile
+time and there is nothing to interpret it with, so the compiler compiles it into
+a shared object and loads it with ~dlopen~ into its own process.
 
-*** Open: does the interpreter survive milestone 3?
-Now that compiled redefinition is measured at 16ms, the case for a /permanent/
-interpreter is weaker than it looked. 16ms is perceptually instant for expression
-eval too, and one backend removes a standing obligation — two backends must agree
-on observable behaviour forever, and every divergence is a bug that reproduces in
-only one of them.
+Consequences applied elsewhere in this document: milestone 2's "interpreted calls
+per second" exit criterion is dropped, and the host ABI moved onto the critical
+path in its place.
 
-Against dropping it: the interpreter is clearly right for milestone 2 (far less
-work than an LLVM backend, better error messages, no linking), and the
-instrumentation-based step debugger wants it. Decide at milestone 3 exit on
-measured numbers, not now.
-
-All three paths share the frontend and the typed IR and must agree on observable
-behaviour. That agreement is what the acceptance programs test.
+The paths that remain share the frontend and the typed IR and must agree on
+observable behaviour. That agreement is what the acceptance programs test, and
+for the two code generators it is tested byte for byte.
 
 - Non-local exit lowered *explicitly* (result propagation + branch targets), not
   via platform unwinding. Same on both targets, no dependency on the WASM
@@ -635,7 +663,7 @@ Deliberately different.
 
 |         | Dev                       | Release    |
 |---------+---------------------------+------------|
-| Backend | interpreter /and/ LLVM    | LLVM/clang |
+| Backend | LLVM, or ~--x86~          | LLVM/clang |
 | Calls   | indirection cells | direct  |
 | Code    | never freed       | static  |
 | Frames  | shadow stack      | none    |
@@ -674,6 +702,9 @@ nses-of-symbols and middleware. Treat "speaks nREPL" as milestone 7a and "an
 editor client that is pleasant" as a separate milestone 7b. In the dev runtime:
 - eval string in package; compile form/file with source locations
 - completion, arglist, describe, find-definition
+- macroexpand, one step or to the fixpoint — the compiler builds the macro into a
+  shared object and dlopens it to run the expansion, which is the same route a
+  file's own macros take
 - backtrace + restarts; interrupt
 
 ** Emacs client
@@ -698,8 +729,11 @@ trap handling, frame unwinding), duplicating an enormous existing project.
 
 Neither covers the other's column, so this is not a choice between them.
 
-*DAP is nearly free.* No debug adapter is written: emit DWARF from the LLVM
-backend and point ~lldb-dap~ at the binary; dape speaks to that. lldb and gdb
+*DAP is nearly free.* No debug adapter is written: emit DWARF from the backend
+and point ~lldb-dap~ at the binary; dape speaks to that. Both code generators do
+— the hand-written one writes its compile unit, subprograms and line table out as
+bytes, since ~.loc~ cannot work against a file whose instructions are ~.byte~
+blobs, and what it does not describe is locals and types. lldb and gdb
 both ship DAP interfaces already.
 
 This is where /no object headers/ pays off a second time. Flan structs *are* C
@@ -756,17 +790,21 @@ building the whole live environment at once.
 1. *Freeze the model.* spec-memory.md and spec-conditions.md — done before any
    code. Fixed arrays, non-owning slices, move-only ~Vec~/~Map~, allocators,
    ~Ptr~, explicit ~clone~; the six restart cases. /Done./
-2. *Run calc-me.flan on the interpreter.* Reader, typed IR, checker,
-   tree-walking backend. /Exit criterion includes a measured throughput number/
-   — interpreted calls per second on a tight loop — because milestone 4's frame
-   budget depends on it (see Compilation). Packages, structs, ~(Ptr T)~ + ~addr~, byte slices,
+2. *Run calc-me.flan.* Reader, typed IR, checker, and a backend that can carry
+   the program end to end. The exit criterion was once a measured interpreter
+   throughput number; with no interpreter that criterion is gone and the narrow
+   host ABI took its place on the critical path (see Compilation). Packages,
+   structs, ~(Ptr T)~ + ~addr~, byte slices,
    ~at~/~len~, ~while~, ~set~ on the fixed place list, ~cond~, ~match~, ~Option~
    + ~some~, ~i32~/~u8~/~f64~, recursion, argv, stdout. No allocator, no ~Vec~,
    no generics, no user macros, no FFI, no window. Headless, so the acceptance
    test is a table of expression/result pairs.
 3. *Emit LLVM IR and pass the same calc-me test AOT*, on native and wasm32 in CI.
-   Both backends, one test table, one narrow host ABI (argv, stdout, exit). This
+   Both targets, one test table, one narrow host ABI (argv, stdout, exit). This
    is where the second target gets proven — while there is almost nothing to port.
+   The hand-written x86-64 code generator is not on this path: it arrived later,
+   as a second route to the same behaviour rather than a milestone of its own,
+   and is held to the LLVM backend's output byte for byte (see Compilation).
 4. *Run sand.flan.* Fixed 2-D arrays, ~dotimes~, ~defer~, and typed FFI to
    raylib including keyword→enum coercion. Acceptance test twice: headless (N
    frames, hash the grid — runnable in CI on both targets) and interactive at
@@ -776,8 +814,8 @@ building the whole live environment at once.
    special forms in the compiler.
 6. *Allocators, ~Vec~/~Map~, ~Result~/~try~/~errdefer~, then conditions and
    restarts* against spec-conditions.md, with dedicated tests per numbered case.
-7. *Hot reload* — free in the interpreter, indirection cells for compiled dev
-   builds, with signature generations and stale-caller warnings, plus the
+7. *Hot reload* — indirection cells in dev builds, with signature generations
+   and stale-caller warnings, plus the
    remaining compatibility limits written down and enforced: struct layout
    changes, live callbacks held by C, captured environments.
 8. *Debugger, nREPL, async* — last, and 8 splits into transport (8a) and editor
@@ -823,8 +861,8 @@ monomorphisation, no restarts and no reload.
 None of these block milestone 2. The milestone each one must be answered by is
 marked.
 
-1. *Host language: OCaml or Rust* — the only thing blocking the scaffold. See
-   Host language. /Milestone 2./
+1. *Host language: OCaml or Rust* — /settled: OCaml,/ and the compiler has been
+   written in it since. See Host language for what the choice turned on.
 2. Macro hygiene is settled for milestone 5: explicit ~gensym~, deliberately
    non-hygienic expansion, no local macros until a concrete use case appears.
 3. Borrow checking and escaping frame-arena values. /Deferred; revisit after
@@ -855,7 +893,8 @@ marked.
    a ~defvar~. Each needs an answer of the form "rejected", "accepted with a
    migration", or "accepted and the old code keeps running".
 7. Does the interpreter survive milestone 3, or is the compiled path the only
-   backend? /Milestone 3, on measured numbers./ See Compilation.
+   backend? /Settled: the compiled path is the only one, and there is no
+   interpreter./ See Compilation, and docs/BUILT.md's "Why there is no interpreter".
 8. ~(Option a)~ /settled:/ an ordinary stdlib union with ~Some~/~None~; the
    compiler niche-optimises ~(Option (Ptr T))~ to a nullable pointer. The
    CL-vs-Clojure truthiness question is moot under static typing.
@@ -875,8 +914,10 @@ marked.
 - Dev redefinition latency → ~16ms, measured: ~llc~ + ~ld -shared~ + ~dlopen~,
   never the ~clang~ driver, ~dlopen~ off the game thread, cells published in a
   batch at a frame boundary. See Compilation.
-- Dev backend → interpreter for milestone 2 certainly. Whether it /survives/
-  milestone 3 is open, not settled — see Compilation.
+- Dev backend → compiled, and only compiled. The interpreter that milestone 2
+  was going to be written against was never needed and does not exist: expression
+  eval is a compiled shared object like everything else, and a macro is the case
+  that made the absence load-bearing rather than merely tidy. See Compilation.
 - ~set~ on places → a fixed list of assignable forms, not ~setf~.
 - Loop story → imperative ~while~/~until~/~dotimes~ with ~break~/~continue~ and
   ~return~; ~loop~/~recur~ only if it later earns its place. It did: both are

spec-conditions.md

@@ -139,6 +139,31 @@ non-idempotent mutation bites. §3's rule that every clause body and the body
 share a type places the restart syntactically; nothing places it *semantically*,
 and that choice is the author's.
 
+**Which of the runtime's own conditions establish a restart, and why only some
+do.** Four are signalled from below the program with `error`: `StorageExhausted`
+when an allocator cannot satisfy a request, `FileError` when a file operation
+fails, `BoundsError` for an index or a slice outside its container, and
+`ArithError` for an arithmetic operation that has no answer — a divide or
+remainder by zero, `INT64_MIN / -1`, and a float-to-integer cast whose value does
+not fit, each of which was a raw `SIGFPE` or an undefined result before it was a
+condition. The first two establish a `retry` restart at the failing site, because
+their attempt is repeatable: a handler frees something or supplies another path
+and the same operation then succeeds. The last two establish **nothing**, and
+that is a decision rather than an omission. Nothing a handler can do makes index
+51 valid for a length-50 array or makes a division by zero have a quotient, so
+there is no attempt to resume into. A site restart would also have to be
+allocated by the `restart-case` that offers it, on its own stack (§3), which
+means an `alloca` and a push/pop pair emitted at every indexing and every
+division in every checked build — and what it would buy is a *different* answer,
+silently.
+
+So the rule this section describes is unchanged by them: the restarts that matter
+for a bad index or a bad division are the ones the program already established —
+a frame loop's `continue` — and those are on the restart stack and reachable from
+a handler or from the break loop without anything being pushed at the failing
+site. Allocation and file failure are the named exceptions, and spec-memory.md's
+"Allocation failure" says why they have to be.
+
 ## 6. Crossing compiler-generated frames
 
 Transfer is lowered **explicitly** — result propagation plus branch targets — not

spec-memory.md

@@ -38,12 +38,16 @@ enums, strings, fixed arrays, and value structs composed recursively from those
 types. Tuples and triples join that set when they are introduced. `Ptr`, slices,
 `Vec`, and `Map` are not map keys yet.
 
-Equality and hashing for those keys are compiler-provided structural operations,
-not type classes and not operations available to an unconstrained type variable.
-An empty map takes its type from its context:
+Equality and hashing for those keys are compiler-provided structural operations
+and not type classes. They are not available to an unconstrained type variable
+either; a variable that means to key a map declares `hashable?` in the signature
+that binds it, and the refusal then lands at the call site that names an
+unhashable key. An empty map names its key and value types, because a global
+cannot hold one and there is therefore no declaration for it to take a type from:
 
 ```
-(defvar enemies (Map string Enemy) (map-new))
+(let [enemies (map-new string Enemy)]
+  ...)
 ```
 
 `(get m k)` returns `(Option V)`: absence is `None`, not an untyped `nil`.
@@ -128,26 +132,54 @@ visible in the type:
 
 ## Generics
 
-Parametric polymorphism is monomorphisation, with **no type classes and no
-constraints**. The consequence is a hard rule:
+Parametric polymorphism is monomorphisation, with **no type classes**. A type
+variable is written `$t` wherever a *type* goes — a parameter, the return type,
+or nested as `[$t]` or `(Vec $t)` — and bare `t` where a type's *name* is an
+argument in expression position, as in `(vec-new t)` and the cast `(t x)`. A
+generic body is checked **abstractly**, with nothing substituted, so the rule
+below bites at the definition rather than at whichever call site first
+instantiates it:
 
-> A type variable `a` supports only what every type supports: move, `clone`,
+> A type variable `$t` supports only what every type supports: move, `clone`,
 > field-free storage. It does **not** support `=`, `<`, `+`, or `hash`.
 
-Anything else is passed in explicitly as a function value:
+What makes that liveable is a `where` clause of compile-time type predicates,
+written as a map at the head of the body. There are five — `ordered?`, `equal?`,
+`hashable?`, `numeric?`, `copyable?` — they are not type classes because a
+predicate carries no implementations and merely gates a builtin the compiler
+already has, and they entail one another in one direction, so one clause usually
+does. A variable is move-only by default and `copyable?` is the opt-out, because
+whether a variable moves is not decidable abstractly. plan.org's Types section
+has the full account.
 
 ```
-(defn largest [xs [a]  gt (Fn [a a] bool)] (Option a) ...)
+(defn sort! [s [$t]] ()
+  {:where (ordered? $t)}
+  ...)
 ```
 
-Ordered/arithmetic operators over `a` are therefore rejected, not silently
-instantiated. The alternatives — compile-time interfaces, or intrinsics
-restricted to primitives — are deliberately deferred until the base checker is
-stable (build sequence milestone 4).
+Without such a clause the operator is rejected where it is written, not silently
+instantiated, and the operation is passed in explicitly as a function value
+instead:
+
+```
+(defn largest [xs [$t]  gt (Fn [$t $t] bool)] (Option $t) ...)
+```
+
+The value handed to such a parameter is a named `defn`. An `fn` cannot be written
+inline into it, because the generic body is checked with nothing substituted and
+there is no concrete type yet for the `fn`'s own parameters to come from; that
+restriction lifts at a monomorphic call site, where `reduce`'s and `filter`'s
+callbacks are ordinary inline `fn`s.
+
+The alternatives to predicates — compile-time interfaces, or intrinsics
+restricted to primitives — remain deliberately deferred until the base checker is
+stable (build sequence milestone 4). The ceiling is that nobody can supply a
+user-defined `<`.
 
 `println` is the deliberate exception. It is a compiler-provided,
 type-directed intrinsic: monomorphisation selects or emits a structural printer
-for each concrete instantiation, so `(println x)` is legal for `x : a` without
+for each concrete instantiation, so `(println x)` is legal for `x : $t` without
 introducing a `Printable` type class. Structs, fixed arrays, options and,
 eventually, Vecs and Maps print structurally. `Ptr` and `Handle` print their
 address or identity rather than recursively dereferencing, and collection

syntax-sketch.flan

@@ -2,11 +2,13 @@
 ;;
 ;; Rules held here:
 ;;   - every type notation reads as exactly ONE data item
-;;   - types are inline name/type pairs, as in `let` and `defstruct`
+;;   - types are inline name/type pairs, as in `defstruct` and a restart-case
+;;     clause. NOT in `let`: a local is inferred and takes no annotation
 ;;   - the return type is always written; () is unit, a real zero-sized type
 ;;     rather than C's void
-;;   - lowercase type names are variables, Capitalized are concrete
-;;   - no `!` convention (nothing is immutable), no `->`, no sigils
+;;   - a type VARIABLE is $t; every other type name is concrete, whatever its
+;;     case. Lowercase-is-a-variable was the first spelling and is gone
+;;   - no `!` convention (nothing is immutable), and no `->`
 ;;
 ;; Normative references: spec-memory.md (ownership, containers, places,
 ;; generics, function values) and spec-conditions.md (restart semantics).
@@ -31,8 +33,8 @@
 ;; $t)}, is the other brace form, and it sits after the return type.
 ;;   (Ptr World)   pointer
 ;;   (Fn [f32] bool)  function pointer, no captured environment
-;;   (Option a)    union from the stdlib
-;;   (Handle a)    generational handle into a pool
+;;   (Option $t)   union from the stdlib
+;;   (Handle $t)   generational handle into a pool
 ;;
 ;; A struct is a value type iff all its fields are. One Vec field makes it
 ;; move-only. Copying an owning container is always explicit: (clone v).
@@ -57,22 +59,51 @@
     (Circle r) (* PI r r)
     (Rect w h) (* w h)))
 
-;; ── Lowercase = type variable. Monomorphised at each call site ────────
-;; There are no type classes, so `a` supports only what EVERY type supports.
-;; Ordering is not that — it is passed in as a function value. Type arguments
-;; are inferred from the argument types; there is no explicit instantiation.
-;; The inner `fn` captures `gt`, a parameter: legal because it does not outlive
-;; this frame (spec-memory.md, non-escaping fn).
-(defn largest [xs [a]  gt (Fn [a a] bool)] (Option a)
+;; ── $t binds a type variable. Monomorphised at each call site ─────────
+;; The sigil is on the type, everywhere a type goes: [$t], (Fn [$t $t] bool),
+;; (Option $t). Bare t is the same variable where a type's NAME is an argument
+;; in expression position — (vec-new t), (map-new t i32), the cast (t x).
+;; There are no type classes, so $t supports only what EVERY type supports, and
+;; the body is checked abstractly, so an unsupported operation is an error here
+;; rather than at the first call site that happened to instantiate it. Ordering
+;; is not supported, so it is passed in as a function value. Type arguments are
+;; inferred from the argument types; there is no explicit instantiation.
+(defn largest [xs [$t]  gt (Fn [$t $t] bool)] (Option $t)
+  {:where (copyable? $t)}
   (if (> (len xs) 0)
-    (Some (reduce (fn [x y] (if (gt x y) x y)) (at xs 0) xs))
+    (let [best (at xs 0)]
+      (dotimes [i (len xs)]
+        (when (gt (at xs i) best) (set best (at xs i))))
+      (Some best))
     None))
 
-;; (largest hps >)   — `>` at i32 is an ordinary function value
-;; (largest es (fn [x y] (> (.hp x) (.hp y))))
+;; A {:where ...} clause admits the operator instead of taking it as an
+;; argument. Five predicates — ordered? equal? hashable? numeric? copyable? —
+;; and each instantiation is checked against the ones the signature declares.
+(defn smallest [xs [$t]] (Option $t)
+  {:where (ordered? $t)}
+  (if (> (len xs) 0)
+    (let [m (at xs 0)]
+      (dotimes [i (len xs)] (set m (min m (at xs i))))
+      (Some m))
+    None))
+
+;; (largest hps taller)  — a top-level defn is an ordinary function value.
+;; An OPERATOR is not: `>` is not a name, and (largest hps >) is "unknown name
+;; >". Nor can an `fn` be written inline into a (Fn [$t $t] bool) argument: the
+;; generic body is checked with nothing substituted, so there is no type for the
+;; fn's own parameters to come from yet. Inside a generic the callback is a
+;; named defn; at a monomorphic call site, where the types are already
+;; concrete, the fn can be written inline where it is used.
 
 ;; Parameters are immutable values; pass a pointer to mutate. `[Enemy]` is a
 ;; borrowed slice — centroid neither owns nor frees the storage.
+;; This one is still a sketch of where the syntax is going and does not compile
+;; today, on two counts worth naming rather than leaving to be discovered:
+;; component-wise `+` and `/` over a fixed array are planned and not built, and
+;; the prelude's `reduce` is (reduce s init f) with its accumulator at the
+;; ELEMENT type, so it cannot fold an [Enemy] into a Vec2. Written against what
+;; exists, this is a `dotimes` accumulating into a local.
 (defn centroid [es [Enemy]] Vec2
   (/ (reduce (fn [acc e] (+ acc (.pos e))) [0 0] es)
      (f32 (len es))))
@@ -122,7 +153,9 @@
 ;; load-texture cannot know the right recovery — an editor wants a placeholder,
 ;; a release build wants to abort, a hot-reload session wants to retry after the
 ;; file is fixed on disk. So it offers a menu and the caller chooses.
-(defcondition AssetMissing [path string])
+;; A condition type is an ordinary struct — there is no defcondition, and no
+;; class hierarchy to put one in. Matching is by type plus a predicate.
+(defstruct AssetMissing [path string])
 
 ;; `signal` has type () and RETURNS if every handler returns normally, so the
 ;; fall-through path of a restart-case in value position must still produce the
@@ -139,8 +172,12 @@
 
 ;; Intermediate frames say nothing about AssetMissing. Nothing to thread.
 ;; invoke-restart has type Never: it does not return to the handler.
-(defn load-level [path string] () Level
-  (handler-bind [AssetMissing (fn [c]
+;; A handler clause is (Type [name] body ...) — the type, then the one binding,
+;; then the body. It is not a type paired with an `fn`, and a handler closes
+;; over nothing: it is lifted into its own function, so a value it wants to keep
+;; goes on the condition or into a global.
+(defn load-level [path string] Level
+  (handler-bind [(AssetMissing [c]
                    (log "missing asset:" (.path c))
                    (invoke-restart 'use-placeholder))]
     (parse-level (slurp path))))
@@ -160,10 +197,9 @@
 
 (defn collect-parse-errors [src string] (Result Ast)
   (let [errors (make-vec ParseError)]
-    (handler-bind [ParseError (fn [c]
+    (handler-bind [(ParseError [c]
                      (push errors c)              ; value struct: copies out of
-                                                  ; the signalling frame
-                                (invoke-restart 'skip-form))]
+                     (invoke-restart 'skip-form))] ; the signalling frame
       (let [ast (parse-all (parser src))]
         (if (zero? (len errors))
           (Ok ast)

web/examples/arith.flan

@@ -0,0 +1,9 @@
+;; Three integer operations have no right answer. Each used to be a bare SIGFPE
+;; or an undefined value; each signals ArithError now. The divisor goes through
+;; a global so that constant folding cannot answer it before the backend does.
+(defvar zero i32 0)
+
+(defn main [] ()
+  (println "before")
+  (println (/ 10 zero))
+  (println "unreachable"))

web/examples/arith.out

@@ -0,0 +1,3 @@
+before
+arith.flan:8:12: divide by zero: (/ 10 0)
+exit 134

web/examples/cast.flan

@@ -0,0 +1,7 @@
+;; A float-to-integer cast whose value does not fit. The condition it violated
+;; is reported as the range the destination type can hold, which is the same
+;; shape BoundsError uses for a slice: the violated condition, written out.
+(defvar big f64 1e30)
+
+(defn main [] ()
+  (println (i32 big)))

web/examples/cast.out

@@ -0,0 +1,2 @@
+cast.flan:7:17: this value does not fit the integer type it is cast to, which holds [-2147483648 2147483647]
+exit 134

web/examples/printing.out

@@ -1,6 +1,6 @@
 42
 1.5
-(Enemy {:hp 3 :name "wisp" :key :left})
+(Enemy {.hp 3 .name "wisp" .key :left})
 (some 32)
 none
 no newline: true

web/index.html

@@ -434,6 +434,57 @@ Measured cost on a
 50-million-iteration dependency chain over a 1024-element array: 0.11–0.12s checked
 against 0.12–0.13s unchecked.</p>
 
+<h3>So is arithmetic that has no answer</h3>
+
+<p>Three integer operations have no right result, and each of them used to be a bare
+<code>SIGFPE</code> or an undefined value: a divide or remainder by zero, the one division
+that overflows (<code>INT64_MIN / -1</code>, whose true quotient is one past the top of
+the type), and a float-to-integer cast whose value does not fit. All three now signal
+<code>ArithError</code>, the way a bad index signals <code>BoundsError</code>.</p>
+
+<pre><code>;; Three integer operations have no right answer. Each used to be a bare SIGFPE
+;; or an undefined value; each signals ArithError now. The divisor goes through
+;; a global so that constant folding cannot answer it before the backend does.
+(defvar zero i32 0)
+
+(defn main [] ()
+  (println "before")
+  (println (/ 10 zero))
+  (println "unreachable"))</code></pre>
+
+<pre><code class="sh">$ flan run arith.flan
+before
+arith.flan:8:12: divide by zero: (/ 10 0)
+$ echo $?
+134
+
+$ flan run cast.flan
+cast.flan:7:17: this value does not fit the integer type it is cast to, which
+holds [-2147483648 2147483647]</code></pre>
+
+<pre><code>;; A float-to-integer cast whose value does not fit. The condition it violated
+;; is reported as the range the destination type can hold, which is the same
+;; shape BoundsError uses for a slice: the violated condition, written out.
+(defvar big f64 1e30)
+
+(defn main [] ()
+  (println (i32 big)))</code></pre>
+
+<p>A Lisp that stops naming the file and the line beats one that dies with
+<code>SIGFPE</code>, and a program that genuinely does not care installs a handler once at
+startup and never thinks about it again. Float division is deliberately left alone: IEEE
+already answers it, with an infinity or a NaN.</p>
+
+<p><strong>No restart is established at the failing operation</strong>, which is the same
+decision <code>BoundsError</code> made and for the same reason. A restart frame is
+allocated by the <code>restart-case</code> that offers it, on that frame's own stack, so
+nothing below the program can push one on its behalf; a <code>use-value</code> at a
+division would mean an <code>alloca</code> and a push-and-pop emitted at every division in
+every checked build, and what it would buy is a silently different answer. What answers a
+division by zero is the restart the program already had — a frame loop's
+<code>continue</code> — which is on the stack and reachable from a handler or from the
+break loop without anything being pushed at the failure.</p>
+
 <h2 id="types">Types</h2>
 
 <p>Types are annotated at function boundaries and inferred everywhere else. Every type
@@ -946,7 +997,7 @@ user-supplied printer to choose between.</p>
 
 <pre><code class="sh">42
 1.5
-(Enemy {:hp 3 :name "wisp" :key :left})
+(Enemy {.hp 3 .name "wisp" .key :left})
 (some 32)
 none
 no newline: true</code></pre>
@@ -1248,9 +1299,10 @@ not in a <code>defer</code>, because a defer runs on the ordinary return path to
 that version silently rolls back the frames that succeeded.</p>
   <p>This matters more here than in most Lisps because the intended use is a
   <em>game loop</em>, where the plan is to skip a frame and carry on rather than die. Now
-  that a bad index signals <code>BoundsError</code> instead of ending the process,
-  abandoning a frame and retrying it is a real thing to do — and that is exactly the case
-  a non-idempotent mutation spoils.</p></li>
+  that a bad index signals <code>BoundsError</code> and a bad division signals
+  <code>ArithError</code> instead of ending the process, abandoning a frame and retrying
+  it is a real thing to do — and that is exactly the case a non-idempotent mutation
+  spoils.</p></li>
   <li><strong>An unknown restart name is a hard stop</strong> — a located runtime error.
   There is no <code>find-restart</code> to test with yet.</li>
   <li><strong>No supertype</strong>, so nothing can say "any condition".</li>
@@ -1394,7 +1446,7 @@ the same <code>declare-c</code> line a person would have written, and writes the
 <code>generated.flan</code> in the package — which is <em>committed</em>.</p>
 
 <pre><code class="sh">$ flan generate-c vendor/raylib
-wrote vendor/raylib/generated.flan: 269 declarations, 117 refused, of 581 functions
+wrote vendor/raylib/generated.flan: 268 declarations, 117 refused, of 581 functions
 in vendor/raylib/raylib-5.5.h.
 Every defstruct, every hand-written declare-c and every mapped
 constant agrees with it.</code></pre>
@@ -1833,19 +1885,32 @@ own internal calling convention (every aggregate by pointer, no eightbyte rule,
 classifier) and match SysV only at the C boundary, where the shim has already flattened
 every struct.</p>
 
-<p>It covers a subset of the IR and <strong>refuses the rest by name</strong>, so a
-build that succeeds is one it really compiled rather than one it half-compiled.
-Conditions are the visible gap — anything reaching the transfer channel is refused:</p>
+<p>It <strong>refuses by name</strong> anything it does not lower, so a build that
+succeeds is one it really compiled rather than one it half-compiled. Conditions were the
+visible gap once and are not any more: the transfer channel, the guard after every call,
+bounds and arithmetic failures, indirection cells, redefinition modules and DWARF line
+tables all landed, and what is left refused is narrow — an aggregate crossing the C
+boundary is the one worth naming, because closing it would mean the eightbyte classifier
+this backend is built on not having.</p>
 
-<pre><code class="sh">$ flan build test/programs/algorithms.flan --x86
-Fatal error: exception Flan.X86.Unsupported("restart-case needs the transfer
-channel, which this backend does not emit a guard for")</code></pre>
+<p>What holds it honest is that every program in the corpus is built both ways and the
+two are compared byte for byte on stdout, stderr and exit status — not on a disassembly,
+which has read perfectly beside a wrong answer more than once. <code>spike/x86/survey.sh</code>
+is the script, and it currently reports <strong>103 MATCH, 0 DIFFER, 0 refused by
+name</strong>, with 38 programs skipped because they do not compile on either side, have
+no <code>main</code>, or run forever. <code>dune build @x86</code> runs it as part of the
+build, so a refusal cannot sit unnoticed.</p>
 
 <p><code>--debug</code> is a third flag beside <code>--dev</code> and the optimisation
 level. <code>--dev</code> asks whether you can redefine the program while it runs;
 <code>--debug</code> asks whether you can stop it and read it. It emits DWARF, sets
 <code>-O0</code>, and is refused by name for wasm32. lldb needs no plugin to read a
-Flan struct: the struct is its C struct.</p>
+Flan struct: the struct is its C struct. Both backends emit it, though not the same
+amount: the hand-written one writes a compile unit, a subprogram per function and a line
+table out as bytes, because <code>.loc</code> cannot work against a file whose
+instructions are <code>.byte</code> blobs, so <code>--x86 --debug</code> gives a
+backtrace naming Flan files, functions and lines while <code>print x</code> says the name
+is not in the current context.</p>
 
 <p>Some things are refused by name rather than half-supported, and both cross-target
 refusals say why:</p>