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}