nx_recip_synth_test.nx source

1// nx_recip_synth_test.nx -- TRIANGULATED validation of the Newton-Raphson 2// reciprocal divider instantiated as an NxGsim GATE-NETWORK (nx_recip_synth.nx). 3// 4// Three INDEPENDENT legs must agree on every vector (a bug would have to fool 5// all three), exactly mirroring how nx_alu_divider_test proves the restoring 6// divider gate-network and how nx_alu_divider_newton proves the scalar math: 7// LEG A the GATE-NETWORK Newton divider, run through nx_nxgate_sim (q and r) 8// LEG B an independent restoring (shift-subtract) divider, SCALAR (a DIFFERENT 9// algorithm -- the radix-2 reference) 10// LEG C the i64 oracle / and % 11// Battery = the SAME 2,297,160-vector triangulation the scalar proof passed: 12// dense D in [1,256] x N in [0,8191] (2,097,152 vectors) 13// + 200,000 random full-range W=16 (N,D in [1,65535]) 14// + 8 explicit edges 15// Known answer (FAIL LOUD): "<ok> <total> <q_chk> <r_chk>", ok must == total. 16// On success prints e.g. "2297160 2297160 3 1" and sys_exit(0); any mismatch 17// prints the bad counts and exits non-zero. 18 19import "nx_recip_synth.nx" 20 21const RT_W: i64 = 16 22const RT_LCG_A: i64 = 6364136223846793005 23const RT_LCG_C: i64 = 1442695040888963407 24 25func _emit_num(v: i64) -> i64 { 26 let b: *u8 = sys_mmap(28); var n: i64 = v; if n < 0 { n = 0 - n } 27 let t2: *u8 = sys_mmap(28); var t: i64 = 0 28 if n == 0 { t2[0] = 48; t = 1 } 29 while n > 0 { t2[t] = 48 + (n % 10); n = n / 10; t = t + 1 } 30 var i: i64 = 0; while i < t { b[i] = t2[t - 1 - i]; i = i + 1 } 31 b[t] = 32; sys_write(1, b, t + 1); return 0 32} 33func _nl() -> i64 { let z: *u8 = sys_mmap(2); z[0] = 10; sys_write(1, z, 1); return 0 } 34 35// LEG B -- independent restoring (shift-subtract) divider, W=16, SCALAR. 36func rt_restoring(N: i64, D: i64) -> i64 { 37 var q: i64 = 0 38 var r: i64 = 0 39 var i: i64 = RT_W - 1 40 while i >= 0 { 41 r = (r << 1) | ((N >> i) & 1) 42 if r >= D { r = r - D; q = q | (1 << i) } 43 i = i - 1 44 } 45 return q 46} 47 48// run the prebuilt gate-network once for (N,D); returns the quotient net value, 49// writes the remainder net value to r_out[0]. 50func rt_run(g: *NxGsim, qnet: i64, rnet: i64, N: i64, D: i64, r_out: *i64) -> i64 { 51 g.vals[0] = N 52 g.vals[1] = D 53 if nx_gsim_run(g) != NX_GSIM_OK { r_out[0] = 0 - 1; return 0 - 1 } 54 r_out[0] = g.vals[rnet] 55 return g.vals[qnet] 56} 57 58func main() -> i64 { 59 // Build the gate-network ONCE; inputs are nets 0 (N) and 1 (D). The Newton 60 // divider at W=16 emits a few thousand cells, so size generously. 61 let vals: *i64 = sys_mmap(8 * 4096) as *i64 62 let cells: *NxGsimCell = sys_mmap(48 * 4096) as *NxGsimCell 63 let g: *NxGsim = sys_mmap(64) as *NxGsim 64 g.vals = vals; g.n_nets = 2; g.cells = cells; g.n_cells = 0 65 66 let ro_build: *i64 = sys_mmap(8) as *i64; ro_build[0] = 0 67 let qnet: i64 = nx_recip_div_synth(g, 0, 1, ro_build) 68 let rnet: i64 = ro_build[0] 69 70 let r_out: *i64 = sys_mmap(8) as *i64; r_out[0] = 0 71 72 var total: i64 = 0 73 var ok: i64 = 0 74 var q_chk: i64 = 0 // a sample quotient (D=3,N=12345) to print as a fixed KAT 75 var r_chk: i64 = 0 // a sample remainder for the same KAT 76 77 // dense exhaustive: D in [1,256], N in [0,8191] -- all 3 legs must agree 78 var D: i64 = 1 79 while D <= 256 { 80 var N: i64 = 0 81 while N <= 8191 { 82 let a: i64 = rt_run(g, qnet, rnet, N, D, r_out) // LEG A (gate-net q) 83 let ar: i64 = r_out[0] // LEG A (gate-net r) 84 let b: i64 = rt_restoring(N, D) // LEG B 85 let c: i64 = N / D // LEG C (oracle q) 86 let cr: i64 = N - (N / D) * D // LEG C (oracle r) 87 total = total + 1 88 if a == b { if a == c { if ar == cr { ok = ok + 1 } } } 89 N = N + 1 90 } 91 D = D + 1 92 } 93 94 // a printed fixed KAT (single known answer) for the summary line 95 q_chk = rt_run(g, qnet, rnet, 12345, 7, r_out) // 12345 / 7 = 1763 rem 4 96 r_chk = r_out[0] 97 98 // random full-range W=16: N,D in [1,65535] 99 var seed: i64 = 2463534242 100 var nr: i64 = 0 101 while nr < 200000 { 102 seed = seed * RT_LCG_A + RT_LCG_C; var N: i64 = seed & 65535 103 seed = seed * RT_LCG_A + RT_LCG_C; var D: i64 = (seed & 65535) 104 if D == 0 { D = 1 } 105 let a: i64 = rt_run(g, qnet, rnet, N, D, r_out) 106 let ar: i64 = r_out[0] 107 let b: i64 = rt_restoring(N, D) 108 let c: i64 = N / D 109 let cr: i64 = N - (N / D) * D 110 total = total + 1 111 if a == b { if a == c { if ar == cr { ok = ok + 1 } } } 112 nr = nr + 1 113 } 114 115 // edges 116 let en: *i64 = sys_mmap(8 * 8) as *i64 117 let ed: *i64 = sys_mmap(8 * 8) as *i64 118 en[0]=65535; ed[0]=1 119 en[1]=65535; ed[1]=65535 120 en[2]=65535; ed[2]=32768 121 en[3]=0; ed[3]=65535 122 en[4]=1; ed[4]=1 123 en[5]=65535; ed[5]=2 124 en[6]=12345; ed[6]=255 125 en[7]=65535; ed[7]=257 126 var e: i64 = 0 127 while e < 8 { 128 let a: i64 = rt_run(g, qnet, rnet, en[e], ed[e], r_out) 129 let ar: i64 = r_out[0] 130 let b: i64 = rt_restoring(en[e], ed[e]) 131 let c: i64 = en[e] / ed[e] 132 let cr: i64 = en[e] - (en[e] / ed[e]) * ed[e] 133 total = total + 1 134 if a == b { if a == c { if ar == cr { ok = ok + 1 } } } 135 e = e + 1 136 } 137 138 _emit_num(ok); _emit_num(total); _emit_num(q_chk); _emit_num(r_chk); _nl() 139 // FAIL LOUD: every gate-net result agrees 1:1 with BOTH the restoring divider 140 // and the i64 oracle (quotient AND remainder), over the full battery. 141 if ok != total { sys_exit(1); return 1 } 142 if total != 2297160 { sys_exit(2); return 2 } // dense 2097152 + 200000 + 8 143 if q_chk != 1763 { sys_exit(3); return 3 } // 12345/7 KAT quotient 144 if r_chk != 4 { sys_exit(4); return 4 } // 12345/7 KAT remainder 145 sys_exit(0); return 0 146}