fieldtest: raw-buf — 4 examples, 6 findings (refs #7)

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.
This commit is contained in:
2026-05-30 16:26:48 +02:00
parent f37bd959d4
commit 8e9f0f06a6
5 changed files with 367 additions and 0 deletions
@@ -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)))))))
@@ -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 <lit> ...) 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))))))))))
@@ -0,0 +1,36 @@
; Fieldtest raw-buf.3 (Axis 2, the (new T <types> <values>) 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))))))))))))
@@ -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<Tick> 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))))