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" 18 19func 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 } 20func tg_putn(v: i64) -> i64 { 21 if v == 0 { sys_write(1, "0" as *u8, 1); return 0 } 22 var m: i64 = v; if m < 0 { sys_write(1, "-" as *u8, 1); m = 0 - m } 23 let d: *u8 = sys_mmap(24); var k: i64 = 0 24 while m > 0 { d[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 } 25 var j: i64 = k - 1 26 while j >= 0 { sys_write(1, ((d as i64)+j) as *u8, 1); j = j - 1 } 27 return 0 28} 29func 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 } 30func tg_catn(dst: *u8, off: i64, v: i64) -> i64 { 31 var m: i64 = v; var o: i64 = off 32 let t: *u8 = sys_mmap(28); var k: i64 = 0 33 if m == 0 { t[0] = 48 as u8; k = 1 } 34 while m > 0 { t[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 } 35 var i: i64 = 0; while i < k { dst[o + i] = t[k - 1 - i]; i = i + 1 } 36 return o + k 37} 38func 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 } 39func tg_mkdir(path: *u8) -> i64 { return sys_mkdir(path, 0x1ed) } 40func tg_write(path: *u8, content: *u8) -> i64 { 41 let fd: i64 = sys_openat_wr(path, 0x1a4) 42 if fd < 0 { return 0 - 1 } 43 var n: i64 = 0; while content[n] != 0 as u8 { n = n + 1 } 44 sys_write(fd, content, n); sys_close(fd); return 0 45} 46func tg_assert(label: *u8, cond: i64) -> i64 { 47 if cond != 0 { tg_puts(" [PASS] "); tg_puts(label); tg_puts("\n"); return 1 } 48 tg_puts(" [FAIL] "); tg_puts(label); tg_puts("\n"); return 0 49} 50 51func main() -> i64 { 52 tg_puts("=== nx_teacher_synthesize_gate: consume->synthesize->redundant loop (fixtures + liar-kill) ===\n") 53 let epoch: i64 = sys_now_realtime_sec() 54 let root: *u8 = sys_mmap(512) 55 var ro: i64 = tg_cat(root, 0, "/tmp/tsg-" as *u8); ro = tg_catn(root, ro, epoch); root[ro] = 0 as u8 56 tg_mkdir(root) 57 let fixA: *u8 = sys_mmap(512); tg_join(fixA, root, "/ledger_a.tsv\x00" as *u8) 58 let fixB: *u8 = sys_mmap(512); tg_join(fixB, root, "/ledger_b.tsv\x00" as *u8) 59 let store: *u8 = sys_mmap(512); tg_join(store, root, "/store-\x00" as *u8) 60 61 // fixture A = 3 real insight rows (id<TAB>class<TAB>learning<TAB>reinforces); a '#' comment is skipped. 62 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) 63 // fixture B = A + one EXTRA row never synthesized into the store 64 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) 65 66 let cnt: i64 = tsyn_ingest_ledger(fixA, "fixtureA\x00" as *u8, store) 67 tg_puts(" synthesized count="); tg_putn(cnt); tg_puts("\n") 68 69 var pass: i64 = 0 70 var total: i64 = 0 71 var c: i64 = 0 72 73 c = 0; if cnt == 3 { c = 1 } 74 total = total + 1; pass = pass + tg_assert("T1 synthesized count == 3", c) 75 76 let out: *u8 = sys_mmap(4096) 77 let r2: i64 = tsyn_recall(store, "R2\x00" as *u8, out) 78 c = 0; if r2 == 1 { if tsyn_streq(out, "BETA insight two measure before hypothesize\x00" as *u8) == 1 { c = 1 } } 79 total = total + 1; pass = pass + tg_assert("T2 recall R2 from teacher store == faithful source learning", c) 80 81 let out2: *u8 = sys_mmap(64) 82 c = 0; if tsyn_recall(store, "NOPE\x00" as *u8, out2) == 0 { c = 1 } 83 total = total + 1; pass = pass + tg_assert("T3 recall unknown id -> not found (no phantom answer)", c) 84 85 c = 0; if tsyn_redundant(fixA, store) == 1 { c = 1 } 86 total = total + 1; pass = pass + tg_assert("T4 redundancy+: every learning recoverable -> source REDUNDANT", c) 87 88 c = 0; if tsyn_redundant(fixB, store) == 0 { c = 1 } 89 total = total + 1; pass = pass + tg_assert("T5[neg] superset ledger w/ un-synthesized row -> redundant=0 (cannot retire un-absorbed)", c) 90 91 let h: *i64 = ncfg_open(store) 92 c = 0; if tsyn_store_has_rule(h, "PHANTOM fabricated insight never in source\x00" as *u8) == 0 { c = 1 } 93 total = total + 1; pass = pass + tg_assert("T6[neg] no-fabrication: a rule never in source is ABSENT from the store", c) 94 95 let cnt2: i64 = tsyn_ingest_ledger(fixA, "fixtureA\x00" as *u8, store) 96 c = 0; if cnt2 == 3 { if tsyn_redundant(fixA, store) == 1 { c = 1 } } 97 total = total + 1; pass = pass + tg_assert("T7 idempotent: re-synthesis keeps count=3 + redundant=1", c) 98 99 tg_puts("\n---- nx_teacher_synthesize gate: passed "); tg_putn(pass); tg_puts(" / "); tg_putn(total); tg_puts(" ----\n") 100 if pass == total { tg_puts("verdict=GREEN\n"); sys_exit(0); return 0 } 101 tg_puts("verdict=RED\n"); sys_exit(1); return 1 102}