fix(spec): bound buffer_write by size, and audit what bounds a slice write

.trinity/seals/FPGA_Bridge.json

@@ -1,11 +1,11 @@
 {
-  "gen_hash_c": "sha256:e26d5e7d7b252343f37f1beae4d344af390bf3cdd8fc2c3778d6359990aac6db",
-  "gen_hash_rust": "sha256:fe3ec5eaf7f43ba18226e4939e4b5c9ace140192f1416921d65a06aecd82b528",
-  "gen_hash_verilog": "sha256:7baa41f693b25fd218b7fb41ca5acee278ec413bb0449dbef759e6d6880a852f",
-  "gen_hash_zig": "sha256:52c3832bd59a6d948b03bd92108aa5adc3ca6cafa412afff71acf7f5d271f569",
+  "gen_hash_c": "sha256:765d510a3bf0c74ee2cdbea7a9ad2cf5444bc4e88bb0ff3755b48983f642453b",
+  "gen_hash_rust": "sha256:d1c6ce678fb63db26f6636dc92f17710400cc3acb14cbe4fede86013e365941c",
+  "gen_hash_verilog": "sha256:1fcc41e8c75934e2aa15c4637c5628a80f15e54de03e719dfc2f39d10cb291f1",
+  "gen_hash_zig": "sha256:244c366f2c2ba438dae307442c8e426b09567cf4dbe0b0584c99e88e7f2fa8e2",
   "module": "FPGA_Bridge",
   "ring": 12,
-  "sealed_at": "2026-08-28T18:19:55Z",
-  "spec_hash": "sha256:a6b3892f83131b5c6194a7da5bd5b7edc1de4b33d7bfd8c15cde235fce19a775",
+  "sealed_at": "2026-09-07T23:00:09Z",
+  "spec_hash": "sha256:549e7fa1e7b391e1adeb47ce9e3d4525c56831823e9a119105b8b6718172c8ef",
   "spec_path": "specs/fpga/bridge.t27"
-}
+}

.trinity/seals/fpga_FPGA_Bridge.json

@@ -1,12 +1,12 @@
 {
-  "gen_hash_c": "sha256:e26d5e7d7b252343f37f1beae4d344af390bf3cdd8fc2c3778d6359990aac6db",
-  "gen_hash_rust": "sha256:fe3ec5eaf7f43ba18226e4939e4b5c9ace140192f1416921d65a06aecd82b528",
-  "gen_hash_verilog": "sha256:7baa41f693b25fd218b7fb41ca5acee278ec413bb0449dbef759e6d6880a852f",
-  "gen_hash_zig": "sha256:52c3832bd59a6d948b03bd92108aa5adc3ca6cafa412afff71acf7f5d271f569",
+  "gen_hash_c": "sha256:765d510a3bf0c74ee2cdbea7a9ad2cf5444bc4e88bb0ff3755b48983f642453b",
+  "gen_hash_rust": "sha256:d1c6ce678fb63db26f6636dc92f17710400cc3acb14cbe4fede86013e365941c",
+  "gen_hash_verilog": "sha256:1fcc41e8c75934e2aa15c4637c5628a80f15e54de03e719dfc2f39d10cb291f1",
+  "gen_hash_zig": "sha256:244c366f2c2ba438dae307442c8e426b09567cf4dbe0b0584c99e88e7f2fa8e2",
   "module": "FPGA_Bridge",
   "ring": 12,
-  "sealed_at": "2026-09-07T21:07:02Z",
+  "sealed_at": "2026-09-07T23:00:09Z",
   "sealed_by": "t27c-bootstrap@0.2.0",
-  "spec_hash": "sha256:a6b3892f83131b5c6194a7da5bd5b7edc1de4b33d7bfd8c15cde235fce19a775",
+  "spec_hash": "sha256:549e7fa1e7b391e1adeb47ce9e3d4525c56831823e9a119105b8b6718172c8ef",
   "spec_path": "specs/fpga/bridge.t27"
 }

docs/now/2026-09-08-four-bounds-and-one-that-was-not-there.md

@@ -0,0 +1,11 @@
+# NOW -- Four bounds, and one that was not there (2026-09-08)
+
+## Four bounds, and one that was not there (Closes #3430, Refs #3428)
+
+- I closed #3428 saying I had NOT measured how widespread the shape was. Measured: of **4692** emitted functions, **67** take a slice parameter and **59** index into one.
+- Classifying the bound took **three matcher attempts and each earlier answer was wrong**. "34 write without bounding by `.len()`" was true and useless -- most bound by an explicit length PARAMETER, the only thing that works in C. "3 have a length parameter and do not use it" -- **two of the three were false positives**: `ternary_shift_right` starts its loop at `len - 1` and my regex looked for `while (... len ...)`. "24 bounded by a compile-time constant" was inflated: `TRIT_NEG`/`TRIT_POS`/`TRIT_ZERO` are VALUES, and matching "a declared constant appears in the body" swept in `byte_to_trits`, which I had already hand-verified as correct.
+- **Hand-verified ten functions by eye: two were matcher false positives, eight genuinely bound by something other than the buffer.** I did not read all 59, so the class is between 8 and 24 and I am publishing no single number for it.
+- The four bounds in use: the buffer's own `.len()` (not safe in C -- no length there); an explicit length parameter (`byte_to_trits`, `mac_parallel_multiply`); a compile-time constant (`hash_insert` by `TABLE_SIZE`, `mem_store` by `MEM_SIZE`, `set_insert` by `SET_MAX`); and **nothing at all**. `cache_kv` earns its own line: it writes `cache_k[position * EMBED_DIM + i]`, so the index grows with `position` and nothing bounds `position`.
+- Fixed, because it is unambiguous: `buffer_write` never compared `head` to `size`. The evidence that this is an oversight and not a convention is **in the same file** -- the sibling `buffer_read` guards its index, and its guard was `tail == size`, catching exactly one-past-the-end and letting every larger index through. Both now use `>=`.
+- The bound uses `size`, **not** `buf_in.len`, deliberately: a `[]T` loses its length at the C ABI, so a `.len`-based guard would live in Rust and Zig and be absent from C. With the parameter, the identical `if ((head >= size))` appears in both outputs.
+- Left as a decision: the constant-bounded set is a convention with an unstated precondition -- "your buffer must be at least CONST long" -- coherent, enforced by nothing, and changing it means adding length parameters and changing the ABI.

specs/fpga/bridge.t27

@@ -86,6 +86,20 @@ module FPGA_Bridge;
     // buffer_write(buf: []u8, size: usize, head: usize, data: u8) → bool
     // Write byte to circular buffer
     fn buffer_write(buf_in: []u8, size: usize, head: usize, data: u8) -> bool {
+        // `head` was never checked against `size`, so a caller one past the end
+        // wrote out of bounds: in the generated Rust that panics, and in C the
+        // signature is `bool buffer_write(uint8_t* buf_in, size_t size, size_t
+        // head, uint8_t data)` -- a bare pointer, so the write simply happens.
+        // The sibling `buffer_read` in this same file guards its index; this
+        // one did not, and an asymmetry inside one file is an oversight rather
+        // than a convention.
+        //
+        // The bound uses `size`, not `buf_in.len`, deliberately: a `[]T` loses
+        // its length at the C ABI, so a `.len`-based guard would exist in the
+        // Rust and Zig outputs and be absent from C (#3428).
+        if (head >= size) {
+            return false;
+        }
         const new_head = (head + 1) % size;
         if (new_head == 0 && head == size - 1) {
             return false;  // Buffer full
@@ -97,7 +111,9 @@ module FPGA_Bridge;
     // buffer_read(buf: []u8, size: usize, tail: usize) → (u8, usize)
     // Read byte from circular buffer, return (data, new_tail)
     fn buffer_read(buf: []u8, size: usize, tail: usize) -> (u8, usize) {
-        if (tail == size) {
+        // `>=`, not `==`: the equality caught the one-past-the-end case and
+        // let every larger index through to `buf[tail]`.
+        if (tail >= size) {
             return (0u8, 0);
         }
         const data = buf[tail];