code wiki / _hdl_build / nx_eng_diff_miscompile_test.nx

nx_eng_diff_miscompile_test.nx source

↩ module page · 67 lines · 3729 B

1// nx_eng_diff_miscompile_test.nx -- prove the ENGINEER's differential logic-miscompile 2// detector, and MONITOR the live compiler with it. 3// GATE (must hold): the detector mechanism is sound (agree on equal, diverge on unequal) 4// AND the trusted memory-staged reference equals the known answer. 5// MONITOR (reported): whether the HIGH-register-pressure form diverges -- the known-open 6// class the full-pipeline gate is blind to. A divergence here is the 7// canary firing, not a regression in this test. 8// main() is kept low-pressure (delegated compares, memory-backed verdicts) so the gate 9// itself is not a victim of the very bug it watches for. 10 11import "nx_eng_diff_miscompile.nx" 12 13func ed_puts(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 } 14func ed_num(v: i64) -> i64 { 15 let b: *u8 = sys_mmap(28); var m: i64 = v; if m < 0 { m = 0 - m } 16 let t: *u8 = sys_mmap(28); var k: i64 = 0 17 if m == 0 { t[0] = 48; k = 1 } 18 while m > 0 { t[k] = 48 + (m % 10); m = m / 10; k = k + 1 } 19 if v < 0 { ed_puts("-" as *u8) } 20 var i: i64 = 0; while i < k { b[i] = t[k - 1 - i]; i = i + 1 } 21 sys_write(1, b, k); return 0 22} 23func ed_eq(a: i64, b: i64) -> i64 { if a == b { return 1 } return 0 } 24// tally in a small dedicated frame: r is a fresh argument here, not a fat-main local held 25// across many calls -- so the gate that watches for the miscompile is not its victim. 26func tally3(r: *i64) -> i64 { 27 var ec: i64 = 0 28 var i: i64 = 0 29 while i < 3 { if r[i] != 1 { if ec == 0 { ec = i + 1 } } i = i + 1 } 30 return ec 31} 32 33func main() -> i64 { 34 ed_puts("=== ENGINEER differential logic-miscompile detector (the class the pipeline gate is blind to) ===\n" as *u8) 35 let out: *i64 = sys_mmap(8 * 8) as *i64 36 let r: *i64 = sys_mmap(8 * 8) as *i64 37 38 // 1. detector mechanism is sound 39 r[0] = ed_eq(eng_diff(5, 5), ED_AGREE) 40 r[1] = ed_eq(eng_diff(5, 6), ED_DIVERGE) 41 ed_puts(" detector : eng_diff(5,5)=AGREE? " as *u8); if r[0]==1 {ed_puts("yes" as *u8)} else {ed_puts("NO" as *u8)} 42 ed_puts(" eng_diff(5,6)=DIVERGE? " as *u8); if r[1]==1 {ed_puts("yes" as *u8)} else {ed_puts("NO" as *u8)}; ed_puts("\n" as *u8) 43 44 // 2. run the differential probe on the live compiler 45 let verdict: i64 = eng_detect_logic_miscompile(out) 46 r[2] = ed_eq(out[1], out[2]) // trusted memory-staged path must equal known 47 ed_puts(" probe : hp=" as *u8); ed_num(out[0]); ed_puts(" lp=" as *u8); ed_num(out[1]); ed_puts(" known=" as *u8); ed_num(out[2]); ed_puts("\n" as *u8) 48 49 // 3. MONITOR report on the high-pressure form 50 ed_puts(" MONITOR : " as *u8) 51 if ed_eq(out[0], out[2]) == 1 { 52 ed_puts("no divergence detected at this pressure (hp == known)\n" as *u8) 53 } else { 54 ed_puts("*** LOGIC MISCOMPILE DETECTED *** hp diverged from known -- register-pressure class, owed by the codegen arc\n" as *u8) 55 } 56 ed_puts(" differential verdict = " as *u8); if verdict==ED_AGREE {ed_puts("AGREE\n" as *u8)} else {ed_puts("DIVERGE\n" as *u8)} 57 58 ed_puts("----------------------------------------------------------------\n" as *u8) 59 ed_puts(" The Engineer can now SEE logic miscompiles, not just crashes/compile-fails.\n" as *u8) 60 61 // GATE: detector sound + trusted reference correct. (hp divergence is monitored, not gated.) 62 ed_puts(" gate sees : r[0]=" as *u8); ed_num(r[0]); ed_puts(" r[1]=" as *u8); ed_num(r[1]); ed_puts(" r[2]=" as *u8); ed_num(r[2]); ed_puts("\n" as *u8) 63 let ec: i64 = tally3(r) 64 ed_puts(" gate ec : " as *u8); ed_num(ec); ed_puts("\n" as *u8) 65 sys_exit(ec) 66 return ec 67}