From d5cc6e96b6fc310d0118144df2cf31bb185cca8f Mon Sep 17 00:00:00 2001 From: Brummel Date: Sat, 30 May 2026 17:14:39 +0200 Subject: [PATCH] docs(raw-buf): refresh fixture outcomes; ratify set non-enforcement (refs #7) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - rawbuf_1_score_table / rawbuf_2_running_max: the header OUTCOME blocks described the pre-fix breakage (does-not-check / unknown-variable). Those defects are fixed (B1 #46, B2 #47, B5); update the comments to the current state — both check, build, run to their expected values and are leak-clean under AILANG_RC_STATS. The files now serve as positive regression examples, not bug repros. - design/models/0007 §RawBuf: ratify the fieldtest's B4 spec_gap. The `own -> own` signature of RawBuf.set is a threading discipline, not runtime-enforced single-use; a double-consume of the same owned buffer aliases one slab (consistent with every owned value in the language). State that single-use is the author's responsibility and full linear enforcement is Issue #22 territory. Surfaced by the raw-buf fieldtest (docs/specs/0058). --- design/models/0007-kernel-extensions.md | 16 ++++++++++++++ examples/fieldtest/rawbuf_1_score_table.ail | 23 +++++++++++---------- examples/fieldtest/rawbuf_2_running_max.ail | 13 ++++++------ 3 files changed, 35 insertions(+), 17 deletions(-) diff --git a/design/models/0007-kernel-extensions.md b/design/models/0007-kernel-extensions.md index c3ddb38..c21c5f9 100644 --- a/design/models/0007-kernel-extensions.md +++ b/design/models/0007-kernel-extensions.md @@ -405,6 +405,22 @@ The own/borrow signatures *are* the mutation contract. No existing memory-model — RC + uniqueness as the canonical mutation story. +The `own → own` signature of `RawBuf.set` is a *threading +discipline*, not runtime-enforced single-use. The mode annotations +drive the borrow/consume analysis and the in-place-vs-copy codegen +decision; they do not make a second consume of the same owned +binder a check-time error. An author who hands the same owned +buffer to two consuming calls +(`(let a (RawBuf.set buf 0 1)) (let b (RawBuf.set buf 1 2))`) +gets two bindings aliasing one slab — the second mutation is +visible through the first. This is the same non-enforcement that +holds for every owned value in the language (owned `Str`, owned +ADTs); `RawBuf`'s in-place `own → own` surface is merely the first +place the alias produces a *mutated-in-place* surprise rather than +a benign re-read. Single-use of an owned buffer is the author's +responsibility. Full linear enforcement, if wanted, is tracked +separately (Issue #22 territory). + Storage at the LLVM-IR level is type-specialised: the Rust intercept registered for `RawBuf` dispatches on the element type at each call site and emits the appropriate `getelementptr` / diff --git a/examples/fieldtest/rawbuf_1_score_table.ail b/examples/fieldtest/rawbuf_1_score_table.ail index 7ed4a3a..87f593b 100644 --- a/examples/fieldtest/rawbuf_1_score_table.ail +++ b/examples/fieldtest/rawbuf_1_score_table.ail @@ -11,17 +11,18 @@ ; ; Expected stdout: scores 1, 2, 5, 10, 17 -> sum 35. ; -; OUTCOME: does NOT check. `ail check` reports, for the `total` fn: -; [consume-while-borrowed] total: `buf` is consumed while a borrow of -; it is still live -; even though `total` takes `borrow (RawBuf Int)` and only calls -; RawBuf.size / RawBuf.get on it (both `borrow`-receiver ops per the -; ledger). A single get/size on a borrow-mode receiver triggers it. -; (The `fill` loop, if `total` were removed, would in turn fail at -; `build` with `unknown variable: b` — see rawbuf_2_running_max.ail.) -; First authoring attempt also hit two papercuts: a `loop` binder may -; not carry an `own` mode ("`own` may only appear inside fn-type params -; or ret"), and the prelude comparison is `ge`, not `gte`. +; This was the fieldtest repro for two defects, both now fixed: +; - B1 (#46): the `total` helper, which takes `borrow (RawBuf Int)` +; and only calls RawBuf.size / RawBuf.get on the receiver, was +; falsely rejected with [consume-while-borrowed]. The linearity +; pass now resolves the type-scoped borrow-receiver ops, so the +; borrow helper checks clean. +; - B2 (#47): the `fill` loop, threading the owned buffer through a +; `recur`, failed codegen with `unknown variable: b`. The synth +; type-replay now descends through `loop` with the loop binders in +; scope. +; OUTCOME (current): checks, builds, runs; prints 35. Leak-clean under +; AILANG_RC_STATS (the owned buffer drops at scope close, B5). (module rawbuf_1_score_table diff --git a/examples/fieldtest/rawbuf_2_running_max.ail b/examples/fieldtest/rawbuf_2_running_max.ail index e2c86fa..a8d999a 100644 --- a/examples/fieldtest/rawbuf_2_running_max.ail +++ b/examples/fieldtest/rawbuf_2_running_max.ail @@ -11,12 +11,13 @@ ; ; Expected stdout: 16 (slots 1,4,9,16; running max ends at 16). ; -; OUTCOME: `ail check` passes ("ok"), but `ail build` FAILS at codegen: -; Error: module `rawbuf_2_running_max`: def `main`: unknown variable: `b` -; The owned-RawBuf `loop` binder `b` threaded through `recur` is visible -; to the checker but not to codegen. A plain Int loop binder named `b` -; builds fine, so it is specific to threading an owned RawBuf value -; through a loop binder. The check<->codegen agreement is broken here. +; This was the fieldtest repro for B2 (#47): `ail check` passed but +; `ail build` FAILED at codegen with `unknown variable: b` — the synth +; type-replay walked the `loop` body without the loop binders in scope. +; Now fixed: the replay descends through `loop` with its binders bound. +; OUTCOME (current): checks, builds, runs; prints 16. Leak-clean under +; AILANG_RC_STATS (the loop-threaded owned buffer drops at scope close, +; B5 — the let-bound loop result is now registered for scope-close drop). (module rawbuf_2_running_max (fn main