code wiki / _hdl_build / _bf_pow_gate_authored.nx

_bf_pow_gate_authored.nx source

↩ module page · 156 lines · 7523 B

1// _bf_pow_gate_authored.nx -- self-anchor gate for the SOVEREIGN bigfloat pow 2// oracle (nx_bigfloat120_pow). No external oracle: 3// 1. CORRECTLY-ROUNDED EQUALITIES vs three BLESSED f64 organs at 200 banded 4// random points: pow(x,2) == fl(x*x) (nx_f64_mul), pow(x,-1) == fl(1/x) 5// (nx_f64_div), pow(x,1/2) == sqrt(x) (nx_f64_sqrt), pow(x,1) == x. 6// Both sides round the same true value -> raws must be IDENTICAL. 7// 2. EXACT POWER LADDER: pow(2,n) across the whole format incl. the subnormal 8// floor (n=-1074), the round-to-even-zero tie (n=-1075) and the overflow 9// ceiling (n=1024); mirrored via pow(1/2,-n). 10// 3. The IEEE-754/C99 special matrix + odd-integer sign rule. 11// Markers: BFPOW-EQ / BFPOW-LADDER / BFPOW-SPEC / BFPOW-GATE verdict= 12 13import "nx_syscalls.nx" 14import "nx_f64.nx" 15import "nx_f64_div.nx" 16import "nx_f64_sqrt.nx" 17import "nx_f64_cvt.nx" 18import "nx_bigfloat120.nx" 19import "nx_bigfloat120_div.nx" 20import "nx_bigfloat120_exp.nx" 21import "nx_bigfloat120_ln.nx" 22import "nx_bigfloat120_pow.nx" 23 24func bpg_puts(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 } 25func bpg_putn(v: i64) -> i64 { let bb: *u8 = sys_mmap(28); var m: i64 = v; if m < 0 { m = 0 - m; sys_write(1, "-" as *u8, 1) }; let t: *u8 = sys_mmap(28); var k: i64 = 0; if m == 0 { t[0] = 48; k = 1 }; while m > 0 { t[k] = 48 + (m % 10); m = m / 10; k = k + 1 }; var i: i64 = 0; while i < k { bb[i] = t[k-1-i]; i = i + 1 }; sys_write(1, bb, k); return 0 } 26func bpg_puthex(v: i64) -> i64 { let bb: *u8 = sys_mmap(20); var i: i64 = 0; while i < 16 { let nib: i64 = (v >> ((15 - i) * 4)) & 15; if nib < 10 { bb[i] = 48 + nib } else { bb[i] = 55 + nib } i = i + 1 } sys_write(1, bb, 16); return 0 } 27 28func bpg_rng(state: *i64) -> i64 { 29 var s: i64 = state[0] 30 s = s ^ ((s >> 12) & 0x000FFFFFFFFFFFFF) 31 s = s ^ (s << 25) 32 s = s ^ ((s >> 27) & 0x0000001FFFFFFFFF) 33 state[0] = s 34 return s * 2685821657736338717 35} 36 37func bpg_pow2_expect(n: i64) -> i64 { 38 if n >= 1024 { return 0x7FF0000000000000 } 39 if n >= 0 - 1022 { return (n + 1023) << 52 } 40 if n >= 0 - 1074 { return 1 << (n + 1074) } 41 return 0 42} 43 44func main() -> i64 { 45 var bad: i64 = 0 46 let one_raw: i64 = 0x3FF0000000000000 47 let two_raw: i64 = 0x4000000000000000 48 let half_raw: i64 = 0x3FE0000000000000 49 let mone_raw: i64 = 0xBFF0000000000000 50 51 // ---- 1. correctly-rounded equalities vs blessed organs ---- 52 let st: *i64 = sys_mmap(16) as *i64 53 st[0] = 14142135623730950488 54 var eqbad: i64 = 0 55 var j: i64 = 0 56 while j < 200 { 57 var raw: i64 = bpg_rng(st) 58 var efr: i64 = 0 59 let band: i64 = raw & 3 60 if band == 0 { efr = 1021 + (raw & 7) } // near 1 61 if band == 1 { efr = 1000 + (raw & 63) } // mid-low 62 if band == 2 { efr = 1023 + (raw & 63) } // mid-high 63 if band == 3 { efr = 2 + (raw & 1023) } // deep range incl. tiny 64 if efr > 2040 { efr = 2040 } 65 raw = (efr << 52) | (bpg_rng(st) & 0x000FFFFFFFFFFFFF) 66 var ebad: i64 = 0 67 if bf_pow_f64(raw, one_raw) != raw { ebad = ebad + 1 } 68 if bf_pow_f64(raw, two_raw) != nx_f64_mul(raw, raw) { ebad = ebad + 1 } 69 if bf_pow_f64(raw, mone_raw) != nx_f64_div(one_raw, raw) { ebad = ebad + 1 } 70 if bf_pow_f64(raw, half_raw) != nx_f64_sqrt(raw) { ebad = ebad + 1 } 71 // pow(x, 1) with the sign restored (odd integer rule) 72 if bf_pow_f64(raw | (1 << 63), one_raw) != (raw | (1 << 63)) { ebad = ebad + 1 } 73 if ebad > 0 { 74 eqbad = eqbad + 1 75 if eqbad <= 10 { 76 bpg_puts("BFPOW-EQBAD x=" as *u8); bpg_puthex(raw) 77 bpg_puts(" fails=" as *u8); bpg_putn(ebad); bpg_puts("\n" as *u8) 78 } 79 } 80 j = j + 1 81 } 82 bpg_puts("BFPOW-EQ total=200 bad=" as *u8); bpg_putn(eqbad) 83 bpg_puts(" anchors=mul,div,sqrt,identity\n" as *u8) 84 bad = bad + eqbad 85 86 // ---- 2. exact power-of-two ladder ---- 87 let ns: *i64 = sys_mmap(8 * 16) as *i64 88 ns[0] = 0 - 1075; ns[1] = 0 - 1074; ns[2] = 0 - 1060; ns[3] = 0 - 1023 89 ns[4] = 0 - 1022; ns[5] = 0 - 53; ns[6] = 0 - 1; ns[7] = 1 90 ns[8] = 52; ns[9] = 1000; ns[10] = 1023; ns[11] = 1024 91 var lbad: i64 = 0 92 var i: i64 = 0 93 while i < 12 { 94 let n: i64 = ns[i] 95 let yraw: i64 = nx_i64_to_f64(n) 96 let want: i64 = bpg_pow2_expect(n) 97 if bf_pow_f64(two_raw, yraw) != want { 98 lbad = lbad + 1 99 bpg_puts("BFPOW-LBAD 2^n n=" as *u8); bpg_putn(n); bpg_puts("\n" as *u8) 100 } 101 let ymraw: i64 = nx_i64_to_f64(0 - n) 102 if bf_pow_f64(half_raw, ymraw) != want { 103 lbad = lbad + 1 104 bpg_puts("BFPOW-LBAD half^-n n=" as *u8); bpg_putn(n); bpg_puts("\n" as *u8) 105 } 106 i = i + 1 107 } 108 bpg_puts("BFPOW-LADDER rungs=24 bad=" as *u8); bpg_putn(lbad); bpg_puts("\n" as *u8) 109 bad = bad + lbad 110 111 // ---- 3. IEEE special matrix + odd-integer sign rule ---- 112 var sbad: i64 = 0 113 let nanr: i64 = 0x7FF8000000000000 114 let pinf: i64 = 0x7FF0000000000000 115 let ninf: i64 = 0xFFF0000000000000 116 let nzero: i64 = 1 << 63 117 let three: i64 = 0x4008000000000000 118 let mthree: i64 = 0xC008000000000000 119 let four: i64 = 0x4010000000000000 120 if bf_pow_f64(nanr, 0) != one_raw { sbad = sbad + 1 } // pow(NaN, 0) = 1 121 if bf_pow_f64(one_raw, nanr) != one_raw { sbad = sbad + 1 } // pow(1, NaN) = 1 122 if bf_pow_f64(nanr, one_raw) != nanr { sbad = sbad + 1 } 123 if bf_pow_f64(two_raw, nanr) != nanr { sbad = sbad + 1 } 124 if bf_pow_f64(mone_raw, pinf) != one_raw { sbad = sbad + 1 } // pow(-1, inf) = 1 125 if bf_pow_f64(mone_raw, ninf) != one_raw { sbad = sbad + 1 } 126 if bf_pow_f64(two_raw, pinf) != pinf { sbad = sbad + 1 } 127 if bf_pow_f64(two_raw, ninf) != 0 { sbad = sbad + 1 } 128 if bf_pow_f64(half_raw, pinf) != 0 { sbad = sbad + 1 } 129 if bf_pow_f64(half_raw, ninf) != pinf { sbad = sbad + 1 } 130 if bf_pow_f64(pinf, three) != pinf { sbad = sbad + 1 } 131 if bf_pow_f64(pinf, mthree) != 0 { sbad = sbad + 1 } 132 if bf_pow_f64(ninf, three) != ninf { sbad = sbad + 1 } // odd int keeps sign 133 if bf_pow_f64(ninf, four) != pinf { sbad = sbad + 1 } 134 if bf_pow_f64(ninf, mthree) != nzero { sbad = sbad + 1 } 135 if bf_pow_f64(0, three) != 0 { sbad = sbad + 1 } 136 if bf_pow_f64(nzero, three) != nzero { sbad = sbad + 1 } 137 if bf_pow_f64(nzero, four) != 0 { sbad = sbad + 1 } 138 if bf_pow_f64(nzero, mthree) != ninf { sbad = sbad + 1 } 139 if bf_pow_f64(0, mthree) != pinf { sbad = sbad + 1 } 140 if bf_pow_f64(0xC000000000000000, three) != 0xC020000000000000 { sbad = sbad + 1 } // (-2)^3 = -8 141 if bf_pow_f64(0xC000000000000000, two_raw) != four { sbad = sbad + 1 } // (-2)^2 = 4 142 if bf_pow_f64(0xC000000000000000, half_raw) != nanr { sbad = sbad + 1 } // neg^non-int 143 if bf_pow_f64(mone_raw, three) != mone_raw { sbad = sbad + 1 } // (-1)^3 = -1 144 if bf_pow_f64(mone_raw, four) != one_raw { sbad = sbad + 1 } // (-1)^4 = 1 145 if bf_pow_f64(four, half_raw) != two_raw { sbad = sbad + 1 } // 4^0.5 = 2 146 bpg_puts("BFPOW-SPEC asserts=26 bad=" as *u8); bpg_putn(sbad); bpg_puts("\n" as *u8) 147 bad = bad + sbad 148 149 if bad == 0 { 150 bpg_puts("BFPOW-GATE verdict=GREEN\n" as *u8) 151 return 0 152 } 153 bpg_puts("BFPOW-GATE verdict=RED\n" as *u8) 154 if bad > 100 { bad = 100 } 155 return bad 156}