From 8e9f0f06a636816f6ef194c145e452a8d56560e5 Mon Sep 17 00:00:00 2001 From: Brummel Date: Sat, 30 May 2026 16:26:48 +0200 Subject: [PATCH] =?UTF-8?q?fieldtest:=20raw-buf=20=E2=80=94=204=20examples?= =?UTF-8?q?,=206=20findings=20(refs=20#7)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Downstream field test of the raw-buf surface as a consumer with only the public interface (design ledger + `ail` CLI; no crate source). Four fixtures under examples/fieldtest/, spec at docs/specs/0058-fieldtest-raw-buf.md. Every recorded outcome reproduced independently before commit. Findings (3 bug, 1 spec_gap, 2 working): - B1 [bug] `borrow (RawBuf a)` receiver is unusable. A fn taking `borrow (RawBuf Int)` that calls RawBuf.get/.size on the parameter even once is rejected `consume-while-borrowed` — the diagnostic names the wrong cause (the receiver is not consumed). The ledger advertises get/size as borrow-receiver ops, so the documented use is unreachable from any helper-function decomposition. This blocks Series (#8) — the milestone's own downstream raison d'être — whose at/total_count read through a `borrow (Series a)`. - B2 [bug] An owned RawBuf threaded through a `loop` binder passes check but panics codegen `unknown variable: b` at build. A plain Int loop binder builds fine, so the fault is specific to an owned RawBuf loop binder. Breaks the check↔codegen agreement. - B3 [bug] `param-not-in-restricted-set` omits the allowed set. design/models/0007 §4 promises the diagnostic "names the offending type and the allowed set"; the shipped message names the type, the type-var, and the home type but not `{Int, Float, Bool}`. A downstream author is told what is wrong but not what is right. - B4 [spec_gap] RawBuf.set receiver double-consume is not enforced; two set calls on the same owned buffer silently alias the slab. Not raw-buf-specific (owned Str/ADT behave identically) — a pre-existing linearity-non-enforcement property. Recorded because RawBuf's own→own mutation is the first place a silent alias yields a mutated-in-place surprise. Ratify in the ledger or open a backlog item for full linear enforcement. - W1 [working] `(new …)` sugar + inference-from-use across Int/Float/Bool builds and runs first try (sensor_pair prints 5.0); the Bool i1/i8 packing edge round-trips. The milestone's cleanest win. - W2 [working] param-in reject fires for both Str and a user TypeDef. Net: B1+B2 mean the only RawBuf programs that build today are straight-line owned let-threading with literal indices — the shipped-fixture shape. Helper decomposition (B1) and runtime-length loop fill (B2) both fail. fieldtest does not self-resolve; routing is the orchestrator's call. --- docs/specs/0058-fieldtest-raw-buf.md | 200 ++++++++++++++++++ examples/fieldtest/rawbuf_1_score_table.ail | 56 +++++ examples/fieldtest/rawbuf_2_running_max.ail | 40 ++++ examples/fieldtest/rawbuf_3_sensor_pair.ail | 36 ++++ .../fieldtest/rawbuf_4_paramin_reject.ail | 35 +++ 5 files changed, 367 insertions(+) create mode 100644 docs/specs/0058-fieldtest-raw-buf.md create mode 100644 examples/fieldtest/rawbuf_1_score_table.ail create mode 100644 examples/fieldtest/rawbuf_2_running_max.ail create mode 100644 examples/fieldtest/rawbuf_3_sensor_pair.ail create mode 100644 examples/fieldtest/rawbuf_4_paramin_reject.ail diff --git a/docs/specs/0058-fieldtest-raw-buf.md b/docs/specs/0058-fieldtest-raw-buf.md new file mode 100644 index 0000000..9061898 --- /dev/null +++ b/docs/specs/0058-fieldtest-raw-buf.md @@ -0,0 +1,200 @@ +# Fieldtest — raw-buf — 2026-05-30 + +**Status:** Draft — awaiting orchestrator triage +**Author:** fieldtester (dispatched by fieldtest skill) + +## Scope + +The raw-buf milestone (#7, range `a163c8c..f37bd95`) shipped `RawBuf a`, +the first kernel-tier *base* extension: a mutable, indexed, fixed-size +flat buffer of primitive elements (`a ∈ {Int, Float, Bool}`). New +user-visible surface: the four type-scoped ops `(app RawBuf.new n)`, +`(app RawBuf.get b i)`, `(app RawBuf.set b i v)`, `(app RawBuf.size b)` +(`set` linear `own → own`; `get`/`size` `borrow`); the general +`(new T )` construction sugar with element type +recovered by inference-from-use; kernel-tier auto-import (bare `RawBuf`, +no `(import …)`); the `param-in (a Int Float Bool)` element-type +restriction rejected at `ail check`; and owned-RawBuf drop at scope +close. I exercised the four axes from the carrier as a downstream +consumer with only `ail check`/`build`/`run` and the design ledger +(`design/models/0007`, `docs/specs/0054`). + +## Examples + +### examples/fieldtest/rawbuf_1_score_table.ail — score table via borrow-helpers +- Fill a 5-slot Int buffer with `i*i+1` in a `loop`, then sum it back in + a `total : borrow (RawBuf Int) -> Int` helper that drives off + `RawBuf.size`. The LLM-natural decomposition: factor read-back into a + `borrow`-receiver helper. +- Fits axis 1 (mutable indexed storage) and exercises `size`, which the + ledger's worked program (literal 0/1/2 indices) never does. +- Outcome: **does not check.** `total` is rejected with + `consume-while-borrowed` although it only calls `RawBuf.size`/`.get` + on a `borrow` receiver. (Surfaces finding B1.) Authoring also hit two + papercuts: a `loop` binder may not carry `own`, and the prelude + comparison is `ge` not `gte`. + +### examples/fieldtest/rawbuf_2_running_max.ail — fill-loop + running max +- Populate a 4-slot Int buffer of length-N in a `loop`/`recur` (one + `RawBuf.set` per iteration, threading the owned buffer through the loop + binder `b`), then read it back for the running maximum. The natural way + to fill a buffer whose length is not three literals. +- Fits axis 1 + axis 4 (loop-threaded linear ownership). +- Outcome: **checks `ok`, then fails at `build`** with + `def main: unknown variable: b`. (Surfaces finding B2.) + +### examples/fieldtest/rawbuf_3_sensor_pair.ail — Float + Bool buffers +- Store three Float readings and one Bool alarm flag in two buffers, + average the readings, double if the alarm is set. Drives + `(new RawBuf (con Float) 3)` and `(new RawBuf (con Bool) 1)`; element + type recovered purely from stored values (`1.5`, `true`). +- Fits axis 2 (the `new` sugar across element types; Bool is the i1/i8 + packing edge). +- Outcome: **check + build + run clean; prints `5.0`** (expected). + (Finding W1.) + +### examples/fieldtest/rawbuf_4_paramin_reject.ail — user-TypeDef element reject +- Model a `Tick` ADT and try to hold a batch in `RawBuf` — the + obvious move for batch storage. Probes the user-TypeDef path (distinct + from the shipped `Str` fixture). +- Fits axis 3 (`param-in` restriction). +- Outcome: **rejects at `ail check` (exit 1)** with + `param-not-in-restricted-set` — the reject fires correctly, but the + message omits the allowed set the ledger promises. (Findings W2 + B3.) + +## Findings + +### [bug] B1 — `borrow (RawBuf a)` receiver is unusable: a single get/size is rejected +- Examples: `rawbuf_1_score_table.ail`; minimal repros below. +- A function taking `borrow (RawBuf Int)` that calls `RawBuf.get` or + `RawBuf.size` on the parameter even **once** is rejected: + ``` + [consume-while-borrowed] read_one: `buf` is consumed while a borrow of it is still live + ``` + Both ops take `borrow (RawBuf a)` per `design/models/0007` §RawBuf and + `docs/specs/0054`, so borrowing the receiver to read it is exactly the + advertised use. An inline owned `let`-bound buffer reads fine (the + shipped fixtures), but the moment the buffer is behind a `borrow`-mode + *parameter*, the read ops are misclassified as consuming. This makes + the `borrow` signatures in the ledger unreachable from the natural + decomposition (helper functions over a shared read-only buffer) — e.g. + Series's own `Series.at`/`Series.total_count` (ledger §Series, which + call `RawBuf.get` through a `borrow (Series a)`) would hit this. +- Why a bug: the ledger advertises `get`/`size` as `borrow`-receiver + ops; the checker rejects the documented use with a borrow-related + diagnostic naming the wrong cause (`buf` is not consumed). +- Repro: `ail check` the module + `(fn read_one (type (fn-type (params (borrow (con RawBuf (con Int)))) (ret (con Int)))) (params buf) (body (app RawBuf.get buf 0)))` + → `[consume-while-borrowed]`. +- Recommended action: **debug** (RED test: a `borrow (RawBuf Int)` + helper doing one `RawBuf.get` should check `ok`). + +### [bug] B2 — owned RawBuf threaded through a `loop` binder passes check but fails codegen +- Examples: `rawbuf_2_running_max.ail`; minimal repro below. +- A `loop` binder holding an owned `RawBuf` value threaded through + `recur` (`(loop (b (con RawBuf (con Int)) buf) (i …) … (recur (app RawBuf.set b i …) …))`) + checks `ok` but fails at `ail build`: + ``` + Error: module `…`: def `main`: unknown variable: `b` + ``` + A plain `Int` loop binder named `b` builds and runs fine, so the fault + is specific to threading an owned RawBuf through a loop binder. This + breaks the check↔codegen agreement (the CLAUDE.md discipline that a + program passing `check` is a program codegen can lower). +- Why a bug: `check` accepts, codegen panics with `unknown variable`; + the loop binder is not registered in the codegen scope for an owned + RawBuf value. +- Repro: `ail check` ok then `ail build` fail on + `(let buf (new RawBuf (con Int) 3) (loop (b (con RawBuf (con Int)) buf) (i (con Int) 0) (if (app ge i 3) b (recur (app RawBuf.set b i 0) (app + i 1)))))`. +- Recommended action: **debug** (RED test: build the fill-loop fixture → + no `unknown variable`). + +### [bug] B3 — `param-not-in-restricted-set` omits the allowed set the ledger promises +- Example: `rawbuf_4_paramin_reject.ail` (and the shipped Str fixture). +- Verbatim: + ``` + [param-not-in-restricted-set] first_price: type-arg `Tick` is not in the restricted set for type-variable `a` of `raw_buf.RawBuf` + ``` + `design/models/0007` §4 states: "`ParamNotInRestrictedSet` names the + offending type **and the allowed set**." The shipped message names the + offending type, the type-var, and the home type, but **not** the + allowed `{Int, Float, Bool}`. A downstream author is told `Tick` is + wrong but not what is right; self-correction requires reading the + kernel source, which a downstream consumer cannot do. +- Why a bug: diagnostic content is narrower than the ledger's stated + diagnostic contract. (Borderline friction, but it is a concrete + ledger-vs-implementation discrepancy → classified `bug`.) +- Repro: `ail check examples/fieldtest/rawbuf_4_paramin_reject.ail`. +- Recommended action: **debug** (small) — append the allowed set to the + message; OR if the ledger over-promised, **tighten the ledger** (drop + "and the allowed set"). The former is the author-useful fix. + +### [spec_gap] B4 — `RawBuf.set` linearity of the receiver is not enforced (double-consume silently aliases) +- Examples: `/tmp` probes `p_double.ail`, `p_double2.ail`. +- An owned buffer consumed by two `RawBuf.set` calls + (`(let a (app RawBuf.set buf 0 1) (let b (app RawBuf.set buf 1 2) …))`) + checks `ok` and builds; `a` and `b` alias the same slab (reading + `a[0]`+`b[1]` printed `3`). The ledger presents `set` as "linear: + caller hands over the buffer, callee returns it" — implying the + handed-over buffer can't be used again. The checker does not enforce + that for `set`'s `own` receiver. **Not RawBuf-specific:** owned `Str` + and owned ADT values double-consumed through a consuming fn also check + `ok` (controls `p_str.ail`, `p_adt.ail`), so this is a pre-existing + linearity-enforcement property, not a raw-buf regression. Recorded + because RawBuf's `own → own` mutation surface is the first place a + silent alias produces a *mutated-in-place* surprise rather than a + benign re-read. +- Why spec_gap: the ledger's "linear" framing for `set` and the actual + non-enforcement of receiver single-use are two equally plausible + readings; the milestone picked non-enforcement (consistent with the + rest of the language) without the ledger saying so for RawBuf. +- Recommended action: **ratify** the current behaviour in the ledger + (state that mode annotations are not full linearity enforcement and + double-consume of an owned RawBuf is the author's responsibility), OR + open a backlog item if full linear enforcement is wanted. Either way a + ledger note; not urgent. + +### [working] W1 — `(new …)` sugar + inference-from-use across Int/Float/Bool +- Example: `rawbuf_3_sensor_pair.ail` (Float + Bool); also every fixture + uses `(new RawBuf (con Int) n)`. +- `(new RawBuf (con Float) 3)` and `(new RawBuf (con Bool) 1)` both + construct cleanly with no element-type annotation on any + `RawBuf.set`/`.get`; the element type is recovered from the stored + values (`1.5 : Float`, `true : Bool`). Built and ran first try, + printing `5.0`. The i1/i8 Bool packing edge round-trips correctly + (`true` stored, read back, discriminated). This is the milestone's + cleanest win — the sugar reads exactly as the ledger's worked example + promised and the inference-from-use story holds across all three + element widths. +- Recommended action: **carry-on**. + +### [working] W2 — `param-in` reject fires for both Str and a user TypeDef +- Example: `rawbuf_4_paramin_reject.ail`. +- The `param-not-in-restricted-set` reject fires at `ail check` (exit 1) + for a user-defined `Tick` ADT element, identically to the shipped + `Str` fixture. The restriction is enforced on the real payload type, + names the offending type, the type-var, and the home type + `raw_buf.RawBuf`. (Its one shortfall — the missing allowed set — is + B3; the *firing* itself is a clean win.) +- Recommended action: **carry-on**. + +## Recommendation summary + +| Finding | Class | Action | +|---|---|---| +| B1 borrow-receiver get/size rejected | bug | debug | +| B2 owned-RawBuf loop binder fails codegen | bug | debug | +| B3 param-in message omits allowed set | bug | debug (small) / or tighten ledger | +| B4 set receiver double-consume not enforced | spec_gap | ratify (ledger note) | +| W1 `new` sugar + inference across types | working | carry-on | +| W2 param-in reject on Str + user TypeDef | working | carry-on | + +### Orthogonal observations (not raw-buf findings, noted in passing) +- `loop` binders reject an `own` mode annotation + (`own may only appear inside fn-type params or ret`); combined with B2, + there is currently no working way to thread an owned RawBuf through a + loop at all. +- Prelude comparison ops are `ge`/`le`/`gt`/`lt`/`ne` (not `gte`/`lte`); + `ail builtins` does not list them (they live in the prelude), so an + author guesses the spelling. Minor surface-discoverability friction, + pre-existing, outside the raw-buf axes. diff --git a/examples/fieldtest/rawbuf_1_score_table.ail b/examples/fieldtest/rawbuf_1_score_table.ail new file mode 100644 index 0000000..7ed4a3a --- /dev/null +++ b/examples/fieldtest/rawbuf_1_score_table.ail @@ -0,0 +1,56 @@ +; Fieldtest raw-buf.1 (Axis 1, RawBuf as mutable indexed storage). +; Task an LLM author is naturally given: "build a small score table of +; N slots, fill slot i with a computed score (i*i + 1), then read every +; slot back and total the scores." The natural shape uses RawBuf.size to +; drive the read loop rather than hard-coding the bound, which the spec's +; worked program (literal 0/1/2 indices) never exercises. +; +; Fill loop: thread the owned buffer through RawBuf.set in a (loop ...) +; with a recur per slot. Read loop: borrow the buffer, drive i from 0 to +; (RawBuf.size buf) accumulating (RawBuf.get buf i). +; +; 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`. + +(module rawbuf_1_score_table + + (fn fill + (doc "Fill slots 0..n of buf with (i*i + 1). Linear: own in, own out.") + (type (fn-type (params (own (con RawBuf (con Int))) (con Int)) (ret (own (con RawBuf (con Int)))))) + (params buf n) + (body + (loop (b (con RawBuf (con Int)) buf) (i (con Int) 0) + (if (app ge i n) + b + (recur (app RawBuf.set b i (app + (app * i i) 1)) + (app + i 1)))))) + + (fn total + (doc "Sum every slot of buf, driving the bound off RawBuf.size.") + (type (fn-type (params (borrow (con RawBuf (con Int)))) (ret (con Int)))) + (params buf) + (body + (loop (acc (con Int) 0) (i (con Int) 0) + (if (app ge i (app RawBuf.size buf)) + acc + (recur (app + acc (app RawBuf.get buf i)) + (app + i 1)))))) + + (fn main + (type (fn-type (params) (ret (con Unit)) (effects IO))) + (params) + (body + (let buf (new RawBuf (con Int) 5) + (let buf (app fill buf 5) + (app print (app total buf))))))) diff --git a/examples/fieldtest/rawbuf_2_running_max.ail b/examples/fieldtest/rawbuf_2_running_max.ail new file mode 100644 index 0000000..e2c86fa --- /dev/null +++ b/examples/fieldtest/rawbuf_2_running_max.ail @@ -0,0 +1,40 @@ +; Fieldtest raw-buf.2 (Axis 1 + Axis 4, loop-threaded owned RawBuf). +; Task: "fill a buffer of N slots with a sequence in a loop, then read it +; back and print the running maximum." This is the LLM-natural way to +; populate a buffer whose length is a runtime N rather than three literal +; (RawBuf.set buf ...) lines: thread the owned buffer through a +; (loop ...) / recur, one RawBuf.set per iteration. +; +; The whole program is inlined into main (no borrow-mode helper, which +; rawbuf_1_score_table.ail showed is rejected). The fill loop threads the +; owned `b` through recur; the read loop drives off RawBuf.size. +; +; 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. + +(module rawbuf_2_running_max + (fn main + (type (fn-type (params) (ret (con Unit)) (effects IO))) + (params) + (body + (let buf (new RawBuf (con Int) 4) + (let filled + (loop (b (con RawBuf (con Int)) buf) (i (con Int) 0) + (if (app ge i 4) + b + (recur (app RawBuf.set b i (app * (app + i 1) (app + i 1))) + (app + i 1)))) + (app print + (loop (mx (con Int) 0) (i (con Int) 0) + (if (app ge i (app RawBuf.size filled)) + mx + (recur (if (app gt (app RawBuf.get filled i) mx) + (app RawBuf.get filled i) + mx) + (app + i 1)))))))))) diff --git a/examples/fieldtest/rawbuf_3_sensor_pair.ail b/examples/fieldtest/rawbuf_3_sensor_pair.ail new file mode 100644 index 0000000..79725fb --- /dev/null +++ b/examples/fieldtest/rawbuf_3_sensor_pair.ail @@ -0,0 +1,36 @@ +; Fieldtest raw-buf.3 (Axis 2, the (new T ) sugar across +; element types). Task: "store three Float sensor readings and a Bool +; alarm flag in flat buffers, then report the average of the readings, +; doubled if the alarm flag is set." This drives (new RawBuf (con Float) 3) +; and (new RawBuf (con Bool) 1) in one program, so the construction sugar +; and its inference-from-use story are exercised on both the 8-byte +; (Float) and the 1-byte (Bool) element widths. +; +; The element type of each buffer is never written on RawBuf.set/.get; it +; is recovered purely from the values stored (1.5 : Float, true : Bool). +; Straight-line owned `let`-threading (the only shape that currently +; builds for RawBuf — see rawbuf_1/rawbuf_2). +; +; Expected stdout: average (1.5+2.5+3.5)/3 = 2.5, alarm set => doubled +; => 5.0 -> "5.0". + +(module rawbuf_3_sensor_pair + (fn main + (type (fn-type (params) (ret (con Unit)) (effects IO))) + (params) + (body + (let readings (new RawBuf (con Float) 3) + (let readings (app RawBuf.set readings 0 1.5) + (let readings (app RawBuf.set readings 1 2.5) + (let readings (app RawBuf.set readings 2 3.5) + (let alarm (new RawBuf (con Bool) 1) + (let alarm (app RawBuf.set alarm 0 true) + (let avg (app / + (app + (app RawBuf.get readings 0) + (app + (app RawBuf.get readings 1) + (app RawBuf.get readings 2))) + 3.0) + (app print + (if (app RawBuf.get alarm 0) + (app * avg 2.0) + avg)))))))))))) diff --git a/examples/fieldtest/rawbuf_4_paramin_reject.ail b/examples/fieldtest/rawbuf_4_paramin_reject.ail new file mode 100644 index 0000000..06977a5 --- /dev/null +++ b/examples/fieldtest/rawbuf_4_paramin_reject.ail @@ -0,0 +1,35 @@ +; Fieldtest raw-buf.4 (Axis 3, param-in element-type restriction). +; Task: an LLM author models a small "tick" record and reaches for a +; RawBuf to hold a batch of them — the obvious move for batch storage. +; RawBuf's element type is restricted to {Int, Float, Bool} via param-in, +; so a user TypeDef element must be rejected at `ail check` with a +; diagnostic that tells the author *why* and *what is allowed*. +; +; This probes the user-TypeDef path (distinct from the Str path the +; shipped raw_buf_reject_str.ail covers): does param-in fire for a type +; the author defined themselves, and does the message name the allowed +; set so the author can self-correct (e.g. switch to a Float field)? +; +; Expected: `ail check` exits non-zero with param-not-in-restricted-set +; naming `Tick` and the allowed set {Int, Float, Bool}. +; +; OUTCOME: rejects as expected (exit 1). Verbatim: +; [param-not-in-restricted-set] first_price: type-arg `Tick` is not in +; the restricted set for type-variable `a` of `raw_buf.RawBuf` +; The reject fires (good) and names the offending type, the type-var, and +; the home type. BUT it does NOT name the allowed set {Int, Float, Bool}, +; which design/models/0007 §4 explicitly promises ("ParamNotInRestrictedSet +; names the offending type AND the allowed set"). A downstream author who +; reaches for RawBuf is told `Tick` is wrong but not what would be +; right; they cannot self-correct without reading the kernel source. + +(module rawbuf_4_paramin_reject + + (data Tick + (ctor MkTick (con Float) (con Int))) + + (fn first_price + (doc "Read the first Tick out of a batch buffer. Should never check: RawBuf cannot hold a user ADT.") + (type (fn-type (params (borrow (con RawBuf (con Tick)))) (ret (con Tick)))) + (params batch) + (body (app RawBuf.get batch 0))))