code wiki / _hdl_build / nx_doc_autoheal_gate.nx

nx_doc_autoheal_gate.nx source

↩ module page · 72 lines · 5023 B

1import "nx_gate_gn.nx" 2// nx_doc_autoheal_gate.nx -- liar-kill gate for the Doctor's autonomous RESOLVE loop (recall -> route -> fix -> 3// verify). Proves the loop turns a real failing source into a verified-clean one, AND that it is honest by 4// construction: it never invents a fix for a novel diagnostic, and never falsely claims a heal for a symptom its 5// one fixer cannot handle (reserved-keyword sub-case, clean source). Depends on the ki- catalogue carrying the 6// empty-.s lesson (seeded durably by nx_meet_bug_train); KAT1 fails LOUD if that recall is missing. expect_exit: 0 7import "nx_syscalls.nx" 8import "nx_doc_autoheal.nx" 9import "nx_gate_verdict.nx" 10 11func gp(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 } 12func slen(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} return n } 13func gfind(hay: *u8, hl: i64, needle: *u8) -> i64 { 14 let nl: i64 = slen(needle); if nl == 0 { return 0-1 } 15 var i: i64 = 0 16 while i + nl <= hl { var k: i64=0; var hit: i64=1; while k<nl { if hay[i+k]!=needle[k]{hit=0;k=nl}else{k=k+1} } if hit==1 {return i} i=i+1 } 17 return 0-1 18} 19func ghas(hay: *u8, needle: *u8) -> i64 { if gfind(hay, slen(hay), needle) >= 0 { return 1 } return 0 } 20 21func main() -> i64 { 22 gp("=== nx_doc_autoheal_gate: Doctor autonomous RESOLVE loop (recall -> route -> fix -> verify) ===\n" as *u8) 23 let out: *u8 = sys_mmap(8192) 24 let oid: *u8 = sys_mmap(128) 25 let orem: *u8 = sys_mmap(2048) 26 var pass: i64 = 0; var fail: i64 = 0 27 28 // the real diagnostic a build emits for the #1 cause (contains the NX-EMPTYS-REALERR signature) 29 let de: *u8 = "[nx_sov_build_run] nx_meet_foo: COMPILE-FAIL (empty .s after retries)" as *u8 30 31 // KAT1 the loop HEALS a real reassigned-let source end-to-end and VERIFIES the defect is gone 32 let s1: *u8 = "func f() -> i64 { let x: i64 = 0; x = 1; return x }" as *u8 33 let r1: i64 = dah_resolve(de, slen(de), s1, slen(s1), out, 8192, oid, orem) 34 if r1 == 1 { pass=pass+1 } else { fail=fail+1; gp(" FAIL kat1-not-healed r=" as *u8); gn(r1); gp("\n" as *u8) } 35 if ghas(out, "var x: i64 = 0" as *u8) == 1 { pass=pass+1 } else { fail=fail+1; gp(" FAIL kat1-no-var\n" as *u8) } 36 if gfind(out, slen(out), "let x" as *u8) < 0 { pass=pass+1 } else { fail=fail+1; gp(" FAIL kat1-let-remains\n" as *u8) } 37 if dah_has_reassigned_let(out, slen(out)) == 0 { pass=pass+1 } else { fail=fail+1; gp(" FAIL kat1-postcond-dirty\n" as *u8) } 38 if ghas(oid, "NX-EMPTYS" as *u8) == 1 { pass=pass+1 } else { fail=fail+1; gp(" FAIL kat1-wrong-recall id=" as *u8); gp(oid); gp("\n" as *u8) } 39 40 // KAT2 honest NO-FIX: an empty-.s caused by a reserved keyword (no reassigned let) -> routed to our class but our 41 // let-fixer has no applicable change -> DAH_NOFIX (the reserved-kw renamer is the sibling follow-on), NOT a fake heal 42 let s2: *u8 = "func q(match: i64) -> i64 { return match + 1 }" as *u8 43 let r2: i64 = dah_resolve(de, slen(de), s2, slen(s2), out, 8192, oid, orem) 44 if r2 == 0 { pass=pass+1 } else { fail=fail+1; gp(" FAIL kat2-should-be-nofix r=" as *u8); gn(r2); gp("\n" as *u8) } 45 46 // KAT3 neg-control: a novel/clean diagnostic -> DAH_UNKNOWN; the loop invents nothing 47 let d3: *u8 = "everything compiled and ran fine, all green, nothing to see" as *u8 48 let r3: i64 = dah_resolve(d3, slen(d3), s1, slen(s1), out, 8192, oid, orem) 49 if r3 == (0-1) { pass=pass+1 } else { fail=fail+1; gp(" FAIL kat3-should-be-unknown r=" as *u8); gn(r3); gp("\n" as *u8) } 50 51 // KAT4 the exact session case heals end-to-end 52 let s4: *u8 = "let hit1: i64 = 0; if r == 1 { hit1 = 1 }" as *u8 53 let r4: i64 = dah_resolve(de, slen(de), s4, slen(s4), out, 8192, oid, orem) 54 if r4 == 1 { pass=pass+1 } else { fail=fail+1; gp(" FAIL kat4-not-healed r=" as *u8); gn(r4); gp("\n" as *u8) } 55 if ghas(out, "var hit1" as *u8) == 1 { pass=pass+1 } else { fail=fail+1; gp(" FAIL kat4-no-var-hit1\n" as *u8) } 56 57 // KAT5 must-not-break: a clean let (never reassigned) + the same diag -> DAH_NOFIX (no false heal) 58 let s5: *u8 = "func g() -> i64 { let y: i64 = 5; return y + 1 }" as *u8 59 let r5: i64 = dah_resolve(de, slen(de), s5, slen(s5), out, 8192, oid, orem) 60 if r5 == 0 { pass=pass+1 } else { fail=fail+1; gp(" FAIL kat5-clean-falsely-touched r=" as *u8); gn(r5); gp("\n" as *u8) } 61 62 gp("DOC-AUTOHEAL-GATE pass=" as *u8); gn(pass); gp(" fail=" as *u8); gn(fail) 63 // MIGRATED onto nx_gate_verdict by nx_gate_dry_apply (D001, minimal form): every check 64 // row above is untouched, so the PASS/FAIL vector cannot change; only the hand-rolled 65 // verdict emission is replaced by the ONE shared base class. Proven by nx_gate_migrate verify. 66 let ctr__dry: *i64 = gv_ctr() 67 ctr__dry[0] = pass 68 ctr__dry[1] = pass + fail 69 let rc__dry: i64 = gv_verdict("DOC-AUTOHEAL-GATE" as *u8, ctr__dry, "autonomous resolve: recall->route->fix->verify heals real let-reassign; UNKNOWN/NOFIX honest)" as *u8) 70 sys_exit(rc__dry) 71 return rc__dry 72}