The follow-ups the day's reviews left behind, each re-verified

flan.abi.require was spelled by hand in both backends, which is the one
job Mangle has. Moved; emit and x86 produce byte-identical output on the
reload path either way.

Four comments in the dyn-cast code asserted things that are not true.
The warning's location prefix now reads like every other loc-bearing
runtime diagnostic instead of inventing a shape. widen's contract says
what cast_dyn actually does with it. The thread-safety note names the
torn {ptr,len} overread rather than a duplicated line, and says why no
lock. The site table's borrowed loc pointer names what keeps it valid.

The memory op's note claimed a completeness it does not have: dyn push
and put may allocate and are deliberately silent. Said so, in the note,
in the classifier, and in FIX.org where the decision belongs.

The documented flycheck form only matched warnings, so a real error
made it say the checker returned non-zero and found nothing.

flan-clear-memory cleared one buffer where the toggle clears all.

Two comments claimed test/dyn_ops.c calls every function flan_dyn.h
declares; six are declared and never called there.

flan_dyn_stub.c's deadness is written into FIX.org for the author to
decide on. Not deleted here.

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)))
+    (with-current-buffer b
       (remove-overlays (point-min) (point-max) 'flan-memory t)
-    (remove-hook 'after-change-functions #'flan--clear-memory-on-change 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.