M2 item 3: typed containers cross into dyn as views of permanent storage

# Conflicts: # lib/emit.ml # runtime/flan_dyn.h
2026-09-20 11:18:18 +07:00 · 2026-09-20 11:18:18 +07:00 · eec9efc94c
commit eec9efc94c
parent 3a9088604e c765aad70f
13 changed files with 1310 additions and 31 deletions
--- a/FIX.org
+++ b/FIX.org
@ -420,7 +420,85 @@ rename. typed-flan branch freezes the static language pre-dyn.
   Left open until the lane is built: whether the descriptor points at the
   container or is a fattened slice stored beside it. That only bites if the
   container can grow and move, which would leave a push through dyn holding
-   a stale pointer.
+   a stale pointer. — LANDED. Settled: a Vec view holds the address of the
   Vec's own header and reads its ptr/len live on every operation, so a push
   that reallocates cannot go stale — there is no snapshot to invalidate,
   because flan_vec_grow overwrites that same header in place. A slice and a
   fixed array cannot grow, so a flat view snapshots pointer and length once,
   which is sound for both and is not the weaker half of an asymmetric
   choice — pointing a flat view at its own value's slot instead would be
   worse, since a slot's lifetime is not the slice's. The element set is i64,
   f64 and bool only: a string element's dyn form is a pointer into the
   collector's heap, and a typed container's storage is memory the collector
   never scans, so a wider set would let a write plant a live reference
   nothing traces. (Vec string) and (Map K V) keep the refusal [box] already
   gave every container. Both backends, runtime/flan_dyn.c and .h, checker
   tests, an acceptance row per backend, and a survey program
   (dyn-view.flan) proving the view against both a growing Vec and a fixed
   array/slice, plus its own two trap modes.
   REVIEW, 2026-09-20: relocation was proved sound but relocation was not
   the hazard that mattered — a view can outlive the frame its Vec header
   sits in, which nothing could reach before this lane because [box]
   refused every container outright. Three routes, all newly constructible,
   all stack-use-after-return: returning a view, stashing one in a dyn
   global, leaving one behind across a condition transfer. AUTHOR'S RULE:
   on the dynamic side Flan aims where Clojure and Common Lisp are — holding
   a value should not hand you garbage — so a container may cross into dyn as
   a view only when its own storage is permanent — a global's.
   [permanent_root] in check.ml decides it: a global, a field of one, an
   element of a permanent ARRAY (an element of a slice is NOT — a slice holds
   only ptr+len, and what they point at can be a frame already gone; the [At]
   arm steps every index of a multi-index [(at g i j)] the way [indexed] does
   and demands an array at each level, because the whole index list rides on
   one node and reading the target's type alone settled level zero only), or
   a slice cut directly from one at the call (the trace is lost the moment
   it is bound to a name first). Everything else — a local, a parameter, a
   temporary, anything behind a (Ptr T) — is refused by name, pointing at
   the defvar spelling that works. A heap-held header is not expressible
   soundly at this milestone for a structural reason rather than a missing
   feature: a (Ptr (Vec i64)) taken off a heap block and one taken off a
   local are the same type, so admitting a Ptr as permanent would readmit
   the exact hole this closes.
   The rule is a narrowing, not a proof, and flan_dyn.h states the property
   that actually holds: a view is exactly as stale-safe as the thing it is a
   view of, no more and no less. A global [i64] whose data was cut from a
   frame that has since returned still passes [permanent_root] and still
   reads a dead frame. What the guard closes is the routes the checker can
   see, not every route.
   An arena-held header is not a separate case for [permanent_root] — an
   arena changes where a Vec's elements live, never where its own header
   (the binding) lives, so the cases above already decide it — but that is
   coverage of the HEADER's lifetime only, and releasing the arena under a
   live view is a separate hazard handled at RUN time, not here.
   [view_vec_check] in flan_dyn.c is what handles it: a Vec records its
   allocator's epoch and every view operation re-checks it, so (free-all ar)
   with a live view over an arena-grown global Vec traps cleanly and by name
   at the next read — verified. (arena-destroy ar) is the gap: it frees the
   allocator block itself, so the epoch [view_vec_check] goes to read is
   freed memory. Run plainly it happens to trap anyway — the freed block
   still held the bumped epoch — but that is the allocator not having reused
   it yet, not a check that held; under ASan the same program is a
   heap-use-after-free in [view_vec_check] before it decides anything. Left
   standing rather than fixed with this lane: the typed side has it
   identically in [flan_vec_check], flan_rt.c, which reads the same freed
   allocator's epoch, so it is a repo-level question about arena-destroy's
   ordering and not about views.
   Three more, all in the runtime rather than the boundary: [view_vec_check]
   recursed into itself rendering the very view it had just declared unsafe
   to read (fixed by never rendering it — the sentence names the epochs and
   nothing else); [dyn_equal]'s VEC arm read raw [len]/[items] regardless of
   kind, so two views with different contents compared equal and a map keyed
   by a view collided with every other view (fixed with view-aware
   length/element readers, [vecish_len]/[vecish_at]); and the three
   restatements of flan_vec's layout (flan_rt.c, flan_dyn.c, dyn_ops.c) had
   nothing tying them together despite a comment's claim that they did — a
   [layout] probe on each, compared field by field in dyn_ops.c's new
   "layout" mode, makes a disagreement a FAIL line instead of a silent
   corruption.
 4. nil: arrives with maps. nil <-> None at (Option T) boundaries, trap at
   bare T, (Some nil) unconstructible. — LANDED, 3c1fb1b. The bare-T trap is
   split: a literal nil the checker can see is refused at compile time, in
--- a/lib/check.ml
+++ b/lib/check.ml
@ -1441,6 +1441,138 @@ let no_dyn_yet loc ~into t extra =
    "%s does not cross into %s yet%s"
    (Types.to_string t) (if into then "dyn" else "a written type") extra
 (* M2 item 3: a typed container crossing into dyn as a view. The element set
   is exactly [unboxable] above — i64, f64, bool — and that is not a smaller
   version of the same cut for the same reason: every other element type
   would need [box] to run on IT too, and a string element's dyn form is a
   pointer into the collector's heap, while a typed container's storage is
   arena or stack memory the collector never scans. Writing that pointer
   into memory nobody roots is a live reference the collector could free out
   from under — the hazard runtime/flan_dyn.h's view section states at
   length — and i64/f64/bool carry no pointer, so a view restricted to them
   cannot manufacture it. It is a compile-time refusal here rather than a
   run-time one because the element type is exactly what the checker already
   knows at the crossing. The FLAN_VIEW_* constants are runtime/flan_dyn.h's;
   this is the compiler's one copy of the same table. *)
 let view_elem (t : Types.t) : int64 option =
  match t with
  | Types.Int Types.I64 -> Some 0L   (* FLAN_VIEW_I64 *)
  | Types.Float Types.F64 -> Some 1L (* FLAN_VIEW_F64 *)
  | Types.Bool -> Some 2L            (* FLAN_VIEW_BOOL *)
  | _ -> None
 let view_elem_lit loc (k : int64) =
  mk loc (Types.Int Types.I32) (Tast.Int (k, Types.I32))
 let view_not_yet loc (container : Types.t) (elem : Types.t) =
  no_dyn_yet loc ~into:true container
    (Printf.sprintf
       ". A container view at this milestone holds i64, f64 or bool \
        elements only, and %s is not one of the three. The restriction \
        exists for the string case: a dyn string's form is a pointer into \
        the collector's heap, and a typed container's storage is memory the \
        collector never scans, so a write through a view over strings could \
        plant a pointer where nothing will ever trace it. Every other \
        element type is refused with it rather than admitted one width at a \
        time"
       (Types.to_string elem))
 (* M2 item 3's second guard, added on review: a view's descriptor holds an
   address into the container's own storage, chased fresh on every
   operation, which is what makes a Vec's growth safe — but it is also what
   makes a *dangling* container's storage a live hazard nothing catches
   until somebody reads through the view. A view returned from the function
   whose frame the Vec lived in, stashed in a global and read after that
   frame is gone, or left behind when a condition transfer unwinds it, are
   all stack-use-after-return once box stopped refusing containers outright
   — reachable now for the first time, not a pre-existing hole this lane
   merely inherited.
   On the dynamic side Flan aims where Clojure and Common Lisp are: holding
   a value should not hand you garbage. Treating a view as a bare pointer and
   calling the lifetime the programmer's problem is the Odin answer, and
   neither Odin nor C stops it — this guard is the trade going the other way,
   refused rather than merely documented.
   What it is NOT is a proof. runtime/flan_dyn.h states the actual property:
   the view is exactly as stale-safe as the thing it is a view of, no more
   and no less. This guard narrows what a view can be taken of; it does not
   make the underlying storage outlive anything. A global [[T]] slice whose
   data was cut from a frame that has since returned still passes here, and
   reading through the view then reads a dead frame. So this is a guard that
   closes the routes the checker can see, not a guarantee that a dyn value
   never dangles.
   [permanent_root] asks whether an expression's own address — the one a
   view's pointer will chase — is guaranteed to outlive every frame, which is
   true of exactly one thing at this milestone: a global. A field of a
   permanent value is permanent at the same fixed offset from it, and so is
   an element of a permanent *array* — both are still inside the permanent
   value's own storage. An element of a permanent *slice* is not: a slice is
   ptr+len, so a global [[T]] holds only the two words, and the storage they
   point at can be a frame that has already gone. The [At] arm below is where
   that distinction is made, and it is made per index rather than once: an
   [(at g i j)] is a single node carrying the whole index list, so the arm
   steps the list the way [indexed] does and an array level at every step is
   what it demands. Reading only the target's type would settle level zero
   and let a slice at any later level through — which it did, and the
   accepted program printed a returned frame's contents. A slice built directly from
   [(slice T lo hi)] inherits the
   permanence of the [T] it was cut from — unwrapped here because that is
   the one shape still carrying the trace back to it; once a slice has been
   bound to a name the trace is gone and it is refused; the spelling that
   keeps it is to view the slice expression directly, the way this file's
   own survey program does.
   Everything else — a local, a parameter, a temporary, anything reached
   through a [Ptr] — answers false. A [Ptr] is refused rather than trusted
   because a heap-allocated block and a frame slot are the same type: a
   [(Ptr (Vec i64))] taken from a heap allocation would be sound to view, but
   the same type is what [(addr some-local)] answers too, and the checker
   cannot tell the two apart. Admitting one admits the other, which is the
   whole hazard this guard exists to close — so until a Flan type exists
   that says "durably heap-owned" and a [Ptr] does not, a container reached
   through one is refused rather than guessed at. An arena-held container is
   not a separate case: an arena changes where a Vec's *elements* live, never
   where its own header — the value a name is bound to — lives, so a Vec
   grown from an arena is exactly as permanent as the binding that holds it,
   already covered by the cases above. *)
 let rec permanent_root (e : Tast.expr) : bool =
  match e.Tast.e with
  | Tast.Global _ -> true
  | Tast.Field (target, _) -> permanent_root target
  | Tast.Prim (Tast.At, target :: idx) ->
    (* [(at g i j)] is ONE node carrying every index, so the target's own type
       is only level zero and asking about it alone misses a slice reached at
       any later level. Step the list the way [indexed] does — that walk is
       the definition of which levels exist — and require every level stepped
       to be an array. *)
    let rec all_array ty = function
      | [] -> true
      | _ :: rest ->
        (match ty with
         | Types.Array (_, elem) -> all_array elem rest
         | _ -> false)
    in
    all_array target.Tast.ty idx && permanent_root target
  | Tast.Prim (Tast.Slice, [ target; _; _ ]) -> permanent_root target
  | _ -> false
 let view_not_permanent loc (container : Types.t) =
  Loc.failk "check/dyn-view-lifetime" loc
    "%s does not cross into dyn as a view here — its storage is not known \
     to outlive the view, and a view is exactly as stale-safe as the thing \
     it is a view of, no more and no less. A global's storage does outlive \
     it: (defvar g %s ...) viewed from anywhere reads storage fixed for the \
     process, and so does a field or an array element of one. A local, a \
     parameter, a temporary, anything reached through a slice at any index \
     level — even a global one, which holds only ptr+len and can point at a \
     frame that is gone — or \
     anything reached through a (Ptr T) is refused: the checker cannot tell \
     a heap-durable pointer from a frame's own, and admitting one admits \
     the other"
    (Types.to_string container) (Types.to_string container)
 let box loc (e : Tast.expr) : Tast.expr =
  let dyn sym args = rt loc Types.Dyn sym args in
  match e.Tast.ty with
@ -1465,11 +1597,47 @@ let box loc (e : Tast.expr) : Tast.expr =
       nothing a dyn could hold. The absent dyn value is nil, which is a \
       literal here: write nil"
  | Types.Never -> e
-  | Types.Vec _ | Types.Map _ | Types.Slice _ | Types.Array _ ->
+  (* A view, not a copy: the box holds one word naming where the elements
     live and what one of them is, and every read or write goes straight
     through to the container's own storage — see runtime/flan_dyn.h's
     view section for the whole of the argument, including why the
     descriptor points AT the container (a Vec's own header address)
     rather than snapshotting its ptr+len. That is what makes a push
     through the view safe even though a Vec can grow and move: there is
     no snapshot for the growth to invalidate. A slice and a fixed array
     cannot grow, so a snapshot taken once at the crossing is sound for
     both, and they share [flan_dyn_view_flat]. *)
  (* The element check runs before the lifetime one in all three arms, and
     the order is load-bearing rather than incidental: the lifetime message
     points at [(defvar g ...)] as the spelling that works, and for an
     element type no view can carry — a string, an i32 — the global spelling
     is refused too, so the wrong order hands the programmer advice that
     fails when they take it. Whichever refusal is unconditional wins. *)
  | Types.Vec elem ->
    (match view_elem elem with
     | None -> view_not_yet loc e.Tast.ty elem
     | Some k ->
       if not (permanent_root e) then view_not_permanent loc e.Tast.ty
       else dyn "flan_dyn_view_vec" [ e; view_elem_lit loc k ])
  | Types.Slice elem ->
    (match view_elem elem with
     | None -> view_not_yet loc e.Tast.ty elem
     | Some k ->
       if not (permanent_root e) then view_not_permanent loc e.Tast.ty
       else dyn "flan_dyn_view_flat" [ e; view_elem_lit loc k ])
  | Types.Array (n, elem) ->
    (match view_elem elem with
     | None -> view_not_yet loc e.Tast.ty elem
     | Some k ->
       if not (permanent_root e) then view_not_permanent loc e.Tast.ty
       else
         dyn "flan_dyn_view_flat"
           [ e; mk loc dyn_i64 (Tast.Int (n, Types.I64)); view_elem_lit loc k ])
  | Types.Map _ ->
    no_dyn_yet loc ~into:true e.Tast.ty
      ". The dyn container at this milestone is the runtime's own, from \
-       (vec-new dyn); a typed container has a representation the dyn runtime \
+       (map-new dyn); a typed (Map K V) has a representation the dyn \
-       cannot walk"
+       runtime cannot walk"
  (* [Option] is on this list in name only: [expect] intercepts it before
     [box] ever sees one — [box_option] is the real answer, M2 item 4 — so
     this arm only fires for a direct caller that hands [box] an Option
@ -2078,6 +2246,36 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr =
    (match ctx.defers with
     | [] -> r
     | ds -> mk loc Types.Never (Tast.Do (ds @ [ r ])))
  (* (set (at target i) x) against a dyn target — a dyn vec from (vec-new
     dyn), or a typed container's own view (M2 item 3) — is a call and not a
     place: [flan_dyn_set_at] tag-checks [x]'s dyn tag against what the vec
     or the view holds and traps on a mismatch, which is not a memory write
     [Tast.Set] could express through a pointer. [target] is checked once,
     here, and handed to [vec_at]/[indexed] unchecked in the [else] branch
     below rather than re-checked by [check_place] — checking it twice would
     evaluate a target with a side effect twice. A dyn target indexed more
     than once — nothing in this milestone builds one — still falls to the
     ordinary [Ast.Set] arm below, and [indexed] refuses it by name. *)
  | Ast.Set (Ast.Pindex (target, [ idx ]), v) ->
    let target = check ctx target in
    if target.Tast.ty = Types.Dyn then
      let i = check ctx ~want:Types.Dyn idx in
      let v = check ctx ~want:Types.Dyn v in
      expect ctx loc ~want
        (rt loc Types.Unit "flan_dyn_set_at" [ target; i; v ])
    else begin
      let p, pty =
        match target.Tast.ty with
        | Types.Vec _ ->
          let pp, ty = vec_at ctx loc target [ idx ] in
          Tast.Pderef pp, ty
        | _ ->
          let iidx, ty = indexed ctx target [ idx ] in
          Tast.Pindex (target, iidx), ty
      in
      let v = check ctx ~want:pty v in
      expect ctx loc ~want (mk loc Types.Unit (Tast.Set (p, v)))
    end
  | Ast.Set (p, v) ->
    let p, pty = check_place ctx loc p in
    let v = check ctx ~want:pty v in
--- a/lib/emit.ml
+++ b/lib/emit.ml
@ -2640,6 +2640,15 @@ and prim f (e : Tast.expr) (p : Tast.prim) (args : Tast.expr list) =
                 Passing the header by value here would hand the runtime a
                 copy to grow and leave the caller's untouched. *)
              | Types.Vec _ | Types.Map _ -> [ "ptr " ^ addr f a ]
              (* A fixed array crossing into a dyn view (M2 item 3) needs its
                 address for the same reason a Vec or a Map does here — the
                 view reads through it live, and passing the value would hand
                 the runtime a copy nothing writes back through. Every other
                 [Rt] caller of an array argument is [flan_dyn_view_flat],
                 which takes the address and never mutates the array's shape,
                 so this is not the move-only argument Vec/Map's comment is
                 about — it is simply the only way to view rather than copy. *)
              | Types.Array _ -> [ "ptr " ^ addr f a ]
              | t -> [ ll t ^ " " ^ value f a ])
           args)
    in
@ -3388,6 +3397,8 @@ declare i32 @flan_dyn_need_bool(i64)
 declare i32 @flan_dyn_is_nil(i64)
 declare i64 @flan_dyn_need_not_nil(i64)
 declare i32 @flan_dyn_truthy(i64)
 declare i64 @flan_dyn_view_vec(ptr, i32)
 declare i64 @flan_dyn_view_flat(ptr, i64, i32)
 declare void @flan_dyn_root_push(ptr)
 declare void @flan_dyn_root_push_desc(ptr, ptr)
 declare void @flan_dyn_root_pop(i64)
--- a/lib/x86.ml
+++ b/lib/x86.ml
@ -1461,6 +1461,13 @@ let classify_c (l : loc) (t : Types.t) =
  | Types.String | Types.Slice _ -> [ Aint (l, Types.Ptr Types.Unit); Alen l ]
  | Types.Unit | Types.Never -> []
  | Types.Vec _ | Types.Map _ -> [ Aptr l ]
  (* A fixed array crossing into a dyn view (M2 item 3) needs its address for
     the same reason: the view reads through it live and a copy would leave
     the caller's own array unseen by later writes through the view. Every
     [Rt] call that takes an array argument is [flan_dyn_view_flat], which
     never mutates the array's shape, so this is not the move-only case
     Vec/Map is. *)
  | Types.Array _ -> [ Aptr l ]
  | _ when is_agg t ->
    unsupported "aggregate %s across the C boundary" (Types.to_string t)
  | _ when is_float t -> [ Aflt (l, t) ]
@ -2708,7 +2715,7 @@ and call_native f ~sym ?(chan = false) ~(args : Tast.expr list) ~rty dst =
    List.map
      (fun (a : Tast.expr) ->
         (match a.Tast.ty with
-          | Types.Vec _ | Types.Map _ -> lvalue f a
+          | Types.Vec _ | Types.Map _ | Types.Array _ -> lvalue f a
          | _ -> eval f a), a.Tast.ty)
      args
  in
--- a/runtime/flan_dyn.c
+++ b/runtime/flan_dyn.c
@ -34,6 +34,7 @@
 */
 #include <stdint.h>
 #include <stddef.h>
 #include <stdio.h>
 #include <stdlib.h>
 #include <string.h>
@ -55,6 +56,16 @@ void flan_write_stdout(const uint8_t *p, int64_t n);
 * only one of. So flan_rt.c exports a thin wrapper and this calls it. */
 _Noreturn void flan_trap(const uint8_t *name, int64_t namelen);
 /* Growing a Vec through a dyn view borrows flan_rt.c's own growth: doubling,
 * allocator adoption and the epoch check all live in [flan_vec_push], and
 * re-implementing any of that here would be a second copy of logic the
 * duplicity doctrine (docs/SPIKE-DUPLICITY.md) says belongs on one side only.
 * [v] is declared [void *] rather than [flan_vec *] so this file need not
 * name flan_rt.c's type; the two structs' layouts must agree, which is
 * [flan_dyn_vec_hdr] below, restated for the same reason [flan_desc] is. */
 int8_t flan_vec_push(void *v, const void *elem, int64_t size, int64_t align,
                      const uint8_t *loc, int64_t loclen);
 /* ── The representation ────────────────────────────────────────────────
 *
 * NaN-boxed, in a word. A double is *itself*: the 2^64 minus a NaN's worth of
@ -126,6 +137,11 @@ typedef struct flan_desc {
 * already opens with, never a memcmp. */
 #define BOX_KW   4u
 /* Restated from flan_dyn.h — a view's element kind. */
 #define FLAN_VIEW_I64  0
 #define FLAN_VIEW_F64  1
 #define FLAN_VIEW_BOOL 2
 /* Spelled as a negated positive rather than as a shift of -1: shifting a
 * negative value left is undefined, and this file is swept by UBSan. */
 #define DYN_INT_MAX (((int64_t)1 << 47) - 1)
@ -164,6 +180,45 @@ static inline flan_dyn dyn_make(unsigned tag, uint64_t payload) {
 #define OBJ_VEC  1
 #define OBJ_INT  2   /* an i64 too wide for the payload */
 #define OBJ_MAP  3   /* keys and values interleaved: k0 v0 k1 v1 ... */
 #define OBJ_VIEW 4   /* a typed container crossing into dyn as a view */
 /* flan_vec, restated. This file must not name flan_rt.c's [flan_vec] — see
 * the "if either table changes, change both" note above [flan_vec_push] —
 * so a view over a [(Vec T)] is built from an address whose first five words
 * this mirrors exactly. Only [ptr], [len] and [epoch]/[alloc] are ever read
 * through it; nothing here writes one. */
 typedef struct flan_dyn_vec_hdr {
  void    *ptr;
  int64_t  len;
  int64_t  cap;
  void    *alloc;
  int64_t  epoch;
 } flan_dyn_vec_hdr;
 /* This mirror's own layout, reported the same way flan_rt.c's
 * [flan_vec_layout] reports the original's — see that function's comment
 * for what ties the two together and why nothing at compile time otherwise
 * does. */
 void flan_dyn_vec_hdr_layout(int64_t out[6]) {
  out[0] = (int64_t)sizeof(flan_dyn_vec_hdr);
  out[1] = (int64_t)offsetof(flan_dyn_vec_hdr, ptr);
  out[2] = (int64_t)offsetof(flan_dyn_vec_hdr, len);
  out[3] = (int64_t)offsetof(flan_dyn_vec_hdr, cap);
  out[4] = (int64_t)offsetof(flan_dyn_vec_hdr, alloc);
  out[5] = (int64_t)offsetof(flan_dyn_vec_hdr, epoch);
 }
 /* flan_allocator's prefix, far enough to read the one word a stale-container
 * check needs. The struct has more fields after [epoch]; this file never
 * touches them; and the alignment of a leading same-typed prefix is the same
 * in any translation unit that agrees on the field order, which is the
 * "change both" this comment is the other half of. */
 typedef struct flan_dyn_alloc_hdr {
  void     *proc;
  void     *data;
  uint32_t  caps;
  uint64_t  epoch;
 } flan_dyn_alloc_hdr;
 typedef struct flan_obj {
  struct flan_obj *next;   /* every object ever allocated, newest first */
@ -179,13 +234,32 @@ typedef struct flan_obj {
      entries and [cap] counting entries too. Sharing the arm is what lets the
      marker and the sweep treat the two kinds with one load and a doubled
      count rather than a second field to keep in step. */
    /* OBJ_VIEW: a typed container's elements, native words this file did not
       allocate and does not own. [is_vec] set means [base] is a
       [flan_dyn_vec_hdr *] and [len] here is unused — the live length is
       read from the header on every operation, which is the whole of why a
       Vec growing through the view cannot go stale. [is_vec] clear means
       [base] is the first element's address and [len] is the snapshot taken
       at the crossing, for a slice or a fixed array, neither of which moves.
       [elem] is one of FLAN_VIEW_I64/F64/BOOL. */
    struct { void *base; int64_t len; int32_t elem; int32_t is_vec; } view;
    /* OBJ_TEXT's bytes trail the header; see [obj_text_bytes]. */
  } u;
 } flan_obj;
 /* How many dyn words hang off an object's items block — the count the marker
- * walks and the sweep charges. A map holds two per entry. */
+ * walks and the sweep charges. A map holds two per entry.
 *
 * OBJ_VIEW answers 0 explicitly rather than falling into the [o->len] arm.
 * [mark_push] never puts a view on the mark stack — it traces only
 * OBJ_VEC/OBJ_MAP — so this is not reachable today, but [o->u.view.base]
 * aliases [o->u.v.items] in the union, and a native array of i64 or f64
 * reinterpreted as dyn words is exactly the kind of thing this file's
 * roots contract exists to prevent happening by accident. Answering 0 here
 * is what keeps a future change to the marking gate from silently trusting
 * this function's default arm instead of failing loudly. */
 static inline int64_t obj_words(flan_obj *o) {
  if (o->kind == OBJ_VIEW) return 0;
  return o->kind == OBJ_MAP ? o->len * 2 : o->len;
 }
@ -309,7 +383,11 @@ int32_t flan_dyn_tag(flan_dyn v) {
    if (o == NULL) return FLAN_DYN_TAG_NIL;
    switch (o->kind) {
    case OBJ_TEXT: return FLAN_DYN_TAG_TEXT;
    /* A view answers the same tag a heap vec does: from a dyn program's
       side there is nothing to tell them apart by, which is the point of a
       view being indistinguishable rather than a fourth kind of vec. */
    case OBJ_VEC:  return FLAN_DYN_TAG_VEC;
    case OBJ_VIEW: return FLAN_DYN_TAG_VEC;
    case OBJ_MAP:  return FLAN_DYN_TAG_MAP;
    default:       return FLAN_DYN_TAG_INT;
    }
@ -403,6 +481,19 @@ static void emit_escaped(const uint8_t *p, int64_t n) {
 static int64_t dyn_int_value(flan_dyn v);   /* forward: both int shapes */
 static double  dyn_num_value(flan_dyn v);
 /* forward: the view helpers, needed by [render] and [say_render] above where
 * they are defined, alongside the container operations below */
 static int64_t  view_len(const char *op, flan_obj *o);
 static void    *view_base(flan_obj *o);
 static flan_dyn  view_box(int32_t elem, const uint8_t *p);
 static int64_t   view_elem_size(int32_t elem);
 /* forward: needed by [dyn_equal] below, defined alongside the view helpers
 * further down — a length and an element reader that answer correctly
 * whether [o] is an ordinary heap vec or a view over a typed container. */
 static int64_t  vecish_len(flan_obj *o);
 static flan_dyn vecish_at(flan_obj *o, int64_t i);
 static void render(flan_dyn v, int depth, int nested) {
  char buf[64];
  int32_t t = flan_dyn_tag(v);
@ -461,11 +552,17 @@ static void render(flan_dyn v, int depth, int nested) {
  }
  default: {
    flan_obj *o = dyn_obj(v);
-    int64_t i;
+    int64_t i, n = o->kind == OBJ_VIEW ? view_len("print", o) : o->len;
    emit("[");
-    for (i = 0; i < o->len; i++) {
+    for (i = 0; i < n; i++) {
      emit(" ");
-      render(o->u.v.items[i], depth + 1, 1);
+      if (o->kind == OBJ_VIEW)
        render(view_box(o->u.view.elem,
                        (const uint8_t *)view_base(o)
                          + i * view_elem_size(o->u.view.elem)),
               depth + 1, 1);
      else
        render(o->u.v.items[i], depth + 1, 1);
    }
    emit("]");
    return;
@ -551,14 +648,21 @@ static void say_render(sayer *s, flan_dyn v, int depth) {
  }
  default: {
    flan_obj *o = dyn_obj(v);
-    int64_t i;
+    int64_t i, n = o->kind == OBJ_VIEW ? view_len("print", o) : o->len;
    if (depth >= 2) { say_puts(s, "[...]"); return; }
    say_puts(s, "[");
-    for (i = 0; i < o->len && s->n < s->cap - 8; i++) {
+    for (i = 0; i < n && s->n < s->cap - 8; i++) {
      say_puts(s, " ");
-      say_render(s, o->u.v.items[i], depth + 1);
+      if (o->kind == OBJ_VIEW)
        say_render(s,
                   view_box(o->u.view.elem,
                            (const uint8_t *)view_base(o)
                              + i * view_elem_size(o->u.view.elem)),
                   depth + 1);
      else
        say_render(s, o->u.v.items[i], depth + 1);
    }
-    say_puts(s, i < o->len ? " ...]" : "]");
+    say_puts(s, i < n ? " ...]" : "]");
    return;
  }
  }
@ -1211,12 +1315,23 @@ static int dyn_equal(flan_dyn a, flan_dyn b, int depth) {
  }
  if (ta == FLAN_DYN_TAG_VEC) {
    flan_obj *x = dyn_obj(a), *y = dyn_obj(b);
-    int64_t i;
+    int64_t i, xn, yn;
    if (x == y) return 1;
    if (depth >= EQ_DEPTH) return 0;
-    if (x->len != y->len) return 0;
+    /* [x]/[y] may each be an ordinary heap vec or a view (M2 item 3) — the
-    for (i = 0; i < x->len; i++)
+       tag does not say which, so [vecish_len]/[vecish_at] below read either
-      if (!dyn_equal(x->u.v.items[i], y->u.v.items[i], depth + 1)) return 0;
+       shape correctly. Reading raw through [x->u.v.items] the way this arm
       used to is wrong for a view: nothing sets [len] for OBJ_VIEW, so it
       reads back 0, and the elements alias [u.view.base] reinterpreted as
       dyn words — two views with different contents would compare equal, a
       view and an equal heap vec would compare unequal, and a map keyed by
       any view would collide with every other view, silently, with nothing
       to crash. */
    xn = vecish_len(x);
    yn = vecish_len(y);
    if (xn != yn) return 0;
    for (i = 0; i < xn; i++)
      if (!dyn_equal(vecish_at(x, i), vecish_at(y, i), depth + 1)) return 0;
    return 1;
  }
  /* Two maps are equal when they hold the same keys and each key answers an
@ -1265,9 +1380,156 @@ static inline int is_map(flan_dyn v) {
  return flan_dyn_tag(v) == FLAN_DYN_TAG_MAP;
 }
 /* ── Typed containers as views ─────────────────────────────────────────
 *
 * Every entry point below already dispatches on [flan_dyn_tag], which does
 * not distinguish a view from a heap vec — see [flan_dyn_tag]'s switch — so
 * [flan_dyn_len], [flan_dyn_at], [flan_dyn_set_at], [flan_dyn_push] and the
 * printer each add one branch for [OBJ_VIEW] beside the existing [OBJ_VEC]
 * one. What follows is that branch's machinery. */
 static int64_t view_elem_size(int32_t elem) {
  return elem == FLAN_VIEW_BOOL ? 1 : 8;
 }
 /* The stale-container check flan_rt.c's [flan_vec_check] runs for a typed
 * Vec, restated for a view's own trap rather than reused: the duplicity
 * doctrine's dyn side gets its own spelling (docs/SPIKE-DUPLICITY.md), and a
 * dyn program that hits this wants the same park-and-inspect [flan_trap]
 * gives every other dyn mistake, not the typed side's [rt_die]. A Vec with
 * no allocator yet — one nobody has pushed to — has nothing to check.
 *
 * The message never renders the view it just declared unsafe to read —
 * review's second finding, and it was not a decoration this dropped for
 * safety's sake, it was a real infinite recursion: [say] on a view calls
 * [say_render]'s view branch, which calls [view_len], which calls back in
 * here, unconditionally, because the epoch is still stale. Every render of
 * this same view would hit the same check and take the same branch, so
 * nothing about depth or a visited set closes it — the fix is that a
 * stale-container check must never read the container it has just refused
 * to trust, not even to describe it in the sentence explaining why. */
 static void view_vec_check(const char *op, flan_dyn_vec_hdr *h) {
  if (h->alloc) {
    flan_dyn_alloc_hdr *a = (flan_dyn_alloc_hdr *)h->alloc;
    if ((int64_t)a->epoch != h->epoch) {
      fflush(stdout);
      fprintf(stderr,
              "dyn %s: this view's container's allocator was released — the "
              "Vec was made at epoch %lld and the allocator is at %lld now\n",
              op, (long long)h->epoch, (long long)(int64_t)a->epoch);
      flan_trap((const uint8_t *)"DynRange", 8);
    }
  }
 }
 /* [len] and [base], read live for a Vec view (so a push that grows and
 * moves the underlying Vec is seen the very next operation) and read from
 * the snapshot for a flat one. */
 static int64_t view_len(const char *op, flan_obj *o) {
  if (o->u.view.is_vec) {
    flan_dyn_vec_hdr *h = (flan_dyn_vec_hdr *)o->u.view.base;
    view_vec_check(op, h);
    return h->len;
  }
  return o->u.view.len;
 }
 static void *view_base(flan_obj *o) {
  if (o->u.view.is_vec) return ((flan_dyn_vec_hdr *)o->u.view.base)->ptr;
  return o->u.view.base;
 }
 /* Reads box the element on the way out — the runtime already knows how to
 * box an i64, an f64 or a bool, so this is that, from raw bytes rather than
 * from a C value already in hand. */
 static flan_dyn view_box(int32_t elem, const uint8_t *p) {
  switch (elem) {
  case FLAN_VIEW_I64: { int64_t x; memcpy(&x, p, 8); return flan_dyn_from_i64(x); }
  case FLAN_VIEW_F64: { double x;  memcpy(&x, p, 8); return flan_dyn_from_f64(x); }
  default:            { uint8_t b = *p; return flan_dyn_from_bool(b); }
  }
 }
 /* A length and an element reader that answer correctly whether [o] is an
 * ordinary heap vec (OBJ_VEC, elements are dyn words) or a view over a
 * typed container (OBJ_VIEW, elements are native bytes boxed on the way
 * out) — the pair [dyn_equal]'s VEC arm needs so that a view compares
 * correctly against another view and against an ordinary vec alike. Reading
 * [o->len]/[o->u.v.items] directly, the way that arm used to, answers 0 and
 * garbage for a view: nothing sets [len] for OBJ_VIEW, and its elements
 * alias [u.view.base] reinterpreted as dyn words rather than the native
 * bytes they are. */
 static int64_t vecish_len(flan_obj *o) {
  return o->kind == OBJ_VIEW ? view_len("=", o) : o->len;
 }
 static flan_dyn vecish_at(flan_obj *o, int64_t i) {
  if (o->kind == OBJ_VIEW)
    return view_box(o->u.view.elem,
                    (const uint8_t *)view_base(o)
                      + i * view_elem_size(o->u.view.elem));
  return o->u.v.items[i];
 }
 /* Writes tag-check on the way in: the dyn value's tag must be the one this
 * view's element type wants, or this traps by name and never coerces or
 * truncates a mismatched value into the slot. [v] is the view, for the
 * sentence's container half; [x] is the value that was refused. */
 static void view_unbox(const char *op, flan_dyn v, int32_t elem, flan_dyn x,
                       uint8_t *p) {
  switch (elem) {
  case FLAN_VIEW_I64: {
    int64_t n;
    if (flan_dyn_tag(x) != FLAN_DYN_TAG_INT)
      trap2(TYPE_TRAP, op, "this view's elements are int", v, x);
    n = dyn_int_value(x);
    memcpy(p, &n, 8);
    return;
  }
  case FLAN_VIEW_F64: {
    double d;
    if (flan_dyn_tag(x) != FLAN_DYN_TAG_FLOAT)
      trap2(TYPE_TRAP, op, "this view's elements are float", v, x);
    d = dyn_num_value(x);
    memcpy(p, &d, 8);
    return;
  }
  default: {
    uint8_t b;
    if (flan_dyn_tag(x) != FLAN_DYN_TAG_BOOL)
      trap2(TYPE_TRAP, op, "this view's elements are bool", v, x);
    b = dyn_payload(x) ? 1 : 0;
    *p = b;
    return;
  }
  }
 }
 flan_dyn flan_dyn_view_vec(void *hdr, int32_t elem) {
  flan_obj *o = gc_alloc(OBJ_VIEW, 0);
  o->u.view.base = hdr;
  o->u.view.len = 0;
  o->u.view.elem = elem;
  o->u.view.is_vec = 1;
  return dyn_make(BOX_OBJ, (uint64_t)(uintptr_t)o);
 }
 flan_dyn flan_dyn_view_flat(void *data, int64_t len, int32_t elem) {
  flan_obj *o = gc_alloc(OBJ_VIEW, 0);
  o->u.view.base = data;
  o->u.view.len = len;
  o->u.view.elem = elem;
  o->u.view.is_vec = 0;
  return dyn_make(BOX_OBJ, (uint64_t)(uintptr_t)o);
 }
 flan_dyn flan_dyn_len(flan_dyn v) {
-  if (is_text(v) || is_vec(v) || is_map(v))
+  if (is_text(v) || is_map(v)) return flan_dyn_from_i64(dyn_obj(v)->len);
-    return flan_dyn_from_i64(dyn_obj(v)->len);
+  if (is_vec(v)) {
    flan_obj *o = dyn_obj(v);
    if (o->kind == OBJ_VIEW) return flan_dyn_from_i64(view_len("len", o));
    return flan_dyn_from_i64(o->len);
  }
  trap1(TYPE_TRAP, "len", "only a text, a vec or a map has one", v);
 }
@ -1290,6 +1552,12 @@ flan_dyn flan_dyn_at(flan_dyn v, flan_dyn i) {
    trap2(TYPE_TRAP, "at", "only a text or a vec is indexed", v, i);
  k = need_index("at", v, i);
  o = dyn_obj(v);
  if (o->kind == OBJ_VIEW) {
    int64_t len = view_len("at", o);
    if (k < 0 || k >= len) trap_range("at", v, k, len);
    return view_box(o->u.view.elem,
                    (const uint8_t *)view_base(o) + k * view_elem_size(o->u.view.elem));
  }
  if (k < 0 || k >= o->len) trap_range("at", v, k, o->len);
  if (o->kind == OBJ_TEXT) return flan_dyn_from_i64(obj_text_bytes(o)[k]);
  return o->u.v.items[k];
@ -1298,13 +1566,20 @@ flan_dyn flan_dyn_at(flan_dyn v, flan_dyn i) {
 void flan_dyn_set_at(flan_dyn v, flan_dyn i, flan_dyn x) {
  int64_t k;
  flan_obj *o;
  (void)x;
  if (is_text(v))
    trap2(TYPE_TRAP, "set-at", "a text is immutable — build another one", v, i);
  if (!is_vec(v))
    trap2(TYPE_TRAP, "set-at", "only a vec is assigned into", v, i);
  k = need_index("set-at", v, i);
  o = dyn_obj(v);
  if (o->kind == OBJ_VIEW) {
    int64_t len = view_len("set-at", o);
    uint8_t *p;
    if (k < 0 || k >= len) trap_range("set-at", v, k, len);
    p = (uint8_t *)view_base(o) + k * view_elem_size(o->u.view.elem);
    view_unbox("set-at", v, o->u.view.elem, x, p);
    return;
  }
  if (k < 0 || k >= o->len) trap_range("set-at", v, k, o->len);
  o->u.v.items[k] = x;
 }
@ -1317,6 +1592,20 @@ void flan_dyn_push(flan_dyn v, flan_dyn x) {
    trap2(TYPE_TRAP, "push", "only a vec is pushed to", v, x);
  }
  o = dyn_obj(v);
  if (o->kind == OBJ_VIEW) {
    uint8_t buf[8];
    static const uint8_t push_loc[] = "(dyn push)";
    int64_t size;
    if (!o->u.view.is_vec)
      trap2(TYPE_TRAP, "push",
            "this view is a slice or an array and cannot grow", v, x);
    size = view_elem_size(o->u.view.elem);
    view_unbox("push", v, o->u.view.elem, x, buf);
    if (!flan_vec_push(o->u.view.base, buf, size, size, push_loc,
                        (int64_t)sizeof(push_loc) - 1))
      trap_oom(size);
    return;
  }
  if (o->len == o->u.v.cap) {
    int64_t cap = o->u.v.cap ? o->u.v.cap * 2 : 8;
    flan_dyn *items =
--- a/runtime/flan_dyn.h
+++ b/runtime/flan_dyn.h
@ -151,6 +151,64 @@ flan_dyn flan_dyn_need_not_nil(flan_dyn v);
 * "", an empty vec, an empty map, and any keyword. Never traps. */
 uint8_t flan_dyn_truthy(flan_dyn v);
 /* ── Typed containers as views — M2 item 3 ─────────────────────────────
 *
 * A [(Vec T)], a [T] slice, or a fixed [n T] array crossing into dyn is a
 * VIEW, not a copy: the box holds a small heap record naming where the
 * elements live and what one of them is, and every read or write goes
 * straight through to the container's own storage. [flan_dyn_at] boxes an
 * element on the way out; [flan_dyn_set_at] tag-checks the dyn value it is
 * given against the element type on the way in and traps, by [flan_trap],
 * on a mismatch — never a silent coercion.
 *
 * T is restricted to i64, f64 and bool — exactly the set [flan_dyn_need_i64]
 * and friends already treat as crossing the typed boundary both ways. That
 * is not an arbitrary cut: the excluded case that matters is a string
 * element, whose dyn form is a pointer into this collector's heap, while a
 * typed container's storage is arena or stack memory the collector never
 * scans. Writing such a pointer into that memory would be a live reference
 * nothing ever traces — a use-after-free the collector cannot see coming,
 * not a bug in this file but a hazard the type admits. i64, f64 and bool
 * carry no such pointer, so a view restricted to them cannot manufacture
 * it. [box] in lib/check.ml keeps the "does not cross into dyn yet" refusal
 * for every other element type, and this paragraph is why.
 *
 * Two kinds, because the containers split exactly here: a [(Vec T)] can grow
 * and move (a push may reallocate), a slice and a fixed array cannot.
 *
 * [flan_dyn_view_vec] takes the address of the Vec's own header — the
 * struct [flan_vec] in flan_rt.c, restated in flan_dyn.c under the same
 * "if either table changes, change both" rule this whole boundary already
 * lives under. That address is the Vec's home, fixed for as long as the Vec
 * exists — but "as long as the Vec exists" is the whole of the guarantee,
 * which is why [permanent_root] in lib/check.ml admits only storage that
 * outlives every frame: a global, a field or an array element of one, or a
 * slice cut from one at the crossing. A local's slot is a home too, and it
 * is precisely the one that is refused. Every operation re-reads that
 * header's [ptr] and [len] fresh, so a push that grows and moves the Vec is
 * never seen as stale — [flan_vec_grow] overwrites the SAME header's [ptr]
 * field in place, and there is no snapshot anywhere to go stale. That is
 * what makes the failure the open design question worried about
 * (a push through dyn holding a dangling pointer) impossible rather than
 * merely unlikely: there is nothing captured at the crossing for a later
 * push to invalidate.
 *
 * [flan_dyn_view_flat] takes a data address and a length captured once, at
 * the crossing — sound for a slice and for a fixed array because neither
 * ever moves or grows. Note the asymmetry is not an oversight: pointing
 * *this* case at the value's own slot instead would be worse than a
 * snapshot, because a slot's lifetime is not the slice's, and a slice taken
 * from a Vec is already one push away from dangling on its own account
 * (flan_vec_grow's own comment says so) — the view is exactly as
 * stale-safe as the thing it is a view of, no more and no less.
 */
 #define FLAN_VIEW_I64  0
 #define FLAN_VIEW_F64  1
 #define FLAN_VIEW_BOOL 2
 flan_dyn flan_dyn_view_vec(void *hdr, int32_t elem);
 flan_dyn flan_dyn_view_flat(void *data, int64_t len, int32_t elem);
 /* ── The collector ─────────────────────────────────────────────────────
 *
 * Mark-sweep, precise, and never moving. [flan_gc_init] is idempotent, and the
@ -261,6 +319,14 @@ const char *flan_dyn_tag_name(int32_t tag);
 int64_t flan_gc_count(void);
 void    flan_gc_set_floor(int64_t bytes);
 /* Reports flan_dyn.c's own mirror of flan_rt.c's [flan_vec] — [size, then
 * the offset of ptr, len, cap, alloc, epoch] — for test/dyn_ops.c's
 * "layout" mode to compare against flan_rt.c's [flan_vec_layout] and
 * against its own hand-built mirror. See [flan_vec_layout]'s comment in
 * flan_rt.c for what this ties together and why nothing at compile time
 * otherwise does. */
 void flan_dyn_vec_hdr_layout(int64_t out[6]);
 #ifdef __cplusplus
 }
 #endif
--- a/runtime/flan_rt.c
+++ b/runtime/flan_rt.c
@ -12,6 +12,7 @@
 */
 #include <stdint.h>
 #include <stddef.h>
 #include <stdio.h>
 #include <stdlib.h>
 #include <string.h>
@ -1490,6 +1491,27 @@ typedef struct flan_vec {
  int64_t         epoch;
 } flan_vec;
 /* This struct's layout is restated twice more in the tree — flan_dyn.c's
 * [flan_dyn_vec_hdr], for a typed container's view (M2 item 3), and
 * test/dyn_ops.c's [hand_vec], which builds one by hand because it has no
 * [flan_vec] type to initialise, this file being linked into it but not
 * included by it. None of the three can [#include]
 * this file (see [Build.compile_c]), so nothing at compile time ties them
 * together — a reordered field here links and runs, and corrupts whichever
 * of the other two disagrees. [flan_vec_layout] is the tie: it reports this
 * struct's real size and field offsets, and test/dyn_ops.c's "layout" mode
 * compares them against its own [hand_vec]'s and against flan_dyn.c's
 * [flan_dyn_vec_hdr_layout], so a disagreement is a FAIL line in `dune test`
 * rather than a silent corruption the next line over. */
 void flan_vec_layout(int64_t out[6]) {
  out[0] = (int64_t)sizeof(flan_vec);
  out[1] = (int64_t)offsetof(flan_vec, ptr);
  out[2] = (int64_t)offsetof(flan_vec, len);
  out[3] = (int64_t)offsetof(flan_vec, cap);
  out[4] = (int64_t)offsetof(flan_vec, alloc);
  out[5] = (int64_t)offsetof(flan_vec, epoch);
 }
 /* The request that did not fit, for the condition the compiler builds at the
 * failing site. A pair of globals rather than out-parameters because the
 * condition is a value struct on the signalling frame's stack with fixed
--- a/test/dyn_ops.c
+++ b/test/dyn_ops.c
@ -32,6 +32,9 @@
 #include "flan_dyn.h"
 void flan_rt_init(int32_t argc, char **argv);
 void flan_vec_free(void *v, int64_t size, int64_t align, const uint8_t *loc,
                    int64_t loclen);
 void flan_vec_layout(int64_t out[6]);
 static int failures;
@ -361,6 +364,203 @@ static void ops(void) {
  (void)s;
 }
 /* A typed container's own header, restated a third time — flan_rt.c's
 * [flan_vec], flan_dyn.c's [flan_dyn_vec_hdr], and this. The three must
 * agree on layout, and none of them can [#include] another's to say so at
 * compile time (see [Build.compile_c]) — so the header below is built by
 * hand, the same five words [flan_vec_grow] would leave behind after a few
 * pushes. flan_rt.c IS linked into this binary (the [flan_vec_free] and
 * [flan_vec_layout] calls below are its), but without its header there is
 * no [flan_vec] type to declare an initialiser over; the restatement is
 * what the [#include] restriction costs, not a missing link.
 *
 * What actually ties the three together is [layout], further down: it reads
 * flan_rt.c's [flan_vec_layout] and flan_dyn.c's [flan_dyn_vec_hdr_layout]
 * and compares both against [offsetof] on this very struct, so a field
 * reordered in any one of the three is a FAIL line here rather than a
 * silent corruption at whatever call site next dereferences the wrong
 * offset. A declared-as-[void*] prototype on its own proves nothing about
 * layout — it was named as if it did in an earlier version of this
 * comment, which was wrong, and [layout] is what makes the claim true. */
 typedef struct {
  void    *ptr;
  int64_t  len;
  int64_t  cap;
  void    *alloc;
  int64_t  epoch;
 } hand_vec;
 /* The runtime's half of M2 item 3: a typed container crossing into dyn as a
 * view, driven directly with no compiler in the loop — [flan_dyn_view_vec]
 * and [flan_dyn_view_flat] built by hand over a [hand_vec] and a plain
 * array, exactly as the checker's [box] will build them over a real [(Vec
 * i64)] and a real [[4]i64]. */
 static void view(void) {
  int64_t buf[4] = { 10, 20, 30, 40 };
  flan_dyn flat = flan_dyn_nil(), vv = flan_dyn_nil();
  flan_dyn_root_push(&flat);
  flan_dyn_root_push(&vv);
  /* A flat view over a fixed array: reads box, writes tag-check, and the
     storage really is the array's own — a write through the view is read
     back through the C array with no call into this file at all. */
  flat = flan_dyn_view_flat(buf, 4, FLAN_VIEW_I64);
  check(flan_dyn_tag(flat) == FLAN_DYN_TAG_VEC, "a view tags as a vec");
  check(num(flan_dyn_len(flat)) == 4, "flat view len");
  check(num(flan_dyn_at(flat, flan_dyn_from_i64(2))) == 30, "flat view at");
  flan_dyn_set_at(flat, flan_dyn_from_i64(2), flan_dyn_from_i64(99));
  check(buf[2] == 99, "flat view write reaches the array");
  buf[3] = 7;
  check(num(flan_dyn_at(flat, flan_dyn_from_i64(3))) == 7,
        "the array's own write reaches the view — it is not a copy");
  prints(flat, "[ 10 20 99 7]");
  /* Structural equality, view-aware — review's third finding. [dyn_equal]'s
     VEC arm used to read [x->len]/[x->u.v.items] regardless of kind, which
     for a view answers 0 and garbage: two views with different contents
     compared equal, a view and an equal heap vec compared unequal, and a
     map keyed by any view collided with every other view. [buf] now reads
     [ 10 20 99 7]; [same] is a second, independent view over the identical
     bytes, and [other] a view over one differing element. */
  {
    int64_t same_buf[4] = { 10, 20, 99, 7 };
    int64_t diff_buf[4] = { 10, 20, 99, 8 };
    flan_dyn same = flan_dyn_view_flat(same_buf, 4, FLAN_VIEW_I64);
    flan_dyn other = flan_dyn_view_flat(diff_buf, 4, FLAN_VIEW_I64);
    flan_dyn heap = flan_dyn_vec_new();
    flan_dyn_root_push(&same);
    flan_dyn_root_push(&other);
    flan_dyn_root_push(&heap);
    check(truth(flan_dyn_eq(flat, same)),
          "two views over equal bytes are equal");
    check(!truth(flan_dyn_eq(flat, other)),
          "two views over different bytes are not equal");
    flan_dyn_push(heap, flan_dyn_from_i64(10));
    flan_dyn_push(heap, flan_dyn_from_i64(20));
    flan_dyn_push(heap, flan_dyn_from_i64(99));
    flan_dyn_push(heap, flan_dyn_from_i64(7));
    check(truth(flan_dyn_eq(flat, heap)),
          "a view and an equal heap vec are equal");
    flan_dyn_set_at(heap, flan_dyn_from_i64(3), flan_dyn_from_i64(0));
    check(!truth(flan_dyn_eq(flat, heap)),
          "a view and a differing heap vec are not equal");
    flan_dyn_root_pop(3);
  }
  /* A vec view: points at the header's own address, so a push that grows
     and moves it is seen on the very next read — there is no snapshot to
     go stale. */
  {
    hand_vec hv;
    hv.ptr = NULL; hv.len = 0; hv.cap = 0; hv.alloc = NULL; hv.epoch = 0;
    vv = flan_dyn_view_vec(&hv, FLAN_VIEW_I64);
    check(num(flan_dyn_len(vv)) == 0, "vec view starts empty");
    {
      int i;
      for (i = 0; i < 20; i++) flan_dyn_push(vv, flan_dyn_from_i64(i));
    }
    check(num(flan_dyn_len(vv)) == 20, "vec view len after growth");
    check(num(flan_dyn_at(vv, flan_dyn_from_i64(0))) == 0,
          "first element survived the growth and the move");
    check(num(flan_dyn_at(vv, flan_dyn_from_i64(19))) == 19,
          "pushed element reachable after the header's ptr moved");
    /* [hv]'s own fields moved under the view's feet, by construction — the
       view never captured [hv.ptr]; it captured [&hv]. */
    check(hv.len == 20 && hv.cap >= 20, "the hand-built header itself grew");
    flan_dyn_set_at(vv, flan_dyn_from_i64(0), flan_dyn_from_i64(-1));
    check(((int64_t *)hv.ptr)[0] == -1, "write through the view reaches hv");
    flan_vec_free(&hv, 8, 8, (const uint8_t *)"view", 4);
  }
  /* A bool view and a float view, so the element-tag dispatch is exercised
     on all three kinds and not only i64. */
  {
    uint8_t bools[2] = { 1, 0 };
    double floats[2] = { 1.5, -2.0 };
    flan_dyn bv = flan_dyn_view_flat(bools, 2, FLAN_VIEW_BOOL);
    flan_dyn fv = flan_dyn_view_flat(floats, 2, FLAN_VIEW_F64);
    check(truth(flan_dyn_at(bv, flan_dyn_from_i64(0))), "bool view at true");
    check(!truth(flan_dyn_at(bv, flan_dyn_from_i64(1))), "bool view at false");
    flan_dyn_set_at(bv, flan_dyn_from_i64(1), flan_dyn_from_bool(1));
    check(bools[1] == 1, "bool view write");
    check(flan_dyn_need_f64(flan_dyn_at(fv, flan_dyn_from_i64(0))) == 1.5,
          "float view at");
    flan_dyn_set_at(fv, flan_dyn_from_i64(0), flan_dyn_from_f64(3.25));
    check(floats[0] == 3.25, "float view write");
  }
  flan_dyn_root_pop(2);
  printf(failures == 0 ? "view ok\n" : "view failed\n");
 }
 /* Every wrong way to use a view: out of range, a mismatched write on each of
 * the three element kinds, and a push against a fixed-size (flat) view. Each
 * is its own mode because each ends the process. */
 static void refuse_view(const char *what) {
  static int64_t buf[2] = { 1, 2 };
  flan_dyn v;
  if (strcmp(what, "range") == 0) {
    v = flan_dyn_view_flat(buf, 2, FLAN_VIEW_I64);
    (void)flan_dyn_at(v, flan_dyn_from_i64(2));
  } else if (strcmp(what, "wrongwrite") == 0) {
    v = flan_dyn_view_flat(buf, 2, FLAN_VIEW_I64);
    flan_dyn_set_at(v, flan_dyn_from_i64(0), text("nope"));
  } else if (strcmp(what, "wrongbool") == 0) {
    static uint8_t bb[1];
    v = flan_dyn_view_flat(bb, 1, FLAN_VIEW_BOOL);
    flan_dyn_set_at(v, flan_dyn_from_i64(0), flan_dyn_from_i64(1));
  } else if (strcmp(what, "wrongfloat") == 0) {
    static double ff[1];
    v = flan_dyn_view_flat(ff, 1, FLAN_VIEW_F64);
    flan_dyn_set_at(v, flan_dyn_from_i64(0), flan_dyn_from_i64(1));
  } else if (strcmp(what, "flatpush") == 0) {
    v = flan_dyn_view_flat(buf, 2, FLAN_VIEW_I64);
    flan_dyn_push(v, flan_dyn_from_i64(9));
  } else {
    printf("no such refusal: %s\n", what);
    exit(2);
  }
  printf("did not trap\n");
  exit(3);
 }
 /* The three restatements of flan_vec's layout, compared — see [hand_vec]'s
 * comment for why nothing at compile time otherwise ties them together.
 * [offsetof] on [hand_vec] itself is this file's half; [flan_vec_layout]
 * and [flan_dyn_vec_hdr_layout] are the other two's. */
 static void layout(void) {
  int64_t rt[6], dyn[6];
  int64_t here[6] = {
    (int64_t)sizeof(hand_vec),
    (int64_t)offsetof(hand_vec, ptr),
    (int64_t)offsetof(hand_vec, len),
    (int64_t)offsetof(hand_vec, cap),
    (int64_t)offsetof(hand_vec, alloc),
    (int64_t)offsetof(hand_vec, epoch)
  };
  static const char *const names[6] =
    { "sizeof", "offset of ptr", "offset of len", "offset of cap",
      "offset of alloc", "offset of epoch" };
  int i;
  char msg[128];
  flan_vec_layout(rt);
  flan_dyn_vec_hdr_layout(dyn);
  for (i = 0; i < 6; i++) {
    if (rt[i] != here[i]) {
      snprintf(msg, sizeof msg, "flan_vec vs. hand_vec's %s: %lld vs. %lld",
               names[i], (long long)rt[i], (long long)here[i]);
      fail(msg);
    }
    if (dyn[i] != here[i]) {
      snprintf(msg, sizeof msg,
               "flan_dyn_vec_hdr vs. hand_vec's %s: %lld vs. %lld",
               names[i], (long long)dyn[i], (long long)here[i]);
      fail(msg);
    }
  }
  printf(failures == 0 ? "layout ok\n" : "layout failed\n");
 }
 /* ── The collector ─────────────────────────────────────────────────────*/
 /* Allocate a great many, hold a few, and assert the heap does not grow. The
@ -748,7 +948,19 @@ int main(int argc, char **argv) {
  if (strcmp(argv[1], "sharing") == 0) { sharing(); return 0; }
  if (strcmp(argv[1], "unrooted") == 0) { unrooted(); return 0; }
  if (strcmp(argv[1], "desc") == 0) { desc(); return 0; }
  if (strcmp(argv[1], "view") == 0) {
    view();
    return failures == 0 ? 0 : 1;
  }
  if (strcmp(argv[1], "layout") == 0) {
    layout();
    return failures == 0 ? 0 : 1;
  }
  if (strncmp(argv[1], "refuse:", 7) == 0) { refuse(argv[1] + 7); return 0; }
  if (strncmp(argv[1], "refuseview:", 11) == 0) {
    refuse_view(argv[1] + 11);
    return 0;
  }
  printf("no such mode: %s\n", argv[1]);
  return 2;
 }
--- a/test/programs/dyn-view.flan
+++ b/test/programs/dyn-view.flan
@ -0,0 +1,151 @@
 ;;;; M2 item 3: a typed container crossing into dyn is a VIEW, not a copy.
 ;;;;
 ;;;; [as-dyn]'s parameter is unannotated dyn and its argument is a typed
 ;;;; (Vec i64), a fixed array or a slice — the box happens at the call, on the
 ;;;; caller's own value, which is what makes [dv] below the SAME storage [v]
 ;;;; is and not a copy of it.
 ;;;;
 ;;;; Every container viewed below is a GLOBAL, and that is not incidental to
 ;;;; this program — it is the lifetime guard review added after the first
 ;;;; landing: a view's descriptor chases the container's own address on every
 ;;;; operation, which is what makes a Vec's growth safe, but it is also what
 ;;;; makes a DANGLING container's address a live hazard. box refuses a Vec, a
 ;;;; slice or a fixed array whose storage is not known to outlive the view —
 ;;;; a local's, a parameter's, a temporary's — and a global's is the one
 ;;;; storage this milestone can prove permanent: fixed in .data for the
 ;;;; process — as is a field of one, and an ELEMENT of one when the global
 ;;;; is an array, whose elements sit inside its own storage. An element of a
 ;;;; global SLICE is not: the slice is ptr+len and says nothing about where
 ;;;; the data is — and that holds at every index of a multi-index (at g i j),
 ;;;; not just the first, so one slice level anywhere in the walk refuses.
 ;;;; test_flan.ml's checker tests carry the refusal side of this (a local
 ;;;; Vec, a Vec parameter, a Vec behind a Ptr, a slice rebound to a local, an
 ;;;; element of a global slice, and an element reached through a slice at a
 ;;;; later index level); this program is the acceptance side, over storage
 ;;;; the guard allows.
 ;;;;
 ;;;; Mode 0 is the survey: a read through the view boxes the element
 ;;;; correctly, a write through either side is seen through the other, and a
 ;;;; push through the view — which can only mean the Vec case, since neither
 ;;;; a slice nor a fixed array can grow — moves the Vec's backing storage and
 ;;;; the typed side still sees the grown length and the new element. That is
 ;;;; the design's central claim: the view's descriptor points AT the Vec's
 ;;;; own header rather than snapshotting its pointer and length, so there is
 ;;;; no snapshot for the growth to invalidate — and the header itself is the
 ;;;; global's, which never moves even though the buffer behind it does.
 ;;;;
 ;;;; Modes 1 and 2 are the two traps a view can throw: an index outside its
 ;;;; length, and a write whose dyn tag does not match the element type the
 ;;;; view was built over. Both come from the runtime, by name, and both end
 ;;;; the process — a survey program can show at most one trap, so each gets
 ;;;; its own mode the way test/programs/bounds.flan's do.
 (defn as-dyn [d dyn] dyn d)
 (defvar v (Vec i64) (vec-new i64))
 (defvar a [4 i64])
 (defvar a2 [3 f64])
 (defvar bv (Vec bool) (vec-new bool))
 ;; A global ARRAY of Vecs. An element of this is permanent — it sits inside
 ;; the global's own storage at a fixed offset — and a view over it is the
 ;; acceptance half of the [At] arm's guard. The refusal half is the same
 ;; program with [[(Vec i64)]] (a global SLICE) instead, which holds only
 ;; ptr+len and so says nothing about where the Vecs live; test_flan.ml
 ;; carries that pair, because a refusal cannot run.
 (defvar rows [2 (Vec i64)])
 (defn main [args [string]] i32
  (let [n (i32 (bytes->i64 (bytes (at args 1))))]
    (cond
      (= n 0)
      (do
        ;; A (Vec i64) view, over the global.
        (push v 10)
        (push v 20)
        (push v 30)
        (let [dv (as-dyn v)]
          (print dv)
          (print "\n")
          ;; Write through the view, read through the typed side.
          (set (at dv 1) 999)
          (print (at v 1))
          (print "\n")
          ;; Write through the typed side, read through the view.
          (set (at v 2) 777)
          (print (at dv 2))
          (print "\n")
          ;; Grow through the view. flan_vec_grow reallocates v's backing
          ;; storage and overwrites v's own header in place, which is the
          ;; same header the view points at — so the typed side, asked
          ;; afterwards, already agrees with the push it never made itself.
          (push dv 40)
          (print (len v))
          (print "\n")
          (print (at v 3))
          (print "\n"))
        ;; A fixed array's view: nothing here can grow, so a snapshot taken
        ;; once at the crossing is sound — there is no move to go stale over.
        (set (at a 0) 1)
        (set (at a 1) 2)
        (set (at a 2) 3)
        (set (at a 3) 4)
        (let [da (as-dyn a)]
          (print da)
          (print "\n")
          (set (at da 0) 100)
          (print (at a 0))
          (print "\n")
          (set (at a 3) 400)
          (print (at da 3))
          (print "\n"))
        ;; A slice's view, over f64 elements, and a bool Vec's view — the
        ;; other two of the three element kinds a view can hold. The slice
        ;; is cut directly from the global at the call, which is what keeps
        ;; its trace back to permanent storage visible to the checker.
        (set (at a2 0) 1.5)
        (set (at a2 1) 2.5)
        (set (at a2 2) 3.5)
        (let [ds (as-dyn (slice a2 0 3))]
          (print ds)
          (print "\n")
          (set (at ds 0) 9.5)
          (print (at a2 0))
          (print "\n"))
        (push bv true)
        (push bv false)
        (let [db (as-dyn bv)]
          (print db)
          (print "\n")
          (set (at db 1) true)
          (print (at bv 1))
          (print "\n"))
        ;; An element of the global array: a (Vec i64) living inside the
        ;; global's own storage, viewed from there. A push through the view
        ;; grows that element's buffer and the typed side sees it, exactly
        ;; as for the plain global Vec above — the element's header never
        ;; moves, because the array it sits in never does.
        (push (at rows 0) 111)
        (push (at rows 0) 222)
        (let [dr (as-dyn (at rows 0))]
          (print dr)
          (print "\n")
          (push dr 333)
          (print (len (at rows 0)))
          (print "\n")
          (print (at (at rows 0) 2))
          (print "\n"))
        0)
      (= n 1)
      ;; Out of range. The runtime's own message names the length.
      (do (push v 1)
          (let [dv (as-dyn v)]
            (print (at dv 5)))
          0)
      (= n 2)
      ;; Wrong type on write: a text where the view holds i64. Tag-checked
      ;; and refused, never coerced and never silently stored.
      (do (push v 1)
          (let [dv (as-dyn v)]
            (set (at dv 0) "nope"))
          0)
      :else (do (println "?") 1))))
--- a/test/test_acceptance.ml
+++ b/test/test_acceptance.ml
@ -3737,6 +3737,59 @@ level "1"
    some_nil ~opt:"-O0" ();
    some_nil ~x86:true ();
    (* ── Typed containers into dyn as views, M2 item 3 ────────────────
       programs/dyn-view.flan takes its mode from argv, the way bounds.flan
       does, because a survey and a trap cannot share a process: mode 0 is
       the survey proper (a Vec view, a fixed-array view, a slice view, a
       bool Vec's view and a view over a Vec that is an ELEMENT of a global
       array, each written through one side and read through the other, plus
       a push through the Vec view that grows and moves it), and
       modes 1 and 2 are the two ways a view refuses — out of range, and a
       write whose dyn tag does not match the element type. The expected
       text for mode 0 was captured from the running program. *)
    let dyn_view_out =
      "[ 10 20 30]\n999\n777\n4\n40\n\
       [ 1 2 3 4]\n100\n400\n\
       [ 1.5 2.5 3.5]\n9.5\n\
       [ true false]\ntrue\n\
       [ 111 222]\n3\n333\n"
    in
    let dyn_view ?opt ?x86 () =
      let exe = compile ?opt ?x86 "programs/dyn-view.flan" in
      let name suffix =
        "dyn: a typed container's view" ^ suffix
        ^ (match opt with Some o -> ", " ^ o | None -> "")
        ^ (match x86 with Some true -> ", --x86" | _ -> "")
      in
      let code, text = run exe (Some "0") in
      if code <> 0 || text <> dyn_view_out then begin
        incr failures;
        Printf.printf
          "FAIL  %s\n        got: %S (exit %d)\n     wanted: %S (exit 0)\n"
          (name "") text code dyn_view_out
      end;
      let code, text = run exe (Some "1") in
      if code <> 134 || not (contains text "index 5 is out of bounds")
      then begin
        incr failures;
        Printf.printf
          "FAIL  %s\n        got: %S (exit %d)\n     wanted a range trap \
           (exit 134)\n" (name ", out of range") text code
      end;
      let code, text = run exe (Some "2") in
      if code <> 134 || not (contains text "this view's elements are int")
      then begin
        incr failures;
        Printf.printf
          "FAIL  %s\n        got: %S (exit %d)\n     wanted a tag-check \
           trap (exit 134)\n" (name ", wrong-type write") text code
      end;
      (try Sys.remove exe with Sys_error _ -> ())
    in
    dyn_view ();
    dyn_view ~opt:"-O0" ();
    dyn_view ~x86:true ();
    (* The root count, which is the part of this feature the runs above cannot
       check — and the reason has outlived the stub it was first written
       about. flan_dyn.c's trigger has a one-megabyte floor, and not one
@ -3810,7 +3863,7 @@ level "1"
      [ "programs/dyn-basic.flan"; "programs/dyn-vec.flan";
        "programs/dyn-struct.flan";
        "programs/dyn-global.flan"; "programs/dyn-boundary.flan";
-        "programs/dyn-defer.flan";
+        "programs/dyn-defer.flan"; "programs/dyn-view.flan";
        (* Included for the same reason every dyn program is, though this
           check cannot see the slot M2 item 4 actually added: [%dx]/[%ax]
           are the pool-ran-dry fallback for a temporary [root_plan] COUNTED
--- a/test/test_dyn.ml
+++ b/test/test_dyn.ml
@ -20,11 +20,25 @@
     nested    a chain of vecs sixty-four deep, traced through one root
     sharing   one object held three times — written through one path and read
               through another, and swept once when the last goes
     view      M2 item 3: a typed container's view, driven directly over a
               hand-built flan_vec header and a plain C array — the runtime
               half of "typed containers into dyn as views", with no
               compiler in the loop. Also carries the view-aware equality
               review's third finding asked for: two views, a view against
               a heap vec, equal contents and differing ones
     layout    the three restatements of flan_vec's layout — flan_rt.c's
               real one, flan_dyn.c's mirror, and this file's [hand_vec] —
               compared field by field, which is what turns a struct any one
               of the three reorders into a FAIL line here instead of a
               silent corruption at whichever view next reads through it
     refuse:*  twenty-four refusals, one process each, asserted on the sentence
               as well as on the status: a process that died some other way is
               not the guard firing, and the exit code cannot tell them apart
     refuseview:*  five more refusals, the view's own: out of range and a
               mismatched write on each of the three element kinds, and a
               push against a flat (slice or array) view
-   One binary, built once, run twenty-nine times. The build is the expensive
+   One binary, built once, run thirty-six times. The build is the expensive
   part and the runs are milliseconds, which is what keeps this inside
   `dune test` rather than behind an alias. *)
@ -133,6 +147,30 @@ let () =
      fail "interior sharing\n        got: %S (exit %d)\n     wanted: %S"
        out code want_sh;
    (* M2 item 3, the runtime's half: a flat view over a fixed C array (reads
       box, writes tag-check, and a write through the view is the array's own
       write and vice versa — proving it is a view and not a copy), a Vec
       view over a hand-built header, pushed through twenty times so the
       header's own [ptr] moves under it — the case that says the descriptor
       pointing AT the header rather than snapshotting it is what survives a
       growth — a bool view and a float view, so the element dispatch is
       exercised on all three kinds dyn_ops.c's [view] carries, and
       [dyn_equal] made view-aware: two views over equal bytes, two views
       over different bytes, a view against an equal heap vec and against a
       differing one. *)
    let code, out, err = run "view" in
    if code <> 0 || out <> "view ok\n" then
      fail "a typed container's view\n        got: %S (exit %d, err %S)"
        out code err;
    (* The three restatements of flan_vec's layout, compared field by field —
       see dyn_ops.c's [layout] and [hand_vec]'s comment for what ties them
       together and why nothing at compile time otherwise does. *)
    let code, out, err = run "layout" in
    if code <> 0 || out <> "layout ok\n" then
      fail "flan_vec's three restatements\n        got: %S (exit %d, err %S)"
        out code err;
    (* Every refusal. The pair is (mode, a phrase the sentence must contain);
       the phrase is chosen to be the part that says *which* mistake it was,
       so a message that named the wrong operation or the wrong tag would not
@ -176,11 +214,34 @@ let () =
           fail "%s did not say %S; it said %S" mode phrase err)
      refusals;
    (* The view's own refusals: an index outside it, a write whose dyn tag
       does not match the element the view holds — once per element kind, so
       the tag-check is asserted on int, on float and on bool separately and
       not only on the one this file happens to build first — and a push
       against a flat (slice or array) view, which cannot grow by
       construction and says so rather than corrupting whatever follows it
       in memory. *)
    let view_refusals =
      [ ("range", "index 2 is out of bounds for vec of length 2");
        ("wrongwrite", "this view's elements are int");
        ("wrongbool", "this view's elements are bool");
        ("wrongfloat", "this view's elements are float");
        ("flatpush", "this view is a slice or an array and cannot grow") ]
    in
    List.iter
      (fun (mode, phrase) ->
         let code, out, err = run ("refuseview:" ^ mode) in
         if code = 0 then
           fail "%s returned rather than trapping: %S" mode out
         else if not (has err phrase) then
           fail "%s did not say %S; it said %S" mode phrase err)
      view_refusals;
    (try Sys.remove exe with Sys_error _ -> ());
    (* A line on the way out, because a test that says nothing when it passes
       is a test nobody can tell from a test that did not run. *)
    if !failures = 0 then
-      Printf.printf "  ok   the dyn runtime: %d refusals and six runs\n"
+      Printf.printf "  ok   the dyn runtime: %d refusals and eight runs\n"
-        (List.length refusals)
+        (List.length refusals + List.length view_refusals)
    else exit 1
  | _ -> print_endline "SKIP  test_dyn: no clang"
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@ -945,15 +945,135 @@ let () =
  rejects_check "a parameter named after a type" "(defn f [i64 x] ())"
    ~needle:"cannot also be this parameter's name";
-  (* The three "not yet" refusals, each by name and each for its own reason.
+  (* M2 item 3 lifted the container-into-dyn refusal: a [(Vec T)], a slice or
-
+     a fixed array with an i64/f64/bool element now crosses as a VIEW rather
-     A typed container does not box: [(Vec i64)] has a representation the dyn
+     than refusing — but only when its storage is permanent, a global's,
-     runtime cannot walk, and the heterogeneous container at this milestone is
+     which review added after the first landing: a view's descriptor chases
-     the runtime's own from [(vec-new dyn)]. *)
+     the container's own address on every operation, and a container whose
-  rejects_check "a typed container boxed into dyn"
+     address dies with a frame is exactly the dangling dyn value the dynamic
     side refuses to hand back. Every accepting row below views a global. A
     [(Map K V)] still refuses regardless of storage — it rides a
     representation this milestone does not give a view — and so does any
     container whose element is outside the three the view can hold. *)
  accepts "a typed Vec boxed into dyn is a view, not a refusal"
    "(defvar v (Vec i64) (vec-new i64))\n\
     (defn take [d dyn] i32 1)\n\
     (defn main [] i32 (take v))";
  accepts "a slice boxed into dyn is a view"
    "(defvar xs [3 i64])\n\
     (defn take [d dyn] i32 1)\n\
     (defn main [] i32 (take (slice xs 0 3)))";
  accepts "a fixed array boxed into dyn is a view"
    "(defvar a [4 i64])\n\
     (defn take [d dyn] i32 1)\n\
     (defn main [] i32 (take a))";
  accepts "a bool Vec's view"
    "(defvar v (Vec bool) (vec-new bool))\n\
     (defn take [d dyn] i32 1)\n\
     (defn main [] i32 (take v))";
  accepts "an f64 Vec's view"
    "(defvar v (Vec f64) (vec-new f64))\n\
     (defn take [d dyn] i32 1)\n\
     (defn main [] i32 (take v))";
  (* The element restriction is still refused, and by name: a string element
     would need a dyn string's own boxing, whose payload is a pointer into
     the collector's heap, planted where nothing will ever trace it. *)
  rejects_check "a Vec of strings does not view into dyn yet"
    "(defvar v (Vec string) (vec-new string))\n\
     (defn take [d dyn] i32 1)\n\
     (defn main [] i32 (take v))"
    ~needle:"does not cross into dyn yet";
  rejects_check "an i32 element is not one of the view's three"
    "(defvar v (Vec i32) (vec-new i32))\n\
     (defn take [d dyn] i32 1)\n\
     (defn main [] i32 (take v))"
    ~needle:"does not cross into dyn yet";
  (* A typed (Map K V) is unrelated to item 3 and keeps its own refusal. *)
  rejects_check "a typed Map still refuses into dyn"
    "(defvar m (Map i64 i64) (map-new i64 i64))\n\
     (defn take [d dyn] i32 1)\n\
     (defn main [] i32 (take m))"
    ~needle:"does not cross into dyn yet";
  (* Which of the two refusals wins when both apply. A LOCAL (Vec string)
     fails the lifetime guard and the element check both, and the element
     one has to be the one that speaks: the lifetime message names
     (defvar g ...) as the spelling that works, and for a string element
     the global spelling is refused too, so the other order would hand back
     advice that fails when taken. *)
  rejects_check "a local Vec of strings gets the element refusal, not the \
                 lifetime one"
    "(defn take [d dyn] i32 1)\n\
     (defn main [] i32 (let [v (vec-new string)] (take v)))"
    ~needle:"does not cross into dyn yet";
  (* ── The lifetime guard, added on review ─────────────────────────
     A local, a parameter and a temporary all answer false to
     [permanent_root], and each gets the same message rather than "cannot be
     indexed" or some other accident of which path noticed. *)
  rejects_check "a local Vec does not view into dyn — its frame ends"
    "(defn take [d dyn] i32 1)\n\
     (defn main [] i32 (let [v (vec-new i64)] (take v)))"
-    ~needle:"does not cross into dyn yet";
+    ~needle:"does not cross into dyn as a view here";
  rejects_check "a Vec parameter does not view into dyn"
    "(defn take [d dyn] i32 1)\n\
     (defn give [v (Vec i64)] i32 (take v))\n\
     (defn main [] i32 0)"
    ~needle:"does not cross into dyn as a view here";
  rejects_check "a fixed array local does not view into dyn"
    "(defn take [d dyn] i32 1)\n\
     (defn main [] i32 (let [a (array 4 i64)] (take a)))"
    ~needle:"does not cross into dyn as a view here";
  (* A slice cut from a global is permanent; the same slice expression
     rebound to a local first loses the trace back to it and is refused —
     conservative rather than wrong, and the message says what does work. *)
  accepts "a slice cut from a global inline is still permanent"
    "(defvar xs [3 i64])\n\
     (defn take [d dyn] i32 1)\n\
     (defn main [] i32 (take (slice xs 0 3)))";
  rejects_check "a slice rebound to a local loses the trace and is refused"
    "(defvar xs [3 i64])\n\
     (defn take [d dyn] i32 1)\n\
     (defn main [] i32 (let [s (slice xs 0 3)] (take s)))"
    ~needle:"does not cross into dyn as a view here";
  (* An element of a global is permanent only when the global is an ARRAY.
     An array's elements are inside the global's own storage; a slice's are
     not — a global [[T]] holds ptr+len and nothing more, and what they
     point at may be a frame that has already returned. The refusal row
     below is one word different from the acceptance row above it, which is
     the point: it is the [At] arm's demand for an array at the level being
     indexed and nothing else deciding. Before that guard the refusal row
     compiled and segfaulted with no diagnostic at all. *)
  accepts "an element of a global array is permanent"
    "(defvar rows [2 (Vec i64)])\n\
     (defn take [d dyn] i32 1)\n\
     (defn main [] i32 (take (at rows 0)))";
  rejects_check "an element of a global slice is not permanent"
    "(defvar sv [(Vec i64)])\n\
     (defn take [d dyn] i32 1)\n\
     (defn main [] i32 (take (at sv 0)))"
    ~needle:"does not cross into dyn as a view here";
  (* [(at g i j)] is ONE typed node holding both indices, not two nested
     ones, so a guard that reads the target's type alone sees level zero and
     nothing after it. These two rows pin the multi-index spelling on both
     sides: every level an array is permanent, and a slice at ANY level is
     not — including the second, which the one-level guard accepted and
     which then printed a dead frame's contents with exit 0. *)
  accepts "an element of a global array of arrays is permanent"
    "(defvar rows [2 [3 (Vec i64)]])\n\
     (defn take [d dyn] i32 1)\n\
     (defn main [] i32 (take (at rows 0 1)))";
  rejects_check "an element reached through a slice level is not permanent"
    "(defvar g [2 [[3 i64]]])\n\
     (defn take [d dyn] i32 1)\n\
     (defn main [] i32 (take (at g 0 1)))"
    ~needle:"does not cross into dyn as a view here";
  (* A Vec behind a Ptr is refused even though some Ptrs really are
     heap-durable — the checker cannot tell this one from a Ptr taken off a
     local, and admitting one admits the other. *)
  rejects_check "a Vec behind a Ptr does not view into dyn"
    "(defn take [d dyn] i32 1)\n\
     (defn use [p (Ptr (Vec i64))] i32 (take (deref p)))\n\
     (defn main [] i32 0)"
    ~needle:"does not cross into dyn as a view here";
  (* A bracket *literal* is not a typed container yet, and where a dyn is
     wanted it builds the runtime's own vec instead — the lowering the map
     literal's values ride on, and what makes {:xs [1 2]} mean what it
--- a/test/test_sanitize.ml
+++ b/test/test_sanitize.ml
@ -213,6 +213,17 @@ let corpus =
       ASan's build being asked to trap the same way the plain build does. *)
    "programs/nil-option.flan", [];
    "programs/some-nil.flan", [];
    (* M2 item 3: a typed container's view. Mode 0, the survey — the modes
       that trap are exercised as C refusals in test_dyn.ml's [refuseview:*]
       instead, the same split [bounds.flan]'s "0" argument makes above. A
       view's storage is a plain array or a Vec's own malloc block, neither
       one this collector allocates, so there is nothing here for ASan to
       catch that the runtime tests above did not already exercise directly
       — this row is about the *compiler* lane: the address the checker
       hands the runtime at the crossing, and whether a push through the
       view that grows and moves the Vec leaves anything for ASan's
       use-after-free detection to find. *)
    "programs/dyn-view.flan", [ "0" ];
    "../spike/x86/p13-dyn-collect.flan", [];
    "programs/sand-headless.flan", [];
    "programs/signedness.flan", [];