The left-redzone claim was inferred, not measured, and was wrong

A negative index into a global is silent in bounds.flan, which is
measured. "Because a global has no left redzone" was the explanation
put on it, and it does not survive the obvious test: declare another
defvar in front of arr and arr[-1] is caught, landing in that global's
right redzone. Underflow detection is a question about what the linker
put in front of the object, not about the access. Corrected in
test_sanitize, BUILT.md and NEXT.md.

NEXT.md's entry also goes back to its stated size. It had grown to 78
lines saying what BUILT.md says in the same commit range -- the
attribute, the -O0 decision, the bounds.flan table -- which is the
half-build-log the file's own header warns about. What stays here is
what is next: the UBSan gap as an undecided compiler question, the four
daemon-path buffers the corpus never reaches, and Valgrind.

BUILT.md

@@ -299,10 +299,14 @@ out-of-bounds `inbounds` getelementptr into a constant is poison and LLVM folds
 wrong answer instead of touching memory. Same family as `(<< 1 32)` compiling to a bare `retq`.
 
 **What ASan covers of the bounds checks' job, since `--sanitize --no-bounds-checks` is the run that asks.** Three of
-`bounds.flan`'s six deliberate out-of-bounds cases are caught. A negative index into a global is not — a global gets a
-right redzone and nothing to its left. Neither is a reversed slice, which computes a negative length and then reads
-nothing at all. ASan sees out-of-*object* access, not out-of-subobject, so a slice into the middle of a larger array can
-overrun its logical bounds without crossing a redzone at all. It is a second net, not a replacement.
+`bounds.flan`'s six deliberate out-of-bounds cases are caught. A negative index into a global is not, and the reason is
+layout rather than anything about the access: ASan lays a global out as `{data, redzone}`, so reading before one lands
+in whatever precedes it, which is a redzone if something instrumented is there and ordinary memory if nothing is.
+Measured both ways — silent in `bounds.flan`, reported as soon as another `defvar` is declared in front of `arr`. A
+reversed slice is not caught either, having computed a negative length and read nothing at all. And ASan sees
+out-of-*object* access, not out-of-subobject, so a slice into the middle of a larger array can overrun its logical
+bounds without crossing a redzone. Three of six is a ceiling on what it covers, not a measurement of the risk. It is a
+second net, not a replacement.
 
 The sweep lives on its own dune alias rather than on `dune test`: a sanitized program links to a statically linked 1.8MB
 binary, and twenty-eight of them twice over is minutes against the suite's seconds.

NEXT.md

@@ -64,82 +64,35 @@ the commit that made it.
 
 ### Landed — the runtime under a sanitizer
 
-`--sanitize` is a build flag beside `--debug`, and `dune build --root . @sanitize` is the sweep: twenty-eight programs
-built twice, plain and sanitized, compared on output and exit status. It is not on `dune test` — a sanitized program is
-a statically linked 1.8MB binary and the sweep is about nine minutes against the suite's seconds.
+`--sanitize` is a build flag beside `--debug`; `dune build --root . @sanitize` builds twenty-eight programs twice, plain
+and sanitized, and compares output and exit status. Its own alias and not `dune test`, because the sweep is about nine
+minutes. The checked sweep is **clean**. How ASan and UBSan reach a language whose IR is written by hand, and why the
+flag does not force `-O0` when `--debug` does, is in [`BUILT.md`](BUILT.md).
 
-**The flag was the easy half. What the sanitizers reach is not symmetric, and this is the thing to remember:**
+Two defects came out of it, both found by reading rather than by the tools, both fixed with a regression case:
+`flan_bytes_to_i64`/`flan_bytes_to_f64` clamped a slice length with `(size_t)n` and so read 63 or 511 bytes off the end
+of a negative-length slice; and the three `snprintf` shims published snprintf's return as a slice length, which is what
+it *would* have written.
 
-- **ASan reaches Flan code only because `Emit` now says so.** AddressSanitizer is an LLVM pass but it instruments only
-  functions carrying the `sanitize_address` attribute, which clang's *C frontend* adds and which nothing adds to IR
-  written by hand. Before that attribute, `clang -fsanitize=address` over the `.ll` instrumented `flan_rt.c` and not one
-  instruction of Flan: a read off the end of a `defvar` array in a `--no-bounds-checks` build printed its garbage and
-  exited 0. With it, the same program reports `global-buffer-overflow in flan.main`. Globals get their redzone from the
-  module pass either way. `test_sanitize`'s first control is that exact program, so the day the attribute stops being
-  emitted the sweep fails loudly instead of going quietly green.
-- **UBSan reaches the runtime's C and nothing else, and there is no lever for it.** Its checks are branches to
-  `__ubsan_handle_*` that clang's C frontend emits; no attribute asks a pass to produce them. `(<< 1 32)` under
-  `-fsanitize=undefined` is still unremarked. **Item 3 of the old plan — shift UB, alignment, the f32→i32 cast on NaN —
-  is therefore not answerable this way, and is still open.** The choices are to emit the checks from `Emit` behind the
-  flag (a compiler feature, and the same shape the bounds checks already have) or to leave those to the checker. The
-  second control in `test_sanitize` is a program with unambiguous shift UB that is expected *not* to be caught, so if a
-  future clang changes this, the sweep says so.
+**What is left, and it is most of what the sweep was meant to settle:**
 
-`-fno-sanitize=signed-integer-overflow` is the one exclusion, because wrapping is what this language's arithmetic means.
-Nothing else is excluded. The flag does **not** force `-O0` the way `--debug` does; see below for why that earned its
-keep. `--sanitize --debug` together works and gives `-O0` plus source lines in the report.
+1. **UBSan sees no Flan code and no flag changes that.** Its checks are branches clang's C frontend emits inline, not a
+   pass, so shift UB (`(<< 1 32)`, see Sharp edges), alignment, and the f32→i32 cast on NaN or an infinity — the things
+   `floor-f32` guards by hand and nothing else does — are unreached. Either `Emit` grows those checks behind the flag,
+   which is a compiler feature of the same shape the bounds checks already have, or they belong to the checker. Not
+   decided. `test_sanitize` pins the current answer with a control that must *not* report, so a future clang changing
+   this is a test failure rather than a discovery.
+2. **Four named buffers got no evidence at all.** The 4K result cap, the dev registry overflow guard,
+   `SNAP_MAX`/`SNAP_NAMES` and `condition_name[128]` are on the daemon and agent paths, which need a socket and are not
+   in the corpus. Their guards were read and are correct; that is reading, not testing. `escaped[ESCAPE_MAX]` is the one
+   that *is* covered, because `println.flan` drives a 1100-character string through it on purpose — 1019 bytes out
+   against a worst case of 1021 into 1024. `scratch[SCRATCH]` never sees more than 20 characters of 64.
+3. **Valgrind over the headless corpus, not done.** ASan does not see uninitialised reads, which is where `zeroed` and
+   struct padding live. MSan is out: it needs every dependency instrumented and raylib settles that.
 
-**The checked sweep is clean: 28 programs, no ASan report, no UBSan report, no divergence from the unsanitized run.**
-What that does and does not prove:
-
-- It **does** cover `escaped[ESCAPE_MAX]` at its boundary. `println.flan` prints a 1100-character string inside a struct
-  on purpose; the escaped output is 1019 bytes against a hand-verified worst case of 1021 into 1024. That buffer is
-  genuinely exercised.
-- It says **nothing** about `scratch[SCRATCH]`, whose longest reachable output is 20 characters (`%lld`) into 64.
-- It says **nothing at all** about the 4K result cap, the dev registry overflow guard, `SNAP_MAX`/`SNAP_NAMES` or
-  `condition_name[128]`. Those are on the dev and agent paths, which need a daemon and a socket and are not in the
-  sweep's corpus. They were read and the guards are correct; that is reading, not evidence.
-
-**Two defects, both found by reading under the sanitizer rather than by the sanitizer, both fixed.**
-
-- `flan_bytes_to_i64` and `flan_bytes_to_f64` clamped with `(size_t)n < sizeof buf - 1`, and a slice's length is signed:
-  `(slice s 2 1)` is −1, `(size_t)(-1)` is not less than 511, so the `memcpy` read 63 or 511 bytes out of a five-byte
-  string constant. Every other `(ptr, len)` entry point in the runtime already folded a negative length to zero, so this
-  was two exceptions and not a missing convention. A checked build traps on the reversed slice first, which is why it
-  took `--no-bounds-checks` to show. Regression case in `test_sanitize`.
-- The three `snprintf` shims published `scratch` as a slice using snprintf's return, which is what it *would* have
-  written. No format here can reach 64, so it could not fire; it is clamped anyway, because the distance between "cannot
-  fire" and "hands out a length past the end of a static buffer" is one format string.
-
-**Left, deliberately.** `break_loop` prints the condition name with `"%.*s"` and a negative `namelen` would drop the
-precision and read to a NUL that a Flan string does not have — compiler-emitted and not reachable from source, so it is
-recorded rather than fixed. `flan_bytes_to_f64` silently parses only the first 511 bytes, which changes a value rather
-than corrupting memory.
-
-**ASan with `--no-bounds-checks`, the variant that asks whether the checks are the only thing holding the line. They
-mostly are.** Of `bounds.flan`'s six deliberate out-of-bounds cases ASan catches three:
-
-| case | what it does | ASan |
-|---|---|---|
-| `3`, `7` | read and write past a 3-element global | caught |
-| `4` | slice `hi` past the end of a string constant | caught |
-| `-1` | negative index into a global | **silent** — a global gets a right redzone and nothing on its left |
-| `9` | read past the end of a string constant | **silent at -O2, caught at -O0** |
-| `2` | reversed slice, negative length | silent — nothing is read at all |
-
-Three of six is an upper bound on ASan's cover, not a measured fraction of the risk: ASan sees out-of-*object* access,
-not out-of-subobject, so a slice into the middle of a larger array can overrun its logical bounds without crossing a
-redzone, and the `-1` case is one instance of that class. **ASan is not a substitute for the bounds checks.**
-
-Case `9` is why `--sanitize` does not force `-O0`. At `-O2` the access does not happen: an out-of-bounds `inbounds`
-getelementptr into a constant is poison, LLVM folds the load away, and the program prints a wrong answer instead of
-touching anything. Same family as `(<< 1 32)` compiling to a bare `retq` under Sharp edges. Running the sweep at both
-levels is cheap and a divergence between them is itself the finding.
-
-**Still not done.** Valgrind over the headless corpus, for the uninitialised reads ASan cannot see — where `zeroed` and
-struct padding live. MSan is out because it needs every dependency instrumented and raylib settles that. The reload path
-is uninstrumented whatever the flag says: a redefinition module is built by `llc` and `ld`, not by clang, so nothing
-puts a pass over it.
+Two things the sweep structurally cannot cover: raylib and libm are uninstrumented, so the windowed examples are noise;
+and a redefinition module is built by `llc` and `ld` rather than clang, so the reload path carries no instrumentation
+whatever the flag says.
 
 ### Managed classes are planned. Do not start them.
 

test/test_sanitize.ml

@@ -198,9 +198,12 @@ let control ~expect_report ?(args = []) ~why name src =
 let unchecked_controls () =
   let reports = [ "3"; "7"; "4" ] in
   let silent =
-    [ "-1", "a negative index into a global: ASan gives a global a right \
-             redzone and nothing on the left, so arr[-1] lands in whatever \
-             is in front of it";
+    [ "-1", "a negative index into a global. Not a property of the access: \
+             ASan lays a global out as {data, redzone}, so an underflow is \
+             caught when something redzoned precedes it and not when nothing \
+             does — measured both ways, and here nothing does. Whether \
+             reading before an array is seen at all is therefore up to what \
+             the linker put in front of it";
       "9",  "at -O2 the load is folded away — an out-of-bounds inbounds GEP \
              into a string constant is poison, so nothing is read and a wrong \
              value is printed. Reported at -O0.";