From 1b2d23ec42f9bd5955254fe963261111777284a2 Mon Sep 17 00:00:00 2001 From: Brummel Date: Sat, 30 May 2026 18:29:00 +0200 Subject: [PATCH] =?UTF-8?q?fieldtest:=20raw-buf=20comprehensive=20?= =?UTF-8?q?=E2=80=94=204=20examples,=208=20findings=20(refs=20#7)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Comprehensive usability re-test of the RawBuf kernel extension in natural LLM-author decompositions the prior field test (0058) did not exercise: a Float RawBuf in a user ADT read through two borrow helpers, a Bool flag buffer filled with a computed value, an Int fib buffer whose fill reads its own writes plus two composed borrow summaries, and a forbidden core-primitive element. All three working fixtures build, run to expected values, and report live=0 across Float/Bool/Int widths — the core RawBuf surface (borrow-helper composition, fill loops, RawBuf-in-ADT, element widths) genuinely holds together. Orchestrator triage corrected the fieldtester's run, which executed a stale target/release/ail (built before the #50 fix). Every outcome was re-verified against a fresh build: - F2 (bare RawBuf ADT field unresolved) — RETRACTED: a stale-binary false positive. On a fresh build the bare name resolves in every configuration (ctor name == or != type name; builds/runs live=0). The #50 fix is correct and general. - F7 (NEW, issue #51) — a `check`-clean program crashes `build`: a buffer whose element type is never observed by a later get/set defaults its element to Unit in monomorphisation and hits an unregistered `RawBuf_new__Unit` intercept. Affects a legitimate `RawBuf` used only for its size AND a forbidden locally- constructed element. Root: the `(new T ...)` desugar drops the explicit element annotation; honouring it reverses the milestone's § Term::New desugar decision, so it routes through brainstorm. - F8 (process) — the field test ran stale; the fieldtester agent now builds from the current tree before running (plugin fix). F1 (spec_gap) resolved here: the design ledger's §Series substrate ctor wrote the storage field `(own (RawBuf a))`, which does not parse (`own` is fn-param/ret only). Rewritten to the verified-authorable `(con RawBuf a)`. The rest of the §Series listing is illustrative and its element- less `(new RawBuf lookback)` construction is entangled with #51; a full compile-verification of that listing belongs with the Series-substrate work. F5 (param-in rejects a forbidden core primitive, message names the set) and F4/F3 (borrow composition; substrate composite) carry on. F6 (param-in set rendered as a Rust-debug list) filed as #52. refs #7 --- design/models/0007-kernel-extensions.md | 3 +- .../0059-fieldtest-raw-buf-comprehensive.md | 275 ++++++++++++++++++ .../fieldtest/rbx_1_float_window_stats.ail | 92 ++++++ examples/fieldtest/rbx_2_bool_sieve.ail | 57 ++++ .../fieldtest/rbx_3_unit_element_reject.ail | 29 ++ .../rbx_4_int_two_borrow_helpers.ail | 76 +++++ 6 files changed, 531 insertions(+), 1 deletion(-) create mode 100644 docs/specs/0059-fieldtest-raw-buf-comprehensive.md create mode 100644 examples/fieldtest/rbx_1_float_window_stats.ail create mode 100644 examples/fieldtest/rbx_2_bool_sieve.ail create mode 100644 examples/fieldtest/rbx_3_unit_element_reject.ail create mode 100644 examples/fieldtest/rbx_4_int_two_borrow_helpers.ail diff --git a/design/models/0007-kernel-extensions.md b/design/models/0007-kernel-extensions.md index 54fb716..1464326 100644 --- a/design/models/0007-kernel-extensions.md +++ b/design/models/0007-kernel-extensions.md @@ -444,7 +444,8 @@ handles allocation, drop, and copy-on-share. (data Series (vars a) (param-in (a Int Float Bool)) - (ctor S (own (RawBuf a)) ; the storage + (ctor S (con RawBuf a) ; the storage (no mode: modes live on + ; fn params/ret, not on ADT fields) (con Int) ; lookback (con Int) ; head index (con Int) ; current count diff --git a/docs/specs/0059-fieldtest-raw-buf-comprehensive.md b/docs/specs/0059-fieldtest-raw-buf-comprehensive.md new file mode 100644 index 0000000..d9bdd8d --- /dev/null +++ b/docs/specs/0059-fieldtest-raw-buf-comprehensive.md @@ -0,0 +1,275 @@ +# Fieldtest — raw-buf (comprehensive re-test) — 2026-05-30 + +**Status:** Triaged — orchestrator re-verified every outcome against a +fresh build. +**Author:** fieldtester (dispatched by fieldtest skill); finding triage +and corrections by the orchestrator. + +## Verification note (orchestrator) + +The fieldtester ran against `target/release/ail`, which was **stale** — +built at 17:22, before the #50 fix landed at 17:48. Every outcome below +was therefore re-verified against a freshly built binary during triage. +The re-verification changed one finding materially: **F2 does not +reproduce on a fresh build and is retracted** (it was an artefact of the +stale binary). It also surfaced a real defect class the stale run masked +(F7, now issue #51) and a process gap (F8). All other outcomes +(F1, F3, F4, F5, F6) reproduce on the fresh binary and stand. + +## Scope + +A comprehensive usability re-test of the `RawBuf` kernel base extension +and the kernel-extension surface as it ships at HEAD (`4ad003d..HEAD`), +*after* this session's usability repairs (#46 borrow-receiver, #47 +fill-loop build, #48 param-in message, #50 RawBuf-in-ADT bare name, +B5 loop-result drop, #49 superseded-heap-binder dec). The brief was +explicitly *not* to re-run the prior four fixtures +(`docs/specs/0058-fieldtest-raw-buf.md`) but to push into natural +decompositions an LLM author would reach for that the prior test did +NOT exercise — RawBuf wrapped in a user ADT with bookkeeping (the +"Series substrate"), Bool-width fills through a loop, two borrow helpers +composed over one buffer, and a forbidden *core-primitive* element type. +Element width was varied across examples (Float, Bool, Int). All work +was done as a downstream consumer with only `ail check` / `build +--alloc=rc` / `run`, `AILANG_RC_STATS=1`, and the public interface +(`design/INDEX.md`, `design/models/0007-kernel-extensions.md`, the +`examples/` corpus). The prior four rawbuf fixtures were also re-run as +a regression spot-check — all still build, run to their expected values, +and report `live=0`. + +## Examples + +### examples/fieldtest/rbx_1_float_window_stats.ail — Float window in a user ADT, two borrow helpers +- A `Window` ADT wraps a `RawBuf` plus an Int `count`. `build_window` + allocates a 4-slot Float buffer, fills it via a `loop`/`recur` (one + `RawBuf.set` per slot, `int_to_float (2*(i+1))`), and wraps it in `W`. + Two `borrow (Window)` helpers — `mean` and `wmax` — each `match` the + ADT and read the buffer through `RawBuf.get` on a borrow. +- Why it fits: the §Series substrate shape (RawBuf in a user ADT field, + axes 1+2+3+4 combined) on the Float width, with the borrow-receiver + read behind a match and composed across two helpers — none of which + the prior test exercised together. +- Outcome: **builds + runs + leak-clean** (`allocs=4 frees=4 live=0`, + prints `5.0` / `8.0`). One surface adjustment was needed: the `own` + mode cannot appear on the storage field (the ledger's `(own (RawBuf a))` + substrate form does not parse — F1), so the field is written + `(con raw_buf.RawBuf (con Float))`. The bare `(con RawBuf (con Float))` + field **also** resolves on a fresh build (the #50 fix); the fixture + keeps the qualified spelling but the bare name is no longer required + (retracted F2). + +### examples/fieldtest/rbx_2_bool_sieve.ail — Bool flag buffer, computed fill, borrow count +- `mark_even` fills an N-slot `RawBuf` via a loop with a *computed* + Bool (`eq (i % 2) 0`) per slot; `count_set` (a `borrow (RawBuf Bool)` + helper) reads the flags back through `RawBuf.get` used directly as an + `if` condition and accumulates an Int. +- Why it fits: the i1/i8 Bool packing edge driven through a runtime-N + fill loop with a *computed* (not literal `true`) value — the prior + W1 only stored one literal Bool at a literal index — plus the #46 + borrow-receiver fix on the Bool width. +- Outcome: **builds + runs + leak-clean** (`allocs=2 frees=2 live=0`, + prints `3`). Clean on first try. See finding F4. + +### examples/fieldtest/rbx_3_unit_element_reject.ail — forbidden core-primitive element +- `(new RawBuf (con Unit) n)` — a RawBuf of `Unit`, a *core primitive* + not in `{Int, Float, Bool}`. +- Why it fits: the prior test rejected `Str` (heap primitive) and `Tick` + (user ADT); this covers the third class, a core primitive, and + re-verifies the #48 message fix names the allowed set. +- Outcome: **rejects at `ail check` (exit 1)** with + `[param-not-in-restricted-set] … type-arg \`Unit\` … (allowed: one of + ["Bool", "Float", "Int"])`. The B3/#48 fix is visible. See findings + F5, F6. + +### examples/fieldtest/rbx_4_int_two_borrow_helpers.ail — Int fib buffer, fill reads itself, two borrow summaries +- `fill` (own→own, across a fn boundary) fills slot i with fib(i), + reading prior slots via `RawBuf.get` on the *owned* loop binder `b`. + `total` and `argmax` are two distinct `borrow (RawBuf Int)` helpers, + called back-to-back on the same owned buffer in `main`; `argmax` + threads a 3-binder loop (`best_i`, `best_v`, `i`). +- Why it fits: composition of the #46 borrow fix (two borrows of one + buffer in sequence, buffer still owned + dropped by main), plus a + fill loop that reads its own in-place writes. +- Outcome: **builds + runs + leak-clean** (`allocs=3 frees=3 live=0`, + prints `20` / `5`). Clean on first try. See finding F4. + +## Findings + +### [spec_gap] F1 — the ledger's §Series substrate form `(ctor … (own (RawBuf a)) …)` does not parse +- Examples: `rbx_1_float_window_stats.ail` (original draft); `/tmp` + probes confirming generality. +- `design/models/0007` §Series writes the storage field of the Series + ADT as `(ctor S (own (RawBuf a)) (con Int) …)` (line 448). Authoring + that verbatim is rejected at the surface: + ``` + error: [surface-parse-error] parse error in type: `own` may only appear inside fn-type params or ret + ``` + This is **general, not RawBuf-specific**: an `own`-mode field on any + plain user ADT (`(data Outer (ctor O (own (con Inner))))`) is rejected + identically. So the canonical Series-substrate example in the design + ledger cannot be authored as written, and the ledger gives no + in-interface signpost to the working form. +- Why spec_gap: the parser rule ("`own` only in fn-type params/ret") and + the ledger's §Series ctor-field syntax are two incompatible readings of + what a substrate ADT looks like; the milestone shipped the parser rule + but the ledger still documents the forbidden form. A downstream author + copying the Series example hits a parse error with no ledger guidance. +- Recommended action: **ratify / tighten the ledger** — done this cycle: + the §Series ctor field is rewritten `(con RawBuf a)` (verified + authorable; the mode lives on fn params, not ADT fields). `own`-mode + ADT fields are not a planned feature, so no grammar work. Note: the + rest of the §Series listing is an illustrative sketch and its + construction `(new RawBuf lookback)` omits the element type — that + shape is entangled with F7/#51, so a full compile-verification of the + §Series listing belongs with the Series-substrate work, not here. + +### [retracted] F2 — bare `(con RawBuf (con Int))` in an ADT field — FALSE POSITIVE (stale binary) +- The fieldtester reported that a bare `(con RawBuf (con Int))` ADT field + still failed to resolve despite the #50 fix, citing + `[type-mismatch] expected RawBuf, got raw_buf.RawBuf`. +- **Retracted on triage.** The finding was produced against a stale + `target/release/ail` (built 17:22, before the #50 fix at 17:48). On a + freshly built binary the bare-name field resolves in every + configuration tested: + - ctor name == type name (`(data Box (ctor Box (con RawBuf (con Int))))`) — checks ok. + - ctor name != type name (`(data Box (ctor B (con RawBuf (con Int))))`, the fieldtester's exact repro) — checks ok. + - `examples/raw_buf_adt_field_bare.ail` — checks/builds/runs → `42`, `live=0`. +- Confirmed mechanism: the stale binary reproduces the error; the + rebuilt binary does not. The #50 fix (`a92bcaf`) is correct and + general. No code action; the real lesson is the process gap (F8). + +### [working] F3 — the Series-substrate composite works end-to-end (with the qualified-name workaround) +- Example: `rbx_1_float_window_stats.ail`. +- Once the field is spelled `(con raw_buf.RawBuf (con Float))`, the full + composite the §Series substrate describes works: a Float RawBuf filled + via loop, wrapped in a `Window` ADT with an Int `count`, read back + through TWO `borrow (Window)` helpers that each `match` the ADT and + drive a read loop off the bookkeeping count via `RawBuf.get` on a + borrow. Builds, prints `5.0`/`8.0`, and is leak-clean + (`allocs=4 frees=4 live=0`) — the Window ADT's drop cascade frees the + buffer slab. This is the substrate the pending Series milestone needs, + and (modulo F1/F2 surface friction) it holds together. +- Recommended action: **carry-on** (and use this as the Series-milestone + smoke fixture). + +### [working] F4 — borrow-receiver helpers compose; Bool/Int fills + reads are correct across widths +- Examples: `rbx_2_bool_sieve.ail`, `rbx_4_int_two_borrow_helpers.ail`. +- The #46 borrow-receiver fix holds under composition: `rbx_4` borrows + one owned Int buffer twice (`total` then `argmax`), each helper doing + multiple `RawBuf.get`/`.size` calls on its borrow param, with the + buffer still owned and dropped by main afterwards — clean, `live=0`, + prints `20`/`5`. `rbx_2` drives the i1/i8 Bool edge through a runtime-N + fill loop storing a *computed* Bool (`eq (i%2) 0`) and reads it back as + an `if` condition in a borrow helper — correct (`3`), `live=0`. A fill + loop that reads its own in-place writes (`rbx_4` fib: `RawBuf.get b + (i-1)` inside the same loop that wrote slot i-1) works — the in-place + `own→own` mutation makes prior slots visible to later iterations. +- These are the milestone's load-bearing wins for the downstream Series + decomposition; all clean on first or second try with no surprises. +- Recommended action: **carry-on**. + +### [working] F5 — `param-in` rejects a forbidden core primitive (`Unit`), message now names the allowed set +- Example: `rbx_3_unit_element_reject.ail`. +- `(new RawBuf (con Unit) n)` is rejected at `ail check` (exit 1): + ``` + [param-not-in-restricted-set] make_presence: type-arg `Unit` is not in the restricted set for type-variable `a` of `raw_buf.RawBuf` (allowed: one of ["Bool", "Float", "Int"]) + ``` + This extends the prior W2 (Str, user ADT) to the third class — a *core* + primitive — and empirically confirms the #48/B3 fix: the allowed set + now travels in the human-readable message. The restriction is on the + real element type regardless of its tier (core / heap / user ADT). +- **Caveat (re-verified):** this reject fires because the forbidden + element appears in a written fn-type position (`make_presence`'s `ret` + type). The restriction is NOT enforced at the bare construction site — + see F7. So F5 is "works *when the type is written in a signature*", + which the fixture happens to do. +- Recommended action: **carry-on** (the signature-position reject is + correct; the construction-site gap is F7 / issue #51). + +### [friction] F6 — `param-in` message renders the allowed set as a Rust-debug list, not the ledger's `{Int, Float, Bool}` +- Example: `rbx_3_unit_element_reject.ail` (and the re-run + `rawbuf_4_paramin_reject.ail`). +- The message renders `(allowed: one of ["Bool", "Float", "Int"])` — a + Rust `Vec` Debug rendering (square brackets, double-quoted, + alphabetised). The ledger (`design/models/0007` §4) and the prior B3 + framing write the set as `{Int, Float, Bool}`. The information is now + present (that was the #48 win), but the surface form is a leaked + internal representation: quotes and brackets an LLM author would not + expect, and the alphabetical order obscures the natural Int/Float/Bool + grouping. +- Why friction: the task (self-correct from the diagnostic) completes, + but the rendering is verbose/leaky vs. the clean set notation the + ledger implies. +- Recommended action: **plan** (tidy) — render the set as + `{Int, Float, Bool}` (brace-set, no quotes) to match the ledger. + Filed as issue #52. + +### [bug] F7 — `(new T …)` drops the explicit element annotation; an unobserved element type crashes codegen (issue #51) +- Surfaced during triage of F2/F5 against the fresh binary, not in the + fieldtester's original run (the stale binary masked it). +- A buffer whose element type is never *observed* by a later `get`/`set` + passes `ail check` and then crashes `ail build`: + ``` + (let b (new RawBuf (con Int) 3) (app print (app RawBuf.size b))) + ; ail check -> ok + ; ail build --alloc=rc -> Error: module raw_buf: def RawBuf_new__Unit: + ; internal: intrinsic fn RawBuf_new__Unit has no registered intercept + ``` + This hits two shapes: a **legitimate** allowed element used only for + its size (`RawBuf` above — the author wrote `(con Int)`, build + still crashes), and a **forbidden** element constructed locally + (`(new RawBuf (con Unit) 3)` — not rejected at check, same crash). +- Root: the `(new T …)` desugar drops `NewArg::Type` + (`crates/ailang-core/src/desugar.rs:1053`); `RawBuf.new`'s `a` appears + only in its result, so the call-site args never pin it; an unpinned + forall var defaults to `Unit` in monomorphisation + (`crates/ailang-codegen/src/subst.rs:56`), and `RawBuf_new__Unit` has + no registered intercept. Verified end-to-end. +- Why bug: a `check`-clean program crashes `build` (the exact class the + raw-buf usability mandate set out to eliminate), and the author's + explicit type annotation is silently discarded — contrary to the + language identity (mandatory annotations; every definition carries its + full type). +- Recommended action: **brainstorm** — honouring the annotation reverses + the milestone's "recover element by inference" decision (§ Term::New + desugar) and there is no type-ascription term in the AST today, so this + is a spec-level decision, not a one-line patch. Full analysis and + candidate directions in issue #51. + +### [process] F8 — the field test ran against a stale release binary +- The fieldtester executed `target/release/ail` without rebuilding it, + so its entire run reflected pre-#50 code. This produced one false + positive (F2) and masked a real defect class (F7) until the + orchestrator re-verified against a fresh build. +- Why it matters: a field test that runs stale silently inverts its own + purpose — it reports the *previous* shipped state as current. Every + "works"/"fails" line is suspect unless the binary under test is known + to include the changes the test claims to exercise. +- Recommended action: **plan** (process) — the field-test harness must + build the binary from the current tree before running (a + `cargo build --release -p ail` step, or run through `cargo run`), so + the consumer always exercises HEAD. Tracked as a skill/profile fix to + the fieldtester dispatch. + +## Recommendation summary + +| Finding | Class | Action | +|---|---|---| +| F1 §Series `own`-field form unparsable | spec_gap | ratify / tighten ledger (done this cycle) | +| F2 bare RawBuf ADT field unresolved despite #50 | retracted | none — stale-binary false positive | +| F3 Series-substrate composite works (qualified) | working | carry-on | +| F4 borrow helpers compose; Bool/Int fills correct | working | carry-on | +| F5 param-in rejects core primitive; names set | working | carry-on (signature-position only; cf. F7) | +| F6 param-in set rendered as Rust-debug list | friction | plan (tidy) — issue #52 | +| F7 `(new T …)` drops element annotation; unobserved element crashes codegen | bug | brainstorm — issue #51 | +| F8 field test ran against a stale release binary | process | plan (harness fix) | + +### Orthogonal observations (not raw-buf findings, noted in passing) +- Float comparison in a RawBuf read loop needs `float_gt` (not `gt`); + the `no-instance` diagnostic is exemplary — it names the missing + instance, the design rationale (IEEE-754 partial order), the exact + replacement ops (`float_gt` and siblings), and the contract ref. A + model diagnostic; no action. +- The known #49 Str-accumulator-loop leak was not hit — every fill loop + here uses `RawBuf.set` (in-place), so no superseded-heap-binder dec is + needed and all four new fixtures report `live=0`. diff --git a/examples/fieldtest/rbx_1_float_window_stats.ail b/examples/fieldtest/rbx_1_float_window_stats.ail new file mode 100644 index 0000000..03525e4 --- /dev/null +++ b/examples/fieldtest/rbx_1_float_window_stats.ail @@ -0,0 +1,92 @@ +; Fieldtest raw-buf comprehensive .1 (Axes 1+2+3+4 combined — the +; "Series substrate" shape with a Float element width). +; +; Task an LLM author is naturally given: "model a fixed-size window of +; Float samples with a running total, fill it from a loop, then report +; the window mean and the window maximum through read-only helpers." +; +; The natural decomposition wraps a RawBuf together with a +; bookkeeping `count` field in a user ADT (Window), exactly the Series +; substrate the ledger (design/models/0007 §Series) describes — an ADT +; holding `(own (RawBuf a))` plus Int bookkeeping. The buffer is filled +; via a (loop ...)/recur (runtime-N, not literal indices), and the +; read-back is factored into two `borrow (Window)` helpers (`mean`, +; `wmax`) that each pattern-match the ADT and drive a read loop off the +; bookkeeping count, reading the buffer through `RawBuf.get` on a borrow. +; +; This stresses, in one program: +; - Float element width through a fill loop (not just literal sets). +; - A RawBuf stored in a user ADT field (the #50 substrate shape). +; - TWO borrow-receiver helpers composing over the same wrapped buffer +; (the #46 borrow-receiver-read fix, under composition + behind a +; match on the ADT). +; - The drop cascade: the Window ADT owns the buffer; dropping the +; Window frees the slab. Leak-clean expected under AILANG_RC_STATS. +; +; Window of 4 samples: 2.0, 4.0, 6.0, 8.0. +; mean = 20.0 / 4 = 5.0 +; wmax = 8.0 +; Expected stdout: two lines, "5.0" then "8.0". + +(module rbx_1_float_window_stats + + ; NOTE (field test): the ledger's §Series substrate form writes the + ; storage field as `(own (RawBuf a))`. That does NOT parse here — `own` + ; in a ctor field position is rejected (surface-parse-error). And the + ; bare `(con RawBuf (con Float))` field gives a type-mismatch + ; (expected RawBuf, got raw_buf.RawBuf). The only form + ; that checks is the fully-qualified `raw_buf.RawBuf`. See findings. + (data Window + (ctor W (con raw_buf.RawBuf (con Float)) (con Int))) + + (fn build_window + (doc "Allocate a 4-slot Float buffer, fill slot i with (2*(i+1)), wrap in a Window with count=4.") + (type (fn-type (params (con Int)) (ret (own (con Window))))) + (params n) + (body + (let buf (new RawBuf (con Float) 4) + (let filled + (loop (b (con RawBuf (con Float)) buf) (i (con Int) 0) + (if (app ge i n) + b + (recur (app RawBuf.set b i (app int_to_float (app * 2 (app + i 1)))) + (app + i 1)))) + (term-ctor Window W filled n))))) + + (fn mean + (doc "Average of the first count slots, read through a borrow of the Window.") + (type (fn-type (params (borrow (con Window))) (ret (con Float)))) + (params w) + (body + (match w + (case (pat-ctor W buf count) + (app / + (loop (acc (con Float) 0.0) (i (con Int) 0) + (if (app ge i count) + acc + (recur (app + acc (app RawBuf.get buf i)) + (app + i 1)))) + (app int_to_float count)))))) + + (fn wmax + (doc "Maximum of the first count slots, read through a borrow of the Window.") + (type (fn-type (params (borrow (con Window))) (ret (con Float)))) + (params w) + (body + (match w + (case (pat-ctor W buf count) + (loop (mx (con Float) 0.0) (i (con Int) 0) + (if (app ge i count) + mx + (recur (if (app float_gt (app RawBuf.get buf i) mx) + (app RawBuf.get buf i) + mx) + (app + i 1)))))))) + + (fn main + (type (fn-type (params) (ret (con Unit)) (effects IO))) + (params) + (body + (let w (app build_window 4) + (seq (seq (app print (app mean w)) (do io/print_str "\n")) + (seq (app print (app wmax w)) (do io/print_str "\n"))))))) diff --git a/examples/fieldtest/rbx_2_bool_sieve.ail b/examples/fieldtest/rbx_2_bool_sieve.ail new file mode 100644 index 0000000..d7a95d9 --- /dev/null +++ b/examples/fieldtest/rbx_2_bool_sieve.ail @@ -0,0 +1,57 @@ +; Fieldtest raw-buf comprehensive .2 (Axes 1+2+3 — Bool element width +; through a fill loop, then counted via a borrow helper). +; +; Task an LLM author is naturally given: "mark which of the numbers +; 0..N are even in a flag buffer, then count how many flags are set." +; A flat Bool RawBuf is the natural storage for a flag/bitset array. +; +; The prior field test only stored a single Bool at a literal index +; (rawbuf_3_sensor_pair). This drives the i1/i8 Bool packing edge +; through a (loop ...)/recur FILL of runtime length N (one RawBuf.set +; per slot, the stored value being a *computed* Bool — the result of +; `eq (i % 2) 0`), and reads the flags back through a `borrow` helper +; (`count_set`) that drives off RawBuf.size and accumulates an Int. +; +; This stresses: +; - Bool stored/loaded across a loop, not a literal set — does the +; i1/i8 round-trip hold when the value is computed, not a `true` +; literal? +; - A borrow-receiver helper over a Bool buffer (the #46 fix on the +; Bool width). +; - `RawBuf.get` of a Bool used directly as an `if` condition inside +; the count loop. +; +; N = 6 -> flags for 0,1,2,3,4,5 -> even at 0,2,4 -> 3 set. +; Expected stdout: "3". + +(module rbx_2_bool_sieve + + (fn mark_even + (doc "Set slot i to (i is even) for i in 0..n. Linear own->own.") + (type (fn-type (params (own (con RawBuf (con Bool))) (con Int)) (ret (own (con RawBuf (con Bool)))))) + (params buf n) + (body + (loop (b (con RawBuf (con Bool)) buf) (i (con Int) 0) + (if (app ge i n) + b + (recur (app RawBuf.set b i (app eq (app % i 2) 0)) + (app + i 1)))))) + + (fn count_set + (doc "Count the set flags, reading the Bool buffer through a borrow.") + (type (fn-type (params (borrow (con RawBuf (con Bool)))) (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 (if (app RawBuf.get buf i) (app + acc 1) acc) + (app + i 1)))))) + + (fn main + (type (fn-type (params) (ret (con Unit)) (effects IO))) + (params) + (body + (let buf (new RawBuf (con Bool) 6) + (let buf (app mark_even buf 6) + (app print (app count_set buf))))))) diff --git a/examples/fieldtest/rbx_3_unit_element_reject.ail b/examples/fieldtest/rbx_3_unit_element_reject.ail new file mode 100644 index 0000000..a7fcf34 --- /dev/null +++ b/examples/fieldtest/rbx_3_unit_element_reject.ail @@ -0,0 +1,29 @@ +; Fieldtest raw-buf comprehensive .3 (Axis 5 — the param-in element-type +; restriction on a forbidden *core primitive*). +; +; The prior field test rejected RawBuf (the shipped fixture) and +; RawBuf (a user ADT). This probes the third natural mistake: a +; RawBuf of `Unit` — a core primitive that is NOT in the allowed set +; {Int, Float, Bool}. An LLM author might reach for `RawBuf` as a +; "presence buffer" / counter-of-slots before realising a Bool flag +; buffer is the right tool. The restriction must reject it, and per the +; B3 fix (#48) the diagnostic should now NAME the allowed set +; {Int, Float, Bool}, not just the offending type. +; +; Expected: `ail check` exits 1 with [param-not-in-restricted-set] +; naming `Unit` AND the allowed set {Int, Float, Bool}. + +(module rbx_3_unit_element_reject + + (fn make_presence + (doc "Try to allocate a RawBuf of Unit — forbidden element type.") + (type (fn-type (params (con Int)) (ret (own (con RawBuf (con Unit)))))) + (params n) + (body (new RawBuf (con Unit) n))) + + (fn main + (type (fn-type (params) (ret (con Unit)) (effects IO))) + (params) + (body + (let buf (app make_presence 3) + (do io/print_str "unreachable\n"))))) diff --git a/examples/fieldtest/rbx_4_int_two_borrow_helpers.ail b/examples/fieldtest/rbx_4_int_two_borrow_helpers.ail new file mode 100644 index 0000000..b4f5a55 --- /dev/null +++ b/examples/fieldtest/rbx_4_int_two_borrow_helpers.ail @@ -0,0 +1,76 @@ +; Fieldtest raw-buf comprehensive .4 (Axes 1+2+3 — Int buffer, an +; own->own fill helper across a function boundary, plus TWO distinct +; borrow-receiver helpers composed over the same buffer). +; +; Task an LLM author is naturally given: "fill a buffer of N slots with +; the Fibonacci sequence, then report both the total and the index of +; the largest element." The natural decomposition is three helpers: +; - `fill` : (own RawBuf, Int) -> own RawBuf (loop/recur, runtime N) +; - `total` : (borrow RawBuf) -> Int (read loop off .size) +; - `argmax`: (borrow RawBuf) -> Int (read loop, tracks idx) +; and a main that threads the owned buffer through `fill`, then borrows +; it TWICE in sequence (`total buf`, then `argmax buf`) — the natural +; "compute several summaries of one read-only buffer" shape. +; +; This stresses the #46 borrow-receiver fix under composition: two +; independent borrows of the same owned binder, each a helper that does +; multiple RawBuf.get / RawBuf.size calls on its borrow parameter. The +; prior rawbuf_1 had a single borrow helper; this has two, called back +; to back on the same buffer, with the buffer still owned (and dropped) +; by main afterwards. +; +; Fib(0..5) = 1,1,2,3,5,8 (seeding fib(0)=fib(1)=1). +; total = 1+1+2+3+5+8 = 20 +; argmax = index 5 (value 8 is largest) +; Expected stdout: "20" then "5". + +(module rbx_4_int_two_borrow_helpers + + (fn fill + (doc "Fill slot i with fib(i) for i in 0..n. Linear own->own.") + (type (fn-type (params (own (con RawBuf (con Int))) (con Int)) (ret (own (con RawBuf (con Int)))))) + (params buf n) + (body + ; Seed slots 0 and 1 to 1, then each later slot = sum of prior two, + ; read back from the buffer itself via RawBuf.get on the owned `b`. + (loop (b (con RawBuf (con Int)) buf) (i (con Int) 0) + (if (app ge i n) + b + (recur (app RawBuf.set b i + (if (app le i 1) + 1 + (app + (app RawBuf.get b (app - i 1)) + (app RawBuf.get b (app - i 2))))) + (app + i 1)))))) + + (fn total + (doc "Sum every slot, borrow receiver.") + (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 argmax + (doc "Index of the largest slot, borrow receiver. Tracks (best_i, best_v).") + (type (fn-type (params (borrow (con RawBuf (con Int)))) (ret (con Int)))) + (params buf) + (body + (loop (best_i (con Int) 0) (best_v (con Int) (app RawBuf.get buf 0)) (i (con Int) 0) + (if (app ge i (app RawBuf.size buf)) + best_i + (if (app gt (app RawBuf.get buf i) best_v) + (recur i (app RawBuf.get buf i) (app + i 1)) + (recur best_i best_v (app + i 1))))))) + + (fn main + (type (fn-type (params) (ret (con Unit)) (effects IO))) + (params) + (body + (let buf (new RawBuf (con Int) 6) + (let buf (app fill buf 6) + (seq (seq (app print (app total buf)) (do io/print_str "\n")) + (seq (app print (app argmax buf)) (do io/print_str "\n"))))))))