diff --git a/bench/orchestrator-stats/2026-06-01-iter-mir.5.json b/bench/orchestrator-stats/2026-06-01-iter-mir.5.json new file mode 100644 index 0000000..7279b20 --- /dev/null +++ b/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." +} diff --git a/crates/ail/tests/codegen_import_map_fallback_pin.rs b/crates/ail/tests/codegen_import_map_fallback_pin.rs index fc01a10..fb817be 100644 --- a/crates/ail/tests/codegen_import_map_fallback_pin.rs +++ b/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__` body references -//! `.show__` even though `prelude` does not -//! import user modules. +//! Property protected: mono synthesises a `prelude.print__` +//! body that references `.show__` 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__` 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}; diff --git a/design/INDEX.md b/design/INDEX.md index d6f93d5..1ffbe9f 100644 --- a/design/INDEX.md +++ b/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 | diff --git a/design/contracts/0013-typeclasses.md b/design/contracts/0013-typeclasses.md index c44aa58..ae90eb5 100644 --- a/design/contracts/0013-typeclasses.md +++ b/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__` references `.show__`, - 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 diff --git a/design/contracts/0018-check-codegen-boundary.md b/design/contracts/0018-check-codegen-boundary.md new file mode 100644 index 0000000..6ee98b4 --- /dev/null +++ b/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). diff --git a/design/models/0003-pipeline.md b/design/models/0003-pipeline.md index 5e0c029..d09db9a 100644 --- a/design/models/0003-pipeline.md +++ b/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; diff --git a/docs/specs/0060-typed-mir.md b/docs/specs/0060-typed-mir.md index a44da1a..4398340 100644 --- a/docs/specs/0060-typed-mir.md +++ b/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):