code wiki / _hdl_build / _f64_exp_gate_authored.nx
_f64_exp_gate_authored.nx source
↩ module page · 106 lines · 3413 B
1// _f64_exp_gate_authored.nx -- ME1 gate: nx_f64_exp vs mpmath-60dps oracle.
2//
3// 203 vectors (_f64_exp_kat_vectors.nx), expected = correctly-rounded f64 of
4// the 60-digit value. Pass = ULP distance <= 1 on every vector (exp is not
5// claimed correctly-rounded in v1; the bound is MEASURED and printed so the
6// grade is evidence, not optimism). exp results are nonnegative bit patterns,
7// so ULP distance = |got - exp| on raw i64 works directly (NaN handled apart).
8//
9// Markers:
10// EXPBAD i=<n> x=<hex> exp=<hex> got=<hex> ulp=<n>
11// EXP-ULP total=<n> exact=<n> ulp1=<n> worse=<n> max=<n>
12// EXP-GATE verdict=GREEN|RED
13
14import "nx_syscalls.nx"
15import "nx_f64.nx"
16import "nx_f64_div.nx"
17import "nx_f64_sqrt.nx"
18import "nx_f64_cvt.nx"
19import "nx_f64_exp.nx"
20import "_f64_exp_kat_vectors.nx"
21
22func f6e_puts(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 }
23
24func f6e_putn(v: i64) -> i64 {
25 let bb: *u8 = sys_mmap(28)
26 var m: i64 = v
27 if m < 0 { m = 0 - m; sys_write(1, "-" as *u8, 1) }
28 let t: *u8 = sys_mmap(28)
29 var k: i64 = 0
30 if m == 0 { t[0] = 48; k = 1 }
31 while m > 0 { t[k] = 48 + (m % 10); m = m / 10; k = k + 1 }
32 var i: i64 = 0
33 while i < k { bb[i] = t[k-1-i]; i = i + 1 }
34 sys_write(1, bb, k)
35 return 0
36}
37
38func f6e_puthex(v: i64) -> i64 {
39 let bb: *u8 = sys_mmap(20)
40 var i: i64 = 0
41 while i < 16 {
42 let nib: i64 = (v >> ((15 - i) * 4)) & 15
43 if nib < 10 { bb[i] = 48 + nib } else { bb[i] = 55 + nib }
44 i = i + 1
45 }
46 sys_write(1, bb, 16)
47 return 0
48}
49
50func main() -> i64 {
51 let av: *i64 = sys_mmap(8 * 256) as *i64
52 let ev: *i64 = sys_mmap(8 * 256) as *i64
53 let n: i64 = f64e_kat_fill_all(av, ev)
54
55 var exact: i64 = 0
56 var ulp1: i64 = 0
57 var worse: i64 = 0
58 var maxulp: i64 = 0
59 var i: i64 = 0
60 while i < n {
61 let x: i64 = av[i]
62 let want: i64 = ev[i]
63 let got: i64 = nx_f64_exp(x)
64 var ulp: i64 = 0
65 if got != want {
66 // NaN expectation: any-NaN-got counts as exact.
67 var settled: i64 = 0
68 if want == 0x7FF8000000000000 {
69 if nx_f64_is_nan(got) == 1 { settled = 1 }
70 }
71 if settled == 0 {
72 ulp = got - want
73 if ulp < 0 { ulp = 0 - ulp }
74 }
75 }
76 if ulp == 0 { exact = exact + 1 }
77 if ulp == 1 { ulp1 = ulp1 + 1 }
78 if ulp > 1 {
79 worse = worse + 1
80 if worse <= 40 {
81 f6e_puts("EXPBAD i=" as *u8); f6e_putn(i)
82 f6e_puts(" x=" as *u8); f6e_puthex(x)
83 f6e_puts(" exp=" as *u8); f6e_puthex(want)
84 f6e_puts(" got=" as *u8); f6e_puthex(nx_f64_exp(x))
85 f6e_puts(" ulp=" as *u8); f6e_putn(ulp)
86 f6e_puts("\n" as *u8)
87 }
88 }
89 if ulp > maxulp { maxulp = ulp }
90 i = i + 1
91 }
92
93 f6e_puts("EXP-ULP total=" as *u8); f6e_putn(n)
94 f6e_puts(" exact=" as *u8); f6e_putn(exact)
95 f6e_puts(" ulp1=" as *u8); f6e_putn(ulp1)
96 f6e_puts(" worse=" as *u8); f6e_putn(worse)
97 f6e_puts(" max=" as *u8); f6e_putn(maxulp)
98 f6e_puts("\n" as *u8)
99 if worse == 0 {
100 f6e_puts("EXP-GATE verdict=GREEN\n" as *u8)
101 return 0
102 }
103 f6e_puts("EXP-GATE verdict=RED\n" as *u8)
104 if worse > 100 { return 100 }
105 return worse
106}