From 207c63649fd7273ead1f3b33efbaa7747802f7a8 Mon Sep 17 00:00:00 2001 From: Brummel Date: Sun, 31 May 2026 12:45:52 +0200 Subject: [PATCH] =?UTF-8?q?spec:=20typed-mir=20check=E2=86=92codegen=20bou?= =?UTF-8?q?ndary=20contract?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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). --- docs/specs/0060-typed-mir.md | 318 +++++++++++++++++++++++++++++++++++ 1 file changed, 318 insertions(+) create mode 100644 docs/specs/0060-typed-mir.md diff --git a/docs/specs/0060-typed-mir.md b/docs/specs/0060-typed-mir.md new file mode 100644 index 0000000..1f02c7b --- /dev/null +++ b/docs/specs/0060-typed-mir.md @@ -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` 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 } +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, ty: Type, tail: bool }, // (2) callee pre-resolved + Let { name: String, mode: Mode, init: Box, body: Box, ty: Type }, // (3) mode + New { type_name: String, elem: Option, args: Vec, ty: Type }, // (1) elem carried + Recur{ args: Vec, 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) } // (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 } // signatures only + +// after — check_workspace yields MIR on success +pub fn elaborate_workspace(ws: &Workspace) -> Result>; +// (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; +fn synth_with_extras(&self, t: &Term, …) -> Result; // ~270 lines — DELETED +fn type_home_module(&self, …) -> Option; // ×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; +// 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.