code wiki / _hdl_build / nx_teacher_trainer_gate.nx

nx_teacher_trainer_gate.nx source

↩ module page · 111 lines · 6167 B

1// nx_teacher_trainer_gate.nx -- proves the TRAINER: spaced-retrieval scheduling + the coverage meter, 2// over a hermetic /tmp capability store. Time is passed explicitly so spacing is testable. 3// 4// T1 all-new-due: 3 fresh insights -> due=3 5// T2 zero-coverage: nothing practiced -> covered=0 6// T3 practice records reps=1, interval=1 (first practice -> 1-day spacing) 7// T4 not-due-within-interval: just-practiced I1 is NOT due at T (due=T+1day) 8// T5 coverage rises: covered=1 after practicing I1 9// T6 due-resurfaces: at T+2days I1 is due again (spacing elapsed) -> due=3 10// T7 spacing-grows: second success doubles interval (1 -> 2) 11// T8[neg] only-practiced-counts: I2/I3 never practiced -> coverage stays 1 (no fake coverage) 12// T9 full: practice I2,I3 -> coverage=3 and due=0 (all freshly scheduled into the future) 13// GREEN iff all. Sovereign: imports nx_teacher_trainer + nx_syscalls. license_tier: ORIGINAL 14import "nx_teacher_trainer.nx" 15import "nx_syscalls.nx" 16import "nx_gate_verdict.nx" 17 18func gt_puts(s: *u8) -> i64 { var n: i64 = 0; while s[n] != 0 as u8 { n = n + 1 } sys_write(1, s, n); return 0 } 19func gt_putn(v: i64) -> i64 { 20 if v == 0 { sys_write(1, "0" as *u8, 1); return 0 } 21 var m: i64 = v; if m < 0 { sys_write(1, "-" as *u8, 1); m = 0 - m } 22 let d: *u8 = sys_mmap(24); var k: i64 = 0 23 while m > 0 { d[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 } 24 var j: i64 = k - 1 25 while j >= 0 { sys_write(1, ((d as i64)+j) as *u8, 1); j = j - 1 } 26 return 0 27} 28func gt_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 } 29func gt_catn(dst: *u8, off: i64, v: i64) -> i64 { 30 var m: i64 = v; var o: i64 = off 31 let t: *u8 = sys_mmap(28); var k: i64 = 0 32 if m == 0 { t[0] = 48 as u8; k = 1 } 33 while m > 0 { t[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 } 34 var i: i64 = 0; while i < k { dst[o + i] = t[k - 1 - i]; i = i + 1 } 35 return o + k 36} 37func gt_join(out: *u8, a: *u8, b: *u8) -> i64 { var o: i64 = gt_cat(out, 0, a); o = gt_cat(out, o, b); out[o] = 0 as u8; return o } 38func gt_mkdir(path: *u8) -> i64 { return sys_mkdir(path, 0x1ed) } 39func gt_write(path: *u8, content: *u8) -> i64 { 40 let fd: i64 = sys_openat_wr(path, 0x1a4) 41 if fd < 0 { return 0 - 1 } 42 var n: i64 = 0; while content[n] != 0 as u8 { n = n + 1 } 43 sys_write(fd, content, n); sys_close(fd); return 0 44} 45func gt_assert(label: *u8, cond: i64) -> i64 { 46 if cond != 0 { gt_puts(" [PASS] "); gt_puts(label); gt_puts("\n"); return 1 } 47 gt_puts(" [FAIL] "); gt_puts(label); gt_puts("\n"); return 0 48} 49 50func main() -> i64 { 51 gt_puts("=== nx_teacher_trainer_gate: spaced-retrieval scheduling + coverage meter (time-driven, neg-control) ===\n") 52 let epoch: i64 = sys_now_realtime_sec() 53 let root: *u8 = sys_mmap(512) 54 var ro: i64 = gt_cat(root, 0, "/tmp/ttr-" as *u8); ro = gt_catn(root, ro, epoch); root[ro] = 0 as u8 55 gt_mkdir(root) 56 let led: *u8 = sys_mmap(512); gt_join(led, root, "/cap.tsv\x00" as *u8) 57 let cap: *u8 = sys_mmap(512); gt_join(cap, root, "/cap-\x00" as *u8) 58 let state: *u8 = sys_mmap(512); gt_join(state, root, "/state-\x00" as *u8) 59 gt_write(led, "# cap\nI1\tC\trule one\tx\nI2\tC\trule two\tx\nI3\tC\trule three\tx\n\x00" as *u8) 60 tsyn_merge_cols(led, "fix\x00" as *u8, cap, 0, 2) // seed the capability store: 3 insights 61 62 let T: i64 = 1000000000 // a fixed synthetic "now" 63 let T2: i64 = T + 2 * 86400 // two days later 64 65 var pass: i64 = 0 66 var total: i64 = 0 67 var c: i64 = 0 68 let st: *i64 = sys_mmap(8 * 4) as *i64 69 70 c = 0; if trn_due_count(cap, state, T) == 3 { c = 1 } 71 total = total + 1; pass = pass + gt_assert("T1 all-new-due: 3 fresh insights are due", c) 72 73 c = 0; if trn_coverage(cap, state) == 0 { c = 1 } 74 total = total + 1; pass = pass + gt_assert("T2 zero-coverage: nothing practiced yet", c) 75 76 trn_practice(state, "I1\x00" as *u8, T) 77 c = 0; if trn_state(state, "I1\x00" as *u8, st) == 1 { if st[0] == 1 { if st[1] == 1 { c = 1 } } } 78 total = total + 1; pass = pass + gt_assert("T3 practice I1 -> reps=1 interval=1 (first practice, 1-day spacing)", c) 79 80 c = 0; if trn_due_count(cap, state, T) == 2 { c = 1 } 81 total = total + 1; pass = pass + gt_assert("T4 not-due-within-interval: I1 not due at T (due=T+1day)", c) 82 83 c = 0; if trn_coverage(cap, state) == 1 { c = 1 } 84 total = total + 1; pass = pass + gt_assert("T5 coverage rises: covered=1", c) 85 86 c = 0; if trn_due_count(cap, state, T2) == 3 { c = 1 } 87 total = total + 1; pass = pass + gt_assert("T6 due-resurfaces: at T+2days I1 is due again", c) 88 89 trn_practice(state, "I1\x00" as *u8, T2) 90 c = 0; if trn_state(state, "I1\x00" as *u8, st) == 1 { if st[0] == 2 { if st[1] == 2 { c = 1 } } } 91 total = total + 1; pass = pass + gt_assert("T7 spacing-grows: second success doubles interval (1 -> 2)", c) 92 93 c = 0; if trn_coverage(cap, state) == 1 { c = 1 } 94 total = total + 1; pass = pass + gt_assert("T8[neg] only-practiced-counts: I2/I3 never practiced -> coverage stays 1", c) 95 96 trn_practice(state, "I2\x00" as *u8, T2) 97 trn_practice(state, "I3\x00" as *u8, T2) 98 c = 0; if trn_coverage(cap, state) == 3 { if trn_due_count(cap, state, T2) == 0 { c = 1 } } 99 total = total + 1; pass = pass + gt_assert("T9 full: practice all -> coverage=3 and due=0 (all scheduled ahead)", c) 100 101 gt_puts("\n---- nx_teacher_trainer gate: passed "); gt_putn(pass); gt_puts(" / "); gt_putn(total); gt_puts(" ----\n") 102 // MIGRATED onto nx_gate_verdict by nx_gate_dry_apply (D001, minimal form): every check 103 // row above is untouched, so the PASS/FAIL vector cannot change; only the hand-rolled 104 // verdict emission is replaced by the ONE shared base class. Proven by nx_gate_migrate verify. 105 let ctr__dry: *i64 = gv_ctr() 106 ctr__dry[0] = pass 107 ctr__dry[1] = total 108 let rc__dry: i64 = gv_verdict("TEACHER-TRAINER-GATE" as *u8, ctr__dry, "teeth unchanged; verdict emission migrated onto the shared base class" as *u8) 109 sys_exit(rc__dry) 110 return rc__dry 111}