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}