nx_teacher_consult_gate.nx source

1// nx_teacher_consult_gate.nx -- proves CONSULT: ask the capability store by topic, get the right insights. 2// Hermetic /tmp store. Discriminating: 3// T1 topic with 2 matches -> count 2 4// T2 a more specific topic -> count 1 5// T3 case-insensitive: an upper-case query matches lower-case rules 6// T4[neg] an absent topic -> count 0 (no fabricated matches) 7// GREEN iff all. Sovereign: imports nx_teacher_consult + nx_syscalls. license_tier: ORIGINAL 8import "nx_teacher_consult.nx" 9import "nx_syscalls.nx" 10import "nx_gate_verdict.nx" 11 12func cc_puts(s: *u8) -> i64 { var n: i64 = 0; while s[n] != 0 as u8 { n = n + 1 } sys_write(1, s, n); return 0 } 13func cc_putn(v: i64) -> i64 { 14 if v == 0 { sys_write(1, "0" as *u8, 1); return 0 } 15 var m: i64 = v; if m < 0 { sys_write(1, "-" as *u8, 1); m = 0 - m } 16 let d: *u8 = sys_mmap(24); var k: i64 = 0 17 while m > 0 { d[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 } 18 var j: i64 = k - 1 19 while j >= 0 { sys_write(1, ((d as i64)+j) as *u8, 1); j = j - 1 } 20 return 0 21} 22func cc_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 } 23func cc_catn(dst: *u8, off: i64, v: i64) -> i64 { 24 var m: i64 = v; var o: i64 = off 25 let t: *u8 = sys_mmap(28); var k: i64 = 0 26 if m == 0 { t[0] = 48 as u8; k = 1 } 27 while m > 0 { t[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 } 28 var i: i64 = 0; while i < k { dst[o + i] = t[k - 1 - i]; i = i + 1 } 29 return o + k 30} 31func cc_join(out: *u8, a: *u8, b: *u8) -> i64 { var o: i64 = cc_cat(out, 0, a); o = cc_cat(out, o, b); out[o] = 0 as u8; return o } 32func cc_mkdir(path: *u8) -> i64 { return sys_mkdir(path, 0x1ed) } 33func cc_assert(label: *u8, cond: i64) -> i64 { 34 if cond != 0 { cc_puts(" [PASS] "); cc_puts(label); cc_puts("\n"); return 1 } 35 cc_puts(" [FAIL] "); cc_puts(label); cc_puts("\n"); return 0 36} 37func cc_row(w: *i64, idx: i64, id: *u8, rule: *u8) -> i64 { 38 let kb: *i64 = sys_mmap(8 * 8) as *i64 39 let vb: *i64 = sys_mmap(8 * 8) as *i64 40 kb[0] = ("id\x00") as i64; vb[0] = (id as i64) 41 kb[1] = ("rule\x00") as i64; vb[1] = (rule as i64) 42 return ncfg_add_row(w, "insight\x00" as *u8, idx, kb, vb, 2) 43} 44func cc_seed(cap: *u8) -> i64 { 45 let w: *i64 = ncfg_begin() 46 cc_row(w, 0, "I1\x00" as *u8, "alpha about publishing pages to the site\x00" as *u8) 47 cc_row(w, 1, "I2\x00" as *u8, "beta about compiling code with the toolchain\x00" as *u8) 48 cc_row(w, 2, "I3\x00" as *u8, "gamma about publishing again, a second note\x00" as *u8) 49 ncfg_set_count(w, "insight\x00" as *u8, 3) 50 return ncfg_commit(cap, w) 51} 52 53func main() -> i64 { 54 cc_puts("=== nx_teacher_consult_gate: ask the capability store by topic (case-insensitive, neg-control) ===\n") 55 let epoch: i64 = sys_now_realtime_sec() 56 let root: *u8 = sys_mmap(512) 57 var ro: i64 = cc_cat(root, 0, "/tmp/tcc-" as *u8); ro = cc_catn(root, ro, epoch); root[ro] = 0 as u8 58 cc_mkdir(root) 59 let cap: *u8 = sys_mmap(512); cc_join(cap, root, "/cap-\x00" as *u8) 60 cc_seed(cap) 61 62 var pass: i64 = 0 63 var total: i64 = 0 64 var c: i64 = 0 65 66 c = 0; if tc_consult(cap, "publish\x00" as *u8) == 2 { c = 1 } 67 total = total + 1; pass = pass + cc_assert("T1 'publish' -> 2 matches (I1, I3)", c) 68 69 c = 0; if tc_consult(cap, "compiling\x00" as *u8) == 1 { c = 1 } 70 total = total + 1; pass = pass + cc_assert("T2 'compiling' -> 1 match (I2)", c) 71 72 c = 0; if tc_consult(cap, "PUBLISHING\x00" as *u8) == 2 { c = 1 } 73 total = total + 1; pass = pass + cc_assert("T3 case-insensitive: 'PUBLISHING' -> 2", c) 74 75 c = 0; if tc_consult(cap, "zebra\x00" as *u8) == 0 { c = 1 } 76 total = total + 1; pass = pass + cc_assert("T4[neg] absent topic 'zebra' -> 0 (no fabricated matches)", c) 77 78 cc_puts("\n---- nx_teacher_consult gate: passed "); cc_putn(pass); cc_puts(" / "); cc_putn(total); cc_puts(" ----\n") 79 // MIGRATED onto nx_gate_verdict by nx_gate_dry_apply (D001, minimal form): every check 80 // row above is untouched, so the PASS/FAIL vector cannot change; only the hand-rolled 81 // verdict emission is replaced by the ONE shared base class. Proven by nx_gate_migrate verify. 82 let ctr__dry: *i64 = gv_ctr() 83 ctr__dry[0] = pass 84 ctr__dry[1] = total 85 let rc__dry: i64 = gv_verdict("TEACHER-CONSULT-GATE" as *u8, ctr__dry, "teeth unchanged; verdict emission migrated onto the shared base class" as *u8) 86 sys_exit(rc__dry) 87 return rc__dry 88}