An allocator outlives the arena arena-destroy hands back, so a container made from it traps on a read of live memory

TODO.org

@@ -1260,11 +1260,14 @@ redefinition module is built separately from its host and nothing makes the two
 agree on a struct size. Give the reload path a way to carry the build flags and
 this falls out.
 
-** TODO arena-destroy under a live view reads freed memory
-The epoch check that makes free-all safe under a live view does not survive
-=arena-destroy=, which frees the block holding the epoch. It happens to trap in
-practice because the freed block still holds the bumped value. A question about
-=arena-destroy='s ordering, not about views, and the typed side has the same shape.
+** DONE arena-destroy under a live view reads freed memory
+CLOSED: [2026-09-25]
+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.
+Rules out freeing the header while any container may hold it. See
+docs/BUILT.md, "Three amendments to a frozen spec".
 
 ** DONE Map removal costs a backward-shift loop
 Removal landed, with the loop the spec predicted as its cost. Deferring it was

docs/BUILT.md

@@ -2829,6 +2829,13 @@ handing the pages back only to ask for them again is the unusual one. Taking the
 the table the spec froze at four names; a second operation does not. The epoch is bumped either way — the pages being
 the same does not make a container built before the reset valid, which is the whole point of the trap.
 
+`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
+one small block per destroyed arena for the life of the process. A second `arena-destroy` of the same allocator 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
 FFI shim, the dev trampolines and the reload ABI, for the same observable behaviour, and it collides with every other

runtime/flan_rt.c

@@ -1448,6 +1448,29 @@ flan_allocator *flan_arena_new(int64_t cap) {
   return a;
 }
 
+/* What an allocator's procedure becomes once [flan_arena_destroy] has handed
+ * its arena back. Every request traps, because there is nothing left to serve
+ * it from and answering NULL would read as exhaustion — which a retry handler
+ * that raises the budget would then retry for ever. */
+static void *flan_destroyed_proc(flan_allocator *a, int32_t mode, void *p,
+                                 int64_t old_size, int64_t size, int64_t align) {
+  (void)a; (void)mode; (void)p; (void)old_size; (void)size; (void)align;
+  rt_flush_out();
+  fprintf(stderr,
+          "this allocator was destroyed by arena-destroy, so nothing can be "
+          "allocated from it or released through it\n");
+  rt_trap((const uint8_t *)"DestroyedAllocator", 18);
+}
+
+/* The pages and the arena record go; the allocator itself does not. Every
+ * container made from it holds this pointer and reads [epoch] through it on
+ * 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
+ * small block per destroyed arena, kept for the life of the process.
+ *
+ * A second destroy finds the retired procedure and does nothing. */
 void flan_arena_destroy(flan_allocator *a) {
   flan_arena *ar;
   if (!a || a->proc != flan_arena_proc) return;
@@ -1458,7 +1481,10 @@ void flan_arena_destroy(flan_allocator *a) {
   flan_dev_reg_dead_range(ar->base, ar->cap);
   free(ar->base);
   free(ar);
-  free(a);
+  a->proc = flan_destroyed_proc;
+  a->data = NULL;
+  a->live_blocks = 0;
+  a->live_bytes = 0;
 }
 
 flan_allocator *flan_heap_allocator(void) { return &flan_heap; }

test/programs/destroy-region.flan

@@ -0,0 +1,26 @@
+;;;; stale-region.flan's trap, reached through arena-destroy rather than
+;;;; free-all. The difference is what the check reads: free-all keeps the
+;;;; allocator and bumps its epoch, while arena-destroy hands the arena back,
+;;;; and a container made from it still points at the allocator to read the
+;;;; epoch from. The allocator therefore outlives its arena, so that read is of
+;;;; memory that is still there and the trap names the site.
+;;;;
+;;;; 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.
+(defn main [args [string]] i32
+  (let [a (arena-new 4096)
+        which (if (> (length args) 1) (i32 (bytes->i64 (bytes-view (at args 1)))) 0)]
+    (if (= which 1)
+      (do
+        (arena-destroy a)
+        (let [w (vec-new i32 a)]
+          (push w 1)
+          (println (length w))))
+      (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/test_acceptance.ml

@@ -1876,6 +1876,33 @@ let () =
     end;
     (try Sys.remove exe with Sys_error _ -> ());
 
+    (* The same trap after arena-destroy, which hands the arena back: the
+       container's allocator pointer has to still be readable for the epoch
+       check to run at all, so the allocator outlives its arena. A new
+       container made from the destroyed arena has no stale epoch, and what
+       stops it is the allocator itself. Both are also clean under memcheck,
+       which is where reading a freed allocator showed up. *)
+    let exe = compile "programs/destroy-region.flan" in
+    let code, text = run exe None in
+    if code <> 134 || not (contains text "programs/destroy-region.flan:")
+       || not (contains text "allocator was released")
+    then begin
+      incr failures;
+      Printf.printf
+        "FAIL  a container used after its arena was destroyed\n\
+        \        got: %S (exit %d)\n     wanted: exit 134, naming the site\n"
+        text code
+    end;
+    let code, text = run exe (Some "1") in
+    if code <> 134 || not (contains text "destroyed by arena-destroy") then begin
+      incr failures;
+      Printf.printf
+        "FAIL  allocating from a destroyed arena\n\
+        \        got: %S (exit %d)\n     wanted: exit 134, naming arena-destroy\n"
+        text code
+    end;
+    (try Sys.remove exe with Sys_error _ -> ());
+
 
     (try Sys.remove exe with Sys_error _ -> ());
 

test/test_valgrind.ml

@@ -186,7 +186,7 @@ let check label path args ~checks =
    - shadow-pkg.flan, which is a package fragment with no main and does not
      link on its own.
 
-   The seven programs here that abort by design — error, exhausted-unhandled,
+   The programs here that abort by design — destroy-region, error, exhausted-unhandled,
    free-all-refused, map-stale-region, slurp-unhandled,
    stale-region — are
    kept. A trap is a controlled abort after an fprintf, and "the trap still
@@ -246,6 +246,10 @@ let corpus =
     "programs/slurp.flan", [];
     "programs/slurp-unhandled.flan", [];
     "programs/stale-region.flan", [];
+    (* The same trap after arena-destroy, which read the freed allocator for
+       its epoch until the allocator was made to outlive its arena. *)
+    "programs/destroy-region.flan", [];
+    "programs/destroy-region.flan", [ "1" ];
     "programs/string-of-bytes.flan", [];
     "programs/text.flan", [];
     "programs/time.flan", [];