nx_dd_verify.nx source

1// nx_dd_verify.nx -- the DD-PRIMITIVE CONTRACT VERIFIER (ONE-STEP-TEN-SECOND tool for 2// the dd-composition bug class). The gamma dd probe hit a ~5e11-ulp STRUCTURAL bug 3// from using _sh_mul2/_sh_2sum/_sh_expdd without verifying their hi/lo output contract. 4// Instead of hand-debugging twice, this organ is the TEAM's one-command answer: it runs 5// each dd primitive on KNOWN double-double values, PRINTS the actual contract (which 6// slot is hi, which is lo, what 2^n means), and gates the round-trip. Run it before 7// ANY dd composition -> the contract is known, the class is retired. 8// KATs (error-free-transform identities, exact): 9// _sh_2sum(a,b) : out[0]=round(a+b), out[1]=exact error; out[0]+out[1]==a+b 10// _sh_mul2(a,b) : out[0]=round(a*b), out[1]=exact error; out[0]+out[1]==a*b 11// _sh_expdd(v) : exp(v)==(out[0]+out[1])*2^out[2] (the scale contract) 12// Durable: DDVERIFY rows (with the OBSERVED slots) + DDGATE -> knowledge/status/ 13// dd_verify.log. Exit 0 = all contracts hold. license_tier: ORIGINAL 14import "nx_syscalls.nx" 15import "nx_f64.nx" 16import "nx_f64_cvt.nx" 17import "_pe_f64sinhcosh.nx" 18func dv_p(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 } 19func dv_f(fd: i64, s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(fd,s,n); return 0 } 20func dv_hx(fd: i64, v: i64) -> i64 { 21 let d: *u8 = "0123456789abcdef" as *u8 22 let b: *u8 = sys_mmap(20) 23 b[0] = 48 as u8; b[1] = 120 as u8 24 var i: i64 = 0 25 while i < 16 { b[2+i] = d[(v >> ((15 - i) * 4)) & 15]; i = i + 1 } 26 sys_write(fd, b, 18) 27 return 0 28} 29// |a-b| in ulp (both finite same-sign-ish); for tiny-diff exactness checks 30func dv_ulp(a: i64, b: i64) -> i64 { if a >= b { return a - b } return b - a } 31func dv_chk(lfd: i64, label: *u8, ok: i64, bad: *i64) -> i64 { 32 dv_p("DDV-" as *u8); dv_p(label) 33 dv_f(lfd, "DDVERIFY check=" as *u8); dv_f(lfd, label) 34 if ok == 1 { dv_p(" ok\n" as *u8); dv_f(lfd, " verdict=HOLDS\n" as *u8) } else { dv_p(" BAD\n" as *u8); dv_f(lfd, " verdict=VIOLATED\n" as *u8); bad[0] = bad[0] + 1 } 35 return 0 36} 37func main() -> i64 { 38 dv_p("=== DD-VERIFY: the dd-primitive contract, shown + gated (ten-second class tool) ===\n" as *u8) 39 let lfd: i64 = sys_openat_append("knowledge/status/dd_verify.log" as *u8, 0x1a4) 40 if lfd < 0 { dv_p(" dd_verify log open failed\n" as *u8); sys_exit(1); return 1 } 41 let bad: *i64 = sys_mmap(16) as *i64 42 bad[0] = 0 43 let o: *i64 = sys_mmap(32) as *i64 44 // --- _sh_2sum(1.0, 2^-60): hi must be 1.0, lo must be 2^-60 (the EFT contract) --- 45 let one: i64 = 0x3FF0000000000000 46 let tiny: i64 = 0x3C30000000000000 // 2^-60 47 _sh_2sum(one, tiny, o) 48 dv_f(lfd, "DDVERIFY 2sum slot0=" as *u8); dv_hx(lfd, o[0]); dv_f(lfd, " slot1=" as *u8); dv_hx(lfd, o[1]); dv_f(lfd, "\n" as *u8) 49 dv_chk(lfd, "2sum-hi-is-slot0" as *u8, o[0] == one, bad) 50 dv_chk(lfd, "2sum-lo-is-slot1" as *u8, o[1] == tiny, bad) 51 // --- _sh_mul2((1+2^-30),(1+2^-30)): a*b = 1 + 2^-29 + 2^-60; hi=1+2^-29, lo~2^-60 --- 52 let a: i64 = nx_f64_add(one, 0x3E10000000000000) // 1 + 2^-30 53 _sh_mul2(a, a, o) 54 let expect_hi: i64 = nx_f64_add(one, 0x3E20000000000000) // 1 + 2^-29 55 dv_f(lfd, "DDVERIFY mul2 slot0=" as *u8); dv_hx(lfd, o[0]); dv_f(lfd, " slot1=" as *u8); dv_hx(lfd, o[1]); dv_f(lfd, "\n" as *u8) 56 dv_chk(lfd, "mul2-hi-is-slot0" as *u8, dv_ulp(o[0], expect_hi) <= 1, bad) 57 // lo must be small + positive-ish (the residual ~2^-60), NOT zero, NOT huge 58 var lo_ok: i64 = 0 59 let alo: i64 = o[1] & 0x7FFFFFFFFFFFFFFF 60 if alo != 0 { if alo < 0x3D00000000000000 { lo_ok = 1 } } // |lo| < 2^-47 61 dv_chk(lfd, "mul2-lo-is-small-residual" as *u8, lo_ok, bad) 62 // round-trip: hi+lo == a*a to f64 (exact reconstruction) 63 let recon: i64 = nx_f64_add(o[0], o[1]) 64 dv_chk(lfd, "mul2-roundtrip" as *u8, recon == nx_f64_mul(a, a), bad) 65 // --- _sh_expdd(0): exp(0)=1 -> (slot0+slot1)*2^slot2 == 1.0 --- 66 _sh_expdd(0, o) 67 let mant0: i64 = nx_f64_add(o[0], o[1]) 68 dv_f(lfd, "DDVERIFY expdd(0) slot0=" as *u8); dv_hx(lfd, o[0]); dv_f(lfd, " slot1=" as *u8); dv_hx(lfd, o[1]); dv_f(lfd, " slot2(n)=" as *u8) 69 let nb: *u8 = sys_mmap(8); var nn: i64 = o[2]; if nn < 0 { dv_f(lfd, "-" as *u8); nn = 0-nn }; nb[0] = (48 + (nn%10)) as u8; sys_write(lfd, nb, 1); dv_f(lfd, "\n" as *u8) 70 // reconstruct exp(0) = mant * 2^n via scale; must equal 1.0 71 let e0: i64 = _sh_scale(mant0, o[2]) 72 dv_chk(lfd, "expdd0-reconstructs-1.0" as *u8, dv_ulp(e0, one) <= 2, bad) 73 dv_f(lfd, "DDGATE checks=" as *u8) 74 let nb2: *u8 = sys_mmap(8); nb2[0] = (48 + (6 - bad[0])) as u8; sys_write(lfd, nb2, 1) 75 dv_f(lfd, "/6 verdict=" as *u8) 76 if bad[0] == 0 { dv_f(lfd, "GREEN\n" as *u8) } else { dv_f(lfd, "RED\n" as *u8) } 77 sys_close(lfd) 78 dv_p(" contract printed to knowledge/status/dd_verify.log (run before composing dd)\n" as *u8) 79 if bad[0] == 0 { dv_p(" DD-VERIFY: GREEN (contracts hold -- dd composition is safe)\n" as *u8); sys_exit(0); return 0 } 80 dv_p(" DD-VERIFY: RED (a contract differs from assumption -- THAT is your dd bug, named)\n" as *u8) 81 sys_exit(1) 82 return 1 83}