nx_recip_div24_test.nx source

1// nx_recip_div24_test.nx -- TRIANGULATED 1:1 proof of the W=24 Newton/Goldschmidt 2// reciprocal divider gate-network (nx_recip_div24_synth), the first rung that 3// composes the proven 64x64->128 wide multiplier (x*t overflows i64 at W=24). 4// 5// Three independent legs must agree on every vector (a bug would have to fool all 6// three): LEG A the GATE-NETWORK Newton divider via nx_nxgate_sim (q and r); 7// LEG B an independent restoring (shift-subtract) divider, W=24, SCALAR; LEG C 8// the i64 oracle / and %. Battery (2,297,160 vectors): dense D in [1,256] x 9// N in [0,8191] + 200,000 random FULL 24-bit (N,D in [1,2^24-1]) + 8 edges. 10// 11// Known answer (FAIL LOUD): "2297160 2297160 1763 4" rc=0 (ok total q_chk r_chk; 12// 12345/7 = 1763 rem 4). Built on the known-good compiler. 13 14import "nx_recip_div24.nx" 15 16const RT_W24: i64 = 16777215 // 2^24 - 1 17const RT_LCG_A: i64 = 6364136223846793005 18const RT_LCG_C: i64 = 1442695040888963407 19 20func _emit_num(v: i64) -> i64 { 21 let b: *u8 = sys_mmap(28); var n: i64 = v; if n < 0 { n = 0 - n } 22 let t2: *u8 = sys_mmap(28); var t: i64 = 0 23 if n == 0 { t2[0] = 48; t = 1 } 24 while n > 0 { t2[t] = 48 + (n % 10); n = n / 10; t = t + 1 } 25 var i: i64 = 0; while i < t { b[i] = t2[t - 1 - i]; i = i + 1 } 26 b[t] = 32; sys_write(1, b, t + 1); return 0 27} 28func _nl() -> i64 { let z: *u8 = sys_mmap(2); z[0] = 10; sys_write(1, z, 1); return 0 } 29 30// LEG B -- independent restoring divider, W=24, SCALAR. 31func rt_restoring(N: i64, D: i64) -> i64 { 32 var q: i64 = 0 33 var r: i64 = 0 34 var i: i64 = 23 35 while i >= 0 { 36 r = (r << 1) | ((N >> i) & 1) 37 if r >= D { r = r - D; q = q | (1 << i) } 38 i = i - 1 39 } 40 return q 41} 42 43// run the prebuilt gate-net for (N,D); returns quotient, writes remainder to r_out. 44func rt_run(g: *NxGsim, qnet: i64, rnet: i64, N: i64, D: i64, r_out: *i64) -> i64 { 45 g.vals[0] = N 46 g.vals[1] = D 47 if nx_gsim_run(g) != NX_GSIM_OK { r_out[0] = 0 - 1; return 0 - 1 } 48 r_out[0] = g.vals[rnet] 49 return g.vals[qnet] 50} 51 52func main() -> i64 { 53 let vals: *i64 = sys_mmap(8 * 4096) as *i64 54 let cells: *NxGsimCell = sys_mmap(48 * 4096) as *NxGsimCell 55 let g: *NxGsim = sys_mmap(64) as *NxGsim 56 g.vals = vals; g.n_nets = 2; g.cells = cells; g.n_cells = 0 57 58 let rob: *i64 = sys_mmap(8) as *i64; rob[0] = 0 59 let qnet: i64 = nx_recip_div24_synth(g, 0, 1, rob) 60 let rnet: i64 = rob[0] 61 let r_out: *i64 = sys_mmap(8) as *i64; r_out[0] = 0 62 63 var total: i64 = 0 64 var ok: i64 = 0 65 var q_chk: i64 = 0 66 var r_chk: i64 = 0 67 68 // dense: D in [1,256], N in [0,8191] 69 var D: i64 = 1 70 while D <= 256 { 71 var N: i64 = 0 72 while N <= 8191 { 73 let a: i64 = rt_run(g, qnet, rnet, N, D, r_out) 74 let ar: i64 = r_out[0] 75 let b: i64 = rt_restoring(N, D) 76 let c: i64 = N / D 77 let cr: i64 = N - (N / D) * D 78 total = total + 1 79 if a == b { if a == c { if ar == cr { ok = ok + 1 } } } 80 N = N + 1 81 } 82 D = D + 1 83 } 84 85 q_chk = rt_run(g, qnet, rnet, 12345, 7, r_out) 86 r_chk = r_out[0] 87 88 // random FULL 24-bit: N,D in [1, 2^24-1] -- exercises the wide-multiplier path 89 var seed: i64 = 2463534242 90 var nr: i64 = 0 91 while nr < 200000 { 92 seed = seed * RT_LCG_A + RT_LCG_C; var N: i64 = seed & RT_W24 93 seed = seed * RT_LCG_A + RT_LCG_C; var D: i64 = (seed & RT_W24) 94 if D == 0 { D = 1 } 95 let a: i64 = rt_run(g, qnet, rnet, N, D, r_out) 96 let ar: i64 = r_out[0] 97 let b: i64 = rt_restoring(N, D) 98 let c: i64 = N / D 99 let cr: i64 = N - (N / D) * D 100 total = total + 1 101 if a == b { if a == c { if ar == cr { ok = ok + 1 } } } 102 nr = nr + 1 103 } 104 105 // edges 106 let en: *i64 = sys_mmap(8 * 8) as *i64 107 let ed: *i64 = sys_mmap(8 * 8) as *i64 108 en[0]=16777215; ed[0]=1 109 en[1]=16777215; ed[1]=16777215 110 en[2]=16777215; ed[2]=8388608 111 en[3]=0; ed[3]=16777215 112 en[4]=1; ed[4]=1 113 en[5]=16777215; ed[5]=2 114 en[6]=12345; ed[6]=255 115 en[7]=16777215; ed[7]=257 116 var e: i64 = 0 117 while e < 8 { 118 let a: i64 = rt_run(g, qnet, rnet, en[e], ed[e], r_out) 119 let ar: i64 = r_out[0] 120 let b: i64 = rt_restoring(en[e], ed[e]) 121 let c: i64 = en[e] / ed[e] 122 let cr: i64 = en[e] - (en[e] / ed[e]) * ed[e] 123 total = total + 1 124 if a == b { if a == c { if ar == cr { ok = ok + 1 } } } 125 e = e + 1 126 } 127 128 _emit_num(ok); _emit_num(total); _emit_num(q_chk); _emit_num(r_chk); _nl() 129 if ok != total { sys_exit(1); return 1 } 130 if total != 2297160 { sys_exit(2); return 2 } 131 if q_chk != 1763 { sys_exit(3); return 3 } 132 if r_chk != 4 { sys_exit(4); return 4 } 133 sys_exit(0); return 0 134}