spec: typed-mir check→codegen boundary contract

Open a new milestone introducing a typed mid-level IR (`ailang-mir`) as the single artefact crossing the check → codegen boundary, so codegen re-derives nothing. Root cause (architect drift review): the boundary today carries no typed artefact. `crates/ail/src/main.rs:2293` calls `check_workspace`, discards the result, and hands `lower_workspace` the raw `Workspace`. `CheckedModule` (ailang-check/src/lib.rs:1283) carries only top-level (Type, hash). Codegen therefore re-runs four independent derivations of what check already proved — type synthesis (`synth_with_extras`), callee resolution (`type_home_module` ×3 + `is_static_callee`), uniqueness/mode (`infer_module_with_cross`, second run), and Str representation (`!is_str` recur gate). Every raw-buf bug (#43/#46/#47/#49/#51/#53, all "check-clean, build-divergent") is a point where one of those re-derivations disagreed with check and got patched one leg at a time. Honest framing: this is removal of a re-derivation architecture, not a RED→GREEN of crashing programs. #51 and #53 build today (patched by ee4107c / 420703d) and are regression guards — they must keep building as the codegen mirrors that hold them green are deleted. #49 is the one open leg (builds, leaks live=3, test #[ignore]'d) and is the single RED→GREEN. Five iterations, each adding one MIR annotation class and deleting the matching codegen re-deriver: mir.1 structural MIR + `ty`; mir.2 `Callee::Static`; mir.3 `Mode`/`consume_count`; mir.4 `StrRep` (#49 live=0); mir.5 element-type residue + ledger (new boundary contract, retract 0013:106-120, fix 0003-pipeline model, INDEX, close #51/#53, reset milestone #7 to not-met). Forward rewrite, not revert (the prior raw-buf milestone close was wrong; the language infrastructure is healthy and survives — only the codegen re-derivation is the disease). Approach B: a separate typed MIR carrier, authoring AST unchanged. Gates: parse-every-block clean (all three .ail witnesses `ail check`-clean, exit 0); grounding-check PASS (13 load-bearing assumptions ratified against green tests / verified code facts).
2026-05-31 12:45:52 +02:00
parent 02775b58ca
commit 207c63649f
1 changed files with 318 additions and 0 deletions
@@ -0,0 +1,318 @@
+# Typed MIR — the check→codegen elaboration boundary — Design Spec
+
+**Date:** 2026-05-31
+**Status:** Approved
+**Authors:** orchestrator + Claude
+
+## Goal
+
+Introduce a typed mid-level IR (`MIR`) as the single artefact that
+crosses the `check` → `codegen` boundary, carrying every fact `check`
+proves — node types, statically-resolved callees, parameter modes /
+consume counts, and value representation (heap vs. static `Str`) — so
+that **codegen re-derives nothing**.
+
+Today there is no such artefact. `crates/ail/src/main.rs:2293` calls
+`ailang_check::check_workspace(&ws)`, discards its result, and at
+`:2348` hands `ailang_codegen::lower_workspace(&ws)` the *raw*
+`Workspace`. `CheckedModule`
+(`crates/ailang-check/src/lib.rs:1283`) carries only top-level
+`(Type, hash)` — zero interior annotation. Codegen therefore runs four
+independent re-derivations of information `check` already computed:
+
+1. **Type synthesis** at every node — `synth_with_extras`
+   (`crates/ailang-codegen/src/lib.rs:3242`, ~270 lines) + `synth_arg_type`
+   (`:3238`), a second inference engine mirroring the checker's
+   lookup ladder.
+2. **Callee resolution** — `type_home_module` (`:2809`), "mirrors the
+   checker's TypeDef-first ladder", replicated at three sites, plus
+   `is_static_callee` (`:2830`).
+3. **Uniqueness / mode** — `infer_module_with_cross` (`:1002`), the
+   *identical* pass `ailang-check::linearity` already ran; codegen
+   re-runs it to recover `consume_count` for drop placement
+   (`:2326` comment: "the typechecker has already pinned uniqueness").
+4. **Str representation** — the `!is_str` gate on the `Term::Recur`
+   superseded-value dec (`~:2131`), a conservatism codegen cannot
+   resolve because it lacks the heap/static distinction.
+
+Every member of the raw-buf bug family (#43 / #46 / #47 / #49 / #51 /
+#53 — all "check-clean, build-divergent") is a point where codegen's
+re-derivation disagreed with what `check` knew, patched one leg at a
+time. This milestone removes the re-derivation architecture itself.
+
+### Framing — these are regression guards, not RED→GREEN bugs
+
+As of 2026-05-31 (HEAD) the acute crashes are **already patched** leg
+by leg:
+
+| Program | Status at HEAD | Held green by |
+|---|---|---|
+| #51 `(new RawBuf (con Int) 3)` used via `size` only | **builds** | `ee4107c` (check-side — honours the written type-arg) |
+| #53 `(new Counter 42)` over a user ADT | **builds** | `420703d` (codegen-side mirror — "symmetric to check") |
+| #49 heap-`Str` loop binder across `recur` | **builds, leaks `live=3`** | unfixed — the one open leg, `#[ignore]`'d (`02775b5`) |
+
+So the milestone is **not** "make three crashing programs compile."
+It is "**remove the codegen re-derivation whose leg-by-leg patches
+keep these programs green today — without breaking their correctness —
+and close the one genuinely-open leg (#49) structurally instead of
+with a fourth patch.**" The check-side corrections (`ee4107c`,
+`#46`/`744ad41`) are *healthy* — they correctly populate what MIR will
+carry, and they stay. The codegen-side mirrors (`420703d`, the
+`synth_with_extras` loop-binder replay in `db710b1`, the `recur` dec
+legs) are the disease, and they are deleted as their information
+moves into MIR.
+
+The empirical acceptance evidence is therefore: **#51 and #53 keep
+building while `synth_with_extras` / the `type_home` mirrors that hold
+them green are deleted** (correctness survives removal of the
+re-derivation), plus **#49 goes `live=3` → `live=0`** (the one
+RED→GREEN).
+
+## Architecture
+
+A new leaf crate `ailang-mir` defines the IR types. It is a neutral
+bridge: `ailang-check` depends on it to *produce* MIR, `ailang-codegen`
+depends on it to *consume* MIR. The edge `codegen → check` already
+exists (`crates/ailang-codegen/Cargo.toml`), so no cycle is created;
+`ailang-mir` itself has no AILang-crate dependencies except
+`ailang-core` (for `Type`).
+
+```
+.ail.json ─ parse ─ resolve ─ desugar ─ typecheck ─┐
+                                                    │  lower_to_mir  (NEW, in ailang-check)
+                                  AST + type env ───┴──▶  MirModule  ──▶  emit LLVM IR
+                                                          (typed, mode/callee/rep-annotated)   (codegen: reads, derives nothing)
+```
+
+- The **authoring AST** (Form A, content-addressed, hashable) is
+  **unchanged**. MIR is a compiler-internal *derived* form — never
+  authored, never hashed, never round-tripped. This preserves the
+  authoring contract: an author writes no type the checker already
+  infers (the feature-acceptance redundancy bar).
+- `lower_to_mir` runs as the final phase of `check_workspace`, after
+  typecheck + lift, reusing the type environment the checker already
+  built. On success it yields a `MirWorkspace`; on type error it
+  yields the existing `Vec<Diagnostic>` and no MIR.
+- `lower_workspace*` in codegen take `&MirWorkspace` instead of
+  `&Workspace`. The `Emitter` fields and methods that re-derive
+  (`locals`' carried `Type`, `synth_with_extras`, `type_home_module`,
+  the second `infer_module_with_cross` run) are deleted; their
+  consumers read the MIR annotation directly.
+
+This also resolves a standing **model drift**:
+`design/models/0003-pipeline.md` already advertises "lower to MIR
+(SSA-like, named SSA values)" — an artefact that never existed. This
+milestone makes the model true.
+
+## Concrete code shapes
+
+### User-facing programs (the boundary's witnesses — parse-gated)
+
+These three `.ail` programs are the milestone's empirical anchor. All
+three are `ail check`-clean today (the disagreement is downstream of
+check), so they exercise exactly the boundary this milestone owns.
+
+**#51 — element type carried only by the author's annotation** (a
+`RawBuf` read only for its `size`; nothing else observes the element
+type). Regression guard: must keep building as the codegen element-type
+re-derivation is removed.
+
+```ail
+(module new_rawbuf_size_only
+  (fn main
+    (type (fn-type (params) (ret (con Unit)) (effects IO)))
+    (params)
+    (body
+      (let b (new RawBuf (con Int) 3)
+        (app print (app RawBuf.size b))))))
+```
+
+**#53 — monomorphic `(new T …)` over a user ADT**, the dotted callee
+`Counter.new` that codegen resolves today only via a hand-copied
+mirror of the checker's ladder. Regression guard: must keep building
+once the mirror is deleted and the callee arrives pre-resolved in MIR.
+
+```ail
+(module new_counter_user_adt
+  (data Counter (ctor MkCounter (con Int)))
+  (fn new (type (fn-type (params (con Int)) (ret (con Counter)))) (params n)
+    (body (term-ctor Counter MkCounter n)))
+  (fn main (type (fn-type (params) (ret (con Unit)) (effects IO))) (params)
+    (body (let c (new Counter 42) (do io/print_str "ok\n")))))
+```
+
+**#49 — heap-`Str` loop binder replaced across `recur`** (the seed is
+a static literal, each `recur` rebinds to a fresh `str_concat` heap
+slab). The one RED→GREEN: leaks `live=3` today (one slab per `recur`
+iteration superseded without a drop); must reach `live=0`.
+
+```ail
+(module loop_recur_str_binder
+  (fn main (type (fn-type (params) (ret (con Unit)) (effects IO))) (params)
+    (body
+      (let s
+        (loop (acc (con Str) "x") (i (con Int) 0)
+          (if (app ge i 3)
+              acc
+              (recur (app str_concat acc "y") (app + i 1))))
+        (app print s)))))
+```
+
+### Implementation shape (secondary — before → after)
+
+**MIR node — the bridge type** (new, `ailang-mir`). Each node carries
+the facts codegen used to re-derive:
+
+```rust
+// ailang-mir/src/lib.rs  (NEW)
+pub struct MirModule { pub name: String, pub defs: Vec<MirDef> }
+pub struct MirDef { pub name: String, pub sig: Type, pub body: MTerm }
+
+pub enum MTerm {
+    Lit  { lit: Literal, ty: Type },
+    Var  { name: String, ty: Type },
+    Call { callee: Callee, args: Vec<MArg>, ty: Type, tail: bool },  // (2) callee pre-resolved
+    Let  { name: String, mode: Mode, init: Box<MTerm>, body: Box<MTerm>, ty: Type },  // (3) mode
+    New  { type_name: String, elem: Option<Type>, args: Vec<MTerm>, ty: Type },        // (1) elem carried
+    Recur{ args: Vec<MArg>, ty: Type },
+    Str  { lit: String, rep: StrRep },   // (4) Heap | Static — set by lower_to_mir
+    // … one variant per Term node, each with `ty`
+}
+pub struct MArg  { pub term: MTerm, pub mode: Mode, pub consume_count: u32 }  // (3)
+pub enum Callee  { Static { module: String, fn_name: String }, Indirect(Box<MTerm>) }  // (2)
+pub enum StrRep  { Heap, Static }  // (4)
+pub enum Mode    { Owned, Borrow }
+```
+
+**check boundary** (`ailang-check`):
+
+```rust
+// before — crates/ailang-check/src/lib.rs:1283
+pub struct CheckedModule { pub symbols: IndexMap<String, (Type, String)> }   // signatures only
+
+// after — check_workspace yields MIR on success
+pub fn elaborate_workspace(ws: &Workspace) -> Result<MirWorkspace, Vec<Diagnostic>>;
+// (check_workspace stays for the diagnostics-only callers; elaborate_* is the build path)
+```
+
+**codegen boundary** (`ailang-codegen`):
+
+```rust
+// before — crates/ailang-codegen/src/lib.rs:278 + the Emitter re-derivers
+pub fn lower_workspace(ws: &Workspace) -> Result<String>;
+fn synth_with_extras(&self, t: &Term, …) -> Result<Type>;   // ~270 lines — DELETED
+fn type_home_module(&self, …) -> Option<String>;            // ×3 mirrors — DELETED
+let uniqueness = infer_module_with_cross(module, …);        // 2nd pass — DELETED
+
+// after — codegen consumes MIR, reads annotations
+pub fn lower_workspace(mir: &MirWorkspace) -> Result<String>;
+// e.g. a Call's target is `callee` (no is_static_callee lookup);
+//      a node's type is `mterm.ty()` (no synth);
+//      drop placement reads `MArg.consume_count` (no re-inference).
+```
+
+## Components
+
+- **`ailang-mir` (new crate):** `MirModule` / `MirDef` / `MTerm` /
+  `Callee` / `Mode` / `StrRep` / `MirWorkspace`. Leaf; depends only on
+  `ailang-core`.
+- **`ailang-check::lower_to_mir` (new module):** walks the
+  typechecked, lifted AST with the live type environment and emits
+  `MTerm`, filling `ty` on every node. Later iterations fill `callee`
+  (mir.2), `mode` / `consume_count` (mir.3), `rep` (mir.4).
+- **`ailang-codegen` (rewired):** entry points take `&MirWorkspace`;
+  the four re-derivers are removed iteration by iteration as their
+  annotation lands in MIR.
+- **CLI (`crates/ail/src/main.rs`):** the build path calls
+  `elaborate_workspace` and threads `MirWorkspace` into
+  `lower_workspace*`. `check` / `emit-ir` / diagnostics paths
+  unchanged where they only need diagnostics.
+
+## Data flow
+
+`Workspace (AST)` → `typecheck` (unchanged) → `lift` (unchanged) →
+`lower_to_mir` (type env → `MirWorkspace`) → `lower_workspace`
+(`MirWorkspace` → LLVM IR text) → `clang`. The type environment that
+`synth` builds inside check is consumed in-process by `lower_to_mir`
+rather than discarded; nothing re-walks the AST for types after MIR
+exists.
+
+## Error handling
+
+`lower_to_mir` runs only on a typechecked module, so it encounters no
+*type* errors. A failure to lower (e.g. an unresolved callee that the
+checker accepted — exactly today's check↔codegen disagreement) is an
+**internal compiler error**, surfaced as a distinct
+`MirLoweringError`, not a user diagnostic: by construction, if check
+passed, lowering must succeed. This is the structural property the
+milestone buys — the class "check-clean but codegen-divergent" becomes
+a single guarded invariant (`elaborate_workspace` returns `Ok` ⇒ MIR
+is complete ⇒ codegen cannot fall through to an `UnknownVar`).
+
+## Testing strategy
+
+- **Regression guards (green → must stay green):** the #51 and #53
+  programs above, plus the full existing workspace suite, run after
+  *each* re-deriver removal. The property: deleting the codegen
+  re-derivation does not change observable output.
+- **#49 RED→GREEN:** `crates/ail/tests/loop_recur_str_binder_no_leak_pin.rs`
+  — the `#[ignore]` is lifted in mir.4; `live=0` under `AILANG_RC_STATS`.
+- **Re-derivation-is-gone pins:** each iteration adds a guard that the
+  removed function is absent (e.g. a codegen unit test that the
+  resolved callee comes from MIR, not a ladder walk) so the
+  re-derivation cannot silently return.
+- **`elaborate ⇒ codegen-total` invariant:** a test that a curated set
+  of check-clean programs all lower to MIR and emit IR — the
+  structural replacement for the bug family.
+
+## Iteration decomposition
+
+Strategy: MIR is structurally complete over all 27 node kinds from
+mir.1 (codegen consumes it fully — no AST/MIR dual path). Each
+iteration adds **one** annotation class and deletes the matching
+codegen re-derivation.
+
+| Iter | Adds to MIR | Deletes from codegen | Acceptance |
+|---|---|---|---|
+| **mir.1** | structural MIR + `ty` on every node | `synth_with_extras` + `synth_arg_type` | whole suite green (regression); `synth_with_extras` gone |
+| **mir.2** | `Callee::Static` pre-resolved | `type_home_module` ×3 + `is_static_callee`; **lockstep pair `lower_app ↔ is_static_callee` struck from CLAUDE.md** | #53 guard green via MIR |
+| **mir.3** | `Mode` + `consume_count` | second `infer_module_with_cross` run (`:1002`) | #43/#47 guards green; drop placement reads MIR |
+| **mir.4** | `StrRep` (loop-carried `Str` ⇒ `Heap` via `str_clone` at loop entry) | the `!is_str` `recur` dec gate | #49 `live=0`; `#[ignore]` lifted |
+| **mir.5** | element-type / `Term::New` fully on MIR + **ledger** | last re-derivation residue | #51 guard green via MIR; ledger consistent |
+
+mir.5 carries the ledger work as part of the milestone (per CLAUDE.md:
+contract changes ship with the iteration that needs them):
+
+- **New contract** `design/contracts/NNNN-check-codegen-boundary.md`:
+  the invariant "codegen re-derives nothing; MIR is total over what
+  check proved; `elaborate_workspace` ⇒ codegen cannot fall through."
+- **Revise** `design/contracts/0013-typeclasses.md:106-120`: the
+  passage that *blesses* codegen-side cross-module re-resolution as
+  correct-by-design is retracted — resolution now lives in MIR.
+- **Correct** `design/models/0003-pipeline.md`: the "lower to MIR"
+  line becomes true (point at the real stage).
+- **INDEX** `design/INDEX.md`: add the boundary contract row; the
+  `qualified-xref` / codegen rows re-point at MIR consumption.
+- **Issue hygiene:** close #51 / #53 (now structurally held, not
+  patch-held); milestone #7 (raw-buf) is reset to **not met** and
+  subsumed — #49/#51/#53 become MIR-iteration acceptance, not a
+  separate patch track.
+
+## Acceptance criteria
+
+1. `ailang-codegen` contains **no** type synthesis, no callee-ladder
+   walk, and no uniqueness inference: `synth_with_extras`,
+   `synth_arg_type`, `type_home_module`, and the
+   `infer_module_with_cross` call are removed; grep-clean.
+2. The build path is `Workspace → elaborate_workspace → MirWorkspace →
+   lower_workspace`; codegen's public entry points take
+   `&MirWorkspace`.
+3. The #51 and #53 programs build and run unchanged across every
+   iteration (correctness survives re-deriver removal).
+4. The #49 program reaches `live=0`; its test's `#[ignore]` is lifted.
+5. The `lower_app ↔ is_static_callee` lockstep pair is gone from
+   CLAUDE.md (structurally unnecessary), and 0013's blessed
+   re-resolution passage is retracted.
+6. `design/models/0003-pipeline.md`'s MIR line names the real stage;
+   the new boundary contract is in INDEX.
+7. The full workspace test suite is green at each iteration close.