test: add sadd cancellation edge to the cross-target proof

docs/NOW.md

@@ -1,7 +1,13 @@
-# NOW — test: cross-target verification hardened to EXTREME operands (2026-08-07)
+# NOW — test: cross-target coverage adds the sadd cancellation edge (2026-08-07)
 
 Last updated: 2026-08-07
 
+## test: verify_multitarget covers exact/near cancellation (a, -a) (Refs #1764)
+
+- Added a targeted edge to the cross-target proof: `gen_pairs` now injects ~20% CANCELLATION pairs `(v, neg(v))` -> `sadd` exact-cancels to 0, plus near-cancellation `(v, neg(v'))`. This is the historically buggy magsub path (cycle 17 found a negative-zero bug when the larger operand is negative and the result is exactly 0) and the magsub-normalize hot path
+- Result: model `smul`/`sadd` == the C and Rust emissions BIT-EXACT on the cancellation edge too -- the fix holds across all backends. Combined with last cycle's extreme-operand coverage, the cross-target proof now spans moderate + extreme + cancellation operands
+- Context: this closes out the operand-space hardening motivated by (but orthogonal to) the bpseq silicon debug, which is confirmed a TIMING issue (nextpnr-xilinx XDC supports only create_clock -- no multicycle/generated-clock -- so bpseq needs a pipelined core or a real divided clock; documented). Tool-only. Refs #1764
+
 ## test: verify_multitarget covers the full GF-T range, not just [-4,4] (Refs #1764)
 
 - Motivated by the bpseq silicon debug: a hypothesis was that the microsequencer diverges on silicon because training-grown weights push operands into a saturation range where the Python GF-T model and the RTL might disagree (the cross-target proof only used moderate [-4,4] operands). Tested it: model smul/sadd vs the C emission over 1500 EXTREME operands (full offset span 0..127, both signs, saturation-adjacent) -- **0 mismatches, ALL MATCH.** So the model is a faithful RTL reference across the WHOLE range; the bpseq silicon divergence is NOT an arithmetic/operand-range bug (it is confirmed TIMING: iverilog stable, board core == verified gen-verilog, model == RTL on all operands)

tools/verify_multitarget.py

@@ -52,7 +52,16 @@ def gen_pairs(g):
     for _ in range(40):
         off = random.choice([0, 1, 2, 38, 39, 40, 41, 79, 80, 120, 126, 127])
         vals.append((random.randint(0, 1) << 16) | (off << 9) | random.randint(0, 511))
-    return [(random.choice(vals), random.choice(vals)) for _ in range(N)]
+    pairs = [(random.choice(vals), random.choice(vals)) for _ in range(N - N // 5)]
+    # CANCELLATION edge: (v, -v) -> sadd exact-cancel to 0 (a historically buggy
+    # magsub path -- negative-zero on the larger-operand-negative branch) and
+    # near-cancel (v, -v') for a neighbouring v' -> the magsub normalize hot path
+    for _ in range(N // 5):
+        v = random.choice(vals)
+        w = g.neg(v) if random.random() < 0.6 else g.neg(random.choice(vals))
+        pairs.append((v, w))
+    random.shuffle(pairs)
+    return pairs
 
 
 def py_ref(g, fn, pairs):