From 26fc9d82a637007f0e6d890964b992106a583c3c Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Sat, 26 Sep 2026 06:17:59 +0700 Subject: [PATCH] docs/BUILT.md states how a dev build decides a dyn view is stale. --- docs/BUILT.md | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) diff --git a/docs/BUILT.md b/docs/BUILT.md index c1cf78c2..f2ea2a5a 100644 --- a/docs/BUILT.md +++ b/docs/BUILT.md @@ -3068,6 +3068,31 @@ the result means — a `Vec` can only be borrowed, a fixed array or a string can chooses between the two — so the second name expressed no choice a reader could make. One name, `slice`, over everything that has elements; the warning is where it bites. +### A dyn view's dev check: which frame, which block + +A typed container crosses into dyn as a view of its storage wherever that storage is, and a `--dev` build traps +(`DynStale`) the first time a view is used after its storage went away. Five files share the protocol: + +- `check.ml`'s `frame_root` says when the storage is the calling function's own frame — a local, a parameter, a + field or array element of one, a slice cut straight from a local array, or a temporary `box` bound to a slot of its + own — and passes that as the view's `here` flag. +- `emit.ml` and `x86.ml` zero a `serial` word in every shadow frame at the push. +- `flan_dyn.c`'s `view_make` claims a serial for the frame at the crossing (`flan_dev_frame_claim`, which numbers a + frame once) and keeps the frame's address, its serial and the function's name. Otherwise it asks the allocation + registry for the smallest live block holding the address and keeps that block's base and note sequence. +- Every read or write checks first. A frame is alive when it is still on the chain from `flan_frame_head` *and* has + the same serial: the walk is needed because dead stack keeps its old bytes, serial included, and the serial is + needed because the next call at the same depth lands at the same address. A block is alive when the registry probe + on its base finds the same sequence not yet dead, which a free, a free-all, an arena's destroy and a `Vec`'s growth + (for the block it left) all end. + +A view's aggregate element inherits its parent's record, except inside a `Vec` (checked against the `Vec`'s block, +since growth moves it) and through a slice (looked up afresh). What neither table knows is not checked: a global, +rodata, C memory, and a caller's local reached through a slice parameter. That last one is deliberate — stamping it +with the callee's frame would trap on a live array after the callee returns. A release build records nothing and +checks nothing; a stale view there reads whatever the memory holds now. One case is refused at compile time instead: +a dyn global's initialiser taking a view of what it built, which is gone before anything can read it. + ### Three amendments to a frozen spec, and one addition **1. `free-all` is retain-capacity, and `arena-destroy` is the operation that hands pages back.** The spec's table has