docs(design): ratify the check→codegen boundary (mir.5, typed-MIR close)

mir.5 is the typed-MIR milestone's closing iteration. Its CODE half had
already converged before the iteration began, so mir.5 ships no code —
it ratifies into the design/ ledger the boundary the code already holds.

Verified at iteration entry (empirically, not from the spec sketch):
  - all four named re-derivers grep-clean in codegen: synth_with_extras,
    synth_arg_type, type_home_module, the second infer_module_with_cross;
  - lower_workspace takes &MirWorkspace (codegen consumes MIR);
  - MTerm::New is unreachable!() — raw-buf.4 desugars Term::New to
    (app T.new …) before codegen, so there is no element-type
    re-derivation left to relocate;
  - #51 / #53 (the element-type / new-T codegen crashes) are closed;
    their residue was fixed by ee4107c / 420f75f plus the New-desugar,
    not by a separate raw-buf patch track.

Ledger work (the mir.5 deliverable):
  - NEW design/contracts/0018-check-codegen-boundary.md: the invariant
    "codegen re-derives nothing; MIR is total over what check proved;
    a codegen arm that recomputes a fact instead of reading MIR is
    drift." Ratifier: lower_to_mir_ty.rs::callee_classification_builtin_and_static.
  - 0013-typeclasses invariant 2 retracted: codegen no longer re-resolves
    cross-module names via an import_map fallback; lower_to_mir::classify_callee
    resolves the reference once into Callee::Static and codegen consumes it.
  - 0003-pipeline.md: the "lower to MIR" line names the real stage
    (elaborate_workspace → MirWorkspace → lower_workspace) and a new
    paragraph states the boundary, cross-referencing 0018.
  - INDEX.md: boundary contract row added; qualified-xref re-pointed at
    lower_to_mir + 0018.
  - codegen_import_map_fallback_pin.rs doc-comment made honest — it pins
    the post-mono AST precondition classify_callee relies on, not a
    codegen-side resolution that no longer exists. Assertions unchanged;
    the test stays green.
  - spec 0060 gains a mir.5 refinement note recording the early code
    convergence.

Acceptance criteria 1-7 of docs/specs/0060-typed-mir.md are all met.
Full workspace suite green (exit 0, 0 failed, 2 ignored); 708 passed
carried from mir.4 (no test added or removed).

Not done here (deliberately): the milestone #7 (raw-buf) subsumption
note is an external Gitea tracker write; the /boss auto-mode classifier
declined it as an unauthorised external write and it is surfaced to the
user rather than worked around. The end-to-end milestone fieldtest
remains the deliberate manual close-gate before the tracker milestone
is marked done.

refs #51 #53

bench/orchestrator-stats/2026-06-01-iter-mir.5.json

@@ -0,0 +1,13 @@
+{
+  "iter_id": "mir.5",
+  "date": "2026-06-01",
+  "mode": "ledger-only",
+  "outcome": "DONE",
+  "tasks_total": 5,
+  "tasks_completed": 5,
+  "reloops_per_task": { "1": 0, "2": 0, "3": 0, "4": 0, "5": 0 },
+  "review_loops_spec": 0,
+  "review_loops_quality": 0,
+  "blocked_reason": null,
+  "notes": "mir.5 is the typed-MIR milestone's closing iteration. At iteration entry the orchestrator verified the CODE half was already complete: all four named re-derivers (synth_with_extras, synth_arg_type, type_home_module, codegen's infer_module_with_cross) are grep-clean; lower_workspace takes &MirWorkspace; MTerm::New is unreachable!() (raw-buf.4 desugars Term::New to (app T.new …) before codegen); #51/#53 are closed (element-type residue converged via the #51/#53 fixes ee4107c/420f75f + the raw-buf.4 New-desugar). So mir.5 shipped NO code — it is ledger-only ratification of the boundary the code already holds. Authored design/contracts/0018-check-codegen-boundary.md (invariant: codegen re-derives nothing; MIR is total over what check proved; ratifier crates/ailang-check/tests/lower_to_mir_ty.rs::callee_classification_builtin_and_static). Retracted 0013-typeclasses invariant 2 (codegen no longer re-resolves cross-module names; lower_to_mir::classify_callee resolves once into Callee::Static). Corrected design/models/0003-pipeline.md MIR line to name the real stage + a boundary paragraph. Updated design/INDEX.md: added the boundary row, re-pointed qualified-xref at lower_to_mir + 0018. Made the codegen_import_map_fallback_pin.rs doc-comment honest (it now pins the post-mono AST precondition classify_callee relies on, not a codegen-side resolution that no longer exists; assertions unchanged, stays green). Added a mir.5 refinement note to spec 0060 recording the early code convergence. Full workspace suite green (exit 0, 0 failed, 2 ignored); 708 passed carried from mir.4 (no test added/removed; the single .rs edit is a doc-comment). RESIDUAL (deferred to user): the milestone #7 (raw-buf) subsumption note is an external Gitea write the /boss auto-mode classifier correctly declined to make autonomously — surfaced to the user with the exact note text. #51/#53 already closed; #49 closes on push of c5fd16a. Acceptance criteria 1-7 of spec 0060 all met. Milestone code+ledger complete; the end-to-end milestone fieldtest is the remaining deliberate manual close-gate."
+}

crates/ail/tests/codegen_import_map_fallback_pin.rs

@@ -1,21 +1,24 @@
-//! Pin for the iter-24.3 codegen `import_map`-fallback path
+//! Pin for the post-mono cross-module reference precondition
 //! (design/contracts/0013-typeclasses.md, "Cross-module references in
-//! synthesised bodies" invariant 2).
+//! synthesised bodies" invariant 2; resolved per the
+//! design/contracts/0018-check-codegen-boundary.md boundary).
 //!
-//! Property protected: post-mono synthesised body cross-module
-//! references resolve at codegen via the fallback to
-//! `module_user_fns` when the prefix is
-//! NOT in the current module's `import_map`. Specifically, the
-//! synthesised `prelude.print__<UserType>` body references
-//! `<user_module>.show__<UserType>` even though `prelude` does not
-//! import user modules.
+//! Property protected: mono synthesises a `prelude.print__<UserType>`
+//! body that references `<user_module>.show__<UserType>` even though
+//! `prelude` does not import user modules — the cross-module reference
+//! exists in the post-mono AST and is import_map-independent. This is
+//! the precondition `lower_to_mir::classify_callee` relies on when it
+//! resolves the reference once into `Callee::Static`; codegen then
+//! consumes that identity and re-derives nothing (the typed-MIR
+//! boundary). The pin asserts the AST-level precondition directly, so
+//! it stays green and cheap to bisect.
 //!
-//! Failure mode this pin catches: a future codegen refactor
-//! tightens `resolve_top_level_fn` or `lower_app`'s cross-module
-//! arm or `synth_with_extras`'s Var arm back to `import_map`-only.
-//! Without this pin, the regression surfaces only at the
-//! `show_user_adt` E2E (which builds + runs a binary, slow to
-//! bisect).
+//! Failure mode this pin catches: a future mono refactor stops
+//! emitting the cross-module `show_user_adt.show__<UserType>` Var (or
+//! routes it through `prelude`'s import_map), which would break the
+//! resolution `classify_callee` performs downstream. Without this pin,
+//! the regression surfaces only at the `show_user_adt` E2E (which
+//! builds + runs a binary, slow to bisect).
 
 use ailang_check::{check_workspace, monomorphise_workspace};
 use ailang_core::ast::{Def, Term};

design/INDEX.md

@@ -87,7 +87,7 @@ is the default.
 | data-model           | LLM author / stable           | crates/ailang-core/tests/design_schema_drift.rs | design/contracts/0002-data-model.md |
 | mangling             | codegen / stable              | crates/ail/tests/eq_ord_e2e.rs            | crates/ailang-codegen/src/lib.rs //! |
 | env-construction     | codegen / stable              | crates/ailang-check/tests/duplicate_ctor_pin.rs | crates/ailang-codegen/src/lib.rs //! |
-| qualified-xref       | codegen / stable              | crates/ail/tests/codegen_import_map_fallback_pin.rs | crates/ail/src/main.rs //! |
+| qualified-xref       | check→codegen / stable        | crates/ail/tests/codegen_import_map_fallback_pin.rs | crates/ailang-check/src/lower_to_mir.rs (classify_callee) + design/contracts/0018-check-codegen-boundary.md |
 | frozen-value-layout  | embedding ABI / one-way-frozen| crates/ailang-codegen/tests/embed_record_layout_pin.rs | design/contracts/0006-frozen-value-layout.md + runtime/rc.c §layout |
 | float-semantics      | LLM author / stable           | crates/ail/tests/eq_float_noinstance.rs   | design/contracts/0005-float-semantics.md |
 | typeclasses          | LLM author / stable           | crates/ail/tests/show_no_instance_e2e.rs  | design/contracts/0013-typeclasses.md |
@@ -99,6 +99,7 @@ is the default.
 | embedding-abi        | embedding host / stable       | crates/ailang-codegen/tests/embed_record_layout_pin.rs | design/contracts/0003-embedding-abi.md |
 | scope-boundaries     | architect+author / stable     | crates/ailang-core/tests/effect_doc_honesty_pin.rs | design/contracts/0010-scope-boundaries.md |
 | verification         | architect / stable            | bench/architect_sweeps.sh                 | design/contracts/0014-verification.md |
+| check-codegen-boundary| architect / stable           | crates/ailang-check/tests/lower_to_mir_ty.rs (callee_classification_builtin_and_static) | design/contracts/0018-check-codegen-boundary.md |
 
 ## Models
 | id | consumer / lifetime | link |

design/contracts/0013-typeclasses.md

@@ -103,21 +103,26 @@ Three invariants make this work:
    bare `Var "show"` post-mono that codegen later rejects with
    `unknown variable`.
 
-2. **Post-mono synthesised body cross-module references may bypass
-   the source template's `import_map`.** `prelude` does not import
-   user modules (the auto-injection runs one-way: user workspaces
-   import prelude, never the inverse). But a synthesised body for
+2. **Post-mono synthesised body cross-module references are resolved
+   once, in `lower_to_mir`.** `prelude` does not import user modules
+   (the auto-injection runs one-way: user workspaces import prelude,
+   never the inverse). But a synthesised body for
    `prelude.print__<UserType>` references `<user_module>.show__<UserType>`,
-   created by mono — not by the prelude source. Codegen's
-   cross-module name-resolution must accept this: at
-   `crates/ailang-codegen/src/lib.rs::resolve_top_level_fn` (Var-
-   resolution), `::lower_app`'s cross-module call arm, and
-   `::synth_with_extras`'s Var arm, the resolution first tries the
-   current module's `import_map`, then falls back to a direct
-   `module_user_fns` / `module_def_ail_types` lookup against the
-   prefix. Both ends were independently typechecked under their own
-   module contexts before mono ran; the cross-module reference is a
-   post-mono construct, not a source-language one.
+   created by mono — not by the prelude source — so the call crosses a
+   module boundary the source template did not. This reference is
+   resolved at lowering time:
+   `crates/ailang-check/src/lower_to_mir.rs::classify_callee` resolves
+   the callee against the workspace and emits
+   `Callee::Static { module, fn_name, .. }` carrying the resolved owner.
+   Codegen consumes that identity off the MIR `App` node and does
+   **not** re-resolve it — the former codegen-side
+   `import_map`-then-`module_user_fns` fallback (at `resolve_top_level_fn`,
+   `lower_app`'s cross-module arm, and the now-deleted
+   `synth_with_extras`) is retracted, per the
+   [check→codegen boundary](0018-check-codegen-boundary.md). Both ends
+   were independently typechecked under their own module contexts before
+   mono ran; the cross-module reference is a post-mono construct, not a
+   source-language one.
 
 3. **FreeFnCall synth pushes one residual per declared forall-
    constraint.** At `crates/ailang-check/src/lib.rs`'s synth Var arm

design/contracts/0018-check-codegen-boundary.md

@@ -0,0 +1,69 @@
+# Check→codegen boundary
+
+## Check→codegen boundary
+
+`check` produces a single elaborated, typed artefact — a
+[`MirWorkspace`](../../crates/ailang-mir/src/lib.rs) — that is **total**
+over every fact codegen needs. Codegen consumes that artefact and
+**re-derives nothing**: it performs no type synthesis, no callee
+resolution, no uniqueness inference. Every decision codegen makes reads
+a field MIR already carries; there is no recompute-or-guess fallback
+path.
+
+The producer is
+[`ailang-check::lower_to_mir`](../../crates/ailang-check/src/lower_to_mir.rs),
+driven by `elaborate_workspace`; the consumer is
+[`ailang-codegen::lower_workspace`](../../crates/ailang-codegen/src/lib.rs),
+whose public entry points take `&MirWorkspace`. The build path is
+
+```
+Workspace → elaborate_workspace → MirWorkspace → lower_workspace → LLVM IR
+```
+
+`lower_to_mir` re-enters check's own canonical synth on the post-mono
+AST, so the MIR each node carries is the *same* judgement check proved,
+not a parallel re-derivation. This is the source of the totality
+guarantee: a fact in MIR is a fact check ratified.
+
+### What MIR carries (the totality)
+
+MIR is structurally complete over all 17 `Term` variants
+([`ailang-core/src/ast.rs`](../../crates/ailang-core/src/ast.rs)), and
+each node carries the annotation classes codegen formerly re-derived:
+
+- **`ty`** on every node — the synthesised type. Codegen reads layout,
+  drop shape, and mangling off it.
+- **`Callee`** on every `App` — `Static { module, fn_name, sig }` /
+  `Builtin { name, sig }` / `Indirect`. The static target is resolved
+  in `lower_to_mir`; codegen reads the identity, it does not walk a
+  callee ladder.
+- **`Mode` + `consume`** — per-arg modes on `MArg` and the per-binder
+  `consume_count` on `MirDef.consume`. Drop placement reads these; the
+  modes/linearity contract is [memory-model](0008-memory-model.md).
+- **`StrRep`** on every `Str` literal — `Static` (constexpr GEP into
+  rodata) / `Heap` (promoted via `str_clone`). The producer decides the
+  representation; codegen emits what the rep says (see
+  [str-abi](0011-str-abi.md)).
+
+### What codegen no longer holds
+
+The re-derivers that made codegen a second, weaker type pass are gone
+and stay grep-clean: `synth_with_extras`, `synth_arg_type`,
+`type_home_module`, and codegen's own `infer_module_with_cross` run.
+Cross-module name resolution in particular is resolved **once**, in
+`lower_to_mir`, into `Callee::Static` — codegen does not re-resolve it
+(the retraction recorded in [typeclasses](0013-typeclasses.md), §
+"Cross-module references in synthesised bodies", invariant 2).
+
+### Failure mode this contract names
+
+A codegen arm that recomputes a fact instead of reading it off MIR is
+**drift**, even when it computes the right answer — it reintroduces the
+weaker parallel pass this boundary exists to delete, and the next
+post-mono inconsistency it silently tolerates is a latent miscompile.
+The architect agent walks codegen for type synthesis, callee-ladder
+walks, and uniqueness inference during drift review; any reappearance
+is a regression against this contract, not a local style choice.
+
+The pipeline view of where this stage sits is
+[pipeline](../models/0003-pipeline.md).

design/models/0003-pipeline.md

@@ -9,13 +9,22 @@
             ├─ desugar (AST → AST)
             ├─ typecheck (HM, effect rows; mode-strict per the memory model)
             ├─ lift_letrecs (post-typecheck AST → AST)
-            ├─ lower to MIR (SSA-like, named SSA values)
-            ├─ emit LLVM IR (.ll)
+            ├─ lower to MIR (elaborate_workspace → MirWorkspace; ailang-check::lower_to_mir)
+            ├─ emit LLVM IR (.ll)  (ailang-codegen::lower_workspace consumes &MirWorkspace)
             └─ clang -O2 *.ll -o binary
                   --alloc=rc   → emits inc/dec    (@ailang_rc_inc / _dec; canonical, default)
                   --alloc=bump → links bump-floor (@bump_malloc; raw-alloc bench-floor)
 ```
 
+MIR ([`ailang-mir`](../../crates/ailang-mir/src/lib.rs)) is the single
+typed artefact crossing the check→codegen boundary: `lower_to_mir`
+re-enters check's canonical synth on the post-mono AST and attaches
+every fact codegen needs (node `ty`, resolved `Callee`, `Mode` +
+`consume`, `StrRep`), so codegen consumes `&MirWorkspace` and
+re-derives nothing — no type synthesis, no callee-ladder walk, no
+uniqueness inference. The invariant and its failure mode are
+[check→codegen boundary](../contracts/0018-check-codegen-boundary.md).
+
 Two allocator backends share the same MIR. `--alloc=rc` is the
 canonical backend committed to in the
 [memory model](../contracts/0008-memory-model.md) and the CLI default;

docs/specs/0060-typed-mir.md

@@ -407,6 +407,21 @@ class and deletes the matching codegen re-derivation.
 > `Str` values reaching such a binder are literals (promoted here) and
 > already-heap expressions (`str_concat`, explicit `clone`).
 
+> mir.5 refinement (discovered at iteration entry, 2026-06-01): the
+> **code** half of mir.5 — "element-type / `Term::New` fully on MIR" —
+> had already converged before mir.5 began. The `New.elem` element-type
+> residue was closed by the #51/#53 bug fixes (`ee4107c` honours the
+> written element type-arg in check; `420f75f` resolves the dotted
+> `T.new` user-ADT callee) together with the raw-buf.4 `New`
+> desugar, which rewrites `Term::New` into `(app T.new …)` *before*
+> codegen — so `MTerm::New` is `unreachable!()` at codegen and there is
+> no element-type re-derivation left to relocate. At mir.5 entry all
+> four named re-derivers are grep-clean, `lower_workspace` takes
+> `&MirWorkspace`, and #51/#53 are closed. **mir.5 is therefore
+> ledger-only:** it ratifies into the `design/` ledger the boundary the
+> code already holds. No new code ships; the acceptance criteria below
+> are met by the landed mir.1–4 work plus the #51/#53 fixes.
+
 mir.5 carries the ledger work as part of the milestone (per CLAUDE.md:
 contract changes ship with the iteration that needs them):