spec: raw-buf — re-carve .2/.3/.4 post intrinsic-bodies (refs #7)
raw-buf.1 (intercept registry) shipped (140a0c0). The intrinsic-bodies
milestone (#9) then landed and pulled the foundation out from under the
original raw-buf.2/.3 split, so this revises the spec.
Two foundation changes from intrinsic-bodies:
1. The placeholder-body convention the original spec leaned on
((body x) round-trip stubs) is gone. prelude.ail now uses
(intrinsic) markers, and check_fn (lib.rs:2173) typechecks every
non-intrinsic body including kernel-tier ones. RawBuf.get with a
placeholder body (declared (ret a), body constructs a RawBuf) is now
a hard type error — get/new/set/size MUST be (intrinsic).
2. An (intrinsic) marker now requires a matching INTERCEPTS entry as a
lockstep pair (intercepts_bijection_with_intrinsic_markers). The
"manifest visible / codegen deferred" intermediate state the original
raw-buf.2 was designed to ship is forbidden by that invariant — the
marker and its codegen entry must land in the same iteration.
Re-carve (3 remaining iterations, retirement isolated):
raw-buf.2 — kernel family-crate rename ailang-kernel-stub →
ailang-kernel. Pure refactor, zero behavioural change.
raw-buf.3 — RawBuf end-to-end: raw_buf module ((intrinsic) markers)
+ 12 INTERCEPTS entries + Term::New desugar + drop +
ailang-surface wiring + E2E. Manifest+codegen land
together. Workspace count 4 → 5.
raw-buf.4 — kernel_stub retirement: RawBuf subsumes every
ratification role (Term::New, param-in, kernel-tier
auto-import, intrinsic); answer entry + stub removed,
count 5 → 4.
Preserved unchanged: Goal, slab layout, feature-acceptance argument.
The raw_buf module Form-A source in § Concrete code shapes is
gate-verified: ail check → ok (35 symbols across 3 modules); the four
(intrinsic) markers are legal because the module is (kernel).
Grounding-check: 8/9 load-bearing current-behaviour assumptions
ratified by named green tests. The single override is the Term::New
codegen-deferral arm (lib.rs:2094 + sibling at lib.rs:3296, the latter
surfaced by the grounding agent) — a transient prep.2 marker that
raw-buf.3 deletes, not a relied-upon invariant; forward-ratified by
raw-buf.3's build-and-run E2E. Override logged, not a discard.
This commit is contained in:
+374
-344
@@ -1,9 +1,36 @@
|
|||||||
# raw-buf — Design Spec
|
# raw-buf — Design Spec
|
||||||
|
|
||||||
**Date:** 2026-05-29
|
**Date:** 2026-05-29 (revised 2026-05-29)
|
||||||
**Status:** Draft — awaiting user spec review
|
**Status:** Draft — awaiting user spec review
|
||||||
**Authors:** orchestrator + Claude
|
**Authors:** orchestrator + Claude
|
||||||
|
|
||||||
|
> **Revision note.** raw-buf.1 (intercept registry) shipped
|
||||||
|
> (`140a0c0`). This spec was then re-carved because the
|
||||||
|
> `intrinsic-bodies` milestone (#9) landed afterwards and removed
|
||||||
|
> the foundation the original raw-buf.2/.3 split stood on:
|
||||||
|
>
|
||||||
|
> 1. The **placeholder-body convention** the original spec relied
|
||||||
|
> on (`(body x)` round-trip stubs, "the existing convention from
|
||||||
|
> `examples/prelude.ail`") no longer exists. `prelude.ail` now
|
||||||
|
> uses `(intrinsic)` markers, and the checker (`check_fn`,
|
||||||
|
> `crates/ailang-check/src/lib.rs:2173`) typechecks every
|
||||||
|
> non-intrinsic body — including kernel-tier bodies. A
|
||||||
|
> placeholder body for `RawBuf.get` (declared `(ret a)`, body
|
||||||
|
> constructing a `RawBuf`) is now a hard type error. `get` (and
|
||||||
|
> `new`/`set`/`size`) MUST be `(intrinsic)`.
|
||||||
|
> 2. An `(intrinsic)` marker now requires a matching `INTERCEPTS`
|
||||||
|
> codegen entry as a **lockstep pair**, enforced by
|
||||||
|
> `intercepts::tests::intercepts_bijection_with_intrinsic_markers`.
|
||||||
|
> The "manifest visible, codegen deferred" intermediate state
|
||||||
|
> the original raw-buf.2 was designed to ship is therefore
|
||||||
|
> forbidden by an invariant. The marker and its codegen entry
|
||||||
|
> must land in the same iteration.
|
||||||
|
>
|
||||||
|
> Consequence: the kernel-manifest and the codegen now land
|
||||||
|
> together in one iteration. The remaining work is re-carved into
|
||||||
|
> three iterations (raw-buf.2/.3/.4) below. The Goal, slab layout,
|
||||||
|
> and feature-acceptance argument are unchanged.
|
||||||
|
|
||||||
## Goal
|
## Goal
|
||||||
|
|
||||||
Ship `RawBuf a` — the first kernel-tier *base* extension — as a
|
Ship `RawBuf a` — the first kernel-tier *base* extension — as a
|
||||||
@@ -22,97 +49,170 @@ backlog:
|
|||||||
RawBuf is that primitive.
|
RawBuf is that primitive.
|
||||||
|
|
||||||
The milestone also fulfils the architectural commitment from the
|
The milestone also fulfils the architectural commitment from the
|
||||||
kernel-extensions whitepaper § "Plugin contract":
|
kernel-extensions whitepaper § "Plugin contract": the migration
|
||||||
|
of the hardcoded primitive-instance intercepts into one registry,
|
||||||
> *The migration of existing hardcoded primitive-instance
|
triggered by the first real base extension shipping. raw-buf.1
|
||||||
> intercepts (`try_emit_primitive_instance_body`) into the plugin
|
already discharged that migration (the registry is live and the
|
||||||
> registry is triggered by the first real base extension shipping
|
`intrinsic-bodies` bijection pin locks marker ↔ entry); RawBuf is
|
||||||
> (RawBuf). One registry mechanism for all intercepts.*
|
now the first *real-payload* consumer of that registry.
|
||||||
|
|
||||||
This makes raw-buf both a feature ship (a new type LLM authors
|
This makes raw-buf both a feature ship (a new type LLM authors
|
||||||
can reach for) and a foundation move (the *one* plumbing path
|
can reach for) and the proof that the registry path carries a
|
||||||
for all current and future codegen intercepts).
|
genuine domain type, not just the migrated primitive intercepts.
|
||||||
|
|
||||||
## Architecture
|
## Architecture
|
||||||
|
|
||||||
Three layered moves, one per iteration:
|
Four iterations. raw-buf.1 is done; .2/.3/.4 remain.
|
||||||
|
|
||||||
1. **Intercept registry** (raw-buf.1) — Lift the existing
|
1. **Intercept registry** (raw-buf.1) — **DONE** (`140a0c0`).
|
||||||
hard-coded `try_emit_primitive_instance_body` match
|
Lifted the hard-coded `try_emit_primitive_instance_body` match
|
||||||
(`eq__Str`, `compare__Int|Bool|Str`, plus the `float_*`
|
into the registry table `INTERCEPTS` in
|
||||||
family that lowers to `fcmp`) into a registry table
|
`crates/ailang-codegen/src/intercepts.rs`; the dispatch site is
|
||||||
`&[Intercept { name, sig, emit }]`. The single existing
|
a `intercepts::lookup` call. Pure refactor, zero behavioural
|
||||||
dispatch site in `lower_fn_body` (the `emit_fn` caller
|
change. (The subsequent `intrinsic-bodies` milestone added the
|
||||||
that today reaches `try_emit_primitive_instance_body`)
|
`(intrinsic)` marker, the `Term::Intrinsic` leaf, and the
|
||||||
becomes a table lookup. Zero behavioural change; every
|
marker ↔ entry bijection pin on top of this registry.)
|
||||||
existing test stays green. This iter is a pure refactor
|
|
||||||
— its ratification is the workspace test suite as-is.
|
|
||||||
|
|
||||||
2. **RawBuf kernel-tier manifest + checker side** (raw-buf.2) —
|
2. **Kernel family-crate rename** (raw-buf.2) — Pure refactor,
|
||||||
Rename `crates/ailang-kernel-stub/` to `crates/ailang-kernel/`
|
zero behavioural change. Rename `crates/ailang-kernel-stub/` →
|
||||||
and re-shape it as a family-crate: one Cargo crate hosting
|
`crates/ailang-kernel/` and reshape it as a *family-crate*: one
|
||||||
*all* kernel-tier modules as sibling Rust submodules under
|
Cargo crate hosting all kernel-tier modules as sibling Rust
|
||||||
`src/`, one submodule per `.ail` source. The renamed crate
|
submodules under `src/`, one submodule per `.ail` source. The
|
||||||
carries `src/kernel_stub/{mod.rs, source.ail}` (the existing
|
renamed crate carries `src/kernel_stub/{mod.rs, source.ail}`
|
||||||
stub, unchanged) and gains `src/raw_buf/{mod.rs, source.ail}`
|
(the existing stub, **verbatim including its current `answer`
|
||||||
(the new RawBuf module). `src/lib.rs` re-exports each
|
intrinsic fn** — the source has grown since the original spec
|
||||||
submodule's `SOURCE` const under a stable name
|
was written). `src/lib.rs` re-exports each submodule's `SOURCE`
|
||||||
(`pub use kernel_stub::SOURCE as STUB_AIL;`,
|
const under the stable name every consumer already binds
|
||||||
`pub use raw_buf::SOURCE as RAW_BUF_AIL;`), preserving the
|
(`pub use kernel_stub::SOURCE as STUB_AIL;`). The acyclic chain
|
||||||
public-symbol surface every consumer already binds to. The
|
`ailang-surface → ailang-kernel → ailang-core` is preserved;
|
||||||
parse hops stay in `ailang-surface` (`parse_kernel_stub`
|
the parse hop `parse_kernel_stub` stays in `ailang-surface`. No
|
||||||
joined by `parse_raw_buf`); the acyclic dependency chain
|
`raw_buf` submodule yet — this iteration is *only* the rename,
|
||||||
`ailang-surface → ailang-kernel → ailang-core` is preserved.
|
so its failure mode is "existing tests break", the cleanest
|
||||||
The raw_buf module declares:
|
bisection target. Ratified by the existing suite green.
|
||||||
- `(data RawBuf (vars a) (ctor B (storage-tag)) (param-in
|
|
||||||
(a Int Float Bool)))` — opaque single-ctor TypeDef with
|
|
||||||
element-type restriction.
|
|
||||||
- `(fn new ...)`, `(fn get ...)`, `(fn set ...)`,
|
|
||||||
`(fn size ...)` with type signatures from the whitepaper
|
|
||||||
and placeholder bodies (same convention as the existing
|
|
||||||
`eq__Int` / `compare__Int` intercept stubs in
|
|
||||||
`examples/prelude.ail`).
|
|
||||||
Checker accepts a consumer-fixture `(con RawBuf (con Int))`
|
|
||||||
in a type slot; `ail check` passes. `ail build` fails
|
|
||||||
precisely with `intercept-not-registered: new__RawBuf__Int`
|
|
||||||
(or the existing Term::New-deferral diagnostic), because the
|
|
||||||
registry has no entry yet — that diagnostic IS the
|
|
||||||
ratification.
|
|
||||||
|
|
||||||
3. **RawBuf codegen intercepts + Term::New desugar + stub
|
3. **RawBuf end-to-end** (raw-buf.3) — The feature ship, landing
|
||||||
retirement** (raw-buf.3) — Register the 12 element-type-
|
the manifest and the codegen together (the lockstep pair the
|
||||||
specialised entries (`new__RawBuf__Int|Float|Bool`,
|
bijection invariant requires). Adds:
|
||||||
`RawBuf_get__Int|Float|Bool`, `RawBuf_set__Int|Float|Bool`,
|
- The `raw_buf` submodule (`src/raw_buf/{mod.rs, source.ail}`)
|
||||||
`RawBuf_size__Int|Float|Bool`) into the registry. Lower
|
with the `RawBuf` TypeDef (`param-in (a Int Float Bool)`) and
|
||||||
each via `@ailang_rc_alloc` + getelementptr + load/store —
|
the four operations `new`/`get`/`set`/`size`, each an
|
||||||
no new C code. Add a desugar pass `(new T args)` →
|
`(intrinsic)` marker (NOT a placeholder body).
|
||||||
`(app T.new args)` so Term::New is eliminated before
|
- The 12 element-specialised `INTERCEPTS` entries (4 ops × 3
|
||||||
codegen — Term::New becomes purely a checker-side construct
|
element types) lowering each via `@ailang_rc_alloc` +
|
||||||
(the desugar is the codegen completion the prep.2 deferral
|
getelementptr + load/store — no new C code. The entry `name`
|
||||||
pointed at). Worked consumer program runs end-to-end. Retire
|
of each MUST equal the mono-mangled symbol of its
|
||||||
the `kernel_stub` submodule from `crates/ailang-kernel/`
|
`(intrinsic)` marker; the bijection test is the pin that
|
||||||
since RawBuf is now the second-and-real kernel-tier
|
forces this and surfaces the exact expected strings.
|
||||||
consumer that CLAUDE.md names as the stub's retirement
|
- A desugar pass `(new T <types…> <values…>)` → an instantiated
|
||||||
trigger: delete `src/kernel_stub/` and its `lib.rs`
|
`(app T.new <values…>)` that consumes the `NewArg::Type`
|
||||||
re-export, drop `parse_kernel_stub` and its surface
|
element type to drive monomorphisation to `new__RawBuf__<T>`,
|
||||||
injection in `ailang-surface`, and update INDEX +
|
so `Term::New` is eliminated before codegen. `Term::New`
|
||||||
whitepaper to reflect.
|
becomes a checker-side-only construct (the codegen completion
|
||||||
|
the prep.2 deferral pointed at). raw-buf.3 removes **both**
|
||||||
|
`Term::New` deferral arms codegen currently carries — the
|
||||||
|
`lower_term` arm (`crates/ailang-codegen/src/lib.rs:2094`,
|
||||||
|
"milestone raw-buf" internal error) and the sibling
|
||||||
|
synth-path arm (`lib.rs:3296`). These arms are the deferral
|
||||||
|
marker prep.2 left; raw-buf.3 discharges them. They are not a
|
||||||
|
relied-upon current invariant — the milestone's correctness
|
||||||
|
depends on *removing* them, not on their persisting.
|
||||||
|
- Drop for primitive-element RawBuf: a single
|
||||||
|
`@ailang_rc_release` on the slab pointer (no element-walking;
|
||||||
|
elements are primitives).
|
||||||
|
- `ailang-surface` wiring: `parse_raw_buf` + the workspace
|
||||||
|
injection that makes `raw_buf` a kernel-tier auto-imported
|
||||||
|
module (workspace module count 4 → 5).
|
||||||
|
The worked consumer program runs end-to-end and prints `60`.
|
||||||
|
`kernel_stub` stays alongside this iteration (count 5).
|
||||||
|
|
||||||
The ordering is not arbitrary: raw-buf.1 is the only iter with
|
4. **kernel_stub retirement** (raw-buf.4) — Focused removal.
|
||||||
zero behavioural change, so its failure mode is "existing tests
|
RawBuf now subsumes every ratification role kernel_stub held:
|
||||||
break" — the cleanest possible bisection target. raw-buf.2 ships
|
`Term::New` end-to-end (the `(new RawBuf …)` consumer),
|
||||||
the checker-visible surface on an unchanged codegen substrate,
|
`param-in` reject (the Str-element reject fixture), kernel-tier
|
||||||
so its failure mode is checker-isolated. raw-buf.3 lands codegen
|
auto-import (RawBuf visible without `(import raw_buf)`), and the
|
||||||
on a registry that has already absorbed every legacy intercept,
|
`(intrinsic)` mechanism (RawBuf's four ops + their registry
|
||||||
so the RawBuf entries do not co-mingle with a registry move.
|
entries). The stub is therefore pure redundancy. Delete
|
||||||
|
`src/kernel_stub/` + its re-export, drop `parse_kernel_stub` and
|
||||||
|
its surface injection, remove the `answer` `INTERCEPTS` entry +
|
||||||
|
`emit_answer` (its `(intrinsic)` marker leaves with the stub —
|
||||||
|
the bijection lockstep holds), delete the
|
||||||
|
`kernel_stub_module_round_trips` test, re-baseline `workspace_pin`
|
||||||
|
to 4 (raw_buf in, kernel_stub out — net unchanged), and update
|
||||||
|
`design/INDEX.md` + `design/models/0007-kernel-extensions.md`.
|
||||||
|
The `ailang-kernel` crate itself stays as the family-crate home
|
||||||
|
for future kernel-tier modules (series, matrix, …). Isolating
|
||||||
|
the retirement keeps each bijection-registry change (12 entries
|
||||||
|
added in .3, the `answer` entry removed in .4) in its own diff.
|
||||||
|
|
||||||
|
The ordering rationale: .2 is the only zero-behavioural-change
|
||||||
|
iteration (rename), the cleanest bisection target; .3 lands the
|
||||||
|
feature on a registry that has already absorbed every legacy
|
||||||
|
intercept (raw-buf.1) and on the renamed family-crate (raw-buf.2),
|
||||||
|
so the RawBuf manifest+codegen do not co-mingle with a registry
|
||||||
|
move or a crate move; .4 removes the now-redundant stub without
|
||||||
|
touching the new RawBuf code.
|
||||||
|
|
||||||
## Concrete code shapes
|
## Concrete code shapes
|
||||||
|
|
||||||
### Primary — the user-facing program raw-buf delivers
|
### Primary — the raw_buf kernel-tier module (raw-buf.3, gate-verified)
|
||||||
|
|
||||||
|
This is the exact Form-A source the `raw_buf` submodule embeds. It
|
||||||
|
parses and type-checks against the current tool (`ail check` →
|
||||||
|
`ok`); the four `(intrinsic)` markers are legal because the module
|
||||||
|
is `(kernel)`. The element type is restricted to `{Int, Float,
|
||||||
|
Bool}` via `param-in`. `RawBuf.get` returns the bare element type
|
||||||
|
`a`; `set` is linear (`own` in, `own` out).
|
||||||
|
|
||||||
|
```ail
|
||||||
|
(module raw_buf
|
||||||
|
(kernel)
|
||||||
|
(data RawBuf (vars a)
|
||||||
|
(doc "Mutable, indexed, fixed-size flat buffer of primitive elements. Opaque single-ctor handle; codegen intercepts emit raw alloc/load/store over an @ailang_rc_alloc slab. Element type restricted to {Int, Float, Bool} via param-in.")
|
||||||
|
(ctor B a)
|
||||||
|
(param-in (a Int Float Bool)))
|
||||||
|
(fn new
|
||||||
|
(doc "Allocate an uninitialised RawBuf of capacity n. Compiler-supplied (intrinsic) body; codegen intercept new__RawBuf__<T> emits @ailang_rc_alloc plus the i64 size header. Element bytes are uninitialised; caller must set before get.")
|
||||||
|
(type (forall (vars a) (fn-type (params (con Int)) (ret (own (con RawBuf a))))))
|
||||||
|
(params n)
|
||||||
|
(intrinsic))
|
||||||
|
(fn get
|
||||||
|
(doc "Indexed read. UB if i >= (size b); caller checks bounds via size. Compiler-supplied (intrinsic) body; codegen intercept emits getelementptr plus load.")
|
||||||
|
(type (forall (vars a) (fn-type (params (borrow (con RawBuf a)) (con Int)) (ret a))))
|
||||||
|
(params b i)
|
||||||
|
(intrinsic))
|
||||||
|
(fn set
|
||||||
|
(doc "Indexed write. Linear: own in, own out. Under uniqueness in-place; under shared copy-on-write (Issue #22). Compiler-supplied (intrinsic) body; codegen intercept emits getelementptr plus store.")
|
||||||
|
(type (forall (vars a) (fn-type (params (own (con RawBuf a)) (con Int) a) (ret (own (con RawBuf a))))))
|
||||||
|
(params b i v)
|
||||||
|
(intrinsic))
|
||||||
|
(fn size
|
||||||
|
(doc "Element count. Compiler-supplied (intrinsic) body; codegen intercept emits a single i64 load from the slab header.")
|
||||||
|
(type (forall (vars a) (fn-type (params (borrow (con RawBuf a))) (ret (con Int)))))
|
||||||
|
(params b)
|
||||||
|
(intrinsic)))
|
||||||
|
```
|
||||||
|
|
||||||
|
The `(ctor B a)` is a nominal fiction for the type system: it
|
||||||
|
gives `RawBuf` an identity and keeps `a` non-phantom. Real code
|
||||||
|
never constructs it — every operation is codegen-intercepted, and
|
||||||
|
`(new RawBuf …)` desugars to `(app RawBuf.new …)`, not to a
|
||||||
|
`(term-ctor RawBuf B …)`. The four `(intrinsic)` markers carry no
|
||||||
|
runnable body; codegen supplies the implementation via the
|
||||||
|
registry (raw-buf.3).
|
||||||
|
|
||||||
|
### Primary — the worked consumer program (raw-buf.3 acceptance)
|
||||||
|
|
||||||
|
This is the program an LLM author naturally writes for "I need a
|
||||||
|
small mutable indexed buffer to score N values and read them
|
||||||
|
back." It is the feature-acceptance criterion's empirical
|
||||||
|
evidence. It references the `raw_buf` module, which is only
|
||||||
|
injected once raw-buf.3 wires it through `ailang-surface` — so it
|
||||||
|
does **not** check against the current tool (RawBuf is not yet a
|
||||||
|
workspace module). Left unlabeled deliberately: it describes
|
||||||
|
post-raw-buf.3 surface, not current behaviour.
|
||||||
|
|
||||||
```
|
```
|
||||||
(module raw_buf_demo
|
(module raw_buf_demo
|
||||||
(import raw_buf)
|
|
||||||
(fn main
|
(fn main
|
||||||
(type (fn-type (params) (ret (con Int))))
|
(type (fn-type (params) (ret (con Int))))
|
||||||
(params)
|
(params)
|
||||||
@@ -127,109 +227,79 @@ so the RawBuf entries do not co-mingle with a registry move.
|
|||||||
; ail check && ail build && ail run → prints 60
|
; ail check && ail build && ail run → prints 60
|
||||||
```
|
```
|
||||||
|
|
||||||
This is the iter raw-buf.3 acceptance fixture (and the
|
No `(import raw_buf)` needed: `RawBuf` is visible via the
|
||||||
feature-acceptance criterion's empirical evidence — see § Feature
|
kernel-tier auto-import path (prep.3). `RawBuf.set` / `.get`
|
||||||
acceptance below). It is exactly the program an LLM author
|
resolve via type-scoped namespacing (prep.1). `(new RawBuf (con
|
||||||
naturally writes to express "I need a small mutable indexed
|
Int) 3)` is a `Term::New` whose `NewArg::Type` is `(con Int)`; the
|
||||||
buffer to score N values and read them back."
|
raw-buf.3 desugar threads that into `new__RawBuf__Int`.
|
||||||
|
|
||||||
### Primary — the param-in reject fixture
|
### Primary — the param-in reject fixture (raw-buf.3 must-fail)
|
||||||
|
|
||||||
```
|
```
|
||||||
(module raw_buf_reject_string
|
(module raw_buf_reject_str
|
||||||
(import raw_buf)
|
(fn cant_str
|
||||||
(fn main
|
(type (fn-type (params (borrow (con RawBuf (con Str)))) (ret (con Str))))
|
||||||
(type (fn-type (params) (ret (con Unit))))
|
(params buf)
|
||||||
(params)
|
(body (app RawBuf.get buf 0))))
|
||||||
(body (do io/print_str "unreached"))
|
|
||||||
(signature-hole (new RawBuf (con Str) 3)))) ; rejected at check
|
|
||||||
; ail check → param-not-in-restricted-set: type Str not in {Int, Float, Bool}
|
; ail check → param-not-in-restricted-set: type Str not in {Int, Float, Bool}
|
||||||
; at TypeDef raw_buf.RawBuf, var a
|
|
||||||
```
|
```
|
||||||
|
|
||||||
This must fail at the checker, with the diagnostic produced by
|
Must fail at the checker with the `ParamNotInRestrictedSet`
|
||||||
the existing `ParamNotInRestrictedSet` arm shipped in
|
diagnostic shipped in prep.3 (fieldtest F8). It is the must-fail
|
||||||
prep.3 (per fieldtest F8). It is the must-fail evidence that the
|
evidence that the `param-in` restriction is alive on a
|
||||||
`param-in` restriction is alive on a real-payload extension, not
|
real-payload extension, not just the prep.3 `StubT` fixture. Like
|
||||||
just on the prep.3 stub.
|
the worked program, it depends on `raw_buf` being injected, so it
|
||||||
|
is not gate-checkable against the current tool (unlabeled).
|
||||||
|
|
||||||
### Primary — the raw-buf kernel-tier module
|
### Secondary — INTERCEPTS entry shape (raw-buf.3, implementation)
|
||||||
|
|
||||||
```
|
The real registry struct (raw-buf.1) is `Intercept { name,
|
||||||
(module raw_buf
|
expected_params, expected_ret, wants_alwaysinline, emit }`. The 12
|
||||||
(kernel)
|
RawBuf entries follow the existing rows' shape. One representative
|
||||||
(data RawBuf (vars a)
|
(the exact symbol strings are derived by the implementer from the
|
||||||
(ctor B (storage-tag))
|
bijection test, which mangles each `(intrinsic)` marker and
|
||||||
(param-in (a Int Float Bool)))
|
reports the expected name):
|
||||||
|
|
||||||
(fn new
|
|
||||||
(doc "Allocate uninitialised RawBuf of capacity n. Codegen
|
|
||||||
intercept new__RawBuf__<T> emits @ailang_rc_alloc + the
|
|
||||||
size header. Element bytes are uninitialised — caller
|
|
||||||
must (set …) before (get …).")
|
|
||||||
(type (fn-type (params (con Int)) (ret (own (RawBuf a)))))
|
|
||||||
(params n)
|
|
||||||
(body (term-ctor RawBuf B n))) ; placeholder
|
|
||||||
|
|
||||||
(fn get
|
|
||||||
(doc "Indexed read. UB if i >= (size b); caller checks
|
|
||||||
bounds. Codegen intercept RawBuf_get__<T> emits
|
|
||||||
getelementptr + load.")
|
|
||||||
(type (fn-type
|
|
||||||
(params (borrow (RawBuf a)) (con Int))
|
|
||||||
(ret (con a))))
|
|
||||||
(params b i)
|
|
||||||
(body (term-ctor RawBuf B 0))) ; placeholder
|
|
||||||
|
|
||||||
(fn set
|
|
||||||
(doc "Indexed write. Linear: own in, own out. Under
|
|
||||||
uniqueness, in-place; under shared, copy-on-write
|
|
||||||
(Issue #22 territory). Codegen intercept
|
|
||||||
RawBuf_set__<T> emits getelementptr + store.")
|
|
||||||
(type (fn-type
|
|
||||||
(params (own (RawBuf a)) (con Int) (con a))
|
|
||||||
(ret (own (RawBuf a)))))
|
|
||||||
(params b i v)
|
|
||||||
(body b)) ; placeholder
|
|
||||||
|
|
||||||
(fn size
|
|
||||||
(doc "Element count. Codegen intercept RawBuf_size__<T>
|
|
||||||
emits a single i64 load from the slab header.")
|
|
||||||
(type (fn-type (params (borrow (RawBuf a))) (ret (con Int))))
|
|
||||||
(params b)
|
|
||||||
(body 0))) ; placeholder
|
|
||||||
```
|
|
||||||
|
|
||||||
The placeholder bodies are the existing convention from
|
|
||||||
`examples/prelude.ail` (e.g. `eq__Int` ships with `(body x)`
|
|
||||||
that the round-trip preserves but codegen replaces). They exist
|
|
||||||
to satisfy the round-trip invariant; codegen never executes them.
|
|
||||||
|
|
||||||
### Secondary — registry shape (implementation only)
|
|
||||||
|
|
||||||
```rust
|
```rust
|
||||||
// crates/ailang-codegen/src/intercepts.rs (new file)
|
// crates/ailang-codegen/src/intercepts.rs — appended to INTERCEPTS
|
||||||
|
Intercept {
|
||||||
pub struct IntrinsicSig {
|
name: "new__RawBuf__Int", // == mono-mangled name of raw_buf.new @ a=Int
|
||||||
pub params: Vec<String>, // LLVM types as text, e.g. "i64", "ptr"
|
expected_params: &["i64"], // capacity n
|
||||||
pub ret: String,
|
expected_ret: "ptr", // slab base pointer
|
||||||
}
|
wants_alwaysinline: false,
|
||||||
|
emit: emit_new_raw_buf_int, // @ailang_rc_alloc(8 + n*8); store i64 n at offset 0
|
||||||
pub struct Intercept {
|
},
|
||||||
pub name: &'static str,
|
// + new__RawBuf__{Float,Bool}, RawBuf_get__{Int,Float,Bool},
|
||||||
pub sig_check: fn(params: &[String], ret: &str) -> Result<()>,
|
// RawBuf_set__{Int,Float,Bool}, RawBuf_size__{Int,Float,Bool}
|
||||||
pub emit: fn(cg: &mut Lowering) -> Result<()>,
|
|
||||||
}
|
|
||||||
|
|
||||||
pub fn lookup(name: &str) -> Option<&'static Intercept> { ... }
|
|
||||||
|
|
||||||
// Wired into crates/ailang-codegen/src/lib.rs:1321 (the existing
|
|
||||||
// try_emit dispatch site) — that match becomes one lookup call.
|
|
||||||
```
|
```
|
||||||
|
|
||||||
### Secondary — slab layout
|
### Secondary — Term::New desugar (raw-buf.3, implementation)
|
||||||
|
|
||||||
RawBuf payload (post RC header) is:
|
`Term::New { type_name, args }` where `args: Vec<NewArg>`
|
||||||
|
(`NewArg::Type | NewArg::Value`, both already parsed + round-trip
|
||||||
|
ratified). The new desugar pass rewrites it to an application of
|
||||||
|
the type's `new` fn, instantiated at the element type carried by
|
||||||
|
the leading `NewArg::Type`:
|
||||||
|
|
||||||
|
```
|
||||||
|
(new RawBuf (con Int) 3) ; Term::New { type_name: "RawBuf",
|
||||||
|
; args: [Type(con Int), Value(3)] }
|
||||||
|
──desugar──▶
|
||||||
|
(app RawBuf.new 3) @ a = Int ; instantiation pins mono → new__RawBuf__Int
|
||||||
|
```
|
||||||
|
|
||||||
|
The desugar consumes the `NewArg::Type` for the instantiation and
|
||||||
|
passes only the `NewArg::Value` args as call arguments. After this
|
||||||
|
pass no `Term::New` survives into codegen; both deferral arms
|
||||||
|
(`lib.rs:2094` in `lower_term`, "milestone raw-buf" internal
|
||||||
|
error, and the sibling at `lib.rs:3296` in the synth path) become
|
||||||
|
unreachable and are removed. Whether
|
||||||
|
the prep.2 checker already accepts the `NewArg::Type`-bearing
|
||||||
|
`Term::New` semantically, or needs a small extension, is a
|
||||||
|
raw-buf.3 task to verify first (the form parses + round-trips
|
||||||
|
today; the lift pass passes `NewArg::Type` through untouched).
|
||||||
|
|
||||||
|
### Secondary — slab layout (raw-buf.3)
|
||||||
|
|
||||||
```
|
```
|
||||||
[ size : i64 ][ elem_0 ][ elem_1 ] ... [ elem_{size-1} ]
|
[ size : i64 ][ elem_0 ][ elem_1 ] ... [ elem_{size-1} ]
|
||||||
@@ -237,217 +307,177 @@ RawBuf payload (post RC header) is:
|
|||||||
offset 0 offset 8 offset 8 + size*sizeof(T)
|
offset 0 offset 8 offset 8 + size*sizeof(T)
|
||||||
```
|
```
|
||||||
|
|
||||||
Element widths: `Int = 8`, `Float = 8`, `Bool = 1`. Alignment to
|
Element widths: `Int = 8`, `Float = 8`, `Bool = 1`. Header is
|
||||||
8 bytes for header; element payload directly follows. `@ailang_rc_alloc`
|
i64, 8-byte aligned; element payload follows directly.
|
||||||
is called with `8 + size * sizeof(T)` and gets back a `ptr` that
|
`@ailang_rc_alloc` is called with `8 + size * sizeof(T)` and
|
||||||
the codegen treats as the slab base. The size header is *self-
|
returns the slab base `ptr`. The size header is self-describing,
|
||||||
describing* so drop and `RawBuf.size` need no side-table.
|
so drop and `RawBuf.size` need no side-table. Drop is a single
|
||||||
|
`@ailang_rc_release` on the slab pointer — primitive elements
|
||||||
Drop for RawBuf with primitive elements is trivial: a single
|
carry no recursive drops. The per-TypeDef drop generation gets a
|
||||||
`@ailang_rc_release` on the slab pointer. No element-walking
|
"primitive-element-RawBuf" arm dispatched via the same registry.
|
||||||
because element types are primitives (no recursive drops). The
|
|
||||||
existing per-TypeDef drop generation gets a "primitive-element-
|
|
||||||
RawBuf" arm that emits the trivial drop, dispatched via the same
|
|
||||||
registry.
|
|
||||||
|
|
||||||
## Components
|
## Components
|
||||||
|
|
||||||
| Component | Iter | Files |
|
| Component | Iter | Files |
|
||||||
|-----------|------|-------|
|
|-----------|------|-------|
|
||||||
| Intercept registry | raw-buf.1 | new file `crates/ailang-codegen/src/intercepts.rs`; edits to `crates/ailang-codegen/src/lib.rs` at the single dispatch site that today calls `try_emit_primitive_instance_body`, and removal of each absorbed match arm in that fn |
|
| Intercept registry | raw-buf.1 (DONE) | `crates/ailang-codegen/src/intercepts.rs` + dispatch site in `lib.rs` |
|
||||||
| Kernel family-crate (rename + reshape) + RawBuf submodule | raw-buf.2 | rename `crates/ailang-kernel-stub/` → `crates/ailang-kernel/`; restructure as `src/lib.rs` + `src/kernel_stub/{mod.rs, source.ail}` (existing stub re-housed) + `src/raw_buf/{mod.rs, source.ail}` (new); update `Cargo.toml` package name `ailang-kernel-stub` → `ailang-kernel`; update workspace member entry + every dependent crate's `Cargo.toml` (`ailang-surface` is the only consumer today); add `parse_raw_buf` in `crates/ailang-surface/` next to existing `parse_kernel_stub`; extend the workspace injection in `ailang-surface` to inject both modules |
|
| Kernel family-crate rename | raw-buf.2 | `git mv crates/ailang-kernel-stub crates/ailang-kernel`; reshape to `src/lib.rs` + `src/kernel_stub/{mod.rs, source.ail}` (existing stub source incl. `answer` re-housed verbatim); `Cargo.toml` package + workspace member + dep-alias renames; `crates/ailang-surface/Cargo.toml` dep rename + `loader.rs` use-path renames; `design/INDEX.md` + `CLAUDE.md` code-layout row |
|
||||||
| RawBuf intercept entries | raw-buf.3 | additions to `crates/ailang-codegen/src/intercepts.rs` (12 entries); desugar pass `Term::New` → `(app T.new args)` in `crates/ailang-codegen/src/synth.rs` or `crates/ailang-check/src/desugar.rs` |
|
| RawBuf module + codegen + desugar + drop | raw-buf.3 | new `crates/ailang-kernel/src/raw_buf/{mod.rs, source.ail}` + `lib.rs` re-export; `parse_raw_buf` + workspace injection in `crates/ailang-surface/src/loader.rs` + re-export in `lib.rs`; 12 entries + emit fns in `crates/ailang-codegen/src/intercepts.rs`; `Term::New` desugar in `crates/ailang-core/src/desugar.rs` (and removal of the codegen `Term::New` error arm in `crates/ailang-codegen/src/lib.rs`); primitive-element-RawBuf drop arm; `workspace_pin` 4 → 5; round-trip + E2E tests |
|
||||||
| Stub retirement (submodule level) | raw-buf.3 (close) | delete `crates/ailang-kernel/src/kernel_stub/` + its re-export in `src/lib.rs`; drop `parse_kernel_stub` and its surface injection in `ailang-surface` (defn at `crates/ailang-surface/src/loader.rs:54`, re-export at `crates/ailang-surface/src/lib.rs:39`); delete the `kernel_stub_module_round_trips` test at `crates/ailang-core/tests/design_schema_drift.rs:743` (its `parse_kernel_stub` callee is gone — the analogous `raw_buf_module_round_trips` test added in raw-buf.2 carries the round-trip invariant forward); update `crates/ailang-core/tests/workspace_pin.rs` (was bumped to 4 in iter-tidy `a844de3`; raw_buf joins as the stub leaves so the count stays at 4 — see Data flow); update `design/INDEX.md` § Models row + `design/models/0007-kernel-extensions.md` § "ratifying fixture" sentence. The `ailang-kernel` crate itself stays — it is the family-crate that future kernel-tier modules (series, matrix, …) will plug into. |
|
| kernel_stub retirement | raw-buf.4 | delete `crates/ailang-kernel/src/kernel_stub/` + its `lib.rs` re-export; drop `parse_kernel_stub` + injection in `ailang-surface`; remove `answer` entry + `emit_answer` in `intercepts.rs`; delete `kernel_stub_module_round_trips` test; `workspace_pin` 5 → 4; `design/INDEX.md` + `design/models/0007-kernel-extensions.md` updates |
|
||||||
|
|
||||||
## Data flow
|
## Data flow
|
||||||
|
|
||||||
**Build-time** (raw-buf.2 onwards):
|
**Build-time** (raw-buf.3 onwards):
|
||||||
1. CLI loads workspace → `ailang-surface` injects `raw_buf` as
|
1. CLI loads workspace → `ailang-surface` injects `raw_buf` as a
|
||||||
a kernel-tier module (`kernel: true`) just like `prelude`
|
kernel-tier module (`kernel: true`) just like `prelude`.
|
||||||
today.
|
2. `check` walks consumer code; `(con RawBuf (con Int))` resolves
|
||||||
2. `check` walks consumer code; `(con RawBuf (con Int))`
|
to `raw_buf.RawBuf` via the kernel-tier auto-import path
|
||||||
resolves to `raw_buf.RawBuf` via the kernel-tier auto-import
|
(prep.3).
|
||||||
path that prep.3 shipped.
|
3. `param-in` on RawBuf's `a` rejects non-{Int,Float,Bool}
|
||||||
3. `param-in` restriction on RawBuf's `a` parameter rejects
|
instantiations at the consumer typecheck site, using the
|
||||||
non-{Int,Float,Bool} instantiations at the consumer
|
existing `ParamNotInRestrictedSet` diagnostic.
|
||||||
typecheck site, using the existing
|
|
||||||
`ParamNotInRestrictedSet` diagnostic from prep.3.
|
|
||||||
|
|
||||||
**Codegen-time** (raw-buf.3 onwards):
|
**Codegen-time** (raw-buf.3 onwards):
|
||||||
1. Desugar pass replaces every `Term::New {type_name, args}`
|
1. The desugar pass replaces every `Term::New { type_name, args }`
|
||||||
with `Term::App { callee: <type_name>.new, args }` — same
|
with an instantiated `(app <type_name>.new <values>)`, pinning
|
||||||
form that already lowers cleanly today.
|
the element type from the leading `NewArg::Type`.
|
||||||
2. For each fn in the workspace, codegen reaches the dispatch
|
2. For each fn, codegen reaches the registry dispatch site. If the
|
||||||
site at `lib.rs:1321`. If the fn's mono name has a registry
|
fn's mono name resolves via `intercepts::lookup`, the entry's
|
||||||
entry, the entry's `emit` runs; the `.ail` placeholder body
|
`emit` runs; the `(intrinsic)` marker carries no body to fall
|
||||||
is discarded. Otherwise, the normal AILang lowering runs.
|
back to. Otherwise the normal AILang lowering runs.
|
||||||
3. For RawBuf consumers, `new__RawBuf__Int` emits the alloc
|
3. For RawBuf consumers, `new__RawBuf__Int` emits the alloc;
|
||||||
call; `RawBuf_set__Int` emits a `store i64`;
|
`RawBuf_set__Int` a `store i64`; `RawBuf_get__Int` a `load
|
||||||
`RawBuf_get__Int` emits a `load i64`; `RawBuf_size__Int`
|
i64`; `RawBuf_size__Int` a single header load.
|
||||||
emits a single header load.
|
|
||||||
|
|
||||||
**Workspace-module-count interaction** (raw-buf.3 close):
|
**Bijection interaction** (raw-buf.3 / .4):
|
||||||
The current count of 4 (`prelude` + `kernel_stub` + two
|
Each RawBuf `(intrinsic)` marker reachable from the workspace is
|
||||||
test-fixture modules per the iter-tidy commit). When
|
collected by `workspace_intrinsic_markers()` and must resolve to
|
||||||
`kernel_stub` retires and `raw_buf` joins, the count stays 4.
|
an `INTERCEPTS` entry (and vice versa, minus the
|
||||||
If `raw_buf` lands *before* the stub retires, the count is 5
|
`OPTIMISATION_ONLY` allowlist). raw-buf.3 adds 12 markers + 12
|
||||||
mid-iter — caught by the existing `workspace_pin` test, which
|
entries together. raw-buf.4 removes the `answer` marker (with the
|
||||||
the iter explicitly re-baselines.
|
stub) and the `answer` entry together. A half-landed change on
|
||||||
|
either side is a hard unit-test failure
|
||||||
|
(`intercepts_bijection_with_intrinsic_markers`).
|
||||||
|
|
||||||
|
**Workspace module count:** prelude + kernel_stub + 2 test
|
||||||
|
fixtures = 4 today. raw-buf.3 adds raw_buf → 5. raw-buf.4 retires
|
||||||
|
kernel_stub → 4. The `workspace_pin` test pins each transition.
|
||||||
|
|
||||||
## Error handling
|
## Error handling
|
||||||
|
|
||||||
Two diagnostics; both already shipped, no new arms needed in
|
Two consumer-facing diagnostics; both already shipped, no new arms
|
||||||
this milestone:
|
needed:
|
||||||
|
|
||||||
- **`param-not-in-restricted-set`** (prep.3, fieldtest F8).
|
- **`param-not-in-restricted-set`** (prep.3, fieldtest F8). Fires
|
||||||
Fires when a consumer writes `(con RawBuf (con Str))` or
|
when a consumer writes `(con RawBuf (con Str))` or any
|
||||||
any non-{Int,Float,Bool} element. Names the type, the
|
non-{Int,Float,Bool} element. Names the type, the variable, the
|
||||||
variable, the TypeDef, and the restricted set.
|
TypeDef, and the restricted set.
|
||||||
|
- **`new-type-not-constructible`** (prep.3, fieldtest F5). Fires
|
||||||
|
when a consumer writes `(new SomeType …)` and `SomeType` has no
|
||||||
|
`(fn new …)` in its home module. raw_buf ships `(fn new …)`, so
|
||||||
|
the worked program passes; the diagnostic still protects future
|
||||||
|
authors who write `(new Counter 0)` against a `new`-less type.
|
||||||
|
|
||||||
- **`new-type-not-constructible`** (prep.3, fieldtest F5).
|
The codegen `Term::New` deferral arms (`lib.rs:2094` in
|
||||||
Fires when a consumer writes `(new SomeType …)` and
|
`lower_term`, message "… milestone raw-buf"; and the sibling at
|
||||||
`SomeType` has no `(fn new …)` in its home module. Since
|
`lib.rs:3296` in the synth path) are **removed** in raw-buf.3 once
|
||||||
raw-buf ships `(fn new …)` in the kernel-tier `raw_buf`
|
the desugar eliminates `Term::New` before codegen. Neither is a
|
||||||
module, the consumer program above passes — but if a
|
user-facing diagnostic — both are the deferral marker prep.2 left,
|
||||||
future LLM author writes `(new Counter 0)` against a
|
which raw-buf.3 discharges. They have no test pinning them today
|
||||||
type that lacks `new`, this diagnostic still fires
|
(they are an internal `CodegenError::Internal`, not an asserted
|
||||||
precisely.
|
behaviour); raw-buf.3's end-to-end build-and-run E2E (the worked
|
||||||
|
program printing `60`) is the forward ratification — it exercises
|
||||||
|
the `Term::New` → desugar → codegen path that replaces them.
|
||||||
|
|
||||||
Bounds checks are *not* in scope. Per whitepaper § "RawBuf —
|
Bounds checks are **not** in scope (whitepaper § "RawBuf — the
|
||||||
the base extension": `RawBuf.get / .set` are UB if `i >=
|
base extension"): `RawBuf.get/.set` are UB if `i >= size(b)`;
|
||||||
size(b)`; caller checks. Bounds-check insertion is a future
|
caller checks via `RawBuf.size`. Bounds-check insertion is a
|
||||||
axis tracked separately (no backlog item yet — the discipline
|
future axis, no backlog item yet.
|
||||||
is "caller checks via `RawBuf.size`").
|
|
||||||
|
|
||||||
A future `intercept-not-registered` diagnostic surfaces at
|
|
||||||
raw-buf.2 — the iter raw-buf.2 acceptance is precisely that
|
|
||||||
this fires (consumer code checks clean but does not build),
|
|
||||||
demonstrating the manifest/codegen separation works. raw-buf.3
|
|
||||||
makes it stop firing for the 12 RawBuf entries.
|
|
||||||
|
|
||||||
## Testing strategy
|
## Testing strategy
|
||||||
|
|
||||||
Each iter ratified independently:
|
**raw-buf.2 (rename):**
|
||||||
|
- All existing workspace tests pass unchanged — the rename is a
|
||||||
|
pure refactor. Zero test-count change. The crate-rename's
|
||||||
|
failure mode is "the workspace does not build / existing tests
|
||||||
|
break", caught by `cargo build --workspace` + `cargo test
|
||||||
|
--workspace`.
|
||||||
|
|
||||||
**raw-buf.1 (registry refactor):**
|
**raw-buf.3 (RawBuf end-to-end):**
|
||||||
- All ~668 existing workspace tests pass unchanged. The
|
- Round-trip: `raw_buf_module_round_trips` (mirror of
|
||||||
refactor is *primarily* ratified by zero behavioural
|
`kernel_stub_module_round_trips` in `design_schema_drift.rs`) —
|
||||||
change in the existing suite — the legacy intercepts
|
parse → serialise → round-trip; assert `kernel == true`, name
|
||||||
(`eq__Str`, `compare__Int|Bool|Str`, the `float_*` family)
|
`raw_buf`, and `RawBuf` TypeDef `param_in` for `a` contains all
|
||||||
are exercised end-to-end by the following build-and-run
|
of Int/Float/Bool.
|
||||||
E2E tests:
|
- E2E `raw_buf_int_e2e`: the worked consumer program — `ail check
|
||||||
- `eq_primitives_smoke_compiles_and_runs` and
|
&& ail build && ail run` → prints `60`.
|
||||||
`compare_primitives_smoke_prints_1_2_3_thrice` in
|
- E2E `raw_buf_float_e2e` / `raw_buf_bool_e2e`: Float and Bool
|
||||||
`crates/ail/tests/e2e.rs` — pin the `eq__Str` and
|
element variants (Bool catches any i1/i8 packing question).
|
||||||
`compare__Int|Bool|Str` arms (Str path included).
|
- E2E `raw_buf_param_in_reject_e2e`: the Str-element reject
|
||||||
- `float_compare_smoke_prints_true_true_false` in
|
fixture — `ail check` exits non-zero with
|
||||||
`crates/ail/tests/float_compare_smoke_e2e.rs` — pins
|
`param-not-in-restricted-set` in stderr.
|
||||||
the `float_*` family via `float_eq` + `float_lt`.
|
- Drop ratification: a consumer that allocates a RawBuf and lets
|
||||||
- `eq_ord_polymorphic_runs_end_to_end` in
|
it go out of scope without a leak — re-uses the existing
|
||||||
`crates/ail/tests/eq_ord_e2e.rs` — secondary Str-path
|
leak-check harness, no new infra.
|
||||||
ratifier via polymorphic Eq/Ord dispatch.
|
- Bijection: `intercepts_bijection_with_intrinsic_markers` stays
|
||||||
If the registry rewrite breaks any intercept, those tests
|
green with the 12 new markers + 12 new entries (the test forces
|
||||||
catch it.
|
the exact mangled-name match).
|
||||||
- One new unit test in the new `intercepts` module:
|
- `workspace_pin` count assertion 4 → 5 (+ `contains_key("raw_buf")`).
|
||||||
`registry_contains_all_legacy_arms` enumerates the names
|
|
||||||
that were in the legacy match (`eq__Str`, `compare__Int`,
|
|
||||||
`compare__Bool`, `compare__Str`, and each `float_*` name)
|
|
||||||
and asserts each resolves to a registered entry. This pins
|
|
||||||
the migration as complete (a half-finished migration where
|
|
||||||
the old match still has an arm becomes a hard test fail).
|
|
||||||
|
|
||||||
**raw-buf.2 (manifest + checker):**
|
**raw-buf.4 (retirement):**
|
||||||
- New E2E test `crates/ail/tests/raw_buf_check_e2e.rs`:
|
- `workspace_pin` re-baselines 5 → 4 (raw_buf in, kernel_stub
|
||||||
consumer fixture with `(con RawBuf (con Int))` in a type
|
out); `contains_key("kernel_stub")` assertion removed,
|
||||||
signature, `ail check` exits 0.
|
`contains_key("raw_buf")` retained.
|
||||||
- New E2E test `crates/ail/tests/raw_buf_param_in_reject_e2e.rs`:
|
- `kernel_stub_module_round_trips` deleted (its `parse_kernel_stub`
|
||||||
consumer fixture with `(con RawBuf (con Str))`, `ail check`
|
callee is gone; `raw_buf_module_round_trips` carries the
|
||||||
exits non-zero with `param-not-in-restricted-set` in stderr.
|
round-trip invariant forward).
|
||||||
- New E2E test `crates/ail/tests/raw_buf_build_intercept_missing_e2e.rs`:
|
- Bijection stays green after the `answer` marker + entry leave
|
||||||
consumer fixture with `(new RawBuf (con Int) 3)`, `ail
|
together.
|
||||||
build` exits non-zero with `intercept-not-registered` (or
|
- The full suite stays green; the diff is a removal, ratified by
|
||||||
the Term::New deferral message) — pins the manifest/codegen
|
"nothing references the stub and everything still builds".
|
||||||
separation. (This test gets deleted or inverted to PASS in
|
|
||||||
raw-buf.3.)
|
|
||||||
- New round-trip test for the embedded `RAW_BUF_AIL` —
|
|
||||||
parse → print round-trips byte-isomorphically (mirrors
|
|
||||||
`kernel_stub_module_round_trips` in
|
|
||||||
`crates/ailang-core/tests/design_schema_drift.rs`).
|
|
||||||
- Workspace module-count test bumped: 4 → 5 (mid-iter state
|
|
||||||
before stub retires).
|
|
||||||
|
|
||||||
**raw-buf.3 (codegen + stub retirement):**
|
|
||||||
- The intercept-missing E2E test from raw-buf.2 inverted:
|
|
||||||
same consumer fixture, `ail build` now exits 0 and the
|
|
||||||
produced binary, when run, prints `60`.
|
|
||||||
- New E2E `crates/ail/tests/raw_buf_float_e2e.rs`: Float
|
|
||||||
variant exercise.
|
|
||||||
- New E2E `crates/ail/tests/raw_buf_bool_e2e.rs`: Bool
|
|
||||||
variant exercise (catches the i1/i8 packing question
|
|
||||||
if any).
|
|
||||||
- Drop ratification: a consumer that allocates and lets
|
|
||||||
the RawBuf go out of scope without a leak. Re-uses the
|
|
||||||
existing leak-check harness; no new infra.
|
|
||||||
- Stub-retirement ratification: deleted-submodule diff hits
|
|
||||||
`crates/ailang-kernel/src/kernel_stub/` (folder removal) +
|
|
||||||
`crates/ailang-kernel/src/lib.rs` (re-export drop) +
|
|
||||||
`crates/ailang-surface/` (parse_kernel_stub + injection
|
|
||||||
drop) + `crates/ailang-core/tests/workspace_pin.rs` +
|
|
||||||
`design/INDEX.md` + `design/models/0007-kernel-extensions.md`.
|
|
||||||
Test `workspace_pin` re-baselines to 4 (raw_buf in,
|
|
||||||
kernel_stub out — net unchanged). The `ailang-kernel` crate
|
|
||||||
itself stays as the family-crate home for future kernel-tier
|
|
||||||
modules (series, matrix, …).
|
|
||||||
|
|
||||||
## Acceptance criteria
|
## Acceptance criteria
|
||||||
|
|
||||||
The milestone ships when:
|
The milestone ships when:
|
||||||
|
|
||||||
1. The worked consumer program in § Concrete code shapes
|
1. The worked consumer program runs end-to-end: `ail check && ail
|
||||||
end-to-end: `ail check && ail build && ail run` prints
|
build && ail run` prints `60` (raw-buf.3).
|
||||||
`60`.
|
|
||||||
2. The param-in reject fixture exits at `ail check` with the
|
2. The param-in reject fixture exits at `ail check` with the
|
||||||
prep.3 diagnostic.
|
prep.3 `param-not-in-restricted-set` diagnostic (raw-buf.3).
|
||||||
3. Every existing primitive-instance intercept (`eq__Str`,
|
3. RawBuf's four operations are `(intrinsic)` markers, each paired
|
||||||
`compare__Int|Bool|Str`, the `float_*` family) is dispatched
|
with an `INTERCEPTS` entry; `intercepts_bijection_with_intrinsic_markers`
|
||||||
via the registry — *no remaining match-arm* in
|
is green (raw-buf.3).
|
||||||
`try_emit_primitive_instance_body` outside the registry path.
|
4. `Term::New` no longer reaches codegen — the desugar eliminates
|
||||||
4. `ailang-kernel-stub` is retired from the workspace; `raw_buf`
|
it and both deferral arms (`lib.rs:2094` + `lib.rs:3296`) are
|
||||||
takes its slot as the canonical kernel-tier base-extension
|
removed (raw-buf.3).
|
||||||
anchor.
|
5. `ailang-kernel-stub` is renamed to the `ailang-kernel`
|
||||||
5. Workspace test suite green, plus the new tests enumerated
|
family-crate (raw-buf.2); `kernel_stub` is retired and `raw_buf`
|
||||||
in § Testing strategy.
|
takes over its ratification roles (raw-buf.4).
|
||||||
|
6. Workspace test suite green at each iteration boundary, plus the
|
||||||
|
new tests enumerated in § Testing strategy.
|
||||||
|
|
||||||
## Feature-acceptance argument
|
## Feature-acceptance argument
|
||||||
|
|
||||||
Applied per `design/contracts/0004-feature-acceptance.md`:
|
Applied per `design/contracts/0004-feature-acceptance.md`:
|
||||||
|
|
||||||
1. **LLM author reaches for it naturally.** RawBuf is the
|
1. **LLM author reaches for it naturally.** RawBuf is the only
|
||||||
only path to mutable indexed storage in AILang — the
|
path to mutable indexed storage in AILang — the language has no
|
||||||
language has no other "I want to fill N slots and read
|
other "fill N slots and read them back" primitive. The worked
|
||||||
them back" primitive. The worked consumer program above is
|
consumer program above is what an LLM author writes for that
|
||||||
what an LLM author writes when expressing that need;
|
need; there is no alternative shape to reach for.
|
||||||
there is no alternative shape to reach for.
|
|
||||||
|
|
||||||
2. **Measurable improvement.** Embedding-ABI M5 measured
|
2. **Measurable improvement.** Embedding-ABI M5 measured per-tick
|
||||||
per-tick FFI at ~206 ns/tick (~658 ms / 3.19M EURUSD ticks).
|
FFI at ~206 ns/tick (~658 ms / 3.19M EURUSD ticks). RawBuf as
|
||||||
RawBuf as the batch-FFI primitive amortises that per-tick
|
the batch-FFI primitive amortises that per-tick cost across one
|
||||||
cost across one crossing. The series milestone (#8) is also
|
crossing. The Series milestone (#8) is also blocked on RawBuf;
|
||||||
blocked on RawBuf; shipping raw-buf removes that block.
|
shipping raw-buf removes that block.
|
||||||
|
|
||||||
3. **No reintroduced bug class.** Mutation discipline stays
|
3. **No reintroduced bug class.** Mutation discipline stays
|
||||||
mode-tracked (whitepaper § "RawBuf — the base extension"):
|
mode-tracked (whitepaper § "RawBuf — the base extension"):
|
||||||
`RawBuf.set` is `own → own`, not effect-tracked. No
|
`RawBuf.set` is `own → own`, not effect-tracked. No `RawBuf`
|
||||||
`RawBuf` effect declared. Uniqueness inference rewrites it
|
effect is declared. Uniqueness inference rewrites in-place;
|
||||||
in-place; shared ownership falls back to copy-on-write
|
shared ownership falls back to copy-on-write (Issue #22). The
|
||||||
(Issue #22). The pure-core invariant — code without a
|
pure-core invariant survives: code without a declared effect is
|
||||||
declared effect is pure — survives intact. The local-
|
pure. Local reasoning survives: a fn taking `borrow (RawBuf
|
||||||
reasoning invariant survives too: a fn that takes
|
Int)` and returning `Int` is pure from the caller's view,
|
||||||
`borrow (RawBuf Int)` and returns `Int` *is* pure from the
|
because the buffer is not mutated.
|
||||||
caller's view, because the buffer is not mutated.
|
|
||||||
|
|
||||||
The registry-migration aspect of the milestone (raw-buf.1)
|
|
||||||
removes redundancy structurally: the growth point of
|
|
||||||
"every new primitive intercept needs another match arm" is
|
|
||||||
collapsed into a single dispatch table. That is criterion-2
|
|
||||||
evidence for the migration as a piece.
|
|
||||||
|
|||||||
Reference in New Issue
Block a user