code wiki / _hdl_build / nx_teacher_trainer_gate.nx

nx_teacher_trainer_gate.nx

buildroot/runtime/_hdl_build/nx_teacher_trainer_gate.nx

5706 B103 linesdepth 11pulls 12 transitivereach 0 importersview sourcekind gate/prooftopic teacher
docsdependenciesstructsconstsfunctions

about

nx_teacher_trainer_gate.nx -- proves the TRAINER: spaced-retrieval scheduling + the coverage meter, over a hermetic /tmp capability store. Time is passed explicitly so spacing is testable. T1 all-new-due: 3 fresh insights -> due=3 T2 zero-coverage: nothing practiced -> covered=0 T3 practice records reps=1, interval=1 (first practice -> 1-day spacing) T4 not-due-within-interval: just-practiced I1 is NOT due at T (due=T+1day) T5 coverage rises: covered=1 after practicing I1 T6 due-resurfaces: at T+2days I1 is due again (spacing elapsed) -> due=3 T7 spacing-grows: second success doubles interval (1 -> 2) T8[neg] only-practiced-counts: I2/I3 never practiced -> coverage stays 1 (no fake coverage) T9 full: practice I2,I3 -> coverage=3 and due=0 (all freshly scheduled into the future) GREEN iff all. Sovereign: imports nx_teacher_trainer + nx_syscalls. license_tier: ORIGINAL

dependencies 2 imports · 0 importers

nx_teacher_trainer.nx nx_syscalls.nx nx_teacher_trainer_gate.nx

imports: nx_teacher_trainer.nxnx_syscalls.nx

imported by: nobody (leaf or entry point)

call flow from main pre-order; caps 40 nodes / depth 6 declared; ↻ = already shown

main gt_puts sys_write sys_now_realtime_sec sys_mmap sys_clock_gettime_real sys_mmap ↻ gt_cat gt_catn sys_mmap ↻ gt_mkdir sys_mkdir gt_join gt_cat ↻ gt_write sys_openat_wr sys_write ↻ sys_close tsyn_merge_cols sys_mmap ↻ sys_read_file sys_openat_rd sys_lseek sys_mmap ↻ sys_read sys_close ↻ ncfg_open ss_open_cached ssc_init sys_mmap ↻ ssc_sig_of ss_cat sys_fstatat ssc_streq ss_open ss_open2 sys_mmap ↻ ss_manifest_dyn ss_cat ↻ ss_loadfile

structs

none

consts

none

functions

17func 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 }
called by 2: gt_assertmain calls 1: sys_write
18func gt_putn(v: i64) -> i64
called by 1: main calls 2: sys_writesys_mmap
27func 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 }
called by 2: gt_joinmain
28func gt_catn(dst: *u8, off: i64, v: i64) -> i64
called by 1: main calls 1: sys_mmap
36func 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 }
called by 1: main calls 1: gt_cat
37func gt_mkdir(path: *u8) -> i64 { return sys_mkdir(path, 0x1ed) }
called by 1: main calls 1: sys_mkdir
38func gt_write(path: *u8, content: *u8) -> i64
called by 1: main calls 3: sys_openat_wrsys_writesys_close
44func gt_assert(label: *u8, cond: i64) -> i64
called by 1: main calls 1: gt_puts
49func main() -> i64
calls 16: gt_putssys_now_realtime_secsys_mmapgt_catgt_catngt_mkdir+10