code wiki / (root) / nx_dr_run_gate.nx

nx_dr_run_gate.nx source

↩ module page · 92 lines · 3869 B

1// nx_dr_run_gate.nx -- KAT + neg-control for the real-text matching/judge stage (DR-0 rung-2). 2// Proves the tokenizer (count, case-insensitivity, determinism) and token-containment matching 3// on REAL English strings, the coverage-at-threshold decision, insight-recall aggregation, and 4// the NEG-CONTROL: an insight with no lexical overlap is NEVER covered (so recall can't be 5// inflated). DRY nx_gate_verdict lib. 6import "nx_dr_run.nx" 7import "nx_dr_verify.nx" 8import "nx_dr_drbench.nx" 9import "nx_gate_verdict.nx" 10 11func main() -> i64 { 12 let ctr: *i64 = gv_ctr() 13 gv_head("nx_dr_run -- sovereign real-text matching / judge stage (DR-0 rung-2)") 14 15 // tokenize the document once 16 let doc: *i64 = sys_mmap(64 * 8) as *i64 17 let ds: *u8 = "the cat sat on a mat" as *u8 18 let nd: i64 = drr_tokenize(ds, drr_strlen(ds), doc, 64) 19 20 // T1 tokenizer count: 6 words 21 var ok1: i64 = 0 22 if nd == 6 { ok1 = 1 } 23 gv_check("T1 tokenize count = 6", ok1, ctr) 24 25 // T2 case-insensitive: "Cat" and "cat" hash to the same id 26 let ca: *i64 = sys_mmap(8) as *i64 27 let cb: *i64 = sys_mmap(8) as *i64 28 let sa: *u8 = "Cat" as *u8 29 let sb: *u8 = "cat" as *u8 30 drr_tokenize(sa, drr_strlen(sa), ca, 1) 31 drr_tokenize(sb, drr_strlen(sb), cb, 1) 32 var ok2: i64 = 0 33 if ca[0] == cb[0] { ok2 = 1 } 34 gv_check("T2 tokenizer case-insensitive", ok2, ctr) 35 36 // T3 full containment: insight "cat sat" fully in doc -> 1000 37 let i3: *i64 = sys_mmap(8 * 8) as *i64 38 let s3: *u8 = "cat sat" as *u8 39 let n3: i64 = drr_tokenize(s3, drr_strlen(s3), i3, 8) 40 var ok3: i64 = 0 41 if dv_entail(i3, n3, doc, nd) == 1000 { ok3 = 1 } 42 gv_check("T3 full containment = 1000", ok3, ctr) 43 44 // T4 partial containment: "cat dog" -> cat in doc, dog not -> 500 45 let i4: *i64 = sys_mmap(8 * 8) as *i64 46 let s4: *u8 = "cat dog" as *u8 47 let n4: i64 = drr_tokenize(s4, drr_strlen(s4), i4, 8) 48 var ok4: i64 = 0 49 if dv_entail(i4, n4, doc, nd) == 500 { ok4 = 1 } 50 gv_check("T4 partial containment = 500", ok4, ctr) 51 52 // T5 absent containment: "zebra fish" -> 0 53 let i5: *i64 = sys_mmap(8 * 8) as *i64 54 let s5: *u8 = "zebra fish" as *u8 55 let n5: i64 = drr_tokenize(s5, drr_strlen(s5), i5, 8) 56 var ok5: i64 = 0 57 if dv_entail(i5, n5, doc, nd) == 0 { ok5 = 1 } 58 gv_check("T5 absent containment = 0", ok5, ctr) 59 60 // T6 coverage at threshold 600: "cat sat"(1000) covered, "cat dog"(500) not 61 var ok6: i64 = 0 62 if drr_covered(i3, n3, doc, nd, 600) == 1 { if drr_covered(i4, n4, doc, nd, 600) == 0 { ok6 = 1 } } 63 gv_check("T6 coverage at threshold 600", ok6, ctr) 64 65 // T7 insight recall: [covered, not, not] over 3 insights -> 333 66 let cov: *i64 = sys_mmap(3 * 8) as *i64 67 cov[0] = drr_covered(i3, n3, doc, nd, 600) 68 cov[1] = drr_covered(i4, n4, doc, nd, 600) 69 cov[2] = drr_covered(i5, n5, doc, nd, 600) 70 var ok7: i64 = 0 71 if dr_frac(cov, 3) == 333 { ok7 = 1 } 72 gv_check("T7 insight recall 1of3 = 333", ok7, ctr) 73 74 // T8 NEG-CONTROL: an unsupported insight is never covered (even at threshold 1) and a 75 // single-unsupported-insight recall is 0 (cannot be inflated). 76 let cov0: *i64 = sys_mmap(8) as *i64 77 cov0[0] = drr_covered(i5, n5, doc, nd, 1) 78 var ok8: i64 = 0 79 if cov0[0] == 0 { if dr_frac(cov0, 1) == 0 { ok8 = 1 } } 80 gv_check("T8 neg-control unsupported insight never covered", ok8, ctr) 81 82 // T9 determinism: tokenizing "cat sat" twice yields identical ids 83 let d2: *i64 = sys_mmap(8 * 8) as *i64 84 let m2: i64 = drr_tokenize(s3, drr_strlen(s3), d2, 8) 85 var ok9: i64 = 0 86 if m2 == n3 { if d2[0] == i3[0] { if d2[1] == i3[1] { ok9 = 1 } } } 87 gv_check("T9 tokenizer deterministic", ok9, ctr) 88 89 let rc: i64 = gv_verdict("DR-RUN", ctr, "tokenize + containment + coverage + recall on real text, neg-control") 90 sys_exit(rc) 91 return rc 92}