spec: raw-buf — re-carve drop ratification to raw-buf.5, retirement to .6 (refs #7)

raw-buf.4 (RawBuf payload + Term::New desugar) implemented and about to
land, but it surfaced that the drop ratification was mis-scoped: the
flat drop FUNCTION is emittable in .4, but the drop CALL needs a codegen
resolution mechanism the .4 plan did not scope. An owned RawBuf binder's
value is a cross-module type-scoped intrinsic call ((app RawBuf.set ..) :
own (RawBuf a)); codegen's is_rc_heap_allocated only marks an App binder
drop-trackable when synth_callee_ret_mode resolves the callee's Own mode,
but codegen synth_arg_type has no TypeDef-first / cross-module-mono
resolution ladder (unlike the checker's lib.rs:3465), so the binder is
non-trackable and no drop call is inserted. A second site
(uniqueness::infer_module's per-module globals) misses the cross-module
borrow mode too.

Re-carve (six iterations; .1-.4 done, .5/.6 remain):
  raw-buf.4 — RawBuf payload + Term::New desugar + flat drop FUNCTION
              (DONE). Worked program prints 60; Float/Bool/reject ship.
  raw-buf.5 — owned cross-module type-scoped drop-call resolution: a
              TypeDef-first + cross-module-mono arm in codegen
              synth_arg_type feeding is_rc_heap_allocated /
              synth_callee_ret_mode / drop_symbol_for_binder, plus
              cross-module op visibility in uniqueness::infer_module.
              Ratified by raw_buf_no_leak (live == 0).
  raw-buf.6 — kernel_stub retirement (was .5).

Also documents the raw-buf.4 diagnostic-behaviour change: because the
Term::New desugar now runs before check, (new T ..) with a missing
new-op surfaces type-scoped-member-not-found (more precise) rather than
the prep.2 new-type-not-constructible it supersedes; new-arg-kind-mismatch
is obsoleted (the desugar drops the type-arg). Same rejection conditions,
preserved. And corrects the @ailang_rc_release spec slip to the real
symbol @ailang_rc_dec.

The drop-call resolution is its own iteration for the same reason
raw-buf.3 became a mechanism prep: it is a codegen-resolution mechanism
(parity with the checker's type-scoped/cross-module ladder), separable
from the RawBuf payload, and isolating it keeps the resolution change
off the .4 payload diff.

docs/specs/0054-raw-buf.md

@@ -72,7 +72,11 @@ of the type-scoped polymorphic intrinsic mechanism raw-buf.3 adds.
 
 ## Architecture
 
-Five iterations. raw-buf.1 and raw-buf.2 are done; .3/.4/.5 remain.
+Six iterations. raw-buf.1–.4 are done; .5/.6 remain. (The drop
+ratification, originally bundled into .4, was re-carved into its own
+iteration .5 once the implement surfaced that an owned cross-module
+type-scoped intrinsic binder's drop-call needs a codegen
+resolution mechanism the .4 plan did not scope — see iteration 5.)
 
 1. **Intercept registry** (raw-buf.1) — **DONE** (`140a0c0`).
    Lifted the hard-coded `try_emit_primitive_instance_body` match
@@ -114,14 +118,14 @@ Five iterations. raw-buf.1 and raw-buf.2 are done; .3/.4/.5 remain.
    plus its 2 scope-qualified `INTERCEPTS` entries
    (`StubT_peek__Int`, `StubT_peek__Float` — StubT's `param-in` is
    `{Int, Float}`) and a unit test asserting the scoped symbols +
-   the bijection. `peek` retires with the stub in raw-buf.5, exactly
+   the bijection. `peek` retires with the stub in raw-buf.6, exactly
    as `answer` does. No running E2E here (constructing a `StubT`
    needs the Term::New desugar that lands in raw-buf.4); the
    mechanism is unit-test ratified.
 
-4. **RawBuf payload + Term::New desugar** (raw-buf.4) — RawBuf as a
+4. **RawBuf payload + Term::New desugar** (raw-buf.4) — **DONE**.
-   clean consumer of the raw-buf.3 mechanism, plus the `(new …)`
+   RawBuf as a clean consumer of the raw-buf.3 mechanism, plus the
-   construction sugar. Adds:
+   `(new …)` construction sugar. Shipped:
    - The `raw_buf` submodule (`src/raw_buf/{mod.rs, source.ail}`)
      with the `RawBuf` TypeDef (`param-in (a Int Float Bool)`) and
      the four ops `new`/`get`/`set`/`size`, each an `(intrinsic)`
@@ -129,20 +133,48 @@ Five iterations. raw-buf.1 and raw-buf.2 are done; .3/.4/.5 remain.
    - The 12 scope-qualified `INTERCEPTS` entries
      (`RawBuf_{new,get,set,size}__{Int,Float,Bool}`) + emit fns
      (`@ailang_rc_alloc` + getelementptr + load/store) — mechanical
-     now that raw-buf.3 built the naming + bijection machinery.
+     on top of the raw-buf.3 naming + bijection machinery.
    - The `Term::New` desugar `(new T <types…> <values…>)` →
      `(app T.new <values…>)` (general — `(new StubT 42)` benefits
-     too), removing BOTH codegen `Term::New` deferral arms
+     too), removing BOTH codegen `Term::New` deferral arms that
-     (`crates/ailang-codegen/src/lib.rs` ~2094 `lower_term` +
+     prep.2 left marked "milestone raw-buf". The desugar runs before
-     ~3296 synth path) that prep.2 left marked "milestone raw-buf".
+     check, dropping the `NewArg::Type`; the element type is
-   - Drop for primitive-element RawBuf: a single
+     recovered by inference from use.
-     `@ailang_rc_release` on the slab pointer.
+   - The flat intrinsic-storage drop *function* `@drop_raw_buf_RawBuf`
+     (a single `@ailang_rc_dec` on the slab pointer), emitted for
+     any TypeDef whose `new` op is `(intrinsic)`-bodied.
    - `ailang-surface` wiring: `parse_raw_buf` + workspace injection
      (raw_buf kernel-tier auto-imported; workspace count 4 → 5).
-   The worked consumer program runs end-to-end and prints `60`.
+   The worked consumer program runs end-to-end and prints `60`;
+   the Float/Bool variants and the `param-in` reject also ship.
    `kernel_stub` (with `peek` + `answer`) stays alongside (count 5).
+   **Not** in .4: the drop *call* does not yet fire at scope close
+   for an owned RawBuf binder — that needs the codegen resolution
+   mechanism in .5 (the drop function is correct and waiting).
 
-5. **kernel_stub retirement** (raw-buf.5) — RawBuf now subsumes
+5. **Owned cross-module type-scoped drop-call resolution**
+   (raw-buf.5) — The codegen mechanism that makes the .4 flat drop
+   *fire*. An owned RawBuf binder's value is a cross-module
+   type-scoped intrinsic call (`(app RawBuf.set …) : own (RawBuf a)`);
+   codegen's `is_rc_heap_allocated` only marks an `App` binder
+   drop-trackable when `synth_callee_ret_mode` resolves the callee's
+   `Own` ret-mode, but codegen `synth_arg_type` has no TypeDef-first
+   / cross-module-mono resolution ladder (unlike the checker's
+   `lib.rs:3465`), so the binder is classified non-trackable and no
+   drop call is inserted. A second site —
+   `uniqueness::infer_module`'s per-module globals map — likewise
+   misses the cross-module `borrow` mode, defaulting the
+   `RawBuf.get` arg to `Consume`. raw-buf.5 teaches codegen's
+   resolution a TypeDef-first + cross-module-mono arm (mirror of the
+   checker ladder) feeding `is_rc_heap_allocated` /
+   `synth_callee_ret_mode` / `drop_symbol_for_binder`, and extends
+   `uniqueness::infer_module` with cross-module op visibility.
+   Ratified by `raw_buf_no_leak` (the worked Int program under
+   `AILANG_RC_STATS` reaches `live == 0`). This is the drop
+   ratification the spec's acceptance criterion requires; isolating
+   it keeps the resolution-mechanism change off the .4 payload diff.
+
+6. **kernel_stub retirement** (raw-buf.6) — RawBuf now subsumes
    every ratification role the stub held: `Term::New` end-to-end
    (the `(new RawBuf …)` consumer), `param-in` reject (the Str
    reject fixture), kernel-tier auto-import, the monomorphic
@@ -162,10 +194,12 @@ Five iterations. raw-buf.1 and raw-buf.2 are done; .3/.4/.5 remain.
 Ordering rationale: .3 isolates the risky mono+bijection mechanism
 change (proven on the stub) from RawBuf's payload diff; .4 lands
 RawBuf as a mechanical consumer plus the orthogonal `(new …)`
-desugar; .5 removes the now-redundant stub without touching the new
+desugar + the flat drop *function*; .5 isolates the codegen
-RawBuf code. Each bijection-registry change is isolated to one diff
+drop-call *resolution* mechanism (cross-module type-scoped ret-mode
-(peek entries added in .3, 12 RawBuf entries in .4, peek+answer
++ uniqueness visibility) off the .4 payload diff; .6 removes the
-removed in .5).
+now-redundant stub without touching the new RawBuf code. Each
+bijection-registry change is isolated to one diff (peek entries
+added in .3, 12 RawBuf entries in .4, peek+answer removed in .6).
 
 ## Concrete code shapes
 
@@ -369,9 +403,12 @@ Element widths: `Int = 8`, `Float = 8`, `Bool = 1`. Header is i64,
 8-byte aligned; element payload follows directly. `@ailang_rc_alloc`
 is called with `8 + size * sizeof(T)` and returns the slab base
 `ptr`. The size header is self-describing, so drop and `RawBuf.size`
-need no side-table. Drop is a single `@ailang_rc_release` on the
+need no side-table. Drop is a single `@ailang_rc_dec` on the
 slab pointer — primitive elements carry no recursive drops; the
-per-TypeDef drop generation gets a "primitive-element-RawBuf" arm.
+per-TypeDef drop generation gets a flat-slab arm (raw-buf.4 emits
+the drop *function*; raw-buf.5 makes the drop *call* fire). (`@ailang_rc_dec`
+is the real runtime symbol — the earlier `@ailang_rc_release`
+spelling was a spec slip.)
 
 ## Components
 
@@ -380,8 +417,9 @@ per-TypeDef drop generation gets a "primitive-element-RawBuf" arm.
 | Intercept registry | raw-buf.1 (DONE) | `crates/ailang-codegen/src/intercepts.rs` + dispatch in `lib.rs` |
 | Kernel family-crate rename | raw-buf.2 (DONE) | `crates/ailang-kernel/` (renamed); `ailang-surface` dep + `loader.rs`; doc/ledger rows |
 | Type-scoped polymorphic intrinsic mechanism | raw-buf.3 | scope-qualified mono mangling in `crates/ailang-check/src/mono.rs` (+ wherever prep.1 type-scoped resolution records the TypeDef, per recon); bijection-collector expansion arm in `crates/ailang-codegen/src/intercepts.rs` (`workspace_intrinsic_markers`); `StubT.peek` fn added to `crates/ailang-kernel/src/kernel_stub/source.ail` + 2 `StubT_peek__*` entries + emit fns; `kernel_stub_module_round_trips` updated for the new fn; mono/bijection unit tests |
-| RawBuf payload + Term::New desugar | raw-buf.4 | new `crates/ailang-kernel/src/raw_buf/{mod.rs, source.ail}` + `lib.rs` re-export; `parse_raw_buf` + injection in `crates/ailang-surface/src/loader.rs` + re-export in `lib.rs`; 12 entries + emit fns in `intercepts.rs`; `Term::New` desugar in `crates/ailang-core/src/desugar.rs` + removal of both codegen deferral arms in `crates/ailang-codegen/src/lib.rs`; primitive-element-RawBuf drop arm; `workspace_pin` 4 → 5; round-trip + E2E tests |
+| RawBuf payload + Term::New desugar | raw-buf.4 (DONE) | new `crates/ailang-kernel/src/raw_buf/{mod.rs, source.ail}` + `lib.rs` re-export; `parse_raw_buf` + injection in `crates/ailang-surface/src/loader.rs` + re-export in `lib.rs`; 12 entries + emit fns in `intercepts.rs`; `Term::New` desugar in `crates/ailang-core/src/desugar.rs` + removal of both codegen deferral arms in `crates/ailang-codegen/src/lib.rs`; flat-slab drop *function* in `drop.rs`/`lib.rs`; `workspace_pin` 4 → 5; round-trip + Int/Float/Bool/reject E2E |
-| kernel_stub retirement | raw-buf.5 | delete `crates/ailang-kernel/src/kernel_stub/` + re-export; drop `parse_kernel_stub` + injection; remove `answer` + `StubT_peek__*` entries + emit fns in `intercepts.rs`; delete `kernel_stub_module_round_trips`; `workspace_pin` 5 → 4; `design/INDEX.md` + `design/models/0007-kernel-extensions.md` |
+| Owned cross-module type-scoped drop-call resolution | raw-buf.5 | TypeDef-first + cross-module-mono resolution arm in codegen `synth_arg_type` (`crates/ailang-codegen/src/lib.rs`) feeding `is_rc_heap_allocated` / `synth_callee_ret_mode` / `drop_symbol_for_binder`; cross-module op visibility in `uniqueness::infer_module` (`crates/ailang-check/src/uniqueness.rs`); `raw_buf_no_leak` E2E |
+| kernel_stub retirement | raw-buf.6 | delete `crates/ailang-kernel/src/kernel_stub/` + re-export; drop `parse_kernel_stub` + injection; remove `answer` + `StubT_peek__*` entries + emit fns in `intercepts.rs`; delete `kernel_stub_module_round_trips`; `workspace_pin` 5 → 4; `design/INDEX.md` + `design/models/0007-kernel-extensions.md` |
 
 ## Data flow
 
@@ -415,9 +453,15 @@ per-TypeDef drop generation gets a "primitive-element-RawBuf" arm.
    i64`; `RawBuf_get__Int` a `load i64`; `RawBuf_size__Int` a header
    load.
 
+**Drop-call resolution (raw-buf.5):** the desugared
+`(app RawBuf.set …) : own (RawBuf a)` binder is recognised as
+rc-heap-trackable once codegen `synth_callee_ret_mode` resolves the
+cross-module type-scoped callee's `Own` mode; the let-scope-close
+drop call to `@drop_raw_buf_RawBuf` then fires.
+
 **Workspace module count:** prelude + kernel_stub + 2 test fixtures
-= 4 today. raw-buf.4 adds raw_buf → 5. raw-buf.5 retires kernel_stub
+= 4 before raw-buf.4. raw-buf.4 adds raw_buf → 5. raw-buf.6 retires
-→ 4. The `workspace_pin` test pins each transition.
+kernel_stub → 4. The `workspace_pin` test pins each transition.
 
 ## Error handling
 
@@ -425,9 +469,17 @@ Two consumer-facing diagnostics; both already shipped, no new arms:
 
 - **`param-not-in-restricted-set`** (prep.3, fieldtest F8) — fires
   on `(con RawBuf (con Str))` or any non-{Int,Float,Bool} element.
-- **`new-type-not-constructible`** (prep.3, fieldtest F5) — fires on
+- **`type-scoped-member-not-found`** — fires on `(new SomeType …)`
-  `(new SomeType …)` when `SomeType` has no `(fn new …)`. raw_buf
+  when `SomeType` has no `(fn new …)`. (raw-buf.4 note: because the
-  ships `new`, so the worked program passes.
+  `Term::New` desugar now runs *before* check, the rejection is
+  raised by synth's type-scoped resolution of the desugared
+  `(app SomeType.new …)`, surfacing the more precise
+  `type-scoped-member-not-found` rather than the prep.2
+  `new-type-not-constructible` it superseded — same rejection
+  condition, more context. The prep.2 `new-arg-kind-mismatch` is
+  obsoleted: the desugar drops the type-arg, so there is no
+  arg-kind to mismatch.) raw_buf ships `new`, so the worked program
+  passes.
 
 The codegen `Term::New` deferral arms (`lib.rs` ~2094 + ~3296,
 message "… milestone raw-buf") are **removed** in raw-buf.4 once the
@@ -467,13 +519,23 @@ backlog item yet.
 - E2E `raw_buf_param_in_reject_e2e`: the Str reject fixture — `ail
   check` exits non-zero with `param-not-in-restricted-set`.
 - Term::New desugar ratified by the `(new RawBuf …)` form building
-  and running (it would hit the now-removed deferral arm otherwise).
+  and running (it would hit the now-removed deferral arm otherwise);
-- Drop ratification: allocate a RawBuf, let it go out of scope, no
+  plus `new_stubt_builds_and_runs` (`(new StubT 42)` via the real-body
-  leak (re-uses the existing leak-check harness).
+  `StubT.new`).
 - Bijection green with the 12 RawBuf entries added.
 - `workspace_pin` count 4 → 5 (+ `contains_key("raw_buf")`).
+- (The drop / no-leak ratification moved to raw-buf.5 — the flat drop
+  function ships here but its call-insertion needs the .5 resolution
+  mechanism.)
 
-**raw-buf.5 (retirement):**
+**raw-buf.5 (drop-call resolution):**
+- `raw_buf_no_leak`: the worked Int program under `AILANG_RC_STATS`
+  reaches `live == 0` (the slab is freed at let-scope close). RED
+  before the resolution arm, GREEN after — the iteration's ratifier.
+- Full suite green; existing symbols unchanged (the resolution arm
+  fires only for owned cross-module type-scoped binders).
+
+**raw-buf.6 (retirement):**
 - `workspace_pin` re-baselines 5 → 4 (raw_buf in, kernel_stub out).
 - `kernel_stub_module_round_trips` deleted;
   `raw_buf_module_round_trips` carries the invariant forward.
@@ -486,19 +548,21 @@ backlog item yet.
 The milestone ships when:
 
 1. The worked consumer program runs end-to-end: `ail check && ail
-   build && ail run` prints `60` (raw-buf.4).
+   build && ail run` prints `60` (raw-buf.4 ✓).
-2. The param-in reject fixture exits at `ail check` with the prep.3
+2. The param-in reject fixture exits at `ail check` with the
-   `param-not-in-restricted-set` diagnostic (raw-buf.4).
+   `param-not-in-restricted-set` diagnostic (raw-buf.4 ✓).
 3. RawBuf's four ops are `(intrinsic)` markers, each mono'd to a
    scope-qualified symbol (`RawBuf_<op>__<T>`) with a matching
    `INTERCEPTS` entry; `intercepts_bijection_with_intrinsic_markers`
-   is green (the mechanism in raw-buf.3, the 12 entries in raw-buf.4).
+   is green (the mechanism in raw-buf.3, the 12 entries in raw-buf.4 ✓).
 4. `Term::New` no longer reaches codegen — the desugar eliminates it
-   and both deferral arms (`lib.rs` ~2094 + ~3296) are removed
+   and both deferral arms are removed (raw-buf.4 ✓).
-   (raw-buf.4).
+5. A RawBuf allocated and dropped at scope close does not leak
-5. `kernel_stub` is retired and `raw_buf` takes over its
+   (`raw_buf_no_leak`, `live == 0`) — the drop call fires
-   ratification roles (raw-buf.5).
+   (raw-buf.5).
-6. Workspace test suite green at each iteration boundary, plus the
+6. `kernel_stub` is retired and `raw_buf` takes over its
+   ratification roles (raw-buf.6).
+7. Workspace test suite green at each iteration boundary, plus the
    new tests in § Testing strategy.
 
 ## Feature-acceptance argument