code wiki / _hdl_build / nx_wirecensus_gate.nx
nx_wirecensus_gate.nx source
↩ module page · 117 lines · 5966 B
1// nx_wirecensus_gate.nx -- proves S4 (registered but never called) on synthetic fixtures where the
2// answer is known by construction, including the two traps that would make the verdict a lie.
3// license_tier: ORIGINAL No hw writes (Rule 26). expect_exit: 0
4import "nx_wirecensus_lib.nx"
5import "nx_gate.nx"
6
7func wg_num(v: i64) -> i64 {
8 let b: *u8 = sys_mmap(32)
9 if v == 0 { b[0] = 48 as u8; sys_write(1, b, 1); return 0 }
10 let t: *u8 = sys_mmap(32)
11 var n: i64 = 0
12 var x: i64 = v
13 while x > 0 { t[n] = ((x % 10) + 48) as u8; x = x / 10; n = n + 1 }
14 var o: i64 = 0
15 while n > 0 { n = n - 1; b[o] = t[n]; o = o + 1 }
16 sys_write(1, b, o)
17 return 0
18}
19func wg_len(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } return n }
20
21func main() -> i64 {
22 gw("=== nx_wirecensus_gate: S4 registered-but-never-called ===\n" as *u8)
23 var pass: i64 = 0
24 var tot: i64 = 0
25
26 let rn: *u8 = sys_mmap(WC_MAXT * WC_NAMEMAX)
27 let rl: *i64 = sys_mmap(WC_MAXT * 8) as *i64
28 let an: *u8 = sys_mmap(WC_MAXT * WC_NAMEMAX)
29 let al: *i64 = sys_mmap(WC_MAXT * 8) as *i64
30 let in2: *u8 = sys_mmap(WC_MAXT * WC_NAMEMAX)
31 let il: *i64 = sys_mmap(WC_MAXT * 8) as *i64
32 let tr: *i64 = sys_mmap(16) as *i64
33 let dk: *i64 = sys_mmap(WC_MAXT * 8) as *i64
34 tr[0] = 0
35
36 // registered: 4 tools. Includes a comment row and a blank line, which must be ignored.
37 let reg: *u8 = "# comment row\ntool_a\t/x/a.elf\tGREEN\ntool_b\t/x/b.elf\tGREEN\ntool_c\t/x/c.elf\tGREEN\ntool_d\t/x/d.elf\tGREEN\n" as *u8
38 let rc: i64 = wc_parse_registered(reg, wg_len(reg), rn, rl, tr)
39 tot = tot + 1
40 var t1: i64 = 0
41 if rc == 4 { t1 = 1 }
42 if t1 == 1 { pass = pass + 1; gw(" [PASS] " as *u8) } else { gw(" [FAIL] " as *u8) }
43 gw("T1 declared surface: 4 tools parsed from the allowlist, comment + blank rows ignored\n" as *u8)
44
45 // W1: tool_a and tool_b were authorised (a in a multi-name CSV, b alone).
46 let cap: *u8 = "CAPMINT epoch=1 allow=tool_a,tool_b exp=2 nonce=3 days=30 src=/api/cap/mint\nCAPMINT epoch=4 allow=tool_b exp=5 nonce=6 days=30 src=/api/cap/mint\n" as *u8
47 let ac: i64 = wc_parse_authorised(cap, wg_len(cap), an, al, tr)
48 tot = tot + 1
49 var t2: i64 = 0
50 if ac == 2 { t2 = 1 }
51 if t2 == 1 { pass = pass + 1; gw(" [PASS] " as *u8) } else { gw(" [FAIL] " as *u8) }
52 gw("T2 W1 authorised: allow= CSV split correctly, deduped across mints, stops at the space\n" as *u8)
53
54 // W2: tool_c was actually invoked (field 2 of the actlog row).
55 let act: *u8 = "1784\tws-intel\ttool_c\trun\tok\tsome note\n1785\tws-intel\ttool_c\trun\tok\tagain\n" as *u8
56 let ic: i64 = wc_parse_invoked(act, wg_len(act), in2, il, tr)
57 tot = tot + 1
58 var t3: i64 = 0
59 if ic == 1 { t3 = 1 }
60 if t3 == 1 { pass = pass + 1; gw(" [PASS] " as *u8) } else { gw(" [FAIL] " as *u8) }
61 gw("T3 W2 invoked: TAB field 2 extracted from the action journal, repeats deduped\n" as *u8)
62
63 // T4 THE VERDICT: only tool_d is dark (a authorised, b authorised, c invoked, d neither).
64 let d4: i64 = wc_dark(rn, rl, rc, an, al, ac, in2, il, ic, dk, WC_MAXT)
65 tot = tot + 1
66 var t4: i64 = 0
67 if d4 == 1 { if dk[0] == 3 { t4 = 1 } }
68 if t4 == 1 { pass = pass + 1; gw(" [PASS] " as *u8) } else { gw(" [FAIL] " as *u8) }
69 gw("T4 VERDICT: exactly tool_d is DARK -- registered, never authorised, never invoked\n" as *u8)
70
71 // T5 THE RESCUE TRAP: W2 must be able to SAVE a tool that W1 never saw. If the census condemned on
72 // W1 alone it would call tool_c dark, which is false -- the actlog proves it ran. Union, not W1 only.
73 let d5: i64 = wc_dark(rn, rl, rc, an, al, ac, in2, il, 0, dk, WC_MAXT)
74 tot = tot + 1
75 var t5: i64 = 0
76 if d5 == 2 { t5 = 1 }
77 if t5 == 1 { pass = pass + 1; gw(" [PASS] " as *u8) } else { gw(" [FAIL] " as *u8) }
78 gw("T5 RESCUE: dropping W2 wrongly darkens tool_c -- proving the invoked witness is load-bearing\n" as *u8)
79
80 // T6 NEG / NO-FALSE-DARK: when every registered tool is authorised, DARK is 0. A census that
81 // reported a nonzero count here would be unusable -- the first false positive gets it switched off.
82 let cap2: *u8 = "CAPMINT epoch=1 allow=tool_a,tool_b,tool_c,tool_d exp=2 nonce=3 days=30 src=/api/cap/mint\n" as *u8
83 let an2: *u8 = sys_mmap(WC_MAXT * WC_NAMEMAX)
84 let al2: *i64 = sys_mmap(WC_MAXT * 8) as *i64
85 let ac2: i64 = wc_parse_authorised(cap2, wg_len(cap2), an2, al2, tr)
86 let d6: i64 = wc_dark(rn, rl, rc, an2, al2, ac2, in2, il, ic, dk, WC_MAXT)
87 tot = tot + 1
88 var t6: i64 = 0
89 if ac2 == 4 { if d6 == 0 { t6 = 1 } }
90 if t6 == 1 { pass = pass + 1; gw(" [PASS] " as *u8) } else { gw(" [FAIL] " as *u8) }
91 gw("T6 NEG: all-authorised yields DARK=0 (no false positives, or the census gets disabled)\n" as *u8)
92
93 // T7 SUBSTRING TRAP: tool_a must NOT be rescued by an unrelated tool_abc appearing in a mint.
94 // Name matching is length-exact; a prefix match would silently bless every short-named tool.
95 let cap3: *u8 = "CAPMINT epoch=1 allow=tool_abc exp=2 nonce=3 days=30 src=/api/cap/mint\n" as *u8
96 let an3: *u8 = sys_mmap(WC_MAXT * WC_NAMEMAX)
97 let al3: *i64 = sys_mmap(WC_MAXT * 8) as *i64
98 let ac3: i64 = wc_parse_authorised(cap3, wg_len(cap3), an3, al3, tr)
99 let d7: i64 = wc_dark(rn, rl, rc, an3, al3, ac3, in2, il, 0, dk, WC_MAXT)
100 tot = tot + 1
101 var t7: i64 = 0
102 if d7 == 4 { t7 = 1 }
103 if t7 == 1 { pass = pass + 1; gw(" [PASS] " as *u8) } else { gw(" [FAIL] " as *u8) }
104 gw("T7 SUBSTRING NEG: tool_abc does NOT satisfy tool_a -- exact-length match, not prefix\n" as *u8)
105
106 gw("\n=== nx_wirecensus_gate " as *u8)
107 wg_num(pass)
108 gw("/" as *u8)
109 wg_num(tot)
110 gw(" ===\n" as *u8)
111 if pass == tot {
112 gw("WIRECENSUS GREEN -- S4 proven: dark only when BOTH witnesses are silent, no false positives\n" as *u8)
113 return 0
114 }
115 gw("WIRECENSUS RED\n" as *u8)
116 return 1
117}