nx_eqsat_rule_proof_test.nx source

1// nx_eqsat_rule_proof_test.nx -- SOVEREIGN soundness proof for the eqsat rewrite rules 2// (algebraic-normal-form leg). Models nx_alu_divider_proof_test.nx: a machine-checked exhaustive 3// small-width check, cross-checked by triangulation legs that all run through nx_gsim (independent 4// of NishiLang `*`/`<<` codegen, because they go via the netlist). 5// 6// WORKED EXAMPLE: certify mul x 8 == shl x 3 BY PROOF (not by battery): build the LHS netlist 7// (MUL x 8) and the RHS netlist (SHL x 3), sweep x over a representative width, and require both 8// legs to equal a third independent oracle on EVERY vector. 9// 10// MIGRATED OFF A HAND-ROLLED VERDICT 2026-08-14, and it had NEVER BEEN COMPILED before that day -- 11// nor had nx_eqsat.nx itself, which did not compile at all (a module const read 470 lines above its 12// declaration). So this proof existed on disk, fully written, and had never once run. 13// 14// A NEGATIVE CONTROL WAS ADDED IN THE SAME PASS. The original asserted only that the sound pair 15// AGREES on all 256 vectors. A triangulator that returned pass for everything would have scored 16// full marks -- the gates-green-on-garbage class. The control sweeps an UNSOUND pair (mul x 8 vs 17// shl x FOUR, off by one bit) through the same machinery and requires it to DISAGREE, so a pass on 18// the sound pair now means the comparison can actually fail. 19// license_tier: ORIGINAL expect_exit: 0 20import "nx_gate_verdict.nx" 21import "nx_alu_divider.nx" 22import "nx_triangulate.nx" 23 24const PW: i64 = 8 // representative width: sweep x in [0, 2^PW) 25const PW_VECTORS: i64 = 256 // 2^PW -- named so the anti-vacuity tooth reads as arithmetic, not a magic literal 26 27// Build a fresh single-input gsim with net 0 = x (primary input). 28func _mk(vals: *i64, cells: *NxGsimCell, g: *NxGsim) -> i64 { 29 g.vals = vals; g.n_nets = 1; g.cells = cells; g.n_cells = 0; return 0 30} 31 32func main() -> i64 { 33 gv_head("nx_eqsat rule-soundness gate -- triangulated exhaustive proof of mul-to-shl strength reduction" as *u8) 34 let ctr: *i64 = gv_ctr() 35 36 let vals: *i64 = sys_mmap(64 * 8) as *i64 37 let cells: *NxGsimCell = sys_mmap(64 * 48) as *NxGsimCell 38 let g: *NxGsim = sys_mmap(64) as *NxGsim 39 40 var total: i64 = 0 41 var proven: i64 = 0 42 var unsound_disagreements: i64 = 0 43 var run_ok: i64 = 1 44 let hi: i64 = 1 << PW // 2^PW 45 46 var x: i64 = 0 47 while x < hi { 48 // LEG A (LHS): MUL x 8 via the netlist (independent of native `*`) 49 _mk(vals, cells, g) 50 let c8: i64 = div_const(g, 8) 51 let prod: i64 = div_op2(g, NX_GATE_KIND_MUL, 0, c8) 52 g.vals[0] = x 53 if nx_gsim_run(g) != NX_GSIM_OK { run_ok = 0 } 54 let lhs: i64 = g.vals[prod] 55 56 // LEG B (RHS): SHL x 3 via the netlist (independent of native `<<`) 57 _mk(vals, cells, g) 58 let c3: i64 = div_const(g, 3) 59 let shft: i64 = div_op2(g, NX_GATE_KIND_SHL, 0, c3) 60 g.vals[0] = x 61 if nx_gsim_run(g) != NX_GSIM_OK { run_ok = 0 } 62 let rhs: i64 = g.vals[shft] 63 64 // ORACLE: x * 8 computed directly (third independent source) 65 let oracle: i64 = x * 8 66 67 // Triangulate: 2 independent netlist legs must BOTH equal the oracle. 68 let legs: *i64 = sys_mmap(2 * 8) as *i64 69 legs[0] = lhs 70 legs[1] = rhs 71 let v: *NxTriVerdict = sys_mmap(64) as *NxTriVerdict 72 let rc: i64 = nx_tri_pass_strict(legs, 2, oracle, 2, v) 73 total = total + 1 74 if rc == 1 { proven = proven + 1 } 75 76 // NEGATIVE CONTROL, same machinery, deliberately WRONG shift amount. 77 _mk(vals, cells, g) 78 let c4: i64 = div_const(g, 4) 79 let bad: i64 = div_op2(g, NX_GATE_KIND_SHL, 0, c4) 80 g.vals[0] = x 81 if nx_gsim_run(g) != NX_GSIM_OK { run_ok = 0 } 82 if g.vals[bad] != oracle { unsound_disagreements = unsound_disagreements + 1 } 83 84 x = x + 1 85 } 86 87 gv_check("every swept vector triangulates: two netlist legs and the oracle agree" as *u8, proven == total, ctr) 88 // BIND THE AGGREGATE TO ITS DENOMINATOR. proven==total is trivially true over an EMPTY sweep, 89 // so the count itself has to be asserted or the tooth passes on the empty set. 90 gv_check("the sweep actually covered all 2^PW vectors" as *u8, total == PW_VECTORS, ctr) 91 gv_check("every netlist evaluation completed" as *u8, run_ok == 1, ctr) 92 // WITHOUT THIS THE GATE IS VACUOUS: it proves the comparison can return NOT-equal, so the 93 // agreement above is a finding rather than a constant. 94 gv_check("neg-control-unsound-shift-by-4-DISAGREES-with-mul-by-8" as *u8, unsound_disagreements > 0, ctr) 95 96 return gv_verdict("nx_eqsat_rule_proof_test" as *u8, ctr, 97 "exhaustive 256-vector triangulated proof of mul-to-shl, with an unsound-pair control proving the comparison can fail" as *u8) 98}