fieldtest: raw-buf comprehensive — 4 examples, 8 findings (refs #7)
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<Int>` 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
This commit is contained in:
@@ -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
|
||||
|
||||
@@ -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<Float>` 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<Bool>` 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<Int>, got raw_buf.RawBuf<Int>`.
|
||||
- **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<String>` 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<Int>` 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`.
|
||||
@@ -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<Float> 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<Float>, got raw_buf.RawBuf<Float>). 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")))))))
|
||||
@@ -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)))))))
|
||||
@@ -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<Str> (the shipped fixture) and
|
||||
; RawBuf<Tick> (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<Unit>` 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")))))
|
||||
@@ -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"))))))))
|
||||
Reference in New Issue
Block a user