raw-buf.5: RawBuf slab leak in linear shadow-rebind idiom (uniqueness key collapses shadowed binders) #42

New Issue

2026-05-30T09:07:52+02:00

Brummel commented

2026-05-30 09:07:52 +02:00

RawBuf's flat drop function (@drop_raw_buf_RawBuf, shipped in raw-buf.4) is
emitted but its drop call never fires for the final owned buffer in the
linear shadow-rebind idiom. examples/raw_buf_int.ail runs and prints 60,
but under AILANG_RC_STATS it shows allocs=2 frees=1 — one slab leaks.
Harmless for a one-shot program, accumulates in a loop.

Root cause (plan-recon confirmed)

The uniqueness side-table

UniquenessTable = BTreeMap<(String, String), UniquenessInfo>   // (def_name, binder_name)

keys ownership facts by binder name and explicitly assumes unique names
per fn — its own doc comment (crates/ailang-check/src/uniqueness.rs:93-96):
"fine in practice because every shipping fixture has unique binder names per
fn." The linear-threading idiom

(let buf (new RawBuf (con Int) 3)
  (let buf (app RawBuf.set buf 0 10)
    (let buf (app RawBuf.set buf 1 20) ...)))

reuses one name buf for four distinct ownership facts; last-write-wins
collapses them to a single entry, so the final owned binder is mis-classified
and its drop is gated off. raw_buf_int.ail is the first shipping fixture
to break the unique-name precondition.

This is let-shadowing, not mutation — each buf is a fresh immutable
binding. The idiom is legal (linearity.rs:179 "binders shadow lexically")
and LLM-natural (Rust/OCaml shadow-threading). The leak class affects any
linear-threading code, not just RawBuf — the series milestone will exercise
the same idiom.

NOT the cause

The spec's raw-buf.5 section (docs/specs/0054-raw-buf.md) diagnoses a codegen
ret-mode "synth ladder" gap (TypeDef-first resolution in codegen synth
mirroring the checker at lib.rs:3465). plan-recon empirically disproved this:
codegen already resolves the binder as drop-trackable. Do not plan against
the spec's raw-buf.5 section — it is mis-scoped and must be re-carved by a
fresh brainstorm.

Decision (2026-05-30): Approach A

Make the uniqueness representation scope-aware / per-occurrence, mirroring
the linearity checker — which already handles shadowing correctly via
Checker::with_binder push/pop and a per-scope consumed flag
(linearity.rs:179,184). This is an internal-consistency fix (bring the
uniqueness side-table up to the representation linearity already uses two files
over), not a memory-model overhaul.

Rejected B (distinct-name convention buf0/buf1/... + a checker reject for
owned-binder shadowing): it is only sound when paired with a new reject, which
is a permanent restriction on an LLM-natural idiom (collides with
feature-acceptance: an LLM reaches for shadow-threading unprompted); without
the reject it merely hides the sole reproducer; and it leaves consumed
bindings nameable in scope.

Sub-choice for the brainstorm

alpha-rename shadowed lets in desugar — risk: synthetic names (buf#1)
leak into diagnostics unless a source-name map is kept.
per-occurrence key in the side-table — keeps real diagnostic names,
changes the key type + its consumers. Preferred: closest to linearity's
representation.

Resumption

Fresh brainstorm session re-specs raw-buf.5. RED ratifier to re-add to
crates/ail/tests/e2e.rs: build_and_run_with_rc_stats("raw_buf_int.ail"),
assert stdout == "60" and live == 0. raw-buf.6 (kernel_stub retirement)
remains after.

refs #7

RawBuf's flat drop function (`@drop_raw_buf_RawBuf`, shipped in raw-buf.4) is emitted but its drop **call** never fires for the final owned buffer in the linear shadow-rebind idiom. `examples/raw_buf_int.ail` runs and prints `60`, but under `AILANG_RC_STATS` it shows `allocs=2 frees=1` — one slab leaks. Harmless for a one-shot program, accumulates in a loop. ## Root cause (plan-recon confirmed) The uniqueness side-table ``` UniquenessTable = BTreeMap<(String, String), UniquenessInfo> // (def_name, binder_name) ``` keys ownership facts by binder **name** and explicitly assumes unique names per fn — its own doc comment (`crates/ailang-check/src/uniqueness.rs:93-96`): *"fine in practice because every shipping fixture has unique binder names per fn."* The linear-threading idiom ``` (let buf (new RawBuf (con Int) 3) (let buf (app RawBuf.set buf 0 10) (let buf (app RawBuf.set buf 1 20) ...))) ``` reuses one name `buf` for four distinct ownership facts; last-write-wins collapses them to a single entry, so the final owned binder is mis-classified and its drop is gated off. `raw_buf_int.ail` is the **first** shipping fixture to break the unique-name precondition. This is `let`-shadowing, not mutation — each `buf` is a fresh immutable binding. The idiom is legal (`linearity.rs:179` "binders shadow lexically") and LLM-natural (Rust/OCaml shadow-threading). The leak class affects **any** linear-threading code, not just RawBuf — the `series` milestone will exercise the same idiom. ## NOT the cause The spec's raw-buf.5 section (`docs/specs/0054-raw-buf.md`) diagnoses a codegen ret-mode "synth ladder" gap (TypeDef-first resolution in codegen synth mirroring the checker at `lib.rs:3465`). plan-recon empirically disproved this: codegen already resolves the binder as drop-trackable. **Do not plan against the spec's raw-buf.5 section — it is mis-scoped and must be re-carved by a fresh brainstorm.** ## Decision (2026-05-30): Approach A Make the uniqueness representation **scope-aware / per-occurrence**, mirroring the linearity checker — which already handles shadowing correctly via `Checker::with_binder` push/pop and a per-scope `consumed` flag (`linearity.rs:179,184`). This is an internal-consistency fix (bring the uniqueness side-table up to the representation linearity already uses two files over), not a memory-model overhaul. **Rejected B** (distinct-name convention `buf0/buf1/...` + a checker reject for owned-binder shadowing): it is only sound when paired with a new reject, which is a permanent restriction on an LLM-natural idiom (collides with feature-acceptance: an LLM reaches for shadow-threading unprompted); without the reject it merely hides the sole reproducer; and it leaves consumed bindings nameable in scope. ## Sub-choice for the brainstorm - **alpha-rename** shadowed lets in desugar — risk: synthetic names (`buf#1`) leak into diagnostics unless a source-name map is kept. - **per-occurrence key** in the side-table — keeps real diagnostic names, changes the key type + its consumers. Preferred: closest to linearity's representation. ## Resumption Fresh brainstorm session re-specs raw-buf.5. RED ratifier to re-add to `crates/ail/tests/e2e.rs`: `build_and_run_with_rc_stats("raw_buf_int.ail")`, assert `stdout == "60"` and `live == 0`. raw-buf.6 (kernel_stub retirement) remains after. refs #7

Brummel added this to the raw-buf milestone 2026-05-30 09:07:52 +02:00

Brummel added the bug label 2026-05-30 09:07:52 +02:00

Brummel referenced this issue

2026-05-30 10:00:01 +02:00

BLOCKER: owned RawBuf never dropped — drop call not emitted at scope end (slab leak) #43

Brummel commented

2026-05-30 10:01:31 +02:00

Root cause disproven empirically (2026-05-30)

While reducing this to a minimal RED reproducer I measured the leak against three variants under AILANG_RC_STATS, and the stated root cause (uniqueness-table binder-name collapse under shadow-rebind) does not hold:

Variant	Binder situation	Result
`raw_buf_int.ail` (3× `let buf`)	colliding names	`allocs=2 frees=1 live=1`
distinct names `b0/b1/b2/b3`, 3 slots	no collision possible	`allocs=2 frees=1 live=1`
fully inline, no `let` at all	no binder	`allocs=2 frees=1 live=1`

The fully inline form

(app print (app RawBuf.get (app RawBuf.set (new RawBuf (con Int) 1) 0 10) 0))

produces byte-identical leaking IR. Where there is no binder there is nothing for the (def_name, binder_name) key to collapse — yet the drop call is still absent.

emit-ir confirms the mechanism directly: @drop_raw_buf_RawBuf is defined but main's body contains no call to it, independent of binder names. The two allocs are the RawBuf slab + the int_to_str string from print; the single free is the string's rc_dec. The slab is what leaks.

Consequence

The defect is in the owned-RawBuf drop-emission decision in codegen, not in name-keyed ownership classification. Approach A (scope-aware uniqueness key) would not fix this — the minimal reproducer has no binders to scope-separate. The Approach-A decision and the raw-buf.5 spec section both rest on the disproven diagnosis.

The real defect is tracked in #43 (BLOCKER) with the minimal reproducer examples/raw_buf_drop_min.ail. This issue should be reframed (or closed in favour of #43) rather than planned against as written.

## Root cause disproven empirically (2026-05-30) While reducing this to a minimal RED reproducer I measured the leak against three variants under `AILANG_RC_STATS`, and the stated root cause (uniqueness-table binder-name collapse under shadow-rebind) does **not** hold: | Variant | Binder situation | Result | |---|---|---| | `raw_buf_int.ail` (3× `let buf`) | colliding names | `allocs=2 frees=1 live=1` | | distinct names `b0/b1/b2/b3`, 3 slots | **no collision possible** | `allocs=2 frees=1 live=1` | | fully inline, **no `let` at all** | **no binder** | `allocs=2 frees=1 live=1` | The fully inline form ``` (app print (app RawBuf.get (app RawBuf.set (new RawBuf (con Int) 1) 0 10) 0)) ``` produces **byte-identical leaking IR**. Where there is no binder there is nothing for the `(def_name, binder_name)` key to collapse — yet the drop call is still absent. `emit-ir` confirms the mechanism directly: `@drop_raw_buf_RawBuf` is *defined* but `main`'s body contains **no call** to it, independent of binder names. The two allocs are the RawBuf slab + the `int_to_str` string from `print`; the single free is the string's `rc_dec`. The slab is what leaks. ### Consequence The defect is in the **owned-RawBuf drop-emission decision** in codegen, not in name-keyed ownership classification. **Approach A (scope-aware uniqueness key) would not fix this** — the minimal reproducer has no binders to scope-separate. The Approach-A decision and the raw-buf.5 spec section both rest on the disproven diagnosis. The real defect is tracked in #43 (BLOCKER) with the minimal reproducer `examples/raw_buf_drop_min.ail`. This issue should be reframed (or closed in favour of #43) rather than planned against as written.

Brummel referenced this issue from a commit

2026-05-30 12:53:00 +02:00

test: RED owned-RawBuf drop-leak repro (refs #43)

Brummel referenced this issue from a commit

2026-05-30 12:53:00 +02:00

test: RED shadow-rebind RawBuf drop-leak on shipped fixtures (refs #43)

Brummel closed this issue

2026-05-30 12:53:11 +02:00

Sign in to join this conversation.