Three more primitives enumerated: 50.6M inputs, and a width bug that would have made the tool agree with itself

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

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