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; }