diff --git a/lib/check.ml b/lib/check.ml
index 4c36d82..b14836d 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -109,6 +109,20 @@ type ctx = {
      function's defers are already half run and the first transfer's target is
      already in hand. Refused where it is written. *)
   mutable in_defer : bool;
+  (* Move tracking, spec-memory.md's "(Vec T) and (Map K V) are move-only".
+     [dead] is the slots whose value has been moved out, with where it went, so
+     that a second use names the first rather than reporting a type error about
+     nothing. It is flow-sensitive at an [if]: the two arms are checked from
+     the same starting set and the *union* survives the join, so moving in one
+     arm only is still a move afterwards — and moving in both arms, which is
+     legal, is not two errors.
+
+     [borrow] is set only while checking the *target* of an operation that
+     reads a container without consuming it ([at], [len], [as-slice], [push],
+     [reserve], [clone]). Without it every one of those would look like a move
+     and no program could push twice. *)
+  mutable dead : (int * Loc.t) list;
+  mutable borrow : bool;
   (* The function being checked, so a clause lifted out of it can be named
      after it. The name has to be stable and has to say whose it is: a
      redefinition module emits the clauses belonging to the bodies it is
@@ -212,7 +226,8 @@ let rec resolve env ?(seen = []) (t : Ast.texpr) : Types.t =
      | "Ptr", [ a ] -> Types.Ptr (resolve env ~seen a)
      | "Option", [ a ] -> Types.Option (resolve env ~seen a)
      | ("Ptr" | "Option"), _ -> fail loc "(%s T) takes exactly one type" name
-     | "Vec", _ -> unimplemented loc "(Vec T)" 6
+     | "Vec", [ a ] -> Types.Vec (resolve env ~seen a)
+     | "Vec", _ -> fail loc "(Vec T) takes exactly one type"
      | "Map", _ -> unimplemented loc "(Map K V)" 6
      | "Result", _ -> unimplemented loc "(Result T E)" 6
      | "Handle", _ -> unimplemented loc "(Handle T)" 6
@@ -332,6 +347,21 @@ let unit_at loc = mk loc Types.Unit Tast.Unit
    crosses as ptr+len like any other. *)
 let here loc = mk loc Types.String (Tast.Str (Loc.to_string loc))
 
+(* A runtime call, with the result type spelled at the site. *)
+let rt loc ty sym args = mk loc ty (Tast.Prim (Tast.Rt sym, args))
+
+let i64_at loc n = mk loc (Types.Int Types.I64) (Tast.Int (n, Types.I64))
+
+(* spec-memory.md, "Alignment": the number is produced where the concrete
+   element type is known, which without generics is simply the call site. *)
+let size_of loc t = mk loc (Types.Int Types.I64) (Tast.Prim (Tast.SizeOf t, []))
+let align_of loc t = mk loc (Types.Int Types.I64) (Tast.Prim (Tast.AlignOf t, []))
+
+(* The address of an expression, place or not: the type-erased runtime takes
+   the element [push] copies by pointer. *)
+let addr_of loc (e : Tast.expr) =
+  mk loc (Types.Ptr e.Tast.ty) (Tast.Prim (Tast.AddrOf, [ e ]))
+
 (* Every integer index into an array or slice is i32 at milestone 2. *)
 let index_ty = Types.Int Types.I32
 
@@ -405,7 +435,9 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr =
   | Ast.If (c, t, e') -> check_if ctx ?want loc c t e'
   | Ast.While (c, body) ->
     let c = check ctx ~want:Types.Bool c in
-    let body = scoped ctx (fun () -> map_lr (fun b -> check ctx b) body) in
+    let body = in_loop ctx (fun () ->
+      scoped ctx (fun () -> map_lr (fun b -> check ctx b) body))
+    in
     expect loc ~want (mk loc Types.Unit (Tast.While (c, body)))
   | Ast.Return v when ctx.in_frames <> None ->
     ignore v;
@@ -585,7 +617,9 @@ and var ctx loc ~want name =
       (mk loc Types.Alloc (Tast.Prim (Tast.Rt "flan_context_temp", [])))
   | _ ->
     match lookup ctx name with
-    | Some b -> expect loc ~want (mk loc b.bty (Tast.Local b.slot))
+    | Some b ->
+      if Types.is_move_only b.bty then moved ctx loc name b.slot;
+      expect loc ~want (mk loc b.bty (Tast.Local b.slot))
     | None ->
       match Hashtbl.find_opt ctx.env.globals name with
       | Some (ty, _) -> expect loc ~want (mk loc ty (Tast.Global name))
@@ -595,6 +629,42 @@ and var ctx loc ~want name =
             (Printf.sprintf "the function value %s (a name used as a value)" name) 5
         else begin captured ctx loc name; fail loc "unknown name %s" name end
 
+(* Reading a move-only local. Every read is a move unless the site said it was
+   a borrow, which is the conservative direction: passing one to a function,
+   binding it, returning it and [free]ing it are all moves and all reach here,
+   and the handful of operations that only look at a container say so. *)
+and moved ctx loc name slot =
+  (match List.assoc_opt slot ctx.dead with
+   | Some where ->
+     fail loc
+       "%s was moved at %s and cannot be used again — a Vec is move-only, so \
+        binding, passing or returning one transfers ownership and the source \
+        binding is dead afterwards (spec-memory.md). That rule is what makes a \
+        double free unrepresentable; (clone %s) if you wanted a second one"
+       name (Loc.to_string where) name
+   | None -> ());
+  if not ctx.borrow then ctx.dead <- (slot, loc) :: ctx.dead
+
+(* The target of an operation that reads a container without consuming it. Only
+   a syntactically simple target is treated as a borrow: in [(len (f v))] the
+   call still moves [v], and setting the flag over the whole subexpression
+   would have hidden that. *)
+and borrowed ctx (a : Ast.expr) f =
+  let simple =
+    match a.Ast.e with
+    | Ast.Var _ | Ast.Field _ -> true
+    | Ast.Call ({ Ast.e = Ast.Var "at"; _ }, _) -> true
+    | _ -> false
+  in
+  if not simple then f ()
+  else begin
+    let saved = ctx.borrow in
+    ctx.borrow <- true;
+    let r = f () in
+    ctx.borrow <- saved;
+    r
+  end
+
 and block ctx ?want loc body =
   match body with
   | [] -> expect loc ~want (unit_at loc)
@@ -638,7 +708,7 @@ and check_handler_bind ctx ?want loc clauses body =
             the enclosing one. *)
          let hctx =
            { env = ctx.env; ret = Types.Unit; slots = 0; slot_tys = []; slot_names = [];
-             scope = []; defers = []; outer = ctx.scope; in_handler = true; in_frames = None; in_defer = false; owner = "<none>" }
+             scope = []; defers = []; outer = ctx.scope; in_handler = true; in_frames = None; in_defer = false; dead = []; borrow = false; owner = "<none>" }
          in
          (* The condition crosses as a pointer, because the handler runs while
             the signalling frame is still alive and there is nothing to copy.
@@ -761,12 +831,31 @@ and check_let ctx ?want loc bs body =
    and the bound to a hidden slot — [n] is evaluated once, before the loop, so
    a body that changes it cannot change the trip count — then step [i] at the
    end of the body. [i] is not assignable, so the step below is the only writer. *)
+(* A loop body that moves a binding declared outside the loop is refused, and
+   this is the one place the dead set cannot answer on its own: the second
+   iteration would use what the first moved, and a set that is merged once at
+   the end of the body sees one move, not two. So it is a rule rather than an
+   inference, stated as one. *)
+and in_loop ctx f =
+  let outer_slots = List.map (fun (_, b) -> b.slot) ctx.scope in
+  let before = ctx.dead in
+  let r = f () in
+  List.iter
+    (fun (slot, where) ->
+       if (not (List.mem_assoc slot before)) && List.mem slot outer_slots then
+         fail where
+           "this moves a value that was bound outside the loop, so the next \
+            iteration would use what this one gave away. Move it out of the \
+            loop, or bind a fresh value inside it")
+    ctx.dead;
+  r
+
 and check_dotimes ctx ~want loc name count body =
   let count = check ctx ~want:index_ty count in
   scoped ctx (fun () ->
     let i = bind ctx name index_ty ~assignable:false in
     let limit = fresh_slot ctx index_ty in
-    let body = map_lr (fun b -> check ctx b) body in
+    let body = in_loop ctx (fun () -> map_lr (fun b -> check ctx b) body) in
     let iv = mk loc index_ty (Tast.Local i) in
     let one = mk loc index_ty (Tast.Int (1L, Types.I32)) in
     let cond =
@@ -792,7 +881,15 @@ and check_if ctx ?want loc c t e =
     let t = scoped ctx (fun () -> check ctx t) in
     expect loc ~want (mk loc Types.Unit (Tast.If (c, t, unit_at loc)))
   | Some e ->
+    (* Both arms start from the same dead set and the union survives: moving in
+       one arm only still kills the binding afterwards, and moving in both —
+       which is legal and common — is not reported twice. A flat set would have
+       refused [(if c (free v) (free v))] and allowed the use after a one-armed
+       move, which are the two ways to be wrong here. *)
+    let before = ctx.dead in
     let t = scoped ctx (fun () -> check ctx ?want t) in
+    let after_then = ctx.dead in
+    ctx.dead <- before;
     (* With no expectation the then-branch supplies one for the else-branch,
        unless it diverges, in which case the else-branch decides. *)
     let ewant =
@@ -801,6 +898,9 @@ and check_if ctx ?want loc c t e =
       | None -> if t.Tast.ty = Types.Never then None else Some t.Tast.ty
     in
     let e = scoped ctx (fun () -> check ctx ?want:ewant e) in
+    ctx.dead <-
+      after_then
+      @ List.filter (fun (k, _) -> not (List.mem_assoc k after_then)) ctx.dead;
     let ty =
       if t.Tast.ty = Types.Never then e.Tast.ty
       else if e.Tast.ty = Types.Never then t.Tast.ty
@@ -960,9 +1060,18 @@ and check_place ctx loc (p : Ast.place) : Tast.place * Types.t =
      | None -> fail loc "%s has no field %s" sname name
      | Some i -> Tast.Pfield (target, i), (List.nth s.Tast.fields i).Tast.fty)
   | Ast.Pindex (target, idx) ->
-    let target = check ctx target in
-    let idx, ty = indexed ctx target idx in
-    Tast.Pindex (target, idx), ty
+    let target = borrowed ctx target (fun () -> check ctx target) in
+    (match target.Tast.ty with
+     (* The same bounds and epoch check the value form gets, through the same
+        helper: an element of a Vec is a place because a Vec element is
+        assignable, and a set that skipped the checks would be the asymmetry
+        [nth] was removed for. *)
+     | Types.Vec _ ->
+       let p, ty = vec_at ctx loc target idx in
+       Tast.Pderef p, ty
+     | _ ->
+       let idx, ty = indexed ctx target idx in
+       Tast.Pindex (target, idx), ty)
   | Ast.Pderef target ->
     let target = check ctx target in
     (match target.Tast.ty with
@@ -1097,6 +1206,138 @@ and fold_left_prim ctx ~want loc name p ok what args =
   in
   expect loc ~want acc
 
+(* ── Allocation failure, spec-memory.md ────────────────────────────────
+   No allocating operation returns an error and none can fail silently. When
+   the allocator cannot satisfy a request the operation signals
+
+     (StorageExhausted {:bytes n :align a :allocator id})
+
+   with [error] — whose type is Never — inside a [restart-case] offering
+   [retry]. That is one rule over every allocating operation, which is what
+   keeps [push] and [reserve] at Unit, [clone] at the container, and no
+   signature anywhere growing a Result. Odin's [append] returns an ignorable
+   Allocator_Error and its type-erased path returns the old length on a failed
+   reserve; an append that appends nothing and says nothing is the outcome this
+   rule exists to make impossible.
+
+   It is *compiler-emitted at the point of failure*, which spec-memory.md names
+   as the exception to plan.org's "restarts go at the resync point, once": a
+   restart established at a parser's top-level loop cannot re-attempt an
+   allocation, and only the allocation site can.
+
+   The shape is built out of nodes that already exist — a while, a restart-case
+   and an error — so the backend learns nothing new about allocation:
+
+     (let [ok false]
+       (while (not ok)
+         (restart-case
+           (do (set ok ATTEMPT)
+               (if (not ok) (error (StorageExhausted {...}))))
+           (retry []))))
+
+   A handler that frees something, releases a scratch region or grows the arena
+   and then invokes [retry] lands in the clause, the clause falls through, and
+   the while re-tests and re-attempts the *same* request. With nothing handling
+   it, [error] stops the program on the frame that erred, as §2 says.
+
+   [attempt] must be a call that can be repeated: every argument to it is bound
+   to a slot before the loop, so a retry does not re-evaluate the element
+   expression a push was given. *)
+and alloc_guard ctx loc (attempt : Tast.expr) =
+  let ok = fresh_slot ctx Types.Bool in
+  let okv = mk loc Types.Bool (Tast.Local ok) in
+  let notok () = mk loc Types.Bool (Tast.Prim (Tast.Not, [ okv ])) in
+  let i8 n = mk loc (Types.Int Types.I8) (Tast.Int (n, Types.I8)) in
+  (* The runtime answers 1 or 0 and never reports failure any other way. *)
+  let attempt = mk loc Types.Bool (Tast.Prim (Tast.Ne, [ attempt; i8 0L ])) in
+  (* A value struct on the signalling frame's stack, with fixed numeric fields
+     and no rendered message: formatting would allocate, and this is the one
+     path that must not. Rendering happens in the handler or the break loop,
+     where a working allocator is known. *)
+  let cond =
+    mk loc (Types.Named "StorageExhausted")
+      (Tast.Make
+         ("StorageExhausted",
+          [ rt loc (Types.Int Types.I64) "flan_alloc_fail_bytes" [];
+            rt loc (Types.Int Types.I64) "flan_alloc_fail_align" [];
+            rt loc (Types.Int Types.I64) "flan_alloc_fail_id" [] ]))
+  in
+  let signal =
+    mk loc Types.Never
+      (Tast.Signal (Tast.Serror, type_id "StorageExhausted", cond))
+  in
+  let attempt_then_signal =
+    mk loc Types.Unit
+      (Tast.Do
+         [ mk loc Types.Unit (Tast.Set (Tast.Plocal ok, attempt));
+           mk loc Types.Unit (Tast.If (notok (), signal, unit_at loc)) ])
+  in
+  let clause =
+    { Tast.rname_id = type_id "retry"; rname = "retry"; rbody = [ unit_at loc ] }
+  in
+  let body =
+    mk loc Types.Unit (Tast.RestartCase ([ clause ], attempt_then_signal))
+  in
+  mk loc Types.Unit
+    (Tast.Let ([ (ok, mk loc Types.Bool (Tast.Bool false)) ],
+               [ mk loc Types.Unit (Tast.While (notok (), [ body ])) ]))
+
+(* The element type for [vec-new]: a leading bare symbol naming a type, or the
+   expectation at the site. A bare symbol shadowed by a local or a global is
+   that binding — an allocator, in practice — and not a type. *)
+and vec_new_elem ctx ~want loc args =
+  let named =
+    match args with
+    | { Ast.e = Ast.Var n; _ } :: rest
+      when lookup ctx n = None
+        && (not (Hashtbl.mem ctx.env.globals n))
+        && (List.mem n Types.primitive_names
+            || Hashtbl.mem ctx.env.structs n
+            || Hashtbl.mem ctx.env.enums n
+            || Hashtbl.mem ctx.env.aliases n) ->
+      Some (resolve_name ctx.env ~seen:[] loc n, rest)
+    | _ -> None
+  in
+  match named with
+  | Some (t, rest) -> t, rest
+  | None ->
+    (match want with
+     | Some (Types.Vec t) -> t, args
+     | _ ->
+       fail loc
+         "nothing here says what (vec-new) is a Vec of — write the element \
+          type, as (vec-new i32), or give the binding a type")
+
+(* The element type, or the reason this is not a Vec. *)
+and vec_elem loc what (t : Types.t) =
+  match t with
+  | Types.Vec e -> e
+  | other -> fail loc "%s takes a (Vec T), found %s" what (Types.to_string other)
+
+(* The allocator an operation uses: the one named at the site, or the current
+   implicit one. spec-memory.md: an operation never falls back to a hidden
+   global allocator, and an explicit allocator can override the context. *)
+and allocator_arg ctx loc = function
+  | [] -> rt loc Types.Alloc "flan_context_allocator" []
+  | [ a ] -> check ctx ~want:Types.Alloc a
+  | _ -> fail loc "at most one allocator may be named here"
+
+(* The address of an element, bounds-checked, with the allocator's epoch
+   checked first. Both the value form [(at v i)] and the place form
+   [(set (at v i) x)] come through here, so they cannot drift apart — which is
+   the asymmetry [nth] was removed for. *)
+and vec_at ctx loc (target : Tast.expr) (idx : Ast.expr list) =
+  let elem = vec_elem loc "at" target.Tast.ty in
+  match idx with
+  | [ i ] ->
+    let i = index_expr ctx i in
+    rt loc (Types.Ptr elem) "flan_vec_at"
+      [ target; i; size_of loc elem; here loc ], elem
+  | _ ->
+    fail loc
+      "a Vec takes exactly one index — (at v i) — and its element is indexed \
+       separately"
+
 and named_call ctx ~want loc name args =
   let prim p ty args = expect loc ~want (mk loc ty (Tast.Prim (p, args))) in
   match name with
@@ -1335,6 +1576,36 @@ and named_call ctx ~want loc name args =
     expect loc ~want
       (mk loc (Types.Int Types.I64)
          (Tast.Prim (Tast.Rt "flan_alloc_epoch", [ a ])))
+  (* The allocator's identity — its address — which is what the condition's
+     :allocator field carries, so a handler holding several regions can tell
+     which one ran out. *)
+  | "alloc-id" ->
+    arity loc name 1 args;
+    let a = check ctx ~want:Types.Alloc (List.hd args) in
+    expect loc ~want
+      (mk loc (Types.Int Types.I64) (Tast.Prim (Tast.Rt "flan_alloc_id", [ a ])))
+  (* A ceiling on live bytes, 0 for none. spec-memory.md's retry restart is
+     answerable only by a handler that can make the *same* request succeed, and
+     for a fixed backing store the handler that works is the one that grows it:
+     releasing the region a container lives in invalidates the container, which
+     is what the epoch check catches. So the spec's "grows the arena and then
+     invokes retry" needs a ceiling to raise, and this is it. It is also how a
+     program exhausts an allocator on purpose. *)
+  | "alloc-budget" ->
+    arity loc name 1 args;
+    let a = check ctx ~want:Types.Alloc (List.hd args) in
+    expect loc ~want
+      (mk loc (Types.Int Types.I64)
+         (Tast.Prim (Tast.Rt "flan_alloc_budget", [ a ])))
+  | "set-alloc-budget" ->
+    arity loc name 2 args;
+    (match args with
+     | [ a; n ] ->
+       let a = check ctx ~want:Types.Alloc a in
+       let n = check ctx ~want:(Types.Int Types.I64) n in
+       expect loc ~want
+         (mk loc Types.Unit (Tast.Prim (Tast.Rt "flan_alloc_set_budget", [ a; n ])))
+     | _ -> assert false)
   (* "Did you forget to free" is an allocator-tier question and this is the
      tier answering it — spec-memory.md, "Leaking is defined behaviour". *)
   | "alloc-live-blocks" ->
@@ -1369,21 +1640,171 @@ and named_call ctx ~want loc name args =
        in
        expect loc ~want (mk loc ty (Tast.WithAlloc (a, body))))
 
+  (* ── (Vec T), spec-memory.md ───────────────────────────────────── *)
+  (* Every one of these is a named call over a type-erased runtime, with
+     size_of and align_of produced here because here is where the concrete
+     element type is known. No generics are involved and none are needed. *)
+  (* (vec-new), (vec-new T), (vec-new a), (vec-new T a).
+     [let] has no type annotation — parse.ml settles that a triple binding is
+     ambiguous and types are inferred — so a local Vec has nowhere to say what
+     it holds, and the element type is written at the call instead. This is not
+     the explicit instantiation syntax the generics section rules out: nothing
+     here is generic, and the name is resolved as an ordinary type, not bound
+     to a type variable. Where the context does say — a defvar's type, a
+     function's return type, an argument — it is not needed and may be left
+     out. *)
+  | "vec-new" ->
+    let elem, args = vec_new_elem ctx ~want loc args in
+    let a = allocator_arg ctx loc args in
+    let v = fresh_slot ctx (Types.Vec elem) in
+    let attempt =
+      rt loc (Types.Int Types.I8) "flan_vec_init"
+        [ mk loc (Types.Vec elem) (Tast.Local v); a; i64_at loc 0L;
+          size_of loc elem; align_of loc elem ]
+    in
+    expect loc ~want
+      (mk loc (Types.Vec elem)
+         (Tast.Let ([ (v, mk loc (Types.Vec elem) (Tast.Zero (Types.Vec elem))) ],
+                    [ alloc_guard ctx loc attempt;
+                      mk loc (Types.Vec elem) (Tast.Local v) ])))
+  (* Unit, not a Result and not an ignorable error code: see [alloc_guard]. *)
+  | "push" ->
+    arity loc name 2 args;
+    (match args with
+     | [ target; x ] ->
+       let target = borrowed ctx target (fun () -> check ctx target) in
+       let elem = vec_elem loc "push" target.Tast.ty in
+       let x = check ctx ~want:elem x in
+       (* The element is bound before the loop so that a [retry] re-attempts
+          the allocation and not the expression that produced the value. *)
+       let e = fresh_slot ctx elem in
+       let attempt =
+         rt loc (Types.Int Types.I8) "flan_vec_push"
+           [ target; addr_of loc (mk loc elem (Tast.Local e));
+             size_of loc elem; align_of loc elem; here loc ]
+       in
+       expect loc ~want
+         (mk loc Types.Unit
+            (Tast.Let ([ (e, x) ], [ alloc_guard ctx loc attempt ])))
+     | _ -> assert false)
+  | "reserve" ->
+    arity loc name 2 args;
+    (match args with
+     | [ target; n ] ->
+       let target = borrowed ctx target (fun () -> check ctx target) in
+       let elem = vec_elem loc "reserve" target.Tast.ty in
+       let n = check ctx ~want:index_ty n in
+       let n64 =
+         mk loc (Types.Int Types.I64) (Tast.Prim (Tast.Cast (Types.Int Types.I64), [ n ]))
+       in
+       let attempt =
+         rt loc (Types.Int Types.I8) "flan_vec_reserve"
+           [ target; n64; size_of loc elem; align_of loc elem; here loc ]
+       in
+       expect loc ~want (alloc_guard ctx loc attempt)
+     | _ -> assert false)
+  (* (as-slice v) and (as-slice v lo hi) — spec-memory.md, "Borrowing". The
+     result is a non-owning view: copying it copies ptr+len and never the
+     elements, and it carries no allocator, so freeing through one is not
+     expressible. A push, a put or a reserve may invalidate it; that is the
+     explicit Zig/Odin contract the spec chose over a borrow checker. *)
+  | "as-slice" ->
+    (match args with
+     | target :: rest when List.length rest = 0 || List.length rest = 2 ->
+       let target = borrowed ctx target (fun () -> check ctx target) in
+       let elem = vec_elem loc "as-slice" target.Tast.ty in
+       let lo, hi =
+         match rest with
+         | [] ->
+           mk loc index_ty (Tast.Int (0L, Types.I32)),
+           (* -1 is "to the end": (as-slice v) has no static length to pass. *)
+           mk loc index_ty (Tast.Int (-1L, Types.I32))
+         | [ lo; hi ] -> index_expr ctx lo, index_expr ctx hi
+         | _ -> assert false
+       in
+       let out = fresh_slot ctx (Types.Slice elem) in
+       let fill =
+         rt loc Types.Unit "flan_vec_as_slice"
+           [ target; addr_of loc (mk loc (Types.Slice elem) (Tast.Local out));
+             lo; hi; size_of loc elem; here loc ]
+       in
+       expect loc ~want
+         (mk loc (Types.Slice elem)
+            (Tast.Let ([ (out, mk loc (Types.Slice elem)
+                                 (Tast.Zero (Types.Slice elem))) ],
+                       [ fill; mk loc (Types.Slice elem) (Tast.Local out) ])))
+     | _ -> fail loc "as-slice is (as-slice v) or (as-slice v lo hi)")
+  (* spec-memory.md's first release point. It consumes its argument exactly as
+     any other move does — the source binding is dead afterwards and using it
+     is a compile error — which is the rule that already makes a double free
+     unrepresentable, so [free] needs no analysis of its own. *)
+  | "free" ->
+    arity loc name 1 args;
+    let target = check ctx (List.hd args) in
+    (match target.Tast.ty with
+     | Types.Vec elem ->
+       expect loc ~want
+         (rt loc Types.Unit "flan_vec_free"
+            [ target; size_of loc elem; align_of loc elem; here loc ])
+     | other ->
+       (* A field is never freed on its own: it would leave its owner partly
+          dead with no way to say so. *)
+       fail loc
+         "free takes a move-only value — a Vec, or a struct that owns one — \
+          found %s. A resource type with a drop hook is step 5 and does not \
+          exist yet"
+         (Types.to_string other))
+  (* (clone v) uses the current allocator, (clone v a) names one. A deep,
+     independent copy: spec-memory.md's "copying is always explicit". *)
+  | "clone" ->
+    (match args with
+     | target :: rest when List.length rest <= 1 ->
+       let target = borrowed ctx target (fun () -> check ctx target) in
+       let elem = vec_elem loc "clone" target.Tast.ty in
+       let a = allocator_arg ctx loc rest in
+       let d = fresh_slot ctx (Types.Vec elem) in
+       let attempt =
+         rt loc (Types.Int Types.I8) "flan_vec_clone"
+           [ mk loc (Types.Vec elem) (Tast.Local d); target; a;
+             size_of loc elem; align_of loc elem; here loc ]
+       in
+       expect loc ~want
+         (mk loc (Types.Vec elem)
+            (Tast.Let ([ (d, mk loc (Types.Vec elem) (Tast.Zero (Types.Vec elem))) ],
+                       [ alloc_guard ctx loc attempt;
+                         mk loc (Types.Vec elem) (Tast.Local d) ])))
+     | _ -> fail loc "clone is (clone v) or (clone v allocator)")
+
   (* ── containers ────────────────────────────────────────────────── *)
+  (* [at] and [len] were already the names for a fixed array and a slice, so a
+     Vec extends them rather than adding a parallel pair — which is the
+     asymmetry [nth] was removed for. A Vec's length is i32 like every other
+     length here (index_ty): widening indices is one change across all of them
+     and not a Vec question. *)
   | "len" ->
     arity loc name 1 args;
-    let a = check ctx (List.hd args) in
+    let target = List.hd args in
+    let a = borrowed ctx target (fun () -> check ctx target) in
     (match a.Tast.ty with
-     | Types.Array _ | Types.Slice _ | Types.String -> ()
-     | other -> fail loc "len takes an array, a slice or a string, found %s"
-                  (Types.to_string other));
-    prim Tast.Len index_ty [ a ]
+     | Types.Array _ | Types.Slice _ | Types.String ->
+       prim Tast.Len index_ty [ a ]
+     | Types.Vec _ ->
+       let n = rt loc (Types.Int Types.I64) "flan_vec_len" [ a; here loc ] in
+       expect loc ~want (mk loc index_ty (Tast.Prim (Tast.Cast index_ty, [ n ])))
+     | other ->
+       fail loc "len takes an array, a slice, a string or a Vec, found %s"
+         (Types.to_string other))
   | "at" ->
     (match args with
      | target :: idx when idx <> [] ->
-       let target = check ctx target in
-       let idx, ty = indexed ctx target idx in
-       prim Tast.At ty (target :: idx)
+       let target = borrowed ctx target (fun () -> check ctx target) in
+       (match target.Tast.ty with
+        | Types.Vec _ ->
+          let p, elem = vec_at ctx loc target idx in
+          expect loc ~want (mk loc elem (Tast.Deref p))
+        | _ ->
+          let idx, ty = indexed ctx target idx in
+          prim Tast.At ty (target :: idx))
      | _ -> fail loc "%s is (%s collection index ...)" name name)
   | "slice" ->
     arity loc name 3 args;
@@ -1858,7 +2279,7 @@ let collect env (decls : Ast.decl list) =
      run without swallowing it. *)
   let infer (_, v) =
     (check { env; ret = Types.Unit; slots = 0; slot_tys = []; slot_names = []; scope = []; defers = [];
-      outer = []; in_handler = false; in_frames = None; in_defer = false; owner = "<none>" } v).Tast.ty
+      outer = []; in_handler = false; in_frames = None; in_defer = false; dead = []; borrow = false; owner = "<none>" } v).Tast.ty
   in
   let pending = ref (List.rev !untyped) in
   let rec settle () =
@@ -1911,7 +2332,7 @@ let check_finite env =
 let check_fn env (fn : Ast.fn) : Tast.fn =
   let params, ret = Hashtbl.find env.fns fn.Ast.name in
   let ctx = { env; ret; slots = 0; slot_tys = []; slot_names = []; scope = []; defers = [];
-                outer = []; in_handler = false; in_frames = None; in_defer = false;
+                outer = []; in_handler = false; in_frames = None; in_defer = false; dead = []; borrow = false;
                 owner = fn.Ast.name } in
   List.iter2
     (fun (p : Ast.field) ty ->
@@ -1987,7 +2408,7 @@ let check_fn env (fn : Ast.fn) : Tast.fn =
 
 let check_global env (d : Ast.decl) : Tast.global option =
   let ctx () = { env; ret = Types.Unit; slots = 0; slot_tys = []; slot_names = []; scope = []; defers = [];
-      outer = []; in_handler = false; in_frames = None; in_defer = false; owner = "<none>" } in
+      outer = []; in_handler = false; in_frames = None; in_defer = false; dead = []; borrow = false; owner = "<none>" } in
   match d.Ast.d with
   | Ast.Defvar (n, _, init) ->
     let ty, _ = Hashtbl.find env.globals n in
@@ -2097,7 +2518,7 @@ let expression env (e : Ast.expr) :
   Tast.expr * Types.t array * string option array =
   let ctx =
     { env; ret = Types.Unit; slots = 0; slot_tys = []; slot_names = []; scope = []; defers = [];
-      outer = []; in_handler = false; in_frames = None; in_defer = false; owner = "<none>" }
+      outer = []; in_handler = false; in_frames = None; in_defer = false; dead = []; borrow = false; owner = "<none>" }
   in
   let t = check ctx e in
   (t, Array.of_list (List.rev ctx.slot_tys),
diff --git a/lib/emit.ml b/lib/emit.ml
index 829869f..8dcc84d 100644
--- a/lib/emit.ml
+++ b/lib/emit.ml
@@ -96,6 +96,12 @@ let rec ll (t : Types.t) =
   (* An [Allocator] is a pointer to the runtime's [flan_allocator] and never a
      copy of one: see Types. Opaque here in the same sense [ptr] is. *)
   | Types.Alloc -> "ptr"
+  (* ptr + len + cap + allocator, and two more words the runtime owns: see
+     flan_rt.c's (Vec T) header for why they are in every build. Nothing in
+     this file reads a field of one — every operation is a runtime call taking
+     the Vec's address — so the shape is here only so that a slot, a struct
+     field and a copy in the IR are the right number of bytes. *)
+  | Types.Vec _ -> "%vec"
   | Types.Option e -> Printf.sprintf "{ i8, %s }" (ll e)
   | Types.Map _ | Types.Fn _ | Types.Var _ ->
     (* The checker rejects each of these by name — nothing reaches here. *)
@@ -233,6 +239,7 @@ let rec lay m (t : Types.t) : int * int =
   | Types.Enum _ -> 4, 4
   | Types.Ptr _ -> 8, 8
   | Types.Alloc -> 8, 8
+  | Types.Vec _ -> 48, 8
   (* [n x T] adds no padding of its own: T's size already carries its tail. *)
   | Types.Array (n, e) -> let s, a = lay m e in Int64.to_int n * s, a
   | Types.Option e -> let s, a, _ = lay_fields m [ Types.Int Types.I8; e ] in s, a
@@ -354,6 +361,14 @@ let rec dty m d (t : Types.t) : int =
       | Types.Alloc ->
         dnode d
           "!DIDerivedType(tag: DW_TAG_pointer_type, name: \"Allocator\", baseType: null, size: 64)"
+      (* Shown as what it is. The two dev words are in the layout and so they
+         are here too: a debugger that showed four fields of a six-field struct
+         would put the reader's offsets out by two. *)
+      | Types.Vec e ->
+        composite (Types.to_string t)
+          [ ("ptr", Types.Ptr e); ("len", Types.Int Types.I64);
+            ("cap", Types.Int Types.I64); ("allocator", Types.Alloc);
+            ("gen", Types.Int Types.I64); ("epoch", Types.Int Types.I64) ]
       | Types.Map _ | Types.Fn _ | Types.Var _ ->
         failwith ("no debug type for " ^ Types.to_string t)
     in
@@ -1310,6 +1325,10 @@ and prim f (e : Tast.expr) (p : Tast.prim) (args : Tast.expr list) =
                 let p, n = explode f a in
                 [ "ptr " ^ p; "i64 " ^ n ]
               | Types.Unit | Types.Never -> []
+              (* A Vec is move-only and never copied, so it crosses to the
+                 runtime as its address — which is also what lets an operation
+                 mutate the caller's Vec in place. *)
+              | Types.Vec _ -> [ "ptr " ^ addr f a ]
               | t -> [ ll t ^ " " ^ value f a ])
            args)
     in
@@ -1322,6 +1341,9 @@ and prim f (e : Tast.expr) (p : Tast.prim) (args : Tast.expr list) =
       ins f "%s = call %s @%s(%s)" t (ll e.Tast.ty) sym args';
       t
     end
+  | Tast.SizeOf t, [] -> Printf.sprintf "%d" (fst (lay f.md t))
+  | Tast.AlignOf t, [] -> Printf.sprintf "%d" (snd (lay f.md t))
+  | Tast.AddrOf, [ x ] -> addr f x
   | Tast.Cast target, [ x ] -> cast f x target
   | _ -> failwith "malformed primitive"
 
@@ -1613,6 +1635,9 @@ let header = {|; Generated by flan. The layout is C's: no object headers anywher
 ; so a Flan struct is exactly its C struct and nothing marshals.
 
 %slice = type { ptr, i64 }
+; (Vec T), spec-memory.md. The element type is nowhere in it: the runtime is
+; type-erased and every operation is handed size and align at its call site.
+%vec = type { ptr, i64, i64, ptr, i64, i64 }
 ; A handler frame: the one it displaced, the condition type it matches, and
 ; the lifted function that runs. Allocated on the establishing frame's stack.
 %handler = type { ptr, i32, ptr }
@@ -1655,6 +1680,20 @@ declare i8 @flan_alloc_can_free(ptr)
 declare i8 @flan_alloc_can_free_all(ptr)
 declare i64 @flan_alloc_epoch(ptr)
 declare i64 @flan_alloc_live_blocks(ptr)
+declare i64 @flan_alloc_id(ptr)
+declare i64 @flan_alloc_fail_bytes()
+declare i64 @flan_alloc_fail_align()
+declare i64 @flan_alloc_fail_id()
+declare i64 @flan_alloc_budget(ptr)
+declare void @flan_alloc_set_budget(ptr, i64)
+declare i8 @flan_vec_init(ptr, ptr, i64, i64, i64)
+declare i8 @flan_vec_reserve(ptr, i64, i64, i64, ptr, i64)
+declare i8 @flan_vec_push(ptr, ptr, i64, i64, ptr, i64)
+declare i8 @flan_vec_clone(ptr, ptr, ptr, i64, i64, ptr, i64)
+declare i64 @flan_vec_len(ptr, ptr, i64)
+declare ptr @flan_vec_at(ptr, i32, i64, ptr, i64)
+declare void @flan_vec_as_slice(ptr, ptr, i32, i32, i64, ptr, i64)
+declare void @flan_vec_free(ptr, i64, i64, ptr, i64)
 |}
 
 (* C's main, adapting to whichever of the four shapes Flan's main has: argv and
diff --git a/lib/prelude.ml b/lib/prelude.ml
index fe39163..6aed562 100644
--- a/lib/prelude.ml
+++ b/lib/prelude.ml
@@ -31,6 +31,19 @@
     it actually holds. *)
 
 let source = {flan|
+;; The condition every allocating operation signals when the allocator cannot
+;; satisfy a request — spec-memory.md, "Allocation failure". It is here rather
+;; than built by the checker because it is an ordinary value struct and the
+;; checker already knows how to build one of those; nothing about it is
+;; special except who signals it.
+;;
+;; Fixed numeric fields and no rendered message, because formatting would
+;; allocate and this is the one path that must not. :allocator is the
+;; allocator's address, which is its identity — the same thing the epoch hangs
+;; off — so a handler can tell which region ran out. Rendering happens in the
+;; handler or the break loop, where a working allocator is known.
+(defstruct StorageExhausted [bytes i64 align i64 allocator i64])
+
 ;; A seeded PRNG in Flan rather than libc's, because a grid hash is only a
 ;; regression test if the sequence is byte-identical on native and wasm32
 ;; (plan.org, RNG is ours). PCG-XSH-RR 32: one u64 LCG step per draw, folded
diff --git a/lib/render.ml b/lib/render.ml
index 67793d0..ec3fe2a 100644
--- a/lib/render.ml
+++ b/lib/render.ml
@@ -114,6 +114,10 @@ let rec render c depth (e : Tast.expr) : Tast.expr list =
        runtime's, its address is not stable across runs, and printing either
        would make an acceptance test's output depend on the heap. *)
     | Types.Alloc -> [ lit "<allocator>" ]
+    (* Printing a Vec structurally would be a walk over storage this function
+       does not own, and the walk is what [as-slice] is for: (print (as-slice
+       v)) prints the elements and says at the call site that it borrowed. *)
+    | Types.Vec _ -> [ lit "<vec>" ]
     | Types.Option t ->
       let tag = { Tast.e = Tast.Field (e, 0); ty = Types.Int Types.I8; loc } in
       let some = { Tast.e = Tast.Field (e, 1); ty = t; loc } in
diff --git a/lib/tast.ml b/lib/tast.ml
index eec1597..461fc08 100644
--- a/lib/tast.ml
+++ b/lib/tast.ml
@@ -45,6 +45,18 @@ type prim =
      same rule as every other shim here. No transfer guard follows one: a
      transfer cannot cross a C frame. *)
   | Rt of string
+  (* spec-memory.md, "Alignment": a property of the type, computed at the call
+     site, passed as a parameter to the type-erased allocator — all three, and
+     they are not alternatives. The checker builds these at the site where the
+     concrete element type is known and the backend fills in the number from
+     the same layout calculator DWARF uses. *)
+  | SizeOf of Types.t
+  | AlignOf of Types.t
+  (* The address of any expression, not only of a place: the element a [push]
+     copies may be a computed value, and the runtime takes it by pointer
+     because it is type-erased. The backend already spills a non-place to a
+     temporary for exactly this. *)
+  | AddrOf
   | Cast of Types.t
 
 type expr = { e : expr_kind; ty : Types.t; loc : Loc.t }
diff --git a/lib/types.ml b/lib/types.ml
index 80fa637..293c476 100644
--- a/lib/types.ml
+++ b/lib/types.ml
@@ -39,6 +39,11 @@ type t =
      the capability set and the epoch have to be shared by every container
      made from it, and a copy would give each its own. *)
   | Alloc
+  (* [(Vec T)]: ptr + len + cap + allocator, owning and move-only. One
+     type-erased runtime over (size, align) stands behind every instantiation,
+     so this is a container without generics — the concrete type is known only
+     at the call site, which is exactly where the two numbers are produced. *)
+  | Vec    of t
   | Option of t                       (* (Option T) *)
   | Fn     of t list * t              (* (Fn [T ...] R) *)
   | Var    of string                  (* a type variable — milestone 5 *)
@@ -85,6 +90,7 @@ let rec equal a b =
   | Map (k, v), Map (k', v') -> equal k k' && equal v v'
   | Ptr x, Ptr y -> equal x y
   | Alloc, Alloc -> true
+  | Vec x, Vec y -> equal x y
   | Option x, Option y -> equal x y
   | Fn (ps, r), Fn (ps', r') ->
     List.length ps = List.length ps'
@@ -106,6 +112,7 @@ let rec to_string = function
   | Map (k, v) -> Printf.sprintf "{%s %s}" (to_string k) (to_string v)
   | Ptr t -> "(Ptr " ^ to_string t ^ ")"
   | Alloc -> "Allocator"
+  | Vec t -> "(Vec " ^ to_string t ^ ")"
   | Option t -> "(Option " ^ to_string t ^ ")"
   | Fn (ps, r) ->
     Printf.sprintf "(Fn [%s] %s)"
@@ -114,6 +121,17 @@ let rec to_string = function
 
 let is_numeric = function Int _ | Float _ -> true | _ -> false
 
+(* Move-only: binding, passing or returning one transfers ownership and the
+   source binding is dead afterwards (spec-memory.md, "The four container
+   types"). That rule is what makes a double free unrepresentable, which is why
+   [free] needs no analysis of its own. A struct that owns one is move-only
+   too; that arrives with [drop], which is the step after this one. *)
+let rec is_move_only = function
+  | Vec _ -> true
+  | Option t -> is_move_only t
+  | Array (_, t) -> is_move_only t
+  | _ -> false
+
 (* Ordering and equality are defined on machine types and on nothing else at
    milestone 2 — strings, structs and slices have no built-in [=], because an
    unconstrained type supports only what every type supports (plan.org, Types). *)
diff --git a/runtime/flan_rt.c b/runtime/flan_rt.c
index d5e5d80..7adc26d 100644
--- a/runtime/flan_rt.c
+++ b/runtime/flan_rt.c
@@ -477,8 +477,22 @@ struct flan_allocator {
    * an allocator-tier question and this is the allocator's answer. */
   int64_t         live_blocks;
   int64_t         live_bytes;
+  /* A cap on live bytes, or 0 for none. It is here because
+   * spec-memory.md's retry restart is only answerable by a handler that can
+   * make the *same* request succeed, and for a fixed backing buffer the only
+   * such handler is one that raises the ceiling: releasing the region a
+   * container lives in invalidates the container, which is what the epoch
+   * check exists to catch. So "grow the arena and then invoke retry", which
+   * the spec names as the handler that works, needs a ceiling to raise. It
+   * doubles as the knob a test exhausts an allocator with on purpose. */
+  int64_t         budget;
 };
 
+/* Would this request put the allocator over its budget? */
+static int flan_over_budget(flan_allocator *a, int64_t size) {
+  return a->budget > 0 && a->live_bytes + size > a->budget;
+}
+
 /* -- The heap allocator: malloc, realloc, free. ---------------------- */
 
 static void *flan_heap_proc(flan_allocator *a, int32_t mode, void *p,
@@ -488,6 +502,7 @@ static void *flan_heap_proc(flan_allocator *a, int32_t mode, void *p,
     void *q = NULL;
     size_t al, sz;
     if (size <= 0) return NULL;
+    if (flan_over_budget(a, size)) return NULL;
     al = (size_t)(align < (int64_t)sizeof(void *) ? (int64_t)sizeof(void *) : align);
     sz = (size_t)size;
     /* aligned_alloc requires a size that is a multiple of the alignment. */
@@ -500,7 +515,9 @@ static void *flan_heap_proc(flan_allocator *a, int32_t mode, void *p,
     /* aligned_alloc has no realloc, so growth is a new block and a copy. The
      * caller passes old_size for exactly this reason, and it is the one
      * number a wrong answer here would read off the end of. */
-    void *q = flan_heap_proc(a, FLAN_ALLOC_ALLOC, NULL, 0, size, align);
+    void *q;
+    if (flan_over_budget(a, size - old_size)) return NULL;
+    q = flan_heap_proc(a, FLAN_ALLOC_ALLOC, NULL, 0, size, align);
     if (!q) return NULL;
     if (p && old_size > 0)
       memcpy(q, p, (size_t)(old_size < size ? old_size : size));
@@ -519,7 +536,7 @@ static void *flan_heap_proc(flan_allocator *a, int32_t mode, void *p,
 static flan_allocator flan_heap = {
   flan_heap_proc, NULL,
   FLAN_CAN_ALLOC | FLAN_CAN_RESIZE | FLAN_CAN_FREE,
-  0, 0, 0
+  0, 0, 0, 0
 };
 
 /* -- The arena: one fixed backing buffer and a bump offset. ----------
@@ -552,6 +569,7 @@ static void *flan_arena_proc(flan_allocator *a, int32_t mode, void *p,
   case FLAN_ALLOC_ALLOC: {
     int64_t start, end;
     if (size <= 0) return NULL;
+    if (flan_over_budget(a, size)) return NULL;
     if (align < 1) align = 1;
     start = flan_align_up(ar->offset, align);
     end = start + size;
@@ -680,6 +698,12 @@ int64_t flan_alloc_live_blocks(flan_allocator *a) {
   return a ? a->live_blocks : 0;
 }
 
+int64_t flan_alloc_budget(flan_allocator *a) { return a ? a->budget : 0; }
+
+void flan_alloc_set_budget(flan_allocator *a, int64_t n) {
+  if (a) a->budget = n < 0 ? 0 : n;
+}
+
 _Noreturn void flan_free_all_fail(const uint8_t *loc, int64_t loclen);
 _Noreturn void flan_null_alloc_fail(const uint8_t *loc, int64_t loclen);
 
@@ -714,3 +738,216 @@ _Noreturn void flan_free_all_fail(const uint8_t *loc, int64_t loclen) {
           (int)loclen, (const char *)loc);
   rt_die();
 }
+
+/* ── (Vec T), spec-memory.md ────────────────────────────────────────────
+ *
+ * One type-erased runtime over (size, align), which is Odin's arrangement
+ * (base/runtime/dynamic_array_internal.odin): the monomorphised wrapper is the
+ * only place the concrete type is known, so it is the only place that can
+ * produce the numbers, and it passes them in. There are no generics here and
+ * none are needed.
+ *
+ * Header, and it is six words rather than the spec's four:
+ *
+ *   ptr len cap allocator      the release layout spec-memory.md fixes
+ *   gen                        bumped on every reallocation — the stale-slice
+ *                              word. It has no reader yet; see BUILT.md.
+ *   epoch                      the allocator's epoch when this Vec last
+ *                              touched it. Any operation on a container whose
+ *                              recorded epoch has moved traps.
+ *
+ * The two dev words are present in every build, not only a dev one, and that
+ * is not laziness: a redefinition module is built by llc and ld against a host
+ * that was built separately, and nothing makes the two agree on a struct size.
+ * A layout that changes with a build flag is a layout that can disagree across
+ * that boundary silently. Dropping them in release is deferred and BUILT.md
+ * says what it is blocked on.
+ *
+ * Every entry point returns int8_t 1/0 for "did it fit", and never reports
+ * failure any other way: the condition, the restart and the message are the
+ * compiler's job (see Check's alloc_guard). */
+
+typedef struct flan_vec {
+  void           *ptr;
+  int64_t         len;
+  int64_t         cap;
+  flan_allocator *alloc;
+  int64_t         gen;
+  int64_t         epoch;
+} flan_vec;
+
+/* The request that did not fit, for the condition the compiler builds at the
+ * failing site. A pair of globals rather than out-parameters because the
+ * condition is a value struct on the signalling frame's stack with fixed
+ * numeric fields and no rendered message — spec-memory.md is explicit that
+ * this is the one path that must not allocate, and reading two words is the
+ * cheapest way to carry the numbers out. */
+static int64_t flan_fail_bytes = 0;
+static int64_t flan_fail_align = 0;
+static int64_t flan_fail_id = 0;
+
+int64_t flan_alloc_fail_bytes(void) { return flan_fail_bytes; }
+int64_t flan_alloc_fail_align(void) { return flan_fail_align; }
+int64_t flan_alloc_fail_id(void) { return flan_fail_id; }
+
+/* The allocator's identity, for the condition's :allocator field. The pointer
+ * is the identity — the same thing the epoch hangs off. */
+int64_t flan_alloc_id(flan_allocator *a) { return (int64_t)(intptr_t)a; }
+
+_Noreturn void flan_vec_stale_fail(const uint8_t *loc, int64_t loclen,
+                                   int64_t was, int64_t now) {
+  fflush(stdout);
+  fprintf(stderr,
+          "%.*s: this container's allocator was released — it was made at "
+          "epoch %lld and the allocator is at %lld now\n",
+          (int)loclen, (const char *)loc, (long long)was, (long long)now);
+  rt_die();
+}
+
+_Noreturn void flan_vec_bounds_fail(const uint8_t *loc, int64_t loclen,
+                                    int64_t i, int64_t len) {
+  fflush(stdout);
+  fprintf(stderr, "%.*s: index %lld is out of bounds for length %lld\n",
+          (int)loclen, (const char *)loc, (long long)i, (long long)len);
+  rt_die();
+}
+
+/* spec-memory.md, "Dev builds detect 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. */
+static void flan_vec_check(flan_vec *v, const uint8_t *loc, int64_t loclen) {
+  if (v->alloc) {
+    int64_t now = (int64_t)v->alloc->epoch;
+    if (now != v->epoch) flan_vec_stale_fail(loc, loclen, v->epoch, now);
+  }
+}
+
+/* A zeroed Vec — a struct field nobody assigned, or a (defvar xs (Vec i32)) —
+ * has a null allocator, and the first operation that needs storage adopts the
+ * context allocator. That is Odin's behaviour, and the alternative was to
+ * refuse a Vec-typed struct field outright until step 5. Shipping the null
+ * silently was not an option: it is a null deref on the first push. */
+static flan_allocator *flan_vec_adopt(flan_vec *v) {
+  if (!v->alloc) {
+    v->alloc = flan_context_allocator();
+    v->epoch = (int64_t)v->alloc->epoch;
+  }
+  return v->alloc;
+}
+
+static int8_t flan_vec_grow(flan_vec *v, int64_t want, int64_t size,
+                            int64_t align) {
+  flan_allocator *a = flan_vec_adopt(v);
+  int64_t cap = v->cap;
+  void *p;
+  if (want <= cap) return 1;
+  /* Doubling, from four. Four rather than one because the three reallocations
+   * a growing-from-one Vec does before it holds anything are pure cost, and
+   * doubling because it is what makes n pushes amortised O(n). */
+  if (cap < 4) cap = 4;
+  while (cap < want) {
+    if (cap > (int64_t)1 << 40) { cap = want; break; }
+    cap *= 2;
+  }
+  flan_fail_bytes = cap * size;
+  flan_fail_align = align;
+  flan_fail_id = (int64_t)(intptr_t)a;
+  if (v->ptr)
+    p = a->proc(a, FLAN_ALLOC_RESIZE, v->ptr, v->cap * size, cap * size, align);
+  else
+    p = a->proc(a, FLAN_ALLOC_ALLOC, NULL, 0, cap * size, align);
+  if (!p) return 0;
+  v->ptr = p;
+  v->cap = cap;
+  /* Any slice taken before this points at storage that may have moved. The
+   * word is bumped here and read nowhere yet; see BUILT.md. */
+  v->gen++;
+  return 1;
+}
+
+int8_t flan_vec_init(flan_vec *v, flan_allocator *a, int64_t cap, int64_t size,
+                     int64_t align) {
+  v->ptr = NULL;
+  v->len = 0;
+  v->cap = 0;
+  v->gen = 0;
+  v->alloc = a ? a : flan_context_allocator();
+  v->epoch = (int64_t)v->alloc->epoch;
+  if (cap <= 0) return 1;
+  return flan_vec_grow(v, cap, size, align);
+}
+
+int8_t flan_vec_reserve(flan_vec *v, int64_t n, int64_t size, int64_t align,
+                        const uint8_t *loc, int64_t loclen) {
+  flan_vec_check(v, loc, loclen);
+  if (n <= v->cap) return 1;
+  return flan_vec_grow(v, n, size, align);
+}
+
+int8_t flan_vec_push(flan_vec *v, const void *elem, int64_t size,
+                     int64_t align, const uint8_t *loc, int64_t loclen) {
+  flan_vec_check(v, loc, loclen);
+  if (v->len + 1 > v->cap && !flan_vec_grow(v, v->len + 1, size, align))
+    return 0;
+  memcpy((uint8_t *)v->ptr + v->len * size, elem, (size_t)size);
+  v->len++;
+  return 1;
+}
+
+int64_t flan_vec_len(flan_vec *v, const uint8_t *loc, int64_t loclen) {
+  flan_vec_check(v, loc, loclen);
+  return v->len;
+}
+
+void *flan_vec_at(flan_vec *v, int32_t i, int64_t size, const uint8_t *loc,
+                  int64_t loclen) {
+  flan_vec_check(v, loc, loclen);
+  /* The same unsigned comparison the fixed-array bounds check uses: a negative
+   * index sign-extends to a huge unsigned and is caught by the one test. */
+  if ((uint64_t)(int64_t)i >= (uint64_t)v->len)
+    flan_vec_bounds_fail(loc, loclen, (int64_t)i, v->len);
+  return (uint8_t *)v->ptr + (int64_t)i * size;
+}
+
+/* [hi] of -1 means "to the end": (as-slice v) has no static length to write. */
+void flan_vec_as_slice(flan_vec *v, void *out, int32_t lo, int32_t hi,
+                       int64_t size, const uint8_t *loc, int64_t loclen) {
+  struct { void *p; int64_t n; } s;
+  int64_t l = lo, h = (hi < 0) ? v->len : hi;
+  flan_vec_check(v, loc, loclen);
+  if (l < 0 || h > v->len || l > h) flan_vec_bounds_fail(loc, loclen, l, v->len);
+  s.p = (uint8_t *)v->ptr + l * size;
+  s.n = h - l;
+  memcpy(out, &s, sizeof s);
+}
+
+/* spec-memory.md's first release point. The Vec is left zeroed rather than
+ * dangling — the checker has already made using it afterwards a compile error,
+ * and zeroing costs nothing and makes a bug that slips past the checker a null
+ * deref rather than a use-after-free. An allocator without can-free keeps the
+ * block: releasing it is free-all's job, and pretending otherwise here is the
+ * silent-no-op this file refuses elsewhere. */
+void flan_vec_free(flan_vec *v, int64_t size, int64_t align,
+                   const uint8_t *loc, int64_t loclen) {
+  flan_vec_check(v, loc, loclen);
+  if (v->ptr && v->alloc && (v->alloc->caps & FLAN_CAN_FREE))
+    v->alloc->proc(v->alloc, FLAN_ALLOC_FREE, v->ptr, v->cap * size, 0, align);
+  (void)align;
+  v->ptr = NULL;
+  v->len = 0;
+  v->cap = 0;
+  v->alloc = NULL;
+  v->gen++;
+  v->epoch = 0;
+}
+
+int8_t flan_vec_clone(flan_vec *dst, flan_vec *src, flan_allocator *a,
+                      int64_t size, int64_t align, const uint8_t *loc,
+                      int64_t loclen) {
+  flan_vec_check(src, loc, loclen);
+  if (!flan_vec_init(dst, a, src->len, size, align)) return 0;
+  if (src->len > 0) memcpy(dst->ptr, src->ptr, (size_t)(src->len * size));
+  dst->len = src->len;
+  return 1;
+}
diff --git a/test/programs/exhausted-unhandled.flan b/test/programs/exhausted-unhandled.flan
new file mode 100644
index 0000000..2d86bef
--- /dev/null
+++ b/test/programs/exhausted-unhandled.flan
@@ -0,0 +1,12 @@
+;;;; An exhausted allocator with nothing handling it. §2: `error` is the
+;;;; diverging variant — a handler that returns normally has not answered it,
+;;;; and with no handler at all the program stops on the frame that erred
+;;;; rather than carrying on with a push that appended nothing.
+(defn main [] i32
+  (let [a (arena-new 32)]
+    (let [v (vec-new i32 a)]
+      (println "before")
+      (dotimes [i 64] (push v i))
+      (println "unreachable")
+      (free v)))
+  0)
diff --git a/test/programs/exhausted.flan b/test/programs/exhausted.flan
new file mode 100644
index 0000000..070c196
--- /dev/null
+++ b/test/programs/exhausted.flan
@@ -0,0 +1,92 @@
+;;;; StorageExhausted and retry — spec-memory.md, "Allocation failure".
+;;;;
+;;;; No allocating operation returns an error and none can fail silently. The
+;;;; operation signals StorageExhausted with `error`, whose type is Never,
+;;;; inside a restart-case offering `retry` — so push stays Unit, clone stays
+;;;; the container, and no signature anywhere grows a Result. Odin's append
+;;;; returns an ignorable Allocator_Error; an append that appends nothing and
+;;;; says nothing is the outcome this rule exists to make impossible.
+;;;;
+;;;; This is also the named exception to plan.org's "restarts go at the resync
+;;;; point, once": the restart is established *at the failing allocation*,
+;;;; because a restart at an outer loop cannot re-attempt an allocation and
+;;;; only the allocation site can.
+;;;;
+;;;; The handler that works is the one that raises the ceiling and retries.
+;;;; Releasing the region the container lives in does not work and must not be
+;;;; written: it invalidates the container, which the epoch check then catches
+;;;; — and that case is its own program, stale-region.flan.
+
+;; Globals, because a handler cannot see the locals of the function that
+;; established it: check.ml's `captured` refuses one by name and says to use a
+;; global. That refusal is the accumulation pattern, and it is not built.
+(defvar tight Allocator)
+(defvar failures i64)
+(defvar last-bytes i64)
+(defvar last-align i64)
+(defvar same-allocator bool)
+
+(defn main [] i32
+  ;; The general-purpose tier, with a ceiling on it. 32 bytes is four i32 and
+  ;; the doubling past it is not.
+  (set tight (heap-allocator))
+  (set-alloc-budget tight 32)
+
+  (handler-bind
+    [(StorageExhausted [c]
+       (set failures (+ failures 1))
+       ;; The condition is a value struct with fixed numeric fields and no
+       ;; rendered message: formatting would allocate, and this is the one path
+       ;; that must not. Rendering happens here, where a working allocator is
+       ;; known.
+       (set last-bytes (.bytes c))
+       (set last-align (.align c))
+       ;; It names which region ran out, so a handler holding several can tell
+       ;; them apart.
+       (set same-allocator (= (.allocator c) (alloc-id tight)))
+       ;; Grow it, then re-attempt the same request. The Vec is untouched and
+       ;; its allocator is unchanged, which is why this retry can succeed.
+       (set-alloc-budget tight (* 4 (alloc-budget tight)))
+       (invoke-restart 'retry))]
+    (let [v (vec-new i32 tight)]
+      ;; Somewhere in here the ceiling is hit, the handler raises it, and the
+      ;; push that failed is re-attempted. No push is lost: a failed push
+      ;; appends nothing and the retry appends exactly once.
+      (dotimes [i 64] (push v (* i 2)))
+      (println (len v))                 ; 64
+      (println (at v 0))                ; 0
+      (println (at v 63))               ; 126
+      (free v)))
+
+  ;; The handler ran, more than once, and what it saw were the numbers of the
+  ;; request that did not fit.
+  (println (> failures 1))              ; true
+  (println (> last-bytes 0))            ; true
+  (println last-align)                  ; 4 — align-of i32, from the call site
+  (println same-allocator)              ; true
+
+  ;; Every allocating operation, not only push. reserve asks for the whole
+  ;; block at once, and clone asks the new allocator for the source's length.
+  (set-alloc-budget tight 32)
+  (set failures 0)
+  (handler-bind
+    [(StorageExhausted [c]
+       (set failures (+ failures 1))
+       (set-alloc-budget tight 4096)
+       (invoke-restart 'retry))]
+    (let [v (vec-new i32 tight)]
+      (reserve v 256)
+      (println (len v))                 ; 0
+      (dotimes [i 8] (push v i))
+      (set-alloc-budget tight 4128)
+      (let [w (clone v)]
+        (println (len w))               ; 8
+        (println (at w 7))              ; 7
+        (free w))
+      (free v)))
+  (println (> failures 0))              ; true
+
+  ;; And the restart is not once-per-program: it is established at each
+  ;; allocation, so a later one offers it again.
+  (set-alloc-budget tight 0)
+  0)
diff --git a/test/programs/stale-region.flan b/test/programs/stale-region.flan
new file mode 100644
index 0000000..fbc1bff
--- /dev/null
+++ b/test/programs/stale-region.flan
@@ -0,0 +1,22 @@
+;;;; spec-memory.md, "Dev builds detect 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
+;;;; moved traps, naming the site. This is the shipping answer to the section
+;;;; the spec leaves open — detection, loud and immediate, rather than the
+;;;; static prevention that with-allocator and context/allocator deny.
+;;;;
+;;;; It is a separate counter from the per-Vec generation word, which answers a
+;;;; different question (a stale slice), and the two must not be conflated.
+(defn main [] i32
+  (let [a (arena-new 4096)]
+    (let [v (vec-new i32 a)]
+      (push v 1)
+      (push v 2)
+      (println (at v 1))
+      ;; The region goes. v is still in scope and still looks fine — nothing
+      ;; is released at scope exit and nothing marked v — which is exactly the
+      ;; case a static rule cannot see.
+      (free-all a)
+      (println (at v 1))))
+  0)
diff --git a/test/programs/vec-double-free.flan b/test/programs/vec-double-free.flan
new file mode 100644
index 0000000..049ee1c
--- /dev/null
+++ b/test/programs/vec-double-free.flan
@@ -0,0 +1,8 @@
+;;;; `free` consumes its argument exactly as any other move does, so the second
+;;;; one is a compile error rather than a runtime crash. Nothing analyses this
+;;;; specially: it is the same dead-binding rule as passing one to a function.
+(defn main [] i32
+  (let [v (vec-new i32)]
+    (free v)
+    (free v)
+    0))
diff --git a/test/programs/vec-moved-in-loop.flan b/test/programs/vec-moved-in-loop.flan
new file mode 100644
index 0000000..fdcd01c
--- /dev/null
+++ b/test/programs/vec-moved-in-loop.flan
@@ -0,0 +1,8 @@
+;;;; A loop body that moves a binding declared outside the loop: the second
+;;;; iteration would use what the first gave away. The dead set alone cannot
+;;;; see this — merged once at the end of the body it counts one move, not two
+;;;; — so it is a rule, and it is refused with the reason.
+(defn main [] i32
+  (let [v (vec-new i32)]
+    (dotimes [i 3] (free v))
+    0))
diff --git a/test/programs/vec-moved.flan b/test/programs/vec-moved.flan
new file mode 100644
index 0000000..7d2ce89
--- /dev/null
+++ b/test/programs/vec-moved.flan
@@ -0,0 +1,15 @@
+;;;; A Vec is move-only: passing one to a function transfers ownership, and the
+;;;; source binding is dead afterwards. That rule is what makes a double free
+;;;; unrepresentable, which is why `free` needs no analysis of its own.
+(defn take [v (Vec i32)] i32
+  (let [n (len v)]
+    (free v)
+    n))
+
+(defn main [] i32
+  (let [v (vec-new i32)]
+    (push v 1)
+    (println (take v))
+    ;; v went with the call. Being refused here is the whole test.
+    (println (len v))
+    0))
diff --git a/test/programs/vec-untyped.flan b/test/programs/vec-untyped.flan
new file mode 100644
index 0000000..0c9651e
--- /dev/null
+++ b/test/programs/vec-untyped.flan
@@ -0,0 +1,8 @@
+;;;; `let` has no type annotation — parse.ml settles that a triple binding is
+;;;; ambiguous and that types are inferred — so a local Vec has nowhere to say
+;;;; what it holds, and the element type is written at the call instead. With
+;;;; neither, this is refused rather than guessed at.
+(defn main [] i32
+  (let [v (vec-new)]
+    (free v)
+    0))
diff --git a/test/programs/vec.flan b/test/programs/vec.flan
new file mode 100644
index 0000000..e352866
--- /dev/null
+++ b/test/programs/vec.flan
@@ -0,0 +1,102 @@
+;;;; (Vec T) — spec-memory.md, "The four container types" and "Allocators".
+;;;;
+;;;; ptr + len + cap + allocator, owning and move-only, over one type-erased
+;;;; runtime. The element type appears nowhere in that runtime: size_of and
+;;;; align_of are produced at the call site, which without generics is simply
+;;;; the concrete call site. So this file being two element types with one
+;;;; runtime behind them is the whole claim.
+
+(defstruct Point [x i32 y i32])
+
+;;; Ownership transfers on the call. The caller's binding is dead after this,
+;;; which is what the refusal cases in test_acceptance assert.
+(defn consume [v (Vec i32)] i32
+  (let [n (len v)]
+    (free v)
+    n))
+
+;;; A Vec is returned by moving it out, so the callee's binding is the
+;;; caller's. Nothing is released at function exit — there is no scope-end
+;;; anything in this language.
+(defn make [n i32] (Vec i32)
+  (let [v (vec-new i32)]
+    (dotimes [i n] (push v (* i i)))
+    v))
+
+(defn sum [xs [i32]] i32
+  (let [total 0]
+    (dotimes [i (len xs)] (set total (+ total (at xs i))))
+    total))
+
+(defn main [] i32
+  (let [v (vec-new i32)]
+    (println (len v))                   ; 0
+    (push v 10)
+    (push v 20)
+    (push v 30)
+    (println (len v))                   ; 3
+    (println (at v 0))                  ; 10
+    (println (at v 2))                  ; 30
+    ;; A Vec element is a place, and the same bounds and epoch check stands
+    ;; behind the value form and the place form.
+    (set (at v 1) 99)
+    (println (at v 1))                  ; 99
+
+    ;; as-slice is a non-owning view: it copies ptr+len and never the
+    ;; elements, and it carries no allocator, so nothing can be freed through
+    ;; one. [at] and [len] over it are the array operations, unchanged.
+    (println (sum (as-slice v)))        ; 139
+    (println (len (as-slice v 1 3)))    ; 2
+    (println (at (as-slice v 1 3) 0))   ; 99
+
+    ;; clone is the only copy: assignment moves. The copy is independent, and
+    ;; freeing it leaves the original alone.
+    (let [w (clone v)]
+      (set (at w 0) -1)
+      (println (at w 0))                ; -1
+      (println (at v 0))                ; 10
+      (free w))
+
+    ;; reserve does not change the length, only the capacity, so a reserve
+    ;; that succeeds is invisible except that the pushes after it do not grow.
+    (reserve v 64)
+    (println (len v))                   ; 3
+    (push v 40)
+    (println (len v))                   ; 4
+
+    (free v))
+
+  ;; A second element type over the same runtime, and a struct element, so
+  ;; that size_of and align_of are doing work rather than both being 4.
+  (let [ps (vec-new Point)]
+    (push ps (Point {:x 1 :y 2}))
+    (push ps (Point {:x 3 :y 4}))
+    (println (len ps))                  ; 2
+    (println (.y (at ps 1)))            ; 4
+    (free ps))
+
+  ;; A Vec made against an explicit allocator records it, so free and clone
+  ;; never need it named again. An arena cannot free one block, so this free
+  ;; keeps the block — releasing it is free-all's job, and that is the
+  ;; difference the capability set exists to state.
+  (let [a (arena-new 4096)]
+    (let [v (vec-new i32 a)]
+      (push v 7)
+      (println (at v 0))                ; 7
+      (free v))
+    (println (can-free? a))             ; false
+    (free-all a)
+    (arena-destroy a))
+
+  ;; The pushes go into whatever the context names, with nothing passed.
+  (let [a (arena-new 4096)]
+    (with-allocator a
+      (let [v (vec-new i32)]
+        (push v 5)
+        (push v 6)
+        (println (+ (at v 0) (at v 1))) ; 11
+        (free v)))
+    (arena-destroy a))
+
+  (println (consume (make 5)))          ; 5
+  0)
diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml
index eadcd5a..da75f72 100644
--- a/test/test_acceptance.ml
+++ b/test/test_acceptance.ml
@@ -293,6 +293,68 @@ let () =
     end;
     (try Sys.remove exe with Sys_error _ -> ());
 
+    (* (Vec T), spec-memory.md. Two element types over one type-erased
+       runtime, which is the whole claim: size_of and align_of are produced at
+       the concrete call site and nothing below it knows the element type. The
+       moves are here too — into a call and out of one — because a Vec that
+       cannot be handed to a function is not a container anyone can use. *)
+    let vec_out =
+      "0\n3\n10\n30\n99\n139\n2\n99\n-1\n10\n3\n4\n2\n4\n7\nfalse\n11\n5\n"
+    in
+    outputs "vec" "programs/vec.flan" vec_out;
+    outputs ~opt:"-O0" "vec, -O0" "programs/vec.flan" vec_out;
+    outputs ~dev:true "vec, dev" "programs/vec.flan" vec_out;
+
+    (* StorageExhausted and retry. The allocator is genuinely exhausted — a
+       ceiling on live bytes, hit repeatedly — and the handler raises it and
+       invokes retry, so the same request is re-attempted and no push is lost.
+       Every allocating operation is covered, not only push: reserve asks for
+       the whole block at once and clone asks for the source's length.
+       At -O0 because the retry loop and the guard after the error are control
+       flow an optimiser would otherwise launder. *)
+    let exhausted_out = "64\n0\n126\ntrue\ntrue\n4\ntrue\n0\n8\n7\ntrue\n" in
+    outputs "storage exhausted, retried" "programs/exhausted.flan" exhausted_out;
+    outputs ~opt:"-O0" "storage exhausted, retried, -O0" "programs/exhausted.flan"
+      exhausted_out;
+    outputs ~dev:true "storage exhausted, retried, dev" "programs/exhausted.flan"
+      exhausted_out;
+
+    (* The same exhaustion with nothing handling it. [error] is the diverging
+       variant: the program stops on the frame that erred rather than carrying
+       on with a push that appended nothing, which is the Odin outcome the rule
+       exists to make impossible. *)
+    let exe = compile "programs/exhausted-unhandled.flan" in
+    let code, text = run exe None in
+    if code <> 134 || not (contains text "before")
+       || not (contains text "unhandled StorageExhausted")
+       || contains text "unreachable"
+    then begin
+      incr failures;
+      Printf.printf
+        "FAIL  an unhandled StorageExhausted stops the program\n\
+        \        got: %S (exit %d)\n     wanted: exit 134, naming the condition\n"
+        text code
+    end;
+    (try Sys.remove exe with Sys_error _ -> ());
+
+    (* The epoch trap: a container whose allocator has been released. This is
+       spec-memory.md's shipping answer to "Open: catching a use-after-release
+       statically" — detection, loud and immediate, rather than a static rule
+       that with-allocator and context/allocator deny the knowledge for. What
+       is asserted is the reason and the site, not the line. *)
+    let exe = compile "programs/stale-region.flan" in
+    let code, text = run exe None in
+    if code <> 134 || not (contains text "programs/stale-region.flan:")
+       || not (contains text "allocator was released")
+    then begin
+      incr failures;
+      Printf.printf
+        "FAIL  a container used after its region was released\n\
+        \        got: %S (exit %d)\n     wanted: exit 134, naming the site\n"
+        text code
+    end;
+    (try Sys.remove exe with Sys_error _ -> ());
+
     (* §2's other half, which cannot be an [outputs] case because it does not
        exit 0: a handler runs, returns normally, and has still not answered the
        error, so the program stops and names the condition. *)
@@ -732,6 +794,21 @@ let () =
        5; this row is the other half of that claim. *)
     refuses "a user-written allocator" "programs/user-allocator.flan"
       "a defn's name in value position";
+    (* Move-only, spec-memory.md. Each of these would otherwise be a double
+       free or a use-after-free at run time, and each is refused at the second
+       use with the first one's location in the message. *)
+    refuses "a Vec used after it was passed" "programs/vec-moved.flan"
+      "was moved at";
+    refuses "a Vec freed twice" "programs/vec-double-free.flan"
+      "double free unrepresentable";
+    (* The one case the dead set cannot answer on its own: merged once at the
+       end of the body it counts one move, not two. *)
+    refuses "a Vec moved inside a loop" "programs/vec-moved-in-loop.flan"
+      "the next iteration would use what this one gave away";
+    (* let has no type annotation, so with no element type and no expectation
+       there is nothing to infer from — and guessing is the alternative. *)
+    refuses "vec-new with nothing saying what of" "programs/vec-untyped.flan"
+      "write the element type";
 
     (* ── wasm32 (NEXT.md, deferred item 6) ──────────────────────────────
        The second target, and the reason sand-headless imports no raylib. What
diff --git a/test/test_flan.ml b/test/test_flan.ml
index ff84835..e2e357e 100644
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@@ -606,8 +606,11 @@ let () =
   (* ── Unconstrained operators, and everything past milestone 2 ──── *)
   rejects_check "no built-in = on strings"
     "(defn f [] bool (= \"a\" \"b\"))" ~needle:"no built-in comparison";
-  rejects_check "Vec is milestone 6"    "(defn f [x (Vec i32)])"
-    ~needle:"milestone 6";
+  (* (Vec T) is built. What is still refused is the arity: one element type,
+     and a near-miss there would otherwise resolve to a type variable and come
+     back as generics. *)
+  rejects_check "Vec takes one type"    "(defn f [x (Vec i32 i32)])"
+    ~needle:"exactly one type";
   rejects_check "Map is milestone 6"    "(defn f [x {string i32}])"
     ~needle:"milestone 6";
   rejects_check "Result is milestone 6" "(defn f [] (Result i32 i32) None)"