nx_teacher_synthesize_gate.nx source

1// nx_teacher_synthesize_gate.nx -- proves the Teacher SYNTHESIS loop: a raw insight-ledger is consumed 2// INTO the native team-capability store, the team can RECALL each insight, and the source is provably 3// REDUNDANT only when every insight is absorbed. 4// 5// Hermetic /tmp fixtures (never touches the real store). Discriminating + liar-killed: 6// T1 count: synthesizing a 3-row ledger stores exactly 3 insights. 7// T2 recall: the team CONSUMES insight R2 from the store, byte-faithful to the source learning. 8// T3 recall-absent: an unknown id recalls nothing (no phantom answer). 9// T4 redundancy+: every learning of the synthesized ledger is recoverable -> redundant=1 (retirable). 10// T5[neg] un-absorbed: a SUPERSET ledger (one extra un-synthesized row) is redundant=0 -- you CANNOT 11// retire a source whose insight was not fully absorbed (the load-bearing control). 12// T6[neg] no-fabrication: a rule never present in the source is ABSENT from the store (Rule 4 -- the 13// synthesis copies real insight, it does not invent any). 14// T7 idempotent: re-synthesizing the same ledger keeps count=3 and redundant=1. 15// GREEN iff all hold. Sovereign: imports nx_teacher_synthesize + nx_syscalls. license_tier: ORIGINAL 16import "nx_teacher_synthesize.nx" 17import "nx_syscalls.nx" 18import "nx_gate_verdict.nx" 19 20func tg_puts(s: *u8) -> i64 { var n: i64 = 0; while s[n] != 0 as u8 { n = n + 1 } sys_write(1, s, n); return 0 } 21func tg_putn(v: i64) -> i64 { 22 if v == 0 { sys_write(1, "0" as *u8, 1); return 0 } 23 var m: i64 = v; if m < 0 { sys_write(1, "-" as *u8, 1); m = 0 - m } 24 let d: *u8 = sys_mmap(24); var k: i64 = 0 25 while m > 0 { d[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 } 26 var j: i64 = k - 1 27 while j >= 0 { sys_write(1, ((d as i64)+j) as *u8, 1); j = j - 1 } 28 return 0 29} 30func tg_cat(dst: *u8, off: i64, s: *u8) -> i64 { var i: i64 = 0; while s[i] != 0 as u8 { dst[off + i] = s[i]; i = i + 1 } return off + i } 31func tg_catn(dst: *u8, off: i64, v: i64) -> i64 { 32 var m: i64 = v; var o: i64 = off 33 let t: *u8 = sys_mmap(28); var k: i64 = 0 34 if m == 0 { t[0] = 48 as u8; k = 1 } 35 while m > 0 { t[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 } 36 var i: i64 = 0; while i < k { dst[o + i] = t[k - 1 - i]; i = i + 1 } 37 return o + k 38} 39func tg_join(out: *u8, a: *u8, b: *u8) -> i64 { var o: i64 = tg_cat(out, 0, a); o = tg_cat(out, o, b); out[o] = 0 as u8; return o } 40func tg_mkdir(path: *u8) -> i64 { return sys_mkdir(path, 0x1ed) } 41func tg_write(path: *u8, content: *u8) -> i64 { 42 let fd: i64 = sys_openat_wr(path, 0x1a4) 43 if fd < 0 { return 0 - 1 } 44 var n: i64 = 0; while content[n] != 0 as u8 { n = n + 1 } 45 sys_write(fd, content, n); sys_close(fd); return 0 46} 47func tg_assert(label: *u8, cond: i64) -> i64 { 48 if cond != 0 { tg_puts(" [PASS] "); tg_puts(label); tg_puts("\n"); return 1 } 49 tg_puts(" [FAIL] "); tg_puts(label); tg_puts("\n"); return 0 50} 51 52func main() -> i64 { 53 tg_puts("=== nx_teacher_synthesize_gate: consume->synthesize->redundant loop (fixtures + liar-kill) ===\n") 54 let epoch: i64 = sys_now_realtime_sec() 55 let root: *u8 = sys_mmap(512) 56 var ro: i64 = tg_cat(root, 0, "/tmp/tsg-" as *u8); ro = tg_catn(root, ro, epoch); root[ro] = 0 as u8 57 tg_mkdir(root) 58 let fixA: *u8 = sys_mmap(512); tg_join(fixA, root, "/ledger_a.tsv\x00" as *u8) 59 let fixB: *u8 = sys_mmap(512); tg_join(fixB, root, "/ledger_b.tsv\x00" as *u8) 60 let store: *u8 = sys_mmap(512); tg_join(store, root, "/store-\x00" as *u8) 61 62 // fixture A = 3 real insight rows (id<TAB>class<TAB>learning<TAB>reinforces); a '#' comment is skipped. 63 tg_write(fixA, "# fixture insight ledger\nR1\tCHEAT\tALPHA insight one orient via Read not shell\tplanning_prefs\nR2\tPROCESS\tBETA insight two measure before hypothesize\tDIGEST-FIRST\nR3\tDRY\tGAMMA insight three compose existing organs\trule15\n\x00" as *u8) 64 // fixture B = A + one EXTRA row never synthesized into the store 65 tg_write(fixB, "# fixture insight ledger\nR1\tCHEAT\tALPHA insight one orient via Read not shell\tplanning_prefs\nR2\tPROCESS\tBETA insight two measure before hypothesize\tDIGEST-FIRST\nR3\tDRY\tGAMMA insight three compose existing organs\trule15\nR4\tNEW\tDELTA insight four never synthesized\tlawX\n\x00" as *u8) 66 67 let cnt: i64 = tsyn_ingest_ledger(fixA, "fixtureA\x00" as *u8, store) 68 tg_puts(" synthesized count="); tg_putn(cnt); tg_puts("\n") 69 70 var pass: i64 = 0 71 var total: i64 = 0 72 var c: i64 = 0 73 74 c = 0; if cnt == 3 { c = 1 } 75 total = total + 1; pass = pass + tg_assert("T1 synthesized count == 3", c) 76 77 let out: *u8 = sys_mmap(4096) 78 let r2: i64 = tsyn_recall(store, "R2\x00" as *u8, out) 79 c = 0; if r2 == 1 { if tsyn_streq(out, "BETA insight two measure before hypothesize\x00" as *u8) == 1 { c = 1 } } 80 total = total + 1; pass = pass + tg_assert("T2 recall R2 from teacher store == faithful source learning", c) 81 82 let out2: *u8 = sys_mmap(64) 83 c = 0; if tsyn_recall(store, "NOPE\x00" as *u8, out2) == 0 { c = 1 } 84 total = total + 1; pass = pass + tg_assert("T3 recall unknown id -> not found (no phantom answer)", c) 85 86 c = 0; if tsyn_redundant(fixA, store) == 1 { c = 1 } 87 total = total + 1; pass = pass + tg_assert("T4 redundancy+: every learning recoverable -> source REDUNDANT", c) 88 89 c = 0; if tsyn_redundant(fixB, store) == 0 { c = 1 } 90 total = total + 1; pass = pass + tg_assert("T5[neg] superset ledger w/ un-synthesized row -> redundant=0 (cannot retire un-absorbed)", c) 91 92 let h: *i64 = ncfg_open(store) 93 c = 0; if tsyn_store_has_rule(h, "PHANTOM fabricated insight never in source\x00" as *u8) == 0 { c = 1 } 94 total = total + 1; pass = pass + tg_assert("T6[neg] no-fabrication: a rule never in source is ABSENT from the store", c) 95 96 let cnt2: i64 = tsyn_ingest_ledger(fixA, "fixtureA\x00" as *u8, store) 97 c = 0; if cnt2 == 3 { if tsyn_redundant(fixA, store) == 1 { c = 1 } } 98 total = total + 1; pass = pass + tg_assert("T7 idempotent: re-synthesis keeps count=3 + redundant=1", c) 99 100 tg_puts("\n---- nx_teacher_synthesize gate: passed "); tg_putn(pass); tg_puts(" / "); tg_putn(total); tg_puts(" ----\n") 101 // MIGRATED onto nx_gate_verdict by nx_gate_dry_apply (D001, minimal form): every check 102 // row above is untouched, so the PASS/FAIL vector cannot change; only the hand-rolled 103 // verdict emission is replaced by the ONE shared base class. Proven by nx_gate_migrate verify. 104 let ctr__dry: *i64 = gv_ctr() 105 ctr__dry[0] = pass 106 ctr__dry[1] = total 107 let rc__dry: i64 = gv_verdict("TEACHER-SYNTHESIZE-GATE" as *u8, ctr__dry, "teeth unchanged; verdict emission migrated onto the shared base class" as *u8) 108 sys_exit(rc__dry) 109 return rc__dry 110}