fix(spec): bound attention's position and seq_len by CONTEXT_LEN

.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"
 }

.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"
 }

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.

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;