From 3e94a60a6b292498aa582e2cd56f9d164cb1c00d Mon Sep 17 00:00:00 2001 From: Vasilev Dmitrii Date: Tue, 18 Aug 2026 22:20:16 +0700 Subject: [PATCH] verify: enumerate pack3, xor2 and sign0 -- 50.6M inputs exhaustive The machinery from #2198/#2200/#2202 is built; this applies it to three more primitives, none of which had any cross-target check before this line of work. full_adder 16,777,216 model == C == Rust; Verilog on a labelled slice maj3 16,777,216 model == C == Rust; Verilog on a labelled slice pack3 16,777,216 model == C == Rust [new] tmul 65,536 four arms, exhaustive xor2 65,536 four arms, exhaustive [new] sign0 65,536 four arms, exhaustive [new] pack2 65,536 model == C == Rust negate 256 four arms, exhaustive 50,594,048 inputs exhaustive across model/C/Rust, of which 196,864 across four independent implementations. A bug caught before it ran, which would have made the tool agree with itself. The Verilog testbench generator sliced every loop variable as i0[7:0], hardcoded to a byte. sign0 takes i16. It would have compiled, run, produced a digest, and compared a NARROWER function than the C and Rust arms evaluated -- Verilog truncating its argument to 8 bits while the others used 16. The digests would then disagree for a reason that has nothing to do with the backends, or agree by luck on some domain and be trusted. The width now comes from the declared type. That is this line's own failure mode, located in the checker rather than the checked: a harness that measures something other than what it reports. pack2 and pack3 return u64. The C and Rust folds take the low 32 bits; a matching Verilog fold needs a 64-bit accumulator. They stay three-way and are labelled, rather than given an arm that quietly compares something narrower -- which is the mistake avoided immediately above. Also corrected in my own issue text: I wrote '262,400 across four implementations', having counted pack2's 65,536 despite it having only three arms. It is 196,864. Closes #2205 Refs #2204 Co-Authored-By: Claude Opus 5 --- docs/NOW.md | 13 +++++++++++++ tools/verify_exhaustive.py | 16 +++++++++++++--- 2 files changed, 26 insertions(+), 3 deletions(-) diff --git a/docs/NOW.md b/docs/NOW.md index abbc8aa71..b3e0e31b3 100644 --- a/docs/NOW.md +++ b/docs/NOW.md @@ -1,3 +1,16 @@ +# NOW -- three more primitives enumerated, and a width bug in the checker (2026-08-18) + +Last updated: 2026-08-18 + +## verify: pack3, xor2 and sign0 join the enumeration -- 50.6M inputs (Closes #2205) + +- **50,594,048 inputs covered exhaustively** by model/C/Rust, of which **196,864 across four independent implementations**. At the start of this line of work none of these specs had any cross-target check at all +- New: \`pack3\` at 16,777,216 (three-way), \`xor2\` and \`sign0\` at 65,536 each (**four-way, exhaustive**) +- **A bug caught before it ran, which would have made the tool agree with itself.** The Verilog testbench generator sliced every loop variable as \`i0[7:0]\`, hardcoded to a byte. \`sign0\` takes \`i16\`. It would have compiled, run, produced a digest, and compared a **narrower function** than the C and Rust arms evaluated -- the Verilog arm truncating to 8 bits while the others used 16. The width now comes from the argument's declared type +- That is this line's own failure mode, in the checker rather than the checked: **a harness that measures something other than what it reports** +- \`pack2\` and \`pack3\` return u64; the C and Rust folds take the low 32 bits and a matching Verilog fold needs a 64-bit accumulator. They stay three-way and are **labelled**, rather than given an arm that quietly compares something narrower -- the mistake avoided just above +- Caught in my own issue text too: I wrote "262,400 across four implementations", which had counted \`pack2\`'s 65,536 despite it having only three arms. The figure is 196,864 + # NOW -- when enumeration beats a prover, and the nightly that uses it (2026-08-18) Last updated: 2026-08-18 diff --git a/tools/verify_exhaustive.py b/tools/verify_exhaustive.py index e45a75c47..a2af288d3 100755 --- a/tools/verify_exhaustive.py +++ b/tools/verify_exhaustive.py @@ -58,9 +58,14 @@ (RIP, "maj3", [U8] * 3, (False, 8)), (RIP, "tmul", [U8] * 2, (True, 8)), (RIP, "negate", [U8], (False, 8)), - # pack2 returns u64; the fold takes the low 32 bits in C and Rust, and a 64-bit - # Verilog reg would need a wider fold to match. Left two-and-model until then. + (RIP, "xor2", [U8] * 2, (False, 8)), + # sign0 takes i16, so its domain is the signed 16-bit range rather than a byte. + (RIP, "sign0", [("int16_t", "i16", -32768, 32767)], (False, 8)), + # pack2 and pack3 return u64. The C and Rust folds take the low 32 bits; a matching + # Verilog fold needs a 64-bit accumulator, so those stay model+C+Rust and are + # labelled 3-way rather than given an arm that compares something narrower. ("specs/ternary/ternary_xor.t27", "pack2", [U8] * 2, None), + (RIP, "pack3", [U8] * 3, None), ] @@ -177,7 +182,12 @@ def verilog_program(vsrc, fn, args, ret_signed, ret_bits): for i in range(len(args)): loops.append(f" for (i{i} = {args[i][2]}; i{i} <= {args[i][3]}; i{i} = i{i} + 1)") close.append("") - call = ", ".join(f"i{i}[7:0]" for i in range(len(args))) + # Slice each loop variable to the argument's declared width. This was hardcoded + # to [7:0] and would have silently truncated sign0's i16 argument to a byte -- + # the tool would have compared a narrower function than the C and Rust arms did, + # and agreed with itself about it. + widths = {"u8": 8, "i8": 8, "u16": 16, "i16": 16, "u32": 32, "i32": 32} + call = ", ".join(f"i{i}[{widths.get(args[i][1], 8) - 1}:0]" for i in range(len(args))) decl = " ".join(f"integer i{i};" for i in range(len(args))) # sign-extend a signed return to 32 bits so the fold matches the C/Rust one ext = (f"{{{{{32 - ret_bits}{{r[{ret_bits - 1}]}}}}, r}}" if ret_signed