Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 7 additions & 7 deletions .trinity/seals/Simulator.json
Original file line number Diff line number Diff line change
@@ -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"
}
}
12 changes: 6 additions & 6 deletions .trinity/seals/fpga_Simulator.json
Original file line number Diff line number Diff line change
@@ -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"
}
Original file line number Diff line number Diff line change
@@ -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.
24 changes: 22 additions & 2 deletions specs/fpga/simulator.t27
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}
Expand Down
Loading