fix(spec): sim_time_ns must saturate, as its hand-written model always did - #3421
Merged
Conversation
…s did Closes #3420 rings/ring-090-rust says in its own doc comment that it is "faithful to the spec" specs/fpga/simulator.t27. A differential harness driving every shared function from both modules on the same inputs -- 14 u32 values crossed with 3 name strings -- disagreed on 126 of 1190 cases. sim_time_ns 4/10 2_000_000_000 -> hand 4294967295, spec 2820130816 sim_time_us 1/10 -> hand 4294967, spec 2820130 sim_time_ms 1/10 -> hand 4294, spec 2820 cycles_for_time_ns 0/10 The hand-written model widens to u64 and then saturates. The spec widened and then narrowed with a bare `as u32`, which wraps: at 2_000_000_000 cycles on the default 100 MHz clock, 20_000_000_000 ns becomes 2_820_130_816. The spec states the assumption that fails, in a comment on the line above: "Widen the intermediate to u64 and narrow the (small) result back." It is not always small. With the guard, the harness reports 1190 of 1190 agreeing, and its control confirms it can see a difference. Context for why this was worth looking for. Ten of the seventeen rings/* crates name a spec that exists in this repository, and the overlap between them is wildly uneven: ring-090 22 hand items, 21 shared, 0 spec-only <- 15/16 signatures identical ring-097 18 hand items, 11 shared, 0 spec-only ring-099 9 hand items, 4 shared, 0 spec-only ring-098 12 hand items, 5 shared, 2 spec-only ring-088 3 hand items, 0 shared <- names gf16.t27, unrelated ring-101 5 hand items, 0 shared <- same ring-090 is the closest pair in the repository and it had still drifted in BEHAVIOUR, which a comparison of names and signatures alone could never show. Two tests are added to the spec in its own language rather than around it: the saturating case and an exact case below the ceiling. Both reach the Zig output. The seal was refreshed by `t27c seal --save`, which reported "and 1 other seal file(s) naming the same spec" and updated both fpga_Simulator.json and Simulator.json -- the repair from #3419 on its first real case, after check_seal_currency.py from #3416 named the stale hashes. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
gHashTag
enabled auto-merge (squash)
September 7, 2026 21:48
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
Contributor
This was referenced Sep 7, 2026
Closed
gHashTag
added a commit
that referenced
this pull request
Sep 7, 2026
… needs (#3425) 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: lab <lab@example.com> Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
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 #3420
rings/ring-090-rustsays in its own doc comment that it is "faithful to the spec"specs/fpga/simulator.t27. It is not — and the spec is the one that is wrong.Measured
A differential harness driving every shared function from both modules on the same inputs — 14
u32values crossed with 3 name strings:sim_time_ns2_000_000_000→ hand 4294967295, spec 2820130816sim_time_ussim_time_mscycles_for_time_nsCause
The hand-written model widens to
u64and then saturates. The spec widened and then narrowed with a bareas u32, which wraps: at 2,000,000,000 cycles on the default 100 MHz clock, 20,000,000,000 ns becomes 2,820,130,816.The spec states the assumption that fails, in a comment on the line above it:
It is not always small. With the guard: 1190 of 1190 agree.
Why this was worth looking for
Ten of the seventeen
rings/*crates name a spec that exists in this repository, and the overlap is wildly uneven:gf16.t27, unrelatedring-090is the closest pair in the repository — and it had still drifted in behaviour. A comparison of names and signatures alone would have called it a match; only running both did.Tests
Two, added to the spec in its own language rather than around it — the saturating case and an exact case below the ceiling. Both reach the Zig output.
Two guards from the last two passes earned their keep here
Neither needed a human to remember:
check_seal_currency.py(fix(seals): refresh 116 stale generated-code hashes, and check them from now on #3416) namedSimulator.jsonand its two stale hashes the moment the spec was edited.t27c seal --save(fix(seal): --save maintains every seal naming the spec, and never twins by case #3419) reported "and 1 other seal file(s) naming the same spec" and updated bothfpga_Simulator.jsonandSimulator.json— its first real case.