iter design-md-rolesplit.1 (DONE 9/9): DESIGN.md -> design/ ledger role-split

The 3020-line docs/DESIGN.md is replaced by the design/ ledger:
design/INDEX.md (sole addressable spine, typed Contracts+Models tables,
polymorphic links — prose file OR authoritative source //!), 14
design/contracts/*.md test-linked invariants + 3 source-link-only
contracts (mangling/env-construction/qualified-xref, no prose file —
code is SoT), 5 design/models/*.md whitepapers, and
docs/journals/2026-05-19-design-decision-records.md (the
relitigation-guard archive — every why/rejected/does-not-do/rollback/
empirical ### moved out at ###-granularity). Clean cut: git rm
docs/DESIGN.md, no stub.

RED-first crates/ailang-core/tests/design_index_pin.rs — the 4-clause
anti-regrowth spine (DESIGN.md-gone / every-INDEX-link-resolves /
every-contract-names-a-resolvable-ratifier /
contracts-carry-no-decision-record-prose) — demonstrably RED before,
GREEN after. Build-atomic by task ordering: design_schema_drift.rs's
include_str! (the only compile-time consumer) retargeted to
design/contracts/data-model.md BEFORE the deletion; its
## Data model/## Pipeline slicer dropped (a simplification the split
enables). 2 NoInstance diagnostics + 2 lockstep E2Es retargeted to
design/contracts/{float-semantics,typeclasses}.md. ~12 agent reading
lists + 5 SKILL bodies + CLAUDE.md + skills/README.md + ~25
code/C/.ail/spec comment xrefs retargeted; OQ7 dangling 'Iter 13b'
cite deleted (no forward target — a pointer would be fiction).
honesty-rule.md rewritten so the rule names the new home
(rationale->journals), resolving the recon-found internal
contradiction; the two docs_honesty_pin.rs:70,72 pinned phrases kept
verbatim+contiguous.

Boss-verified independently: cargo test --workspace 646 passed /
0 failed; design_index_pin 4/4; acceptance grep CLEAN of live
DESIGN.md refs (residuals = only the spec-mandated clause-4
deletion-enforcer). 2 DONE_WITH_CONCERNS routed to the mandatory
milestone-close audit: (a) str-abi.md:23 '(iter str-concat,
2026-05-13)' provenance stamp trips advisory architect_sweeps Sweep-1
— Boss-confirmed byte-identical to DESIGN.md@deeffb1:2062-2065, a
faithfully-migrated PRE-EXISTING anchor (regexes verbatim, only path
retargeted), NOT split-introduced — RATIFY-or-tidy at audit; (b) a
now stale-direction intra-prose 'see Str ABI below' cross-ref in
float-semantics.md — audit-adjudication candidate. Plan defect noted:
Task 9 Step 4's verbatim acceptance grep used a ^./ anchor not
matching the system's grep -rIn output; substance re-verified CLEAN.

Spec grounding-check PASS x2. Journals INDEX + decision-records
pointer appended (Boss-only).

design/models/authoring-surface.md

@@ -0,0 +1,226 @@
+# Authoring surface — notation rationale whitepaper
+
+## Candidate notations (same `map` encoded in each)
+
+The reference target — the polymorphic `map` from `examples/list_map_poly.ail.json`:
+
+```
+data List a where Nil | Cons a (List a)
+fn map : forall a b. ((a) -> b, List a) -> List b
+       = \f xs. match xs of Nil -> Nil
+                          | Cons h t -> Cons(f(h), map(f, t))
+```
+
+#### (A) S-expression with fully-tagged AST nodes
+
+```
+(module list_map_poly
+
+  (data List (vars a)
+    (ctor Nil)
+    (ctor Cons a (con List a)))
+
+  (fn inc
+    (type (fn-type (params (con Int)) (ret (con Int))))
+    (params x)
+    (body (app + x 1)))
+
+  (fn map
+    (type
+      (forall (vars a b)
+        (fn-type
+          (params (fn-type (params a) (ret b)) (con List a))
+          (ret (con List b)))))
+    (params f xs)
+    (body
+      (match xs
+        (case (pat-ctor Nil) (term-ctor List Nil))
+        (case (pat-ctor Cons h t)
+          (term-ctor List Cons
+            (app f h)
+            (app map f t)))))))
+```
+
+Grammar core (3-rule lexical layer + ~25 named-form productions):
+```
+sexpr  ::= atom | "(" sexpr* ")"
+atom   ::= integer | string | ident
+ident  ::= any maximal non-whitespace, non-paren run that is not
+           a recognised integer or string literal.
+```
+
+The lexer recognises one delimiter (`(` / `)`) and whitespace.
+Every other maximal token is classified post-hoc:
+- All-digit run with optional leading `-` → integer atom.
+- `"`-delimited run → string atom.
+- Otherwise → ident.
+
+Consequence: operators like `+`, `==`, `<=`, `**`, qualified
+names like `io/print_str`, and cross-module references like
+`std_list.map` are all single ident tokens with no special lex
+rule. The only reserved tokens are `(`, `)`, and whitespace.
+Bool literals (`true`, `false`) and unit (`(lit-unit)`) are
+disambiguated by parser context, not by lex.
+
+Every AST node form has a unique head keyword (`module`, `data`,
+`fn`, `forall`, `fn-type`, `con`, `var`, `app`, `lam`, `match`,
+`case`, `pat-ctor`, `term-ctor`, `do`, `seq`, ...). A bare atom in
+a positional slot (e.g. inside `(con List a)` second position) is
+a name reference whose **sort** is determined by the parent slot:
+
+- inside `(con NAME args...)` second-and-later positions → type
+  expression. Bare atom there ⇒ `Type::Var { name }`.
+- inside `(app HEAD args...)` first position ⇒ `Term::Var`.
+- inside `(pat-ctor CTOR fields...)` field positions ⇒
+  `Pattern::Var`.
+- inside `(case PAT BODY)` second position ⇒ term.
+
+There is **no lexical case rule**. To construct a value with a
+ctor, write `(term-ctor TypeName CtorName args...)`. To match
+against one, write `(pat-ctor CtorName fields...)`. Capitalised
+identifiers carry no special meaning to the parser. This rules
+out a class of silent errors ("I forgot to capitalise `Cons` and
+it parsed as a function call").
+
+**Pros:** smallest formal grammar of any candidate (the lexical
+core is 3 rules; the named-form productions are uniform — every
+node a tagged list). Foreign-LLM bar lowest. Round-trip with the
+existing pretty-printer is a refactor of `pretty.rs` to emit this
+tagged form, plus a new parser.
+
+**Cons:** paren density is high. `(forall (vars a b) (fn-type
+...))` has more visual nesting than the current pretty-printer's
+`forall a. (...) -> ...`. Verbosity is ~2× JSON for the same node
+when measured in characters, but ~8× shorter in lines (the
+existing JSON `box.ail.json` of 160 lines becomes ~20 lines in
+this form).
+
+#### (B) Indented record-style with explicit terminators
+
+```
+module std_list
+
+data List(a):
+  Nil
+  Cons(a, List(a))
+end
+
+fn map:
+  type: forall a b. fn(fn(a) -> b, List(a)) -> List(b)
+  params: f, xs
+  body:
+    match xs:
+      Nil          => Nil
+      Cons(h, t)   => Cons(f(h), map(f, t))
+    end
+end
+```
+
+Grammar core (~20–30 productions): module-level (def/data/end), type
+sub-grammar (forall, fn, con, var), term sub-grammar (lam, match,
+ctor, app, lit, var, seq), pattern sub-grammar.
+
+**Pros:** higher information density per line, closer to mainstream
+ML/Haskell shape. **Cons:** four sub-grammars instead of one.
+`forall a b. fn(...)` keeps a pseudo-precedence (`->` binds tighter
+than the outer `fn(...)` wrapper). Foreign-LLM bar higher.
+
+#### (C) Pretty-printer-as-source
+
+Use exactly the format `pretty::module` already emits, plus a parser
+that accepts it. The existing pretty-printer's quirks (`::` for
+type-of, `[params]` for fn-params, `<a>` for type-args, `forall a. ...`,
+`!IO`, `()` ambiguous between unit-arg-list and empty-form) become
+the spec.
+
+**Pros:** zero churn — the existing pretty-printer is already the
+spec; only the inverse is missing. Round-trip is the identity by
+construction. **Cons:** the existing format mixes four mini-dialects
+(s-expr at term level, ML-shape at type level, square brackets for
+params, `<>` for type args). Formalising it crisply is harder than
+designing a uniform form from scratch.
+
+## Form (B) — human prose projection
+
+AILang ships a
+second textual projection of the AST: `ailang-prose`, a one-way
+projection from `Module → human-readable text`. It is **not** an
+authoring surface; it is the "display" projection that Decision 6's
+architectural pin (line 167–176) explicitly anticipated:
+
+> *"Future projections are explicitly anticipated: a visual /
+> graphical front-end is a plausible second projection for human
+> review and inspection (display being the one case where non-AI
+> eyes matter). The architecture leaves room: any producer of
+> well-formed `ailang-core::ast::Module` values is a valid
+> front-end."*
+
+Form (B) targets the specific failure mode where a human reviewer
+needs to read an AILang module quickly. Form (A) was designed to
+fit a 30-production EBNF spec and to be parsed zero-shot by foreign
+LLMs; that prioritisation makes it dense and visually noisy for
+human readers. Form (B) inverts the trade-offs:
+
+- **Rust-flavoured surface.** Braces and `=>` for match arms,
+  Rust-aligned 4-level operator precedence, infix arithmetic
+  (`a + b`, not `+(a, b)`), unary `!` for `not`.
+- **Lossy by design.** Projection elides machinery the LLM can
+  re-derive: `(con T)` wrappers (`(con Int)` → `Int`), the
+  `(fn-type (params ...) (ret ...))` wrap, `(term-ctor T C ...)`
+  collapses to `C(...)`, redundant parens. Only the AST machinery
+  whose information is recoverable from typecheck context.
+- **Lossless on load-bearing detail.** Mode annotations
+  (`own T`, `borrow T`), effects (`with IO`), explicit `clone`,
+  `reuse-as`, doc strings, type annotations on signatures and
+  lambdas, the `tail` flag — all preserved verbatim.
+
+Critically, **form (B) has no parser**. Form (A) is round-trippable
+by construction (Decision 6 constraint 2); form (B) deliberately is
+not. Re-integrating prose edits requires an external LLM mediator,
+not a compiler pass — see `docs/PROSE_ROUNDTRIP.md` for the
+six-step cycle and the prompt template `ail merge-prose` composes.
+
+Form (B) does not weaken any Decision 6 invariant:
+
+- The JSON-AST remains the only hashable artefact. Prose is not
+  hashed, not content-addressed, not load-bearing for any
+  cross-module reference.
+- Form (A) remains the canonical authoring surface. Foreign LLMs
+  still author against form (A); humans review and edit through
+  form (B).
+- The 30-production grammar of form (A) is unchanged.
+- `ailang-check` and `ailang-codegen` remain projection-agnostic;
+  `ailang-prose` is a downstream consumer of `ailang-core::ast`,
+  parallel to `ailang-surface` but in the rendering direction only.
+
+The CLI gains `ail prose <m.ail.json>` (the deterministic
+projection) and `ail merge-prose <m.ail.json> <edited.prose.txt>`
+(the mediator-prompt composer); both are listed in the CLI section
+below.
+
+**Form-A spec embedding.** An earlier `merge-prose`
+prompt instructed the LLM to emit JSON-AST and offered a 12-line
+schema-essentials reminder; that combination did not give a
+foreign LLM enough to produce valid output. The current prompt revises this:
+
+- The LLM emits **Form-A** (the canonical authoring surface), not
+  JSON. JSON-AST stays the only hashable artefact, but it is not
+  a writing surface. The user runs `ail parse foo.new.ail`
+  before `ail check` to produce the canonical JSON.
+- `crates/ailang-core/specs/form_a.md` is the complete LLM-targeted
+  Form-A specification — grammar, every term / pattern / type /
+  def keyword, schema invariants, pitfall catalogue, four
+  few-shot modules drawn from `examples/*.ail`. It is exported
+  as `ailang_core::FORM_A_SPEC` and embedded verbatim in every
+  `merge-prose` prompt.
+- `crates/ailang-core/tests/spec_drift.rs` walks every variant of
+  `Term`, `Pattern`, `Type`, `Def`, `Literal` via exhaustive
+  `match` and asserts an anchor for each appears in the spec.
+  The exhaustive match is the load-bearing piece: adding a new
+  variant without updating the match fails compilation in this
+  test, before its assertions even run. Hand-written content,
+  mechanical drift detection.
+
+The cycle's lowest-common-denominator path is the static prompt
+(`ail merge-prose | client | ail parse | ail check`), which works
+with any client.

design/models/effects.md

@@ -0,0 +1,16 @@
+# Effects — pure core + algebraic effects
+
+## Decision 3: pure core language + algebraic effects
+
+The default is total, pure functions. Effects are declared as a set in the
+function type: `(Int) -> Int ![IO]`. The effect set is a
+flat, unordered, closed set of effect names, unified by set-equality —
+there is no effect row variable; a signature lists exactly the effects
+its body may perform.
+In the MVP only the effect `IO` is wired up (its sole op is `io/print_str`).
+`Diverge` (for non-termination) is reserved as an effect name but is
+unimplemented — no op, no codegen, no checker injection — in the same
+sense Decision 4 reserves refinements.
+
+This is the most important LLM property: when I read a function, I can trust
+its signature without reading the body.

design/models/pipeline.md

@@ -0,0 +1,72 @@
+# Pipeline and CLI
+
+## Pipeline
+
+```
+.ail.json  ─┐
+            ├─ load + validate schema
+            ├─ resolve names + assign hashes
+            ├─ desugar (AST → AST)
+            ├─ typecheck (HM, effect rows; mode-strict per Decision 10)
+            ├─ lift_letrecs (post-typecheck AST → AST)
+            ├─ lower to MIR (SSA-like, named SSA values)
+            ├─ emit LLVM IR (.ll)
+            └─ clang -O2 *.ll -o binary
+                  --alloc=rc → emits inc/dec     (@ailang_rc_inc / _dec; canonical, default)
+                  --alloc=gc → links libgc       (@GC_malloc; parity oracle)
+```
+
+Two allocator backends share the same MIR. `--alloc=rc` is the
+canonical backend committed to in Decision 10 and the CLI default.
+The typechecker enforces
+`(own)` / `(borrow)` modes, codegen emits `ailang_rc_inc` / `_dec`
+calls at the points dictated by linearity, and `Term::Clone` /
+`Term::ReuseAs` materialise into actual rc-bumps and in-place
+rewrites respectively. `--alloc=gc` selects the transitional Boehm
+backend; `--alloc=rc` is the canonical backend (Decision 10) and the
+CLI default.
+
+The **desugar** pass (`ailang-core::desugar::desugar_module`) runs
+before typecheck and codegen in every entry point of `ailang-check`
+and `ailang-codegen`. It is a pure AST → AST rewriter — currently
+only flattens nested constructor patterns, but is the chosen
+home for any future surface-smoothing rewrites that should not bloat
+the core AST or the backends. **Critical invariant:** `CheckedModule.symbols`
+in the `check` entry point continues to hash from the *original*
+on-disk module, not the desugared one, so `ail diff` and `ail manifest`
+report identities that match the canonical JSON the user is editing.
+
+The **lift_letrecs** pass (`ailang-check::lift_letrecs`)
+runs **after** typecheck and **before** codegen, but only on the
+`build` / `run` paths — the `check` subcommand stops at typecheck
+and never sees a lifted module. It eliminates every `Term::LetRec`
+that the desugar pass left in place (the case where at least one
+capture is `Term::Let`-bound, so its type is only knowable after
+inference). The output is a module with synthetic `<hint>$lr_N`
+top-level fns appended, ready for codegen. Synthetic FnDefs added
+by this pass do **not** appear in `CheckedModule.symbols` — same
+invariant as the desugar-pass lifts.
+
+## CLI
+
+```
+ail check     <module.ail.json>          — loads, validates, typechecks
+ail manifest  <module.ail.json>          — table: name :: type !effects [hash]
+ail describe  <module> <name>            — detail of a definition (form-A body)
+ail render    <module.ail.json>          — JSON-AST  → form-A text  (exact inverse of `parse`)
+ail parse     <module.ail>              — form-A text → canonical JSON-AST
+ail prose     <module.ail.json>          — JSON-AST  → form-B (lossy human prose, no parser)
+ail merge-prose <m.ail.json> <m.prose.txt>
+                                         — compose the LLM-mediator prompt for the prose round-trip
+                                           (see docs/PROSE_ROUNDTRIP.md)
+ail deps      <module.ail.json>          — list cross-module references
+ail diff      <a.ail.json> <b.ail.json>  — content-addressed def-level diff
+ail workspace <entry.ail.json>           — list all modules transitively reachable from entry
+                                           (`--json` for machine output;
+                                           `manifest --workspace` and `diff --workspace`
+                                           extend single-module subcommands to workspaces)
+ail builtins                             — list built-in fns and effect ops
+ail emit-ir   <module> [--emit=staticlib]  — writes .ll (staticlib: a main-free kernel's IR, no @main)
+ail build     <module> [--emit=staticlib]  — full pipeline → binary (staticlib: lib<entry>.a + libailang_rt.a)
+ail run       <module>                   — build + execute (tempdir), passthrough exit code
+```

design/models/rc-uniqueness.md

@@ -0,0 +1,315 @@
+# RC + Uniqueness — memory model whitepaper
+
+## Decision 9: dual allocator — RC canonical, Boehm parity oracle
+
+AILang ships two allocator backends with an asymmetric role:
+
+- **RC is canonical.** `--alloc=rc` is the CLI default for
+  `ail build` and `ail run`. The runtime AILang's memory model
+  (RC + uniqueness inference) is designed for. New examples,
+  benches, and corpus tests run under RC unless they explicitly
+  pin GC.
+- **Boehm stays as a parity oracle.** `--alloc=gc` remains
+  reachable. Its load-bearing job is differential diagnosis: when
+  RC produces a segfault, refcount underflow, or wrong stdout, the
+  GC build of the same module is the cheap "memory bug or logic
+  bug?" probe. The end-to-end suite includes per-example
+  parity tests that run both backends and assert byte-identical
+  stdout — those tests are what make the oracle real.
+- **`--alloc=bump`** is unchanged: a leak-only bench instrument,
+  not a production target.
+
+Full Boehm retirement (drop libgc, remove the gc backend) reopens
+when the parity oracle stops paying its keep — concretely, when a
+few iter families ship without the gc arm catching anything that
+the rc arm did not already catch. Until then, the cost of
+keeping libgc as a build dependency is accepted in exchange for
+diagnostic leverage. Decision 10 (RC + uniqueness) holds as the
+specification of the canonical runtime; the rest of this section
+documents the Boehm half, retained as the oracle.
+
+**Choice: Boehm-Demers-Weiser conservative GC.** The simplest
+working option:
+
+- Replace `malloc(...)` with `GC_malloc(...)` in every IR site
+  (currently `lower_ctor`'s ADT box, `lower_lambda`'s env block
+  and closure pair).
+- Replace the IR-level `declare ptr @malloc(i64)` with
+  `declare ptr @GC_malloc(i64)`.
+- Add `-lgc` to the `clang` link command (in
+  `crates/ail/src/main.rs`'s `Build` / `Run` paths).
+- No language-level change. No AST change. No schema change.
+
+Rationale:
+
+- **Mature.** Boehm has been the default conservative GC for
+  decades. Linux distros ship it as `libgc` / `libgc-dev` /
+  `gc` (Arch).
+- **No language work.** Conservative scan of the C stack handles
+  AILang's stack frames without LLVM stack-map infrastructure
+  (which is its own multi-iter design).
+- **Single-iter integration.** Lift-and-shift of the four
+  allocation sites; all existing tests must still pass with
+  identical output.
+
+Trade-offs accepted:
+
+- **Conservative over-retention.** A user-supplied `Int` field
+  whose value happens to coincide with a heap address will pin
+  that allocation. In practice, vanishingly rare for typical
+  values; survivable.
+- **Pause time non-deterministic.** Boehm uses stop-the-world
+  mark-sweep. For LLM-author-written stdlib code at MVP scale,
+  pause times are not the bottleneck.
+- **Build-time dependency.** `libgc` must be installed on the
+  build host. Users without it get a link-time error from
+  clang, not a silent failure.
+
+## Per-fn arena via stack `alloca`
+
+This optimisation is layered on top of Boehm in its simplest form.
+`ailang-codegen` runs an escape-analysis pre-pass over every fn
+body (and every lifted lambda thunk body); allocations the pass
+proves do not outlive the fn frame are lowered to LLVM `alloca`
+instead of `@GC_malloc`. Allocations that may escape continue to
+use `@GC_malloc`. The Boehm collector is still linked and
+unchanged; this is purely an optimisation above the floor.
+
+**Allocation mechanism: LLVM `alloca`** (not a heap arena). Stack
+allocation matches the "freed at fn return" lifetime exactly,
+needs no malloc/free pair, and integrates with LLVM's existing
+optimiser (mem2reg / SROA may further promote the alloca'd box
+to registers if the box is small and its uses are simple). No
+new runtime is introduced; no language-level change; no AST or
+schema change.
+
+**Escape rule (conservative).** A `Term::Ctor` or `Term::Lam`
+allocation is non-escaping iff (1) it is the value of a
+`Term::Let { name = X, value = ALLOC, body = B }`, and (2) the
+body `B` does not let any value derived from `X` flow past the
+fn frame. "Derived from" follows two propagation rules:
+- A `Term::Match` whose scrutinee is a `Var` referring to a
+  tainted name propagates taint to every pattern-bound name in
+  every arm. (Pattern bindings hold field projections of the
+  scrutinee, which live inside the same allocation.)
+- A `Term::Let { name = Y, value = Var(t), ... }` where `t` is
+  tainted makes `Y` tainted in the let's body.
+
+A tainted name "escapes" if it appears in any of: the tail
+position of `B`, the arg list of any `Term::App` / `Term::Do`,
+the field list of a `Term::Ctor`, or the free-var capture set of
+a `Term::Lam`. The closure-pair-callee position of `Term::App`
+where the callee is a bare `Var` to the tainted name is NOT an
+escape (calling locally is fine).
+
+**What this is not.** Not a region-inference system. Not
+flow-sensitive within an arm. Not field-sensitive (pattern
+bindings are tainted wholesale). Precision can be improved later;
+correctness is the priority for this iter. A pessimistic answer
+(claiming an allocation escapes when it does not) only loses
+optimisation, never correctness.
+
+**Codegen integration.** Three sites in
+`ailang-codegen/src/lib.rs`:
+- `lower_ctor` — ADT box.
+- `lower_lambda` env block (when there are captures).
+- `lower_lambda` closure pair (always 16 bytes).
+
+Each site queries the per-fn `non_escape: BTreeSet<usize>` (raw
+pointer addresses of `Term::Ctor` / `Term::Lam` AST nodes flagged
+as non-escaping). On a hit the emitter writes
+`alloca i8, i64 <size>, align 8`; on a miss it writes
+`call ptr @GC_malloc(i64 <size>)`. The rest of the lowering (tag
+store, field stores, closure-pair packing) is identical.
+
+The closure-pair and its env share an escape verdict — they have
+parallel lifetimes. If the closure pair is non-escaping, the env
+is too.
+
+## Decision 10: memory model — RC + Uniqueness with LLM-author annotations
+
+**The GC bench (`bench/run.sh`) showed
+Boehm contributing a substantial fraction of runtime on allocation-heavy workloads
+that hold the heap fully live (bench notes in JOURNAL). The
+mainstream "RC + inference" position is extended with mandatory
+LLM-author mode annotations (`borrow` / `own`), explicit `clone`,
+first-class `reuse-as`, and `drop-iterative` data attrs.**
+
+The cost of GC is structurally in the allocate path — Boehm's
+`GC_malloc` is structurally slower than a bump pointer, and the bench
+workloads exercised allocate cost without collection cost.
+Tracing GC's irreducible variability cannot be tuned away; RC's
+costs are bounded and analysable per program point. A corpus
+committed to one memory model is expensive to switch — pre-
+stdlib is the cheapest moment to commit.
+
+**Choice.** AILang's canonical memory model is reference counting
+with static uniqueness inference **and explicit LLM-author
+annotations on fn signatures**, in the lineage of Lean 4 / Roc /
+Koka. Boehm becomes a transitional allocator (Decision 9) and is
+retired when the RC pipeline matches the bump-allocator floor
+within an acceptable margin (target 1.3× on `bench/run.sh`).
+
+**Workload scope of the 1.3× target.** The 1.3× target was
+calibrated on the original `bench/run.sh` corpus: linear list
+sum (`bench_list_sum`) and tree walk (`bench_tree_walk`) — uniform
+single-allocation-per-step workloads where one inc/dec pair
+amortises against one allocation. The corpus was later extended
+with `bench_closure_chain` (closure-pair allocation: each step
+allocates *two* heap objects, the closure cell and its captured
+env struct) and `bench_hof_pipeline` (poly-ADT + indirect
+dispatch). The closure-chain fixture measures wider than the 1.3×
+linear/tree target: each step pays two allocs and two decs against
+one bump-pointer bump, doubling the allocation tax on closure
+construction (current ratio recorded in JOURNAL bench entries).
+This is a representational cost of the closure-pair layout,
+not a defect in the RC implementation; a future slab/pool
+allocator for fixed-shape pair cells (Decision 9 retirement
+follow-up) would compress this ratio without changing semantics.
+
+The 1.3× retirement target therefore applies to the linear /
+tree / poly-ADT subset of the corpus. Closure-heavy workloads are
+tracked under a wider band (the closure-chain baseline records its rc/bump ratio as the `rc_over_bump` reference value with ±15% tolerance) and
+are explicitly excluded from the Boehm-retirement gate until a
+slab/pool answer ships. Decision-10's RC commitment is unchanged;
+what is scoped is the *quantitative* retirement criterion, not
+the choice of memory model.
+
+The architecture has two layers:
+
+1. **Inference.** A post-typecheck pass produces a per-node
+   uniqueness side table. Codegen uses it to elide inc/dec
+   wherever provably redundant.
+2. **LLM-author annotations.** Fn signatures carry mandatory
+   `(borrow T)` / `(own T)` mode markers. Authors mark
+   sharing-vs-consumption explicitly. The compiler verifies
+   rather than guesses.
+
+The combination plays to what LLMs are good at (writing slightly
+more annotation per definition) and avoids what compilers are
+bad at (proving sharing absent in the face of recursion +
+closures + match).
+
+## The LLM-aware sharpening
+
+A mainstream RC implementation (think Lean 4 in default mode)
+infers everything from naked AST plus a few optional hints. The
+inference is conservative; whatever it can't prove unique becomes
+shared and pays runtime inc/dec. AILang exploits its target
+audience to push that conservative ceiling higher.
+
+Five mechanisms.
+
+**(1) Mandatory `(borrow T)` / `(own T)` on fn signatures.**
+
+```
+(fn list_length
+  (type (fn-type (params (borrow (List Int))) (ret (con Int))))
+  ...)
+
+(fn sum_list_consume
+  (type (fn-type (params (own (List Int))) (ret (con Int))))
+  ...)
+```
+
+`(borrow T)` declares the parameter is read-only and lives at
+most until the call returns; the caller still owns it; the
+callee performs no inc/dec on it. `(own T)` declares ownership
+transfer; the callee consumes the value and is responsible for
+its end-of-life. The declaration is structural (visible in JSON)
+and binding (the typechecker rejects bodies that contradict it).
+
+For a Lean 4 / Roc author this is all *optional* and inferred
+when omitted. AILang makes it mandatory because the LLM author
+can carry the cognitive cost trivially, and the compiler gains a
+precise contract at every call site instead of a probabilistic
+guess.
+
+**(2) Linear-by-default consumption with explicit `(clone X)`.**
+
+In bodies, every binder is consumed by exactly one `own`-mode
+use. If the LLM writes:
+
+```
+(let p (expensive_fn x)
+  (let r1 (consume_a p)        ; consume_a takes (own); consumes p
+    (let r2 (consume_b p)      ; ERROR: p already consumed
+      ...)))
+```
+
+the compiler emits a structured non-linear-use diagnostic with
+concrete `suggested_rewrites`:
+
+- "make consume_a borrow": refactor consume_a's signature, no
+  body change at the call site;
+- "explicit clone": insert `(clone p)` at the first use;
+- "fuse traversal": replace the two separate calls with a fused fn.
+
+The LLM picks one. There is no implicit clone — sharing always
+costs visible source.
+
+**(3) Reuse hints as first-class.**
+
+```
+(fn map_inc
+  (type (fn-type (params (own (List Int))) (ret (own (List Int)))))
+  (params xs)
+  (body
+    (match xs
+      (case Nil Nil)
+      (case (Cons h t)
+        (reuse-as xs (term-ctor List Cons (app + h 1) (app map_inc t)))))))
+```
+
+`(reuse-as SRC NEW-CTOR)` asks the codegen to allocate `NEW-CTOR`
+in `SRC`'s memory slot. Compiler verifies: `SRC` is owned, this
+is its last use, sizes match. On a hit: no malloc, no free — the
+box is overwritten in place. On a miss: structured diagnostic
+explains which precondition failed; the LLM either adjusts the
+surrounding code or removes the hint.
+
+This matches Lean 4 / Roc reuse analysis but lifts it from
+"compiler-inferred when possible" to "author-asserted, compiler-
+verified". The LLM applies it everywhere it expects to fire and
+lets the compiler bounce the request when it can't.
+
+**(4) `(drop-iterative)` annotation on data declarations.**
+
+```
+(data Tree (vars a)
+  (ctor Leaf)
+  (ctor Node a (Tree a) (Tree a))
+  (drop-iterative))
+```
+
+When the refcount of a `Tree` value reaches zero, the synthesised
+dec-on-zero traversal is iterative (worklist + heap-allocated
+stack) instead of recursive. Avoids stack overflow on deep
+structures. The LLM adds the annotation where appropriate; the
+compiler refuses to emit recursive dec-cascade on annotated types.
+
+**(5) Structured compiler diagnostics with `suggested_rewrites`.**
+
+Every RC-mode error (use-after-consume, mode-mismatch,
+reuse-as-fail, drop-cascade-too-deep) emits a JSON object
+containing the failure kind, the source span, and a list of
+concrete rewrite suggestions in form-A AILang. The LLM consumes
+these without prose-parsing. This is the missing half of the
+LLM-as-author story: the language spec defines not only what
+compiles, but what the compiler tells the author when it doesn't.
+
+## Inference algorithm
+
+Post-typecheck, post-`lift_letrecs`, pre-codegen pass over the
+elaborated module. For each `Term` node that produces or binds a
+boxed value, the pass computes a uniqueness flag:
+
+- **Unique:** at this program point, the reference is the only
+  outstanding reference to its referent.
+- **Shared:** there may be multiple outstanding references.
+
+A reference is *unique* if every path from its allocation to the
+current program point passes through exactly one binding. The
+inference is a forward dataflow over the AST. The annotations
+(`borrow` / `own`) provide the inter-fn contract; the
+inference fills in intra-fn detail.

design/models/typeclasses.md

@@ -0,0 +1,156 @@
+# Typeclasses — resolution and monomorphisation whitepaper
+
+## Decision 11: typeclasses — Haskell-lite, monomorphised, coherent
+
+**The design pass for typeclasses. Codified after the Feature-acceptance
+criterion (this document, above) was committed; the criterion is
+the explicit basis for the choices below.**
+
+AILang ships typeclasses to compress a real LLM-author redundancy:
+without them, every comparable function must be written per-type
+(`int_eq`, `string_eq`, `bool_eq`, `int_show`, `string_show`, …). With
+typeclasses behind a monomorphising compiler, the LLM author writes
+one signature with a class constraint and one method per concrete
+type, and the compiler emits the same machine code as the per-type
+version. No runtime cost, no dictionary passing, no vtables.
+
+**Choice.** A deliberately narrow typeclass design — narrower than
+Haskell, narrower than Rust traits — calibrated to what an LLM
+author naturally produces. Five semantic axes are committed:
+
+1. **Scope.** Multi-method, single-parameter, optional defaults,
+   single-superclass relation. No multi-param classes, no
+   functional dependencies, no associated types.
+2. **Constraints in signatures.** Explicit and mandatory. A
+   function that calls a class method must declare the constraint
+   in its `forall` block. No constraint inference.
+3. **Resolution.** Orphan-free coherence. An `instance C T` may be
+   declared only in the module of `C` or in the module of `T`.
+   Resolution is global type-directed against a workspace-built
+   registry; coherence makes the lookup unambiguous.
+4. **Defaults.** Opt-in via an explicit `default` keyword in the
+   class body. Methods without `default` are abstract-required;
+   methods with `default` may be overridden or inherited per
+   instance.
+5. **Class-parameter kind.** Concrete types only (kind `*`). No
+   higher-kinded class params; `Functor`/`Monad`-style abstractions
+   over type constructors are not expressible. The LLM-natural
+   pattern is `List.map` / `Tree.map` as separate functions per
+   type, which monomorphisation handles directly.
+
+The five axes follow from the Feature-acceptance criterion: each
+rejected mechanism (multi-param, higher-kinded, FunDeps, assoc
+types) is one an LLM author does not unprompted produce.
+
+## Resolution and monomorphisation
+
+**Constraint collection (per function body).** During typechecking
+of a body, each method call generates a residual constraint of shape
+`<Class> <Type>` where `<Type>` may still contain type variables.
+After local typechecking, residual constraints are checked against
+the function's declared constraints (modulo α-conversion and modulo
+auto-expansion through superclasses; see below). Any residual not
+covered by declared constraints fires `MissingConstraint`.
+
+**Instance registry (workspace-global).** At workspace load (see
+`crates/ailang-core/src/workspace.rs`), all `InstanceDef` nodes
+across all reachable modules are collected into a registry keyed by
+`(class-name, canonical-hash-of-instance-type)`. Registry build
+performs three checks:
+
+- **Coherence.** Each instance's module must be either the class's
+  defining module or the instance type's defining module. Otherwise
+  → `OrphanInstance`.
+- **Uniqueness.** No two entries share a key. Otherwise →
+  `DuplicateInstance`.
+- **Method completeness.** Each instance specifies every required
+  (non-default) method of its class. Otherwise → `MissingMethod`.
+
+Registry build is a one-time-per-build pass that fires before any
+typechecking. Its errors are workspace-load errors, not per-call-site
+errors.
+
+**Resolution at call sites with concrete types.** When the typechecker
+sees a method call where every type variable in the constraint is
+substituted to a concrete type, it queries the registry. Hit →
+resolved. Miss → `NoInstance`.
+
+**Resolution at polymorphic call sites.** When type variables are
+still free, the constraint propagates into the surrounding function's
+constraint context — which the user MUST have declared explicitly
+(per axis 2). No constraint is implicitly hoisted.
+
+**Monomorphisation (post-typecheck, pre-codegen).** A pass between
+typechecking and codegen replaces every call to a
+`Type::Forall`-quantified `Def::Fn` with a call to a synthesised
+monomorphic `FnDef`. Two source-body entry points share the same
+mechanics in one fixpoint:
+
+1. **Class-method entry.** For each unique `(method, concrete-type)`
+   pair produced by a class-constraint residual, the pass looks up
+   the resolved instance body via `Registry::entries[(class,
+   type-hash)]`, substitutes the class parameter to the concrete
+   type, and synthesises a top-level `FnDef` named
+   `<method>__<type-surface-name>`.
+2. **Free-fn entry.** For each call site to a polymorphic free
+   `Def::Fn` with a fully-concrete substitution, the pass takes the
+   source body directly from the polymorphic `Def::Fn`, applies
+   rigid-var substitution on both the type AND the body (the body
+   may contain inner `Term::Lam`s whose `param_tys` reference the
+   outer Forall vars), and synthesises a top-level `FnDef` named
+   `<name>__<type-surface-name-1>__<type-surface-name-2>__…`
+   (concatenated in `Type::Forall.vars` declaration order; the
+   N-ary case extends the single-type-var class-method shape
+   bit-stably).
+
+Both arms share:
+
+- A fixpoint loop that keeps collecting targets until a round adds
+  nothing new (a synthesised free-fn body may invoke class methods
+  at concrete types, scheduling new class-method targets; a
+  class-method body may invoke polymorphic free fns at concrete
+  types, scheduling new free-fn targets).
+- A dedup cache keyed by `(kind, base-name,
+  type-hash-or-joined-hashes)` where the first component
+  (`"class"` / `"free"`) guarantees disjoint keying across the
+  two kinds.
+- A call-site rewrite walker that rewrites bare polymorphic call
+  sites — class-method-named OR poly-free-fn-named — to their
+  mono symbols before codegen runs. The walker advances a single
+  cursor over interleaved class-method and free-fn slots emitted
+  in synth's traversal order.
+
+After this pass, the IR contains no polymorphism, no class
+machinery, no polymorphic call sites — only ordinary monomorphic
+functions and direct calls. Codegen sees no difference between a
+hand-written `show_int` and a synthesised `show__Int`.
+
+**Why mono, not virtual dispatch.** Monomorphisation makes the call
+target visible to the optimiser, unlocking inlining and downstream
+loop transformations that virtual dispatch prevents in principle.
+On a saturating branch predictor with a monomorphic indirect
+target, the indirect call itself is comparable in cost to a
+non-inlined direct call — the win is in what the optimiser can do
+with the visible target, not in the call instruction. The
+end-to-end gain shrinks toward zero on larger callee bodies and
+cold call sites, but the architectural claim — "mono enables
+optimisations vdisp forbids" — holds across the spectrum
+(`bench/mono_dispatch.py` and the corresponding JOURNAL bench-notes
+entry record the measured ratios).
+
+The separator is `__` rather than `#` or `@` because `#` and `@`
+are invalid in LLVM IR global identifiers (the IR verifier rejects
+them inside `@ail_<module>_<def>` mangled names). `__` is legal in
+both LLVM IR and the C ABI used by the runtime glue, and parses
+unambiguously into `<method>__<type-surface-name>` because neither
+component contains `__` by project convention.
+
+**No runtime dispatch, no dictionary passing.** The monomorphisation
+pass is the ONLY specialiser. Codegen sees only monomorphic
+`Def::Fn`s and direct calls; the pre-iter-23.4 codegen-time
+specialiser (`lower_polymorphic_call` + `module_polymorphic_fns` +
+`mono_queue`) was removed in iter 23.4. A call that cannot be
+monomorphised — for instance, because a constraint remains
+unresolved at the entry point — is a static error, not a runtime
+one. This is the LLVM-friendly form and is consistent with
+Decision 10's performance commitment.