nx_eng_diff_miscompile.nx source

1// nx_eng_diff_miscompile.nx -- the ENGINEER's DIFFERENTIAL miscompile detector. The 2// full-pipeline gate (nx_engineer_gate_runner) catches crashes and compile-fails; it is 3// BLIND to a LOGIC miscompile -- a wrong result from correct-looking code. The known-good 4// compiler does exactly this under register pressure (a value held live across many calls 5// is not spilled, so a later comparison reads garbage and flips -- see 6// project-knowngood-compiler-regpressure-miscompile-2026-06-03). 7// 8// This detects that class by DIFFERENTIAL execution: compute the SAME logical value two 9// structurally different ways and flag any divergence -- 10// ed_hp HIGH register pressure: the value is held live across many ed_noise() calls, 11// then tested (the exact shape that miscompiled rc_bad / v1). 12// ed_lp LOW pressure: the value is staged in MEMORY and reloaded for the test. 13// Both must equal the compile-time-known answer (K = -3 -> "is K<0?" -> 1). If ed_hp 14// disagrees with ed_lp or with the known answer, a logic miscompile is present. 15// RACI: detection only -- the Engineer reports; it does not fix or admit. license_tier: ORIGINAL 16 17import "nx_syscalls.nx" 18const ED_MAGIC_999999: i64 = 999999 19 20const ED_AGREE: i64 = 0 21const ED_DIVERGE: i64 = 1 22 23// the detector mechanism: do two results agree? (proven sound independently in the test) 24func eng_diff(a: i64, b: i64) -> i64 { if a == b { return ED_AGREE } return ED_DIVERGE } 25 26// HEAVY register-clobbering callee, modelled on the real reproductions (the dd/cond test 27// mains held values across eng_compile/doc_*/cc_* calls that each make syscalls + use many 28// regs). A leaf loop does NOT pressure the caller enough; a syscall-making callee does. 29func ed_heavy(x: i64) -> i64 { 30 let p: *i64 = sys_mmap(64) as *i64 31 p[0] = x; p[1] = x + 1; p[2] = x + 2; p[3] = x + 3 32 var s: i64 = 0 33 var i: i64 = 0 34 while i < 4 { s = s + p[i]; i = i + 1 } 35 return s 36} 37 38// HIGH-pressure form, shaped like the ACTUAL bug: EIGHT sentinels that must stay negative 39// are held live across eight heavy (syscall-making) calls whose results are also held and 40// summed. Then all eight sentinels are tested. Known answer: 8 (all eight are < 0). 41func ed_hp() -> i64 { 42 let v0: i64 = 0 - 1 43 let v1: i64 = 0 - 2 44 let v2: i64 = 0 - 3 45 let v3: i64 = 0 - 4 46 let v4: i64 = 0 - 5 47 let v5: i64 = 0 - 6 48 let v6: i64 = 0 - 7 49 let v7: i64 = 0 - 8 50 let r0: i64 = ed_heavy(10) 51 let r1: i64 = ed_heavy(20) 52 let r2: i64 = ed_heavy(30) 53 let r3: i64 = ed_heavy(40) 54 let r4: i64 = ed_heavy(50) 55 let r5: i64 = ed_heavy(60) 56 let r6: i64 = ed_heavy(70) 57 let r7: i64 = ed_heavy(80) 58 let sink: i64 = r0 + r1 + r2 + r3 + r4 + r5 + r6 + r7 59 if sink == ED_MAGIC_999999 { return sink } // never true -- keeps all results live 60 var cnt: i64 = 0 61 if v0 < 0 { cnt = cnt + 1 } 62 if v1 < 0 { cnt = cnt + 1 } 63 if v2 < 0 { cnt = cnt + 1 } 64 if v3 < 0 { cnt = cnt + 1 } 65 if v4 < 0 { cnt = cnt + 1 } 66 if v5 < 0 { cnt = cnt + 1 } 67 if v6 < 0 { cnt = cnt + 1 } 68 if v7 < 0 { cnt = cnt + 1 } 69 return cnt 70} 71 72// LOW-pressure twin: identical logic, but the eight sentinels are staged in MEMORY and 73// reloaded for the tests, so they cannot be clobbered in registers across the calls. 74func ed_lp() -> i64 { 75 let s: *i64 = sys_mmap(64) as *i64 76 s[0] = 0 - 1; s[1] = 0 - 2; s[2] = 0 - 3; s[3] = 0 - 4 77 s[4] = 0 - 5; s[5] = 0 - 6; s[6] = 0 - 7; s[7] = 0 - 8 78 let r0: i64 = ed_heavy(10) 79 let r1: i64 = ed_heavy(20) 80 let r2: i64 = ed_heavy(30) 81 let r3: i64 = ed_heavy(40) 82 let r4: i64 = ed_heavy(50) 83 let r5: i64 = ed_heavy(60) 84 let r6: i64 = ed_heavy(70) 85 let r7: i64 = ed_heavy(80) 86 let sink: i64 = r0 + r1 + r2 + r3 + r4 + r5 + r6 + r7 87 if sink == ED_MAGIC_999999 { return sink } 88 var cnt: i64 = 0 89 var i: i64 = 0 90 while i < 8 { if s[i] < 0 { cnt = cnt + 1 } i = i + 1 } 91 return cnt 92} 93 94// the Engineer's verdict: 0 (ED_AGREE) if hp, lp and the known answer all agree; 95// ED_DIVERGE if a logic miscompile is present. out[0]=hp out[1]=lp out[2]=known. 96func eng_detect_logic_miscompile(out: *i64) -> i64 { 97 let known: i64 = 8 98 out[0] = ed_hp() 99 out[1] = ed_lp() 100 out[2] = known 101 if eng_diff(out[1], known) == ED_DIVERGE { return ED_DIVERGE } // trusted path wrong = worse 102 if eng_diff(out[0], known) == ED_DIVERGE { return ED_DIVERGE } // hp diverged = the class 103 return ED_AGREE 104}