plan(mir.4): StrRep loop-carried Str ⇒ Heap, delete the recur !is_str gate

mir.4 closes bug #49 (a heap-Str loop binder replaced across `recur`
leaks every superseded str_concat slab, live=3) structurally rather
than with a fourth leg-by-leg patch.

Design calls made in planning (folded into the spec as the mir.4
refinement note):

- Mechanism: producer-side representation, codegen reads it — the
  milestone thesis. lower_to_mir sets rep = StrRep::Heap on every
  MTerm::Str literal that flows into a Str loop-binder alloca (seed
  inits AND recur args at Str-binder positions); codegen's MTerm::Str
  arm gains a Heap leg that promotes the static literal via
  ailang_str_clone (fresh ailang_rc_alloc slab, rc_header refcount 1).
  No special-casing in the codegen Loop/Recur store arms — the clone is
  emitted automatically when the Str{Heap} node is lowered.

- Recur args are promoted too, not just seeds: `(recur "reset" …)` is
  well-typed (verified: `ail check` accepts it), and a seed-only
  promotion would leave a static literal under the now-unconditional
  dec — a constructible UB hole. Soundness over minimalism on the
  highest-risk RC/drop surface.

- Only the recur dec gate (lib.rs:2231) loses !is_str. The drop.rs
  loop-RESULT trackability gate (drop.rs:493) STAYS conservative:
  deleting it needs a broader "every Str a loop can return is
  owned-heap" guarantee (a static exit-arm literal breaks it) and is
  not required by the #49 acceptance (the #49 loop result is consumed
  by print). drop.rs is untouched.

- Boundary (out of scope, asserted ill-typed): a borrowed static-Str
  Var seeded/recur'd into a consumed Str loop binder is rejected
  upstream by uniqueness (a consumed binder position is owned), so it
  is not constructible.

Plan 0119 carries exact code per step: producer rep promotion + a
loop-frame-driven Str-binder mask for recur args (reusing the existing
ctx.loop_stack, no new ctx field), the codegen Heap leg, the gate
deletion, the #[ignore] lift on the #49 pin, a recur-literal witness
fixture + runtime pin proving the recur-arg leg, and the full-suite +
ir_snapshot verification. The existing lower_to_mir_ty Static-seed pin
flips to assert Heap.
This commit is contained in:
2026-06-01 00:34:18 +02:00
parent eba1be8d9d
commit 2536b5f535
2 changed files with 698 additions and 0 deletions
+44
View File
@@ -352,6 +352,50 @@ class and deletes the matching codegen re-derivation.
> not mir.5 — the mir.5 row's "last re-derivation residue" shrinks to
> the element-type / `Term::New` (`New.elem`) work.
> mir.4 refinement (discovered in planning + recon, `docs/plans/0119-mir.4-strrep-loop-carried-heap.md`):
> The `!is_str` deletion is scoped to the **recur superseded-value dec
> gate** (`crates/ailang-codegen/src/lib.rs:2231`, the gate the row
> names by "recur dec gate"). The *other* `!is_str` site — the
> `MTerm::Loop` arm of `is_rc_heap_allocated`
> (`crates/ailang-codegen/src/drop.rs:493`, the loop-**result**
> trackability gate) — **stays conservative** in mir.4: deleting it
> would require every `Str` a loop can *return* to be owned-heap, which
> a loop's non-`recur` exit arm (`(if … "done" (recur …))`, a static
> exit literal) does not guarantee — a strictly larger representation
> change with its own static-`Str`-dec UB hole, and not required by the
> #49 acceptance (the #49 loop result is consumed by `print`, so the
> result gate is never exercised).
>
> **Mechanism (producer-side rep, codegen reads it — the milestone
> thesis applied):** `lower_to_mir` sets `rep = StrRep::Heap` on every
> `MTerm::Str` **literal that flows into a `Str` loop-binder alloca** —
> both the binder **seed** inits (the `Term::Loop` arm) AND the
> **recur args** at `Str`-binder positions (a per-loop `Str`-binder mask
> threaded on the lowering ctx, stacked for nested loops; the #49
> program has only the seed literal, but a literal `recur` arg —
> `(recur "reset" …)` — is well-typed and would be a static value under
> the now-unconditional dec, so it must be promoted too). codegen's
> `MTerm::Str` arm (`lib.rs:1674`, today `{ lit, .. }` ignoring `rep`)
> gains a `Heap` leg: emit the interned static GEP, then
> `call ptr @ailang_str_clone(ptr <gep>)` — a fresh heap slab with an
> `rc_header` at refcount 1 (`runtime/str.c:211`). **No** special-casing
> in the codegen Loop/Recur store arms: the `str_clone` is emitted
> automatically when the `MTerm::Str{Heap}` node is lowered. This
> establishes the invariant **every value in a `Str` loop-binder alloca
> is an owned heap slab**, making the unconditional superseded-value dec
> at the recur gate sound (the prior value is always RC-tracked). The
> same-pointer guard (`lib.rs:2248`) still elides the identity-thread
> `(recur acc …)` case.
>
> **Boundary (out of scope, asserted ill-typed):** a **borrowed
> static-`Str` `Var`** seeded or recur'd into a *consumed* (dec'd) `Str`
> loop binder has no `rep` field to flip and would leave a static value
> under the unconditional dec. This is rejected upstream by uniqueness
> — a consumed loop-binder position is owned, and a borrowed `Str` `Var`
> there is a mode violation — so it is not constructible; the only owned
> `Str` values reaching such a binder are literals (promoted here) and
> already-heap expressions (`str_concat`, explicit `clone`).
mir.5 carries the ledger work as part of the milestone (per CLAUDE.md:
contract changes ship with the iteration that needs them):