The defining form is fixed at build time, all three of them

The first cut of the form-change refusal asked only about def and defonce
and asserted in its comment that defconst was another arm's business. It
was not: defconst to def at the same type fell past every arm, and defonce
to defconst fell past them into the consts republish, which stores the
declared value over live storage at the frame boundary. One refusal over
gconst and grerun together now covers all six directions.

And two coverage gaps closed by running rather than reasoning: reload-v6
carries a (def dial i64 5) the host was never built with, so the x86 image
path executes and its 5 shows in the transcript's arithmetic; dev-rerun's
echo reads counter in its initialiser and follows it 40, 41, 42, 43 across
re-runs, where a captured first answer would print 40 four times.

FIX.org

@@ -4430,6 +4430,16 @@ by the suite:
   never re-ran, and def→defonce kept re-running. [Session.compatible]
   refuses both ways now and says to restart. Editing the *value* is the
   workflow and stays allowed, which is the row beside it.
+- *Swapping in or out of defconst was silently accepted, and one direction
+  did damage.* The first cut of the refusal above asked only about the two
+  mutable forms, and claimed in its own comment that a defconst on either
+  side was another arm's business. It was not: [defconst x] → [def x] at the
+  same type fell past every arm, and [defonce x] → [defconst x] fell past
+  them into the [consts] republish, which stores the declared value over the
+  storage at the frame boundary — "edit the code, keep the sand" undone by a
+  keyword. One refusal over [gconst] and [grerun] together now covers all
+  six directions, which is right because it is one fact: the defining form
+  is fixed at build time.
 - *[global/<n>] leaked into a user-facing refusal.* Retyping a def hit the
   function-signature arm first, which answered about [global/paint] — a name
   nothing in the source mentions. The lifted initialiser is skipped there
@@ -4437,10 +4447,13 @@ by the suite:
   act on.
 
 Also covered, having been reasoned rather than exercised: a def whose type
-changes between re-runs (the "changes type" refusal), and a def initialiser
+changes between re-runs (the "changes type" refusal); a def initialiser that
-that reads another global at run time rather than only in the static
+reads another global at run time and re-reads it on each re-run
-ordering analysis (an ordinary republish; the read is the running program's
+(dev-rerun.flan's [echo], which follows [counter] at 40, 41, 42, 43 where a
-storage).
+captured first answer would print 40 four times); and the x86 half of the
+new-global image, which reload-v6.flan now *runs* rather than greps — a
+[(def dial i64 5)] the host was never built with, whose 5 shows up in the
+transcript's arithmetic.
 
 ** Red on this branch, for the merger
 sand.flan spells ~defvar~ at lines 15, 16, 24, 25, 26, 115 and 116 and was

docs/BUILT.md

@@ -6217,8 +6217,10 @@ stayed zero while the `defonce` beside it came up 42. `Emit.initial_image` reads
 body instead, and both backends ask it. And *changing the keyword* on an existing global is refused: which form
 declared it lives in the startup function's guard, which was compiled into the host, so a reload can replace the
 initialiser but not how often it is called — swapping `def` for `defonce` would load cleanly and go on doing what the
-old keyword said. `Session.compatible` names it and says to restart. Editing the *value* is the workflow and stays
+old keyword said. `Session.compatible` names it and says to restart — over all three forms and all six directions, because it is one
-allowed.
+fact, and because the direction *into* `defconst` is worse than ineffective: an unfolded constant is republished by
+value at the frame boundary, so accepting it would store the declared value over live state. Editing the *value* is
+the workflow and stays allowed.
 
 **`uninit` is the one spelling where `def` does not do what its name promises.** `(def buf [8 u8] uninit)` keeps its
 bytes across a re-run, because there is nothing to run: the initialiser that would repaint it is the absence of one.

lib/session.ml

@@ -330,30 +330,48 @@ let compatible ?(origin = fun _ -> None) ?(relaxed = []) ~loc
            "%s changes type, from %s to %s; the running program already laid \
             that storage out. Restart to change it."
            g.Tast.gname (Types.to_string h.Tast.gty) (Types.to_string g.Tast.gty)
-       (* Which of the two mutable forms declared it is not in the storage,
+       (* Which form declared a global is not in the storage, it is in the
-          it is in the *startup function*: [Emit.startup_plan] wrote the
+          code the process was *built* with: [Emit.startup_plan] wrote the
-          [.init~once.] guard around a defonce's store and left a def's bare,
+          [.init~once.] guard around a defonce's store, left a def's bare,
-          and that function was compiled into the host when the process was
+          and gave a defconst no store at all, and that startup function was
-          built. A redefinition republishes the initialiser and cannot
+          compiled into the host when the process started. A redefinition
-          republish the thing that decides how often it is called, so
+          republishes the initialiser and cannot republish the thing that
-          swapping the keyword would load cleanly and then do exactly what
+          decides how often — or whether — it is called. So every swap of the
-          the old keyword said — a def that never re-runs, or a defonce that
+          keyword would load cleanly and then go on doing what the *old*
-          keeps being overwritten — with nothing anywhere saying so. That is
+          keyword said, with nothing anywhere saying so:
-          the silent-wrongness class the house rule is about, so it is a
+
-          refusal with the reason. A defconst on either side is the arm
+          - defonce → def keeps the guard and never re-runs; def → defonce
-          above's business and never reaches here: the type check catches a
+            keeps re-running.
-          retype, and a constant's own arm catches the rest. *)
+          - anything → defconst is worse than ineffective. A constant the
+            checker did not fold is republished by value, at the frame
+            boundary, by the [consts] list below — so the store lands on
+            storage holding live state the program has long since moved past,
+            which is "edit the code, keep the sand" broken by a keyword.
+          - defconst → anything gets no store at all, because the host's
+            startup has none to run for a name that was an image when it was
+            compiled.
+
+          One refusal over all of it, because it is one fact: the defining
+          form is fixed at build time. Told by [gconst] and [grerun]
+          together, which is exactly how every other pass tells the three
+          apart. The arms above get first say and are the better message
+          where they apply — a folded constant whose value changed, and any
+          retype — and neither is about the keyword. *)
        | Some h
-         when (not h.Tast.gconst) && (not g.Tast.gconst)
+         when h.Tast.gconst <> g.Tast.gconst
-              && h.Tast.grerun <> g.Tast.grerun ->
+              || h.Tast.grerun <> g.Tast.grerun ->
-         let word b = if b then "def" else "defonce" in
+         let word (x : Tast.global) =
+           if x.Tast.gconst then "defconst"
+           else if x.Tast.grerun then "def"
+           else "defonce"
+         in
          fail loc
-           "%s changes from %s to %s. The running program decides when an \
+           "%s changes from %s to %s. The running program was built with the \
-            initialiser runs in its startup function, which was compiled \
+            first one — when an initialiser runs, or whether it runs at all, \
-            when it started — a reload can replace the initialiser but not \
+            is decided in its startup code, and a reload can replace the \
-            that. Restart to change it, or keep %s and edit the value."
+            initialiser but not that. Restart to change it, or keep %s and \
-           g.Tast.gname (word h.Tast.grerun) (word g.Tast.grerun)
+            edit the value."
-           (word h.Tast.grerun)
+           g.Tast.gname (word h) (word g) (word h)
        | _ -> ())
     new_.Tast.globals;
   List.iter

test/programs/dev-rerun.flan

@@ -72,6 +72,15 @@
 ;; initialiser takes effect on C-c C-c plus re-run.
 (def c 3)
 
+;; A def initialiser that *reads another global*, which is a claim the static
+;; ordering analysis cannot make: the lifted function loads [counter] when it
+;; runs, and it runs again on every re-run, so this follows the value the last
+;; run left rather than the value the first startup saw. [counter] is a
+;; defonce that climbs 41, 42, 43, 44, and the startup store lands before main
+;; increments it — so this prints 40, 41, 42, 43, one behind, and a def that
+;; had captured its initialiser's first answer would print 40 four times.
+(def echo i64 (+ counter 0))
+
 ;; The typed-array spelling of the same form. The re-run repaints the same
 ;; storage — no reallocation — so the element main increments is 7 again by
 ;; the time it is read: 8 on every run, never 9.
@@ -97,6 +106,7 @@
   (print "grid-far ") (print (i32 (at grid 1 2))) (println "")
   (print "base ") (print base) (println "")
   (print "c ") (print c) (println "")
+  (print "echo ") (print echo) (println "")
   (print "hue ") (print (i32 (at hues 0))) (println "")
   ;; Long enough for a client to be served, short enough to park well inside
   ;; any watchdog — dev-macro.flan's clock, for its reason.

test/programs/reload-v6.flan

@@ -4,14 +4,24 @@
 ;;;; not its initial value travelled with the module. [tuning] is 42, and the
 ;;;; transcript is the number the host prints, so an image that never arrived
 ;;;; prints 4 rather than 88.
+;;;; [dial] is the same claim for the other mutable form, and it is the one
+;;;; that needs saying: every def initialiser is lifted into [global/<n>] so
+;;;; that re-evaluating the form can swap it through a cell, which means a
+;;;; def's own [ginit] is a *call* and never a constant. A backend that asked
+;;;; [Tast.const_init] about it — both of them did — would send a null image
+;;;; and this global would be 0 for the life of the process, with no startup
+;;;; in the host to ever put 5 there. [Emit.initial_image] reads the constant
+;;;; back out of the lifted body, and this transcript is the x86 backend
+;;;; running that answer rather than a disassembly agreeing with it.
 (defonce counter i64)
 (defonce tuning i64 42)
+(def dial i64 5)
 
 (defn helper [x i64] i64 (* x 2))
 
 (defn bump [] i64
   (println "v6")
-  (set counter (+ counter tuning 1))
+  (set counter (+ counter tuning dial 1))
   (helper counter))
 
 (defn outer [] i64 (bump))

test/test_dev.ml

@@ -5559,7 +5559,13 @@ let () =
           "c 4";
           (* The typed-array [def]: the fill repaints the same storage, so
              the element every run increments reads 8 every run. *)
-          "hue 8" ]
+          "hue 8";
+          (* A def initialiser that reads another global, re-read on each
+             re-run: [counter] is 43 when the fourth run's startup stores
+             this, and main increments it to 44 afterwards. A def that had
+             captured its first answer would print 40 on all four runs —
+             which is the claim the static ordering analysis cannot make. *)
+          "echo 43" ]
       in
       List.iter
         (fun s ->

test/test_reload.ml

@@ -277,7 +277,14 @@ let () =
        the allocation the first time the name is interned and ignores it every
        time after. [extra] is declared zero here, which calloc would also give,
        so the case is asserted where it is visible -- a run-time-new global
-       with a value of its own. *)
+       with a value of its own.
+
+       [dial] is the def twin of that claim and is x86's only *execution* of
+       [Emit.initial_image]'s second arm: a def's initialiser is always
+       lifted, so its [ginit] is a call and the old [Tast.const_init] test
+       sent a null image, leaving a brand-new def zero for the life of the
+       process. 5 rather than 0 is the whole of the difference, and it is in
+       the number below rather than in a disassembly. *)
     let p6 = checked "programs/reload-v6.flan" in
     let xso6 = xmodule p6 [ "bump" ] "xv6.so" in
     let xhost6 = tmp "xhost6" in
@@ -292,7 +299,10 @@ let () =
            (Filename.quote (tmp "xerr6")))
     in
     let xtext6 = In_channel.with_open_bin xout6 In_channel.input_all in
-    let xwant6 = "v1\nhost 2\nv6\nafter1 88\ncounter 44\n" in
+    (* counter is 1 after the host's own call, then tuning 42 + dial 5 + 1.
+       A null image for either new global shows here: 44 without [dial]'s 5,
+       and 7 without [tuning]'s 42. *)
+    let xwant6 = "v1\nhost 2\nv6\nafter1 98\ncounter 49\n" in
     if xcode6 <> 0 || xtext6 <> xwant6 then
       fail "x86 reload of a new global with a value\n        \
             got: %S (exit %d)\n     wanted: %S" xtext6 xcode6 xwant6;

test/test_session.ml

@@ -335,6 +335,26 @@ let () =
    | exception Loc.Error { Loc.dmsg = m; _ } ->
      if not (has m "paint changes from def to defonce") then
        fail "the def-to-defonce refusal says: %s" m);
+  (* The constant is the third form and the same fact, and the direction
+     into it is the one that does damage rather than nothing: a constant the
+     checker never folded is republished *by value* at the frame boundary, so
+     accepting this would store 7 over storage holding whatever the running
+     program has put there since — "edit the code, keep the sand" undone by a
+     keyword. The other direction gets no store at all, because the host's
+     startup has none for a name that was an image when it was compiled. *)
+  (match Session.eval t "(defconst paint i64 7)" with
+   | _ -> fail "def became defconst without a word"
+   | exception Loc.Error { Loc.dmsg = m; _ } ->
+     if not (has m "paint changes from def to defconst") then
+       fail "the def-to-defconst refusal says: %s" m);
+  (* [palette] is the host's *unfolded* constant — the one a dev build emits
+     as mutable storage and the [consts] list republishes — so it is exactly
+     the one where the form change would reach live bytes. *)
+  (match Session.eval t "(defonce palette [2 u32] [1 2])" with
+   | _ -> fail "defconst became defonce without a word"
+   | exception Loc.Error { Loc.dmsg = m; _ } ->
+     if not (has m "palette changes from defconst to defonce") then
+       fail "the defconst-to-defonce refusal says: %s" m);
   (* Editing the *value* of a def is the workflow and stays allowed: same
      form, same type, a new initialiser, and the lifted [global/paint]
      republished through its cell so the next re-run stores the edited value.