nx_dr_verify_gate.nx source
↩ module page · 89 lines · 3797 B
1// nx_dr_verify_gate.nx -- KAT + neg-control for the citation-entailment verifier (DR-3).
2// Proves token-containment entailment (full/partial/unsupported), threshold support,
3// the batch drop-on-fail loop, the belief-revision rate, and the NEG-CONTROL that
4// encodes the structural fix for the 68%-evidence-ignored failure: an unsupported claim
5// (entail 0) is dropped at the LOOSEST threshold -> it can never enter context memory.
6// DRY nx_gate_verdict lib (D001 migrate-on-touch).
7import "nx_dr_verify.nx"
8import "nx_gate_verdict.nx"
9
10func main() -> i64 {
11 let ctr: *i64 = gv_ctr()
12 gv_head("nx_dr_verify -- sovereign citation-entailment verification loop (DR-3)")
13
14 let ev: *i64 = sys_mmap(5 * 8) as *i64
15 ev[0]=1; ev[1]=2; ev[2]=3; ev[3]=4; ev[4]=5
16
17 // T1 full entailment: all claim tokens present -> 1000
18 let c1: *i64 = sys_mmap(3 * 8) as *i64
19 c1[0]=1; c1[1]=2; c1[2]=3
20 var ok1: i64 = 0
21 if dv_entail(c1, 3, ev, 5) == 1000 { ok1 = 1 }
22 gv_check("T1 full entailment = 1000", ok1, ctr)
23
24 // T2 partial entailment: 2 of 3 tokens present -> 666
25 let ev2: *i64 = sys_mmap(3 * 8) as *i64
26 ev2[0]=1; ev2[1]=2; ev2[2]=3
27 let c2: *i64 = sys_mmap(3 * 8) as *i64
28 c2[0]=1; c2[1]=2; c2[2]=9
29 var ok2: i64 = 0
30 if dv_entail(c2, 3, ev2, 3) == 666 { ok2 = 1 }
31 gv_check("T2 partial entailment 2of3 = 666", ok2, ctr)
32
33 // T3 UNSUPPORTED: no claim token in evidence -> 0 (the 68% case)
34 let c3: *i64 = sys_mmap(2 * 8) as *i64
35 c3[0]=7; c3[1]=8
36 var ok3: i64 = 0
37 if dv_entail(c3, 2, ev2, 3) == 0 { ok3 = 1 }
38 gv_check("T3 unsupported claim entail = 0", ok3, ctr)
39
40 // T4 supported at threshold: entail 666 >= 500 -> 1
41 var ok4: i64 = 0
42 if dv_supported(c2, 3, ev2, 3, 500) == 1 { ok4 = 1 }
43 gv_check("T4 supported when entail >= threshold", ok4, ctr)
44
45 // T5 NEG-CONTROL structural forcing: an unsupported claim is dropped at the LOOSEST
46 // threshold (1) -> cannot enter context memory unsupported.
47 var ok5: i64 = 0
48 if dv_supported(c3, 2, ev2, 3, 1) == 0 { ok5 = 1 }
49 gv_check("T5 neg-control unsupported dropped at threshold 1", ok5, ctr)
50
51 // T6 batch drop-on-fail: [1000,666,0,800,300] threshold 500 -> keep 3 drop 2
52 let sc: *i64 = sys_mmap(5 * 8) as *i64
53 sc[0]=1000; sc[1]=666; sc[2]=0; sc[3]=800; sc[4]=300
54 let keep: *i64 = sys_mmap(5 * 8) as *i64
55 let dropped: *i64 = sys_mmap(8) as *i64
56 let nk: i64 = dv_batch(sc, 5, 500, keep, dropped)
57 var ok6: i64 = 0
58 if nk == 3 { if dropped[0] == 2 { ok6 = 1 } }
59 gv_check("T6 batch keeps 3 drops 2", ok6, ctr)
60
61 // T7 belief-revision rate = 2 of 5 = 400
62 var ok7: i64 = 0
63 if dv_revision_rate(dropped[0], 5) == 400 { ok7 = 1 }
64 gv_check("T7 belief-revision rate 2of5 = 400", ok7, ctr)
65
66 // T8 all-unsupported batch -> 0 survivors, revision 1000 (nothing enters memory)
67 let sc0: *i64 = sys_mmap(3 * 8) as *i64
68 sc0[0]=0; sc0[1]=0; sc0[2]=0
69 let keep0: *i64 = sys_mmap(3 * 8) as *i64
70 let dropped0: *i64 = sys_mmap(8) as *i64
71 let nk0: i64 = dv_batch(sc0, 3, 500, keep0, dropped0)
72 var ok8: i64 = 0
73 if nk0 == 0 { if dv_revision_rate(dropped0[0], 3) == 1000 { ok8 = 1 } }
74 gv_check("T8 all-unsupported keeps 0 revision 1000", ok8, ctr)
75
76 // T9 threshold boundary is inclusive: score == threshold -> supported
77 let scb: *i64 = sys_mmap(1 * 8) as *i64
78 scb[0]=500
79 let keepb: *i64 = sys_mmap(1 * 8) as *i64
80 let droppedb: *i64 = sys_mmap(8) as *i64
81 let nkb: i64 = dv_batch(scb, 1, 500, keepb, droppedb)
82 var ok9: i64 = 0
83 if nkb == 1 { ok9 = 1 }
84 gv_check("T9 threshold boundary inclusive", ok9, ctr)
85
86 let rc: i64 = gv_verdict("DR-VERIFY", ctr, "entailment+drop-on-fail+belief-revision+structural-forcing neg-control")
87 sys_exit(rc)
88 return rc
89}