A destroyed arena's allocator is reused by the next arena-new with its epoch kept, a stale dyn view names its site, and the spec fixes the Vec at five words in every build

TODO.org

@@ -1264,20 +1264,11 @@ live bytes, 0 for none, that a =retry= handler raises. The failure bullet says
 "raises the allocator's budget" where it said "grows the arena", since no arena
 grows. A growable arena is not ruled out; nothing here asks for one.
 
-** NEXT The Vec header is not the size the spec fixes
+** DONE The Vec header is not the size the spec fixes
-Decided 2026-09-25: five words in every build, the epoch included, so a release build still traps on a container whose region was released. The spec changes to match the code; nothing else does.
+CLOSED: [2026-09-25]
-Five words in every build rather than the spec's four, and for a stated reason: a
+Five words in every build, the epoch included, so a release build still traps on
-redefinition module is built separately from its host and nothing makes the two
+a container whose region was released. spec-memory.md, "Every build detects a
-agree on a struct size. Give the reload path a way to carry the build flags and
+released region", now says so. Rules out a four-word release layout.
-this falls out.
-Decision needed first: a four-word release header means release builds no longer
-trap on a released region (the epoch check is what reads the fifth word), where
-today every build does. Checked 2026-09-25 and not contained either way: the
-reload side is already consistent (modules and their hosts are both dev builds),
-but the runtime C is compiled with no dev define, so the change is a
-dev-conditional =flan_vec= in flan_rt.c, its mirror in flan_dyn.c and
-test/dyn_ops.c, =%vec= and the Vec's size in both emitters and the debug info,
-and the Map, whose header carries the same word.
 
 ** DONE arena-destroy under a live view reads freed memory
 CLOSED: [2026-09-25]
@@ -1285,6 +1276,9 @@ No ordering of the frees fixes it: the container holds a pointer to the header.
 =arena-destroy= now frees the pages and the arena record and retires the
 allocator header — epoch bumped, procedure trapping as =DestroyedAllocator=,
 never freed — so the stale check reads live memory on every side that makes it.
+The next =arena-new= takes a retired header back, epoch kept, so a loop of them
+stays flat and a container made before the destroy still traps. An =Allocator=
+value kept past its destroy names the new arena once its header is reused.
 Rules out freeing the header while any container may hold it. The
 =DestroyedAllocator= trap prints no site: the allocator procedure is given none. See
 docs/BUILT.md, "Three amendments to a frozen spec".
@@ -1431,8 +1425,8 @@ CLOSED: [2026-09-25]
 ptr+len, like the arithmetic, and every trap they reach prints it — type, range,
 a view's tag check, and push's growth failing. =trap_oom= takes a site and only
 push gives one: its other callers are the collector's own allocations, which
-have no line to name. A stale view's check, reached through =view_len= from the
+have no line to name. A stale view's check prints the site when =at= or
-printers as well, stays siteless.
+=set-at= reaches it; reached from =length=, printing or equality, it has none.
 
 ** TODO A restart has no location
 The restart frame is mirrored across both backends and the runtime, so giving

docs/BUILT.md

@@ -2832,9 +2832,12 @@ the same does not make a container built before the reset valid, which is the wh
 `arena-destroy` hands back the pages and the arena record but not the allocator header. A container made from the
 arena still holds a pointer to that header and reads the epoch through it on its next operation, so freeing the header
 turned the trap into a read of freed memory that happened to see the bumped value (memcheck reported it). The header is
-retired instead — epoch bumped, procedure swapped for one that traps as `DestroyedAllocator`, never freed — which costs
+retired instead — epoch bumped, procedure swapped for one that traps as `DestroyedAllocator`, never freed — and put on a
-one small block per destroyed arena for the life of the process. A second `arena-destroy` of the same allocator does
+list that the next `arena-new` takes from. The epoch is kept on reuse: it only ever rises on a header, so a container
-nothing.
+made before the destroy still records an older number and still traps. Keeping every retired header instead grew
+without bound — ten million `arena-new`/`arena-destroy` rounds peaked at 626 MB against 1.7 MB. The cost of reuse is
+an `Allocator` value kept past its destroy: while its header is on the list it traps, and once a later `arena-new` has
+taken the header it names that new arena. A second `arena-destroy` of the same allocator, before reuse, does nothing.
 
 **2. `context/allocator` and `context/temp` are dynamic variables with save and restore, not extra parameters.** The
 spec says the allocator is "part of the calling convention". The literal reading touches every function signature, the

runtime/flan_dyn.c

@@ -557,7 +557,8 @@ 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 int64_t  view_len(const uint8_t *loc, int64_t loclen, 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);
@@ -633,7 +634,7 @@ static void render(dyn_sink w, flan_dyn v, int depth, int nested) {
   }
   default: {
     flan_obj *o = dyn_obj(v);
-    int64_t i, n = o->kind == OBJ_VIEW ? view_len("print", o) : o->len;
+    int64_t i, n = o->kind == OBJ_VIEW ? view_len(NULL, 0, "print", o) : o->len;
     emit(w, "[");
     for (i = 0; i < n; i++) {
       emit(w, " ");
@@ -750,7 +751,7 @@ static void say_render(sayer *s, flan_dyn v, int depth) {
   }
   default: {
     flan_obj *o = dyn_obj(v);
-    int64_t i, n = o->kind == OBJ_VIEW ? view_len("print", o) : o->len;
+    int64_t i, n = o->kind == OBJ_VIEW ? view_len(NULL, 0, "print", o) : o->len;
     if (depth >= 2) { say_puts(s, "[...]"); return; }
     say_puts(s, "[");
     for (i = 0; i < n && s->n < s->cap - 8; i++) {
@@ -1979,11 +1980,13 @@ static int64_t view_elem_size(int32_t elem) {
  * 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) {
+static void view_vec_check(const uint8_t *loc, int64_t loclen, 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);
+      trap_where(loc, loclen);
       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",
@@ -1996,10 +1999,11 @@ static void view_vec_check(const char *op, flan_dyn_vec_hdr *h) {
 /* [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) {
+static int64_t view_len(const uint8_t *loc, int64_t loclen, 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);
+    view_vec_check(loc, loclen, op, h);
     return h->len;
   }
   return o->u.view.len;
@@ -2031,7 +2035,7 @@ static flan_dyn view_box(int32_t elem, const uint8_t *p) {
  * 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;
+  return o->kind == OBJ_VIEW ? view_len(NULL, 0, "=", o) : o->len;
 }
 
 static flan_dyn vecish_at(flan_obj *o, int64_t i) {
@@ -2106,7 +2110,7 @@ flan_dyn flan_dyn_len(flan_dyn v) {
   }
   if (is_vec(v)) {
     flan_obj *o = dyn_obj(v);
-    if (o->kind == OBJ_VIEW) return flan_dyn_from_i64(view_len("length", o));
+    if (o->kind == OBJ_VIEW) return flan_dyn_from_i64(view_len(NULL, 0, "length", o));
     return flan_dyn_from_i64(o->len);
   }
   trap1(NULL, 0, TYPE_TRAP, "length", "only a text, a vec or a map has one", v);
@@ -2134,7 +2138,7 @@ flan_dyn flan_dyn_at(flan_dyn v, flan_dyn i, const uint8_t *loc,
   k = need_index(loc, loclen, "at", v, i);
   o = dyn_obj(v);
   if (o->kind == OBJ_VIEW) {
-    int64_t len = view_len("at", o);
+    int64_t len = view_len(loc, loclen, "at", o);
     if (k < 0 || k >= len) trap_range(loc, loclen, "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));
@@ -2156,7 +2160,7 @@ void flan_dyn_set_at(flan_dyn v, flan_dyn i, flan_dyn x, const uint8_t *loc,
   k = need_index(loc, loclen, "set-at", v, i);
   o = dyn_obj(v);
   if (o->kind == OBJ_VIEW) {
-    int64_t len = view_len("set-at", o);
+    int64_t len = view_len(loc, loclen, "set-at", o);
     uint8_t *p;
     if (k < 0 || k >= len) trap_range(loc, loclen, "set-at", v, k, len);
     p = (uint8_t *)view_base(o) + k * view_elem_size(o->u.view.elem);

runtime/flan_rt.c

@@ -1099,7 +1099,7 @@ struct flan_allocator {
   void           *data;
   uint32_t        caps;
   /* Bumped on every free-all. A container records it and traps if it moved:
-   * spec-memory.md, "Dev builds detect a released region". */
+   * spec-memory.md, "Every build detects a released region". */
   uint64_t        epoch;
   /* Dev accounting for the general-purpose tier: "did you forget to free" is
    * an allocator-tier question and this is the allocator's answer. */
@@ -1430,15 +1430,37 @@ void flan_context_restore(flan_allocator *a) {
   if (a) flan_ctx_alloc = a;
 }
 
+/* Allocator headers [flan_arena_destroy] retired, linked through [data]. See
+ * there for why a header is never freed; this is why that does not grow. */
+static flan_allocator *flan_retired;
+
+/* A retired header is taken back rather than a new one made. Its epoch is
+ * kept, never reset: it only ever rises on a header, so a container made from
+ * the arena this header used to serve still records an older number and still
+ * traps. Only the bookkeeping a new arena starts from is cleared. */
+static flan_allocator *flan_header_new(void) {
+  flan_allocator *a = flan_retired;
+  if (a == NULL) return (flan_allocator *)calloc(1, sizeof *a);
+  flan_retired = (flan_allocator *)a->data;
+  a->data = NULL;
+  a->live_blocks = 0;
+  a->live_bytes = 0;
+  a->budget = 0;
+  return a;
+}
+
+static void flan_header_retire(flan_allocator *a);
+
 flan_allocator *flan_arena_new(int64_t cap) {
   flan_allocator *a;
   flan_arena *ar;
   if (cap <= 0) cap = FLAN_TEMP_DEFAULT;
-  a = (flan_allocator *)calloc(1, sizeof *a);
   ar = (flan_arena *)calloc(1, sizeof *ar);
-  if (!a || !ar) { free(a); free(ar); return NULL; }
+  if (!ar) return NULL;
   ar->base = (uint8_t *)malloc((size_t)cap);
-  if (!ar->base) { free(a); free(ar); return NULL; }
+  if (!ar->base) { free(ar); return NULL; }
+  a = flan_header_new();
+  if (!a) { free(ar->base); free(ar); return NULL; }
   ar->cap = cap;
   a->proc = flan_arena_proc;
   a->data = ar;
@@ -1467,10 +1489,14 @@ static void *flan_destroyed_proc(flan_allocator *a, int32_t mode, void *p,
  * its next operation — that read is the whole of the stale-region trap — so
  * freeing the header would turn the trap into a read of freed memory that
  * happens to see the bumped value. The header is retired instead: epoch
- * bumped, procedure swapped for one that refuses, never freed. That is one
+ * bumped, procedure swapped for one that refuses, never freed. Retired
- * small block per destroyed arena, kept for the life of the process.
+ * headers go on a list that [flan_arena_new] takes from, so a program that
+ * makes and destroys arenas in a loop holds as many headers as it ever had
+ * arenas alive at once.
  *
- * A second destroy finds the retired procedure and does nothing. */
+ * A second destroy finds the retired procedure and does nothing — while the
+ * header is still on the list. Once a later arena-new has taken it back, the
+ * old Allocator value names the new arena. */
 void flan_arena_destroy(flan_allocator *a) {
   flan_arena *ar;
   if (!a || a->proc != flan_arena_proc) return;
@@ -1481,10 +1507,15 @@ void flan_arena_destroy(flan_allocator *a) {
   flan_dev_reg_dead_range(ar->base, ar->cap);
   free(ar->base);
   free(ar);
+  flan_header_retire(a);
+}
+
+static void flan_header_retire(flan_allocator *a) {
   a->proc = flan_destroyed_proc;
-  a->data = NULL;
   a->live_blocks = 0;
   a->live_bytes = 0;
+  a->data = flan_retired;
+  flan_retired = a;
 }
 
 flan_allocator *flan_heap_allocator(void) { return &flan_heap; }
@@ -1700,7 +1731,7 @@ _Noreturn void flan_vec_bounds_fail(const uint8_t *loc, int64_t loclen,
   rt_die();
 }
 
-/* spec-memory.md, "Dev builds detect a released region". This is the check
+/* spec-memory.md, "Every build detects a released region". This is the check
  * that makes the epoch word worth carrying, and it runs on every operation,
  * not only in a dev build — see the header on why the words are unconditional.
  * A Vec that never allocated has no allocator and nothing to check. */

spec-memory.md

@@ -594,15 +594,16 @@ Whatever the dead element owned stays allocated until `free-all`. That is a
 region leak bounded by the region, which is what a region already is; it is not
 a use-after-free, because nothing was released.
 
-### Dev builds detect a released region
+### Every build detects a released region
 
-A `Vec` or `Map` records its allocator (see above). In a dev build it also
+A `Vec` or `Map` records its allocator (see above) and that allocator's
-records that allocator's **epoch** — a counter the allocator bumps on every
+**epoch** — a counter the allocator bumps on every `free-all` and on
-`free-all`. Any operation on a container whose recorded epoch has moved traps,
+`arena-destroy`. Any operation on a container whose recorded epoch has moved
-naming the allocation site and the release site. This is a second and separate
+traps, naming the site of the operation. The epoch is in every build, release
-counter from the per-`Vec` generation word that catches stale slices; the two
+included, so the layout of a `Vec` is `ptr + len + cap + allocator + epoch` —
-answer different questions and must not be conflated. Both are dev-only: the
+five words — whatever the build flags. One layout is also what lets a
-release layout of a `Vec` is `ptr + len + cap + allocator` and nothing more.
+redefinition module, built separately from its host, agree with it on the size
+of a struct holding a `Vec`.
 
 This is what covers a use after `free-all`, including the case the section
 above makes reachable: an inner container's header copied *out* of an

test/programs/destroy-region.flan

@@ -8,19 +8,45 @@
 ;;;; Argument 1 is the other use of a destroyed arena: a new container made
 ;;;; from it, which has no stale epoch to catch and reaches the allocator
 ;;;; itself.
+;;;;
+;;;; Argument 2 is a destroyed allocator taken back by the next arena-new. The
+;;;; container made before the destroy still traps, because the epoch on a
+;;;; header only ever rises.
+;;;;
+;;;; Argument 3 makes and destroys arenas in a loop, as many times as the
+;;;; second argument says. A retired allocator is reused rather than kept, so
+;;;; the loop's memory stays flat however long it runs.
 (defn main [args [string]] i32
-  (let [a (arena-new 4096)
+  (let [which (if (> (length args) 1) (i32 (bytes->i64 (bytes-view (at args 1)))) 0)
-        which (if (> (length args) 1) (i32 (bytes->i64 (bytes-view (at args 1)))) 0)]
+        a (arena-new 4096)]
-    (if (= which 1)
+    (cond
-      (do
+      (= which 1)
-        (arena-destroy a)
+        (do
-        (let [w (vec-new i32 a)]
+          (arena-destroy a)
-          (push w 1)
+          (let [w (vec-new i32 a)]
-          (println (length w))))
+            (push w 1)
-      (let [v (vec-new i32 a)]
+            (println (length w))))
-        (push v 1)
+      (= which 2)
-        (push v 2)
+        (let [v (vec-new i32 a)]
-        (println (at v 1))
+          (push v 1)
-        (arena-destroy a)
+          (arena-destroy a)
-        (println (at v 1)))))
+          (let [b (arena-new 4096)
+                w (vec-new i32 b)]
+            (push w 5)
+            (println (at w 0))
+            (println (at v 0))))
+      (= which 3)
+        (let [n (bytes->i64 (bytes-view (at args 2)))]
+          (arena-destroy a)
+          (dotimes [i (i32 n)]
+            (let [b (arena-new 64)]
+              (arena-destroy b)))
+          (println "done"))
+      :else
+        (let [v (vec-new i32 a)]
+          (push v 1)
+          (push v 2)
+          (println (at v 1))
+          (arena-destroy a)
+          (println (at v 1)))))
   0)

test/programs/dyn-index-site.flan

@@ -4,14 +4,28 @@
 ;;;;
 ;;;; The argument chooses which one fails, one per run, because each ends the
 ;;;; process. The line numbers are asserted by the test, so an edit above them
-;;;; moves them.
+;;;; moves them. Modes 3 and 4 reach at and set-at through a view of a typed
+;;;; Vec whose arena was released, which is a different trap on the same call.
+(defn as-dyn [d dyn] dyn d)
+
+(defonce tv (Vec i64))
+
 (defn main [args [string]] i32
   (let [which (if (> (length args) 1) (i32 (bytes->i64 (bytes-view (at args 1)))) 0)
-        v (vec-new dyn)]
+        v (vec-new dyn)
+        ar (arena-new 4096)]
     (push v 1)
+    (set tv (vec-new i64 ar))
+    (push tv 7)
     (println "before")
     (cond
       (= which 0) (println (at v 5))
       (= which 1) (set (at v 5) 2)
-      :else (let [n (at v 0)] (push n 3))))
+      (= which 2) (let [n (at v 0)] (push n 3))
+      :else
+        (let [dv (as-dyn tv)]
+          (free-all ar)
+          (if (= which 3)
+            (println (at dv 0))
+            (set (at dv 0) 8)))))
   0)

test/programs/map-stale-region.flan

@@ -1,4 +1,4 @@
-;;;; spec-memory.md, "Dev builds detect a released region" — the Map's half.
+;;;; spec-memory.md, "Every build detects a released region" — the Map's half.
 ;;;;
 ;;;; A Map records the epoch of the allocator it was made with, exactly as a
 ;;;; Vec does, and free-all bumps that counter. Any operation on a container

test/programs/stale-region.flan

@@ -1,4 +1,4 @@
-;;;; spec-memory.md, "Dev builds detect a released region".
+;;;; spec-memory.md, "Every build detects a released region".
 ;;;;
 ;;;; A Vec records the epoch of the allocator it was made with, and free-all
 ;;;; bumps that counter. Any operation on a container whose recorded epoch has

test/test_acceptance.ml

@@ -1901,6 +1901,52 @@ let () =
         \        got: %S (exit %d)\n     wanted: exit 134, naming arena-destroy\n"
         text code
     end;
+    (* The retired allocator taken back by the next arena-new: the new
+       arena's container works, and the one made before the destroy still
+       traps, because the epoch on a header only rises. *)
+    let code, text = run exe (Some "2") in
+    if code <> 134 || not (contains text "5\n")
+       || not (contains text "programs/destroy-region.flan:37:")
+       || not (contains text "allocator was released")
+    then begin
+      incr failures;
+      Printf.printf
+        "FAIL  a container whose destroyed allocator was reused\n\
+        \        got: %S (exit %d)\n     wanted: 5, then the trap at 37 (exit 134)\n"
+        text code
+    end;
+    (* And the reuse is what keeps a make-and-destroy loop flat: two million
+       rounds peak where a thousand do. Without it each round kept a header,
+       about 130 MB here. Peak resident size comes from /usr/bin/time, and the
+       case is skipped without one. *)
+    if Sys.file_exists "/usr/bin/time" then begin
+      let peak n =
+        let o = Filename.temp_file "flan-destroy" ".rss" in
+        let code =
+          Sys.command
+            (Printf.sprintf "/usr/bin/time -f %%M -o %s %s 3 %d > /dev/null 2>&1"
+               (Filename.quote o) (Filename.quote exe) n)
+        in
+        let kb =
+          try int_of_string (String.trim (In_channel.with_open_bin o
+                                             In_channel.input_all))
+          with _ -> -1
+        in
+        (try Sys.remove o with Sys_error _ -> ());
+        (code, kb)
+      in
+      let c1, small = peak 1000 and c2, large = peak 2_000_000 in
+      if c1 <> 0 || c2 <> 0 || small < 0 || large < 0
+         || large - small > 20_000
+      then begin
+        incr failures;
+        Printf.printf
+          "FAIL  arena-new and arena-destroy in a loop\n\
+          \        got: %d KB after 1000 rounds, %d KB after 2000000 (exits %d, %d)\n\
+          \     wanted: within 20 MB of each other\n"
+          small large c1 c2
+      end
+    end;
     (try Sys.remove exe with Sys_error _ -> ());
 
 
@@ -4823,9 +4869,13 @@ level "1"
                (match x86 with Some true -> ", --x86" | _ -> "")
                text code want
            end)
-        [ ("0", "dyn-index-site.flan:14:28: dyn at: index 5 is out of bounds");
+        [ ("0", "dyn-index-site.flan:22:28: dyn at: index 5 is out of bounds");
-          ("1", "dyn-index-site.flan:15:19: dyn set-at: index 5 is out of bounds");
+          ("1", "dyn-index-site.flan:23:19: dyn set-at: index 5 is out of bounds");
-          ("2", "dyn-index-site.flan:16:31: dyn push: int and int") ];
+          ("2", "dyn-index-site.flan:24:37: dyn push: int and int");
+          ("3", "dyn-index-site.flan:29:22: dyn at: this view's container's \
+                 allocator was released");
+          ("4", "dyn-index-site.flan:30:13: dyn set-at: this view's \
+                 container's allocator was released") ];
       (try Sys.remove exe with Sys_error _ -> ())
     in
     index_site ();

test/test_valgrind.ml

@@ -250,6 +250,8 @@ let corpus =
        its epoch until the allocator was made to outlive its arena. *)
     "programs/destroy-region.flan", [];
     "programs/destroy-region.flan", [ "1" ];
+    "programs/destroy-region.flan", [ "2" ];
+    "programs/destroy-region.flan", [ "3"; "1000" ];
     "programs/string-of-bytes.flan", [];
     "programs/text.flan", [];
     "programs/time.flan", [];