feat(tools): generate the differential harness a CONVERGED pair still needs - #3425
Merged
Conversation
… needs Closes #3424 Refs #3420 check_ring_spec_drift.py reports CONVERGED when every shared function has an identical signature, and carries a warning it earned: ring-090 measured CONVERGED at 16 of 16 identical and still disagreed with its spec on 126 of 1190 differential cases. Only running both found it, and that harness was written by hand for one pair. This writes it. For a CONVERGED pair it emits a Rust program including both modules, calls every shared function on the same synthesised inputs, and compares. ring-090 / specs/fpga/simulator.t27 936 cases, all agree, 16 of 16, 0 refused ring-099 / specs/pipeline/e2e_test.t27 25 cases, all agree, 4 of 4, 0 refused The control ran on the live pair, not only a fixture: re-introducing the exact defect #3421 repaired -- deleting the saturation guard from the spec -- makes the tool report `936 cases, agree 864, disagree 72`, name sim_time_ms, and exit 1. Restoring it returns 936/936 and exit 0. Three design points, each because the naive version would have lied: * It REFUSES rather than skips. A parameter or return type it cannot synthesise is named and the run exits 2. A harness covering eight of sixteen functions and printing "agree" is worse than no harness, because the eight it dropped are where a difference hides. * A panic is a DISAGREEMENT. Both calls run under catch_unwind with -C overflow-checks=on. Without it the process dies with no output, which reads as "no cases run" rather than as the sharpest difference there is; a release build would wrap silently in both and hide it. * Structs are built by their PRODUCERS -- SimConfig comes from calling sim_config with the same grid -- so the generator needs no knowledge of fields, which is how the hand-written harness did it. Stated rather than hidden: ring-099's 25 cases are thin. Its functions take &mut slices and the generator passes zero-initialised buffers, so values are compared after the call but the inputs are not varied. 25 is not the evidence 936 is. Also reported rather than done silently: 55 inner doc-comment and attribute lines are stripped from ring-090 (3 from ring-099) so the crate can be `include!`d as a module. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
gHashTag
enabled auto-merge (squash)
September 7, 2026 22:19
Contributor
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.
Closes #3424 · Refs #3420
check_ring_spec_drift.pyreports CONVERGED on identical signatures, and carries a warning it earned:That harness was written by hand, for one pair. This writes it.
Results
ring-090/simulator.t27ring-099/e2e_test.t27The control ran on the live pair, not only a fixture
Re-introducing the exact defect #3421 repaired — deleting the saturation guard from the spec:
exit 1. Restoring it: 936/936, exit 0.
--self-checkproves two synthetic properties besides: modules differing by construction are reported as disagreeing, and an unsynthesisable parameter is REFUSED rather than passed over.Three design points, each because the naive version would have lied
catch_unwindwith-C overflow-checks=on. Without it the process dies with no output at all, which reads as "no cases run" rather than as the sharpest difference there is; a release build would wrap silently in both and hide it.SimConfigcomes from callingsim_configwith the same grid, so the generator needs no knowledge of fields — which is how the hand-written harness did it.Stated, not hidden
ring-099s 25 cases are thin. Its functions take&mut [u8],&mut [bool],&mut usize, and the generator passes zero-initialised buffers: values are compared after the call, but the inputs are not varied. 25 is not the evidence 936 is, and a buffer grid is the obvious next step.It also reports that it strips inner doc comments and attributes from the ring crate — 55 lines for ring-090, 3 for ring-099 — because
include!inside amodrejects them. Editing someone elses file to run a test should be visible.One process note
Fifth time this session I wrote
exit=$?after a pipe and readgreps status. It told me the tool exited 0 while printing 72 disagreements. Measured without the pipe, it exits 1.