spec: unique binder names per fn — A2b leg of RawBuf drop-leak (refs #43)

The last open leg of the #43 owned-heap drop-leak cluster is the
UniquenessTable shadow-name collapse: the side-table keys by
(def_name, binder_name), so a fn that shadows a binder name collapses
every shadow onto one key. The outermost binding (records last, on pop)
overwrites the inner ones; codegen's scope-close drop gates then read
the collapsed consume_count for the innermost binding and suppress its
drop, leaking the owned slab.

Spec 0056 resolves this as a compiler-internal naming collision — NOT
the deeper, separate problem of persistent AST provenance back to the
authored form (certain to be needed eventually, deliberately deferred;
conflating the two is a category error). Fix: alpha-rename shadowing
binders during desugar (reusing the existing fresh-name machinery that
already mints $mp_N / $lr_N), making the (def, name) key injective
again. No consumer of the uniqueness table changes — they all key by
name, and the name becomes a per-fn injective identity. IR-neutral:
codegen names heap by fresh SSA, never by source binder name. The
pre-desugar hashed form is untouched, so module identity and hash-pin
tests are unaffected.

RED fixtures securing the binder-kind class (the user's gating
condition before proceeding to the uniform-across-kinds fix):
- Let-shadow: the three raw_buf_{int,float,bool}_shadow_rebind tests
  (already in tree, committed f7f4c3b) — assert live == 0.
- Flat-pattern-shadow: a differential test plus its two fixtures
  (flat_pat_shadow_leak.ail shadows the outer binder; _control.ail
  alpha-renames it to a distinct name). The shadow must reach the
  control's live count. Differential by design, to isolate the
  shadow-collapse drop from unrelated baseline drop gaps out of
  #43's scope.

Grounding-check PASS; ail-check parse-gate green on every fenced block.

crates/ail/tests/e2e.rs

@@ -2330,6 +2330,42 @@ fn raw_buf_bool_shadow_rebind_drop_balances_rc_stats() {
     );
 }
 
+/// A2b completeness (refs #43): the pattern-binder sibling of the
+/// Let-shadow leak. A flat-match pattern-binder that shadows an outer
+/// same-named heap binder must not leak more than its alpha-renamed
+/// equivalent. The uniqueness side-table keys by `(def, binder_name)`
+/// (`crates/ailang-check/src/uniqueness.rs`); the shadowing pattern
+/// binder `x` collides with the outer `let x`, and the arm-close drop
+/// gate (`crates/ailang-codegen/src/match_lower.rs:795`) reads the
+/// collapsed (outer) `consume_count` and suppresses the inner
+/// payload's drop. `flat_pat_shadow_leak.ail` (inner binder `x`,
+/// shadows) and `flat_pat_shadow_control.ail` (inner binder `y`,
+/// alpha-renamed) are byte-identical apart from that one name; the
+/// shadow must reach the control's live count. RED until binder names
+/// are made unique per fn at desugar (the same fix that closes the
+/// three `raw_buf_*_shadow_rebind` Let-shadow tests). Differential
+/// rather than `live == 0` on purpose: it isolates the shadow-collapse
+/// drop from unrelated baseline drop gaps (Box outer cell,
+/// implicit-consume of the outer binder) that are out of #43's scope.
+#[test]
+fn flat_pat_shadow_binder_does_not_leak_more_than_alpha_renamed() {
+    let (s_out, s_allocs, s_frees, s_live) =
+        build_and_run_with_rc_stats("flat_pat_shadow_leak.ail");
+    let (c_out, _c_allocs, _c_frees, c_live) =
+        build_and_run_with_rc_stats("flat_pat_shadow_control.ail");
+    assert_eq!(
+        s_out.trim(),
+        c_out.trim(),
+        "shadow and alpha-renamed control must print identically"
+    );
+    assert_eq!(
+        s_live, c_live,
+        "flat-pattern shadow leaks live={s_live} (allocs={s_allocs} frees={s_frees}) \
+         vs alpha-renamed control live={c_live}; the shadowing pattern-binder's \
+         arm-close drop is suppressed by the (def,name) uniqueness-table collision"
+    );
+}
+
 /// raw-buf.4 Float variant: a 2-slot Float RawBuf (1.5 + 2.5),
 /// exercising the `double` load/store emits. Prints `4.0` (the `%g`
 /// whole-double `.0` fallback).

docs/specs/0056-unique-binder-names.md

@@ -0,0 +1,263 @@
+# Unique Binder Names per Fn — Design Spec
+
+**Date:** 2026-05-30
+**Status:** Draft — awaiting user spec review
+**Authors:** orchestrator + Claude
+
+## Goal
+
+Close the last open leg of the owned-heap drop-leak cluster #43: the
+`UniquenessTable` shadow-name collapse. The uniqueness side-table is
+keyed by `(def_name, binder_name)`
+(`crates/ailang-check/src/uniqueness.rs:99`). When a fn shadows a
+binder name — `(let buf (new …) (let buf (set buf …) … (get buf)))` —
+every shadow records under the same key; the last `record_binder` to
+fire (the **outermost** binding, which pops last) overwrites the
+inner ones. Codegen's scope-close drop gates then read the collapsed
+`consume_count` for the *innermost* binding, misjudge whether it is
+still owned, and suppress its drop. The owned heap slab leaks.
+
+The fix gives every binder a name that is unique within its fn, so the
+`(def, name)` key is injective again. This is done by alpha-renaming
+shadowing binders during desugaring — the existing lowering pass that
+already mints fresh unique names for its own synthetic binders
+(`$mp_N`, `$lr_N`). No consumer of the uniqueness table changes: they
+all key by name, and the name is now an injective per-fn identity.
+
+### Scope: what this is and is not
+
+This resolves a **compiler-internal naming collision**. It is *not*
+the deeper, separate problem of giving AST nodes a persistent identity
+with provenance back to the pre-desugar (authored) form — that
+back-reference is certain to be needed eventually but is **not** a
+requirement here, and conflating the two is a category error. The
+authored `.ail` (the canonical, content-addressed, hashed form) is
+untouched: renaming happens only on the post-desugar internal tree,
+which is already a lowered form whose binder names desugar already
+treats as tags.
+
+## Architecture
+
+The post-desugar AST is an internal lowering, not the authored
+artifact. Desugar already (a) threads a lexical `scope` through every
+term (`desugar_term(t, scope)`), and (b) owns a collision-free
+fresh-name generator (`Desugarer::fresh`, used for `$mp_N` match
+temporaries and `$lr_N` lifted letrecs). The fix extends (a) to detect
+a binder whose name is already bound in the enclosing `scope` and, on
+such a shadow, allocate a fresh unique name for it, recording the
+original→fresh mapping in the scope handed to that binder's body. The
+one structural addition is that `Term::Var` — today a verbatim
+`t.clone()` — must rewrite its name through the active rename map so
+references resolve to the renamed binder.
+
+The rename is **on shadow only** and **uniform across binder kinds**.
+Non-shadowing binders keep their authored name, so every existing
+fixture's desugared output is byte-identical; only an actual shadow is
+renamed. The scope check is identical at every binder-introduction
+site, so a single mechanism covers `Term::Let`, flat-`Match`
+pattern-binders, `Term::Lam` params, and `Term::Loop` binders. Of
+those, only `Term::Let` and flat-`Match` pattern-binders currently
+reach a uniqueness-gated drop site (see Components); covering the
+others is free under the same scope check and forecloses the collision
+class for any future gate.
+
+Emitted LLVM IR is unaffected: codegen names heap values by fresh SSA
+(`%vN`), never by the source binder name (the binder name is only an
+internal lookup key into `self.locals` / `moved_slots` / the
+uniqueness table). Renaming an internal binder therefore changes no IR
+bytes — only which uniqueness entry the lookup resolves to, which is
+the entire point.
+
+## Concrete code shapes
+
+### North-star — the LLM-natural programs that must stop leaking
+
+These are shipped (or completeness-securing) fixtures. They are the
+empirical evidence: an LLM author *did* write the shadow-rebind idiom
+(it is the milestone fixture), and the fix makes it correct.
+
+**Let-shadow (the shipped #43/#42 symptom, `examples/raw_buf_int.ail`):**
+
+```ail
+(module raw_buf_int
+  (fn main
+    (type (fn-type (params) (ret (con Unit)) (effects IO)))
+    (params)
+    (body
+      (app print
+        (let buf (new RawBuf (con Int) 3)
+          (let buf (app RawBuf.set buf 0 10)
+            (let buf (app RawBuf.set buf 1 20)
+              (let buf (app RawBuf.set buf 2 30)
+                (app + (app RawBuf.get buf 0)
+                  (app + (app RawBuf.get buf 1)
+                    (app RawBuf.get buf 2)))))))))))
+```
+
+Prints `60`; under `AILANG_RC_STATS` must reach `live == 0` (today
+`live == 1`).
+
+**Flat-pattern-shadow (completeness, `examples/flat_pat_shadow_leak.ail`):**
+a flat-match pattern-binder `x` shadowing an outer `let x`; the inner
+`x` (a heap `Box` payload) is borrow-only and must drop at arm close,
+but the collision suppresses it. Paired with
+`examples/flat_pat_shadow_control.ail` (inner binder alpha-renamed to
+`y`); the shadow must reach the control's live count.
+
+### How desugar rewrites the north-star (worked, Let case)
+
+Input is the four-`buf` body above. Output binds each shadow to a
+fresh name and rewrites references in its body; values are desugared
+in the *outer* scope (before the binder is installed), so each
+`RawBuf.set` still refers to the previous binding:
+
+```text
+(let buf   (new RawBuf (con Int) 3)
+  (let buf$1 (app RawBuf.set buf   0 10)
+    (let buf$2 (app RawBuf.set buf$1 1 20)
+      (let buf$3 (app RawBuf.set buf$2 2 30)
+        (app + (app RawBuf.get buf$3 0)
+          (app + (app RawBuf.get buf$3 1)
+            (app RawBuf.get buf$3 2)))))))
+```
+
+Keys become `(main,buf)`, `(main,buf$1)`, `(main,buf$2)`,
+`(main,buf$3)` — all distinct. The three outer bindings are each
+consumed once by the next `set`'s `own` param (`consume_count == 1`,
+correctly not dropped: `set` is in-place, same slab); the innermost
+`buf$3` is only borrowed by the three `get`s (`consume_count == 0`)
+and is dropped once at scope close. Exactly one drop fires, balancing
+the one slab alloc → `live == 0`.
+
+### Implementation shape (secondary)
+
+**`Term::Var` — rewrite through the active rename map.** Before:
+
+```rust
+Term::Lit { .. } | Term::Var { .. } => t.clone(),
+```
+
+After (Var split out; rename map carried alongside `scope`):
+
+```rust
+Term::Lit { .. } => t.clone(),
+Term::Var { name } => Term::Var {
+    name: scope.resolved_name(name),   // renamed binding, or `name` verbatim
+},
+```
+
+**Each binder-introduction site — rename on shadow.** Before
+(`Term::Let`):
+
+```rust
+Term::Let { name, value, body } => {
+    let v = self.desugar_term(value, scope);
+    let mut inner = scope.clone();
+    inner.insert(name.clone(), ScopeEntry::LetBound);
+    let b = self.desugar_term(body, &inner);
+    Term::Let { name: name.clone(), value: Box::new(v), body: Box::new(b) }
+}
+```
+
+After:
+
+```rust
+Term::Let { name, value, body } => {
+    let v = self.desugar_term(value, scope);          // outer scope: refs to prior binding
+    let mut inner = scope.clone();
+    let bound = inner.bind_renaming_on_shadow(name, &mut self.fresh_binder);
+    let b = self.desugar_term(body, &inner);
+    Term::Let { name: bound, value: Box::new(v), body: Box::new(b) }
+}
+```
+
+`bind_renaming_on_shadow` returns `name` verbatim when it is free in
+`scope`, or a fresh unique name (recorded as `name → fresh` in `inner`
+for `resolved_name`) when it shadows. The same call wraps the
+`Match`-arm pattern-binder insertion (`desugar_term`'s `Term::Match`
+arm loop), the `Term::Lam` param loop, and the `Term::Loop` binder
+loop. Flat-match arms (returned verbatim by `desugar_match` today)
+must carry the renamed pattern so the renamed name reaches codegen's
+arm-close gate.
+
+The fresh-name generator must avoid all in-scope names and the
+existing `$mp_N` / `$lr_N` spaces; a per-fn `<name>$<n>` scheme
+checked against the scope satisfies this and is visually traceable to
+its origin binder.
+
+## Components
+
+| Component | File | Change |
+|---|---|---|
+| Rename-on-shadow at binder sites | `crates/ailang-core/src/desugar.rs` | detect shadow against `scope`, mint fresh name, record mapping; applied at `Let`, flat-`Match` arm, `Lam` params, `Loop` binders |
+| `Term::Var` resolution | `crates/ailang-core/src/desugar.rs` | rewrite name through the active rename map |
+| Fresh-binder name scheme | `crates/ailang-core/src/desugar.rs` | per-fn `<name>$<n>`, collision-checked against scope + `$mp`/`$lr` |
+
+**No change** to the uniqueness pass, codegen drop gates, or
+`linearity`. They key by `(def, name)`; the fix makes `name`
+injective, so their existing lookups become correct without edits.
+The three uniqueness-gated drop sites and their exposure:
+
+| Drop gate | Site | Keyed by | Shadows? |
+|---|---|---|---|
+| fn `own`-param dec at return | `codegen/src/lib.rs:1447` | `(def, pname)` | never (params unique per signature) |
+| `Term::Let` scope-close drop | `codegen/src/lib.rs:1792` | `(def, name)` | **yes — fixed here** |
+| `Match` arm-close pattern dec | `codegen/src/match_lower.rs:795` | `(def, bname)` | **yes — fixed here** |
+
+## Data flow
+
+`parse (.ail → JSON-AST, hashed)` → **`desugar_module` (renames
+shadows here)** → `lift_letrecs` → `monomorphise` → `check`
+(uniqueness inference reads renamed names) / `codegen` (drop gates
+read renamed names). The rename lives entirely between parse and the
+two consumers; both consumers see the same renamed tree, so they
+cannot disagree about which binding a key denotes. The pre-desugar
+hashed form never carries a rename, so module identity and all
+hash-pin tests are unaffected.
+
+## Error handling
+
+No new diagnostics. Renaming is a total, infallible rewrite: every
+binder either keeps its name or receives a guaranteed-fresh one.
+The fresh-name loop is bounded by the in-scope set (finite per fn) and
+cannot fail to terminate (it increments until free, exactly as
+`Desugarer::fresh` already does). Programs that were ill-typed before
+desugar are rejected upstream as today; the rename does not run on
+un-parsed input.
+
+## Testing strategy
+
+RED-first; all RED fixtures already exist in the working tree:
+
+- **Let-shadow (3, shipped):** `raw_buf_{int,float,bool}_shadow_rebind_drop_balances_rc_stats` — assert `live == 0`. RED today (`live == 1`).
+- **Flat-pattern-shadow (1, differential):** `flat_pat_shadow_binder_does_not_leak_more_than_alpha_renamed` — assert the shadow fixture's `live` equals its alpha-renamed control's. RED today (`5` vs `3`). Differential by design, to isolate the shadow-collapse drop from unrelated baseline drop gaps (Box outer cell, implicit-consume of the outer binder) that are out of #43's scope.
+
+Regression guards (must stay green):
+
+- **No-op on non-shadowing fixtures:** the full existing suite must
+  stay byte-identical — every fixture without a shadow desugars
+  unchanged. This is the evidence that the rename is on-shadow-only.
+- **Reference rewrite correctness:** a shadow whose body reads the
+  renamed binder (the `get buf$3` path) must still compute the right
+  value — covered by the stdout assertions on the four fixtures
+  (`60`, and the pattern fixtures' printed sums).
+- **Desugar unit tests:** any existing `desugar_module` test on a
+  shadowing input updates to the renamed output; non-shadowing inputs
+  are untouched.
+
+## Acceptance criteria
+
+1. All four RED tests above are GREEN.
+2. The full workspace test suite is otherwise unchanged (no
+   regression; no non-shadowing fixture's output drifts).
+3. Emitted IR for the shipped fixtures is unchanged except for the
+   added drop call(s) — SSA names do not depend on binder names.
+4. `examples/raw_buf_int.ail` reaches `live == 0` under
+   `AILANG_RC_STATS`, closing #43.
+5. No change to `uniqueness.rs`, the codegen drop gates, or
+   `linearity.rs`; the `UniquenessTable` doc-comment
+   (`uniqueness.rs:90-98`), currently wrong about pop-order
+   ("last = innermost") and about every fixture having unique binder
+   names, is corrected to state that desugar guarantees per-fn name
+   uniqueness.
+```

examples/flat_pat_shadow_control.ail

@@ -0,0 +1,31 @@
+(module flat_pat_shadow_control
+  (data IntList
+    (ctor Nil)
+    (ctor Cons (con Int) (con IntList)))
+  (data Box (vars a)
+    (ctor MkBox a))
+  (fn blen
+    (doc "borrow-only length over a borrowed IntList")
+    (type (fn-type (params (borrow (con IntList))) (ret (con Int))))
+    (params xs)
+    (body (match xs
+      (case (pat-ctor Nil) 0)
+      (case (pat-ctor Cons h t) (app + 1 (app blen t))))))
+  (fn csum
+    (doc "consuming sum over an IntList")
+    (type (fn-type (params (con IntList)) (ret (con Int))))
+    (params xs)
+    (body (match xs
+      (case (pat-ctor Nil) 0)
+      (case (pat-ctor Cons h t) (app + h (app csum t))))))
+  (fn main
+    (doc "Alpha-renamed control for flat_pat_shadow_leak.ail (refs #43): structurally identical, but the inner flat-match pattern-binder is `y` (no shadow of the outer `x`). The inner payload's arm-close drop fires because (def,\"y\") does not collide with (def,\"x\"). This is the live-count baseline the shadow fixture must reach once binder names are unique per fn at desugar (C').")
+    (type (fn-type (params) (ret (con Unit)) (effects IO)))
+    (params)
+    (body
+      (let x (term-ctor IntList Cons 1 (term-ctor IntList Nil))
+        (seq
+          (match (term-ctor Box MkBox (term-ctor IntList Cons 2 (term-ctor IntList Nil)))
+            (case (pat-ctor MkBox y)
+              (app print (app blen y))))
+          (app print (app csum x)))))))

examples/flat_pat_shadow_leak.ail

@@ -0,0 +1,31 @@
+(module flat_pat_shadow_leak
+  (data IntList
+    (ctor Nil)
+    (ctor Cons (con Int) (con IntList)))
+  (data Box (vars a)
+    (ctor MkBox a))
+  (fn blen
+    (doc "borrow-only length over a borrowed IntList")
+    (type (fn-type (params (borrow (con IntList))) (ret (con Int))))
+    (params xs)
+    (body (match xs
+      (case (pat-ctor Nil) 0)
+      (case (pat-ctor Cons h t) (app + 1 (app blen t))))))
+  (fn csum
+    (doc "consuming sum over an IntList")
+    (type (fn-type (params (con IntList)) (ret (con Int))))
+    (params xs)
+    (body (match xs
+      (case (pat-ctor Nil) 0)
+      (case (pat-ctor Cons h t) (app + h (app csum t))))))
+  (fn main
+    (doc "A2b completeness fixture (refs #43): a flat-match pattern-binder `x` shadows the outer let `x`. The inner `x` (Box payload, a heap IntList) is borrow-only (consume_count 0) and must be dropped at arm close; the outer `x` is consumed once by csum (count 1). Under the (def,name) uniqueness-table collision the arm-close drop gate (match_lower.rs) reads the collapsed outer count 1 and suppresses the inner payload's drop, leaking 2 cells. Pairs with flat_pat_shadow_control.ail (same program, inner binder alpha-renamed to `y`); the live-count delta is exactly the suppressed drop. GREEN once binder names are made unique per fn at desugar.")
+    (type (fn-type (params) (ret (con Unit)) (effects IO)))
+    (params)
+    (body
+      (let x (term-ctor IntList Cons 1 (term-ctor IntList Nil))
+        (seq
+          (match (term-ctor Box MkBox (term-ctor IntList Cons 2 (term-ctor IntList Nil)))
+            (case (pat-ctor MkBox x)
+              (app print (app blen x))))
+          (app print (app csum x)))))))