A slice level after the first index was invisible to the lifetime rule

(at g i j) is one Tast node carrying the whole index list, so the At
arm's guard on target.ty settled level zero and nothing after it. A
global [2 [[3 i64]]] indexed twice reached a slice's element, crossed
into dyn as a view, and printed a returned frame's contents with exit
0 (ASan: stack-use-after-scope in view_box). The arm now steps each
index the way [indexed] does and demands an array at every level;
the Field and Slice arms inherit the fix by recursing into it.

FIX.org

@@ -449,7 +449,9 @@ rename. typed-flan branch freezes the static language pre-dyn.
    [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 checks the target's type for exactly this), or
+   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

lib/check.ml

@@ -1508,11 +1508,15 @@ let view_not_yet loc (container : Types.t) (elem : Types.t) =
    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, and the
+   value's own storage. An element of a permanent *slice* is not: a slice is
-   [At] arm below checks the target's type for exactly that reason: a slice
+   ptr+len, so a global [[T]] holds only the two words, and the storage they
-   is ptr+len, so a global [[T]] holds only the two words, and the storage
+   point at can be a frame that has already gone. The [At] arm below is where
-   they point at can be a frame that has already gone. That distinction is
+   that distinction is made, and it is made per index rather than once: an
-   the whole of the arm's guard. A slice built directly from
+   [(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
@@ -1537,10 +1541,20 @@ 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 :: _) ->
+  | Tast.Prim (Tast.At, target :: idx) ->
-    (match target.Tast.ty with
+    (* [(at g i j)] is ONE node carrying every index, so the target's own type
-     | Types.Array _ -> permanent_root target
+       is only level zero and asking about it alone misses a slice reached at
-     | _ -> false)
+       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
 
@@ -1551,8 +1565,9 @@ let view_not_permanent loc (container : Types.t) =
      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, an element of a slice — even a global slice, \
+     parameter, a temporary, anything reached through a slice at any index \
-     which holds only ptr+len and can point at a frame that is gone — or \
+     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"

test/programs/dyn-view.flan

@@ -16,10 +16,13 @@
 ;;;; 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. test_flan.ml's checker tests carry the refusal side of
+;;;; the data is — and that holds at every index of a multi-index (at g i j),
-;;;; this (a local Vec, a Vec parameter, a Vec behind a Ptr, a slice rebound
+;;;; not just the first, so one slice level anywhere in the walk refuses.
-;;;; to a local, an element of a global slice); this program is the
+;;;; test_flan.ml's checker tests carry the refusal side of this (a local
-;;;; acceptance side, over storage the guard allows.
+;;;; 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

test/test_flan.ml

@@ -968,9 +968,9 @@ let () =
      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 guard on the target's type and nothing
+     the point: it is the [At] arm's demand for an array at the level being
-     else deciding. Before that guard the refusal row compiled and
+     indexed and nothing else deciding. Before that guard the refusal row
-     segfaulted with no diagnostic at all. *)
+     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\
@@ -980,6 +980,21 @@ let () =
      (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. *)