code wiki / _hdl_build / nx_superopt_govern_test.nx

nx_superopt_govern_test.nx source

↩ module page · 74 lines · 3652 B

1// nx_superopt_govern_test.nx -- the team builds END TO END, no human in the rule: 2// the GENERATOR authors a lowering for each constant (by search), the VERIFIER 3// proves it 1:1, the COUNCIL (3->2->1) governs admission, and the winners are 4// BANKED into a rewrite library the team grew ITSELF. I wrote the searcher and the 5// council; the team wrote + selected the rules. 6// 7// GENERATE (so_best) -> VERIFY (so_verify) -> GOVERN (cc_council) -> BANK 8// 9// A genuine improvement (cheaper than mul) is ADMITTED; a constant with no cheaper 10// form (the LCG prime -> mul) is "not worth it" and the council does NOT bank it -- 11// the team only keeps real wins. Known answer: every reducible constant banked, 12// the non-reducible one rejected. exit 0. 13 14import "nx_superopt_strength.nx" 15import "nx_crew_council.nx" 16 17func sg_puts(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 } 18func sg_num(v: i64) -> i64 { 19 let b: *u8 = sys_mmap(28); var m: i64 = v; if m < 0 { m = 0 - m } 20 let t: *u8 = sys_mmap(28); var k: i64 = 0 21 if m == 0 { t[0] = 48; k = 1 } 22 while m > 0 { t[k] = 48 + (m % 10); m = m / 10; k = k + 1 } 23 var i: i64 = 0; while i < k { b[i] = t[k - 1 - i]; i = i + 1 } 24 sys_write(1, b, k); return 0 25} 26 27func main() -> i64 { 28 sg_puts("=== TEAM BUILDS END TO END: generate -> verify -> govern -> bank ===\n" as *u8) 29 let consts: *i64 = sys_mmap(8 * 16) as *i64 30 var n: i64 = 0 31 consts[n] = 8; n = n + 1 32 consts[n] = 7; n = n + 1 33 consts[n] = 9; n = n + 1 34 consts[n] = 100; n = n + 1 35 consts[n] = 31; n = n + 1 36 consts[n] = 6364136223846793005; n = n + 1 // no cheaper form -> must be rejected 37 38 let out: *i64 = sys_mmap(32) as *i64 39 let a: *CrewAction = sys_mmap(64) as *CrewAction 40 let why: *i64 = sys_mmap(8) as *i64 41 42 var banked: i64 = 0 43 var rejected: i64 = 0 44 var wins: i64 = 0 // constants the SEARCH actually found a cheaper form for 45 var i: i64 = 0 46 while i < n { 47 let C: i64 = consts[i] 48 let cost: i64 = so_best(C, out) // GENERATE 49 let verified: i64 = so_verify(out[0], out[1], out[2], out[3], C) // VERIFY 50 var worth: i64 = 0 51 if cost < SO_MUL_COST { worth = 1; wins = wins + 1 } 52 // GOVERN: Engineer=verified, Genealogist=novel, Racing=worth(cheaper), Warden=safe. 53 cc_set(a, "rewrite x*C -> shifts" as *u8, verified, 1, worth, 1, 1) 54 let vd: i64 = cc_council(a, why) 55 sg_puts(" x*" as *u8); sg_num(C); sg_puts(" cost " as *u8); sg_num(cost) 56 sg_puts(" verified " as *u8); sg_num(verified); sg_puts(" -> " as *u8); sg_puts(cc_verdict_name(vd)) 57 if vd == CC_ACT { banked = banked + 1; sg_puts(" (BANKED)\n" as *u8) } 58 else { rejected = rejected + 1; sg_puts(" (kept multiply -- no real win)\n" as *u8) } 59 i = i + 1 60 } 61 62 sg_puts("----------------------------------------------------------------\n" as *u8) 63 sg_puts(" team-authored + governed rewrite library grew by " as *u8); sg_num(banked) 64 sg_puts(" rules; " as *u8); sg_num(rejected); sg_puts(" rejected (no win).\n" as *u8) 65 sg_puts(" the team generated the rules, proved them, and chose which to keep -- itself.\n" as *u8) 66 67 // GATE: the council banked EXACTLY the genuine wins (cheaper-than-mul), and 68 // rejected the rest -- the team kept real improvements only. 69 if banked != wins { sys_exit(1); return 1 } 70 if rejected != (n - wins) { sys_exit(2); return 2 } 71 if banked < 1 { sys_exit(3); return 3 } // it must have authored SOME win 72 sys_exit(0) 73 return 0 74}