gft: the counterpart is the spec, not a path that never existed (Refs #2161) - #2659
Merged
Conversation
…2161) Closing the sticky finding I cited `board/bpseq.v` as the reason not to change a rounding rule I had just shown to be wrong. `git log --all` for that path is empty -- it has never existed in this repository. The pointer came out of the file's own docstring and I repeated it without checking it resolved. The counterpart is `specs/ternary/gft_sadd.t27`. Measured: it carries the rule line for line, 30 specs carry a copy, the arm is dead there too (exhaustive over every (hm, lm, d) for six ho), and the spec's barrel shift agrees with this file's 12-step loop bit-for-bit over 2_193_075 points. The generated Verilog, C and Rust all carry the same dormant rule, and the bit-exactness gates cannot see it: they prove the compiler faithful to the spec, never the spec correct. verify_multitarget's operands were `uniform(-4, 4)` -- off 35..41, six of 81 exponents. Widened to 16 of 81 across the full range by APPENDING pairs, so the existing 600 stay byte-identical: 1744 pairs, still green; negative control gives 12 mismatches on a mutated model. New `tri pointers`: prose pointers ("see X", "cf. X") that do not resolve. Every path-shaped string was measured first -- 873 mentions, 409 unresolved, mostly paths a program creates -- and discarded as noise. The narrow form gives 193 and 16. Its first run flagged its own docstring; the docstring was reworded rather than the tool special-cased.
Contributor
PR DashboardGenerated at: 2026-08-24 03:51:48 UTC
Summary
Seal Status
|
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
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.
Closing the sticky finding I wrote, in a merged pull request:
git log --all -- board/bpseq.vis empty. That path has never existed in this repository. I repeated a pointer out of the file's own docstring without checking it resolved, and then used it as the reason not to fix a rule I had just shown to be wrong.A wrong pointer is worse than a missing one. A missing one sends a reader looking; a wrong one makes them stop — and it stopped me at exactly the moment I was deciding whether a defect was real.
What the counterpart actually is
specs/ternary/gft_sadd.t27. Measured this tick:specs/ternary/(hm, lm, d)for sixhoThe spec's barrel shift (
8/4/2/1, capped) and this file's 12-step loop are different code reaching identical results. So the generated Verilog, C and Rust all carry the same dormant wrong rule.The bit-exactness suite cannot see this, by construction
verify_multitargetandverify_emit_bitexactprove Verilog, C and Rust agree with the Python model. They prove the compiler faithful to the spec; they can never say the spec is right. A defect written in the spec propagates to every target and the suite stays green — that is the suite working, not failing.ALL TARGETS BIT-EXACTis a true sentence that reads as "the arithmetic is verified". It is worth exactly what it says.One narrowness that was fixable
The suite's operands were
uniform(-4, 4)— measured, that isoff35..41, six of the format's 81 exponents. A divergence that only appears when operands are decades apart had never been in front of it.Widened to 16 of 81 across the full range, appending pairs rather than reseeding so the existing 600 stay byte-identical — trading coverage for coverage is not adding it. 1744 pairs, still green, and the negative control confirms it still reddens: 12 mismatches on a mutated model.
I had also guessed the suite was blind to rounding ties. Measured: 20 of 256 pairs land on
rem == half. The guess was wrong and the measurement was cheap — the blind spot was one dimension over from where I expected it.New:
tri pointersThe obvious version — check every path-shaped string — was measured first: 873 mentions, 409 unresolved, dominated by paths a program creates and fixture names inside unit tests. A report that is 95% noise gets switched off, and the 5% goes with it.
Narrowing to a prose pointer (
see X,cf. X,documented in X): 193 mentions, 16 unresolved — a list a person can read, each row written on purpose. The narrowing was chosen by measuring both, not by taste. Against the pre-fix commit it flags the pointer that occasioned it.It caught its own docstring
The first run reported the new tool's own docstring, which quoted "see
board/bpseq.v" while explaining the bug. Second time in two days that a checker read its own documentation as data.A special case for the tool's own file would have hidden the same thing in the next document that discusses pointers, so the fix went where it belongs: the docstring no longer spells the path after a cue word, and it says why. Both times the tell was a count one higher than it should have been — not the list.
Refs #2161