spec: raw-buf — re-carve .3/.4/.5, type-scoped polymorphic intrinsic prep (refs #7)
Second re-carve. Planning raw-buf.3 (via plan-recon) surfaced that
RawBuf's ops are a THIRD intrinsic shape the intrinsic-bodies mechanism
never handled: type-scoped polymorphic top-level intrinsics (forall a,
param-in {Int,Float,Bool}, called as RawBuf.get). The existing bijection
+ symbol story covers only monomorphic top-level intrinsics (answer,
float_*) and per-type class-method instances (eq__Int).
The gap (both confirmed in source by recon + grounding-check):
- mono_symbol_n mints <base>__<T> from the bare fn name, so RawBuf.get
@ Int → get__Int — the RawBuf scope never enters the symbol;
new/get/set/size @ Int would collide with any other poly free fn of
those (very common) names.
- the bijection collector's Def::Fn arm records the bare name "get" as
one marker, matching neither the per-type entries nor their symbols;
one polymorphic marker must map to N per-element entries, which the
1-marker-to-1-entry bijection cannot express.
So raw-buf.3 is no longer "add 12 table rows" — it is a new language
mechanism. Re-carve (3 remaining iterations):
raw-buf.3 — type-scoped polymorphic intrinsic mechanism: scope-
qualified mono symbols (RawBuf_get__Int) + bijection-
collector expansion over param-in. Built and ratified
standalone on the stub (a StubT.peek op + its 2 scoped
entries + mono/bijection unit tests), the prep pattern
prep.1/.2/.3 used. No RawBuf, no Term::New dependency.
raw-buf.4 — RawBuf payload (module + 12 scoped entries + drop) +
Term::New desugar ((new RawBuf ...) sugar, removes both
deferral arms). Pure consumer of .3. Worked program → 60.
raw-buf.5 — kernel_stub retirement (peek + answer + stub leave;
RawBuf carries all roles).
Decided design (Option A): scope-qualified symbols, not bare. Rationale
is semantic — the type-scoped call convention RawBuf.get should carry
through to a collision-free, IR-legible symbol; bare get__Int is a
latent collision landmine on the most-reused op names. Removing that
collision class is itself feature-acceptance criterion-3 evidence.
The raw_buf module Form-A in § Concrete code shapes is gate-verified
(ail check → ok, 35 symbols / 3 modules). Grounding-check PASS: all 10
current-behaviour assumptions ratified by named green tests; the
Term::New codegen-deferral (lib.rs ~2096 + ~3298) is the same
about-to-be-deleted prep.2 transient, reported-not-blocked (consistent
with the override logged on 3ec406e).
This commit is contained in:
+349
-303
@@ -1,35 +1,49 @@
|
|||||||
# raw-buf — Design Spec
|
# raw-buf — Design Spec
|
||||||
|
|
||||||
**Date:** 2026-05-29 (revised 2026-05-29)
|
**Date:** 2026-05-29 (revised twice 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
|
> **Revision 1 note (post intrinsic-bodies).** raw-buf.1 (intercept
|
||||||
> (`140a0c0`). This spec was then re-carved because the
|
> registry) shipped (`140a0c0`). The `intrinsic-bodies` milestone
|
||||||
> `intrinsic-bodies` milestone (#9) landed afterwards and removed
|
> (#9) then landed and removed the placeholder-body convention the
|
||||||
> the foundation the original raw-buf.2/.3 split stood on:
|
> original spec relied on — kernel-tier fn bodies are now
|
||||||
|
> typechecked, so `RawBuf.get` cannot ship a type-lying placeholder
|
||||||
|
> body; it must be `(intrinsic)`. And an `(intrinsic)` marker now
|
||||||
|
> requires a matching `INTERCEPTS` entry as a lockstep pair, so a
|
||||||
|
> "manifest-only / codegen-deferred" intermediate state is
|
||||||
|
> forbidden. The kernel-manifest and codegen therefore land
|
||||||
|
> together.
|
||||||
>
|
>
|
||||||
> 1. The **placeholder-body convention** the original spec relied
|
> **Revision 2 note (post raw-buf.2 + plan-recon).** raw-buf.2 (the
|
||||||
> on (`(body x)` round-trip stubs, "the existing convention from
|
> family-crate rename) shipped (`fbdbe74`). Planning raw-buf.3 then
|
||||||
> `examples/prelude.ail`") no longer exists. `prelude.ail` now
|
> surfaced a deeper gap: RawBuf's operations are a *third* intrinsic
|
||||||
> uses `(intrinsic)` markers, and the checker (`check_fn`,
|
> shape the `intrinsic-bodies` mechanism never handled. The bijection
|
||||||
> `crates/ailang-check/src/lib.rs:2173`) typechecks every
|
> + symbol story was built for (a) monomorphic top-level intrinsics
|
||||||
> non-intrinsic body — including kernel-tier bodies. A
|
> (`answer`, `float_*`) and (b) per-type class-method instances
|
||||||
> placeholder body for `RawBuf.get` (declared `(ret a)`, body
|
> (`eq__Int`). RawBuf's ops are **type-scoped polymorphic top-level
|
||||||
> constructing a `RawBuf`) is now a hard type error. `get` (and
|
> intrinsics** (`forall a` with `param-in {Int,Float,Bool}`, called
|
||||||
> `new`/`set`/`size`) MUST be `(intrinsic)`.
|
> as `RawBuf.get`). For that shape:
|
||||||
> 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
|
> 1. `mono_symbol_n` mints `<base>__<T>` from the bare fn name, so
|
||||||
> together in one iteration. The remaining work is re-carved into
|
> `RawBuf.get` @ Int becomes `get__Int` — the `RawBuf` scope never
|
||||||
> three iterations (raw-buf.2/.3/.4) below. The Goal, slab layout,
|
> enters the symbol. `new`/`get`/`set`/`size` @ Int would collide
|
||||||
> and feature-acceptance argument are unchanged.
|
> with any other polymorphic free fn of those (very common) names.
|
||||||
|
> 2. The bijection collector's `Def::Fn` arm records the bare name
|
||||||
|
> `"get"` as one marker — matching neither the per-type entries nor
|
||||||
|
> their symbols. One polymorphic marker must map to N per-element
|
||||||
|
> entries, which the current 1-marker-to-1-entry bijection cannot
|
||||||
|
> express.
|
||||||
|
>
|
||||||
|
> So raw-buf.3 is no longer "add 12 table rows" — it is a new
|
||||||
|
> language mechanism (type-scoped polymorphic intrinsics) that RawBuf
|
||||||
|
> is the first consumer of. The remaining work is re-carved into a
|
||||||
|
> mechanism prep (raw-buf.3), the RawBuf payload (raw-buf.4), and the
|
||||||
|
> stub retirement (raw-buf.5). The decided naming scheme is
|
||||||
|
> scope-qualified mono symbols (`RawBuf_get__Int`); the mechanism is
|
||||||
|
> ratified standalone on the stub (the prep pattern that prep.1/.2/.3
|
||||||
|
> used) before RawBuf consumes it. The Goal, slab layout, and
|
||||||
|
> feature-acceptance argument are unchanged.
|
||||||
|
|
||||||
## Goal
|
## Goal
|
||||||
|
|
||||||
@@ -52,116 +66,140 @@ The milestone also fulfils the architectural commitment from the
|
|||||||
kernel-extensions whitepaper § "Plugin contract": the migration
|
kernel-extensions whitepaper § "Plugin contract": the migration
|
||||||
of the hardcoded primitive-instance intercepts into one registry,
|
of the hardcoded primitive-instance intercepts into one registry,
|
||||||
triggered by the first real base extension shipping. raw-buf.1
|
triggered by the first real base extension shipping. raw-buf.1
|
||||||
already discharged that migration (the registry is live and the
|
already discharged that migration; RawBuf is now the first
|
||||||
`intrinsic-bodies` bijection pin locks marker ↔ entry); RawBuf is
|
*real-payload* consumer of that registry — and the first consumer
|
||||||
now the first *real-payload* consumer of that registry.
|
of the type-scoped polymorphic intrinsic mechanism raw-buf.3 adds.
|
||||||
|
|
||||||
This makes raw-buf both a feature ship (a new type LLM authors
|
|
||||||
can reach for) and the proof that the registry path carries a
|
|
||||||
genuine domain type, not just the migrated primitive intercepts.
|
|
||||||
|
|
||||||
## Architecture
|
## Architecture
|
||||||
|
|
||||||
Four iterations. raw-buf.1 is done; .2/.3/.4 remain.
|
Five iterations. raw-buf.1 and raw-buf.2 are done; .3/.4/.5 remain.
|
||||||
|
|
||||||
1. **Intercept registry** (raw-buf.1) — **DONE** (`140a0c0`).
|
1. **Intercept registry** (raw-buf.1) — **DONE** (`140a0c0`).
|
||||||
Lifted the hard-coded `try_emit_primitive_instance_body` match
|
Lifted the hard-coded `try_emit_primitive_instance_body` match
|
||||||
into the registry table `INTERCEPTS` in
|
into the registry table `INTERCEPTS` in
|
||||||
`crates/ailang-codegen/src/intercepts.rs`; the dispatch site is
|
`crates/ailang-codegen/src/intercepts.rs`; the dispatch site is
|
||||||
a `intercepts::lookup` call. Pure refactor, zero behavioural
|
an `intercepts::lookup` call. (The subsequent `intrinsic-bodies`
|
||||||
change. (The subsequent `intrinsic-bodies` milestone added the
|
milestone added the `(intrinsic)` marker, the `Term::Intrinsic`
|
||||||
`(intrinsic)` marker, the `Term::Intrinsic` leaf, and the
|
leaf, and the marker ↔ entry bijection pin on top of it.)
|
||||||
marker ↔ entry bijection pin on top of this registry.)
|
|
||||||
|
|
||||||
2. **Kernel family-crate rename** (raw-buf.2) — Pure refactor,
|
2. **Kernel family-crate rename** (raw-buf.2) — **DONE**
|
||||||
zero behavioural change. Rename `crates/ailang-kernel-stub/` →
|
(`fbdbe74`). Renamed `crates/ailang-kernel-stub/` →
|
||||||
`crates/ailang-kernel/` and reshape it as a *family-crate*: one
|
`crates/ailang-kernel/`, reshaped as a family-crate
|
||||||
Cargo crate hosting all kernel-tier modules as sibling Rust
|
(`src/lib.rs` hub re-exporting `src/kernel_stub/{mod.rs,
|
||||||
submodules under `src/`, one submodule per `.ail` source. The
|
source.ail}`). Public symbol `STUB_AIL` preserved; zero
|
||||||
renamed crate carries `src/kernel_stub/{mod.rs, source.ail}`
|
behavioural change.
|
||||||
(the existing stub, **verbatim including its current `answer`
|
|
||||||
intrinsic fn** — the source has grown since the original spec
|
|
||||||
was written). `src/lib.rs` re-exports each submodule's `SOURCE`
|
|
||||||
const under the stable name every consumer already binds
|
|
||||||
(`pub use kernel_stub::SOURCE as STUB_AIL;`). The acyclic chain
|
|
||||||
`ailang-surface → ailang-kernel → ailang-core` is preserved;
|
|
||||||
the parse hop `parse_kernel_stub` stays in `ailang-surface`. No
|
|
||||||
`raw_buf` submodule yet — this iteration is *only* the rename,
|
|
||||||
so its failure mode is "existing tests break", the cleanest
|
|
||||||
bisection target. Ratified by the existing suite green.
|
|
||||||
|
|
||||||
3. **RawBuf end-to-end** (raw-buf.3) — The feature ship, landing
|
3. **Type-scoped polymorphic intrinsic mechanism** (raw-buf.3) —
|
||||||
the manifest and the codegen together (the lockstep pair the
|
The new language mechanism RawBuf needs, built and ratified
|
||||||
bijection invariant requires). Adds:
|
standalone on the stub (no RawBuf yet), mirroring how prep.1/.2/.3
|
||||||
|
built kernel-extension mechanisms ratified by the stub. Two
|
||||||
|
coupled pieces:
|
||||||
|
- **Scope-qualified mono symbols.** When a type-scoped call
|
||||||
|
`T.f` (prep.1 spelling) resolves to a polymorphic op `f` of
|
||||||
|
TypeDef `T`, monomorphisation mints `T_f__<elem>` (e.g.
|
||||||
|
`StubT_peek__Int`) — the TypeDef scope is part of the symbol,
|
||||||
|
so two different types' identically-named ops never collide,
|
||||||
|
and the emitted IR is legible (it reads as "the `T.f`
|
||||||
|
specialised to `<elem>`"). The codegen intercept dispatch keys
|
||||||
|
on this scoped symbol.
|
||||||
|
- **Bijection expansion over `param-in`.** The bijection
|
||||||
|
collector (`intercepts::tests::workspace_intrinsic_markers`)
|
||||||
|
gains an arm: a top-level `(intrinsic)` op that is polymorphic
|
||||||
|
and type-scoped to a TypeDef with `param-in (a S1 S2 …)`
|
||||||
|
expands to one marker `T_f__Si` per allowed element type `Si`.
|
||||||
|
One polymorphic marker → N per-element entries, all pinned by
|
||||||
|
`intercepts_bijection_with_intrinsic_markers`.
|
||||||
|
Ratified by adding ONE polymorphic type-scoped `(intrinsic)` op
|
||||||
|
to the stub's `StubT` (`StubT.peek : (borrow (StubT a)) -> a`)
|
||||||
|
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
|
||||||
|
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:
|
||||||
- The `raw_buf` submodule (`src/raw_buf/{mod.rs, source.ail}`)
|
- The `raw_buf` submodule (`src/raw_buf/{mod.rs, source.ail}`)
|
||||||
with the `RawBuf` TypeDef (`param-in (a Int Float Bool)`) and
|
with the `RawBuf` TypeDef (`param-in (a Int Float Bool)`) and
|
||||||
the four operations `new`/`get`/`set`/`size`, each an
|
the four ops `new`/`get`/`set`/`size`, each an `(intrinsic)`
|
||||||
`(intrinsic)` marker (NOT a placeholder body).
|
marker.
|
||||||
- The 12 element-specialised `INTERCEPTS` entries (4 ops × 3
|
- The 12 scope-qualified `INTERCEPTS` entries
|
||||||
element types) lowering each via `@ailang_rc_alloc` +
|
(`RawBuf_{new,get,set,size}__{Int,Float,Bool}`) + emit fns
|
||||||
getelementptr + load/store — no new C code. The entry `name`
|
(`@ailang_rc_alloc` + getelementptr + load/store) — mechanical
|
||||||
of each MUST equal the mono-mangled symbol of its
|
now that raw-buf.3 built the naming + bijection machinery.
|
||||||
`(intrinsic)` marker; the bijection test is the pin that
|
- The `Term::New` desugar `(new T <types…> <values…>)` →
|
||||||
forces this and surfaces the exact expected strings.
|
`(app T.new <values…>)` (general — `(new StubT 42)` benefits
|
||||||
- A desugar pass `(new T <types…> <values…>)` → an instantiated
|
too), removing BOTH codegen `Term::New` deferral arms
|
||||||
`(app T.new <values…>)` that consumes the `NewArg::Type`
|
(`crates/ailang-codegen/src/lib.rs` ~2094 `lower_term` +
|
||||||
element type to drive monomorphisation to `new__RawBuf__<T>`,
|
~3296 synth path) that prep.2 left marked "milestone raw-buf".
|
||||||
so `Term::New` is eliminated before codegen. `Term::New`
|
|
||||||
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
|
- Drop for primitive-element RawBuf: a single
|
||||||
`@ailang_rc_release` on the slab pointer (no element-walking;
|
`@ailang_rc_release` on the slab pointer.
|
||||||
elements are primitives).
|
- `ailang-surface` wiring: `parse_raw_buf` + workspace injection
|
||||||
- `ailang-surface` wiring: `parse_raw_buf` + the workspace
|
(raw_buf kernel-tier auto-imported; workspace count 4 → 5).
|
||||||
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`.
|
The worked consumer program runs end-to-end and prints `60`.
|
||||||
`kernel_stub` stays alongside this iteration (count 5).
|
`kernel_stub` (with `peek` + `answer`) stays alongside (count 5).
|
||||||
|
|
||||||
4. **kernel_stub retirement** (raw-buf.4) — Focused removal.
|
5. **kernel_stub retirement** (raw-buf.5) — RawBuf now subsumes
|
||||||
RawBuf now subsumes every ratification role kernel_stub held:
|
every ratification role the stub held: `Term::New` end-to-end
|
||||||
`Term::New` end-to-end (the `(new RawBuf …)` consumer),
|
(the `(new RawBuf …)` consumer), `param-in` reject (the Str
|
||||||
`param-in` reject (the Str-element reject fixture), kernel-tier
|
reject fixture), kernel-tier auto-import, the monomorphic
|
||||||
auto-import (RawBuf visible without `(import raw_buf)`), and the
|
intrinsic path (RawBuf has no nullary intrinsic, but the path is
|
||||||
`(intrinsic)` mechanism (RawBuf's four ops + their registry
|
exercised by the prelude's `float_*`), and — crucially — the
|
||||||
entries). The stub is therefore pure redundancy. Delete
|
type-scoped polymorphic intrinsic mechanism (RawBuf's four ops).
|
||||||
`src/kernel_stub/` + its re-export, drop `parse_kernel_stub` and
|
Delete `src/kernel_stub/` + its re-export, drop
|
||||||
its surface injection, remove the `answer` `INTERCEPTS` entry +
|
`parse_kernel_stub` + its injection, remove the `answer` and the
|
||||||
`emit_answer` (its `(intrinsic)` marker leaves with the stub —
|
two `StubT_peek__*` `INTERCEPTS` entries + their emit fns (their
|
||||||
the bijection lockstep holds), delete the
|
markers leave with the stub — the bijection lockstep holds),
|
||||||
`kernel_stub_module_round_trips` test, re-baseline `workspace_pin`
|
delete `kernel_stub_module_round_trips`, re-baseline
|
||||||
to 4 (raw_buf in, kernel_stub out — net unchanged), and update
|
`workspace_pin` to 4 (raw_buf in, kernel_stub out), and update
|
||||||
`design/INDEX.md` + `design/models/0007-kernel-extensions.md`.
|
`design/INDEX.md` + `design/models/0007-kernel-extensions.md`.
|
||||||
The `ailang-kernel` crate itself stays as the family-crate home
|
The `ailang-kernel` crate stays as the family-crate home for
|
||||||
for future kernel-tier modules (series, matrix, …). Isolating
|
future kernel-tier modules.
|
||||||
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
|
Ordering rationale: .3 isolates the risky mono+bijection mechanism
|
||||||
iteration (rename), the cleanest bisection target; .3 lands the
|
change (proven on the stub) from RawBuf's payload diff; .4 lands
|
||||||
feature on a registry that has already absorbed every legacy
|
RawBuf as a mechanical consumer plus the orthogonal `(new …)`
|
||||||
intercept (raw-buf.1) and on the renamed family-crate (raw-buf.2),
|
desugar; .5 removes the now-redundant stub without touching the new
|
||||||
so the RawBuf manifest+codegen do not co-mingle with a registry
|
RawBuf code. Each bijection-registry change is isolated to one diff
|
||||||
move or a crate move; .4 removes the now-redundant stub without
|
(peek entries added in .3, 12 RawBuf entries in .4, peek+answer
|
||||||
touching the new RawBuf code.
|
removed in .5).
|
||||||
|
|
||||||
## Concrete code shapes
|
## Concrete code shapes
|
||||||
|
|
||||||
### Primary — the raw_buf kernel-tier module (raw-buf.3, gate-verified)
|
### Primary — the raw-buf.3 mechanism ratifier (StubT.peek)
|
||||||
|
|
||||||
This is the exact Form-A source the `raw_buf` submodule embeds. It
|
raw-buf.3 adds one polymorphic type-scoped `(intrinsic)` op to the
|
||||||
parses and type-checks against the current tool (`ail check` →
|
stub to prove the mechanism. The op and its scope-qualified entries
|
||||||
`ok`); the four `(intrinsic)` markers are legal because the module
|
are the iteration's concrete deliverable (the must-pass evidence
|
||||||
is `(kernel)`. The element type is restricted to `{Int, Float,
|
that scoped symbols + bijection expansion work). The fn is appended
|
||||||
Bool}` via `param-in`. `RawBuf.get` returns the bare element type
|
to the existing `STUB_AIL` source (`crates/ailang-kernel/src/kernel_stub/source.ail`):
|
||||||
`a`; `set` is linear (`own` in, `own` out).
|
|
||||||
|
```text
|
||||||
|
(fn peek
|
||||||
|
(doc "Ratifies the type-scoped polymorphic intrinsic mechanism: StubT.peek is polymorphic over a (param-in {Int,Float}) and type-scoped to StubT. Codegen intercepts StubT_peek__Int / StubT_peek__Float emit a load from the Stub payload. Retires with the stub in raw-buf.5.")
|
||||||
|
(type (forall (vars a) (fn-type (params (borrow (con StubT a))) (ret a))))
|
||||||
|
(params s)
|
||||||
|
(intrinsic))
|
||||||
|
```
|
||||||
|
|
||||||
|
(Shown `text`, not `ail`: `kernel_stub` is a reserved built-in
|
||||||
|
module name, so the source cannot be `ail check`-ed standalone —
|
||||||
|
`reserved-module-name`. Ratification is the round-trip test + the
|
||||||
|
bijection/mono unit tests, not a standalone parse.) Its two
|
||||||
|
scope-qualified entries (`StubT_peek__Int`, `StubT_peek__Float`)
|
||||||
|
land in `INTERCEPTS` together with the bijection-collector
|
||||||
|
extension; the bijection test pins the 1-marker→2-entries mapping.
|
||||||
|
|
||||||
|
### Primary — the raw_buf kernel-tier module (raw-buf.4, gate-verified)
|
||||||
|
|
||||||
|
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)`. `RawBuf.get` returns the bare element type `a`; `set`
|
||||||
|
is linear (`own` in, `own` out).
|
||||||
|
|
||||||
```ail
|
```ail
|
||||||
(module raw_buf
|
(module raw_buf
|
||||||
@@ -171,22 +209,22 @@ Bool}` via `param-in`. `RawBuf.get` returns the bare element type
|
|||||||
(ctor B a)
|
(ctor B a)
|
||||||
(param-in (a Int Float Bool)))
|
(param-in (a Int Float Bool)))
|
||||||
(fn new
|
(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.")
|
(doc "Allocate an uninitialised RawBuf of capacity n. Compiler-supplied (intrinsic) body; codegen intercept RawBuf_new__<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))))))
|
(type (forall (vars a) (fn-type (params (con Int)) (ret (own (con RawBuf a))))))
|
||||||
(params n)
|
(params n)
|
||||||
(intrinsic))
|
(intrinsic))
|
||||||
(fn get
|
(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.")
|
(doc "Indexed read. UB if i >= (size b); caller checks bounds via size. Compiler-supplied (intrinsic) body; codegen intercept RawBuf_get__<T> emits getelementptr plus load.")
|
||||||
(type (forall (vars a) (fn-type (params (borrow (con RawBuf a)) (con Int)) (ret a))))
|
(type (forall (vars a) (fn-type (params (borrow (con RawBuf a)) (con Int)) (ret a))))
|
||||||
(params b i)
|
(params b i)
|
||||||
(intrinsic))
|
(intrinsic))
|
||||||
(fn set
|
(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.")
|
(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 RawBuf_set__<T> emits getelementptr plus store.")
|
||||||
(type (forall (vars a) (fn-type (params (own (con RawBuf a)) (con Int) a) (ret (own (con RawBuf a))))))
|
(type (forall (vars a) (fn-type (params (own (con RawBuf a)) (con Int) a) (ret (own (con RawBuf a))))))
|
||||||
(params b i v)
|
(params b i v)
|
||||||
(intrinsic))
|
(intrinsic))
|
||||||
(fn size
|
(fn size
|
||||||
(doc "Element count. Compiler-supplied (intrinsic) body; codegen intercept emits a single i64 load from the slab header.")
|
(doc "Element count. Compiler-supplied (intrinsic) body; codegen intercept RawBuf_size__<T> emits a single i64 load from the slab header.")
|
||||||
(type (forall (vars a) (fn-type (params (borrow (con RawBuf a))) (ret (con Int)))))
|
(type (forall (vars a) (fn-type (params (borrow (con RawBuf a))) (ret (con Int)))))
|
||||||
(params b)
|
(params b)
|
||||||
(intrinsic)))
|
(intrinsic)))
|
||||||
@@ -196,20 +234,18 @@ The `(ctor B a)` is a nominal fiction for the type system: it
|
|||||||
gives `RawBuf` an identity and keeps `a` non-phantom. Real code
|
gives `RawBuf` an identity and keeps `a` non-phantom. Real code
|
||||||
never constructs it — every operation is codegen-intercepted, and
|
never constructs it — every operation is codegen-intercepted, and
|
||||||
`(new RawBuf …)` desugars to `(app RawBuf.new …)`, not to a
|
`(new RawBuf …)` desugars to `(app RawBuf.new …)`, not to a
|
||||||
`(term-ctor RawBuf B …)`. The four `(intrinsic)` markers carry no
|
`(term-ctor RawBuf B …)`.
|
||||||
runnable body; codegen supplies the implementation via the
|
|
||||||
registry (raw-buf.3).
|
|
||||||
|
|
||||||
### Primary — the worked consumer program (raw-buf.3 acceptance)
|
### Primary — the worked consumer program (raw-buf.4 acceptance)
|
||||||
|
|
||||||
This is the program an LLM author naturally writes for "I need a
|
The program an LLM author naturally writes for "I need a small
|
||||||
small mutable indexed buffer to score N values and read them
|
mutable indexed buffer to score N values and read them back." It is
|
||||||
back." It is the feature-acceptance criterion's empirical
|
the feature-acceptance criterion's empirical evidence. It uses the
|
||||||
evidence. It references the `raw_buf` module, which is only
|
`(new RawBuf …)` construction sugar (available once raw-buf.4 lands
|
||||||
injected once raw-buf.3 wires it through `ailang-surface` — so it
|
the Term::New desugar). It references the `raw_buf` module, injected
|
||||||
does **not** check against the current tool (RawBuf is not yet a
|
only from raw-buf.4 — so it does **not** check against the current
|
||||||
workspace module). Left unlabeled deliberately: it describes
|
tool (RawBuf is not yet a workspace module). Left unlabeled
|
||||||
post-raw-buf.3 surface, not current behaviour.
|
deliberately: it describes post-raw-buf.4 surface.
|
||||||
|
|
||||||
```
|
```
|
||||||
(module raw_buf_demo
|
(module raw_buf_demo
|
||||||
@@ -227,13 +263,18 @@ post-raw-buf.3 surface, not current behaviour.
|
|||||||
; ail check && ail build && ail run → prints 60
|
; ail check && ail build && ail run → prints 60
|
||||||
```
|
```
|
||||||
|
|
||||||
No `(import raw_buf)` needed: `RawBuf` is visible via the
|
No `(import raw_buf)` needed: `RawBuf` is visible via kernel-tier
|
||||||
kernel-tier auto-import path (prep.3). `RawBuf.set` / `.get`
|
auto-import (prep.3). `RawBuf.set`/`.get`/`.new` resolve via
|
||||||
resolve via type-scoped namespacing (prep.1). `(new RawBuf (con
|
type-scoped namespacing (prep.1) and mono to the scope-qualified
|
||||||
Int) 3)` is a `Term::New` whose `NewArg::Type` is `(con Int)`; the
|
symbols `RawBuf_set__Int` / `RawBuf_get__Int` / `RawBuf_new__Int`.
|
||||||
raw-buf.3 desugar threads that into `new__RawBuf__Int`.
|
The element type `a = Int` is fixed by inference: it flows from the
|
||||||
|
`(app RawBuf.set buf 0 10)` value arg (`10 : Int`) through the
|
||||||
|
linear `own (RawBuf a)` threading. (For the direct-call equivalent
|
||||||
|
without the `(new …)` sugar — `(let buf (app RawBuf.new 3) …)` —
|
||||||
|
the same inference applies; the desugar reduces `(new RawBuf (con
|
||||||
|
Int) 3)` to exactly that.)
|
||||||
|
|
||||||
### Primary — the param-in reject fixture (raw-buf.3 must-fail)
|
### Primary — the param-in reject fixture (raw-buf.4 must-fail)
|
||||||
|
|
||||||
```
|
```
|
||||||
(module raw_buf_reject_str
|
(module raw_buf_reject_str
|
||||||
@@ -245,61 +286,78 @@ raw-buf.3 desugar threads that into `new__RawBuf__Int`.
|
|||||||
```
|
```
|
||||||
|
|
||||||
Must fail at the checker with the `ParamNotInRestrictedSet`
|
Must fail at the checker with the `ParamNotInRestrictedSet`
|
||||||
diagnostic shipped in prep.3 (fieldtest F8). It is the must-fail
|
diagnostic shipped in prep.3 (fieldtest F8) — the must-fail evidence
|
||||||
evidence that the `param-in` restriction is alive on a
|
that `param-in` is alive on a real-payload extension. Depends on
|
||||||
real-payload extension, not just the prep.3 `StubT` fixture. Like
|
`raw_buf` being injected, so not gate-checkable today (unlabeled).
|
||||||
the worked program, it depends on `raw_buf` being injected, so it
|
|
||||||
is not gate-checkable against the current tool (unlabeled).
|
|
||||||
|
|
||||||
### Secondary — INTERCEPTS entry shape (raw-buf.3, implementation)
|
### Secondary — scope-qualified mono symbol (raw-buf.3, implementation)
|
||||||
|
|
||||||
The real registry struct (raw-buf.1) is `Intercept { name,
|
Current behaviour: `mono_symbol_n(base, types)`
|
||||||
expected_params, expected_ret, wants_alwaysinline, emit }`. The 12
|
(`crates/ailang-check/src/mono.rs:521`) joins `base` and each
|
||||||
RawBuf entries follow the existing rows' shape. One representative
|
type's mono suffix with `__`. For a bare-named poly free fn `get`
|
||||||
(the exact symbol strings are derived by the implementer from the
|
it yields `get__Int` — no type scope. The bijection collector's
|
||||||
bijection test, which mangles each `(intrinsic)` marker and
|
`Def::Fn` arm (`intercepts.rs` ~490) inserts the bare `f.name`.
|
||||||
reports the expected name):
|
|
||||||
|
raw-buf.3 change (shape — exact threading mapped by plan-recon):
|
||||||
|
a type-scoped call `T.f` carries the resolved TypeDef `T`; mono
|
||||||
|
uses a scope-qualified base `T_f` so the symbol is `T_f__<elem>`
|
||||||
|
(`StubT_peek__Int`, later `RawBuf_get__Int`). The bijection
|
||||||
|
collector gains an arm that, for a polymorphic top-level
|
||||||
|
`(intrinsic)` op scoped to a TypeDef with `param-in (a S1 …)`,
|
||||||
|
emits `T_f__Si` for each `Si`. Both the mono mint and the collector
|
||||||
|
must compute the identical string (the bijection test is the pin).
|
||||||
|
|
||||||
|
### Secondary — INTERCEPTS entry shape (raw-buf.4, implementation)
|
||||||
|
|
||||||
|
The registry struct (raw-buf.1) is `Intercept { name,
|
||||||
|
expected_params, expected_ret, wants_alwaysinline, emit }`. One
|
||||||
|
representative of the 12 RawBuf entries (the exact symbol strings
|
||||||
|
are produced by the raw-buf.3 mechanism and pinned by the bijection
|
||||||
|
test):
|
||||||
|
|
||||||
```rust
|
```rust
|
||||||
// crates/ailang-codegen/src/intercepts.rs — appended to INTERCEPTS
|
// crates/ailang-codegen/src/intercepts.rs — appended to INTERCEPTS
|
||||||
Intercept {
|
Intercept {
|
||||||
name: "new__RawBuf__Int", // == mono-mangled name of raw_buf.new @ a=Int
|
name: "RawBuf_new__Int", // scope-qualified mono symbol of RawBuf.new @ Int
|
||||||
expected_params: &["i64"], // capacity n
|
expected_params: &["i64"], // capacity n
|
||||||
expected_ret: "ptr", // slab base pointer
|
expected_ret: "ptr", // slab base pointer
|
||||||
wants_alwaysinline: false,
|
wants_alwaysinline: false,
|
||||||
emit: emit_new_raw_buf_int, // @ailang_rc_alloc(8 + n*8); store i64 n at offset 0
|
emit: emit_rawbuf_new_int, // @ailang_rc_alloc(8 + n*8); store i64 n at offset 0
|
||||||
},
|
},
|
||||||
// + new__RawBuf__{Float,Bool}, RawBuf_get__{Int,Float,Bool},
|
// + RawBuf_new__{Float,Bool}, RawBuf_get__{Int,Float,Bool},
|
||||||
// RawBuf_set__{Int,Float,Bool}, RawBuf_size__{Int,Float,Bool}
|
// RawBuf_set__{Int,Float,Bool}, RawBuf_size__{Int,Float,Bool}
|
||||||
```
|
```
|
||||||
|
|
||||||
### Secondary — Term::New desugar (raw-buf.3, implementation)
|
### Secondary — Term::New desugar (raw-buf.4, implementation)
|
||||||
|
|
||||||
`Term::New { type_name, args }` where `args: Vec<NewArg>`
|
`Term::New { type_name, args }` with `args: Vec<NewArg>`
|
||||||
(`NewArg::Type | NewArg::Value`, both already parsed + round-trip
|
(`NewArg::Type | NewArg::Value`, both parsed + round-trip ratified).
|
||||||
ratified). The new desugar pass rewrites it to an application of
|
The desugar rewrites it to an application of the type's `new` fn,
|
||||||
the type's `new` fn, instantiated at the element type carried by
|
passing only the `NewArg::Value` args:
|
||||||
the leading `NewArg::Type`:
|
|
||||||
|
|
||||||
```
|
```
|
||||||
(new RawBuf (con Int) 3) ; Term::New { type_name: "RawBuf",
|
(new RawBuf (con Int) 3) ; Term::New { type_name: "RawBuf",
|
||||||
; args: [Type(con Int), Value(3)] }
|
; args: [Type(con Int), Value(3)] }
|
||||||
──desugar──▶
|
──desugar──▶
|
||||||
(app RawBuf.new 3) @ a = Int ; instantiation pins mono → new__RawBuf__Int
|
(app RawBuf.new 3) ; a = Int resolved by inference from use
|
||||||
```
|
```
|
||||||
|
|
||||||
The desugar consumes the `NewArg::Type` for the instantiation and
|
Important: the AST has no type-ascription term and `Term::App`
|
||||||
passes only the `NewArg::Value` args as call arguments. After this
|
carries no type-args, so the desugar **drops** the `NewArg::Type`
|
||||||
pass no `Term::New` survives into codegen; both deferral arms
|
and the element type is recovered by ordinary inference (it flows
|
||||||
(`lib.rs:2094` in `lower_term`, "milestone raw-buf" internal
|
from how the result is used — see the worked program). This
|
||||||
error, and the sibling at `lib.rs:3296` in the synth path) become
|
suffices for every real program that uses the buffer; an isolated
|
||||||
unreachable and are removed. Whether
|
`(new RawBuf (con Int) 3)` with no constraining use would leave `a`
|
||||||
the prep.2 checker already accepts the `NewArg::Type`-bearing
|
ambiguous, which is acceptable (no real program does that). After
|
||||||
`Term::New` semantically, or needs a small extension, is a
|
this pass no `Term::New` survives into codegen; both deferral arms
|
||||||
raw-buf.3 task to verify first (the form parses + round-trips
|
(`lib.rs` ~2094 `lower_term`, ~3296 synth) are removed. The prep.2
|
||||||
today; the lift pass passes `NewArg::Type` through untouched).
|
checker already accepts `Term::New` (it parses, round-trips, and
|
||||||
|
typechecks via the `new` def's signature); whether it needs any
|
||||||
|
extension for the `NewArg::Type`-bearing form is a raw-buf.4
|
||||||
|
verify-first task (plan-recon maps the current Term::New typecheck
|
||||||
|
path).
|
||||||
|
|
||||||
### Secondary — slab layout (raw-buf.3)
|
### Secondary — slab layout (raw-buf.4)
|
||||||
|
|
||||||
```
|
```
|
||||||
[ size : i64 ][ elem_0 ][ elem_1 ] ... [ elem_{size-1} ]
|
[ size : i64 ][ elem_0 ][ elem_1 ] ... [ elem_{size-1} ]
|
||||||
@@ -307,177 +365,165 @@ today; the lift pass passes `NewArg::Type` through untouched).
|
|||||||
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`. Header is
|
Element widths: `Int = 8`, `Float = 8`, `Bool = 1`. Header is i64,
|
||||||
i64, 8-byte aligned; element payload follows directly.
|
8-byte aligned; element payload follows directly. `@ailang_rc_alloc`
|
||||||
`@ailang_rc_alloc` is called with `8 + size * sizeof(T)` and
|
is called with `8 + size * sizeof(T)` and returns the slab base
|
||||||
returns the slab base `ptr`. The size header is self-describing,
|
`ptr`. The size header is self-describing, so drop and `RawBuf.size`
|
||||||
so drop and `RawBuf.size` need no side-table. Drop is a single
|
need no side-table. Drop is a single `@ailang_rc_release` on the
|
||||||
`@ailang_rc_release` on the slab pointer — primitive elements
|
slab pointer — primitive elements carry no recursive drops; the
|
||||||
carry no recursive drops. The per-TypeDef drop generation gets a
|
per-TypeDef drop generation gets a "primitive-element-RawBuf" arm.
|
||||||
"primitive-element-RawBuf" arm dispatched via the same registry.
|
|
||||||
|
|
||||||
## Components
|
## Components
|
||||||
|
|
||||||
| Component | Iter | Files |
|
| Component | Iter | Files |
|
||||||
|-----------|------|-------|
|
|-----------|------|-------|
|
||||||
| Intercept registry | raw-buf.1 (DONE) | `crates/ailang-codegen/src/intercepts.rs` + dispatch site in `lib.rs` |
|
| Intercept registry | raw-buf.1 (DONE) | `crates/ailang-codegen/src/intercepts.rs` + dispatch in `lib.rs` |
|
||||||
| 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 |
|
| Kernel family-crate rename | raw-buf.2 (DONE) | `crates/ailang-kernel/` (renamed); `ailang-surface` dep + `loader.rs`; doc/ledger rows |
|
||||||
| 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 |
|
| 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 |
|
||||||
| 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 |
|
| 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` |
|
||||||
|
|
||||||
## Data flow
|
## Data flow
|
||||||
|
|
||||||
**Build-time** (raw-buf.3 onwards):
|
**Mechanism (raw-buf.3):**
|
||||||
|
1. A consumer call `T.f` (type-scoped spelling, prep.1) resolves to
|
||||||
|
the polymorphic op `f` of TypeDef `T`, recording `T` as the
|
||||||
|
resolution scope.
|
||||||
|
2. Monomorphisation at element type `Si` mints the scope-qualified
|
||||||
|
symbol `T_f__Si`; codegen emits a fn of that name; the intercept
|
||||||
|
dispatch keys on it.
|
||||||
|
3. The bijection collector expands each polymorphic type-scoped
|
||||||
|
`(intrinsic)` op over its TypeDef's `param-in` set into the same
|
||||||
|
`T_f__Si` strings, and requires each to resolve to an `INTERCEPTS`
|
||||||
|
entry (and vice versa, minus `OPTIMISATION_ONLY`).
|
||||||
|
|
||||||
|
**Build-time (raw-buf.4 onwards):**
|
||||||
1. CLI loads workspace → `ailang-surface` injects `raw_buf` as a
|
1. CLI loads workspace → `ailang-surface` injects `raw_buf` as a
|
||||||
kernel-tier module (`kernel: true`) just like `prelude`.
|
kernel-tier module (`kernel: true`).
|
||||||
2. `check` walks consumer code; `(con RawBuf (con Int))` resolves
|
2. `check` walks consumer code; `(con RawBuf (con Int))` resolves
|
||||||
to `raw_buf.RawBuf` via the kernel-tier auto-import path
|
to `raw_buf.RawBuf` via kernel-tier auto-import (prep.3).
|
||||||
(prep.3).
|
3. `param-in` on `a` rejects non-{Int,Float,Bool} instantiations
|
||||||
3. `param-in` on RawBuf's `a` rejects non-{Int,Float,Bool}
|
via the existing `ParamNotInRestrictedSet` diagnostic.
|
||||||
instantiations at the consumer typecheck site, using the
|
|
||||||
existing `ParamNotInRestrictedSet` diagnostic.
|
|
||||||
|
|
||||||
**Codegen-time** (raw-buf.3 onwards):
|
**Codegen-time (raw-buf.4 onwards):**
|
||||||
1. The desugar pass replaces every `Term::New { type_name, args }`
|
1. The desugar replaces every `Term::New` with `(app T.new
|
||||||
with an instantiated `(app <type_name>.new <values>)`, pinning
|
<values>)`; the element type is inferred from use.
|
||||||
the element type from the leading `NewArg::Type`.
|
2. Codegen reaches the registry dispatch site; if the fn's
|
||||||
2. For each fn, codegen reaches the registry dispatch site. If the
|
scope-qualified mono symbol resolves via `intercepts::lookup`,
|
||||||
fn's mono name resolves via `intercepts::lookup`, the entry's
|
the entry's `emit` runs (the `(intrinsic)` marker has no body).
|
||||||
`emit` runs; the `(intrinsic)` marker carries no body to fall
|
3. `RawBuf_new__Int` emits the alloc; `RawBuf_set__Int` a `store
|
||||||
back to. Otherwise the normal AILang lowering runs.
|
i64`; `RawBuf_get__Int` a `load i64`; `RawBuf_size__Int` a header
|
||||||
3. For RawBuf consumers, `new__RawBuf__Int` emits the alloc;
|
load.
|
||||||
`RawBuf_set__Int` a `store i64`; `RawBuf_get__Int` a `load
|
|
||||||
i64`; `RawBuf_size__Int` a single header load.
|
|
||||||
|
|
||||||
**Bijection interaction** (raw-buf.3 / .4):
|
**Workspace module count:** prelude + kernel_stub + 2 test fixtures
|
||||||
Each RawBuf `(intrinsic)` marker reachable from the workspace is
|
= 4 today. raw-buf.4 adds raw_buf → 5. raw-buf.5 retires kernel_stub
|
||||||
collected by `workspace_intrinsic_markers()` and must resolve to
|
→ 4. The `workspace_pin` test pins each transition.
|
||||||
an `INTERCEPTS` entry (and vice versa, minus the
|
|
||||||
`OPTIMISATION_ONLY` allowlist). raw-buf.3 adds 12 markers + 12
|
|
||||||
entries together. raw-buf.4 removes the `answer` marker (with the
|
|
||||||
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 consumer-facing diagnostics; both already shipped, no new arms
|
Two consumer-facing diagnostics; both already shipped, no new arms:
|
||||||
needed:
|
|
||||||
|
|
||||||
- **`param-not-in-restricted-set`** (prep.3, fieldtest F8). Fires
|
- **`param-not-in-restricted-set`** (prep.3, fieldtest F8) — fires
|
||||||
when a consumer writes `(con RawBuf (con Str))` or any
|
on `(con RawBuf (con Str))` or any non-{Int,Float,Bool} element.
|
||||||
non-{Int,Float,Bool} element. Names the type, the variable, the
|
- **`new-type-not-constructible`** (prep.3, fieldtest F5) — fires on
|
||||||
TypeDef, and the restricted set.
|
`(new SomeType …)` when `SomeType` has no `(fn new …)`. raw_buf
|
||||||
- **`new-type-not-constructible`** (prep.3, fieldtest F5). Fires
|
ships `new`, so the worked program passes.
|
||||||
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.
|
|
||||||
|
|
||||||
The codegen `Term::New` deferral arms (`lib.rs:2094` in
|
The codegen `Term::New` deferral arms (`lib.rs` ~2094 + ~3296,
|
||||||
`lower_term`, message "… milestone raw-buf"; and the sibling at
|
message "… milestone raw-buf") are **removed** in raw-buf.4 once the
|
||||||
`lib.rs:3296` in the synth path) are **removed** in raw-buf.3 once
|
desugar eliminates `Term::New` before codegen. Neither is
|
||||||
the desugar eliminates `Term::New` before codegen. Neither is a
|
user-facing — both are the prep.2 deferral marker. They have no test
|
||||||
user-facing diagnostic — both are the deferral marker prep.2 left,
|
pinning them today (internal `CodegenError::Internal`); raw-buf.4's
|
||||||
which raw-buf.3 discharges. They have no test pinning them today
|
build-and-run E2E (the worked program printing `60`) is the forward
|
||||||
(they are an internal `CodegenError::Internal`, not an asserted
|
ratification.
|
||||||
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 (whitepaper § "RawBuf — the
|
Bounds checks are **not** in scope: `RawBuf.get/.set` are UB if `i
|
||||||
base extension"): `RawBuf.get/.set` are UB if `i >= size(b)`;
|
>= size(b)`; caller checks via `RawBuf.size`. A future axis, no
|
||||||
caller checks via `RawBuf.size`. Bounds-check insertion is a
|
backlog item yet.
|
||||||
future axis, no backlog item yet.
|
|
||||||
|
|
||||||
## Testing strategy
|
## Testing strategy
|
||||||
|
|
||||||
**raw-buf.2 (rename):**
|
**raw-buf.3 (mechanism):**
|
||||||
- All existing workspace tests pass unchanged — the rename is a
|
- Mono unit test: a type-scoped poly intrinsic op mints the
|
||||||
pure refactor. Zero test-count change. The crate-rename's
|
scope-qualified symbol (`StubT_peek__Int`, `StubT_peek__Float`) —
|
||||||
failure mode is "the workspace does not build / existing tests
|
asserts the new mangling directly, no running program needed.
|
||||||
break", caught by `cargo build --workspace` + `cargo test
|
|
||||||
--workspace`.
|
|
||||||
|
|
||||||
**raw-buf.3 (RawBuf end-to-end):**
|
|
||||||
- Round-trip: `raw_buf_module_round_trips` (mirror of
|
|
||||||
`kernel_stub_module_round_trips` in `design_schema_drift.rs`) —
|
|
||||||
parse → serialise → round-trip; assert `kernel == true`, name
|
|
||||||
`raw_buf`, and `RawBuf` TypeDef `param_in` for `a` contains all
|
|
||||||
of Int/Float/Bool.
|
|
||||||
- E2E `raw_buf_int_e2e`: the worked consumer program — `ail check
|
|
||||||
&& ail build && ail run` → prints `60`.
|
|
||||||
- E2E `raw_buf_float_e2e` / `raw_buf_bool_e2e`: Float and Bool
|
|
||||||
element variants (Bool catches any i1/i8 packing question).
|
|
||||||
- E2E `raw_buf_param_in_reject_e2e`: the Str-element reject
|
|
||||||
fixture — `ail check` exits non-zero with
|
|
||||||
`param-not-in-restricted-set` in stderr.
|
|
||||||
- Drop ratification: a consumer that allocates a RawBuf and lets
|
|
||||||
it go out of scope without a leak — re-uses the existing
|
|
||||||
leak-check harness, no new infra.
|
|
||||||
- Bijection: `intercepts_bijection_with_intrinsic_markers` stays
|
- Bijection: `intercepts_bijection_with_intrinsic_markers` stays
|
||||||
green with the 12 new markers + 12 new entries (the test forces
|
green with the `peek` marker expanded to its 2 scope-qualified
|
||||||
the exact mangled-name match).
|
entries (proves the 1-marker→N-entries expansion).
|
||||||
- `workspace_pin` count assertion 4 → 5 (+ `contains_key("raw_buf")`).
|
- `kernel_stub_module_round_trips` updated for the added `peek` fn
|
||||||
|
(parse → serialise → round-trip holds).
|
||||||
|
- Full suite green; no workspace-count change (peek is added to the
|
||||||
|
existing stub, no new module).
|
||||||
|
|
||||||
**raw-buf.4 (retirement):**
|
**raw-buf.4 (RawBuf payload + desugar):**
|
||||||
- `workspace_pin` re-baselines 5 → 4 (raw_buf in, kernel_stub
|
- Round-trip `raw_buf_module_round_trips` (mirror
|
||||||
out); `contains_key("kernel_stub")` assertion removed,
|
`kernel_stub_module_round_trips`): assert `kernel == true`, name
|
||||||
`contains_key("raw_buf")` retained.
|
`raw_buf`, `RawBuf` TypeDef `param_in` for `a` contains
|
||||||
- `kernel_stub_module_round_trips` deleted (its `parse_kernel_stub`
|
Int/Float/Bool.
|
||||||
callee is gone; `raw_buf_module_round_trips` carries the
|
- E2E `raw_buf_int_e2e`: the worked program — `ail check && ail
|
||||||
round-trip invariant forward).
|
build && ail run` → prints `60`.
|
||||||
- Bijection stays green after the `answer` marker + entry leave
|
- E2E `raw_buf_float_e2e` / `raw_buf_bool_e2e`: Float and Bool
|
||||||
together.
|
variants (Bool catches any i1/i8 packing question).
|
||||||
- The full suite stays green; the diff is a removal, ratified by
|
- E2E `raw_buf_param_in_reject_e2e`: the Str reject fixture — `ail
|
||||||
"nothing references the stub and everything still builds".
|
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).
|
||||||
|
- Bijection green with the 12 RawBuf entries added.
|
||||||
|
- `workspace_pin` count 4 → 5 (+ `contains_key("raw_buf")`).
|
||||||
|
|
||||||
|
**raw-buf.5 (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.
|
||||||
|
- Bijection green after `answer` + `StubT_peek__*` markers + entries
|
||||||
|
leave together with the stub.
|
||||||
|
- Full suite green; the diff is a removal.
|
||||||
|
|
||||||
## Acceptance criteria
|
## Acceptance criteria
|
||||||
|
|
||||||
The milestone ships when:
|
The milestone ships when:
|
||||||
|
|
||||||
1. The worked consumer program runs end-to-end: `ail check && ail
|
1. The worked consumer program runs end-to-end: `ail check && ail
|
||||||
build && ail run` prints `60` (raw-buf.3).
|
build && ail run` prints `60` (raw-buf.4).
|
||||||
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
|
||||||
prep.3 `param-not-in-restricted-set` diagnostic (raw-buf.3).
|
`param-not-in-restricted-set` diagnostic (raw-buf.4).
|
||||||
3. RawBuf's four operations are `(intrinsic)` markers, each paired
|
3. RawBuf's four ops are `(intrinsic)` markers, each mono'd to a
|
||||||
with an `INTERCEPTS` entry; `intercepts_bijection_with_intrinsic_markers`
|
scope-qualified symbol (`RawBuf_<op>__<T>`) with a matching
|
||||||
is green (raw-buf.3).
|
`INTERCEPTS` entry; `intercepts_bijection_with_intrinsic_markers`
|
||||||
4. `Term::New` no longer reaches codegen — the desugar eliminates
|
is green (the mechanism in raw-buf.3, the 12 entries in raw-buf.4).
|
||||||
it and both deferral arms (`lib.rs:2094` + `lib.rs:3296`) are
|
4. `Term::New` no longer reaches codegen — the desugar eliminates it
|
||||||
removed (raw-buf.3).
|
and both deferral arms (`lib.rs` ~2094 + ~3296) are removed
|
||||||
5. `ailang-kernel-stub` is renamed to the `ailang-kernel`
|
(raw-buf.4).
|
||||||
family-crate (raw-buf.2); `kernel_stub` is retired and `raw_buf`
|
5. `kernel_stub` is retired and `raw_buf` takes over its
|
||||||
takes over its ratification roles (raw-buf.4).
|
ratification roles (raw-buf.5).
|
||||||
6. Workspace test suite green at each iteration boundary, plus the
|
6. Workspace test suite green at each iteration boundary, plus the
|
||||||
new tests enumerated in § Testing strategy.
|
new tests 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 only
|
1. **LLM author reaches for it naturally.** RawBuf is the only path
|
||||||
path to mutable indexed storage in AILang — the language has no
|
to mutable indexed storage in AILang — the language has no other
|
||||||
other "fill N slots and read them back" primitive. The worked
|
"fill N slots and read them back" primitive. The worked consumer
|
||||||
consumer program above is what an LLM author writes for that
|
program is what an LLM author writes for that need; there is no
|
||||||
need; there is no alternative shape to reach for.
|
alternative shape to reach for.
|
||||||
|
|
||||||
2. **Measurable improvement.** Embedding-ABI M5 measured per-tick
|
2. **Measurable improvement.** Embedding-ABI M5 measured per-tick
|
||||||
FFI at ~206 ns/tick (~658 ms / 3.19M EURUSD ticks). RawBuf as
|
FFI at ~206 ns/tick (~658 ms / 3.19M EURUSD ticks). RawBuf as the
|
||||||
the batch-FFI primitive amortises that per-tick cost across one
|
batch-FFI primitive amortises that per-tick cost across one
|
||||||
crossing. The Series milestone (#8) is also blocked on RawBuf;
|
crossing. The Series milestone (#8) is also 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 stays mode-tracked:
|
||||||
mode-tracked (whitepaper § "RawBuf — the base extension"):
|
`RawBuf.set` is `own → own`, not effect-tracked; no `RawBuf`
|
||||||
`RawBuf.set` is `own → own`, not effect-tracked. No `RawBuf`
|
effect is declared. Uniqueness inference rewrites in-place; shared
|
||||||
effect is declared. Uniqueness inference rewrites in-place;
|
ownership falls back to copy-on-write (Issue #22). The pure-core
|
||||||
shared ownership falls back to copy-on-write (Issue #22). The
|
invariant survives (code without a declared effect is pure); local
|
||||||
pure-core invariant survives: code without a declared effect is
|
reasoning survives (a fn taking `borrow (RawBuf Int)` and
|
||||||
pure. Local reasoning survives: a fn taking `borrow (RawBuf
|
returning `Int` is pure from the caller's view). The new
|
||||||
Int)` and returning `Int` is pure from the caller's view,
|
scope-qualified mono symbols *remove* a latent bug class — the
|
||||||
because the buffer is not mutated.
|
`get__Int`-style collision between different types' identically
|
||||||
|
named polymorphic ops.
|
||||||
|
|||||||
Reference in New Issue
Block a user