JosephFerano/flan
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Merge: the ownership repeal

Browse Source
This commit is contained in:
Joseph Ferano 2026-09-18 08:11:19 +07:00
commit 28f20eb146
8 changed files with 187 additions and 315 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

22
FIX.org
View File

@ -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.

13
NEXT.md
View File

@ -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`.

8
docs/BUGS-2026-09-18.md
View File

@ -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.

9
docs/BUILT.md
View File

@ -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

307
lib/check.ml
View File

@ -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),

74
spec-memory.md
View File

@ -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

21
test/test_acceptance.ml
View File

@ -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

48
test/test_flan.ml
View File

@ -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