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}