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.
This commit is contained in:
+103
-39
@@ -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
|
||||
clean consumer of the raw-buf.3 mechanism, plus the `(new …)`
|
||||
construction sugar. Adds:
|
||||
4. **RawBuf payload + Term::New desugar** (raw-buf.4) — **DONE**.
|
||||
RawBuf as a clean consumer of the raw-buf.3 mechanism, plus the
|
||||
`(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
|
||||
(`crates/ailang-codegen/src/lib.rs` ~2094 `lower_term` +
|
||||
~3296 synth path) that prep.2 left marked "milestone raw-buf".
|
||||
- Drop for primitive-element RawBuf: a single
|
||||
`@ailang_rc_release` on the slab pointer.
|
||||
too), removing BOTH codegen `Term::New` deferral arms that
|
||||
prep.2 left marked "milestone raw-buf". The desugar runs before
|
||||
check, dropping the `NewArg::Type`; the element type is
|
||||
recovered by inference from use.
|
||||
- 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
|
||||
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 .5).
|
||||
desugar + the flat drop *function*; .5 isolates the codegen
|
||||
drop-call *resolution* mechanism (cross-module type-scoped ret-mode
|
||||
+ uniqueness visibility) off the .4 payload diff; .6 removes the
|
||||
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 |
|
||||
| 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` |
|
||||
| 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 |
|
||||
| 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. The `workspace_pin` test pins each transition.
|
||||
= 4 before raw-buf.4. raw-buf.4 adds raw_buf → 5. raw-buf.6 retires
|
||||
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
|
||||
`(new SomeType …)` when `SomeType` has no `(fn new …)`. raw_buf
|
||||
ships `new`, so the worked program passes.
|
||||
- **`type-scoped-member-not-found`** — fires on `(new SomeType …)`
|
||||
when `SomeType` has no `(fn new …)`. (raw-buf.4 note: because the
|
||||
`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).
|
||||
- Drop ratification: allocate a RawBuf, let it go out of scope, no
|
||||
leak (re-uses the existing leak-check harness).
|
||||
and running (it would hit the now-removed deferral arm otherwise);
|
||||
plus `new_stubt_builds_and_runs` (`(new StubT 42)` via the real-body
|
||||
`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).
|
||||
2. The param-in reject fixture exits at `ail check` with the prep.3
|
||||
`param-not-in-restricted-set` diagnostic (raw-buf.4).
|
||||
build && ail run` prints `60` (raw-buf.4 ✓).
|
||||
2. The param-in reject fixture exits at `ail check` with the
|
||||
`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
|
||||
(raw-buf.4).
|
||||
5. `kernel_stub` is retired and `raw_buf` takes over its
|
||||
ratification roles (raw-buf.5).
|
||||
6. Workspace test suite green at each iteration boundary, plus the
|
||||
and both deferral arms are removed (raw-buf.4 ✓).
|
||||
5. A RawBuf allocated and dropped at scope close does not leak
|
||||
(`raw_buf_no_leak`, `live == 0`) — the drop call fires
|
||||
(raw-buf.5).
|
||||
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
|
||||
|
||||
Reference in New Issue
Block a user