nx_autofix_cascade_gate.nx source

1// nx_autofix_cascade_gate.nx -- gate for THE NEURO-SYMBOLIC ENSEMBLE (nx_autofix_cascade). 2// On nx_gate_verdict (D001 law). Proves the union is computed correctly + sound: 3// T1 instance green in ledger1 ONLY -> resolved 4// T2 instance green in ledger2 ONLY -> resolved (complementarity = the whole point) 5// T3 instance MISS in both -> unresolved 6// T4 union count exact (3/4 over the synthetic complementary pair) 7// T5 property-verified count = greens with symj=GREEN (soundness signal) 8// T6 single-ledger mode = just ledger1 (2/4) -- degrades to one maker cleanly 9// Requires /tmp/nx_autofix_cascade.sov.elf staged. license_tier: ORIGINAL expect_exit: 0 10import "nx_seg_store.nx" 11import "nx_deploy_lib.nx" 12import "nx_gate_verdict.nx" 13import "nx_syscalls.nx" 14 15const ACG_CAP: i64 = 65536 16 17func acg_slen(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } return n } 18func acg_has(q: *u8, n: i64, s: *u8) -> i64 { 19 let sn: i64 = acg_slen(s) 20 if sn == 0 { return 1 } 21 var i: i64 = 0 22 while i + sn <= n { 23 var hit: i64 = 1 24 var j: i64 = 0 25 while j < sn { if q[i+j] != s[j] { hit = 0; j = sn } else { j = j + 1 } } 26 if hit == 1 { return 1 } 27 i = i + 1 28 } 29 return 0 30} 31 32func main() -> i64 { 33 let ctr: *i64 = gv_ctr() 34 gv_head("nx_autofix_cascade gate -- neuro-symbolic ensemble: sound union of property-verified greens" as *u8) 35 let elf: *u8 = "/tmp/nx_autofix_cascade.sov.elf" as *u8 36 37 // synthetic complementary makers over 4 instances a,b,c,d (each ledger single-batch, one row/cand) 38 let man: *u8 = "a|runtime/a.nx\nb|runtime/b.nx\nc|runtime/c.nx\nd|runtime/d.nx\n" as *u8 39 let l1: *u8 = "AUTOFIX-AUTO ts=1 cand=a located=a attempts=1 maker=GREEN revert=1 symj=GREEN\nAUTOFIX-AUTO ts=1 cand=b located=b attempts=5 maker=MISS revert=1 symj=SKIP\nAUTOFIX-AUTO ts=1 cand=c located=c attempts=1 maker=GREEN revert=1 symj=GREEN\nAUTOFIX-AUTO ts=1 cand=d located=d attempts=5 maker=MISS revert=1 symj=SKIP\n" as *u8 40 let l2: *u8 = "AUTOFIX-AUTO ts=2 cand=a located=a attempts=5 maker=MISS revert=1 symj=SKIP\nAUTOFIX-AUTO ts=2 cand=b located=b attempts=1 maker=GREEN revert=1 symj=GREEN\nAUTOFIX-AUTO ts=2 cand=c located=c attempts=5 maker=MISS revert=1 symj=SKIP\nAUTOFIX-AUTO ts=2 cand=d located=d attempts=5 maker=MISS revert=1 symj=SKIP\n" as *u8 41 ss_writefile("/tmp/acg_man.txt" as *u8, man, acg_slen(man)) 42 ss_writefile("/tmp/acg_l1.txt" as *u8, l1, acg_slen(l1)) 43 ss_writefile("/tmp/acg_l2.txt" as *u8, l2, acg_slen(l2)) 44 45 // cascade over BOTH ledgers 46 let av: *i64 = sys_mmap(64) as *i64 47 av[0] = "/tmp/acg_man.txt" as *u8 as i64 48 av[1] = "/tmp/acg_l1.txt" as *u8 as i64 49 av[2] = "/tmp/acg_l2.txt" as *u8 as i64 50 dep_run_capture(elf, av, 3, "/tmp/acg_out.txt" as *u8) 51 let c: *u8 = sys_mmap(ACG_CAP) 52 let n: i64 = dp_read("/tmp/acg_out.txt" as *u8, c, ACG_CAP - 4) 53 54 gv_check("T1 green-in-ledger1-only resolved (a)" as *u8, acg_has(c, n, "a -> RESOLVED by ledger#1" as *u8), ctr) 55 gv_check("T2 green-in-ledger2-only resolved (b)" as *u8, acg_has(c, n, "b -> RESOLVED by ledger#2" as *u8), ctr) 56 gv_check("T3 miss-in-both unresolved (d)" as *u8, acg_has(c, n, "d -> unresolved by any maker" as *u8), ctr) 57 gv_check("T4 union count exact 3/4" as *u8, acg_has(c, n, "3/4 resolved = 75%" as *u8), ctr) 58 gv_check("T5 property-verified count 3" as *u8, acg_has(c, n, "3 property-verified" as *u8), ctr) 59 60 // single-ledger mode = just ledger1 -> a,c resolved = 2/4 61 av[1] = "/tmp/acg_l1.txt" as *u8 as i64 62 dep_run_capture(elf, av, 2, "/tmp/acg_out2.txt" as *u8) 63 let c2: *u8 = sys_mmap(ACG_CAP) 64 let n2: i64 = dp_read("/tmp/acg_out2.txt" as *u8, c2, ACG_CAP - 4) 65 gv_check("T6 single-maker degrades cleanly 2/4" as *u8, acg_has(c2, n2, "2/4 resolved = 50%" as *u8), ctr) 66 67 let rc: i64 = gv_verdict("AUTOFIX-CASCADE-GATE" as *u8, ctr, "sound union of property-verified greens across diverse makers" as *u8) 68 sys_exit(rc) 69 return rc 70}