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}