nx_regalloc_absorb_governed_test.nx source

1// nx_regalloc_absorb_governed_test.nx -- the LOOP governs absorbing the allocator 2// into codegen. Absorption is the risky step (the prior g1 attempt miscompiled), so 3// it goes through the crew council (3->2->1) with the REAL gates as the Engineer's 4// evidence: 5// ENGINEER = the allocator is sound (ra_validate) AND execution-equivalent to the 6// reference (ri_interp_ref == ri_interp_alloc) AND fits (0 spills). 7// GENEALOGIST = novel (a new codegen path, not a duplicate). 8// WARDEN = additive-safe (a NEW path; the known-good compiler is untouched). 9// Only then does the Conductor ACT (absorb). A MISCOMPILING allocator (Engineer 10// evidence fails) must be DENIED/ESCALATED -- governance blocks the g1 regression. 11// 12// Known answer: proven allocator -> council ACT (absorb); miscompiling allocator -> 13// council NOT ACT (blocked). exit 0. 14 15import "nx_crew_council.nx" 16import "nx_regalloc_interp.nx" 17 18func ab_puts(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 } 19 20const AB_N: i64 = 11 21const AB_NREG: i64 = 8 22const AB_K: i64 = 6364136223846793005 23const AB_A: i64 = 1442695040888963407 24const AB_M: i64 = 65535 25const AB_KK: i64 = 1000000 26 27func ab_rng(s: i64) -> i64 { return s * 6364136223846793005 + 1442695040888963407 } 28 29// build the race-kernel IR into caller arrays; returns nothing meaningful. 30func ab_build_ir(op: *i64, u0: *i64, u1: *i64, imm: *i64) -> i64 { 31 op[0] = ROP_INPUT; u0[0] = 0 - 1; u1[0] = 0 - 1; imm[0] = 0 32 op[1] = ROP_INPUT; u0[1] = 0 - 1; u1[1] = 0 - 1; imm[1] = 1 33 op[2] = ROP_INPUT; u0[2] = 0 - 1; u1[2] = 0 - 1; imm[2] = 2 34 op[3] = ROP_MUL_IMM; u0[3] = 0; u1[3] = 0 - 1; imm[3] = AB_K 35 op[4] = ROP_ADD_IMM; u0[4] = 3; u1[4] = 0 - 1; imm[4] = AB_A 36 op[5] = ROP_SHR_IMM; u0[5] = 4; u1[5] = 0 - 1; imm[5] = 31 37 op[6] = ROP_XOR; u0[6] = 4; u1[6] = 5; imm[6] = 0 38 op[7] = ROP_AND_IMM; u0[7] = 6; u1[7] = 0 - 1; imm[7] = AB_M 39 op[8] = ROP_ADD; u0[8] = 1; u1[8] = 7; imm[8] = 0 40 op[9] = ROP_ADD_IMM; u0[9] = 2; u1[9] = 0 - 1; imm[9] = 1 41 op[10] = ROP_LT_IMM; u0[10] = 9; u1[10] = 0 - 1; imm[10] = AB_KK 42 return 0 43} 44 45// run the ENGINEER gates on a given allocation; returns 1 if it PROVES OUT (sound + 46// execution-equivalent over trials), else 0. 47func ab_engineer_ok(op: *i64, u0: *i64, u1: *i64, imm: *i64, last_use: *i64, alloc: *i64) -> i64 { 48 if ra_validate(AB_N, last_use, alloc, AB_NREG) != 0 { return 0 } // unsound 49 let inputs: *i64 = sys_mmap(8 * 4) 50 var s: i64 = 2654435761 51 var tr: i64 = 0 52 while tr < 64 { 53 s = ab_rng(s); inputs[0] = s 54 s = ab_rng(s); inputs[1] = s 55 s = ab_rng(s); inputs[2] = s 56 let rr: i64 = ri_interp_ref(AB_N, op, u0, u1, imm, inputs, 6, 8, 9) 57 let ra: i64 = ri_interp_alloc(AB_N, AB_NREG, op, u0, u1, imm, alloc, inputs, 6, 8, 9) 58 if rr != ra { return 0 } // miscompile 59 tr = tr + 1 60 } 61 return 1 62} 63 64func main() -> i64 { 65 ab_puts("=== GOVERNED ABSORPTION: the loop absorbs regalloc only if proven ===\n" as *u8) 66 67 let op: *i64 = sys_mmap(8 * AB_N) 68 let u0: *i64 = sys_mmap(8 * AB_N) 69 let u1: *i64 = sys_mmap(8 * AB_N) 70 let imm: *i64 = sys_mmap(8 * AB_N) 71 ab_build_ir(op, u0, u1, imm) 72 73 let last_use: *i64 = sys_mmap(8 * AB_N) 74 let alloc: *i64 = sys_mmap(8 * AB_N) 75 ra_compute_last_use(AB_N, u0, u1, last_use) 76 last_use[6] = AB_N; last_use[8] = AB_N; last_use[9] = AB_N 77 ra_linscan(AB_N, AB_NREG, last_use, alloc) 78 79 let a: *CrewAction = sys_mmap(64) as *CrewAction 80 let why: *i64 = sys_mmap(8) as *i64 81 82 // --- POSITIVE: the proven allocator goes to the council --- 83 let eng_ok: i64 = ab_engineer_ok(op, u0, u1, imm, last_use, alloc) 84 ab_puts(" engineer (sound + exec-equiv) : " as *u8) 85 if eng_ok == 1 { ab_puts("PROVES OUT\n" as *u8) } else { ab_puts("FAILED\n" as *u8) } 86 cc_set(a, "absorb linear-scan regalloc into codegen" as *u8, eng_ok, 1, 1, 1, 1) 87 let vd_ok: i64 = cc_council(a, why) 88 ab_puts(" council verdict (proven) : " as *u8); ab_puts(cc_verdict_name(vd_ok)); ab_puts("\n" as *u8) 89 90 // --- NEGATIVE: a MISCOMPILING allocator (g1-style) -- corrupt the alloc --- 91 let bad: *i64 = sys_mmap(8 * AB_N) 92 var c: i64 = 0 93 while c < AB_N { bad[c] = alloc[c]; c = c + 1 } 94 bad[1] = alloc[3] // alias overlapping vregs -> miscompile 95 let eng_bad: i64 = ab_engineer_ok(op, u0, u1, imm, last_use, bad) 96 ab_puts(" engineer (miscompiling alloc) : " as *u8) 97 if eng_bad == 1 { ab_puts("PROVES OUT\n" as *u8) } else { ab_puts("FAILED (caught)\n" as *u8) } 98 cc_set(a, "absorb a MISCOMPILING regalloc" as *u8, eng_bad, 1, 1, 1, 1) 99 let vd_bad: i64 = cc_council(a, why) 100 ab_puts(" council verdict (miscompile) : " as *u8); ab_puts(cc_verdict_name(vd_bad)); ab_puts("\n" as *u8) 101 102 ab_puts("----------------------------------------------------------------\n" as *u8) 103 ab_puts(" the loop ABSORBS the proven allocator and BLOCKS the miscompiling one\n" as *u8) 104 ab_puts(" -- regalloc enters codegen only under governance. No g1 can ship.\n" as *u8) 105 106 // GATE: proven -> ACT; miscompiling -> NOT act (governance blocks it). 107 if eng_ok != 1 { sys_exit(1); return 1 } 108 if vd_ok != CC_ACT { sys_exit(2); return 2 } 109 if eng_bad != 0 { sys_exit(3); return 3 } // the miscompile must be caught 110 if vd_bad == CC_ACT { sys_exit(4); return 4 } // and must NOT be absorbed 111 sys_exit(0) 112 return 0 113}