nx_self_build_cycle_test.nx source

1// nx_self_build_cycle_test.nx -- THE CAPSTONE: a full autonomous SELF-BUILD CYCLE, 2// governed. The loop builds a capability itself, with the crew as checks & balances: 3// 4// GENERATOR proposes a rewrite rule as DATA (one of the eqsat identities) 5// | 6// VERIFIER PROVES it sound over ALL inputs (nx_rs_certify_unary, x in [0,2^W)) 7// | -- a real 1:1 gate-sim proof, not a claim 8// COUNCIL gates it 3 -> 2 -> 1 (Engineer=proven? + Genealogist + Racing -> 9// | Warden + Archivist -> Conductor) -- nx_crew_council 10// ABSORB admit iff the council clears it; an UNSOUND candidate is caught by 11// the Verifier (Engineer leg) and REFUSED -- never admitted. 12// 13// This is the loop building itself under governance (M2: Claude supervises, the 14// loop does the work). The Generator authors, the Verifier proves, the crew 15// governs, the ecosystem grows -- no LLM, no human in the inner loop. 16// 17// Known answer: 7 candidates authored -> 6 ADMITTED (sound rules) + 1 REFUSED 18// (mul_pow2 at the k>=W boundary, proven UNSOUND -> Engineer refuses). exit 0. 19 20import "nx_rule_soundness.nx" // the VERIFIER: certify_unary / mulpow2 boundary 21import "nx_crew_council.nx" // the GOVERNANCE: cc_council / CrewAction / CC_* 22 23const SBC_W: i64 = 8 24 25func sbc_putn(v: i64) -> i64 { 26 let b: *u8 = sys_mmap(24); var n: i64 = v; if n < 0 { n = 0 - n } 27 let t: *u8 = sys_mmap(24); var k: i64 = 0 28 if n == 0 { t[0] = 48; k = 1 } 29 while n > 0 { t[k] = 48 + (n % 10); n = n / 10; k = k + 1 } 30 var i: i64 = 0; while i < k { b[i] = t[k - 1 - i]; i = i + 1 } 31 sys_write(1, b, k); return 0 32} 33 34// VERIFIER leg: PROVE a unary rule sound over every x in [0, 2^W). Returns 1 sound. 35func sbc_prove_unary(rule: i64, vals: *i64, cells: *NxGsimCell, g: *NxGsim, 36 legs: *i64, v: *NxTriVerdict) -> i64 { 37 let hi: i64 = 1 << SBC_W 38 var x: i64 = 0 39 var ok: i64 = 0 40 while x < hi { 41 if nx_rs_certify_unary(rule, x, SBC_W, vals, cells, g, legs, v) == 1 { ok = ok + 1 } 42 x = x + 1 43 } 44 if ok == hi { return 1 } 45 return 0 46} 47 48// VERIFIER leg: is the mul_pow2 rule at shift k SOUND over W? k>=W is UNSOUND 49// (any witnessing x where the wrapped multiply disagrees with a faithful shift). 50func sbc_prove_mulpow2(k: i64) -> i64 { 51 let hi: i64 = 1 << SBC_W 52 var x: i64 = 0 53 while x < hi { 54 if nx_rs_mulpow2_boundary_unsound(x, k, SBC_W) == 1 { return 0 } 55 x = x + 1 56 } 57 return 1 58} 59 60// one cycle: author -> verify result `sound` -> council -> print -> verdict. 61func sbc_cycle(a: *CrewAction, why: *i64, name: *u8, sound: i64) -> i64 { 62 cc_set(a, name, sound, 1, 1, 1, 1) // verifies=sound; novel/worth/safe/recorded structural 63 let vd: i64 = cc_council(a, why) 64 cc_puts(" author: " as *u8); cc_puts(name) 65 cc_puts("\n VERIFY sound=" as *u8) 66 if sound == 1 { cc_puts("Y" as *u8) } else { cc_puts("N" as *u8) } 67 cc_puts(" COUNCIL=" as *u8); cc_puts(cc_verdict_name(vd)) 68 if vd == CC_ACT { cc_puts(" -> ABSORBED\n" as *u8) } else { cc_puts(" -> REFUSED (" as *u8); cc_puts(why[0] as *u8); cc_puts(")\n" as *u8) } 69 return vd 70} 71 72func main() -> i64 { 73 let vals: *i64 = sys_mmap(128 * 8) as *i64 74 let cells: *NxGsimCell = sys_mmap(128 * 48) as *NxGsimCell 75 let g: *NxGsim = sys_mmap(64) as *NxGsim 76 let legs: *i64 = sys_mmap(2 * 8) as *i64 77 let v: *NxTriVerdict = sys_mmap(64) as *NxTriVerdict 78 let a: *CrewAction = sys_mmap(64) as *CrewAction 79 let why: *i64 = sys_mmap(8) as *i64 80 81 cc_puts("================================================================\n" as *u8) 82 cc_puts(" SELF-BUILD CYCLE -- the loop builds itself, the crew governs\n" as *u8) 83 cc_puts(" Generator -> Verifier (1:1 proof) -> Council (3->2->1) -> absorb\n" as *u8) 84 cc_puts("================================================================\n" as *u8) 85 86 var admitted: i64 = 0 87 var refused: i64 = 0 88 89 if sbc_cycle(a, why, "(add x 0) == x" as *u8, sbc_prove_unary(NX_RS_ADD_ZERO, vals, cells, g, legs, v)) == CC_ACT { admitted = admitted + 1 } else { refused = refused + 1 } 90 if sbc_cycle(a, why, "(sub x x) == 0" as *u8, sbc_prove_unary(NX_RS_SUB_SELF, vals, cells, g, legs, v)) == CC_ACT { admitted = admitted + 1 } else { refused = refused + 1 } 91 if sbc_cycle(a, why, "(add x x) == (shl x 1)" as *u8, sbc_prove_unary(NX_RS_ADD_SELF, vals, cells, g, legs, v)) == CC_ACT { admitted = admitted + 1 } else { refused = refused + 1 } 92 if sbc_cycle(a, why, "(and x x) == x" as *u8, sbc_prove_unary(NX_RS_AND_SELF, vals, cells, g, legs, v)) == CC_ACT { admitted = admitted + 1 } else { refused = refused + 1 } 93 if sbc_cycle(a, why, "(or x 0) == x" as *u8, sbc_prove_unary(NX_RS_OR_ZERO, vals, cells, g, legs, v)) == CC_ACT { admitted = admitted + 1 } else { refused = refused + 1 } 94 if sbc_cycle(a, why, "(mul x 1) == x" as *u8, sbc_prove_unary(NX_RS_MUL_ONE, vals, cells, g, legs, v)) == CC_ACT { admitted = admitted + 1 } else { refused = refused + 1 } 95 // an UNSOUND candidate the Generator might propose: mul_pow2 at the k>=W boundary. 96 if sbc_cycle(a, why, "(mul x 2^8) == (shl x 8) @W=8 [BOUNDARY]" as *u8, sbc_prove_mulpow2(SBC_W)) == CC_ACT { admitted = admitted + 1 } else { refused = refused + 1 } 97 98 cc_puts("----------------------------------------------------------------\n" as *u8) 99 cc_puts(" loop authored 7 candidates -> ABSORBED " as *u8); sbc_putn(admitted) 100 cc_puts(" (proven sound) | REFUSED " as *u8); sbc_putn(refused) 101 cc_puts(" (unsound, caught)\n the loop BUILT itself -- generator authored, verifier proved 1:1,\n" as *u8) 102 cc_puts(" the crew governed; the unsound rule never entered. M2 self-build.\n" as *u8) 103 cc_puts("----------------------------------------------------------------\n" as *u8) 104 105 if admitted != 6 { sys_exit(1); return 1 } 106 if refused != 1 { sys_exit(2); return 2 } 107 sys_exit(0) 108 return 0 109}