The follow-up batch: honest prose, one prefix, one shared label

FIX.org

@@ -952,6 +952,24 @@ Interned and immortal — flan_dyn.c's intern table holds the only copy of each
 name, nothing removes one, and [mark_value] walks BOX_OBJ and nothing else.
 There is no GC object to attribute.
 
+*** Dyn push and put are not marked.
+Added 2026-09-20, from a review: it had only ever been in a test comment.
+[flan_dyn_push] and [flan_dyn_map_set] are not in [Check.memory_class]'s
+table and they provably may allocate — a dyn vector or map growing itself is
+[gc_alloc] on the collector's heap, the same class every other gc row names.
+This is the one row the precision rule does not decide; it is a judgement.
+The unit this pass reports is a line the programmer can act on — crossing
+into dyn is a choice, pushing onto an allocator's Vec is a choice — and a dyn
+container taking a block to hold what was just put in it is the only thing it
+could do. Marking it would squiggle every =(push dv x)= in a program that
+chose dyn, which is the noise the rule exists to keep out. Pinned as a
+negative in test_flan.ml's "collected heap" row, beside the typed push that
+IS marked on the line above it.
+
+The consequence is that the daemon's =:note= cannot claim "every site the
+checker can prove may allocate", and no longer does: lib/dev.ml's memory op
+says what holds and names this exception.
+
 *** The overlays outlive the next command.
 The spec asked for the paths that clear an error overlay. Those hang off
 [pre-command-hook], which takes an overlay down before the next keystroke —
@@ -1077,7 +1095,14 @@ that two mentions of one site share a pointer. Sixty-four sites, and past that
 it stops deduplicating rather than stops warning — the noisy failure, not the
 silent one. The line is:
 
-  flan FILE:LINE:COL: (f64 x) found a dyn holding an int, and converted it to f64 — warned once for this site
+  FILE:LINE:COL: (f64 x) found a dyn holding an int, and converted it to f64 — warned once for this site
+
+The bare =FILE:LINE:COL:= is the house shape for a loc-bearing runtime
+diagnostic — flan_rt.c's bounds, divide-by-zero and null-allocator sentences
+all open that way, and the =flan:= prefix is reserved for the lines that carry
+no location (the leak report at flan_dev.c:1765, the argv failure at
+flan_rt.c:179). An earlier draft of this warning wore =flan= in front of the
+location; it was taken off to match the neighbours.
 
 Both builds warn, dev and release. No precedent was found making a diagnostic
 of this kind dev-only: the allocation registry's notes are the one runtime
@@ -1125,3 +1150,70 @@ sand.flan defines =dyn->f64= and =dyn->u32=, one-line functions whose only
 job is that their parameter slot unboxes. Every call site can now write the
 cast directly — =(f64 d)=, =(u32 d)= — and the two defns deleted. Not done
 here: sand.flan is the author's WIP and this lane did not touch it.
+
+* Follow-ups from the 2026-09-20 reviews
+Small, verified findings the reviews turned up after their lanes had landed.
+Each was re-checked against the tree before it was written or fixed.
+
+** runtime/flan_dyn_stub.c is dead, and the author should decide its fate
+RECOMMENDATION: delete it. Not done here — it is a file the author added and
+removing it is his call, so the facts are written down instead.
+
+*** What it was for, in its own words
+Its header says it plainly: "a standing-in implementation of the flan_dyn.h
+ABI ... THE MERGE REPLACES THIS FILE WITH runtime/flan_dyn.c. It exists so
+that the compiler side of dynamic-by-default can be built and run against the
+fixed ABI before the real runtime lands." The merge it names happened. The
+real runtime is =runtime/flan_dyn.c=, and lib/dune pastes *that* file — not
+this one — into Runtime_src (lib/dune:41, :52).
+
+*** Why it is dead
+- No dune rule mentions it, in lib/dune, runtime/ or test/dune.
+- No .ml refers to it; no test links it; =flan build= never compiles it.
+- The only mentions anywhere are two historical citations in docs —
+  docs/SPIKE-DUPLICITY.md:58 cites a line number in it, and
+  docs/handoffs/HANDOFF-dyn-m1.md:131 explains that the stub verified nothing
+  about root discipline. Both are narrative about a period that has ended;
+  neither gives the file a live job.
+
+*** It does not compile
+Two conflicting-type errors against its own header, both pre-existing and
+neither caught by anything, because nothing builds it:
+
+  clang -c runtime/flan_dyn_stub.c -Iruntime
+  flan_dyn_stub.c:90:  flan_dyn flan_dyn_from_bool(int32_t v)
+    vs flan_dyn.h:68:  flan_dyn flan_dyn_from_bool(uint8_t b);
+  flan_dyn_stub.c:293: int32_t  flan_dyn_need_bool(flan_dyn v)
+    vs flan_dyn.h:145: uint8_t  flan_dyn_need_bool(flan_dyn v);
+
+So the one thing it could still be — a second implementation the header is
+diffed against — is a thing it has already stopped being.
+
+*** The cost of keeping it
+It is maintained by accident: the dyn-cast lane added [flan_dyn_cast_kind] to
+it (flan_dyn_stub.c:333) alongside the real one. That is a duplicity the
+doctrine does not ask for — the same side of the same capability, written
+twice — and the copy is the one no test can reach. This batch deliberately did
+NOT carry the warning-prefix change below into it, so the two now disagree.
+
+** The cast warning wears the house prefix
+See "The warning is once per SITE" above. The =flan= in front of the location
+came off; a loc-bearing runtime diagnostic opens with a bare =FILE:LINE:COL:=
+everywhere else in the runtime.
+
+** Where the memory classifier overrode the spec: dyn push and put
+Written into the memory-diagnostics decision above, where its siblings live:
+see "Dyn push and put are not marked" under "Where this overrode the spec,
+and the evidence". It had only ever been in a test comment.
+
+** Two stale "kept honest by" claims, corrected
+lib/build.ml's note beside the header write and test/dyn_ops.c's own header
+both said dyn_ops.c calls every function runtime/flan_dyn.h declares. It does
+not, and the corrected header made that visible: [flan_dyn_cast_kind],
+[flan_dyn_is_nil], [flan_dyn_need_not_nil], [flan_dyn_map_get],
+[flan_dyn_map_set] and [flan_dyn_map_contains] are declared and never called
+there. The check the include buys is real but narrower than the claim: for a
+function dyn_ops.c *calls*, the call is compiled against the header and the
+symbol has to resolve against flan_dyn.o, so a rename, a removal or a changed
+argument list is a compile or link error in =dune test=. A function nothing
+here calls gets neither. Both comments now say that instead.

emacs/MANUAL.md

@@ -595,10 +595,21 @@ what it should call, and the message shape is what it should parse:
   :command ("flan" "check" "--warn-memory" source-original)
   :error-patterns
   ((warning line-start (file-name) ":" line ":" column
-            ": warning: " (message) line-end))
+            ": warning: " (message) line-end)
+   (error line-start (file-name) ":" line ":" column
+          ": " (message) line-end))
   :modes flan-mode)
 ```
 
+**Both patterns, and in that order.** A rejection is not labelled: `flan check`
+prints `file:line:col: message` and exits 1, so a checker with only the warning
+pattern reports "checker returned non-zero but no errors" on every real type
+error — the one case you most want it for. The error pattern is second because
+flycheck takes the first that matches a line, and the warning line would
+otherwise land in the error bucket with `warning: ` glued to the front of its
+message. The squiggle lines under each diagnostic and the closing `1 error` are
+matched by neither, which is fine.
+
 Only the file named on the command line is reported, so the prelude's own pushes
 — real, and none of your business — stay out of it.
 

emacs/flan.el

@@ -2766,18 +2766,29 @@ can print the same breakdown to stderr under FLAN_DEV_LEAKS."
                 (overlays-in (point-min) (point-max)))))
 
 (defun flan-clear-memory (&optional buffer)
-  "Remove the allocation annotations from BUFFER, or from the current buffer."
+  "Remove the allocation annotations from BUFFER.
+Called with no BUFFER, which is what running the command does, it takes
+them down everywhere instead: every buffer that has them.  One
+request paints every buffer visiting a file the answer names, so the marks
+are one reading spread over several buffers and not a per-buffer thing;
+clearing only the one point happens to be in would leave the rest of that
+reading up.  This is the same sweep the toggle in `flan-check-memory' does."
   (interactive)
-  (with-current-buffer (or buffer (current-buffer))
+  (dolist (b (if buffer (list buffer) (flan--marked-buffers)))
-    (remove-overlays (point-min) (point-max) 'flan-memory t)
+    (with-current-buffer b
-    (remove-hook 'after-change-functions #'flan--clear-memory-on-change t)))
+      (remove-overlays (point-min) (point-max) 'flan-memory t)
+      (remove-hook 'after-change-functions #'flan--clear-memory-on-change t))))
 
 (defun flan--clear-memory-on-change (_beg _end _len)
   "Take this buffer's allocation annotations down, as an `after-change-functions'.
 They are a reading of the source as it was when you asked, and an edit is
 what makes that reading stale — nothing smaller does, which is why this is
-not the `pre-command-hook' the error overlays use."
+not the `pre-command-hook' the error overlays use.
-  (flan-clear-memory))
+
+This one is deliberately per-buffer where the command is not: editing one
+file stales that file's reading, and the marks still standing in the others
+are still true."
+  (flan-clear-memory (current-buffer)))
 
 (defun flan--marked-buffers ()
   "Every buffer that currently has allocation annotations in it.

lib/build.ml

@@ -698,8 +698,14 @@ let compile_c ~opts ?tflags ?(warn = []) ~src ~name () =
 
        flan_dyn.c does *not* include it. The object cache is keyed on the
        source text, so a header edit would serve an object compiled against the
-       previous one, and the two copies of the declarations are kept honest by
+       previous one. What keeps the two copies of the declarations honest is
-       test/dyn_ops.c naming every function instead. *)
+       test/dyn_ops.c, which includes this header and links against flan_dyn.c:
+       every function it *calls* is compiled against the header and has to
+       resolve against the object, so a rename, a removal or a changed argument
+       list is a compile or link error in [dune test]. That is not the whole
+       header — six entry points are declared and never called there, listed in
+       dyn_ops.c's own comment — so it is a check with a known edge, not a
+       proof. *)
     write (Filename.concat dir "flan_dyn.h") Runtime_src.dyn_header;
     write c src;
     (* A distinct temporary target, renamed into place, so two builds running

lib/check.ml

@@ -1418,11 +1418,20 @@ let restart_sig tys =
 let dyn_i64 = Types.Int Types.I64
 let dyn_f64 = Types.Float Types.F64
 
-(* Widening to the one width the ABI carries. runtime/flan_dyn.h boxes integers
+(* Converting to whatever width the other side of the boundary wants, with a
-   as [i64] and floats as [f64] and offers no other width, which is the
+   [Cast] and not a silent reinterpretation. The name is for the direction it
-   language's "dyn integers are i64" written where it is enforced. The cast is
+   was written for: runtime/flan_dyn.h boxes integers as [i64] and floats as
-   explicit in the tree rather than left to the backend: a [Cast] is what the
+   [f64] and offers no other width, so *into* a box this only ever widens, and
-   language's own conversions emit, and a widening one loses nothing. *)
+   a widening cast loses nothing.
+
+   Coming back *out* it is used in both directions, and that is deliberate:
+   [cast_dyn] below unboxes to [i64]/[f64] and then hands the value to this to
+   reach the cast's target, which may be narrower ([(i32 d)]) or a different
+   kind ([(f32 d)]). Nothing is lost quietly there either — the [Cast] emitted
+   is the same node [(i32 x)] on a typed value emits, so the narrowing rule,
+   the fptosi range check and NaN are the emitter's, identical to the typed
+   spelling. This helper picks the node; it does not promise the conversion is
+   free. *)
 let widen loc (want : Types.t) (e : Tast.expr) =
   if Types.equal want e.Tast.ty then e
   else mk loc want (Tast.Prim (Tast.Cast want, [ e ]))
@@ -8530,6 +8539,15 @@ let no_gc (p : Tast.program) =
      integer type provably cannot.
    - A keyword is interned and immortal — [flan_dyn_kw]'s entry is not a GC
      object and the collector never traces one — so it is not named here.
+   - A dyn container growing itself is not named, and this one is a judgement
+     rather than a fact about the runtime: [flan_dyn_push] and
+     [flan_dyn_map_set] provably may [gc_alloc], and they are still left out.
+     The unit this pass reports is a line the programmer can act on — crossing
+     into dyn is a choice, pushing onto an allocator's Vec is a choice — and a
+     dyn vector taking a block to hold what was just put in it is the only
+     thing it could do. Marking it would squiggle every [(push dv x)] in a
+     program that chose dyn. Written down in FIX.org, because it is the one
+     row here that the precision rule alone does not decide.
    - Dyn arithmetic is not named. [flan_dyn_add] and its siblings end in
      [flan_dyn_from_i64], so a wide enough result spills, but nothing static
      knows the operands and a squiggle on every [(+ a b)] over dyn is the

lib/dev.ml

@@ -3038,9 +3038,12 @@ let memory_op t ~file =
       Printf.sprintf ":count %d" (List.length ds);
       ":note "
       ^ Wire.quote
-          "every site the checker can prove allocates, and every one it can \
+          "a site listed here allocates, or says in its first two words that \
-           prove may; a dyn immediate — nil, a bool, an f64, a keyword, an \
+           it may; a dyn immediate — nil, a bool, an f64, a keyword, an int \
-           int inside the payload — is not one and is not listed" ]
+           inside the payload — is not one and is not listed. Not every \
+           allocation the checker could prove: a dyn container growing itself \
+           on a push or a put is deliberately silent, being the container \
+           doing the only thing it can. See FIX.org" ]
 
 let handle t req =
   match Wire.string_field req "op" with

lib/emit.ml

@@ -4301,7 +4301,7 @@ let redefinition ?(checks = true) ?(dev = false) ?(debug = false)
        host's marker is the only part that matters. *)
     Buffer.add_string m.out
       (Printf.sprintf "%s = external global i64\n%s = hidden global ptr %s\n\n"
-         abi_marker_sym ("@" ^ quoted "flan.abi.require") abi_marker_sym);
+         abi_marker_sym ("@" ^ quoted Mangle.abi_require) abi_marker_sym);
     (* The cells are the host's, like the globals. Referencing one is how a
        redefined function reaches its siblings, and storing into one is how it
        replaces itself. A name the host lacks gets a slot instead, filled by

lib/mangle.ml

@@ -12,11 +12,13 @@
    Flan name holds -, ?, > and /, which is why every emitted name is quoted
    at all. This module only decides *which string* is quoted.
 
-   Not here: the ABI marker. [Emit.abi_marker] is ["flan.abi.llvm"] and
+   Not here: the ABI marker itself. [Emit.abi_marker] is ["flan.abi.llvm"] and
    [X86.abi_marker] is ["flan.abi.x86"], and the two must stay distinct —
    a crossed pair is refused at [dlopen] precisely because the marker one
    image defines is not the one the other references. Sharing that string
-   would delete the mechanism. *)
+   would delete the mechanism. The *label* a module hangs its requirement on
+   is the other half of that mechanism and is shared, so it is here: see
+   [abi_require] below. *)
 
 (* The prefix itself. It keeps the Flan [main] from colliding with C's, and
    it is what makes every Flan symbol recognisable in a disassembly. *)
@@ -40,3 +42,11 @@ let globalptr n = prefix ^ "gp." ^ n
 (* A compiled macro's entry point, which the expander dlsyms by this name out
    of the module [Build.macro_module] wrote. *)
 let macro n = prefix ^ "macro." ^ n
+
+(* The datum a redefinition module puts its host's ABI marker into. Nothing
+   outside the module names it — the relocation against the marker is the
+   whole of what it does — but both backends emit it, so the string is spelled
+   once here rather than twice, beside every other name that has to read the
+   same on both sides. What it *holds* is each backend's own marker, and that
+   pair stays distinct; see the paragraph at the top. *)
+let abi_require = prefix ^ "abi.require"

lib/x86.ml

@@ -4893,7 +4893,7 @@ let redefinition ~checks ?(dev = true) ?(known = fun _ -> true)
      relocation against the marker matters. *)
   Buffer.add_string out
     (Printf.sprintf "\n\t.data\n\t.align\t8\n%s:\n\t.quad\t%s\n"
-       (asm_sym "flan.abi.require") (asm_sym abi_marker));
+       (asm_sym Mangle.abi_require) (asm_sym abi_marker));
   (* Nothing outside this module refers to anything in it once the call has
      returned -- no cell holds an address in its text, the registry has no slot
      for it, and the value it produced was copied out. So it says so, and the

runtime/flan_dyn.c

@@ -1174,10 +1174,29 @@ uint8_t flan_dyn_need_bool(flan_dyn v) {
  * number of cross-kind cast sites a program has, which is a handful in the
  * programs this was written for. A program with more than [SITE_MAX] of them
  * stops deduplicating for the overflow — it still warns, every time, which
- * is the noisy failure rather than the silent one. Not thread-safe, and
+ * is the noisy failure rather than the silent one.
- * deliberately: a duplicated or dropped line under a race is a diagnostic
+ *
- * that came out twice, and the alternative is a lock on a path that runs per
+ * What the table stores is the loc's pointer, never a copy — the same licence
- * cast in a frame loop. */
+ * the allocation registry takes for its type names (flan_dev.c:1073-1075).
+ * The bytes are a string constant in the image of whatever module emitted the
+ * cast, and a module that emitted a string constant is never unloaded: the
+ * cell table forbids dlclose outright (flan_dev.c:27), and the one path that
+ * does unload — an expression thunk — is gated on the module having emitted
+ * no string literal at all ([nstr] in lib/emit.ml:383-391). A cast site's loc
+ * IS a string literal, emitted through [string_const] like any other, so a
+ * module holding one of these sites is on the never-unloaded side of that
+ * test. If that ever stops being true the table has to copy.
+ *
+ * Not thread-safe, and that is a statement about who runs this rather than a
+ * shrug: [flan_dyn_cast_kind] runs on the program's own thread and Flan has
+ * no second one today. The dev agent's listener thread reads flan_dev.c's
+ * tables — which is why *those* carry a seqlock — and never touches this one.
+ * Were a second thread ever to reach a cast, the cost would not be a line
+ * printed twice: {ptr, len} is a pair only meaningful together, and a reader
+ * that took the new pointer with the old length would read off the end of a
+ * string literal, exactly the hazard flan_dev.c:1126-1129 describes. The fix
+ * then is the registry's, not a lock on a path that runs per cast in a frame
+ * loop. */
 
 #define SITE_MAX 64
 
@@ -1216,7 +1235,7 @@ int32_t flan_dyn_cast_kind(flan_dyn v, const uint8_t *loc, int64_t loc_len,
   if (is_float != (want_float ? 1 : 0) && site_first_time(loc, loc_len)) {
     fflush(stdout);
     fprintf(stderr,
-            "flan %.*s: (%.*s x) found a dyn holding %s, and converted it to "
+            "%.*s: (%.*s x) found a dyn holding %s, and converted it to "
             "%.*s — warned once for this site\n",
             (int)loc_len, (const char *)loc, (int)target_len,
             (const char *)target, is_float ? "a float" : "an int",

test/dyn_ops.c

@@ -5,13 +5,22 @@
  * there is no program that could reach it. The .flan this links against
  * therefore has no [main] of its own; see programs/dyn-host.flan.
  *
- * This file includes runtime/flan_dyn.h and calls every function the header
+ * This file includes runtime/flan_dyn.h and calls most of what the header
  * declares. That is not tidiness — the build compiles flan_dyn.c on its own
  * with no include path, so the implementation declares its own prototypes and
  * the header is a second copy of them. Including it *here* is what makes a
  * divergence between the two a compile or link error in `dune test` rather
  * than a surprise in the compiler lane's emitted code.
  *
+ * "Most", not "every", and the gap is worth knowing: the check only covers a
+ * function this file calls. flan_dyn_cast_kind, flan_dyn_is_nil,
+ * flan_dyn_need_not_nil, flan_dyn_map_get, flan_dyn_map_set and
+ * flan_dyn_map_contains are declared in the header and reached from nowhere
+ * here, so nothing compares their two declarations. Each is lowered by
+ * lib/check.ml and so is exercised by the Flan programs the acceptance tests
+ * run — a check on the behaviour, not on the header. Adding a call for each
+ * is the way to close it.
+ *
  * One mode per run, chosen by argv, because most of the modes end in a trap
  * and a trap ends the process. The happy paths share one run; each refusal
  * gets its own.