code wiki / _hdl_build / nx_mathspec_erfc.nx
`nx_mathspec_erfc.nx` source

1// nx_mathspec_erfc.nx -- SOVEREIGN SPEC EMITTER for the ERFC kernel (DLMF ch7 rung 2,
2// ME2-ERF-002, the Laplace-CF range 1.75..6 that erf-Taylor cannot reach).  The erfc CF
3// kernel is control-flow (the backward recurrence), so its spec is just the scale/CF
4// constants -- every one DERIVED from the 120-bit bigfloat, no python, no minimax:
5//   1/sqrt(pi) = (2/sqrt(pi))/2 where 2/sqrt(pi) is bf_pi + Newton sqrt + bf_div (the
6//   SAME derivation the erf spec rail-proved bit-exact), halved by an exact exponent
7//   decrement.  0.5 and 1.0 are the exact CF coefficients (structural, exact f64).
8// REFUSAL RAIL (refuse > fabricate): derived 1/sqrt(pi) bits MUST equal the known-good
9//   libm constant 0x3FE20DD750429B6D, else exit 2 no emit (derive sovereignly, verify
10//   vs the world).
11// Layout: c[0]=inv_sqrt_pi  c[1]=half(0.5)  c[2]=one(1.0)
12// Emits runtime/_hdl_build/_pm_erfc_spec.nx :: pm_erfc_spec_fill(c)->3
13// license_tier: ORIGINAL
14import "nx_syscalls.nx"
15import "nx_pattern_emit.nx"
16import "nx_bigfloat120.nx"
17import "nx_bigfloat120_div.nx"
18import "nx_bigfloat120_trig.nx"
19
20func msc_wlit(fd: i64, v: i64) -> i64 {
21    if v < 0 { pe_w(fd, "0 - " as *u8); pe_wn(fd, 0 - v); return 0 }
22    pe_wn(fd, v)
23    return 0
24}
25
26func msc_row(fd: i64, idx: i64, v: i64) -> i64 {
27    pe_w(fd, "    c[" as *u8); pe_wn(fd, idx); pe_w(fd, "] = " as *u8)
28    msc_wlit(fd, v)
29    pe_w(fd, "\n" as *u8)
30    return 0
31}
32
33// Newton sqrt (8 iterations from an f64 seed) -- the erf/gamma rail algorithm.
34func msc_sqrt(out: *i64, a: *i64, seed_raw: i64) -> i64 {
35    let s: *i64 = bf_new()
36    bf_set_f64(s, seed_raw)
37    let q: *i64 = bf_new()
38    let sum: *i64 = bf_new()
39    var i: i64 = 0
40    while i < 8 {
41        bf_div(q, a, s)
42        bf_add(sum, s, q)
43        bf_div_small(s, sum, 2)
44        i = i + 1
45    }
46    bf_copy(out, s)
47    return 0
48}
49
50func main() -> i64 {
51    // derive 2/sqrt(pi) (erf-proven), then 1/sqrt(pi) = that / 2 (exact exponent shift)
52    let pi: *i64 = bf_new()
53    bf_pi(pi)
54    let spi: *i64 = bf_new()
55    msc_sqrt(spi, pi, 0x3FFC5BF891B4EF6A)
56    let two: *i64 = bf_new()
57    bf_set_int(two, 2)
58    let tosp: *i64 = bf_new()
59    bf_div(tosp, two, spi)                 // 2/sqrt(pi)
60    let invspi: *i64 = bf_new()
61    bf_copy(invspi, tosp)
62    if bf_is_zero(invspi) == 0 { invspi[0] = invspi[0] - 1 }   // / 2  -> 1/sqrt(pi)
63    let bits: i64 = bf_to_f64(invspi, 0, 0)
64    // RAIL: derived bits == known-good 1/sqrt(pi)
65    if bits != 0x3FE20DD750429B6D {
66        pe_w(1, "REFUSED: derived 1/sqrt(pi) bits differ from known-good 0x3FE20DD750429B6D\n" as *u8)
67        sys_exit(2)
68        return 2
69    }
70    let fd: i64 = sys_openat_wr("runtime/_hdl_build/_pm_erfc_spec.nx" as *u8, 0x1a4)
71    if fd < 0 { sys_exit(2); return 2 }
72    pe_w(fd, "// _pm_erfc_spec.nx -- GENERATED by nx_mathspec_erfc (SOVEREIGN bigfloat:\n" as *u8)
73    pe_w(fd, "// 2/sqrt(pi) erf-derivation halved; rail held vs known-good). DO NOT HAND-EDIT.\n" as *u8)
74    pe_w(fd, "import \"nx_syscalls.nx\"\n\nfunc pm_erfc_spec_fill(c: *i64) -> i64 {\n" as *u8)
75    msc_row(fd, 0, bits)                      // 1/sqrt(pi)
76    msc_row(fd, 1, 0x3FE0000000000000)        // 0.5
77    msc_row(fd, 2, 0x3FF0000000000000)        // 1.0
78    pe_w(fd, "    return 3\n}\n" as *u8)
79    sys_close(fd)
80    pe_w(1, "SPEC EMITTED: _pm_erfc_spec.nx (3 consts; rail held: sovereign 1/sqrt(pi) == known-good)\n" as *u8)
81    sys_exit(0)
82    return 0
83}
nx_mathspec_erfc.nx source

`nx_mathspec_erfc.nx` source
