nx_self_repair_cycle_test.nx source

1// nx_self_repair_cycle_test.nx -- the self-build cycle UPGRADED to self-REPAIR, 2// drawing on the growable RESEARCHER knowledge base (nx_research_basis). 3// Cardinal #25: when a proposal is bad, REWRITE it better -- don't just filter it. 4// 5// On UNSOUND, the loop: (1) diagnoses the failure (counterexample = WHY, CEGIS), 6// (2) the RESEARCHER consults the basis for a modern, CITED alternative, 7// (3) the VERIFIER re-proves the alternative 1:1, (4) ABSORBS the repaired 8// capability -- and ESCALATES (hard no) ONLY when the basis has no alternative. 9// 10// Star case (real, verified both ways): `(mul x 2^k) == (shl x k)` is UNSOUND at 11// the k>=W boundary; the basis's research-grounded fix is the k<W validity guard 12// (egg POPL21; Hacker's Delight). Guarded, it is sound for all k<W, all x. 13// 14// Known answer: 2 unsound proposals -> 1 REPAIRED+ABSORBED + 1 ESCALATED. exit 0. 15 16import "nx_rule_soundness.nx" // VERIFIER 17import "nx_crew_council.nx" // GOVERNANCE 18import "nx_research_basis.nx" // RESEARCHER (growable cited basis) 19 20const SR_W: i64 = 8 21 22// RESEARCHER leg: consult the basis for pattern `id`. Sets fix + citation; 1 found. 23func sr_repair_lookup(id: i64, fix_out: *i64, cite_out: *i64) -> i64 { 24 if rb_has(id) == 1 { 25 fix_out[0] = rb_fix(id) as i64 26 cite_out[0] = rb_citation(id) as i64 27 return 1 28 } 29 fix_out[0] = ("no research-grounded alternative in the basis" as *u8) as i64 30 cite_out[0] = ("" as *u8) as i64 31 return 0 32} 33 34func sr_mulpow2_unguarded_sound() -> i64 { 35 let hi: i64 = 1 << SR_W 36 var x: i64 = 0 37 while x < hi { 38 if nx_rs_mulpow2_boundary_unsound(x, SR_W, SR_W) == 1 { return 0 } 39 x = x + 1 40 } 41 return 1 42} 43 44func sr_mulpow2_guarded_sound(vals: *i64, cells: *NxGsimCell, g: *NxGsim, 45 legs: *i64, v: *NxTriVerdict) -> i64 { 46 let hi: i64 = 1 << SR_W 47 var k: i64 = 0 48 while k < SR_W { 49 var x: i64 = 0 50 while x < hi { 51 if nx_rs_certify_mulpow2(x, k, SR_W, vals, cells, g, legs, v) != 1 { return 0 } 52 x = x + 1 53 } 54 k = k + 1 55 } 56 return 1 57} 58 59func main() -> i64 { 60 let vals: *i64 = sys_mmap(128 * 8) as *i64 61 let cells: *NxGsimCell = sys_mmap(128 * 48) as *NxGsimCell 62 let g: *NxGsim = sys_mmap(64) as *NxGsim 63 let legs: *i64 = sys_mmap(2 * 8) as *i64 64 let v: *NxTriVerdict = sys_mmap(64) as *NxTriVerdict 65 let a: *CrewAction = sys_mmap(64) as *CrewAction 66 let why: *i64 = sys_mmap(8) as *i64 67 let fix: *i64 = sys_mmap(8) as *i64 68 let cite: *i64 = sys_mmap(8) as *i64 69 70 cc_puts("================================================================\n" as *u8) 71 cc_puts(" SELF-REPAIR CYCLE -- unsound? the RESEARCHER proposes a cited,\n" as *u8) 72 cc_puts(" research-grounded fix; hard-no only if the basis has none (#25)\n" as *u8) 73 cc_puts("================================================================\n" as *u8) 74 75 var repaired: i64 = 0 76 var escalated: i64 = 0 77 78 // ---- Candidate 1: (mul x 2^k) == (shl x k), UNGUARDED ---- 79 cc_puts(" author: (mul x 2^k) == (shl x k) [unguarded]\n" as *u8) 80 let s1: i64 = sr_mulpow2_unguarded_sound() 81 if s1 == 1 { 82 cc_puts(" VERIFY sound=Y -> absorb\n" as *u8); repaired = repaired + 1 83 } else { 84 cc_puts(" VERIFY sound=N (counterexample at k>=W: wrapped mul collapses to 0)\n" as *u8) 85 let hr: i64 = sr_repair_lookup(RB_STRENGTH_SHIFT, fix, cite) 86 if hr == 1 { 87 cc_puts(" RESEARCHER proposes: " as *u8); cc_puts(fix[0] as *u8) 88 cc_puts("\n [research: " as *u8); cc_puts(cite[0] as *u8); cc_puts("]\n" as *u8) 89 let s1b: i64 = sr_mulpow2_guarded_sound(vals, cells, g, legs, v) 90 cc_puts(" RE-VERIFY guarded (k<W): sound=" as *u8) 91 if s1b == 1 { cc_puts("Y" as *u8) } else { cc_puts("N" as *u8) } 92 cc_set(a, "(mul x 2^k) == (shl x k) WHEN k<W [repaired]" as *u8, s1b, 1, 1, 1, 1) 93 let vd: i64 = cc_council(a, why) 94 cc_puts(" COUNCIL=" as *u8); cc_puts(cc_verdict_name(vd)) 95 if vd == CC_ACT { cc_puts(" -> ABSORBED (REPAIRED)\n" as *u8); repaired = repaired + 1 } else { cc_puts(" -> escalate\n" as *u8); escalated = escalated + 1 } 96 } else { 97 cc_puts(" no alternative -> ESCALATE\n" as *u8); escalated = escalated + 1 98 } 99 } 100 101 // ---- Candidate 2: an unsound proposal with NO basis entry ---- 102 cc_puts(" author: (some speculative identity, proven unsound)\n" as *u8) 103 cc_puts(" VERIFY sound=N\n" as *u8) 104 let hr2: i64 = sr_repair_lookup(RB_NONE, fix, cite) 105 if hr2 == 1 { 106 cc_puts(" RESEARCHER proposes a fix -> repair\n" as *u8); repaired = repaired + 1 107 } else { 108 cc_puts(" RESEARCHER: " as *u8); cc_puts(fix[0] as *u8) 109 cc_puts(" -> ESCALATE to operator (hard no, justified)\n" as *u8); escalated = escalated + 1 110 } 111 112 cc_puts("----------------------------------------------------------------\n" as *u8) 113 cc_puts(" 2 unsound proposals -> REPAIRED+ABSORBED " as *u8) 114 let rp: *u8 = sys_mmap(2); rp[0] = 48 + repaired; sys_write(1, rp, 1) 115 cc_puts(" | ESCALATED " as *u8) 116 let es: *u8 = sys_mmap(2); es[0] = 48 + escalated; sys_write(1, es, 1) 117 cc_puts("\n the loop REWRITES bad proposals better (research-grounded + cited)\n" as *u8) 118 cc_puts(" and hard-stops only when no alternative exists. intelligence, never strip.\n" as *u8) 119 cc_puts("----------------------------------------------------------------\n" as *u8) 120 121 if repaired != 1 { sys_exit(1); return 1 } 122 if escalated != 1 { sys_exit(2); return 2 } 123 sys_exit(0) 124 return 0 125}