Brummel
bd62f2b9d0
Audit follow-up (typed-MIR milestone-close drift review, clean). The boundary contract said codegen does "no callee resolution"; that is true for App callees — the only thing `Callee` totality claims over — but `resolve_top_level_fn` still resolves a dotted fn used as a *value* via `import_map` (the in-corpus-unreachable type-home residue the spec blessed at mir.2), and ctor/const resolution stay codegen-side. Tighten the prose to "no App-callee resolution" and name the value-position carve-out, so the contract is precise and a future drift review does not read the blanket claim as violated. Prose-only; no code, no test change.
80 lines
3.8 KiB
Markdown
80 lines
3.8 KiB
Markdown
# 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).
|