AILang/docs/specs/0058-fieldtest-raw-buf.md

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 <types…> <values…>) 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<Tick> — 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.