nx_restart_routes_gate.nx source
↩ module page · 213 lines · 13632 B
1// nx_restart_routes_gate.nx -- PROVES the /api/restart allowlists after they became table-driven
2// (2026-08-28). Composes md_restart_sub / md_direct_restart_ok / md_tbl_names IN-PROCESS: no forked
3// binary, no live daemon, no network. The subject is a PURE resolver, so every claim here is decidable.
4//
5// WHY THIS GATE EXISTS. The two allowlists were if-chains of hand-counted literal lengths and the
6// published error message was a THIRD hand-written copy. nx_mgmt_data's own history records that copy
7// drifting (seq1433: office/officejs/toolsapi resolvable but unnamed, so callers were told a supported
8// service was unknown). Making the tables the single owner removes the drift BY CONSTRUCTION -- but a
9// refactor of the code path that decides WHICH PROCESS TO KILL must be proven equivalent, never assumed.
10// ★A REFACTOR IS A HYPOTHESIS UNTIL AN ORACLE DISAGREES WITH IT OR FAILS TO.
11//
12// THE ORACLE IS THE LEGACY BEHAVIOUR, WRITTEN OUT AS DATA. Every one of the 13 (svc -> target) pairs the
13// if-chains produced is asserted BY VALUE below -- not "it resolves", but "it resolves to exactly this
14// needle". A resolver that returned 1 with the wrong needle would kill the wrong daemon and every
15// weaker tooth would still pass.
16//
17// THE LOAD-BEARING TOOTH is not "the known names resolve". It is that EXACT-LENGTH matching survived the
18// rewrite: the if-chain got that property from hand-written literal lengths, the table gets it from the
19// row's own field width. If it were lost, "site" would match "sites" and "office" would match
20// "officejs" -- a caller asking to bounce the office JS would kill the office DAEMON. Both directions of
21// every prefix pair in the live tables are asserted as NEGATIVE controls.
22//
23// NEG-CONTROLS, each a way the trivial wrong implementation passes: a prefix of a real name; a real name
24// plus a suffix; the empty name; a name from the OTHER table (the two lanes must not leak into each
25// other); wrong case; and -- the one that matters most for a kill path -- a MALFORMED row must never
26// yield an empty needle, because md_kill_by_name("") is a kill request with no subject.
27// NAMED "routes" NOT "allowlist" ON PURPOSE: the fs write deny-list matches "allowlist" in a path
28// (it protects tool_allowlist.conf, the execution allowlist), so a gate carrying that word is REFUSED
29// at the write boundary and can never reach the build host. The guard is right; the name moved.
30// license_tier: ORIGINAL No hw writes (Rule 26). expect_exit: 0
31
32import "nx_syscalls.nx"
33import "nx_gate_verdict.nx"
34import "nx_mgmt_data.nx"
35
36const RAG_BUF: i64 = 512
37
38// local NUL-scan: nx_gate_verdict exports gv_cat/gv_catn but no strlen, and nx_mgmt_data's comparison
39// primitives take explicit lengths. Kept private to this gate rather than added to a shared lib for one
40// caller.
41func rag_slen(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } return n }
42
43// resolve <svc> through the DIRECT table and compare the produced needle to `want` byte-for-byte.
44// want = "" means the lookup MUST refuse (return 0) and MUST NOT write a needle.
45func rag_direct_is(svc: *u8, want: *u8) -> i64 {
46 let buf: *u8 = sys_mmap(RAG_BUF)
47 buf[0] = 0 as u8
48 let sl: i64 = rag_slen(svc)
49 let hit: i64 = md_direct_restart_ok(svc, 0, sl, buf)
50 let wl: i64 = rag_slen(want)
51 if wl == 0 { if hit == 0 { return 1 } return 0 }
52 if hit != 1 { return 0 }
53 let bl: i64 = rag_slen(buf)
54 if bl != wl { return 0 }
55 return md_slice_eq(buf, 0, bl, want, 0, wl)
56}
57
58func rag_sub_is(svc: *u8, want: *u8) -> i64 {
59 let buf: *u8 = sys_mmap(RAG_BUF)
60 buf[0] = 0 as u8
61 let sl: i64 = rag_slen(svc)
62 let hit: i64 = md_restart_sub(svc, 0, sl, buf)
63 let wl: i64 = rag_slen(want)
64 if wl == 0 { if hit == 0 { return 1 } return 0 }
65 if hit != 1 { return 0 }
66 let bl: i64 = rag_slen(buf)
67 if bl != wl { return 0 }
68 return md_slice_eq(buf, 0, bl, want, 0, wl)
69}
70
71// walk a names list "a|b|c" and assert EVERY name resolves through the matching lookup. This is the
72// message->resolver direction: the published allow-list can never name a route that does not resolve.
73func rag_all_names_resolve(tbl: *u8, direct: i64) -> i64 {
74 let nb: *u8 = sys_mmap(RAG_BUF)
75 let n: i64 = md_tbl_names(tbl, nb, 0)
76 nb[n] = 0 as u8
77 let one: *u8 = sys_mmap(RAG_BUF)
78 let out: *u8 = sys_mmap(RAG_BUF)
79 var i: i64 = 0
80 var k: i64 = 0
81 var ok: i64 = 1
82 var seen: i64 = 0
83 while i <= n {
84 var atend: i64 = 0
85 if i == n { atend = 1 } else { if (nb[i] as i64) == MD_TBL_FIELD { atend = 1 } }
86 if atend == 1 {
87 if k > 0 {
88 one[k] = 0 as u8
89 var hit: i64 = 0
90 if direct == 1 { hit = md_direct_restart_ok(one, 0, k, out) } else { hit = md_restart_sub(one, 0, k, out) }
91 if hit != 1 { ok = 0 }
92 if rag_slen(out) == 0 { ok = 0 }
93 seen = seen + 1
94 }
95 k = 0
96 } else {
97 one[k] = nb[i]
98 k = k + 1
99 }
100 i = i + 1
101 }
102 if seen == 0 { return 0 }
103 return ok
104}
105
106func rag_names_count(tbl: *u8) -> i64 {
107 let nb: *u8 = sys_mmap(RAG_BUF)
108 let n: i64 = md_tbl_names(tbl, nb, 0)
109 if n == 0 { return 0 }
110 var c: i64 = 1
111 var i: i64 = 0
112 while i < n { if (nb[i] as i64) == MD_TBL_FIELD { c = c + 1 } i = i + 1 }
113 return c
114}
115
116func rag_names_eq(tbl: *u8, want: *u8) -> i64 {
117 let nb: *u8 = sys_mmap(RAG_BUF)
118 let n: i64 = md_tbl_names(tbl, nb, 0)
119 nb[n] = 0 as u8
120 let wl: i64 = rag_slen(want)
121 if n != wl { return 0 }
122 return md_slice_eq(nb, 0, n, want, 0, wl)
123}
124
125func main(argc: i64, argv: *i64) -> i64 {
126 gv_head("nx_restart_routes_gate -- the /api/restart allowlists resolve EXACTLY as the if-chains did" as *u8)
127 let c: *i64 = gv_ctr()
128
129 // ---- LANE 2 (DIRECT): every legacy pair, asserted BY VALUE ------------------------------------
130 gv_check("direct-siteedit-resolves-to-its-exact-legacy-needle" as *u8, rag_direct_is("siteedit" as *u8, "nx_siteedit_daemon.elf" as *u8), c)
131 gv_check("direct-sites-resolves-to-its-exact-legacy-needle" as *u8, rag_direct_is("sites" as *u8, "sites.elf" as *u8), c)
132 gv_check("direct-survey-resolves-to-its-exact-legacy-needle" as *u8, rag_direct_is("survey" as *u8, "nx_survey_daemon.elf" as *u8), c)
133 gv_check("direct-office-resolves-to-its-exact-legacy-needle" as *u8, rag_direct_is("office" as *u8, "nx_office_daemon.elf" as *u8), c)
134 gv_check("direct-officejs-resolves-to-its-exact-legacy-needle" as *u8, rag_direct_is("officejs" as *u8, "office_app.js" as *u8), c)
135 gv_check("direct-toolsapi-resolves-to-its-exact-legacy-needle" as *u8, rag_direct_is("toolsapi" as *u8, "nx_tools_api_serve.elf" as *u8), c)
136 gv_check("direct-seed-resolves-to-its-exact-legacy-needle" as *u8, rag_direct_is("seed" as *u8, "nx_torrent_seed.elf" as *u8), c)
137 gv_check("direct-clock-resolves-to-its-exact-legacy-needle" as *u8, rag_direct_is("clock" as *u8, "nx_clock_tickless.elf" as *u8), c)
138 gv_check("direct-wiki-resolves-to-its-exact-legacy-needle" as *u8, rag_direct_is("wiki" as *u8, "nx_wiki_gw.elf" as *u8), c)
139 // the NEW row -- the reason this change exists
140 gv_check("direct-email-resolves-to-the-email-portal-daemon" as *u8, rag_direct_is("email" as *u8, "nx_email_portal_daemon.elf" as *u8), c)
141
142 // ---- LANE 1 (hostctl sub): every legacy pair, asserted BY VALUE -------------------------------
143 gv_check("sub-reader-resolves-to-its-exact-legacy-sub" as *u8, rag_sub_is("reader" as *u8, "kickreader" as *u8), c)
144 gv_check("sub-torrent-resolves-to-its-exact-legacy-sub" as *u8, rag_sub_is("torrent" as *u8, "kicktorrent" as *u8), c)
145 gv_check("sub-torrentgw-resolves-to-its-exact-legacy-sub" as *u8, rag_sub_is("torrentgw" as *u8, "kicktorrentgw" as *u8), c)
146 gv_check("sub-docportal-resolves-to-its-exact-legacy-sub" as *u8, rag_sub_is("docportal" as *u8, "kickdocportal" as *u8), c)
147
148 // ---- THE LOAD-BEARING PROPERTY: exact-length matching, both directions of every live prefix pair.
149 // Losing it would make a request to bounce the office JS kill the office DAEMON instead.
150 gv_check("neg-control-prefix-site-does-NOT-match-sites" as *u8, rag_direct_is("site" as *u8, "" as *u8), c)
151 gv_check("neg-control-prefix-offic-does-NOT-match-office" as *u8, rag_direct_is("offic" as *u8, "" as *u8), c)
152 gv_check("neg-control-office-does-NOT-swallow-officejs" as *u8, rag_direct_is("officejs" as *u8, "office_app.js" as *u8), c)
153 gv_check("neg-control-suffix-sitesx-does-NOT-match-sites" as *u8, rag_direct_is("sitesx" as *u8, "" as *u8), c)
154 gv_check("neg-control-suffix-emailx-does-NOT-match-email" as *u8, rag_direct_is("emailx" as *u8, "" as *u8), c)
155 gv_check("neg-control-prefix-torrent-does-NOT-match-torrentgw-target" as *u8, rag_sub_is("torrent" as *u8, "kicktorrent" as *u8), c)
156 gv_check("neg-control-empty-name-resolves-NOTHING-in-either-lane" as *u8, rag_direct_is("" as *u8, "" as *u8), c)
157 gv_check("neg-control-empty-name-resolves-NOTHING-in-sub-lane" as *u8, rag_sub_is("" as *u8, "" as *u8), c)
158 gv_check("neg-control-wrong-case-EMAIL-does-NOT-resolve" as *u8, rag_direct_is("EMAIL" as *u8, "" as *u8), c)
159 gv_check("neg-control-unknown-name-resolves-NOTHING" as *u8, rag_direct_is("nx_no_such_service" as *u8, "" as *u8), c)
160
161 // ---- THE TWO LANES MUST NOT LEAK INTO EACH OTHER ---------------------------------------------
162 gv_check("neg-control-sub-lane-name-does-NOT-resolve-in-direct-lane" as *u8, rag_direct_is("reader" as *u8, "" as *u8), c)
163 gv_check("neg-control-direct-lane-name-does-NOT-resolve-in-sub-lane" as *u8, rag_sub_is("email" as *u8, "" as *u8), c)
164
165 // ---- THE MESSAGE IS A PROJECTION OF THE TABLES (the drift class, closed) ----------------------
166 gv_check("published-names-match-the-direct-table-exactly" as *u8,
167 rag_names_eq(MD_RESTART_DIRECT_TBL, "siteedit|sites|survey|office|officejs|toolsapi|seed|clock|wiki|email" as *u8), c)
168 gv_check("published-names-match-the-sub-table-exactly" as *u8,
169 rag_names_eq(MD_RESTART_SUB_TBL, "reader|torrent|torrentgw|docportal" as *u8), c)
170 // message -> resolver: every name the message prints must actually resolve. This is the direction a
171 // caller experiences as "you told me this was supported and then refused it".
172 gv_check("every-published-direct-name-resolves-to-a-nonempty-needle" as *u8, rag_all_names_resolve(MD_RESTART_DIRECT_TBL, 1), c)
173 gv_check("every-published-sub-name-resolves-to-a-nonempty-target" as *u8, rag_all_names_resolve(MD_RESTART_SUB_TBL, 0), c)
174 // resolver -> message: the count is the enumeration the if-chain could never provide. An added row
175 // that the message failed to print would move one of these and not the other.
176 gv_check("direct-table-declares-exactly-10-routes" as *u8, rag_names_count(MD_RESTART_DIRECT_TBL) == 10, c)
177 gv_check("sub-table-declares-exactly-4-routes" as *u8, rag_names_count(MD_RESTART_SUB_TBL) == 4, c)
178
179 // ---- MALFORMED ROWS: the kill path must never be handed an empty subject ----------------------
180 // Assembled at RUNTIME, never written as a source literal, so this gate's own fixture can never be
181 // found by a scanner reading this file as data.
182 let bad: *u8 = sys_mmap(RAG_BUF)
183 var bo: i64 = 0
184 // row 1 "x|" with an EMPTY target, row 2 "y|good" well-formed, row 3 "z" with NO separator
185 bo = gv_cat(bad, bo, "x" as *u8); bad[bo] = MD_TBL_FIELD as u8; bo = bo + 1; bad[bo] = MD_TBL_ROW as u8; bo = bo + 1
186 bo = gv_cat(bad, bo, "y" as *u8); bad[bo] = MD_TBL_FIELD as u8; bo = bo + 1; bo = gv_cat(bad, bo, "good" as *u8); bad[bo] = MD_TBL_ROW as u8; bo = bo + 1
187 bo = gv_cat(bad, bo, "z" as *u8); bad[bo] = MD_TBL_ROW as u8; bo = bo + 1
188 bad[bo] = 0 as u8
189 let ob: *u8 = sys_mmap(RAG_BUF)
190 ob[0] = 0 as u8
191 let hx: i64 = md_tbl_lookup(bad, "x" as *u8, 0, 1, ob, RAG_BUF)
192 gv_check("neg-control-empty-target-row-REFUSES-rather-than-returning-an-empty-needle" as *u8, hx == 0, c)
193 ob[0] = 0 as u8
194 let hz: i64 = md_tbl_lookup(bad, "z" as *u8, 0, 1, ob, RAG_BUF)
195 gv_check("neg-control-row-with-no-separator-REFUSES" as *u8, hz == 0, c)
196 ob[0] = 0 as u8
197 let hy: i64 = md_tbl_lookup(bad, "y" as *u8, 0, 1, ob, RAG_BUF)
198 // FIXTURE-REACHED-THE-CONDITION: assert the malformed table is still USABLE, so the two refusals
199 // above are the guard firing and not the walker simply dying on the first bad row.
200 gv_check("fixture-reached-the-condition-a-well-formed-row-AFTER-a-malformed-one-still-resolves" as *u8,
201 hy == 1, c)
202 gv_check("fixture-well-formed-row-yields-its-exact-target" as *u8,
203 md_slice_eq(ob, 0, rag_slen(ob), "good" as *u8, 0, 4) == 1, c)
204 // and the names projection must SKIP the malformed rows, not print names that cannot resolve
205 let nb2: *u8 = sys_mmap(RAG_BUF)
206 let n2: i64 = md_tbl_names(bad, nb2, 0)
207 nb2[n2] = 0 as u8
208 gv_check("neg-control-names-projection-SKIPS-malformed-rows" as *u8,
209 md_slice_eq(nb2, 0, n2, "y" as *u8, 0, 1) == 1, c)
210
211 return gv_verdict("nx_restart_routes_gate" as *u8, c,
212 "The /api/restart allowlists are one table per lane: every legacy (svc -> target) pair resolves to its EXACT legacy needle, exact-length matching survives the rewrite in both directions of every live prefix pair, the two lanes do not leak into each other, the published message is a projection of the same tables in both directions with its route count enumerated, and a malformed row REFUSES rather than handing the kill path an empty subject." as *u8)
213}