nx_recip64_test.nx source

1// nx_recip64_test.nx -- proves the 64-bit Goldschmidt divider GATE-NETWORK 2// (nx_recip64_synth) emits what the bit-exact scalar computes: cross-checked vs 3// the proven unsigned oracle (nx_rv64im_udiv / urem), quotient AND remainder, 4// over dense-small + every power of two + random FULL 64-bit (incl. bit-63-set, 5// via xorshift) + the overflow edges. Known answer: "<ok> <total>" ok==total. 6 7import "nx_recip64.nx" 8import "rv64im_min_alu.nx" 9 10const R64T_HALF: i64 = 0 - 9223372036854775808 // 2^63 11 12func _emit_dec(v: i64) -> i64 { 13 let b: *u8 = sys_mmap(28); var n: i64 = v; if n < 0 { n = 0 - n } 14 let t: *u8 = sys_mmap(28); var k: i64 = 0 15 if n == 0 { t[0] = 48; k = 1 } 16 while n > 0 { t[k] = 48 + (n % 10); n = n / 10; k = k + 1 } 17 var i: i64 = 0; while i < k { b[i] = t[k - 1 - i]; i = i + 1 } 18 b[k] = 32; sys_write(1, b, k + 1); return 0 19} 20func _nl() -> i64 { let z: *u8 = sys_mmap(2); z[0] = 10; sys_write(1, z, 1); return 0 } 21 22func r64t_chk(g: *NxGsim, qnet: i64, rnet: i64, N: i64, D: i64) -> i64 { 23 g.vals[0] = N 24 g.vals[1] = D 25 if nx_gsim_run(g) != NX_GSIM_OK { return 0 } 26 let gq: i64 = g.vals[qnet] 27 let gr: i64 = g.vals[rnet] 28 if gq != nx_rv64im_udiv(N, D) { return 0 } 29 if gr != nx_rv64im_urem(N, D) { return 0 } 30 return 1 31} 32 33func main() -> i64 { 34 let vals: *i64 = sys_mmap(8 * 4096) as *i64 35 let cells: *NxGsimCell = sys_mmap(48 * 4096) as *NxGsimCell 36 let g: *NxGsim = sys_mmap(64) as *NxGsim 37 g.vals = vals; g.n_nets = 2; g.cells = cells; g.n_cells = 0 38 let rob: *i64 = sys_mmap(8) as *i64; rob[0] = 0 39 let qnet: i64 = nx_recip64_synth(g, 0, 1, rob) 40 let rnet: i64 = rob[0] 41 42 var total: i64 = 0 43 var ok: i64 = 0 44 45 // dense small: D in [1,32], N in [0,511] 46 var D: i64 = 1 47 while D <= 32 { 48 var N: i64 = 0 49 while N <= 511 { 50 total = total + 1; ok = ok + r64t_chk(g, qnet, rnet, N, D) 51 N = N + 1 52 } 53 D = D + 1 54 } 55 56 // every power of two divisor, assorted dividends 57 var kb: i64 = 0 58 while kb < 64 { 59 let pd: i64 = 1 << kb 60 let nv: *i64 = sys_mmap(8 * 5) as *i64 61 nv[0]=0; nv[1]=1; nv[2]=pd; nv[3]=0-1; nv[4]=(0-1)-pd 62 var j: i64 = 0 63 while j < 5 { total = total + 1; ok = ok + r64t_chk(g, qnet, rnet, nv[j], pd); j = j + 1 } 64 kb = kb + 1 65 } 66 67 // random FULL 64-bit 68 var seed: i64 = 88172645463325252 69 var nr: i64 = 0 70 while nr < 5000 { 71 seed = seed ^ (seed << 13); seed = seed ^ nx_rv64im_lshr(seed, 7); seed = seed ^ (seed << 17) 72 let N: i64 = seed 73 seed = seed ^ (seed << 13); seed = seed ^ nx_rv64im_lshr(seed, 7); seed = seed ^ (seed << 17) 74 var D: i64 = seed 75 if D == 0 { D = 1 } 76 total = total + 1; ok = ok + r64t_chk(g, qnet, rnet, N, D) 77 nr = nr + 1 78 } 79 80 // edges 81 let en: *i64 = sys_mmap(8 * 8) as *i64 82 let ed: *i64 = sys_mmap(8 * 8) as *i64 83 en[0]=0-1; ed[0]=1 84 en[1]=0-1; ed[1]=0-1 85 en[2]=0-1; ed[2]=2 86 en[3]=0-1; ed[3]=R64T_HALF 87 en[4]=R64T_HALF; ed[4]=3 88 en[5]=0-1; ed[5]=(0-1) 89 en[6]=12345678901234; ed[6]=99991 90 en[7]=0-1; ed[7]=R64T_HALF + 1 91 var e: i64 = 0 92 while e < 8 { total = total + 1; ok = ok + r64t_chk(g, qnet, rnet, en[e], ed[e]); e = e + 1 } 93 94 _emit_dec(ok); _emit_dec(total); _nl() 95 if ok != total { sys_exit(1); return 1 } 96 sys_exit(0); return 0 97}