From 43e3b210800afe1dd27b0241d68a8169cc217cf2 Mon Sep 17 00:00:00 2001 From: Brummel Date: Sat, 30 May 2026 17:23:29 +0200 Subject: [PATCH] =?UTF-8?q?audit:=20raw-buf=20usability=20repair=20?= =?UTF-8?q?=E2=80=94=20cycle=20tidy=20(refs=20#7)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Close-out audit for the raw-buf usability repair (range 8e9f0f0..HEAD: B1 #46, B2 #47, B3 #48, B5 loop-result drop, docs). Architect drift review (against design/INDEX.md + the kernel-extensions model): all three lockstep-invariant pairs undisturbed (INTERCEPTS ↔ intrinsic markers, lower_app ↔ is_static_callee, Pattern::Lit ↔ pre_desugar_validation — none touched; the edits sit in linearity, synth_with_extras, and drop.rs). Every fix shipped a property-protecting RED test. B3 brings the diagnostic into conformance with the model's pre-existing §4 promise rather than opening a gap. One drift item raised and fixed here: the B4 ratification paragraph in design/models/0007 §RawBuf overstated the set non-enforcement as unconditional. Verified: a double-consume of an own-param RawBuf inside a fn with explicit modes fires [use-after-consume]; it slips through only where the linearity activation gate skips the fn (paramless main, or implicit-mode params). The paragraph now states the enforcement is gated, names the gate, and gives both the caught and the uncaught case. Regression (commands.regression, verbatim): - bench/check.py EXIT 0 — 34 metrics; 0 regressed, 34 stable - bench/compile_check.py EXIT 0 — 24 metrics; 0 regressed, 24 stable - bench/cross_lang.py EXIT 0 — 25 metrics; 0 regressed, 25 stable No baseline moved; carry-on. Two forward-queue items filed during the repair, both out of scope here: - #49 per-iteration leak of superseded heap loop-binder values across recur (a Str accumulator leaks; RawBuf does not — set is in-place). - #50 bare RawBuf not auto-imported in type-constructor positions (a RawBuf in a user ADT field needs the qualified raw_buf.RawBuf); the RawBuf-in-ADT substrate itself works (builds, runs, drop cascades leak-clean) with the qualified name. cycle raw-buf-usability tidy (clean). --- design/models/0007-kernel-extensions.md | 33 ++++++++++++++----------- 1 file changed, 19 insertions(+), 14 deletions(-) diff --git a/design/models/0007-kernel-extensions.md b/design/models/0007-kernel-extensions.md index c21c5f9..54fb716 100644 --- a/design/models/0007-kernel-extensions.md +++ b/design/models/0007-kernel-extensions.md @@ -406,20 +406,25 @@ existing memory-model — RC + uniqueness as the canonical mutation story. The `own → own` signature of `RawBuf.set` is a *threading -discipline*, not runtime-enforced single-use. The mode annotations -drive the borrow/consume analysis and the in-place-vs-copy codegen -decision; they do not make a second consume of the same owned -binder a check-time error. An author who hands the same owned -buffer to two consuming calls -(`(let a (RawBuf.set buf 0 1)) (let b (RawBuf.set buf 1 2))`) -gets two bindings aliasing one slab — the second mutation is -visible through the first. This is the same non-enforcement that -holds for every owned value in the language (owned `Str`, owned -ADTs); `RawBuf`'s in-place `own → own` surface is merely the first -place the alias produces a *mutated-in-place* surprise rather than -a benign re-read. Single-use of an owned buffer is the author's -responsibility. Full linear enforcement, if wanted, is tracked -separately (Issue #22 territory). +discipline* enforced by the uniqueness/linearity check where that +check is active, not a runtime guard. The mode annotations drive +the borrow/consume analysis and the in-place-vs-copy codegen +decision. Where the linearity check runs — a fn whose parameters +all carry explicit `own`/`borrow` modes — a second consume of the +same owned binder *is* rejected at check time (`use-after-consume`): +a helper `(fn f (params (own (RawBuf Int))) …)` that hands its +buffer to two consuming calls is caught. The check has an +activation gate, though: it does not run on a fn with no parameters +(a paramless top-level `main`) or one with implicit-mode parameters. +A double-consume written directly in such an unchecked context — +`(let a (RawBuf.set buf 0 1)) (let b (RawBuf.set buf 1 2))` inside a +paramless `main` — is not caught, and the two bindings alias one +slab (the second mutation is visible through the first). `RawBuf`'s +in-place `own → own` surface is the first place this alias produces +a *mutated-in-place* surprise rather than a benign re-read. Single- +use of an owned buffer in an unchecked context is the author's +responsibility. Tightening the activation gate, or full linear +enforcement, is tracked separately (Issue #22 territory). Storage at the LLVM-IR level is type-specialised: the Rust intercept registered for `RawBuf` dispatches on the element type