nx_undopath_lib.nx source
↩ module page · 397 lines · 19691 B
1// nx_undopath_lib.nx -- DOES EACH DEPLOY TARGET'S REVERSE GEAR REVERSE ITS OWN SUBJECT?
2//
3// THE QUESTION NOTHING ELSE ASKED. nx_deploycover_gate asks whether the deploy plane COVERS the fleet
4// (is there a row at all); nx_deploy_listen_gate asks whether the post-deploy check verified the INCOMING
5// listener. Neither asks the third question in that family: when the row's reverse gear FIRES, does it
6// reverse THIS target -- or somebody else's?
7//
8// MEASURED 2026-09-03, and this is why the lib exists: 16 of 31 rows in deploy_targets.conf declared
9// `rollback` in field 5, and nx_hostctl.cmd_rollback() TAKES NO TARGET ARGUMENT -- it unconditionally
10// renames sites.elf.prev over sites.elf and kills sites.elf. So the declared reverse gear of 16 daemons
11// reverted THE PUBLIC FRONT DOOR and left the bad daemon live. And /api/deploy's health watchdog invokes
12// field 5, so that wrong-subject destruction was AUTOMATIC, not merely a manual footgun.
13// ★THE ESTATE HAD ALREADY DIAGNOSED THIS TWICE BY HAND -- docportal corrected 2026-09-02, comparegw
14// dodging it with a deliberately unknown verb -- with the sentence "every gdeploy row above carries that
15// word" sitting in the same file. A DEFECT NAMED IN A COMMENT BESIDE THE ROWS THAT STILL HAVE IT IS NOT
16// DOCUMENTED, IT IS ADVERTISED. When a comment says "every row above has this", that sentence IS the
17// census and it belongs in an exit code.
18//
19// FOUR STATES, and the fourth is the one that keeps this honest:
20// UP_OWN -- the gear provably acts on this row's own subject.
21// UP_WRONG -- the gear provably acts on a DIFFERENT subject. The finding.
22// UP_FAILSAFE -- the verb is not implemented at all, so the sub is a proven no-op
23// (nx_hostctl's dispatcher tail: hc_puts("unknown subcommand"); sys_exit(2)).
24// comparegw chose this DELIBERATELY, and it is strictly safer than a wrong subject.
25// UP_UNPROVEN -- a verb exists but its subject could not be resolved from source. ABSTAIN, NEVER ACQUIT:
26// an unreadable reverse gear must not read as a correct one.
27//
28// The decision is PURE over already-resolved booleans so a gate can drive every branch without a host,
29// and so /api/deploy can one day REFUSE a wrong-subject rollback at the door using the SAME ruler that
30// censuses it -- one ruler, never two.
31// license_tier: ORIGINAL Read-only. No hw writes (Rule 26). lib (no main)
32import "nx_syscalls.nx"
33
34const UP_OWN: i64 = 0
35const UP_WRONG: i64 = 1
36const UP_FAILSAFE: i64 = 2
37const UP_UNPROVEN: i64 = 3
38
39// the hardcoded edge gear and the generic per-row gear, named so no caller retypes them
40const UP_EDGE_GEAR: *u8 = "rollback"
41const UP_PERROW_PFX: *u8 = "gdeployrb@"
42// the verb the per-row gear DISPATCHES TO. Named here so no caller retypes it, and so the existence
43// check below asks about the function that will actually run rather than about the row's spelling.
44const UP_PERROW_VERB: *u8 = "gdeploy_rollback"
45const UP_PERROW_PFXLEN: i64 = 10
46const UP_EDGE_ROW: *u8 = "sites"
47const UP_FUNC_PFX: *u8 = "func cmd_"
48const UP_FUNC_HEAD: *u8 = "\nfunc "
49const UP_CONST_PFX: *u8 = "const "
50// a `}` at column 0 -- in this dialect that closes exactly one top-level function, so it is the function's
51// OWN boundary and cannot absorb the comment block documenting whatever comes next.
52const UP_FUNC_CLOSE: *u8 = "\n}"
53
54func up_state_name(s: i64) -> *u8 {
55 if s == UP_OWN { return "OWN-SUBJECT" as *u8 }
56 if s == UP_WRONG { return "WRONG-SUBJECT" as *u8 }
57 if s == UP_FAILSAFE { return "FAILSAFE-UNKNOWN-VERB" as *u8 }
58 return "UNPROVEN" as *u8
59}
60
61func up_len(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } return n }
62
63func up_streq(a: *u8, b: *u8) -> i64 {
64 var i: i64 = 0
65 while a[i] != (0 as u8) { if a[i] != b[i] { return 0 } i = i + 1 }
66 if b[i] != (0 as u8) { return 0 }
67 return 1
68}
69
70func up_prefix(s: *u8, p: *u8) -> i64 {
71 var i: i64 = 0
72 while p[i] != (0 as u8) { if s[i] != p[i] { return 0 } i = i + 1 }
73 return 1
74}
75
76// substring search over a COUNTED buffer (the source is not NUL-terminated), returns index or -1
77func up_find(hay: *u8, hn: i64, needle: *u8) -> i64 {
78 let m: i64 = up_len(needle)
79 if m == 0 { return 0 - 1 }
80 if m > hn { return 0 - 1 }
81 var i: i64 = 0
82 let last: i64 = hn - m
83 while i <= last {
84 var j: i64 = 0
85 var ok: i64 = 1
86 while j < m {
87 if hay[i + j] != needle[j] { ok = 0; j = m } else { j = j + 1 }
88 }
89 if ok == 1 { return i }
90 i = i + 1
91 }
92 return 0 - 1
93}
94
95// the last path segment of a live path -- the artifact name a reverse gear must mention to be about it
96func up_basename(path: *u8, out: *u8, cap: i64) -> i64 {
97 let n: i64 = up_len(path)
98 var s: i64 = 0
99 var i: i64 = 0
100 while i < n { if (path[i] as i64) == 47 { s = i + 1 } i = i + 1 }
101 var o: i64 = 0
102 while s + o < n { if o + 1 >= cap { return o } out[o] = path[s + o]; o = o + 1 }
103 out[o] = 0 as u8
104 return o
105}
106
107// Body span of `func cmd_<verb>(` up to its OWN CLOSING BRACE -- a `}` at column 0, which in this dialect
108// closes exactly one top-level function (nested blocks are indented).
109//
110// ⚠IT USED TO END AT THE NEXT `\nfunc `, AND THAT WAS A REAL DEFECT MEASURED 2026-09-03 ON THE LIVE CENSUS:
111// the region between one function's closing brace and the next function's `func` keyword is THE NEXT
112// FUNCTION'S COMMENT BLOCK. cmd_loginrollback is followed by the hub-deploy header comment, which names
113// HC_HUB_GW -- so the const hop resolved nx_hub_gw.elf, set body_other, and the row landed UNPROVEN by
114// ambiguity. The verb was innocent and correct the whole time.
115// ★A SPAN THAT ENDS WHERE THE NEXT THING BEGINS INCLUDES THAT THING'S DOCUMENTATION, AND PROSE IS SOURCE
116// BYTES: THE MATCHER THEN RESOLVES A NEIGHBOUR'S SUBJECT AS THIS ONE'S. The estate already banked "a
117// scanner that does not skip comments measures the documentation, not the code" -- this is that law one
118// layer up, in a span boundary rather than a token filter, which is why reading the rule did not stop me.
119// A closing brace is the function's own boundary, so it cannot absorb anything that is not the function.
120func up_verb_body(src: *u8, n: i64, verb: *u8, box: *i64) -> i64 {
121 let pat: *u8 = sys_mmap(256)
122 var o: i64 = 0
123 var i: i64 = 0
124 while UP_FUNC_PFX[i] != (0 as u8) { pat[o] = UP_FUNC_PFX[i]; o = o + 1; i = i + 1 }
125 i = 0
126 while verb[i] != (0 as u8) { pat[o] = verb[i]; o = o + 1; i = i + 1 }
127 pat[o] = 40 as u8
128 o = o + 1
129 pat[o] = 0 as u8
130 let at: i64 = up_find(src, n, pat)
131 if at < 0 { return 0 }
132 let rest: *u8 = ((src as i64) + at + 1) as *u8
133 let cl: i64 = up_find(rest, n - at - 1, UP_FUNC_CLOSE)
134 box[0] = at
135 if cl >= 0 {
136 // include the brace itself so the span is the whole function and nothing after it
137 box[1] = at + 1 + cl + 2
138 return 1
139 }
140 // no closing brace found (a truncated read) -- fall back to the next function head, and NEVER past the
141 // buffer. This is the conservative direction: a wider span can only add candidate names, and the
142 // classifier treats a body naming two artifacts as UNPROVEN, never as OWN.
143 let nxt: i64 = up_find(rest, n - at - 1, UP_FUNC_HEAD)
144 if nxt < 0 { box[1] = n } else { box[1] = at + 1 + nxt }
145 return 1
146}
147
148
149// ---- ARTIFACT RESOLUTION, TWO HOPS (2026-09-03, added after the first census left 8 rows UNPROVEN) ----
150// MEASURED CAUSE OF THOSE 8, and it was the MATCHER, not the verbs: a ROLLBACK verb never mentions the
151// STAGED name. cmd_mgmtrollback names `nx_mgmt_api.elf.prev` and `nx_mgmt_api.elf`; the row's src is
152// `nx_mgmt_api.elf.new`. Comparing against the staged name can therefore never match a reverse gear.
153// Worse, cmd_superrollback and cmd_toolchainrollback name their subject ONLY THROUGH CONSTS (HC_SELF,
154// HC_TC_CC_PREV) -- there is no literal path in the body at all.
155// ★A REVERSE GEAR THAT NAMES ITS SUBJECT THROUGH A CONST IS STILL NAMING IT. A LITERALS-ONLY MATCHER WOULD
156// HAVE REPORTED THOSE VERBS UNPROVEN FOREVER AND CALLED THAT HONESTY -- an abstention caused by the
157// instrument, dressed as caution about the subject. Shrink UNPROVEN to what is genuinely unresolvable.
158
159// the row's artifact STEM: basename with a trailing ".new" removed, so "nx_mgmt_api.elf.new" -> "nx_mgmt_api.elf"
160// and "nx_torrent_daemon.sov.elf.new" -> "nx_torrent_daemon.sov.elf". That stem is a SUBSTRING of both the
161// live path and the .prev path, which is exactly what a reverse gear touches.
162func up_stem(src: *u8, out: *u8, cap: i64) -> i64 {
163 let n: i64 = up_basename(src, out, cap)
164 if n < 4 { return n }
165 if out[n-4] == (46 as u8) { if out[n-3] == (110 as u8) { if out[n-2] == (101 as u8) { if out[n-1] == (119 as u8) {
166 out[n-4] = 0 as u8
167 return n - 4
168 } } } }
169 return n
170}
171
172// value of `const <name>: *u8 = "<value>"` -- returns 1 and fills out, else 0
173func up_const_value(src: *u8, n: i64, name: *u8, out: *u8, cap: i64) -> i64 {
174 let pat: *u8 = sys_mmap(256)
175 var o: i64 = 0
176 var i: i64 = 0
177 while UP_CONST_PFX[i] != (0 as u8) { pat[o] = UP_CONST_PFX[i]; o = o + 1; i = i + 1 }
178 i = 0
179 while name[i] != (0 as u8) { pat[o] = name[i]; o = o + 1; i = i + 1 }
180 pat[o] = 58 as u8
181 o = o + 1
182 pat[o] = 0 as u8
183 let at: i64 = up_find(src, n, pat)
184 if at < 0 { return 0 }
185 // first quote after the declaration, then capture to the closing quote
186 var p: i64 = at
187 var qs: i64 = 0 - 1
188 var go: i64 = 1
189 while go == 1 {
190 if p >= n { go = 0 } else {
191 if (src[p] as i64) == 34 { qs = p; go = 0 } else {
192 if (src[p] as i64) == 10 { go = 0 } else { p = p + 1 }
193 }
194 }
195 }
196 if qs < 0 { return 0 }
197 var w: i64 = 0
198 var q: i64 = qs + 1
199 go = 1
200 while go == 1 {
201 if q >= n { go = 0 } else {
202 if (src[q] as i64) == 34 { go = 0 } else {
203 if w + 1 >= cap { go = 0 } else { out[w] = src[q]; w = w + 1; q = q + 1 }
204 }
205 }
206 }
207 out[w] = 0 as u8
208 if w == 0 { return 0 }
209 return 1
210}
211
212// Does this verb body NAME the artifact stem -- directly, or through a const it mentions?
213func up_body_names(src: *u8, n: i64, bs: i64, be: i64, stem: *u8) -> i64 {
214 if up_len(stem) == 0 { return 0 }
215 let bp: *u8 = ((src as i64) + bs) as *u8
216 let bn: i64 = be - bs
217 if bn <= 0 { return 0 }
218 if up_find(bp, bn, stem) >= 0 { return 1 }
219 let nm: *u8 = sys_mmap(256)
220 let vb: *u8 = sys_mmap(1024)
221 var i: i64 = 0
222 while i < bn {
223 var hit: i64 = 0
224 if (bp[i] as i64) == 72 { if i + 2 < bn { if (bp[i+1] as i64) == 67 { if (bp[i+2] as i64) == 95 { hit = 1 } } } }
225 if hit == 1 {
226 var j: i64 = i
227 var w: i64 = 0
228 var go: i64 = 1
229 while go == 1 {
230 if j >= bn { go = 0 } else {
231 let c: i64 = bp[j] as i64
232 var isid: i64 = 0
233 if c == 95 { isid = 1 }
234 if c >= 48 { if c <= 57 { isid = 1 } }
235 if c >= 65 { if c <= 90 { isid = 1 } }
236 if c >= 97 { if c <= 122 { isid = 1 } }
237 if isid == 0 { go = 0 } else {
238 if w + 1 < 256 { nm[w] = bp[j]; w = w + 1 }
239 j = j + 1
240 }
241 }
242 }
243 nm[w] = 0 as u8
244 if w > 3 {
245 if up_const_value(src, n, nm, vb, 1024) == 1 {
246 if up_find(vb, up_len(vb), stem) >= 0 { return 1 }
247 }
248 }
249 if j > i { i = j } else { i = i + 1 }
250 } else { i = i + 1 }
251 }
252 return 0
253}
254
255// PURE: the classification. Every input is an already-resolved fact so a gate can drive every branch.
256// is_edge -- this row IS the edge (it owns sites.elf)
257// rb_is_edge_gear -- the rb verb is the hardcoded edge gear (cmd_rollback, no target argument)
258// rb_perrow_self -- rb is the generic per-row gear pointed at THIS row
259// rb_perrow_other -- rb is the generic per-row gear pointed at ANOTHER row
260// verb_exists -- a cmd_<rb> is defined in the control-plane source
261// body_own -- that verb's body names this row's own artifact
262// body_other -- that verb's body names some other row's artifact
263// ORDER MATTERS and is the whole safety argument: the edge gear is decided FIRST, because it is the one
264// verb that is correct for exactly one row and catastrophic for every other.
265func up_classify(is_edge: i64, rb_is_edge_gear: i64, rb_perrow_self: i64, rb_perrow_other: i64,
266 verb_exists: i64, body_own: i64, body_other: i64) -> i64 {
267 // ⚠VERB EXISTENCE IS NOW THE FIRST QUESTION, MOVED HERE 2026-09-03, AND IT CLOSED A VACUITY IN THIS
268 // VERY RULER. It used to be checked only AFTER the edge-gear and per-row branches, so `rb_perrow_self`
269 // returned OWN from the ROW'S SPELLING ALONE -- the gate never asked whether cmd_gdeploy_rollback
270 // exists in the control plane at all. MEASURED: the moment 16 rows were re-pointed at gdeployrb@<row>
271 // the census called all 16 OWN-SUBJECT while the LIVE hostctl did not implement that verb, so their
272 // real behaviour was the dispatcher's unknown-subcommand no-op.
273 // ★A COMPLETION SIGNAL THAT KEYS ON A NAME REWARDS WRITING THE NAME -- the estate says this about
274 // compare watches, and this ruler was doing it to itself: declaring the gear was scored as having it.
275 // Asking first is also strictly MORE truthful for every other branch: an unimplemented verb cannot act
276 // on anything, so whose subject it NAMES is irrelevant -- it is the dispatcher's proven no-op either
277 // way. That ordering leaves every existing branch verdict unchanged (they all pass verb_exists=1),
278 // which is why this is a safe reorder and not a re-specification.
279 if verb_exists == 0 { return UP_FAILSAFE }
280 if rb_is_edge_gear == 1 {
281 if is_edge == 1 { return UP_OWN }
282 return UP_WRONG
283 }
284 if rb_perrow_other == 1 { return UP_WRONG }
285 if rb_perrow_self == 1 { return UP_OWN }
286 if body_other == 1 {
287 if body_own == 1 { return UP_UNPROVEN }
288 return UP_WRONG
289 }
290 if body_own == 1 { return UP_OWN }
291 return UP_UNPROVEN
292}
293
294// ---- HOP 3: THE PAIR (2026-09-03, added after hops 1+2 still left galxgw UNPROVEN) ------------------
295// MEASURED CAUSE, and it was the PAIR I was comparing, not the gear: row galxgw stages
296// `nx_gallery_gateway.sov.elf.new` in nishihost, but cmd_galxdeploy DELIBERATELY BRIDGES that artifact into
297// /volume1/ai/galx/nx_gallery_gateway.elf ("bridged nishihost .sov.elf.new -> galx .elf.new" -- its own
298// words), and cmd_galxgwrollback restores /volume1/ai/galx/nx_gallery_gateway.elf.prev over exactly that
299// live path. The reverse gear agrees with its FORWARD gear perfectly; only the row's STAGED filename
300// differs, by a `.sov` infix and a directory.
301// ★THE INVARIANT IS PAIRWISE, NOT ROW-TO-VERB: A REVERSE GEAR IS CORRECT IFF IT ACTS ON THE ARTIFACT ITS
302// OWN FORWARD GEAR WRITES. Comparing it against the row's staged filename measures the WRONG PAIR the
303// moment the forward gear bridges paths -- and a bridge is legitimate, common, and documented in the
304// forward verb itself.
305// STRICTLY ADDITIVE BY CONSTRUCTION: up_classify is UNTOUCHED and up_classify_pair may only convert
306// UNPROVEN -> OWN. It can never convert WRONG -> OWN, so a wrong-subject gear cannot be acquitted by
307// discovering that its forward twin is wrong in the same way. That property is exhaustively provable over
308// all 128 input combinations, and the gate proves it rather than asserting it.
309
310// the artifact NAME a deploy pair actually operates on: basename, with a trailing .new or .prev removed
311// (a forward gear names <a>.new and <a>; a reverse gear names <a>.prev and <a>; the shared token is <a>)
312func up_artifact_name(path: *u8, out: *u8, cap: i64) -> i64 {
313 var n: i64 = up_basename(path, out, cap)
314 if n > 4 {
315 if out[n-4] == (46 as u8) { if out[n-3] == (110 as u8) { if out[n-2] == (101 as u8) { if out[n-1] == (119 as u8) {
316 n = n - 4
317 out[n] = 0 as u8
318 } } } }
319 }
320 if n > 5 {
321 if out[n-5] == (46 as u8) { if out[n-4] == (112 as u8) { if out[n-3] == (114 as u8) { if out[n-2] == (101 as u8) { if out[n-1] == (118 as u8) {
322 n = n - 5
323 out[n] = 0 as u8
324 } } } } }
325 }
326 return n
327}
328
329// Does the FORWARD verb body (fs..fe) and the REVERSE verb body (bs..be) name a COMMON artifact?
330// Candidates come from the consts the forward body mentions -- which is how a control-plane verb names a
331// path -- reduced to their artifact name; each is then tested against the reverse body through the SAME
332// two-hop resolver (up_body_names), so there is exactly one matcher in this file, never two.
333func up_pair_common(src: *u8, n: i64, fs: i64, fe: i64, bs: i64, be: i64) -> i64 {
334 if fe <= fs { return 0 }
335 if be <= bs { return 0 }
336 let fp: *u8 = ((src as i64) + fs) as *u8
337 let fn: i64 = fe - fs
338 let nm: *u8 = sys_mmap(256)
339 let vb: *u8 = sys_mmap(1024)
340 let cand: *u8 = sys_mmap(256)
341 var i: i64 = 0
342 while i < fn {
343 var hit: i64 = 0
344 if (fp[i] as i64) == 72 { if i + 2 < fn { if (fp[i+1] as i64) == 67 { if (fp[i+2] as i64) == 95 { hit = 1 } } } }
345 if hit == 1 {
346 var j: i64 = i
347 var w: i64 = 0
348 var go: i64 = 1
349 while go == 1 {
350 if j >= fn { go = 0 } else {
351 let c: i64 = fp[j] as i64
352 var isid: i64 = 0
353 if c == 95 { isid = 1 }
354 if c >= 48 { if c <= 57 { isid = 1 } }
355 if c >= 65 { if c <= 90 { isid = 1 } }
356 if c >= 97 { if c <= 122 { isid = 1 } }
357 if isid == 0 { go = 0 } else {
358 if w + 1 < 256 { nm[w] = fp[j]; w = w + 1 }
359 j = j + 1
360 }
361 }
362 }
363 nm[w] = 0 as u8
364 if w > 3 {
365 if up_const_value(src, n, nm, vb, 1024) == 1 {
366 // only a path that names an artifact can be a shared subject
367 if up_find(vb, up_len(vb), ".elf" as *u8) >= 0 {
368 let cn: i64 = up_artifact_name(vb, cand, 256)
369 if cn > 4 {
370 if up_body_names(src, n, bs, be, cand) == 1 { return 1 }
371 }
372 }
373 }
374 }
375 if j > i { i = j } else { i = i + 1 }
376 } else { i = i + 1 }
377 }
378 return 0
379}
380
381// The pairwise rescue. STRICTLY ADDITIVE: UNPROVEN -> OWN when the pair provably agrees, nothing else.
382func up_classify_pair(is_edge: i64, rb_is_edge_gear: i64, rb_perrow_self: i64, rb_perrow_other: i64,
383 verb_exists: i64, body_own: i64, body_other: i64, pair_own: i64) -> i64 {
384 let s: i64 = up_classify(is_edge, rb_is_edge_gear, rb_perrow_self, rb_perrow_other,
385 verb_exists, body_own, body_other)
386 if s == UP_UNPROVEN { if pair_own == 1 { return UP_OWN } }
387 return s
388}
389
390// RATCHET arithmetic (PURE): the wrong-subject count may only fall. Returns the floor to WRITE, or -1 when
391// the observed count is ABOVE the floor -- a regression, and the baseline is NOT rewritten.
392func up_ratchet_next(floor: i64, wrong: i64) -> i64 {
393 if wrong < 0 { return 0 - 1 }
394 if floor < 0 { return wrong }
395 if wrong > floor { return 0 - 1 }
396 return wrong
397}