From 2edd441ecf664a6ea1a10bfb57025bb6ea067307 Mon Sep 17 00:00:00 2001
From: Joseph Ferano <joseph@ferano.io>
Date: Fri, 18 Sep 2026 07:45:00 +0700
Subject: [PATCH 1/2] The flow analysis is repealed: ownership lives in the
 types, the allocator, and the dev runtime

---
 lib/check.ml            | 307 ++++++++++------------------------------
 test/test_acceptance.ml |  21 +--
 test/test_flan.ml       |  48 ++-----
 3 files changed, 89 insertions(+), 287 deletions(-)

diff --git a/lib/check.ml b/lib/check.ml
index 4635e68..ca3dc2a 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -289,20 +289,6 @@ 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 *data type* 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
@@ -541,9 +527,8 @@ let tyvar_of (t : Types.t) = match t with Types.Var v -> Some v | _ -> None
    double-frees. [copyable?] is the opt-out, exactly as Rust's [T: Copy] is.
 
    In the body this means a generic may not use a parameter twice without
-   declaring [copyable?]: [(defn twice [x $t] $t (+ x x))] is refused, which
-   is right — correct at [i32], a double read of a moved value at [(Vec i32)],
-   and the checker cannot tell which until it substitutes.
+   declaring [copyable?]. Since the repeal this gates the structural rules
+   only — what a struct, union or pool may own — not any use of a binding.
 
    A [Var] only ever survives the abstract pass. Inside an instantiation
    [env.subst] has made everything concrete, so this is [Types.is_move_only]
@@ -1368,7 +1353,7 @@ let invented_ctx env ret =
   { env; ret; slots = 0; slot_tys = []; slot_names = []; scope = [];
     defers = []; outer = []; outer_what = None; in_frames = None; loops = []; tail = false;
     in_defer = false; defer_ok = false; defer_block = "a nested form";
-    dead = []; borrow = false; owner = "<none>" }
+    owner = "<none>" }
 
 (* The address of field [i] of the struct the pointer in slot [p] points at. *)
 let field_addr_of loc sty fty p i =
@@ -1687,24 +1672,11 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr =
   | Ast.If (c, t, e') -> check_if ctx ~tail ?want loc c t e'
   | Ast.While (label, c, body) ->
     (* The condition is part of the loop even though it is written outside the
-       braces: emit puts it in the header block, so it is re-evaluated at the
-       top of every trip, and a condition that gives a value away frees it once
-       per trip. So it is held to the loop's rule on moves and to nothing else
-       the loop changes: it stays outside [in_loop], because a [break] in a
-       condition still means the enclosing loop and a [defer] there is still
-       the outer block's, but its moves are diffed against the same dead set.
-       [dotimes]' count and a [loop]'s initial values are checked outside this
-       regime on purpose: they are evaluated exactly once, before the first
-       trip, so giving one away there is no more than giving it away before
-       the loop. *)
-    let before = ctx.dead in
-    let outer = List.map (fun (_, b) -> b.slot) ctx.scope in
+       braces — emit puts it in the header block, so it is re-evaluated at the
+       top of every trip — but it stays outside [in_loop], because a [break]
+       in a condition still means the enclosing loop and a [defer] there is
+       still the outer block's. *)
     let c = check ctx ~want:Types.Bool c in
-    moved_across_iterations ctx ~before ~outer
-      "this while condition moves a value that was bound outside the loop, and \
-       the condition is evaluated again at the top of every trip, so the second \
-       one would use what the first gave away. Move it out of the loop, or \
-       test something the loop does not give away";
     let body = in_loop ctx ?label (fun () ->
       scoped ctx (fun () -> map_lr (fun b -> check ctx b) body))
     in
@@ -1951,13 +1923,10 @@ and var ctx loc ~want name =
   | _ ->
     match lookup ctx name with
     | Some b ->
-      if move_only ctx.env.tvpreds b.bty then
-        moved ~ty:b.bty 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, _) ->
-        if Types.is_move_only ty then global_borrow ctx loc name ty;
         expect loc ~want (mk loc ty (Tast.Global name))
       | None ->
         match Hashtbl.find_opt ctx.env.cases name with
@@ -2003,95 +1972,16 @@ and var ctx loc ~want name =
            | None -> captured ctx loc name;
          Loc.failk "check/unknown-name" loc "unknown name %s" name)
 
-(* 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 ?ty 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 — %s 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)
-       (match ty with Some t -> Types.to_string t | None -> "a Vec") name
-   | None -> ());
-  if not ctx.borrow then ctx.dead <- (slot, loc) :: ctx.dead
-
-(* Reading a move-only *global*, which is the same fork as [moved] with the
-   other answer: a global is never moved out of, so a site that would have
-   taken ownership is refused rather than recorded.
-
-   The rule this enforces is one sentence — reading a move-only global is
-   always a borrow. It is sound for a reason that does not generalise to
-   locals: the lifetime question, which ownership tracking exists to answer,
-   has a constant answer here. A global lives as long as the process, so
-   nothing may free it and nothing needs to; there is no frame whose exit it
-   could outlive and no second owner to disagree with. What would break the
-   argument is exactly one thing — someone taking ownership — and that is a
-   move, and every move reaches this function because [ctx.borrow] is false
-   everywhere except the operations that said they only look.
-
-   So the dead set is not consulted and not extended. A global cannot be dead:
-   two functions reading the same one are both borrowing it, which is why the
-   per-function dead set that the declaration site used to argue from was
-   never the obstacle it looked like. It could not track a global's ownership;
-   with this rule there is no ownership to track.
-
-   Mutation is not a move and is not refused. [push], [put] and [set] all take
-   their target through [borrowed], so a global (Vec u8) is filled and grown in
-   place, and the aliasing that raises — a push that reallocates invalidating a
-   slice into the same Vec — is the programmer's, exactly as it is for a local
-   (spec-memory.md, "Borrowing", and the note on [as-slice] below). Globals get
-   no rule locals do not have: the dev build's generation word lives on the Vec
-   and traps on a stale slice whether the Vec is a global or not. *)
-and global_borrow ctx loc name (ty : Types.t) =
-  if not ctx.borrow then
-    (* The last clause is conditional, because [clone] stopped being offerable
-       for one of these. A global whose elements own storage is admitted — a
-       move-only global starts zeroed and this one is no different — but
-       cloning it is refused, on the grounds that a bytewise copy is an alias
-       under a name that promises independence. Offering it anyway would send a
-       reader to a second refusal, and there is no other route to an
-       independent copy: the region owns the graph, and [free-all] is the only
-       thing that releases any of it. *)
-    fail loc
-      "%s is %s, which is move-only, and a global of one is only ever \
-       borrowed: its lifetime is the process's, so nothing may take ownership \
-       of it, and this site would. A free through the new owner would leave \
-       every other reader of %s pointing at released memory. Read and mutate \
-       it where it is — (len %s), (at %s i), (push %s x), (set (at %s i) x) \
-       — or take a view with (as-slice %s) or a pointer with (addr %s)%s"
-      name (Types.to_string ty) name name name name name name name
-      (if region_only ctx.env ty then
-         ". There is no independent copy of this one: its elements own \
-          storage, so a clone would alias rather than copy and is refused"
-       else
-         Printf.sprintf
-           ", or an independent copy with (clone %s), which is the one of \
-            these that something else may own" name)
-
-(* 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
+(* What remains of spec-memory.md's ownership section after the repeal of
+   2026-09-18 is entirely in the types: move-only decides what may be copied,
+   the struct/union/pool rules below decide what may own what, and the
+   allocator's capability decides what a free means at run time. Which frees
+   run, and in what order, is the program's own business — the same contract
+   Odin ships with — and the dev build's generation words are the net under
+   it. The flow analysis that used to live here (a per-function dead set, a
+   borrow flag over container reads, a loop-iteration diff) tracked use-after-
+   move and double-free statically; it was repealed rather than repaired when
+   its holes proved structural. See spec-memory.md, "The repeal". *)
 
 (* [defer_ok] is granted again before *every* form, not once before the block:
    [check] withdraws it as it starts, so granting it once would let the first
@@ -2170,7 +2060,7 @@ and check_fn ctx ~want loc (params : string list) body =
       scope = []; defers = []; outer = ctx.scope;
       outer_what = Some "an fn"; in_frames = None; loops = []; tail = false;
       in_defer = false; defer_ok = false; defer_block = "a nested form";
-      dead = []; borrow = false; owner = ctx.owner }
+      owner = ctx.owner }
   in
   List.iter2
     (fun n t -> ignore (bind fctx n t ~assignable:false)) params pts;
@@ -2244,7 +2134,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; outer_what = Some "a handler"; in_frames = None; loops = []; tail = false; in_defer = false; defer_ok = false; defer_block = "a nested form"; dead = []; borrow = false; owner = "<none>" }
+             scope = []; defers = []; outer = ctx.scope; outer_what = Some "a handler"; in_frames = None; loops = []; tail = false; in_defer = false; defer_ok = false; defer_block = "a nested form"; 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.
@@ -2422,53 +2312,24 @@ and check_let ctx ?(tail = false) ?want ?(defer_ok = false) 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 ?label ?entry ?(fresh = []) f =
-  let outer_slots =
-    List.filter (fun s -> not (List.mem s fresh))
-      (List.map (fun (_, b) -> b.slot) ctx.scope)
-  in
-  let before = ctx.dead in
+(* What a loop still contributes to checking after the repeal is scoping, not
+   ownership: the entry below is what [break] and [continue] resolve against,
+   and the defer_block name is what makes a [defer] in here refused as "a loop
+   body" — it would fire once at function exit rather than once per iteration,
+   and the message says so. [fresh] and the iteration move-diff that used it
+   are gone with the flow analysis. *)
+and in_loop ctx ?label ?entry f =
   (* The loop goes on the stack before the body is checked and comes off after,
      so a [break] inside it can see it and one outside it cannot. *)
   let loops = ctx.loops in
-  (* [fresh] is a [loop]'s own names. They are bound before the entry is pushed
-     — their initial values are evaluated once, outside — but [recur] writes
-     every one of them on the way round, so the next iteration never sees what
-     this one gave away and the rule below is not about them. *)
   ctx.loops <- (match entry with Some e -> e | None -> Lloop label) :: loops;
-  (* Named so that a defer written in here is refused as "a loop body" rather
-     than as a nested form: the reason is specific — it would fire once at
-     function exit rather than once per iteration — and the message says it. *)
   let blocker = ctx.defer_block in
   ctx.defer_block <- "a loop body";
   let r = f () in
   ctx.defer_block <- blocker;
   ctx.loops <- loops;
-  moved_across_iterations ctx ~before ~outer:outer_slots
-    "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";
   r
 
-(* The rule a loop adds to the move checker, in one place because two forms
-   need it and they need it for the same reason. Everything that runs more
-   than once runs against the dead set it left behind last time: a slot that
-   was live on the way in and is dead on the way out was given away by code
-   that is about to run again, and the second run would be using what the
-   first one released. Slots bound inside the repeated region are not in
-   [outer] and are not the question — they are born again every trip. *)
-and moved_across_iterations ctx ~before ~outer why =
-  List.iter
-    (fun (slot, where) ->
-       if (not (List.mem_assoc slot before)) && List.mem slot outer then
-         fail where "%s" why)
-    ctx.dead
-
 (* Which loop a [break] or a [continue] means, as a count of loops outwards
    from the innermost — which is what [Tast.Break] carries and what [emit]
    indexes. Refuses three things, each by its own reason: nothing to break out
@@ -2606,7 +2467,7 @@ and check_loop ctx ?want loc bs body =
        is therefore monomorphic, and every other caller hands it a list. *)
     let tbody =
       match
-        in_loop ctx ~entry:(Lrecur names) ~fresh:(List.map fst binds) (fun () ->
+        in_loop ctx ~entry:(Lrecur names) (fun () ->
           [ scoped ctx (fun () ->
               (* The body's last form is the loop's tail, which is the only
                  place a [recur] may stand. [block] distributes it. *)
@@ -2704,15 +2565,7 @@ and check_if ctx ?(tail = false) ?want loc c t e =
     let t = branch ctx (fun () -> in_tail (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 data type 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 = branch ctx (fun () -> in_tail (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 =
@@ -2721,9 +2574,6 @@ and check_if ctx ?(tail = false) ?want loc c t e =
       | None -> if t.Tast.ty = Types.Never then None else Some t.Tast.ty
     in
     let e = branch ctx (fun () -> in_tail (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
@@ -3030,13 +2880,6 @@ and check_match ctx ?(tail = false) ?want loc scrutinee arms =
   let want = ref want in
   let seen = Hashtbl.create 8 in
   let saw_wild = ref false in
-  (* The same rule as [if], and for the same reason: the arms are alternatives,
-     so each is checked from the state before the match and the data type of what
-     they moved survives the join. Checked in sequence against one mutating set
-     they would report the second arm's (free v) as a use after the first arm's
-     move, which is a legal program refused. *)
-  let before = ctx.dead in
-  let joined = ref [] in
   let arms =
     map_lr
       (fun (a : Ast.arm) ->
@@ -3047,28 +2890,20 @@ and check_match ctx ?(tail = false) ?want loc scrutinee arms =
             if Hashtbl.mem seen c then
               fail a.Ast.aloc "this match has two %s arms" c;
             Hashtbl.add seen c ());
-         ctx.dead <- before;
-         let arm =
-           branch ctx (fun () ->
-             let binds =
-               List.map
-                 (fun (n, ty) -> bind ctx n ty ~assignable:false) binds
-             in
-             (* Every arm is the tail, exactly as an [if]'s two arms are.
-                Restored here because checking the scrutinee withdrew it. *)
-             ctx.tail <- tail;
-             let body = block ctx ?want:!want a.Ast.aloc a.Ast.body in
-             if !want = None && body.Tast.ty <> Types.Never then
-               want := Some body.Tast.ty;
-             { Tast.acase = ctor; binds; abody = [ body ] })
-         in
-         joined :=
-           !joined
-           @ List.filter (fun (k, _) -> not (List.mem_assoc k !joined)) ctx.dead;
-         arm)
+         branch ctx (fun () ->
+           let binds =
+             List.map
+               (fun (n, ty) -> bind ctx n ty ~assignable:false) binds
+           in
+           (* Every arm is the tail, exactly as an [if]'s two arms are.
+              Restored here because checking the scrutinee withdrew it. *)
+           ctx.tail <- tail;
+           let body = block ctx ?want:!want a.Ast.aloc a.Ast.body in
+           if !want = None && body.Tast.ty <> Types.Never then
+             want := Some body.Tast.ty;
+           { Tast.acase = ctor; binds; abody = [ body ] }))
       arms
   in
-  ctx.dead <- !joined;
   (* Exhaustiveness is refused, not defaulted. A match that silently fell
      through would have to produce a value of the match's type out of nothing,
      and there is no such value for most types; and the case a data type grows
@@ -3161,7 +2996,7 @@ and check_place ctx loc (p : Ast.place) : Tast.place * Types.t =
          "%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 = borrowed ctx target (fun () -> check ctx target) in
+    let target = 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
@@ -3993,7 +3828,7 @@ and named_call ctx ~want loc name args =
     arity loc name 2 args;
     (match args with
      | [ target; x ] ->
-       let target = borrowed ctx target (fun () -> check ctx target) in
+       let target = 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
@@ -4021,7 +3856,7 @@ and named_call ctx ~want loc name args =
     arity loc name 2 args;
     (match args with
      | [ target; n ] ->
-       let target = borrowed ctx target (fun () -> check ctx target) in
+       let target = check ctx target 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 ]))
@@ -4064,7 +3899,7 @@ and named_call ctx ~want loc name args =
   | "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 target = check ctx target in
        let elem = vec_elem loc "as-slice" target.Tast.ty in
        let lo, hi =
          match rest with
@@ -4087,10 +3922,12 @@ and named_call ctx ~want loc name args =
                                  (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. *)
+  (* spec-memory.md's first release point. Since the repeal, what it consumes
+     it consumes at run time only: nothing marks the binding dead, so a second
+     [free] or a read after this one type-checks and misbehaves at run time —
+     the allocator aborts on a double free it can see, and the dev build's
+     generation word traps a stale read. That is the Odin contract: free is a
+     thing you write, and writing it twice is yours to not do. *)
   | "free" ->
     arity loc name 1 args;
     let target = check ctx (List.hd args) in
@@ -4166,7 +4003,7 @@ and named_call ctx ~want loc name args =
        (* Checked once, then dispatched on what it turned out to be: checking
           it inside a guard as well would allocate the target's slots twice and
           evaluate whatever it was written as twice. *)
-       let target = borrowed ctx target (fun () -> check ctx target) in
+       let target = check ctx target in
        let a = allocator_arg ctx loc rest in
        (match target.Tast.ty with
         (* The refusal that did *not* come down with the type-level ones, and
@@ -4294,7 +4131,7 @@ and named_call ctx ~want loc name args =
     arity loc name 2 args;
     (match args with
      | [ target; x ] ->
-       let target = borrowed ctx target (fun () -> check ctx target) in
+       let target = check ctx target in
        let elem = pool_elem loc "insert" target.Tast.ty in
        let x = check ctx ~want:elem x in
        let hty = Types.Handle elem in
@@ -4344,7 +4181,7 @@ and named_call ctx ~want loc name args =
     arity loc name 2 args;
     (match args with
      | [ target; h ] ->
-       let target = borrowed ctx target (fun () -> check ctx target) in
+       let target = check ctx target in
        let elem = pool_elem loc "resolve" target.Tast.ty in
        let h = check ctx ~want:(Types.Handle elem) h in
        (match h.Tast.ty with
@@ -4400,7 +4237,7 @@ and named_call ctx ~want loc name args =
     arity loc name 2 args;
     (match args with
      | [ target; h ] ->
-       let target = borrowed ctx target (fun () -> check ctx target) in
+       let target = check ctx target in
        let elem = pool_elem loc "release" target.Tast.ty in
        let h = check ctx ~want:(Types.Handle elem) h in
        (match h.Tast.ty with
@@ -4425,7 +4262,7 @@ and named_call ctx ~want loc name args =
      quiet wrong answer this whole type exists to remove. *)
   | "live" ->
     arity loc name 1 args;
-    let target = borrowed ctx (List.hd args) (fun () -> check ctx (List.hd args)) in
+    let target = check ctx (List.hd args) in
     ignore (pool_elem loc "live" target.Tast.ty);
     let n = rt loc (Types.Int Types.I64) "flan_pool_live" [ target; here loc ] in
     expect loc ~want (mk loc index_ty (Tast.Prim (Tast.Cast index_ty, [ n ])))
@@ -4444,7 +4281,7 @@ and named_call ctx ~want loc name args =
     arity loc name 2 args;
     (match args with
      | [ target; i ] ->
-       let target = borrowed ctx target (fun () -> check ctx target) in
+       let target = check ctx target in
        let elem = pool_elem loc "pool-handle" target.Tast.ty in
        let i = check ctx ~want:index_ty i in
        let hty = Types.Handle elem in
@@ -4510,7 +4347,7 @@ and named_call ctx ~want loc name args =
     arity loc name 3 args;
     (match args with
      | [ target; k; v ] ->
-       let target = borrowed ctx target (fun () -> check ctx target) in
+       let target = check ctx target in
        let kt, vt = map_kv loc "put" target.Tast.ty in
        let k = check ctx ~want:kt k in
        let v = check ctx ~want:vt v in
@@ -4549,7 +4386,7 @@ and named_call ctx ~want loc name args =
     arity loc name 2 args;
     (match args with
      | [ target; k ] ->
-       let target = borrowed ctx target (fun () -> check ctx target) in
+       let target = check ctx target in
        let kt, vt = map_kv loc "get" target.Tast.ty in
        let k = check ctx ~want:kt k in
        (* Deferred, and the placeholder is [None] rather than [Unit]: this
@@ -4607,7 +4444,7 @@ and named_call ctx ~want loc name args =
     arity loc name 2 args;
     (match args with
      | [ target; k ] ->
-       let target = borrowed ctx target (fun () -> check ctx target) in
+       let target = check ctx target in
        let kt, vt = map_kv loc "map-remove!" target.Tast.ty in
        let k = check ctx ~want:kt k in
        (* Deferred exactly as [get] is, and with [None] for the same reason:
@@ -4668,7 +4505,7 @@ and named_call ctx ~want loc name args =
     arity loc name 4 args;
     (match args with
      | [ target; cur; k; v ] ->
-       let target = borrowed ctx target (fun () -> check ctx target) in
+       let target = check ctx target in
        let kt, vt = map_kv loc "map-next!" target.Tast.ty in
        let cur = check ctx ~want:(Types.Ptr (Types.Int Types.I64)) cur in
        let k = check ctx ~want:(Types.Ptr kt) k in
@@ -4692,7 +4529,7 @@ and named_call ctx ~want loc name args =
     arity loc name 2 args;
     (match args with
      | [ target; k ] ->
-       let target = borrowed ctx target (fun () -> check ctx target) in
+       let target = check ctx target in
        let kt, vt = map_kv loc "has-key?" target.Tast.ty in
        let k = check ctx ~want:kt k in
        (* Deferred, and the placeholder is a [bool] — the form a condition
@@ -4967,7 +4804,7 @@ and named_call ctx ~want loc name args =
   | "len" ->
     arity loc name 1 args;
     let target = List.hd args in
-    let a = borrowed ctx target (fun () -> check ctx target) in
+    let a = check ctx target in
     (match a.Tast.ty with
      | Types.Array _ | Types.Slice _ | Types.String ->
        prim Tast.Len index_ty [ a ]
@@ -4993,7 +4830,7 @@ and named_call ctx ~want loc name args =
   | "at" ->
     (match args with
      | target :: idx when idx <> [] ->
-       let target = borrowed ctx target (fun () -> check ctx target) in
+       let target = check ctx target in
        (match target.Tast.ty with
         | Types.Vec _ ->
           let p, elem = vec_at ctx loc target idx in
@@ -5208,7 +5045,7 @@ and named_call ctx ~want loc name args =
        nothing. Without this, (println v) would consume a Vec and every
        printing of one would be its last. *)
     let target = List.hd args in
-    let a = borrowed ctx target (fun () -> check ctx target) in
+    let a = check ctx target in
     (* ── The allow-list, and what it takes to get on it ───────────────
        plan.org names [println] as the one compiler-provided exception — it
        "selects a structural printer at each concrete instantiation" — and
@@ -6081,7 +5918,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 = []; outer_what = None; in_frames = None; loops = []; tail = false; in_defer = false; defer_ok = false; defer_block = "a nested form"; dead = []; borrow = false; owner = "<none>" } v).Tast.ty
+      outer = []; outer_what = None; in_frames = None; loops = []; tail = false; in_defer = false; defer_ok = false; defer_block = "a nested form"; owner = "<none>" } v).Tast.ty
   in
   let pending = ref (List.rev !untyped) in
   let rec settle () =
@@ -6204,7 +6041,7 @@ let check_union_members env =
 let rec 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 = []; outer_what = None; in_frames = None; loops = []; tail = false; in_defer = false; defer_ok = false; defer_block = "a nested form"; dead = []; borrow = false;
+                outer = []; outer_what = None; in_frames = None; loops = []; tail = false; in_defer = false; defer_ok = false; defer_block = "a nested form";
                 owner = fn.Ast.name } in
   List.iter2
     (fun (p : Ast.field) ty ->
@@ -6323,10 +6160,12 @@ and check_generic env (fn : Ast.fn) =
    checking a function. *)
 let () = check_fn_ref := check_fn
 
-(* A global of move-only type is legal, and what makes it legal is [var]'s
-   refusal rather than anything here: reading one is always a borrow, so no
-   function can take it, and none can free it. See [global_borrow] for why that
-   one sentence is enough where a general ownership model would not be.
+(* A global of move-only type is legal. Before the repeal what made it legal
+   was a flow rule — reading one was always a borrow, so nothing could take
+   or free it. That rule is gone with the rest of the flow analysis: a global
+   Vec may now be handed to a function, bound, or freed, and keeping its
+   process-long lifetime honest is the program's business, on the same terms
+   as every other free.
 
    What this pass still decides is how such a global may be *started*, and the
    answer is zeroed and nothing else. A zeroed Vec is a real empty Vec — null
@@ -6405,7 +6244,7 @@ let no_union_init env loc n what (v : Tast.expr) =
 
 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 = []; outer_what = None; in_frames = None; loops = []; tail = false; in_defer = false; defer_ok = false; defer_block = "a nested form"; dead = []; borrow = false; owner = "<none>" } in
+      outer = []; outer_what = None; in_frames = None; loops = []; tail = false; in_defer = false; defer_ok = false; defer_block = "a nested form"; owner = "<none>" } in
   match d.Ast.d with
   | Ast.Defvar (n, _, init) ->
     let ty, _ = Hashtbl.find env.globals n in
@@ -6668,7 +6507,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 = []; outer_what = None; in_frames = None; loops = []; tail = false; in_defer = false; defer_ok = false; defer_block = "a nested form"; dead = []; borrow = false; owner = "<none>" }
+      outer = []; outer_what = None; in_frames = None; loops = []; tail = false; in_defer = false; defer_ok = false; defer_block = "a nested form"; owner = "<none>" }
   in
   let t = check ctx e in
   (t, Array.of_list (List.rev ctx.slot_tys),
diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml
index 6451bb8..48df08c 100644
--- a/test/test_acceptance.ml
+++ b/test/test_acceptance.ml
@@ -1958,17 +1958,11 @@ let () =
        pointer-width. Two reasons, both named, neither a function value. *)
     refuses "a user-written allocator" "programs/user-allocator.flan"
       "is no longer what is missing";
-    (* 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";
+    (* Move-only, spec-memory.md, since the repeal: the three fixtures that
+       were refused here — a use after a pass, a double free, a move inside a
+       loop — now compile, and what they do at run time is the allocator's and
+       the dev build's to catch. They are kept as programs (the double-free
+       one is what the sanitize sweep watches) but no longer as refusals. *)
     (* 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"
@@ -2537,11 +2531,6 @@ ERR@7 unexpected token: not the kind the caller was reading
     refuses_src "map-new with nothing to say what it maps"
       "(defn main [] i32 (let [m (map-new)] (free m)) 0)"
       "nothing here says what (map-new) maps";
-    (* A map is move-only like a Vec, and the refusal names the type that was
-       moved rather than saying "a Vec" whatever it was. *)
-    refuses_src "a map used after it was moved"
-      "(defn main [] i32 (let [m (map-new i32 i32)] (free m) (put m 1 2)) 0)"
-      "cannot be used again";
     (* ── Data type values ───────────────────────────────────────────
        defdata parsed and its shape was checked; naming the type and
        constructing a value were refused as milestone 6. The program covers a
diff --git a/test/test_flan.ml b/test/test_flan.ml
index 167c9c1..c8292b5 100644
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@@ -1078,26 +1078,11 @@ let () =
     ~needle:"cannot be cloned";
 
   (* ── A move-only global ─────────────────────────────────────────────
-     Legal now, and legal because of one rule: reading one is always a borrow.
-     The accepted side is programs/vec-global.flan, which has to run to say
-     anything; these are the four things the rule refuses, and between them
-     they are the whole of it.
-
-     The first two are the rule itself. Ownership is what may not be taken, and
-     the two ways to take it — hand the global to something that owns its
-     parameter, or bind it to a local that owns it — are the same refusal at
-     the read, because that is where a move would have been recorded for a
-     local. [free] is the third of them and reaches it the same way: it does
-     not borrow its target, so nothing special had to be written for it. *)
-  rejects_check "passing a global Vec to a function"
-    "(defvar g (Vec u8)) (defn eat [v (Vec u8)] () (free v)) (defn f [] () (eat g))"
-    ~needle:"only ever borrowed";
-  rejects_check "freeing a global Vec"
-    "(defvar g (Vec u8)) (defn f [] () (free g))"
-    ~needle:"only ever borrowed";
-  rejects_check "binding a global Vec to a local"
-    "(defvar g (Vec u8)) (defn f [] () (let [v g] (free v)))"
-    ~needle:"only ever borrowed";
+     Legal, started zeroed, and since the repeal of the flow analysis it is
+     ownable like anything else: passing, binding and freeing one all
+     type-check, and the process-long lifetime is the program's to keep. The
+     accepted side is programs/vec-global.flan. What is still refused about
+     one is declaration-shaped, below. *)
   (* And the two declaration shapes. A computed initialiser would have to run
      before main, which is a path [Emit.const] does not have and which
      [x86.ml] deliberately leaves out of a reload module; a defconst could
@@ -1224,14 +1209,7 @@ let () =
   rejects_check "a labelled break may not leave a loop"
     "(defn f [] () (while :o true (loop [i 0] (break :o))))"
     ~needle:"no value to give";
-  (* A while's condition runs once per trip, so it lives under the same rule
-     as the body: what it gives away, it gives away again next time round.
-     Before this was checked the program below compiled and aborted in free(). *)
-  rejects_check "a while condition may not move what the loop is standing on"
-    "(defn eat [v (Vec i32)] bool (do (free v) true)) \
-     (defn f [] () (let [v (vec-new i32)] (while (eat v) (break))))"
-    ~needle:"evaluated again at the top of every trip";
-  accepts "a condition that only looks at what it tests is fine"
+  accepts "a while condition is an ordinary expression"
     "(defn f [] () (let [v (vec-new i32)  n 0] \
        (while (and (< n 10) (> (len v) 0)) (set n (+ n 1))) (free v)))";
   rejects_check "loop takes no label"
@@ -2687,16 +2665,12 @@ let () =
     ~needle:"is not a type variable of f"
     "(defn f [a i32] i32 {:where (ordered? $t)} a)";
 
-  (* Move-only by default, which is the other half of the where clause and the
-     one with no Odin counterpart: Odin has no move semantics, so its $T never
-     has to answer. The prior art is Rust's T: Copy, and the difference is
-     that copyable? is a question the compiler answers rather than a trait a
-     user implements. Conservative in the safe direction — move is the
-     stricter rule, so assuming it can only refuse a valid program. *)
-  rejects_check "a type variable is move-only until it says otherwise"
-    ~needle:"cannot be used again"
+  (* Move-only by default still decides the structural rules for a $t — what
+     may own one — but since the repeal a double use of a binding is not
+     checked, so both of these are accepted with and without the clause. *)
+  accepts "a type variable is usable twice without copyable?"
     "(defn twice [a $t b (Fn [$t $t] $t)] $t (b a a))";
-  accepts "and copyable? is the opt-out"
+  accepts "and copyable? is still a clause a signature may state"
     "(defn twice [a $t b (Fn [$t $t] $t)] $t {:where (copyable? $t)} (b a a))";
 
   (* The allow-list, and it has two members. println over a type variable is

From 2b9f271cc3347822a7064b7695e4e37f744550e1 Mon Sep 17 00:00:00 2001
From: Joseph Ferano <joseph@ferano.io>
Date: Fri, 18 Sep 2026 07:46:37 +0700
Subject: [PATCH 2/2] The repeal is written down where the rules were: spec,
 BUILT, NEXT, the ledger, FIX

---
 FIX.org                 | 22 ++++++++++++
 NEXT.md                 | 13 ++++----
 docs/BUGS-2026-09-18.md |  8 ++++-
 docs/BUILT.md           |  9 +++--
 spec-memory.md          | 74 +++++++++++++++++++++++++++++++----------
 5 files changed, 98 insertions(+), 28 deletions(-)

diff --git a/FIX.org b/FIX.org
index 88a1e5d..2d001f2 100644
--- a/FIX.org
+++ b/FIX.org
@@ -234,3 +234,25 @@ Left for the author, recorded where each lives:
 - sand.flan:167 still holds the refused defconst experiment; the diagnostic
   now prints in full and names the fix.
 - Tier 2 (install and shipping) deliberately not started.
+
+* The repeal, 2026-09-18
+
+The ownership flow analysis is removed: the per-function dead set, the borrow
+flag, the loop-iteration diff, and the borrowed-never-moved rule for globals.
+Use-after-move and double-free are no longer compile errors. What stands:
+move-only as a type property (assignment hands over the header, clone is the
+only copy), the struct/union/pool ownership rules, defconst-vs-defvar for
+move-only globals, defer, all allocator capabilities, and the dev build's
+generation checks — now the primary net, which is the Odin position the
+memory design came from.
+
+Decided after the bug hunt put four of its ten lanes inside this machinery.
+An unsound checker is worse than none, because it is believed. The door back
+is spec-memory.md's provenance pass: removal widened acceptance without
+changing any accepted program's meaning, so a stricter pass can return
+additively. spec-memory.md "The repeal" is the amendment; BUILT.md and
+NEXT.md are annotated at their live claims.
+
+Two of the day's fix lanes were cancelled with this (borrowed-flag, region
+element); the while-condition fix merged in the morning is deleted again by
+the repeal, and its pin with it.
diff --git a/NEXT.md b/NEXT.md
index 966f2d9..f033eb8 100644
--- a/NEXT.md
+++ b/NEXT.md
@@ -657,9 +657,9 @@ The prelude keeps a per-type layer for the numeric ones. That is the honest numb
    while `copyable?` is a predicate the compiler answers, because it already knows which types own heap storage.
    Same ergonomics, none of the trait machinery, consistent with the `where` decision above.
 
-   What this means in the body: a generic may not use a parameter twice unless it declares `copyable?`.
-   `(defn twice [x $t] $t (+ x x))` is refused without it — correct at `i32`, wrong at `(Vec i32)`, and the
-   checker cannot tell which until it substitutes.
+   What this meant in the body — a generic may not use a parameter twice unless it declares `copyable?` — was
+   repealed 2026-09-18 with the rest of the flow analysis; move-only-by-default still governs the structural
+   rules (what a struct, union or pool may own at a `$t`).
 
 1. **The runaway refusal.** `(defn grow [x $t] () (grow [x x]))` asks for a copy at `[2 t]`, then `[2 [2 t]]`,
    forever. Before the spike's cap it did not fail, it **hung** — and `Session.eval` runs the same code, so what
@@ -1728,10 +1728,9 @@ Two smaller findings, both written down beside the code that ran into them:
   macros from the forms fed back as `extra`. `format-f64` is `(clamp prec 0 9)` now. "A prelude macro may not call a
   macro" stands and names itself when violated.
 
-- **A returned `Vec` is a move, and the dead set spans the function**, so an early `(return v)` on one branch kills
-  the binding for the `v` at the foot of another. `replace-bytes` guards its empty-needle case with an `if` rather
-  than a `when`/`return` for that reason. Probably correct as it stands — the analysis is not path-sensitive and
-  making it so is a real piece of work — but it is a shape that reads as though it should compile.
+- ~~**A returned `Vec` is a move, and the dead set spans the function**~~ **Repealed 2026-09-18** with the rest of
+  the flow analysis (spec-memory.md, "The repeal"): the early-`return` shape compiles now, and `replace-bytes` no
+  longer needs its `if` workaround, though it keeps it harmlessly.
 
 Already present and easy to miss: an **EDN parser**, at `vendor/edn/edn.flan`.
 
diff --git a/docs/BUGS-2026-09-18.md b/docs/BUGS-2026-09-18.md
index a143d87..3ecae2a 100644
--- a/docs/BUGS-2026-09-18.md
+++ b/docs/BUGS-2026-09-18.md
@@ -7,6 +7,8 @@ marked **DISPATCHED** have fix lanes; the rest are recorded here and wait.
 ## Dispatched
 
 ### 1. `borrowed` grants the borrow flag to whole subtrees — moves inside container targets vanish
+**Repealed, not fixed (2026-09-18):** the flow analysis this hole lived in was removed wholesale
+(spec-memory.md, "The repeal"). The trigger programs now compile by design and misbehave at run time.
 `lib/check.ml:2062-2076`. The flag gates both `moved` (2003) and `global_borrow` (2033),
 and is set across the entire checking of the target: the index argument of `at`, the base
 of any `Field`. A move nested there is never recorded.
@@ -20,6 +22,8 @@ Fix direction: narrow the flag to the target's own read — restore `ctx.borrow`
 index of `at`; treat `Field` as simple only when its base chain bottoms out at a `Var`.
 
 ### 2. A `while` condition is move-checked outside `in_loop` — double free on iteration two
+**Fixed, then repealed (2026-09-18):** the fix merged (47cb46a) and was removed the same day with the
+whole flow analysis. The trigger compiles and aborts in the allocator at run time, by design.
 `lib/check.ml:1688-1691`. The condition is checked before `in_loop` is entered, but
 emit re-runs it every trip (`emit.ml:1838`). A condition that moves a local frees it
 once per iteration. Confirmed: glibc double-free abort, exit 134.
@@ -66,7 +70,9 @@ territory; fix or record, the lane's call.
 
 ## Recorded, not scheduled
 
-- **Region guard never asks about elements** (`lib/check.ml:1272`, refusals 4092/4165):
+- **Region guard never asks about elements** — **repealed, not fixed (2026-09-18)**: with the flow
+  analysis gone, `free` of an `at` result is no longer a checker question; the mixed-allocator
+  construction is legal and its misuse is a run-time matter. (`lib/check.ml:1272`, refusals 4092/4165):
   a heap-backed inner Vec pushed into an arena-backed outer passes the guard; `at` then
   hands out an owning header, `free` accepts it, and the later read is a confirmed UAF
   (printed garbage). Breaks the premise stated in the clone note at check.ml:4152.
diff --git a/docs/BUILT.md b/docs/BUILT.md
index 5f33f1a..19df4e9 100644
--- a/docs/BUILT.md
+++ b/docs/BUILT.md
@@ -2483,6 +2483,10 @@ different reason (below), but the adopt rule is what makes `Zero` of a Vec a usa
 
 ### Move-only is a dead set, and it is flow-sensitive at a join
 
+**Repealed 2026-09-18.** The dead set, the borrow flag, and the loop rule this section describes were removed with
+the rest of the flow analysis — spec-memory.md, "The repeal", is the amendment. The section is kept as the record of
+what was built and why. Move-only as a *type* property (what may be copied, what may own what) stands.
+
 Reading a move-only local is a move unless the site said it was a borrow. That is the conservative direction: passing
 one to a function, binding it, returning it and `free`ing it are all moves and all reach one place, and the handful of
 operations that only look at a container (`at`, `len`, `as-slice`, `push`, `reserve`, `clone`) say so. Only a
@@ -3597,9 +3601,8 @@ be wrong in a way worth being able to see: the prelude *was* reaching the expand
   over the file being compiled; the prelude reaches the checker through `Check.program`'s prepend. The call resolves
   to the macro's underlying `defn` and reports an arity error, which is why `format-f64` writes
   `(min 9 (max 0 prec))`.
-- **A returned `Vec` is a move and the dead set spans the function**, so an early `(return v)` on one branch kills
-  the binding at the foot of another. `replace-bytes` guards its empty needle with an `if` rather than a
-  `when`/`return` for that reason.
+- ~~**A returned `Vec` is a move and the dead set spans the function**~~ Repealed 2026-09-18; the shape compiles
+  now and `replace-bytes`'s `if` guard is a harmless leftover.
 
 ### The refusal block is down from eight reasons to four
 
diff --git a/spec-memory.md b/spec-memory.md
index 23558f4..ad960e0 100644
--- a/spec-memory.md
+++ b/spec-memory.md
@@ -1,6 +1,9 @@
 # Spec 1 — Ownership, containers, and copies
 
-Status: **frozen**. Closes plan.org open decisions #6 and #10, and resolves the
+Status: **frozen**, with one amendment: **the repeal of 2026-09-18** (see "The
+repeal", below), which removed the static flow analysis — use-after-move and
+double-free are no longer compile errors. Everything structural in this
+document still governs. Closes plan.org open decisions #6 and #10, and resolves the
 contradiction between "value structs copy on assignment" and owning containers.
 The Allocators section additionally settles the four things that had to be
 decided before `Vec` and `Map` are written: when storage is released, the `drop`
@@ -26,9 +29,13 @@ facility (see plan.org, "Managed classes").
   or a literal in read-only memory. Copying a slice copies ptr+len, never the
   elements. A slice may be `const`-qualified; freeing through one is not possible
   because a slice has no allocator and no `cap`.
-- `(Vec T)` and `(Map K V)` are **move-only**. Binding, passing, or returning one
-  transfers ownership; the source binding is dead afterwards and using it is a
-  compile error. There is no shallow copy, so there is no double free.
+- `(Vec T)` and `(Map K V)` are **move-only**. Assignment hands over the one
+  header rather than copying it — there is no implicit shallow copy, so two
+  owners never arise from an assignment; `(clone x)` is the only spelling of a
+  second, independent one. Since the repeal, using the source binding again is
+  not a compile error: the header is still there, and a program that frees
+  through it twice or reads through it after a free misbehaves at run time,
+  where the allocator and the dev build's generation word are the net.
 
 ## Maps — first implementation
 
@@ -106,15 +113,14 @@ region" for the rule that stands in its place and for what it costs.
 
 ## Globals of move-only type
 
-A global may be a `Vec` or a `Map`, and **reading one is always a borrow, never
-a move**. Nothing can take ownership of it, so nothing can `free` it; its
-lifetime is the process's and it is never released. That is one rule rather than
-a general ownership model for globals, and it is sound for the reason a general
-model would be needed and is not: the lifetime question has a constant answer.
-Passing a global to a function that owns its parameter, binding it to a local,
-returning it and freeing it are all refused at the read, which is exactly where
-a move would have been recorded for a local. `(clone g)` is the one of these
-that yields something another owner may have.
+A global may be a `Vec` or a `Map`. Its intended lifetime is the process's — it
+is loaded once and never released — and before the repeal a flow rule enforced
+that: reading one was always a borrow, so nothing could take or free it. Since
+the repeal the intent is unchanged and the enforcement is manners: passing,
+binding, or freeing a global type-checks, and a program that frees one while
+other code still reads it has the ordinary use-after-free it would have with
+any other value. `(clone g)` remains the way to get something another owner
+may have.
 
 Such a global is **mutable in place**: `push`, `put`, `reserve` and `set` all
 take their target as a borrow, so a global `(Vec u8)` is filled and grown where
@@ -139,6 +145,40 @@ outlive `main` — nothing re-runs between one entry and the next, so a re-enter
 `main` finds the global as it left it. Assigning a second time overwrites the
 first block and leaks it; there is no `drop`, and freeing is a thing you write.
 
+## The repeal — 2026-09-18
+
+The first implementation carried a static flow analysis: a per-function dead
+set recording moved-out bindings, a borrow flag over the container-reading
+operations, an iteration diff for loops, and a borrowed-never-moved rule for
+globals. It made use-after-move and double-free compile errors. It was removed,
+and removed rather than repaired, after one day's bug hunt found four
+structural holes in it (a move hidden in a borrowed target's subtree, the same
+hole through a global, a `while` condition outside the loop rule, and the
+region guard never asking about elements — docs/BUGS-2026-09-18.md). Each was
+fixable; the shape of the four together said the analysis would keep growing
+holes, and a checker that sometimes misses is worse than none, because it is
+believed.
+
+What the language promises after the repeal is Odin's contract, which is the
+model this memory design was built from in the first place:
+
+- **The types** still decide what may be copied and what may own what: move-only
+  assignment hands over the header, `clone` is the only copy, and the
+  struct/union/pool ownership rules all stand.
+- **The allocator** still decides what a free means: `can-free`, regions,
+  `free-all`, and the region-only rules for containers of owning elements all
+  stand.
+- **Which frees run, and when, is the program's.** `defer` is the tool, and a
+  double free or use-after-free is a run-time misbehaviour, not a compile
+  error.
+- **The dev build detects.** The generation word on `Vec`, the region epoch
+  trap, and the block registry are the net, where a game is actually run.
+
+A future provenance pass (the "Open" section at the end of this document, and
+plan.org #3) remains the door back to static checking. It is additive: nothing
+removed here changed what an accepted program means, so a stricter pass can
+return without changing the language, only its acceptances.
+
 ## Taking an address
 
 `(addr x)` yields `(Ptr T)` for any assignable place `x` — a local, a global, a
@@ -334,10 +374,10 @@ There are exactly two release points, and neither of them is a scope.
    (a `Texture2D`, a socket, a file handle — see `drop` below). For a value that
    holds a resource and no storage, `free` runs `drop` and nothing else; it is
    still the release operation, and it is how a `Texture2D` in a local is
-   released. `free` consumes its argument exactly as any other move does: the source
-   binding is dead afterwards and using it is a compile error. That rule is
-   already what makes a double free unrepresentable, so `free` needs no new
-   analysis.
+   released. Since the repeal, `free` consumes at run time only: nothing marks
+   the binding dead, and a second `free` or a later read through it is a
+   run-time misbehaviour the allocator or the dev build catches, not a compile
+   error.
 2. **Region release** — `(free-all a)` on an allocator, which releases
    everything made from it at once, including storage reachable from bindings
    that are still in scope. The per-frame `(free-all context/temp)` at the top