diff --git a/.trinity/seals/FPGA_Bridge.json b/.trinity/seals/FPGA_Bridge.json index 65e70a6af..c73e0d68e 100644 --- a/.trinity/seals/FPGA_Bridge.json +++ b/.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" -} +} \ No newline at end of file diff --git a/.trinity/seals/fpga_FPGA_Bridge.json b/.trinity/seals/fpga_FPGA_Bridge.json index bf343e0f6..5445d0fed 100644 --- a/.trinity/seals/fpga_FPGA_Bridge.json +++ b/.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" } \ No newline at end of file diff --git a/docs/now/2026-09-08-four-bounds-and-one-that-was-not-there.md b/docs/now/2026-09-08-four-bounds-and-one-that-was-not-there.md new file mode 100644 index 000000000..956a8efaa --- /dev/null +++ b/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. diff --git a/specs/fpga/bridge.t27 b/specs/fpga/bridge.t27 index bd335b9bb..6f5e61a72 100644 --- a/specs/fpga/bridge.t27 +++ b/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];