nx_dr_refute_gate.nx source
↩ module page · 65 lines · 2896 B
1// nx_dr_refute_gate.nx -- KAT + neg-control for the adversarial refutation aggregator (DR-2).
2// Proves vote tally, the S1 decorrelation function m_eff=m/(1+(m-1)rho), and the kill rule --
3// including the CENTRAL neg-control: the SAME 4 refutes KILL a claim when the verifiers are
4// INDEPENDENT but CANNOT when they are correlated (correlated retries buy almost nothing), and
5// an UNREFUTED claim is never killed. DRY nx_gate_verdict lib (D001 migrate-on-touch).
6import "nx_dr_refute.nx"
7import "nx_gate_verdict.nx"
8
9func main() -> i64 {
10 let ctr: *i64 = gv_ctr()
11 gv_head("nx_dr_refute -- sovereign adversarial refutation aggregator (DR-2)")
12
13 // T1 effective_n independent: m=5 rho=0 -> 5000 permille (5 effective)
14 var ok1: i64 = 0
15 if rf_effective_n(5, 0) == 5000 { ok1 = 1 }
16 gv_check("T1 effective_n independent m=5 = 5000", ok1, ctr)
17
18 // T2 effective_n fully-correlated: m=5 rho=1000 -> 1000 permille (1 effective)
19 var ok2: i64 = 0
20 if rf_effective_n(5, 1000) == 1000 { ok2 = 1 }
21 gv_check("T2 effective_n correlated m=5 = 1000", ok2, ctr)
22
23 // T3 effective_n partial: m=3 rho=500 -> 1500 permille (1.5 effective)
24 var ok3: i64 = 0
25 if rf_effective_n(3, 500) == 1500 { ok3 = 1 }
26 gv_check("T3 effective_n partial m=3 rho=500 = 1500", ok3, ctr)
27
28 // T4 tally: votes [-1,-1,1,0,-1] -> R=3 S=1 A=1
29 let vt: *i64 = sys_mmap(5 * 8) as *i64
30 vt[0]=0-1; vt[1]=0-1; vt[2]=1; vt[3]=0; vt[4]=0-1
31 let out: *i64 = sys_mmap(3 * 8) as *i64
32 rf_tally(vt, 5, out)
33 var ok4: i64 = 0
34 if out[0] == 3 { if out[1] == 1 { if out[2] == 1 { ok4 = 1 } } }
35 gv_check("T4 tally R3 S1 A1", ok4, ctr)
36
37 // T5 INDEPENDENT majority kills: R=4 S=1 m=5 rho=0 bar=2000 -> KILL
38 var ok5: i64 = 0
39 if rf_kill(4, 1, 5, 0, 2000) == 1 { ok5 = 1 }
40 gv_check("T5 independent majority kills", ok5, ctr)
41
42 // T6 CORRELATED cannot kill: SAME R=4 S=1 m=5 but rho=1000 -> SURVIVES (S1)
43 var ok6: i64 = 0
44 if rf_kill(4, 1, 5, 1000, 2000) == 0 { ok6 = 1 }
45 gv_check("T6 correlated refutes cannot kill (S1)", ok6, ctr)
46
47 // T7 decorrelation is DECISIVE: identical votes, kill flips on rho alone
48 var ok7: i64 = 0
49 if rf_kill(4, 1, 5, 0, 2000) == 1 { if rf_kill(4, 1, 5, 1000, 2000) == 0 { ok7 = 1 } }
50 gv_check("T7 decorrelation decides identical votes", ok7, ctr)
51
52 // T8 support-majority survives: R=1 S=4 -> not killed
53 var ok8: i64 = 0
54 if rf_kill(1, 4, 5, 0, 2000) == 0 { ok8 = 1 }
55 gv_check("T8 support-majority survives", ok8, ctr)
56
57 // T9 NEG-CONTROL: an UNREFUTED claim (R=0) is never killed (no false refutation)
58 var ok9: i64 = 0
59 if rf_kill(0, 0, 5, 0, 1) == 0 { ok9 = 1 }
60 gv_check("T9 neg-control unrefuted claim never killed", ok9, ctr)
61
62 let rc: i64 = gv_verdict("DR-REFUTE", ctr, "tally + decorrelated effective-N + kill-on-majority, S1 neg-control")
63 sys_exit(rc)
64 return rc
65}