The projectile asks, and is told the thing it was chasing is gone

The surface: (pool-new T), (insert p x) answering a handle, (resolve p h)
answering (Option (Ptr T)), (release p h) answering whether this call was
the one that released it, (len p) and (live p), and (pool-handle p i) for
enumeration. free extends to the pool and refuses a handle by name, because
a handle owns nothing and consuming one copy would say nothing about the
others.

resolve answers a pointer rather than a value because spec-memory.md's own
worked example does, and says why a line above it: a pattern binding binds
a value, and a copy cannot be written back.

test/programs/handles.flan prints <handle 1:1> and <handle 1:3> for the same
slot before and after a death, and the projectile still holding the first
gets -1 rather than the newcomer's 99.
This commit is contained in:
Joseph Ferano 2026-09-13 07:55:24 +07:00
parent 8f429bcd5d
commit e933f5a84c
4 changed files with 423 additions and 2 deletions

View File

@ -2467,6 +2467,42 @@ and map_new_types ctx ~want loc args =
"nothing here says what (map-new) maps — write the key and value \
types, as (map-new string i32), or give the binding a type")
(* The element type for [pool-new]. The same rule [vec-new] uses and for the
same reason: a [let] has no type annotation, so a local pool has nowhere
else to say what it holds. *)
and pool_new_elem ctx ~want loc args =
let named =
match args with
| { Ast.e = Ast.Var n; _ } :: rest
when lookup ctx n = None
&& (not (Hashtbl.mem ctx.env.globals n))
&& type_named ctx n ->
Some (resolve_name ctx.env ~seen:[] loc n, rest)
| _ -> None
in
match named with
| Some (t, rest) ->
if Types.is_move_only t then
fail loc
"(Pool %s) holds a move-only element, and the type-erased runtime \
copies and releases slots bytewise. Recursive teardown arrives with \
drop (step 5 in NEXT.md)"
(Types.to_string t);
t, rest
| None ->
(match want with
| Some (Types.Pool t) -> t, args
| _ ->
fail loc
"nothing here says what (pool-new) is a Pool of — write the element \
type, as (pool-new Enemy), or give the binding a type")
(* The element type, or the reason this is not a Pool. *)
and pool_elem loc what (t : Types.t) =
match t with
| Types.Pool e -> e
| other -> fail loc "%s takes a (Pool T), found %s" what (Types.to_string other)
(* The element type, or the reason this is not a Vec. *)
and vec_elem loc what (t : Types.t) =
match t with
@ -2937,6 +2973,20 @@ and named_call ctx ~want loc name args =
expect loc ~want
(rt loc Types.Unit "flan_map_free"
[ target; size_of loc k; size_of loc v; here loc ])
(* The owner, not a slot. Every handle into it is stale afterwards and
answers None, which is a strictly better afterlife than a Vec's
binding gets that one is a compile error and this one is a run-time
answer, because handles are copies and the checker cannot see them
all. That asymmetry is the reason handles exist. *)
| Types.Pool elem ->
expect loc ~want
(rt loc Types.Unit "flan_pool_free"
[ target; size_of loc elem; align_of loc elem; here loc ])
| Types.Handle _ ->
fail loc
"free takes the owner, and a handle owns nothing — it is a copyable \
number, so consuming one copy would say nothing about the others. \
(release p h) recycles one slot; (free p) releases the pool"
| other ->
(* A field is never freed on its own: it would leave its owner partly
dead with no way to say so. *)
@ -2974,6 +3024,18 @@ and named_call ctx ~want loc name args =
(Tast.Let ([ (d, mk loc mty (Tast.Zero mty)) ],
[ alloc_guard ctx loc attempt;
mk loc mty (Tast.Local d) ])))
(* Refused by name rather than falling through to "clone takes a
(Vec T)". Copying a pool would duplicate every slot *and* every
generation counter, so a handle into the original would resolve in
the copy too two live entities behind one identity, which is the
exact confusion the type exists to prevent. If a program wants a
second world it builds one and inserts into it, and the new handles
say they are new. *)
| Types.Pool _ ->
fail loc
"a pool cannot be cloned: the copy would carry the same slot \
generations, so one handle would resolve in both and name two \
different things. Build a second pool and insert into it"
| _ ->
let elem = vec_elem loc "clone" target.Tast.ty in
let d = fresh_slot ctx (Types.Vec elem) in
@ -2990,6 +3052,212 @@ and named_call ctx ~want loc name args =
mk loc (Types.Vec elem) (Tast.Local d) ]))))
| _ -> fail loc "clone is (clone v) or (clone v allocator)")
(* ── (Pool T) and (Handle T), spec-memory.md ───────────────────── *)
(* The same type-erased shape the Vec has, for the same reason: size_of and
align_of are produced here because here is where the concrete element
type is known, and nothing below the call site has ever heard of it. *)
(* (pool-new), (pool-new T), (pool-new a), (pool-new T a). *)
| "pool-new" ->
let elem, args = pool_new_elem ctx ~want loc args in
let a = allocator_arg ctx loc args in
let pty = Types.Pool elem in
let p = fresh_slot ctx pty in
(* [flan_pool_init] cannot fail — a pool with no slots allocates nothing —
but it goes under the guard anyway, so that the day it does allocate
the site is already the one that signals. *)
let attempt =
rt loc (Types.Int Types.I8) "flan_pool_init"
[ mk loc pty (Tast.Local p); a; size_of loc elem; align_of loc elem;
here loc ]
in
expect loc ~want
(mk loc pty
(Tast.Let ([ (p, mk loc pty (Tast.Zero pty)) ],
[ alloc_guard ctx loc attempt;
mk loc pty (Tast.Local p) ])))
(* (insert p x) -> (Handle T). The handle is the *only* way back to what was
inserted: a pool hands out no index and no pointer, because an index does
not notice a reuse and that is the entire point. *)
| "insert" ->
arity loc name 2 args;
(match args with
| [ target; x ] ->
let target = borrowed ctx target (fun () -> 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
(* The element is bound before the loop so that a [retry] re-attempts
the allocation and not the expression that produced the value
[push]'s rule, and for the same reason. *)
let e = fresh_slot ctx elem in
let h = fresh_slot ctx hty in
let attempt =
rt loc (Types.Int Types.I8) "flan_pool_insert"
[ target; addr_of loc (mk loc elem (Tast.Local e));
addr_of loc (mk loc hty (Tast.Local h));
size_of loc elem; align_of loc elem; here loc ]
in
expect loc ~want
(mk loc hty
(Tast.Let ([ (e, x); (h, mk loc hty (Tast.Zero hty)) ],
[ alloc_guard ctx loc attempt;
mk loc hty (Tast.Local h) ])))
| _ -> assert false)
(* (resolve p h) -> (Option (Ptr T)).
A pointer and not a value, and spec-memory.md settles it rather than this
lane guessing: its worked example under "Mutating something you matched"
is written out as (Option (Ptr Enemy)), for the reason stated a line
above it "pattern bindings bind values, so a matched struct is a copy",
and a copy cannot be written back. Mutating the pooled thing in place is
what a pool is for, so (Option T) would answer a question nobody asked.
An [Option] rather than a trap because the whole thesis is that a stale
reference *reports* the same shape (get m k) has, and for the same
reason: absence is an answer, not a failure.
The hole, said plainly: the (Ptr T) is invalidated by any [insert] that
grows the pool, exactly as a slice is invalidated by a [push]. The handle
survives that and the pointer does not. It is spec-memory.md's explicit
Zig/Odin contract one level down, and it is worth naming because it is
the silent-wrong-answer mode the handle just removed, reintroduced for
anyone who keeps the pointer across an insert. Chunked never-moving
storage is the fix and it costs code; taking the contract is the smaller
correct thing, given [as-slice] already established it. *)
| "resolve" ->
arity loc name 2 args;
(match args with
| [ target; h ] ->
let target = borrowed ctx target (fun () -> 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
| Types.Handle e when Types.equal e elem -> ()
| other ->
fail loc "resolve takes a (Handle %s), found %s"
(Types.to_string elem) (Types.to_string other));
let pty = Types.Ptr elem in
let oty = Types.Option pty in
let out = fresh_slot ctx pty in
let got =
rt loc pty "flan_pool_resolve"
[ target; h; size_of loc elem; here loc ]
in
(* The runtime answers a pointer or NULL and the Option is built here,
which is [get]'s arrangement: the runtime has no idea what an
Option's layout is, and keeping it that way is what lets one entry
point serve every element type. *)
let cond =
mk loc Types.Bool
(Tast.Prim (Tast.Ne,
[ mk loc (Types.Int Types.I64)
(Tast.Prim (Tast.Cast (Types.Int Types.I64),
[ mk loc pty (Tast.Local out) ]));
mk loc (Types.Int Types.I64) (Tast.Int (0L, Types.I64)) ]))
in
let some = mk loc oty (Tast.Some_ (mk loc pty (Tast.Local out))) in
let none = mk loc oty Tast.None_ in
expect loc ~want
(mk loc oty
(Tast.Let ([ (out, got) ],
[ mk loc oty (Tast.If (cond, some, none)) ])))
| _ -> assert false)
(* (release p h) -> bool: true if this call released it, false if the handle
was already gone.
This is how a pooled value dies, and it is not [free]. [free] consumes
its argument as a move, and a handle is a copyable number that owns
nothing consuming one copy would say nothing about the others. The pool
is the owner, so the release operation is on the pool and takes the
handle as an ordinary argument. spec-memory.md's two release points are
untouched: (free p) is release point 1 applied to the owner, and a
free-all of the region takes the pool with everything else. This is a
third thing and it is not a release point it recycles a slot inside
storage the pool still owns.
It answers a bool rather than () because the generational scheme makes a
double release *detectable*, which is worth handing to the caller: this
is the one place in the language where freeing something twice is an
answer instead of a refusal. *)
| "release" ->
arity loc name 2 args;
(match args with
| [ target; h ] ->
let target = borrowed ctx target (fun () -> 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
| Types.Handle e when Types.equal e elem -> ()
| other ->
fail loc "release takes a (Handle %s), found %s"
(Types.to_string elem) (Types.to_string other));
let got = rt loc (Types.Int Types.I8) "flan_pool_release"
[ target; h; here loc ] in
expect loc ~want
(mk loc Types.Bool
(Tast.Prim (Tast.Ne,
[ got;
mk loc (Types.Int Types.I8) (Tast.Int (0L, Types.I8)) ])))
| _ -> assert false)
(* (live p) — how many slots are live now. (len p) is the *slot high-water*,
which is deliberately the other number: 0..(len p) are the indices
(pool-handle p i) accepts, so a loop bounded by [len] visits every live
entry. Bounding it by the live count instead would silently skip entries
the moment anything had been released, which is precisely the kind of
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
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 ])))
(* (pool-handle p i) -> (Option (Handle T)): the handle of slot [i], or None
if that slot is dead. This plus (len p) is the whole of iteration, and
iteration is not a convenience migrate-instances has to *enumerate*
live instances, and a pool behind generational handles gives that by
construction where a world arena and an owned region do not. It is the
reason plan.org's three storage strategies are not a free choice.
An index out of 0..(len p) traps, exactly as (at v i) traps: an index is
an index here, and answering None for one would hide a bug rather than a
death. *)
| "pool-handle" ->
arity loc name 2 args;
(match args with
| [ target; i ] ->
let target = borrowed ctx target (fun () -> 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
let oty = Types.Option hty in
let out = fresh_slot ctx hty in
let got = rt loc hty "flan_pool_handle" [ target; i; here loc ] in
(* 0 is the never-valid handle — generation 0 is even, and a live slot's
generation is odd so the runtime says "dead" with it and needs no
second return value. *)
let cond =
mk loc Types.Bool
(Tast.Prim (Tast.Ne,
[ mk loc (Types.Int Types.I64)
(Tast.Prim (Tast.Cast (Types.Int Types.I64),
[ mk loc hty (Tast.Local out) ]));
mk loc (Types.Int Types.I64) (Tast.Int (0L, Types.I64)) ]))
in
expect loc ~want
(mk loc oty
(Tast.Let ([ (out, got) ],
[ mk loc oty
(Tast.If (cond,
mk loc oty (Tast.Some_ (mk loc hty (Tast.Local out))),
mk loc oty Tast.None_)) ])))
| _ -> assert false)
(* ── (Map K V), spec-memory.md ─────────────────────────────────── *)
(* Every one of these is a named call over the same type-erased runtime the
Vec uses, with the two sizes and the key's hash and equality pair produced
@ -3347,9 +3615,16 @@ and named_call ctx ~want loc name args =
| Types.Map _ ->
let n = rt loc (Types.Int Types.I64) "flan_map_len" [ a; here loc ] in
expect loc ~want (mk loc index_ty (Tast.Prim (Tast.Cast index_ty, [ n ])))
(* A pool's [len] is its slot high-water, not its live count, so that
0..(len p) stays the range of valid indices the way it is for every
other container here. (live p) is the other number. *)
| Types.Pool _ ->
let n = rt loc (Types.Int Types.I64) "flan_pool_len" [ a; here loc ] in
expect loc ~want (mk loc index_ty (Tast.Prim (Tast.Cast index_ty, [ n ])))
| other ->
fail loc
"len takes an array, a slice, a string, a Vec or a Map, found %s"
"len takes an array, a slice, a string, a Vec, a Map or a Pool, \
found %s"
(Types.to_string other))
| "at" ->
(match args with

View File

@ -1907,7 +1907,14 @@ and cast f (x : Tast.expr) target =
the REPL's renderer needs an enum's number when it falls outside the
declared members. *)
let concrete (t : Types.t) =
match t with Types.Enum _ -> Types.Int Types.I32 | t -> t
match t with
| Types.Enum _ -> Types.Int Types.I32
(* A handle already *is* an i64 — see [ll] — so a cast involving one
changes the reading and never the bits. [pool-handle] tests one against
the never-valid zero, and the renderer splits one into its index and
its generation. Unsigned, because both halves are. *)
| Types.Handle _ -> Types.Int Types.U64
| t -> t
in
let src = concrete x.Tast.ty and target = concrete target in
if Types.equal src target then v
@ -1928,6 +1935,10 @@ and cast f (x : Tast.expr) target =
holds and under opaque pointers there is no instruction to emit for
it, both sides being [ptr]. *)
| Types.Ptr _, Types.Ptr _ -> "bitcast"
(* Also not written in the surface language. [resolve] needs it: the
pool answers a pointer or NULL and the Option is built in the
checker, so the null test is one integer compare on the address. *)
| Types.Ptr _, Types.Int Types.I64 -> "ptrtoint"
| _ -> failwith "unsupported cast"
in
if op = "bitcast" then v
@ -2347,6 +2358,18 @@ declare i64 @flan_vec_len(ptr, ptr, i64)
declare ptr @flan_vec_at(ptr, i32, i64, ptr, i64)
declare void @flan_vec_as_slice(ptr, ptr, i32, i32, i64, ptr, i64)
declare void @flan_vec_free(ptr, i64, i64, ptr, i64)
; (Pool T) and (Handle T). A handle crosses as the i64 it is; the pool, like
; every other owning container, crosses as its address. [resolve] answers a
; pointer or null and [pool-handle] answers a packed handle or the never-valid
; zero, so neither needs a second return value.
declare i8 @flan_pool_init(ptr, ptr, i64, i64, ptr, i64)
declare i8 @flan_pool_insert(ptr, ptr, ptr, i64, i64, ptr, i64)
declare ptr @flan_pool_resolve(ptr, i64, i64, ptr, i64)
declare i8 @flan_pool_release(ptr, i64, ptr, i64)
declare i64 @flan_pool_len(ptr, ptr, i64)
declare i64 @flan_pool_live(ptr, ptr, i64)
declare i64 @flan_pool_handle(ptr, i32, ptr, i64)
declare void @flan_pool_free(ptr, i64, i64, ptr, i64)
; (Map K V). The two ptr arguments before the location on put/get/clone are the
; hash and equality pair, which the checker emits per key type and passes here
; the way Odin hangs them off Map_Info.

View File

@ -122,6 +122,28 @@ let rec render c depth (e : Tast.expr) : Tast.expr list =
does not own, and the walk is what [as-slice] is for: (print (as-slice
v)) prints the elements and says at the call site that it borrowed. *)
| Types.Vec _ -> [ lit "<vec>" ]
(* Opaque for the reason a Vec is: the slots are storage this function does
not own, and a walk over them would print the dead ones too there is
no way to say "dead" inside a rendered element. (pool-handle p i) and
(resolve p h) are how a program looks, and they say it. *)
| Types.Pool _ -> [ lit "<pool>" ]
(* Its identity, which is what spec-memory.md says a handle prints —
"Ptr and Handle print their address or identity rather than recursively
dereferencing". Shown as index:generation rather than as the packed
number, because those are the two things a reader is trying to tell
apart when two handles disagree. *)
| Types.Handle _ ->
let h = cast (Types.Int Types.U64) e in
let u64 v = { Tast.e = v; ty = Types.Int Types.U64; loc } in
let idx =
u64 (Tast.Prim (Tast.BitAnd,
[ h; u64 (Tast.Int (0xFFFFFFFFL, Types.U64)) ]))
in
let gen =
u64 (Tast.Prim (Tast.Shr, [ h; u64 (Tast.Int (32L, Types.U64)) ]))
in
[ do_ [ lit "<handle "; c.emit.eu64 idx; lit ":"; c.emit.eu64 gen;
lit ">" ] ]
(* A function value is a code address, and printing the address would make
an inspection depend on where the image loaded. The signature is what a
reader can act on, so that is what is shown and the inspector reaches

101
test/programs/handles.flan Normal file
View File

@ -0,0 +1,101 @@
;;;; (Handle T) and (Pool T), spec-memory.md — "Cross-referencing long-lived
;;;; objects uses (Handle a) into a pool, never a raw pointer or slice. A
;;;; stale handle is detectable."
;;;;
;;;; The thesis, in one program: something holds a reference to an entity; the
;;;; entity dies; the slot is reused by a different entity; and the old
;;;; reference answers "gone" instead of answering wrong. Every other case
;;;; here is secondary to that one.
;;;;
;;;; It is all one function because a Pool is move-only exactly as a Vec is,
;;;; so passing one to a helper *consumes* it — there is no borrowing
;;;; parameter in the language yet. That is not a pool question and this
;;;; program does not work around it; see BUILT.md.
(defstruct Enemy [hp i32 kind i32])
;; The projectile does not hold an Enemy and does not hold an index. It holds
;; a handle, which is a number that owns nothing and copies freely — which is
;; why a struct may contain one where it may not contain a Vec.
(defstruct Projectile [target (Handle Enemy) damage i32])
(defn main [] i32
(let [pool (pool-new Enemy)]
(let [a (insert pool (Enemy {.hp 10 .kind 1}))
b (insert pool (Enemy {.hp 20 .kind 2}))
c (insert pool (Enemy {.hp 30 .kind 3}))
sum 0]
(println (len pool)) ; 3 slots handed out
(println (live pool)) ; 3 of them live
;; Enumeration, which is what a world arena and an owned region do not
;; give and which migrate-instances will need. (len p) is the slot
;; high-water, so 0..(len p) visits every slot ever handed out, and
;; (pool-handle p i) says which of them are still live.
(dotimes [i (len pool)]
(match (pool-handle pool i)
(Some h) (match (resolve pool h)
;; resolve yields a *pointer*, not a copy: mutating the
;; pooled thing in place is what a pool is for, and a
;; pattern binding binds a value.
(Some e) (set sum (+ sum (.hp e)))
None (do))
None (do)))
(println sum) ; 60
;; A write through a resolved pointer is a write to the pooled entity.
(match (resolve pool b)
(Some e) (set (.hp e) 21)
None (do))
(match (resolve pool b)
(Some e) (println (.hp e)) ; 21
None (println -1))
;; ── The thesis ────────────────────────────────────────────────
;; A projectile chasing b. b dies. The slot is reused by a fourth
;; enemy, which lands in exactly that slot — and the projectile's
;; handle says so rather than chasing the newcomer.
(let [shot (Projectile {.target b .damage 5})]
(println (release pool b)) ; true — this call released it
(println (release pool b)) ; false — it was already gone
(println (live pool)) ; 2
(let [d (insert pool (Enemy {.hp 99 .kind 4}))]
;; Printed as index:generation. Same slot, later generation — the
;; two halves of the answer, visible.
(println b)
(println d)
(println (= d b)) ; false
(println (= d d)) ; true
(match (resolve pool (.target shot))
(Some e) (println (.hp e))
None (println -1)) ; -1, not 99
(match (resolve pool d)
(Some e) (println (.hp e)) ; 99
None (println -1))
(println (len pool)) ; still 3 slots
(println (live pool)) ; 3 live
;; A zeroed handle is generation 0, which is even, and a live slot's
;; generation is always odd — so ZII gives a handle field the right
;; meaning for free rather than pointing it at slot 0.
(let [z (Projectile {.damage 1})]
(println (.target z))
(match (resolve pool (.target z))
(Some e) (println (.hp e))
None (println -1))) ; -1
;; a and c are untouched by any of it.
(match (resolve pool a)
(Some e) (println (.hp e)) ; 10
None (println -1))
(match (resolve pool c)
(Some e) (println (.hp e)) ; 30
None (println -1))
;; spec-memory.md's first release point, applied to the owner. Every
;; handle into it is stale afterwards and says so — which is a
;; better afterlife than a freed Vec's binding gets, that one being
;; a compile error the checker can see and this one an answer it
;; cannot.
(free pool)
0)))))