fix(spec): bound the pipeline loops by their buffers, and drive buffers in the harness

.trinity/seals/PipelineE2E.json

@@ -1,11 +1,11 @@
 {
-  "gen_hash_c": "sha256:6de267b1261e93c8b42d557f26b6e6d1d40fe4c567e8afd0b271058013a33db1",
-  "gen_hash_rust": "sha256:c1a6e06636114237d6d2a4e8e124ac3f1458d45ff2fbefb54d76f756aeafe3bc",
-  "gen_hash_verilog": "sha256:5034b456a26c7ffda98213b086e83601447de0d2fe760b23f2c846694436fa21",
-  "gen_hash_zig": "sha256:ec929d8c75309f7f642e52c2a3d92de5733318a5e498819255301ab77bc9c632",
+  "gen_hash_c": "sha256:47d34e68f6576889ea639a5632f49ef37873858a3d82ec4c05a8613e2420504e",
+  "gen_hash_rust": "sha256:cccfeddf4a16c31e189b8db5e696936b8f72dfdc748afdcadb12f564872f8236",
+  "gen_hash_verilog": "sha256:d934e06ab713c6c15acec34b5308773df27dd423fd4bd7058c40588378819e29",
+  "gen_hash_zig": "sha256:6fd74c502aa81e37faa297719b0418a0b452d828df8b8786f906770cf04029f5",
   "module": "PipelineE2E",
   "ring": 12,
-  "sealed_at": "2026-09-07T22:05:58Z",
-  "spec_hash": "sha256:47ff992484aab2a06b5e58c1487fffee481eac77c19fe81827b1e1572f5aee59",
+  "sealed_at": "2026-09-07T22:44:14Z",
+  "spec_hash": "sha256:9bc29526cd752989255b14925191d722cb8c5ebbf8b805412b22de07945d095c",
   "spec_path": "specs/pipeline/e2e_test.t27"
 }

.trinity/seals/pipeline_PipelineE2E.json

@@ -1,12 +1,12 @@
 {
-  "gen_hash_c": "sha256:6de267b1261e93c8b42d557f26b6e6d1d40fe4c567e8afd0b271058013a33db1",
-  "gen_hash_rust": "sha256:c1a6e06636114237d6d2a4e8e124ac3f1458d45ff2fbefb54d76f756aeafe3bc",
-  "gen_hash_verilog": "sha256:5034b456a26c7ffda98213b086e83601447de0d2fe760b23f2c846694436fa21",
-  "gen_hash_zig": "sha256:ec929d8c75309f7f642e52c2a3d92de5733318a5e498819255301ab77bc9c632",
+  "gen_hash_c": "sha256:47d34e68f6576889ea639a5632f49ef37873858a3d82ec4c05a8613e2420504e",
+  "gen_hash_rust": "sha256:cccfeddf4a16c31e189b8db5e696936b8f72dfdc748afdcadb12f564872f8236",
+  "gen_hash_verilog": "sha256:d934e06ab713c6c15acec34b5308773df27dd423fd4bd7058c40588378819e29",
+  "gen_hash_zig": "sha256:6fd74c502aa81e37faa297719b0418a0b452d828df8b8786f906770cf04029f5",
   "module": "PipelineE2E",
   "ring": 12,
-  "sealed_at": "2026-09-07T22:05:58Z",
+  "sealed_at": "2026-09-07T22:44:14Z",
   "sealed_by": "t27c-bootstrap@0.2.0",
-  "spec_hash": "sha256:47ff992484aab2a06b5e58c1487fffee481eac77c19fe81827b1e1572f5aee59",
+  "spec_hash": "sha256:9bc29526cd752989255b14925191d722cb8c5ebbf8b805412b22de07945d095c",
   "spec_path": "specs/pipeline/e2e_test.t27"
 }

docs/now/2026-09-08-the-weakness-i-named-was-hiding-a-write-past-the-end.md

@@ -0,0 +1,10 @@
+# NOW -- The weakness I named was hiding a write past the end (2026-09-08)
+
+## The weakness I named was hiding a write past the end (Closes #3428)
+
+- One pass ago I shipped a differential generator and wrote down its weakest part: a `&mut [T]` parameter got a single zero-filled `[T; 8]`, so it compared what came BACK while never varying what went IN. `ring-099` read **25 of 25 agreeing** and I recorded that "25 is not the evidence 936 is". Driving length and fill -- lengths **0, 1, 4, 8** -- the same pair reads **80 cases, 44 agree, 36 disagree**.
+- The defect: the spec bounds its loop by the constant `MAX_PIPELINE_STAGES = 10` and indexes without consulting the buffer. Hand it four elements and it writes `stages[4..10]`. The hand-written `rings/ring-099-rust`, which this spec is supposed to define, has always computed `stages.len().min(results.len()).min(MAX_PIPELINE_STAGES)`.
+- **In C there is nothing to check.** `uint8_t pipeline_run(uint8_t* stages, bool* results, size_t* count)` -- no length parameter. A `[]T` becomes a bare pointer at the C ABI and the length is gone; probed directly, `buf.len` lowers to `buf.len()` in Rust and `buf.len` in Zig and the C backend emits nothing for it. The bound this spec needs is expressible in **2 of 4 backends**. In Rust a short buffer panics; in C it writes past the end silently.
+- Fixed: both loops now bound by `stages.len` and `results.len`, so Rust and Zig match the model -- **80 of 80** agree, and reverting the bound reproduces 44 of 80 and exit 1. NOT fixed: the C output still writes to the constant. Making C safe needs an explicit length parameter, which changes the ABI for all four and would make ring-099 DRIFTED again unless the ring changes too. Filed as a decision.
+- **Third pass in a row where the hand-written code was right and the spec was wrong** -- #3420 wrapped where the model saturated, #3422 emitted a raw pointer where the model took a safe reference, and this one writes past the end. The first two were wrong values; this is memory safety.
+- The lesson worth more than the fix: I wrote the limitation down as prose one pass ago and it changed nothing. It only became a finding when the grid was built and RUN. A named weakness is not a measured one.

specs/pipeline/e2e_test.t27

@@ -23,7 +23,17 @@ module PipelineE2E {
     fn pipeline_run(stages: []u8, results: []bool, count: *usize) u8 {
         var current : u8 = STAGE_INIT;
         var i : usize = 0;
-        while (i < MAX_PIPELINE_STAGES and current != STAGE_DONE and current != STAGE_FAIL) {
+        // Bound by the BUFFERS, not only by the constant. The loop wrote
+        // stages[0..MAX_PIPELINE_STAGES] whatever length it was handed: with a
+        // zero-length buffer the generated Rust panics on the first write, and
+        // the hand-written model in rings/ring-099-rust has always computed
+        // `stages.len().min(results.len()).min(MAX_PIPELINE_STAGES)`. A buffer
+        // grid over lengths 0, 1, 4 and 8 found 36 of 80 differential cases
+        // disagreeing; before the grid the same pair read 25 of 25 agreeing.
+        var cap : usize = MAX_PIPELINE_STAGES;
+        if (stages.len < cap) { cap = stages.len; }
+        if (results.len < cap) { cap = results.len; }
+        while (i < cap and current != STAGE_DONE and current != STAGE_FAIL) {
             stages[i] = current;
             results[i] = true;
             count.* = i + 1;
@@ -45,7 +55,10 @@ module PipelineE2E {
     fn pipeline_inject_failure(fail_at: u8, stages: []u8, results: []bool, count: *usize) u8 {
         var current : u8 = STAGE_INIT;
         var i : usize = 0;
-        while (i < MAX_PIPELINE_STAGES and current != STAGE_DONE and current != STAGE_FAIL) {
+        var cap2 : usize = MAX_PIPELINE_STAGES;
+        if (stages.len < cap2) { cap2 = stages.len; }
+        if (results.len < cap2) { cap2 = results.len; }
+        while (i < cap2 and current != STAGE_DONE and current != STAGE_FAIL) {
             stages[i] = current;
             if (current == fail_at) {
                 results[i] = false;

tools/ring_spec_differential.py

@@ -112,6 +112,7 @@ def emit(ring_lib: str, spec_rs: str, sigs: dict, prod: dict) -> tuple:
         covered.append(fn)
 
         loops, args_h, args_s, post, pre = [], [], [], [], []
+        need_buf_loop = False
         for i, (pname, t) in enumerate(params):
             v = f"v{i}"
             if t in GRID:
@@ -130,11 +131,25 @@ def emit(ring_lib: str, spec_rs: str, sigs: dict, prod: dict) -> tuple:
                 args_h.append(f"{v}h")
                 args_s.append(f"{v}s")
             elif t.startswith("&mut ["):
+                # A buffer parameter used to be one zero-filled `[T; 8]`, so the
+                # 25 cases for ring-099 compared what came BACK while never
+                # varying what went IN. Length and fill are now driven, and the
+                # zero length is in the grid because an empty buffer is where an
+                # off-by-one lives.
+                #
+                # All slice parameters of one call share the (len, fill) pair:
+                # in the corpus they are parallel arrays, and giving each its
+                # own loop would multiply the case count without adding a shape
+                # the callee can distinguish.
                 el = t[6:-1]
-                zero = "false" if el == "bool" else "0"
-                pre.append(f"let mut {v}h: [{el}; 8] = [{zero}; 8]; let mut {v}s: [{el}; 8] = [{zero}; 8];")
-                args_h.append(f"&mut {v}h")
-                args_s.append(f"&mut {v}s")
+                need_buf_loop = True
+                fill = "bfill != 0" if el == "bool" else f"bfill as {el}"
+                pre.append(
+                    f"let mut {v}h: Vec<{el}> = vec![{fill}; blen]; "
+                    f"let mut {v}s: Vec<{el}> = vec![{fill}; blen];"
+                )
+                args_h.append(f"&mut {v}h[..]")
+                args_s.append(f"&mut {v}s[..]")
                 post.append(f"&& {v}h == {v}s")
             else:  # &mut T
                 el = t[5:]
@@ -168,6 +183,11 @@ def emit(ring_lib: str, spec_rs: str, sigs: dict, prod: dict) -> tuple:
         for v, vals in reversed(loops):
             arr = ", ".join(vals)
             inner = f"    for {v} in [{arr}] {{\n{inner}\n    }}"
+        if need_buf_loop:
+            inner = (
+                "    for blen in [0usize, 1, 4, 8] {\n"
+                "    for bfill in [0u8, 1, 255] {\n" + inner + "\n    }\n    }"
+            )
         body.append("    {\n" + inner + "\n    }")
 
     src = f"""#[allow(dead_code, unused_mut, non_snake_case, unused_variables)] mod hand {{ include!("{ring_lib}"); }}