audit: raw-buf usability repair — cycle tidy (refs #7)
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).
This commit is contained in:
@@ -406,20 +406,25 @@ existing memory-model — RC + uniqueness as the canonical
|
|||||||
mutation story.
|
mutation story.
|
||||||
|
|
||||||
The `own → own` signature of `RawBuf.set` is a *threading
|
The `own → own` signature of `RawBuf.set` is a *threading
|
||||||
discipline*, not runtime-enforced single-use. The mode annotations
|
discipline* enforced by the uniqueness/linearity check where that
|
||||||
drive the borrow/consume analysis and the in-place-vs-copy codegen
|
check is active, not a runtime guard. The mode annotations drive
|
||||||
decision; they do not make a second consume of the same owned
|
the borrow/consume analysis and the in-place-vs-copy codegen
|
||||||
binder a check-time error. An author who hands the same owned
|
decision. Where the linearity check runs — a fn whose parameters
|
||||||
buffer to two consuming calls
|
all carry explicit `own`/`borrow` modes — a second consume of the
|
||||||
(`(let a (RawBuf.set buf 0 1)) (let b (RawBuf.set buf 1 2))`)
|
same owned binder *is* rejected at check time (`use-after-consume`):
|
||||||
gets two bindings aliasing one slab — the second mutation is
|
a helper `(fn f (params (own (RawBuf Int))) …)` that hands its
|
||||||
visible through the first. This is the same non-enforcement that
|
buffer to two consuming calls is caught. The check has an
|
||||||
holds for every owned value in the language (owned `Str`, owned
|
activation gate, though: it does not run on a fn with no parameters
|
||||||
ADTs); `RawBuf`'s in-place `own → own` surface is merely the first
|
(a paramless top-level `main`) or one with implicit-mode parameters.
|
||||||
place the alias produces a *mutated-in-place* surprise rather than
|
A double-consume written directly in such an unchecked context —
|
||||||
a benign re-read. Single-use of an owned buffer is the author's
|
`(let a (RawBuf.set buf 0 1)) (let b (RawBuf.set buf 1 2))` inside a
|
||||||
responsibility. Full linear enforcement, if wanted, is tracked
|
paramless `main` — is not caught, and the two bindings alias one
|
||||||
separately (Issue #22 territory).
|
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
|
Storage at the LLVM-IR level is type-specialised: the Rust
|
||||||
intercept registered for `RawBuf` dispatches on the element type
|
intercept registered for `RawBuf` dispatches on the element type
|
||||||
|
|||||||
Reference in New Issue
Block a user