diff --git a/.trinity/seals/SacredAttention.json b/.trinity/seals/SacredAttention.json index 5c4b145042..1a87aa25a2 100644 --- a/.trinity/seals/SacredAttention.json +++ b/.trinity/seals/SacredAttention.json @@ -1,11 +1,11 @@ { - "gen_hash_c": "sha256:f4454df1de407b648599bab4486b3a2161b55cb98e8bf08c3dccce823ebfd3ac", - "gen_hash_rust": "sha256:c003a0bd2dcc0558499a3b8df923cf1103ceaeb0075213861601a942ba660e42", - "gen_hash_verilog": "sha256:f10591dc966a8ac3535e358d35427cb7b03128d6095bad3d76f51b5ca8514f2f", - "gen_hash_zig": "sha256:04869b3b6648bcb78f992e671734c17295760ccce99c82281f6969a55ff4a5b9", + "gen_hash_c": "sha256:f48f48d3f0815081c9df3e506ef5aeb2a5080fd5161312b18885fec9ee07b5d9", + "gen_hash_rust": "sha256:0a4064c4d5ae45dda501198128042849e7b9f0b1b598012ddf8ff34367df1b72", + "gen_hash_verilog": "sha256:c42b9ba4364a38267215c0c16fadc075cffeb0cc94fdf5a612b2c35dee2ec06d", + "gen_hash_zig": "sha256:187bc0b9346fcc3d35ae53a9bad1be0fab2cfe59ddedbf8f61fe4a2856f4cd36", "module": "SacredAttention", "ring": 12, - "sealed_at": "2026-09-07T22:05:58Z", - "spec_hash": "sha256:9d16a7efd14f69af62f5d85612ed1c99f0caf6dda097f403eda5c4f865fdf125", + "sealed_at": "2026-09-07T23:13:13Z", + "spec_hash": "sha256:be83d2a916a15957502d6afa4d6eff7ab07d0373e81555704ee842500db47187", "spec_path": "specs/nn/attention.t27" } \ No newline at end of file diff --git a/.trinity/seals/nn_SacredAttention.json b/.trinity/seals/nn_SacredAttention.json index 52c4df677d..242aee7634 100644 --- a/.trinity/seals/nn_SacredAttention.json +++ b/.trinity/seals/nn_SacredAttention.json @@ -1,12 +1,12 @@ { - "gen_hash_c": "sha256:f4454df1de407b648599bab4486b3a2161b55cb98e8bf08c3dccce823ebfd3ac", - "gen_hash_rust": "sha256:c003a0bd2dcc0558499a3b8df923cf1103ceaeb0075213861601a942ba660e42", - "gen_hash_verilog": "sha256:f10591dc966a8ac3535e358d35427cb7b03128d6095bad3d76f51b5ca8514f2f", - "gen_hash_zig": "sha256:04869b3b6648bcb78f992e671734c17295760ccce99c82281f6969a55ff4a5b9", + "gen_hash_c": "sha256:f48f48d3f0815081c9df3e506ef5aeb2a5080fd5161312b18885fec9ee07b5d9", + "gen_hash_rust": "sha256:0a4064c4d5ae45dda501198128042849e7b9f0b1b598012ddf8ff34367df1b72", + "gen_hash_verilog": "sha256:c42b9ba4364a38267215c0c16fadc075cffeb0cc94fdf5a612b2c35dee2ec06d", + "gen_hash_zig": "sha256:187bc0b9346fcc3d35ae53a9bad1be0fab2cfe59ddedbf8f61fe4a2856f4cd36", "module": "SacredAttention", "ring": 12, - "sealed_at": "2026-09-07T22:05:58Z", + "sealed_at": "2026-09-07T23:13:13Z", "sealed_by": "t27c-bootstrap@0.2.0", - "spec_hash": "sha256:9d16a7efd14f69af62f5d85612ed1c99f0caf6dda097f403eda5c4f865fdf125", + "spec_hash": "sha256:be83d2a916a15957502d6afa4d6eff7ab07d0373e81555704ee842500db47187", "spec_path": "specs/nn/attention.t27" } \ No newline at end of file diff --git a/docs/now/2026-09-08-the-bound-was-eleven-lines-above-it.md b/docs/now/2026-09-08-the-bound-was-eleven-lines-above-it.md new file mode 100644 index 0000000000..3da7ee009d --- /dev/null +++ b/docs/now/2026-09-08-the-bound-was-eleven-lines-above-it.md @@ -0,0 +1,9 @@ +# NOW -- The bound was eleven lines above it (2026-09-08) + +## The bound was eleven lines above it (Closes #3432, Refs #3430) + +- One pass ago I listed `cache_kv` as needing "either a new parameter or `.len`, and that is a decision". It was not. `const CONTEXT_LEN : usize = 81; // Max sequence length` is declared **eleven lines above it** in the same file. +- Three functions in `specs/nn/attention.t27` share the shape, and **two of them were not in that audit at all** -- I found them by reading the neighbours of the one I had flagged. `apply_rope_qk` reads `rope_tables.cos[position * ROPE_PAIRS + pair_idx]` against a `[CONTEXT_LEN * ROPE_PAIRS]` table; `cache_kv` writes `cache_k[position * EMBED_DIM + i]`; `compute_scores` writes `scores[h * CONTEXT_LEN + j]` with `j < seq_len` against `[NUM_HEADS * CONTEXT_LEN]`. Nothing bounded `position` or `seq_len`. In the generated Rust each panics; in C the write simply happens, the parameter being a bare pointer. +- **The intent was already written down twice.** The declaration carries `// [CONTEXT_LEN][EMBED_DIM]` in a comment, and the spec's own test allocates `[0.0; EMBED_DIM * CONTEXT_LEN]`. Stated in a comment, exercised by a test, enforced by nothing. +- Guarded by the CONSTANT, not by `.len`, for the same reason as #3431: a `[]T` loses its length at the C ABI, so a `.len` guard would live in Rust and Zig and be absent from C. `compute_scores` clamps `seq_len` rather than returning -- a caller asking for more rows than exist still wants the ones that do. rustc errors on the file are unchanged at 23, all pre-existing. +- The lesson: I read the function and not the file. Twice now the thing I called a decision was a constant already in scope -- the same mistake as calling the CI cost a decision, and as calling the out-parameter shape one. diff --git a/specs/nn/attention.t27 b/specs/nn/attention.t27 index f5dd8dd6d2..e7e7583434 100644 --- a/specs/nn/attention.t27 +++ b/specs/nn/attention.t27 @@ -220,6 +220,13 @@ module SacredAttention { // Apply φ-RoPE rotation to Q and K // Rotates pairs of dimensions using precomputed tables fn apply_rope_qk(buffers: *AttentionBuffers, position: usize) -> void { + // `rope_tables.cos` is [CONTEXT_LEN * ROPE_PAIRS] and this reads + // `position * ROPE_PAIRS + pair_idx`. Nothing bounded `position`, so a + // caller past the end read off the end of the table -- a panic in the + // generated Rust, and a silent read in C, where a []T is a bare pointer. + if (position >= CONTEXT_LEN) { + return; + } var h : usize = 0; while (h < NUM_HEADS) { @@ -264,6 +271,13 @@ module SacredAttention { position: usize, cache_k: []f64, cache_v: []f64, ) -> void { + // The shape is stated in a comment on the declaration -- + // `cache_k: []f64, cache_v: []f64, // [CONTEXT_LEN][EMBED_DIM]` -- and + // was enforced nowhere. `position` indexes into that, so an unbounded + // one writes past the end. + if (position >= CONTEXT_LEN) { + return; + } const offset = position * EMBED_DIM; var i : usize = 0; @@ -287,13 +301,20 @@ module SacredAttention { seq_len: usize, cache_k: []f64, ) -> void { + // `buffers.scores` is [NUM_HEADS * CONTEXT_LEN] and the write index is + // `h * CONTEXT_LEN + j` with `j < seq_len`. A `seq_len` above + // CONTEXT_LEN therefore runs off the end of every head's row. + var bounded_len : usize = seq_len; + if (bounded_len > CONTEXT_LEN) { + bounded_len = CONTEXT_LEN; + } var h : usize = 0; while (h < NUM_HEADS) { const head_offset = h * HEAD_DIM; var j : usize = 0; - while (j < seq_len) { + while (j < bounded_len) { // Skip if j > position (causal mask) if (j > position) { buffers.scores[h * CONTEXT_LEN + j] = 0.0;