diff --git a/.trinity/seals/PipelineE2E.json b/.trinity/seals/PipelineE2E.json index 7ae01758d1..843706c1d2 100644 --- a/.trinity/seals/PipelineE2E.json +++ b/.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" } \ No newline at end of file diff --git a/.trinity/seals/pipeline_PipelineE2E.json b/.trinity/seals/pipeline_PipelineE2E.json index 5774b25b8f..a68190fa18 100644 --- a/.trinity/seals/pipeline_PipelineE2E.json +++ b/.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" } \ No newline at end of file diff --git a/docs/now/2026-09-08-the-weakness-i-named-was-hiding-a-write-past-the-end.md b/docs/now/2026-09-08-the-weakness-i-named-was-hiding-a-write-past-the-end.md new file mode 100644 index 0000000000..68cd172af4 --- /dev/null +++ b/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. diff --git a/specs/pipeline/e2e_test.t27 b/specs/pipeline/e2e_test.t27 index 30d1757761..e56565f9a1 100644 --- a/specs/pipeline/e2e_test.t27 +++ b/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; diff --git a/tools/ring_spec_differential.py b/tools/ring_spec_differential.py index b6076e0760..0ea16b6b40 100755 --- a/tools/ring_spec_differential.py +++ b/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}"); }}