docs/BUILT.md states how a dev build decides a dyn view is stale.

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