nx_dr_route_gate.nx source
↩ module page · 65 lines · 2954 B
1// nx_dr_route_gate.nx -- KAT + neg-control for the web-vs-private router (DR-7).
2// Proves coverage, all four route outcomes, the uses_web/uses_private predicates, boundary
3// inclusivity, and the CENTRAL neg-control encoding DRBench's dominant failure fix: a query
4// whose private coverage is BELOW threshold is NEVER routed private-only -- it always
5// involves the web (WEB_ONLY or ESCALATE_WEB), so the agent can never dead-end. DRY verdict lib.
6import "nx_dr_route.nx"
7import "nx_gate_verdict.nx"
8
9func main() -> i64 {
10 let ctr: *i64 = gv_ctr()
11 gv_head("nx_dr_route -- sovereign web-vs-private source router (DR-7)")
12
13 // T1 coverage 3 of 5 = 600
14 var ok1: i64 = 0
15 if rt_coverage(3, 5) == 600 { ok1 = 1 }
16 gv_check("T1 coverage 3of5 = 600", ok1, ctr)
17
18 // T2 BOTH: private and web both sufficient
19 var ok2: i64 = 0
20 if rt_route(800, 700, 500, 500) == 2 { ok2 = 1 }
21 gv_check("T2 route BOTH when both sufficient", ok2, ctr)
22
23 // T3 PRIVATE_ONLY: private sufficient, web not needed
24 var ok3: i64 = 0
25 if rt_route(800, 200, 500, 500) == 0 { ok3 = 1 }
26 gv_check("T3 route PRIVATE_ONLY", ok3, ctr)
27
28 // T4 WEB_ONLY: private insufficient, web sufficient (the DRBench fix)
29 var ok4: i64 = 0
30 if rt_route(200, 800, 500, 500) == 1 { ok4 = 1 }
31 gv_check("T4 route WEB_ONLY when private insufficient", ok4, ctr)
32
33 // T5 ESCALATE_WEB: neither sufficient -> still search web, never dead-end
34 var ok5: i64 = 0
35 if rt_route(100, 100, 500, 500) == 3 { ok5 = 1 }
36 gv_check("T5 route ESCALATE_WEB not dead-end", ok5, ctr)
37
38 // T6 uses_web predicate
39 var ok6: i64 = 0
40 if rt_uses_web(0) == 0 { if rt_uses_web(1) == 1 { if rt_uses_web(2) == 1 { if rt_uses_web(3) == 1 { ok6 = 1 } } } }
41 gv_check("T6 uses_web only PRIVATE_ONLY is 0", ok6, ctr)
42
43 // T7 uses_private predicate
44 var ok7: i64 = 0
45 if rt_uses_private(0) == 1 { if rt_uses_private(2) == 1 { if rt_uses_private(1) == 0 { if rt_uses_private(3) == 0 { ok7 = 1 } } } }
46 gv_check("T7 uses_private only PRIVATE_ONLY and BOTH", ok7, ctr)
47
48 // T8 boundary inclusive: priv_cov == threshold is PRIVATE-sufficient
49 var ok8: i64 = 0
50 if rt_route(500, 200, 500, 500) == 0 { ok8 = 1 }
51 gv_check("T8 threshold boundary inclusive", ok8, ctr)
52
53 // T9 NEG-CONTROL (the dominant-failure fix): private BELOW threshold -> NEVER private-only,
54 // ALWAYS uses web (whether web is sufficient or not).
55 let r_websufficient: i64 = rt_route(100, 800, 500, 500)
56 let r_webalso_low: i64 = rt_route(100, 100, 500, 500)
57 var ok9: i64 = 0
58 if r_websufficient != 0 { if rt_uses_web(r_websufficient) == 1 {
59 if r_webalso_low != 0 { if rt_uses_web(r_webalso_low) == 1 { ok9 = 1 } } } }
60 gv_check("T9 neg-control private-insufficient never dead-ends", ok9, ctr)
61
62 let rc: i64 = gv_verdict("DR-ROUTE", ctr, "coverage + 4-way route + predicates + never-dead-end neg-control")
63 sys_exit(rc)
64 return rc
65}