nx_superopt_governed_test.nx source

1// nx_superopt_governed_test.nx -- a SECOND GENERATOR in the governed cycle: the 2// superoptimizer. Unlike the rewrite-rule author, this generator SEARCHES (e-graph 3// saturation) for a strictly-cheaper EQUIVALENT program and the loop governs the 4// result -- so the loop now authors OPTIMIZATIONS, not just identities. 5// 6// GENERATOR build seed (mul x 8), saturate, emit the cost-minimal DAG (shl x 3) 7// VERIFIER the emitted candidate must EVALUATE equal to the seed over a battery 8// (nx_superopt_eval_emit) -- proven equivalent, not assumed 9// COUNCIL verifies = equivalent ; worth = strictly cheaper (cost decreased) ; 10// 3->2->1 -> ABSORB the optimization, else escalate 11// NEG-CTRL a WRONG candidate (shl x 2 = x*4 != x*8) is NOT equivalent -> refused 12// 13// Known answer: the real optimization is ABSORBED, the negative control REFUSED; 14// exit 0 iff governed correctly. 15 16import "nx_superopt.nx" // GENERATOR: e-graph search + nx_superopt_eval_emit 17import "nx_crew_council.nx" // GOVERNANCE 18 19const SOG_W: i64 = 16 20 21// VERIFY: does the emitted candidate DAG evaluate == seed (x*8) over a battery? 22func sog_equiv(cand_out: *NxEmitNode, cand_n: i64, cand_root: i64) -> i64 { 23 let env: *i64 = sys_mmap(8 * 8) as *i64 24 let val: *i64 = sys_mmap(64 * 8) as *i64 25 var x: i64 = 0 - 128 26 while x <= 128 { 27 env[0] = x 28 let got: i64 = nx_superopt_eval_emit(cand_out, cand_n, cand_root, env, val) 29 if got != (x * 8) { return 0 } 30 x = x + 1 31 } 32 return 1 33} 34 35func main() -> i64 { 36 cc_puts("================================================================\n" as *u8) 37 cc_puts(" SUPEROPT, GOVERNED -- a 2nd generator: the loop SEARCHES for a\n" as *u8) 38 cc_puts(" cheaper equivalent program, then the crew governs the result\n" as *u8) 39 cc_puts("================================================================\n" as *u8) 40 41 // ===== GENERATOR: e-graph search (mul x 8) -> (shl x 3) ===== 42 let nodes: *NxENode = sys_mmap(256 * 128) as *NxENode 43 let classes: *NxEClass = sys_mmap(256 * 64) as *NxEClass 44 let g: *NxEGraph = sys_mmap(256) as *NxEGraph 45 if nx_eqsat_init(g, nodes, 256, classes, 256) != NX_EQSAT_OK { sys_exit(10); return 10 } 46 let x: i64 = nx_eqsat_add_var(g, 0) 47 let eight: i64 = nx_eqsat_add_const(g, 8) 48 let seed_cls: i64 = nx_eqsat_add_binary(g, NX_EQ_OP_MUL, x, eight) 49 let seed_cost: i64 = nx_eqsat_class_cost(g, seed_cls) 50 nx_eqsat_saturate(g, 16) 51 if nx_eqsat_recompute_best(g) != NX_EQSAT_OK { sys_exit(11); return 11 } 52 let cand_cost: i64 = nx_eqsat_best_cost(g, seed_cls) 53 let cand_out: *NxEmitNode = sys_mmap(64 * 40) as *NxEmitNode 54 let cnt: *i64 = sys_mmap(8) as *i64 55 cnt[0] = 0 56 let cand_root: i64 = nx_eqsat_emit(g, seed_cls, cand_out, 64, cnt) 57 if cand_root < 0 { sys_exit(12); return 12 } 58 let cand_count: i64 = cnt[0] 59 60 // ===== VERIFY: equivalent? + cheaper? ===== 61 let equiv: i64 = sog_equiv(cand_out, cand_count, cand_root) 62 var cheaper: i64 = 0 63 if cand_cost < seed_cost { cheaper = 1 } 64 cc_puts(" GENERATOR: (mul x 8) -> emitted candidate (cost " as *u8) 65 let sc: *u8 = sys_mmap(2); sc[0] = 48 + seed_cost; sys_write(1, sc, 1) 66 cc_puts(" -> " as *u8); let cc2: *u8 = sys_mmap(2); cc2[0] = 48 + cand_cost; sys_write(1, cc2, 1) 67 cc_puts(")\n VERIFY: equivalent over battery=" as *u8) 68 if equiv == 1 { cc_puts("Y" as *u8) } else { cc_puts("N" as *u8) } 69 cc_puts(" cheaper=" as *u8); if cheaper == 1 { cc_puts("Y" as *u8) } else { cc_puts("N" as *u8) } 70 cc_puts("\n" as *u8) 71 72 let a: *CrewAction = sys_mmap(64) as *CrewAction 73 let why: *i64 = sys_mmap(8) as *i64 74 var absorbed: i64 = 0 75 var refused: i64 = 0 76 77 // ===== COUNCIL: govern the optimization (verifies=equiv, worth=cheaper) ===== 78 cc_set(a, "superopt: (mul x 8) == (shl x 3) [cheaper equivalent]" as *u8, equiv, 1, cheaper, 1, 1) 79 let vd: i64 = cc_council(a, why) 80 cc_puts(" [" as *u8); cc_puts(cc_verdict_name(vd)); cc_puts("] " as *u8); cc_puts(a.name as *u8) 81 cc_puts("\n -> " as *u8); cc_puts(why[0] as *u8); cc_puts("\n" as *u8) 82 if vd == CC_ACT { absorbed = absorbed + 1 } else { refused = refused + 1 } 83 84 // ===== NEGATIVE CONTROL: a WRONG candidate (shl x 2 = x*4) ===== 85 var neg_equiv: i64 = 1 86 var nx: i64 = 0 - 128 87 while nx <= 128 { 88 if (nx << 2) != (nx * 8) { neg_equiv = 0 } 89 nx = nx + 1 90 } 91 cc_set(a, "superopt: (mul x 8) == (shl x 2) [WRONG: = x*4]" as *u8, neg_equiv, 1, 1, 1, 1) 92 let vd2: i64 = cc_council(a, why) 93 cc_puts(" [" as *u8); cc_puts(cc_verdict_name(vd2)); cc_puts("] " as *u8); cc_puts(a.name as *u8) 94 cc_puts("\n -> " as *u8); cc_puts(why[0] as *u8); cc_puts("\n" as *u8) 95 if vd2 == CC_ACT { absorbed = absorbed + 1 } else { refused = refused + 1 } 96 97 cc_puts("----------------------------------------------------------------\n" as *u8) 98 cc_puts(" superopt (2nd generator): ABSORBED " as *u8) 99 let ab: *u8 = sys_mmap(2); ab[0] = 48 + absorbed; sys_write(1, ab, 1) 100 cc_puts(" | REFUSED " as *u8); let rf: *u8 = sys_mmap(2); rf[0] = 48 + refused; sys_write(1, rf, 1) 101 cc_puts("\n the loop now authors OPTIMIZATIONS (search-found, verified equivalent\n" as *u8) 102 cc_puts(" + cheaper) under the same governance; wrong candidates are caught.\n" as *u8) 103 cc_puts("----------------------------------------------------------------\n" as *u8) 104 105 if equiv != 1 { sys_exit(1); return 1 } // the real candidate IS equivalent 106 if cheaper != 1 { sys_exit(2); return 2 } // ... and strictly cheaper 107 if absorbed != 1 { sys_exit(3); return 3 } // real optimization absorbed 108 if refused != 1 { sys_exit(4); return 4 } // negative control refused 109 sys_exit(0) 110 return 0 111}