docs(raw-buf): refresh fixture outcomes; ratify set non-enforcement (refs #7)

- rawbuf_1_score_table / rawbuf_2_running_max: the header OUTCOME blocks
  described the pre-fix breakage (does-not-check / unknown-variable).
  Those defects are fixed (B1 #46, B2 #47, B5); update the comments to
  the current state — both check, build, run to their expected values
  and are leak-clean under AILANG_RC_STATS. The files now serve as
  positive regression examples, not bug repros.

- design/models/0007 §RawBuf: ratify the fieldtest's B4 spec_gap. The
  `own -> own` signature of RawBuf.set is a threading discipline, not
  runtime-enforced single-use; a double-consume of the same owned buffer
  aliases one slab (consistent with every owned value in the language).
  State that single-use is the author's responsibility and full linear
  enforcement is Issue #22 territory.

Surfaced by the raw-buf fieldtest (docs/specs/0058).
This commit is contained in:
2026-05-30 17:14:39 +02:00
parent 8bcdae1b53
commit d5cc6e96b6
3 changed files with 35 additions and 17 deletions
+12 -11
View File
@@ -11,17 +11,18 @@
;
; 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`.
; This was the fieldtest repro for two defects, both now fixed:
; - B1 (#46): the `total` helper, which takes `borrow (RawBuf Int)`
; and only calls RawBuf.size / RawBuf.get on the receiver, was
; falsely rejected with [consume-while-borrowed]. The linearity
; pass now resolves the type-scoped borrow-receiver ops, so the
; borrow helper checks clean.
; - B2 (#47): the `fill` loop, threading the owned buffer through a
; `recur`, failed codegen with `unknown variable: b`. The synth
; type-replay now descends through `loop` with the loop binders in
; scope.
; OUTCOME (current): checks, builds, runs; prints 35. Leak-clean under
; AILANG_RC_STATS (the owned buffer drops at scope close, B5).
(module rawbuf_1_score_table
+7 -6
View File
@@ -11,12 +11,13 @@
;
; 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.
; This was the fieldtest repro for B2 (#47): `ail check` passed but
; `ail build` FAILED at codegen with `unknown variable: b` — the synth
; type-replay walked the `loop` body without the loop binders in scope.
; Now fixed: the replay descends through `loop` with its binders bound.
; OUTCOME (current): checks, builds, runs; prints 16. Leak-clean under
; AILANG_RC_STATS (the loop-threaded owned buffer drops at scope close,
; B5 — the let-bound loop result is now registered for scope-close drop).
(module rawbuf_2_running_max
(fn main