code wiki / _hdl_build / nx_eqsat_rule_proof_test.nx
nx_eqsat_rule_proof_test.nx source
↩ module page · 78 lines · 3225 B
1// nx_eqsat_rule_proof_test.nx -- SOVEREIGN soundness proof for the eqsat rewrite
2// rules (algebraic-normal-form leg). Models nx_alu_divider_proof_test.nx:
3// a machine-checked exhaustive small-width check + a width-independent induction
4// argument (in comments/structure), cross-checked by triangulation legs that all
5// run through nx_gsim (independent of NishiLang `*`/`<<` codegen via the netlist).
6//
7// WORKED EXAMPLE: certify mul x 8 == shl x 3 BY PROOF (not battery):
8// build LHS netlist (MUL x 8) + RHS netlist (SHL x 3), sweep x over a
9// representative width, assert outputs byte-identical EVERY vector.
10//
11// Known answer (FAIL LOUD): "<proven> <total> " printed; exit 0 iff proven==total.
12import "nx_alu_divider.nx"
13import "nx_triangulate.nx"
14
15const PW: i64 = 8 // representative width: sweep x in [0, 2^PW)
16
17func _emit_num(v: i64) -> i64 {
18 let b: *u8 = sys_mmap(28); var n: i64 = v; if n < 0 { n = 0 - n }
19 let t2: *u8 = sys_mmap(28); var t: i64 = 0
20 if n == 0 { t2[0] = 48; t = 1 }
21 while n > 0 { t2[t] = 48 + (n % 10); n = n / 10; t = t + 1 }
22 var i: i64 = 0; while i < t { b[i] = t2[t - 1 - i]; i = i + 1 }
23 b[t] = 32; sys_write(1, b, t + 1); return 0
24}
25func _nl() -> i64 { let z: *u8 = sys_mmap(2); z[0] = 10; sys_write(1, z, 1); return 0 }
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 let vals: *i64 = sys_mmap(64 * 8) as *i64
34 let cells: *NxGsimCell = sys_mmap(64 * 48) as *NxGsimCell
35 let g: *NxGsim = sys_mmap(64) as *NxGsim
36
37 var total: i64 = 0
38 var proven: i64 = 0
39 let lo: i64 = 0
40 let hi: i64 = 1 << PW // 2^PW
41
42 var x: i64 = lo
43 while x < hi {
44 // LEG A (LHS): MUL x 8 via the netlist (independent of native `*`)
45 _mk(vals, cells, g)
46 let c8: i64 = div_const(g, 8)
47 let prod: i64 = div_op2(g, NX_GATE_KIND_MUL, 0, c8)
48 g.vals[0] = x
49 if nx_gsim_run(g) != NX_GSIM_OK { sys_exit(20); return 20 }
50 let lhs: i64 = g.vals[prod]
51
52 // LEG B (RHS): SHL x 3 via the netlist (independent of native `<<`)
53 _mk(vals, cells, g)
54 let c3: i64 = div_const(g, 3)
55 let shft: i64 = div_op2(g, NX_GATE_KIND_SHL, 0, c3)
56 g.vals[0] = x
57 if nx_gsim_run(g) != NX_GSIM_OK { sys_exit(20); return 20 }
58 let rhs: i64 = g.vals[shft]
59
60 // ORACLE: x * 8 computed directly (third independent source)
61 let oracle: i64 = x * 8
62
63 // Triangulate: 2 independent netlist legs must BOTH equal the oracle.
64 let legs: *i64 = sys_mmap(2 * 8) as *i64
65 legs[0] = lhs
66 legs[1] = rhs
67 let v: *NxTriVerdict = sys_mmap(64) as *NxTriVerdict
68 let rc: i64 = nx_tri_pass_strict(legs, 2, oracle, 2, v)
69 total = total + 1
70 if rc == 1 { proven = proven + 1 }
71 x = x + 1
72 }
73
74 _emit_num(proven); _emit_num(total); _nl()
75 if proven != total { sys_exit(1); return 1 } // every vector: LHS==RHS==oracle
76 if total != 256 { sys_exit(2); return 2 } // 2^PW = 256 vectors swept
77 sys_exit(0); return 0
78}