diff --git a/docs/BUILT.md b/docs/BUILT.md
index 0be3459c..0c3c3e97 100644
--- a/docs/BUILT.md
+++ b/docs/BUILT.md
@@ -4692,8 +4692,8 @@ neither of them a function-value question:
 1. The runtime calls `a->proc(a, mode, p, old_size, size, align)` — six C arguments and no transfer channel — and
    every Flan function value's signature ends with one. It is the same mismatch a foreign function's address is
    refused for, pointing the other way.
-2. `Allocator` is opaque and pointer-width, so there is nowhere for a program to put the `flan_allocator` that
-   pointer would have to point at.
+2. `Allocator` is opaque — a pointer to a runtime `flan_allocator` and an incarnation — so there is nowhere for a
+   program to put the `flan_allocator` that pointer would have to point at.
 
 The refusal message says both, and `programs/user-allocator.flan` is the row that holds it. `(arena-new ...)` over a
 backing buffer remains the parameterised allocator that does exist.
diff --git a/lib/types.ml b/lib/types.ml
index 42a309bd..4ff45ee0 100644
--- a/lib/types.ml
+++ b/lib/types.ml
@@ -38,9 +38,10 @@ type t =
      is what lets spec-memory.md's "procedure plus an opaque data pointer" be
      expressed with none of milestone 5's function values — the procedure is a
      C symbol the emitter names and no Flan type ever mentions it. At run time
-     it is a pointer to the runtime's [flan_allocator], never a copy of one:
-     the capability set and the epoch have to be shared by every container
-     made from it, and a copy would give each its own. *)
+     it is two words: a pointer to the runtime's [flan_allocator], never a
+     copy of one — the capability set and the epoch have to be shared by every
+     container made from it — and the incarnation of it the value was made
+     for, which arena-destroy bumps so a stale value traps on use. *)
   | Alloc
   (* [(Vec T)]: ptr + len + cap + allocator, owning and move-only. One
      type-erased runtime over (size, align) stands behind every instantiation,
diff --git a/web/index.html b/web/index.html
index bee16947..f424d0ce 100644
--- a/web/index.html
+++ b/web/index.html
@@ -528,7 +528,7 @@ notation reads as exactly one data item.</p>
 <tr><td><code>(Fn [T ...] R)</code></td><td>a function value, which may have captured</td><td>a code address and an environment pointer</td></tr>
 <tr><td><code>(CFn [T ...] R)</code></td><td>a function value that cannot capture — the <code>C</code> is what a C function pointer would need, not a way to reach C today</td><td>a pointer</td></tr>
 <tr><td><code>dyn</code></td><td>a value the runtime knows the type of and the checker does not — see <a href="#dyn">dyn</a></td><td>one word, on a collected heap</td></tr>
-<tr><td><code>Allocator</code></td><td>an opaque builtin: a proc, its data and a capability set</td><td>a pointer to that</td></tr>
+<tr><td><code>Allocator</code></td><td>an opaque builtin: a proc, its data and a capability set</td><td>a pointer to that, and a count that says whether it has since been destroyed</td></tr>
 <tr><td><code>$t</code></td><td>a type variable — see <a href="#generics">generics</a></td><td>whatever it is instantiated at</td></tr>
 <tr><td>a struct</td><td>value type</td><td>fields in declaration order</td></tr>
 <tr><td>a tagged data type</td><td><code>defdata</code>, matched by case</td><td>tag + the widest payload</td></tr>