# 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 App-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).

The totality claim is over **`App` callees**: every `App` carries a
resolved `Callee`, so codegen never walks a callee ladder to find a call
target. One value-position residue remains and is deliberately not MIR's
job — `resolve_top_level_fn` resolves a dotted fn used as a *value* (not
an `App` callee) through the module's `import_map`. That path is
unreachable for type-scoped names in the current corpus (the type-home
residue blessed in `docs/specs/0060-typed-mir.md`, mir.2 refinement);
ctor and const resolution likewise stay codegen-side. None of these is
callee resolution, so `Callee` totality is intact.

### 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).