fix(spec): bound the pipeline loops by their buffers, and drive buffers in the harness - #3429
Merged
Conversation
…rs in the harness 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: cases 80 agree 44 disagree 36 first disagreement: pipeline_inject_failure The spec bounds its loop by the constant MAX_PIPELINE_STAGES = 10 and indexes without consulting the buffer, so a buffer of four gets stages[4..10] written. 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 the generated Rust a short buffer panics; in C it does not. In C there is nothing to check: `uint8_t pipeline_run(uint8_t* stages, bool* results, size_t* count)` has no length parameter. A `[]T` becomes a bare pointer at the C ABI. Probed directly, `buf.len` lowers to `buf.len()` in Rust and `buf.len` in Zig, and the C backend emits nothing for it -- so the bound this spec needs is expressible in 2 of the 4 backends. Fixed here: both loops bound by `stages.len` and `results.len`. Rust and Zig now 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 regardless of what it was handed. Making C safe needs an explicit length parameter, which changes the ABI for all four backends and would make ring-099 read DRIFTED again unless the ring changes with it. Filed rather than decided. All slice parameters of one call share the (length, fill) pair: in the corpus they are parallel arrays, and a loop each would multiply cases without adding a shape the callee can distinguish. 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; this writes past the end. The first two were wrong values. The lesson worth more than the fix: the limitation was written down as prose one pass ago and changed nothing. It became a finding only when the grid was built and run. A named weakness is not a measured one. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
gHashTag
enabled auto-merge (squash)
September 7, 2026 22:46
Contributor
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
This was referenced Sep 7, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
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-099read 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:
The defect
The spec bounds its loop by a constant and indexes without consulting the buffer:
MAX_PIPELINE_STAGESis 10. Hand it four elements and it writesstages[4..10].The hand-written
rings/ring-099-rust, which this spec is supposed to define, has always bounded by the buffers:In C there is nothing to check
No length parameter. A
[]Tbecomes a bare pointer at the C ABI. Probed directly:buf.lenlowers tobuf.len()in Rust andbuf.lenin Zig, and the C backend emits nothing for it at all. The bound this spec needs is expressible in 2 of the 4 backends.In the generated Rust a short buffer panics. In C it writes past the end, silently.
Fixed, and not fixed
Fixed: both loops bound by
stages.lenandresults.len. Rust and Zig now match the model — 80 of 80 agree — and reverting the bound reproduces 44 of 80 and exit 1, which is the control.Not fixed: the C output still writes to the constant regardless of what it was handed. Making C safe needs an explicit length parameter, which changes the ABI for all four backends and would make
ring-099read DRIFTED again unless the ring changes with it. Filed rather than decided.Third pass in a row where the hand-written code was right
The first two were wrong values. This one is memory safety.
The lesson worth more than the fix
I wrote this limitation down as prose one pass ago and it changed nothing. It became a finding only when the grid was built and run. A named weakness is not a measured one.
Verified end to end: the full
Spec Guardsworkflow body runs green under bash 3.2 —936/936,80/80,CONVERGED pairs run: 2,STALE 0— and both seals for the edited spec were refreshed byt27c seal --save, duplicates included.