feat(codegen): relocate per-binder consume_count into MIR; delete codegen's second uniqueness run (mir.3a)
First of two iterations delivering spec 0060's mir.3 row (plan docs/plans/0117-mir.3a-consume-count-relocation.md). The per-binder consume_count — the only thing codegen read from its second infer_module_with_cross run — now lives on a new binder-keyed MirDef.consume: BTreeMap<String,u32>, filled once by lower_to_mir on the post-mono body. Codegen builds its existing (def,binder)->consume_count lookup from those maps and the three scope-close drop sites (own-param, let-binder, match-arm) read it; the codegen uniqueness run, its UniquenessTable field, and the import are deleted. mir.3 is split into two iterations (recorded in spec 0060): the named deletion depends ONLY on consume_count. All three drop sites read consume_count from self.uniqueness, while the modes they also gate on (param_modes for the own-param dec, scrutinee_is_owned for the match dec) come from the type, not the uniqueness pass (UniquenessInfo carries no mode). So mir.3a relocates consume_count and ships the deletion; mir.3b (next) fills MArg.mode/MTerm::Let.mode and switches emit_call's anon-temp gate onto MArg.mode. The split halves the change at the codebase's highest-risk surface (RC/drop correctness, the raw-buf leak saga) and makes each half independently verifiable against the live=0 leak pins. Design: consume_count lands on MirDef (binder-keyed), NOT on MArg. The drop sites key by (def, binder_name) — a per-binder aggregate — while the spec-sketched MArg.consume_count is per-arg-position and never reaches them; the per-def map matches the UniquenessTable's own keying and all three binder kinds (param/let/pattern) uniformly. MArg.consume_count stays a mir.1 default. Source = run check's infer_module_with_cross inside lower_to_mir post-mono (the synth_pure single-engine-re-walked pattern); retaining a check-time result is blocked (check's uniqueness is pre-mono and runs on-demand-from-codegen, never in check_workspace, so it would miss the mono specialisations). cross_module_types (= codegen's module_def_ail_types) is rebuilt in elaborate_workspace from the post-mono workspace. Safety property held: this is a PURE RELOCATION of an identical computation — infer_module_with_cross ran on the post-mono module in codegen and now runs on the same post-mono module in lower_to_mir, so drop placement is byte-identical. cross_module_types matches module_def_ail_types exactly (both insert f.name->f.ty over post-mono Def::Fn), confirmed by the leak pins staying green. Verification (orchestrator, post-implement inspect): diff matches the plan; codegen grep-clean for infer_module_with_cross + UniquenessTable (now ailang-check-internal); cargo build --workspace clean (no errors, no unused warnings — module_def_ail_types survives for emit_call's anon-temp param_modes gate); cargo test --workspace 701 passed / 0 failed / 3 ignored (+1 = the new producer pin mirdef_consume_is_populated_for_let_binder; no #[ignore] added). The live=0 drop-correctness witnesses all green: alloc_rc_loop_valued_rawbuf_binder_drops_at_scope_close (#43/#47), alloc_rc_heap_loop_binder_replaced_by_recur_does_not_leak, alloc_rc_print_int_does_not_leak_show_result_str. #49 stays #[ignore] (mir.4); #51/#53 build guards green.
This commit is contained in:
@@ -322,6 +322,23 @@ class and deletes the matching codegen re-derivation.
|
||||
> type-scoped names in the current corpus, so the acceptance
|
||||
> "type_home_module grep-clean" holds.
|
||||
|
||||
> mir.3 split (discovered in planning, `docs/plans/0117-mir.3a-consume-count-relocation.md`):
|
||||
> mir.3 ships in two iterations. **mir.3a** relocates `consume_count`
|
||||
> only — the deletion of the second `infer_module_with_cross` run
|
||||
> depends solely on it (all three codegen drop sites read `consume_count`
|
||||
> from `self.uniqueness`; the *modes* they also test come from the
|
||||
> type, not the uniqueness pass, which carries no mode). The per-binder
|
||||
> `consume_count` lands on a new `MirDef.consume: BTreeMap<String, u32>`
|
||||
> (binder-keyed, matching how the drop sites and the `UniquenessTable`
|
||||
> key it — the spec's `MArg.consume_count` field is per-arg-position
|
||||
> and does not reach the binder-keyed drop sites, so it stays a mir.1
|
||||
> default). lower_to_mir runs the single uniqueness pass on the
|
||||
> post-mono body — a pure relocation of the identical computation
|
||||
> codegen ran, so drop placement is byte-identical. **mir.3b** fills
|
||||
> `MArg.mode` / `MTerm::Let.mode` from the type modes and switches
|
||||
> `emit_call`'s anon-temp borrow-slot gate onto `MArg.mode` (additive;
|
||||
> no further re-deriver deletion).
|
||||
|
||||
mir.5 carries the ledger work as part of the milestone (per CLAUDE.md:
|
||||
contract changes ship with the iteration that needs them):
|
||||
|
||||
|
||||
Reference in New Issue
Block a user