A global slice's element is not permanent, and four comments that were not true

The [At] arm of [permanent_root] recursed through any indexed target, so an
element of a global SLICE answered permanent the way an element of a global
ARRAY does. An array's elements are inside the global's storage; a slice's
are ptr+len pointing wherever, which can be a frame already returned — the
program that stashes (slice local 0 2) in a global slice and views an element
compiled and segfaulted with no diagnostic. The arm now recurses only when
the target's own type is an Array.

With it, the refusal/acceptance pair in test_flan.ml (one word apart) and a
view over an element of a global array in dyn-view.flan's mode 0.

The element check now runs before the lifetime check in all three container
arms: a local (Vec string) was told to make it a global, and a global
(Vec string) is refused anyway, so the advice was a dead end.

And the four strings that claimed more than the code does. flan_dyn.h
already had the honest version — a view is exactly as stale-safe as the
thing it is a view of — so the refusal message, box's comment and FIX.org
now say that instead of promising a dyn value can never dangle; a global
[i64] cut from a dead frame still passes and still reads it (ASan:
stack-use-after-scope in view_box). The element message no longer tells a
(Vec string) that string is not the case the restriction exists for.
dyn_ops.c's hand_vec comment no longer says flan_rt.c is unlinked when it
calls two of its functions; flan_rt.c said the same thing and is fixed too.
FIX.org's arena paragraph now separates the header's lifetime (compile time,
already covered) from releasing the arena under a live view: free-all traps
cleanly on the epoch, arena-destroy is a heap-use-after-free in
view_vec_check, the same gap flan_vec_check has on the typed side.

FIX.org

@@ -443,10 +443,13 @@ rename. typed-flan branch freezes the static language pre-dyn.
    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 follows Clojure and Common Lisp, where holding a
+   on the dynamic side Flan aims where Clojure and Common Lisp are — holding
-   value never hands you garbage, so a container may cross into dyn as a
+   a value should not hand you garbage — so a container may cross into dyn as
-   view only when its own storage is permanent — a global's. [permanent_root]
+   a view only when its own storage is permanent — a global's.
-   in check.ml decides it: a global, a field or an array element of one, or
+   [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
    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
@@ -454,10 +457,33 @@ rename. typed-flan branch freezes the static language pre-dyn.
    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. An arena-held header is not a separate case
+   the exact hole this closes.
-   at all — an arena changes where a Vec's elements live, never where its
+
-   own header (the binding) lives, so it is already covered by the cases
+   The rule is a narrowing, not a proof, and flan_dyn.h states the property
-   above.
+   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

lib/check.ml

@@ -1468,12 +1468,13 @@ 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 — %s is neither a width this milestone's view carries \
+        elements only, and %s is not one of the three. The restriction \
-        nor the case the restriction exists for, which is a string element: \
+        exists for the string case: a dyn string's form is a pointer into \
-        a dyn string's form is a pointer into the collector's heap, and a \
+        the collector's heap, and a typed container's storage is memory the \
-        typed container's storage is memory the collector never scans, so \
+        collector never scans, so a write through a view over strings could \
-        a write through a view over strings could plant a pointer where \
+        plant a pointer where nothing will ever trace it. Every other \
-        nothing will ever trace it"
+        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
@@ -1487,19 +1488,32 @@ let view_not_yet loc (container : Types.t) (elem : Types.t) =
    — reachable now for the first time, not a pre-existing hole this lane
    merely inherited.
 
-   On the dynamic side Flan follows Clojure and Common Lisp: holding a value
+   On the dynamic side Flan aims where Clojure and Common Lisp are: holding
-   can never hand you garbage. Treating a view as a bare pointer and calling
+   a value should not hand you garbage. Treating a view as a bare pointer and
-   the lifetime the programmer's problem is the Odin answer, and neither
+   calling the lifetime the programmer's problem is the Odin answer, and
-   Odin nor C stops it — but a dyn value that can dangle is the wrong trade
+   neither Odin nor C stops it — this guard is the trade going the other way,
-   on this side of the language, so this is refused rather than merely
+   refused rather than merely documented.
-   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 an
+   permanent value is permanent at the same fixed offset from it, and so is
-   array element of one likewise; both are still inside the global's own
+   an element of a permanent *array* — both are still inside the permanent
-   storage. A slice built directly from [(slice T lo hi)] inherits the
+   value's own storage. An element of a permanent *slice* is not, and the
+   [At] arm below checks the target's type for exactly that reason: 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. That distinction is
+   the whole of the arm's guard. 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
@@ -1523,20 +1537,25 @@ 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 :: _) -> permanent_root target
+  | Tast.Prim (Tast.At, target :: _) ->
+    (match target.Tast.ty with
+     | Types.Array _ -> permanent_root target
+     | _ -> false)
   | 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 dyn value that can dangle is not one this \
+     to outlive the view, and a view is exactly as stale-safe as the thing \
-     language will hand back. A global's does: (defvar g %s ...) viewed \
+     it is a view of, no more and no less. A global's storage does outlive \
-     from anywhere is sound, because a global's address is fixed for the \
+     it: (defvar g %s ...) viewed from anywhere reads storage fixed for the \
-     process. A local, a parameter, a temporary, or anything reached \
+     process, and so does a field or an array element of one. A local, a \
-     through a (Ptr T) is refused for the same reason — the checker cannot \
+     parameter, a temporary, an element of a slice — even a global slice, \
-     tell a heap-durable pointer from a frame's own, and admitting one \
+     which holds only ptr+len and can point at a frame that is gone — or \
-     admits the other"
+     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 =
@@ -1573,26 +1592,32 @@ let box loc (e : Tast.expr) : Tast.expr =
      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 ->
-    if not (permanent_root e) then view_not_permanent loc e.Tast.ty
+    (match view_elem elem with
-    else
+     | None -> view_not_yet loc e.Tast.ty elem
-      (match view_elem elem with
+     | Some k ->
-       | Some k -> dyn "flan_dyn_view_vec" [ e; view_elem_lit loc k ]
+       if not (permanent_root e) then view_not_permanent loc e.Tast.ty
-       | None -> view_not_yet loc e.Tast.ty elem)
+       else dyn "flan_dyn_view_vec" [ e; view_elem_lit loc k ])
   | Types.Slice elem ->
-    if not (permanent_root e) then view_not_permanent loc e.Tast.ty
+    (match view_elem elem with
-    else
+     | None -> view_not_yet loc e.Tast.ty elem
-      (match view_elem elem with
+     | Some k ->
-       | Some k -> dyn "flan_dyn_view_flat" [ e; view_elem_lit loc k ]
+       if not (permanent_root e) then view_not_permanent loc e.Tast.ty
-       | None -> view_not_yet loc e.Tast.ty elem)
+       else dyn "flan_dyn_view_flat" [ e; view_elem_lit loc k ])
   | Types.Array (n, elem) ->
-    if not (permanent_root e) then view_not_permanent loc e.Tast.ty
+    (match view_elem elem with
-    else
+     | None -> view_not_yet loc e.Tast.ty elem
-      (match view_elem elem with
+     | Some k ->
-       | 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 ]
+           [ e; mk loc dyn_i64 (Tast.Int (n, Types.I64)); view_elem_lit loc k ])
-       | None -> view_not_yet loc e.Tast.ty elem)
   | Types.Map _ ->
     no_dyn_yet loc ~into:true e.Tast.ty
       ". The dyn container at this milestone is the runtime's own, from \

runtime/flan_dyn.h

@@ -173,8 +173,12 @@ flan_dyn flan_dyn_need_not_nil(flan_dyn v);
  * [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: a local's slot, a global, a
+ * lives under. That address is the Vec's home, fixed for as long as the Vec
- * field, fixed for as long as the Vec exists. Every operation re-reads that
+ * 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

runtime/flan_rt.c

@@ -1493,8 +1493,9 @@ typedef struct 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 with no [flan_rt.c]
+ * test/dyn_ops.c's [hand_vec], which builds one by hand because it has no
- * linked in to call [flan_vec_init] for it. None of the three can [#include]
+ * [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

test/dyn_ops.c

@@ -353,9 +353,12 @@ static void ops(void) {
 /* 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]): there is no [flan_vec_init] to call
+ * compile time (see [Build.compile_c]) — so the header below is built by
- * from here, so the header below is built by hand, the same five words
+ * hand, the same five words [flan_vec_grow] would leave behind after a few
- * [flan_vec_grow] would leave behind after a few pushes.
+ * 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]

test/programs/dyn-view.flan

@@ -13,10 +13,13 @@
 ;;;; 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. test_flan.ml's checker tests carry the refusal side of this
+;;;; process — as is a field of one, and an ELEMENT of one when the global
-;;;; (a local Vec, a Vec parameter, a Vec behind a Ptr, a slice rebound to a
+;;;; is an array, whose elements sit inside its own storage. An element of a
-;;;; local); this program is the acceptance side, over storage the guard
+;;;; global SLICE is not: the slice is ptr+len and says nothing about where
-;;;; allows.
+;;;; the data is. 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); 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
@@ -40,6 +43,13 @@
 (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))))]
@@ -106,6 +116,21 @@
           (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.

test/test_acceptance.ml

@@ -3702,9 +3702,10 @@ level "1"
     (* ── 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 and a
+       the survey proper (a Vec view, a fixed-array view, a slice view, a
-       bool Vec's view, each written through one side and read through the
+       bool Vec's view and a view over a Vec that is an ELEMENT of a global
-       other, plus a push through the Vec view that grows and moves it), and
+       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. *)
@@ -3712,7 +3713,8 @@ level "1"
       "[ 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"
+       [ 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

test/test_flan.ml

@@ -923,6 +923,17 @@ let () =
      (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
@@ -952,6 +963,23 @@ let () =
      (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 guard on the target's type 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";
   (* 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. *)