A move-only global is borrowed, never moved

lib/check.ml

@@ -1758,7 +1758,9 @@ and var ctx loc ~want name =
       expect loc ~want (mk loc b.bty (Tast.Local b.slot))
     | None ->
       match Hashtbl.find_opt ctx.env.globals name with
-      | Some (ty, _) -> expect loc ~want (mk loc ty (Tast.Global name))
+      | 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
         (* A case with no fields is a whole value on its own, so it is written
@@ -1820,6 +1822,46 @@ and moved ?ty ctx loc name slot =
    | 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
+    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), a pointer with (addr %s), or an \
+       independent copy with (clone %s), which is the one of these that \
+       something else may own"
+      name (Types.to_string ty) name name name name name name name 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
@@ -5548,22 +5590,63 @@ and check_generic env (fn : Ast.fn) =
    checking a function. *)
 let () = check_fn_ref := check_fn
 
-(* A global of move-only type is refused. The dead set is per function, so two
+(* A global of move-only type is legal, and what makes it legal is [var]'s
-   functions each freeing the same global is a double free nothing here could
+   refusal rather than anything here: reading one is always a borrow, so no
-   see; and within one function a global read does not go through [var]'s move
+   function can take it, and none can free it. See [global_borrow] for why that
-   path at all, so even the local case would be accepted. Rather than half a
+   one sentence is enough where a general ownership model would not be.
-   rule, the type is refused where it is declared. A global *Allocator* is not
+
-   this — an allocator is a copyable opaque handle — which is what makes the
+   What this pass still decides is how such a global may be *started*, and the
-   handler-owns-the-arena shape in exhausted.flan expressible. *)
+   answer is zeroed and nothing else. A zeroed Vec is a real empty Vec — null
-let no_move_only_global loc n (ty : Types.t) =
+   block, zero length, zero capacity — so the ZII value is the value a program
-  no_zeroed_fn loc (Printf.sprintf "the global %s" n) ty;
+   would have written anyway, and filling it is an ordinary (set g (slurp
+   "...")) in whichever function loads it. The alternative, a computed
+   initialiser, does not exist to be relaxed into: [Emit.const] says so in as
+   many words ("there is no init-at-startup path, by design"), and the backend
+   that does run initialisers at startup, [x86.ml], runs them from .init_array
+   before main and deliberately omits them from a reload module, because
+   re-running one would wipe the live state reloading exists to preserve. A
+   rule that held on one backend and not the other would not be a rule.
+
+   That fits what a runtime-loaded global is for. The data is loaded by
+   whoever loads it, once, and it outlives main: a main that returns and is
+   entered again finds the global exactly as it left it, because nothing
+   between the two runs touches it. Assigning a second time overwrites the
+   first block and leaks it — there is no [drop] and no cross-function flow
+   analysis that could see the second assignment, so that is the manual-memory
+   answer and the language's own: free is a thing you write.
+
+   A global *Allocator* is not any of this — an allocator is a copyable opaque
+   handle — which is what makes the handler-owns-the-arena shape in
+   exhausted.flan expressible. *)
+let move_only_global_init loc n (ty : Types.t) (init : Ast.init) =
+  if Types.is_move_only ty then
+    match init with
+    | Ast.Zeroed -> ()
+    | _ ->
+      fail loc
+        "the global %s is %s, which is move-only, and a move-only global \
+         starts zeroed: a global's initialiser is a compile-time constant and \
+         %s is not one. Write (defvar %s %s) with no initialiser — a zeroed \
+         %s is an empty one, and that is a value, not a placeholder — then \
+         load it with (set %s ...) in the function that loads it, which runs \
+         once and whose result outlives every call to main"
+        n (Types.to_string ty)
+        (match init with Ast.Uninit -> "uninit" | _ -> "this initialiser")
+        n (Types.to_string ty) (Types.to_string ty) n
+
+(* A move-only global has to be a [defvar]. A [defconst] is not an assignable
+   place — [check_place] refuses one by name — so a constant Vec could only
+   ever hold the zeroed value it was declared with, and nothing could ever put
+   the file's bytes in it. Refused here, where the fix is one keyword, rather
+   than at the (set ...) that discovers it three forms later. *)
+let no_move_only_defconst loc n (ty : Types.t) =
   if Types.is_move_only ty then
     fail loc
-      "the global %s is %s, which is move-only, and ownership of a global \
+      "the global %s is %s, which is move-only, and a move-only global is a \
-       cannot be tracked: the dead set is per function, so two functions each \
+       defvar and not a defconst: a constant is not an assignable place, so \
-       freeing it is a double free nothing would catch. Hold it in a local and \
+       nothing could ever load this one — it would stay the empty %s it was \
-       pass it, or hold the allocator globally instead"
+       declared as. Write (defvar %s %s) and fill it in a function"
-      n (Types.to_string ty)
+      n (Types.to_string ty) (Types.to_string ty) n (Types.to_string ty)
 
 let check_global env (d : Ast.decl) : Tast.global option =
   let ctx () = { env; ret = Types.Unit; slots = 0; slot_tys = []; slot_names = []; scope = []; defers = [];
@@ -5571,7 +5654,8 @@ let check_global env (d : Ast.decl) : Tast.global option =
   match d.Ast.d with
   | Ast.Defvar (n, _, init) ->
     let ty, _ = Hashtbl.find env.globals n in
-    no_move_only_global d.Ast.dloc n ty;
+    no_zeroed_fn d.Ast.dloc (Printf.sprintf "the global %s" n) ty;
+    move_only_global_init d.Ast.dloc n ty init;
     let ginit =
       match init with
       | Ast.Zeroed -> { Tast.e = Tast.Zero ty; ty; loc = d.Ast.dloc }
@@ -5601,7 +5685,8 @@ let check_global env (d : Ast.decl) : Tast.global option =
     Some { Tast.gname = n; gty = ty; ginit; gconst = false; gfolded = false }
   | Ast.Defconst (n, _, v) ->
     let ty, _ = Hashtbl.find env.globals n in
-    no_move_only_global d.Ast.dloc n ty;
+    no_zeroed_fn d.Ast.dloc (Printf.sprintf "the global %s" n) ty;
+    no_move_only_defconst d.Ast.dloc n ty;
     (* [collect] already folded the integer constants, because an array length
        has to be known before any type resolves. Use that value here rather
        than the expression it came from: a global's initialiser has to be a

spec-memory.md

@@ -42,8 +42,9 @@ Equality and hashing for those keys are compiler-provided structural operations
 and not type classes. They are not available to an unconstrained type variable
 either; a variable that means to key a map declares `hashable?` in the signature
 that binds it, and the refusal then lands at the call site that names an
-unhashable key. An empty map names its key and value types, because a global
+unhashable key. An empty map names its key and value types, because the position
-cannot hold one and there is therefore no declaration for it to take a type from:
+it is usually written in — a `let` binding — has no type slot for it to take
+them from:
 
 ```
 (let [enemies (map-new string Enemy)]
@@ -88,6 +89,41 @@ once — and a type with one cannot be `clone`d.
 - Cross-referencing long-lived objects uses `(Handle a)` into a pool, never a
   raw pointer or slice. A stale handle is detectable.
 
+## 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.
+
+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
+it stands. The aliasing contract is the one above and nothing more — a push that
+reallocates invalidates a slice taken before it, and that is the programmer's
+whether the owner is a local or a global. Globals get no borrow rule locals do
+not have; the dev build's generation word lives on the `Vec`, so the stale-slice
+trap works the same either way.
+
+A move-only global **starts zeroed** — a zeroed `Vec` is an empty `Vec` — and is
+loaded by whichever function loads it, with an ordinary assignment:
+
+```
+(defvar the-data (Vec u8))
+(defn load [] () (set the-data (slurp "game-data.edn")))
+```
+
+A computed initialiser on the declaration is refused: a global's initialiser is
+a link-time constant, and the load has to be something the program does rather
+than something that happens before `main`. That is also what makes the data
+outlive `main` — nothing re-runs between one entry and the next, so a re-entered
+`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.
+
 ## Taking an address
 
 `(addr x)` yields `(Ptr T)` for any assignable place `x` — a local, a global, a

test/programs/reload-v2.flan

@@ -15,6 +15,7 @@
 ;;;; host's [* x 2]; with the two bodies identical nothing at run time would
 ;;;; notice a module that grew its own copy.
 (defvar counter i64)
+(defvar tally (Vec u8))
 
 (defn helper [x i64] i64 (* x 3))
 

test/programs/reload-v3.flan

@@ -9,6 +9,12 @@
 ;;;; is a module referring to storage that does not exist yet.
 (defvar counter i64)
 (defvar extra i64)
+;;; And a run-time-new one of move-only type: no symbol to bind to, so it goes
+;;; through the by-name registry like [extra], with its declared initial value
+;;; travelling along as a constant. A zeroed Vec is an empty Vec, so that
+;;; constant is a zeroinitializer and the allocation the registry makes is a
+;;; usable Vec rather than a placeholder.
+(defvar fresh (Vec u8))
 
 (defn helper [x i64] i64 (* x 2))
 

test/programs/reload.flan

@@ -12,6 +12,15 @@
 ;;;; its own constants, and a one-function module usually has none.
 (defvar counter i64)
 
+;;; A move-only global, which is allowed because reading one is always a borrow
+;;; (spec-memory.md, "Globals of move-only type"). It is here for the reload
+;;; question rather than the ownership one: a redefinition module declares it
+;;; [external] like any other host global, so a load must not hand the module
+;;; its own zeroed header -- that would drop the storage the running process is
+;;; still using, which is the failure a plain i64 counter cannot exhibit
+;;; because a re-zeroed i64 merely looks wrong.
+(defvar tally (Vec u8))
+
 ;;; Unused, and that is the point: the session's compatibility rules only get a
 ;;; chance to speak about a change the *checker* accepts, and retyping a var
 ;;; something else reads is an ordinary type error long before it is a layout

test/programs/vec-global.flan

@@ -1,9 +1,58 @@
-;;;; A global of move-only type. The dead set is per function, so two functions
+;;;; A global of move-only type, which is allowed, and the one rule that makes
-;;;; each freeing this is a double free nothing here could see — and a global
+;;;; it allowed: reading a global Vec is always a borrow and never a move. The
-;;;; read does not go through the move path at all, so even the one-function
+;;;; lifetime question ownership tracking exists to answer has a constant
-;;;; case would be accepted. Half a rule is worse than none, so the type is
+;;;; answer here — the process's — so nothing may take the global and nothing
-;;;; refused where it is declared. A global *Allocator* is a different thing
+;;;; may free it, and with no owner to hand over there is no double free to
-;;;; and is allowed: an allocator is a copyable opaque handle.
+;;;; catch. The refusals that enforce that are in test_flan.ml.
-(defvar everything (Vec i32))
+;;;;
+;;;; A zeroed Vec is a real empty Vec, so the global starts as one and is
+;;;; loaded by whoever loads it. What this program pins is that the loading
+;;;; happens once and survives: [entry] is called twice, the way a re-entered
+;;;; main would be, and the second call finds the data the first one left.
+(defvar the-data (Vec u8))
+(defvar counts (Map u8 i64))
 
-(defn main [] i32 0)
+;; Reading it here is a borrow. So is reading it in [total] below, which is the
+;; case the old rule could not express: two functions holding the same global
+;; at once is fine exactly because neither of them can free it.
+(defn loaded? [] bool (> (len the-data) 0))
+
+(defn load [] ()
+  (when (not (loaded?))
+    (set the-data (vec-new u8))
+    (dotimes [i 5] (push the-data (u8 (* i 3))))))
+
+(defn total [] i64
+  (let [s (i64 0)]
+    (dotimes [i (len the-data)] (set s (+ s (i64 (at the-data i)))))
+    s))
+
+;; Mutating in place, through the global rather than through a copy of it. The
+;; aliasing contract is the one every Vec has (spec-memory.md, "Borrowing"): a
+;; push may reallocate and invalidate a slice taken before it, and that is the
+;; programmer's, here as much as for a local.
+(defn bump [] ()
+  (set (at the-data 0) (+ (at the-data 0) 1))
+  (push the-data 100))
+
+(defn entry [] ()
+  (load)
+  (bump)
+  (put counts 1 (total))
+  (println (len the-data))
+  (println (total))
+  (match (get counts 1) (Some v) (println v) None (println "?")))
+
+(defn main [] i32
+  (entry)
+  ;; The second run. Nothing re-initialises the global between them, so the
+  ;; length keeps climbing and the loaded data is the same block it was.
+  (entry)
+  (println (len (as-slice the-data)))
+  ;; A copy is the one thing something else may own, and freeing that copy
+  ;; leaves the global untouched.
+  (let [c (clone the-data)]
+    (println (len c))
+    (free c))
+  (println (len the-data))
+  0)

test/test_acceptance.ml

@@ -117,6 +117,15 @@ let () =
     outputs "value semantics" "programs/values.flan" values_out;
     outputs "machine surface" "programs/machine.flan" machine_out;
     outputs "unit main exits 0" "programs/unit-main.flan" "ok\n";
+    (* A global of move-only type, which this compiler used to refuse outright.
+       What the numbers assert is the half of the rule no checker test can: the
+       global is loaded once and *stays* loaded across a second entry, which is
+       what a re-entered main needs, and the mutations land on the global
+       itself rather than on a copy of its header — the second run's length is
+       the first run's plus one, and the count after cloning and freeing the
+       clone is still the global's. *)
+    outputs "a global Vec" "programs/vec-global.flan"
+      "6\n131\n131\n7\n232\n232\n7\n7\n7\n";
     (* (array COUNT TYPE). Every line of it is a [let] binding, which is the
        one position with no type slot and the whole reason the form exists. *)
     outputs "array constructor" "programs/array-ctor.flan" "4\n0\n7\n9\n4\n";
@@ -1755,14 +1764,14 @@ let () =
        there is nothing to infer from — and guessing is the alternative. *)
     refuses "vec-new with nothing saying what of" "programs/vec-untyped.flan"
       "write the element type";
-    (* The three shapes ownership is not transitive through yet. Each is
+    (* The two shapes ownership is not transitive through yet. Each is refused
-       refused where it is declared, naming drop as what it waits on, rather
+       where it is declared, naming drop as what it waits on, rather than
-       than accepted into a path that would copy a header and hand out a
+       accepted into a path that would copy a header and hand out a second
-       second owner. *)
+       owner. A global used to be the third; it is not any more, and the
+       program that was this row is now an accepted one — see "a global Vec"
+       above, and [Check.global_borrow] for the rule that replaced it. *)
     refuses "a struct field that owns a Vec" "programs/vec-in-struct.flan"
       "a struct that owns one is move-only too";
-    refuses "a global Vec" "programs/vec-global.flan"
-      "the dead set is per function";
     refuses "a Vec of a Vec" "programs/vec-of-vec.flan"
       "copies and releases elements bytewise";
     (* And it does not cross to C: the shim would flatten a header that owns

test/test_flan.ml

@@ -956,6 +956,47 @@ let () =
      for the same reason: the runtime copies and releases slots bytewise. *)
   rejects_check "a pool of a Vec"
     "(defn f [x (Pool (Vec i32))] ())" ~needle:"move-only element";
+
+  (* ── 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";
+  (* 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
+     never be assigned, so nothing could ever load it. Both name the (defvar g
+     (Vec u8)) that works, which is the point of refusing them here rather
+     than letting the backend say "this one is computed" three passes later. *)
+  rejects_check "a global Vec with a computed initialiser"
+    "(defvar g (Vec u8) (slurp \"game-data.edn\")) (defn f [] ())"
+    ~needle:"starts zeroed";
+  rejects_check "a move-only global as a defconst"
+    "(defconst g (Vec u8) (slurp \"game-data.edn\")) (defn f [] ())"
+    ~needle:"a defvar and not a defconst";
+  (* The borrows, which are what is left once ownership is off the table: a
+     global Vec is read, mutated in place, viewed and copied, and the copy is
+     the one thing something else may own. *)
+  accepts "a global Vec is borrowed, mutated and cloned"
+    "(defvar g (Vec u8)) \
+     (defn f [] () (set g (vec-new u8)) (push g 1) (set (at g 0) 2) \
+       (println (len (as-slice g))) (let [c (clone g)] (free c)))";
   (* Ordering handles would order a slot index, which is a free-list artefact.
      Equality is admitted and ordering is not, which is why there are two
      predicates in Types rather than one. *)

test/test_reload.ml

@@ -111,6 +111,13 @@ let () =
     in
     if not (has ir2 "@\"flan.counter\" = external global i64") then
       fail "redefinition defines the global instead of declaring it";
+    (* The same rule for a global of move-only type, where it has teeth the
+       scalar case cannot show. A module that defined [tally] would get a
+       zeroed Vec header of its own, and the block the running process had
+       already filled would be storage nothing points at any more — a leak the
+       reload caused, not the program. A re-zeroed i64 only looks wrong. *)
+    if not (has ir2 "@\"flan.tally\" = external global %vec") then
+      fail "redefinition defines a move-only global instead of declaring it";
     (* In a dev module a sibling is reached only through its cell, so there is
        nothing to declare and a [define] would be a private copy. *)
     if has ir2 "declare i64 @\"flan.helper\"" then
@@ -133,6 +140,15 @@ let () =
       fail "a run-time-new global did not get a slot";
     if has ir3 "@\"flan.extra\" = " then
       fail "a run-time-new global was given storage in the module";
+    (* And a run-time-new global of move-only type, which takes the same path
+       and is the case where the initial value that travels with it has to be
+       a real value rather than a placeholder: a zeroed Vec is an empty Vec,
+       so the registry's allocation is usable the moment it exists. This runs
+       as well as being read — the host loads v3 below. *)
+    if not (has ir3 "@\"flan.gp.fresh\" = internal global ptr null") then
+      fail "a run-time-new move-only global did not get a slot";
+    if has ir3 "@\"flan.fresh\" = " then
+      fail "a run-time-new move-only global was given storage in the module";
     (* Every lookup is resolved before any body is published: publishing first
        exposes a function whose module-local slots are still null to anything
        that calls it. Not race-testable, so it is asserted on the text. *)