From a2d2ec897543d90987970a7deceb1cd60ccd0dd1 Mon Sep 17 00:00:00 2001 From: lab Date: Tue, 8 Sep 2026 04:47:33 +0700 Subject: [PATCH] fix(spec): sim_time_ns must saturate, as its hand-written model always 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 --- .trinity/seals/Simulator.json | 14 +++++------ .trinity/seals/fpga_Simulator.json | 12 +++++----- ...ong-and-the-hand-written-copy-was-right.md | 9 +++++++ specs/fpga/simulator.t27 | 24 +++++++++++++++++-- 4 files changed, 44 insertions(+), 15 deletions(-) create mode 100644 docs/now/2026-09-08-the-spec-was-wrong-and-the-hand-written-copy-was-right.md diff --git a/.trinity/seals/Simulator.json b/.trinity/seals/Simulator.json index 4b195b5fcd..80f07fc7f8 100644 --- a/.trinity/seals/Simulator.json +++ b/.trinity/seals/Simulator.json @@ -1,11 +1,11 @@ { - "gen_hash_c": "sha256:b92ccd2f541925122daaed81d4b240c1fa808da7f5772a542873209a97995fcb", - "gen_hash_rust": "sha256:c7999edb0d905ff1b7a6f84e7705b267512e0614d92c1c197fea9bc4bba26e79", - "gen_hash_verilog": "sha256:ed8d3af2735e81efd9bcd16b1c855b3241d961fc70a7b7476fde7d57bc07ce79", - "gen_hash_zig": "sha256:c56746c59698981521b8be80cf50173b48e5d4bb2c8b925c529f3ac915ea44ae", + "gen_hash_c": "sha256:b21ac15c5e5dec080fcd73ce085f680e06f4f8f15c0c71fa4836693ca853aae7", + "gen_hash_rust": "sha256:698e3d72f93cccbc0c627531211b6c74e6831347db9befa08b59875b5d8f3d06", + "gen_hash_verilog": "sha256:b8279fcbcc44488f5dd4adb5a934fba3a3588e91afc27f7b5ef43cc6bedec2b7", + "gen_hash_zig": "sha256:47fbae2a42e449ff38941a5fff20e8bc85cf0cfe5842d6c73a2525bbc26641a2", "module": "Simulator", "ring": 12, - "sealed_at": "2026-08-28T18:19:55Z", - "spec_hash": "sha256:b4ab0ea0b34b210665affbbcecf0346f0c9258c849e96a1ab10ed431bac596a5", + "sealed_at": "2026-09-07T21:46:15Z", + "spec_hash": "sha256:806c0c899f339d4bd4b1c2c6c6aab2bcd60409eabc76eb169bcf7a752d9bee1d", "spec_path": "specs/fpga/simulator.t27" -} +} \ No newline at end of file diff --git a/.trinity/seals/fpga_Simulator.json b/.trinity/seals/fpga_Simulator.json index 5f03efd4ce..98a9f1d139 100644 --- a/.trinity/seals/fpga_Simulator.json +++ b/.trinity/seals/fpga_Simulator.json @@ -1,12 +1,12 @@ { - "gen_hash_c": "sha256:b92ccd2f541925122daaed81d4b240c1fa808da7f5772a542873209a97995fcb", - "gen_hash_rust": "sha256:c7999edb0d905ff1b7a6f84e7705b267512e0614d92c1c197fea9bc4bba26e79", - "gen_hash_verilog": "sha256:ed8d3af2735e81efd9bcd16b1c855b3241d961fc70a7b7476fde7d57bc07ce79", - "gen_hash_zig": "sha256:c56746c59698981521b8be80cf50173b48e5d4bb2c8b925c529f3ac915ea44ae", + "gen_hash_c": "sha256:b21ac15c5e5dec080fcd73ce085f680e06f4f8f15c0c71fa4836693ca853aae7", + "gen_hash_rust": "sha256:698e3d72f93cccbc0c627531211b6c74e6831347db9befa08b59875b5d8f3d06", + "gen_hash_verilog": "sha256:b8279fcbcc44488f5dd4adb5a934fba3a3588e91afc27f7b5ef43cc6bedec2b7", + "gen_hash_zig": "sha256:47fbae2a42e449ff38941a5fff20e8bc85cf0cfe5842d6c73a2525bbc26641a2", "module": "Simulator", "ring": 12, - "sealed_at": "2026-09-06T04:36:42Z", + "sealed_at": "2026-09-07T21:46:15Z", "sealed_by": "t27c-bootstrap@0.2.0", - "spec_hash": "sha256:b4ab0ea0b34b210665affbbcecf0346f0c9258c849e96a1ab10ed431bac596a5", + "spec_hash": "sha256:806c0c899f339d4bd4b1c2c6c6aab2bcd60409eabc76eb169bcf7a752d9bee1d", "spec_path": "specs/fpga/simulator.t27" } \ No newline at end of file diff --git a/docs/now/2026-09-08-the-spec-was-wrong-and-the-hand-written-copy-was-right.md b/docs/now/2026-09-08-the-spec-was-wrong-and-the-hand-written-copy-was-right.md new file mode 100644 index 0000000000..7ed3bdf975 --- /dev/null +++ b/docs/now/2026-09-08-the-spec-was-wrong-and-the-hand-written-copy-was-right.md @@ -0,0 +1,9 @@ +# NOW -- The spec was wrong and the hand-written copy was right (2026-09-08) + +## The spec was wrong and the hand-written copy was right (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 on the same inputs: **1190 cases, 126 disagreed.** `sim_time_ns` wraps in the spec where the hand-written model saturates -- at 2_000_000_000 cycles on the default 100 MHz clock, 20_000_000_000 ns becomes **2_820_130_816** instead of **4_294_967_295**. +- The spec states the assumption that fails, in a comment on the line above it: *"Widen the intermediate to u64 and narrow the **(small)** result back."* It is not always small. The hand-written author guarded it; the spec did not. After adding the guard: **1190 of 1190 agree**, with a harness control proving it can see a difference. +- **Ten of seventeen `rings/*` crates name a spec that exists**, and the overlap is wildly uneven: ring-090 shares **21 of 22** declared items and **15 of 16 signatures byte-identical**; ring-097 11 of 18; ring-098 5 of 12 with **2 items only in the spec**; ring-088 and ring-101 share **zero** with `gf16.t27` -- they name a spec they were never generated from. The closest pair in the repository had still drifted in behaviour, which is what a name-level comparison could never have shown. +- Two guards from the previous two passes proved themselves on this change, on their first real case: `check_seal_currency.py` (#3416) named `Simulator.json` and its two stale hashes the moment the spec was edited, and the `--save` duplicate maintenance (#3419) updated **both** `fpga_Simulator.json` and `Simulator.json`, reporting "and 1 other seal file". Neither needed a human to remember. +- Two tests added to the spec itself, in its own language rather than around it: the saturating case and an exact case below the ceiling. Both reach the Zig output. diff --git a/specs/fpga/simulator.t27 b/specs/fpga/simulator.t27 index 5fc7317da0..a6767fafa1 100644 --- a/specs/fpga/simulator.t27 +++ b/specs/fpga/simulator.t27 @@ -139,10 +139,30 @@ module Simulator { } // `cycles * 1000000000` overflows u32 for cycles >= 5: at cycles=100 // the product is 100_000_000_000 against a u32 max of 4_294_967_295. - // Widen the intermediate to u64 and narrow the (small) result back. - return ((cycles as u64) * 1000000000 / (cfg.clock_freq_hz as u64)) as u32; + // Widen the intermediate to u64 -- and then SATURATE, because the + // result is not always small: at 2_000_000_000 cycles on a 100 MHz + // clock it is 20_000_000_000, and a bare `as u32` wraps it to + // 2_820_130_816. The hand-written model in rings/ring-090-rust, which + // this spec is supposed to define, has always had that guard; the spec + // did not, and the two disagreed on 126 of 1190 differential cases. + var ns : u64 = (cycles as u64) * 1000000000 / (cfg.clock_freq_hz as u64); + if (ns > 4294967295) { + return 4294967295; + } + return ns as u32; } + // The case that made the spec and rings/ring-090-rust disagree: at + // 2_000_000_000 cycles on the default 100 MHz clock the nanosecond count is + // 20_000_000_000, and a bare `as u32` wraps it to 2_820_130_816. + test "sim_time_ns_saturates_instead_of_wrapping" + const cfg = sim_config("sat", 0); + assert(sim_time_ns(cfg, 2000000000) == 4294967295); + + test "sim_time_ns_is_exact_below_the_ceiling" + const cfg2 = sim_config("exact", 0); + assert(sim_time_ns(cfg2, 100) == 1000); + fn sim_time_us(cfg: SimConfig, cycles: u32) -> u32 { return sim_time_ns(cfg, cycles) / 1000; }