code wiki / _hdl_build / nx_boot_revive_m6_gate.nx
nx_boot_revive_m6_gate.nx source
↩ module page · 293 lines · 15045 B
1import "nx_gate_gn.nx"
2// nx_boot_revive_m6_gate.nx -- the REFEREE for M6 (boot-revive crash-recovery capstone).
3//
4// Proves nx_boot_revive's M6 upgrade (section 1c, br_replay_resume) RECONSTRUCTS and
5// RESUMES exactly the workstreams that were IN-FLIGHT at a crash, and does NOT resume
6// completed ones -- by REPLAYING the WMS-R2 transition reflog (ledger_replay) for the
7// authoritative current state AND checking WMS-M1 heartbeats (hbm_scan / hb_last_beat)
8// for "recently beating == in-flight at crash" liveness.
9//
10// POSITIVE (the crash scenario): seed a crash state with 2 IN-FLIGHT streams (ws=1,2:
11// reflog new != DONE, heartbeat within threshold) + 1 COMPLETED stream (ws=3: reflog
12// new == DONE) + 1 STALE decoy (ws=4: not-done but heartbeat far past threshold).
13// Expect br_replay_resume: resumed==2 (ws1,ws2 only), completed_skipped==1 (ws3),
14// stale_not_resumed==1 (ws4 -- proves the gate is "recently beating", not just
15// "not done"). The resume JOURNAL must contain BR-RESUME ws=1 and ws=2 and must
16// NOT contain ws=3 or ws=4 (byte-scan, the ledger-gate idiom).
17//
18// NEG-CONTROL #1 (mandatory the-detector-can-see-nothing): a CLEAN boot -- empty
19// reflog + empty heartbeat channel -> nothing seen -> resumed==0. If a clean boot
20// EVER resumes >0 the detector fabricates work -> RED. This is "the crash becomes a
21// non-event AND a no-crash stays a no-event".
22//
23// NEG-CONTROL #2 (corruption surfaced, never swallowed): append one TORN reflog record
24// (no " END" sentinel) -> ledger_flagged >= 1. flagged==0 => corruption silently
25// swallowed => RED.
26//
27// WRITE DISCIPLINE: the gate's OWN logger uses fa_appendz (one assembled record, one
28// locked write) to a UNIQUE scratch path (/tmp/m6_gate_<epoch>_<pid>.log) THEN mirrors
29// the same record to the durable knowledge/status/boot_revive_m6_gate.log. NEVER a
30// sequence of sys_write for a record. Exit 0 GREEN, 1 RED. Sovereign: only nx_syscalls
31// + nx_ws_ledger + nx_heartbeat_monitor + nx_boot_revive (for the REAL br_replay_resume).
32// No-false-green: GREEN requires every lane. license_tier: ORIGINAL
33import "nx_syscalls.nx"
34import "nx_ws_ledger.nx"
35import "nx_heartbeat_monitor.nx"
36import "nx_boot_revive.nx"
37
38const G_RECCAP: i64 = 512 // bounded gate-log record size
39const G_NOW: i64 = 1000 // injected wall-clock for the test (deterministic)
40const G_THR: i64 = 60 // injected liveness threshold
41const G_DONE: i64 = 3 // ledger DONE state code (== BR_WS_DONE)
42
43// stdout printers (console only; the DURABLE record goes via fa_appendz below)
44func gp(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 }
45
46// truncate a file to empty (fresh fixture each run)
47func g_fresh(path: *u8) -> i64 {
48 let fd: i64 = sys_openat_wr(path, 0x1a4)
49 if fd > 0 { sys_close(fd) }
50 return 0
51}
52// build "/tmp/<base>_<pid>.log" into out -- PID-NAMESPACED fixture so CONCURRENT gate runs never share
53// /tmp state (the de-flake: the fixed /tmp/m6_*.log paths corrupted each other under parallel sweeps).
54func g_pidpath(base: *u8, pid: i64, out: *u8) -> i64 {
55 var o: i64 = fa_cat(out, 0, "/tmp/\x00" as *u8)
56 o = fa_cat(out, o, base)
57 out[o] = 95 as u8; o = o + 1 // '_'
58 o = fa_catn(out, o, pid)
59 o = fa_cat(out, o, ".log\x00" as *u8)
60 out[o] = 0 as u8
61 return o
62}
63// getpid (__syscall 39) is BROKEN on this backend (returns -25 for EVERY process -> not unique -> the real
64// cause of the intermittent-RED control-plane flake). Claim a process-unique i64 token ATOMICALLY via O_EXCL:
65// the first process to create /tmp/nxuq_<n> owns <n>; a collision (EEXIST, fd<0) retries n+1. Seeded by
66// monotonic microseconds so concurrent runs start at different points. Provably collision-free.
67func g_uniq() -> i64 {
68 var n: i64 = sys_now_us()
69 if n < 0 { n = 0 - n }
70 var tries: i64 = 0
71 while tries < 1000000 {
72 let p: *u8 = sys_mmap(64)
73 var o: i64 = fa_cat(p, 0, "/tmp/nxuq_\x00" as *u8)
74 o = fa_catn(p, o, n)
75 p[o] = 0 as u8
76 let fd: i64 = __syscall(SYS_OPENAT, AT_FDCWD, p, 0xc1, 0x1a4, 0, 0) // O_CREAT|O_EXCL|O_WRONLY
77 if fd >= 0 { sys_close(fd); return n }
78 n = n + 1
79 tries = tries + 1
80 }
81 return n
82}
83
84// does buffer of n bytes contain the nul-terminated pat? (byte-scan, ledger-gate idiom)
85func g_contains(hay: *u8, n: i64, pat: *u8) -> i64 {
86 var pl: i64 = 0
87 while pat[pl] != (0 as u8) { pl = pl + 1 }
88 if pl == 0 { return 0 }
89 var i: i64 = 0
90 while i + pl <= n {
91 var k: i64 = 0
92 var hit: i64 = 1
93 while k < pl { if hay[i+k] != pat[k] { hit = 0; k = pl } else { k = k + 1 } }
94 if hit == 1 { return 1 }
95 i = i + 1
96 }
97 return 0
98}
99func g_readall(path: *u8, buf: *u8, cap: i64) -> i64 {
100 let fd: i64 = sys_openat_rd(path)
101 if fd < 0 { return 0 }
102 var n: i64 = 0
103 var go: i64 = 1
104 while go == 1 { let base: i64 = buf as i64; let r: i64 = sys_read(fd, (base + n) as *u8, cap - n); if r <= 0 { go = 0 } else { n = n + r } if n >= cap { go = 0 } }
105 sys_close(fd)
106 return n
107}
108
109// ONE framed gate-log record via fa_appendz to BOTH the unique scratch path AND the
110// durable log -- assembled into one buffer, one locked write each (no torn lines).
111func g_logrow(scratch: *u8, durable: *u8, label: *u8, got: i64, want: *u8, pass: i64) -> i64 {
112 let rec: *u8 = sys_mmap(G_RECCAP + 16)
113 var o: i64 = 0
114 o = fa_cat(rec, o, "M6 row=\x00" as *u8)
115 o = fa_cat(rec, o, label)
116 o = fa_cat(rec, o, " got=\x00" as *u8)
117 o = fa_catn(rec, o, got)
118 o = fa_cat(rec, o, " want=\x00" as *u8)
119 o = fa_cat(rec, o, want)
120 if pass == 1 { o = fa_cat(rec, o, " verdict=PASS\x00" as *u8) } else { o = fa_cat(rec, o, " verdict=FAIL\x00" as *u8) }
121 rec[o] = 0 as u8
122 fa_appendz(scratch, rec, G_RECCAP)
123 fa_appendz(durable, rec, G_RECCAP)
124 // console echo
125 gp("M6 row=\x00" as *u8); gp(label); gp(" got=\x00" as *u8); gn(got); gp(" want=\x00" as *u8); gp(want)
126 if pass == 1 { gp(" verdict=PASS\n\x00" as *u8) } else { gp(" verdict=FAIL\n\x00" as *u8) }
127 return 0
128}
129
130func main() -> i64 {
131 let epoch: i64 = sys_now_realtime_sec()
132 let pid: i64 = __syscall(39, 0, 0, 0, 0, 0, 0) // kept ONLY as a semantic worker-id field in the ledger/hb fixtures (value is irrelevant; -25 on this backend)
133 let uniq: i64 = g_uniq() // the REAL per-process namespace for ALL scratch paths
134 // UNIQUE scratch path: /tmp/m6_gate_<epoch>_<uniq>.log
135 let scratch: *u8 = sys_mmap(128)
136 var so: i64 = 0
137 so = fa_cat(scratch, so, "/tmp/m6_gate_\x00" as *u8)
138 so = fa_catn(scratch, so, epoch)
139 so = fa_cat(scratch, so, "_\x00" as *u8)
140 so = fa_catn(scratch, so, uniq)
141 so = fa_cat(scratch, so, ".log\x00" as *u8)
142 scratch[so] = 0 as u8
143 let durable: *u8 = "knowledge/status/boot_revive_m6_gate.log\x00" as *u8
144
145 // ============ POSITIVE: the crash scenario ============
146 let ledger: *u8 = sys_mmap(128); g_pidpath("m6_ledger\x00" as *u8, uniq,ledger)
147 let hb: *u8 = sys_mmap(128); g_pidpath("m6_hb\x00" as *u8, uniq,hb)
148 let resume: *u8 = sys_mmap(128); g_pidpath("m6_resume\x00" as *u8, uniq,resume)
149 g_fresh(ledger); g_fresh(hb); g_fresh(resume)
150
151 // reflog: ws1 -> WIP(1), ws2 -> VIEW(2) [both NOT done], ws3 -> DONE(3), ws4 -> WIP(1)
152 ledger_append(ledger, 1, 0, 1, pid, 0, 1001) // ws1 ends WIP (in-flight candidate)
153 ledger_append(ledger, 2, 0, 2, pid, 0, 1002) // ws2 ends VIEW (in-flight candidate)
154 ledger_append(ledger, 3, 1, 3, pid, 0, 1003) // ws3 ends DONE (completed -> exclude)
155 ledger_append(ledger, 4, 0, 1, pid, 0, 1004) // ws4 ends WIP (not done, but stale below)
156
157 // heartbeats (now=1000, thr=60): ws1 age20 ALIVE, ws2 age25 ALIVE, ws3 age30 ALIVE(but DONE),
158 // ws4 age200 STALLED -> the decoy that proves "recently beating", not merely "not done".
159 hb_beat_at(hb, 1, 980, 0, pid)
160 hb_beat_at(hb, 2, 975, 0, pid)
161 hb_beat_at(hb, 3, 970, 0, pid)
162 hb_beat_at(hb, 4, 800, 0, pid)
163
164 let ctr: *i64 = sys_mmap(8*8) as *i64
165 var z: i64 = 0
166 while z < 8 { ctr[z] = 0; z = z + 1 }
167 // CALL THE REAL CAPABILITY under test:
168 br_replay_resume(ledger, hb, resume, G_NOW, G_THR, 1000, ctr)
169 let resumed: i64 = ctr[0]
170 let completed: i64 = ctr[1]
171 let lflag: i64 = ctr[2]
172 let hflag: i64 = ctr[3]
173 let stale: i64 = ctr[4]
174 let seen: i64 = ctr[5]
175
176 // resume journal must name ws1+ws2, must NOT name ws3/ws4
177 let rb: *u8 = sys_mmap(65536)
178 let rn: i64 = g_readall(resume, rb, 65520)
179 let has1: i64 = g_contains(rb, rn, "BR-RESUME ws=1 \x00" as *u8)
180 let has2: i64 = g_contains(rb, rn, "BR-RESUME ws=2 \x00" as *u8)
181 let has3: i64 = g_contains(rb, rn, "BR-RESUME ws=3 \x00" as *u8)
182 let has4: i64 = g_contains(rb, rn, "BR-RESUME ws=4 \x00" as *u8)
183
184 // ============ NEG-CONTROL #1: clean boot resumes nothing ============
185 let cl_ledger: *u8 = sys_mmap(128); g_pidpath("m6_clean_ledger\x00" as *u8, uniq,cl_ledger)
186 let cl_hb: *u8 = sys_mmap(128); g_pidpath("m6_clean_hb\x00" as *u8, uniq,cl_hb)
187 let cl_resume: *u8 = sys_mmap(128); g_pidpath("m6_clean_resume\x00" as *u8, uniq,cl_resume)
188 g_fresh(cl_ledger); g_fresh(cl_hb); g_fresh(cl_resume)
189 let cctr: *i64 = sys_mmap(8*8) as *i64
190 z = 0
191 while z < 8 { cctr[z] = 0; z = z + 1 }
192 br_replay_resume(cl_ledger, cl_hb, cl_resume, G_NOW, G_THR, 1000, cctr)
193 let clean_resumed: i64 = cctr[0]
194
195 // ============ NEG-CONTROL #2: corruption surfaced ============
196 // append one TORN reflog record (missing the " END" sentinel) to a fresh ledger.
197 let tm_ledger: *u8 = sys_mmap(128); g_pidpath("m6_tamper_ledger\x00" as *u8, uniq,tm_ledger)
198 let tm_hb: *u8 = sys_mmap(128); g_pidpath("m6_tamper_hb\x00" as *u8, uniq,tm_hb)
199 let tm_resume: *u8 = sys_mmap(128); g_pidpath("m6_tamper_resume\x00" as *u8, uniq,tm_resume)
200 g_fresh(tm_ledger); g_fresh(tm_hb); g_fresh(tm_resume)
201 ledger_append(tm_ledger, 1, 0, 1, pid, 0, 1001)
202 let tfd: i64 = sys_openat_append(tm_ledger, 0x1a4)
203 if tfd > 0 {
204 sys_write(tfd, "WSX ws=2 old=1 new=2 actor=7 reason=9 ev=0 epoch=0 BROKEN\n\x00" as *u8, 58)
205 sys_close(tfd)
206 }
207 let tctr: *i64 = sys_mmap(8*8) as *i64
208 z = 0
209 while z < 8 { tctr[z] = 0; z = z + 1 }
210 br_replay_resume(tm_ledger, tm_hb, tm_resume, G_NOW, G_THR, 1000, tctr)
211 let tamper_lflag: i64 = tctr[2]
212
213 // ============ rows (each via fa_appendz; no torn lines) ============
214 var p_resumed: i64 = 0
215 if resumed == 2 { p_resumed = 1 }
216 g_logrow(scratch, durable, "resumed_inflight\x00" as *u8, resumed, "2\x00" as *u8, p_resumed)
217
218 var p_completed: i64 = 0
219 if completed == 1 { p_completed = 1 }
220 g_logrow(scratch, durable, "completed_skipped\x00" as *u8, completed, "1\x00" as *u8, p_completed)
221
222 var p_stale: i64 = 0
223 if stale == 1 { p_stale = 1 }
224 g_logrow(scratch, durable, "stale_not_resumed\x00" as *u8, stale, "1\x00" as *u8, p_stale)
225
226 var p_j1: i64 = 0
227 if has1 == 1 { p_j1 = 1 }
228 g_logrow(scratch, durable, "journal_has_ws1\x00" as *u8, has1, "1\x00" as *u8, p_j1)
229 var p_j2: i64 = 0
230 if has2 == 1 { p_j2 = 1 }
231 g_logrow(scratch, durable, "journal_has_ws2\x00" as *u8, has2, "1\x00" as *u8, p_j2)
232 var p_j3: i64 = 0
233 if has3 == 0 { p_j3 = 1 }
234 g_logrow(scratch, durable, "journal_excludes_ws3_done\x00" as *u8, has3, "0\x00" as *u8, p_j3)
235 var p_j4: i64 = 0
236 if has4 == 0 { p_j4 = 1 }
237 g_logrow(scratch, durable, "journal_excludes_ws4_stale\x00" as *u8, has4, "0\x00" as *u8, p_j4)
238
239 var p_clean: i64 = 0
240 if clean_resumed == 0 { p_clean = 1 }
241 g_logrow(scratch, durable, "negctrl_clean_boot_resumed\x00" as *u8, clean_resumed, "0\x00" as *u8, p_clean)
242
243 var p_tamper: i64 = 0
244 if tamper_lflag >= 1 { p_tamper = 1 }
245 g_logrow(scratch, durable, "negctrl_corruption_flagged\x00" as *u8, tamper_lflag, ">=1\x00" as *u8, p_tamper)
246
247 // ============ verdict (no false green) ============
248 var green: i64 = 1
249 if resumed != 2 { green = 0 } // exactly the 2 in-flight resumed
250 if completed != 1 { green = 0 } // DONE excluded
251 if stale != 1 { green = 0 } // stale (recently-beating gate) NOT resumed
252 if has1 != 1 { green = 0 } // journal names ws1
253 if has2 != 1 { green = 0 } // journal names ws2
254 if has3 != 0 { green = 0 } // journal excludes completed ws3
255 if has4 != 0 { green = 0 } // journal excludes stale ws4
256 if clean_resumed != 0 { green = 0 } // NEG-CTRL: clean boot resumes nothing
257 if tamper_lflag < 1 { green = 0 } // NEG-CTRL: corruption surfaced
258
259 // final verdict record (one assembled buffer, one locked write to each sink)
260 let frec: *u8 = sys_mmap(G_RECCAP + 16)
261 var fo: i64 = 0
262 fo = fa_cat(frec, fo, "BOOT-REVIVE-M6 verdict=\x00" as *u8)
263 if green == 1 { fo = fa_cat(frec, fo, "GREEN\x00" as *u8) } else { fo = fa_cat(frec, fo, "RED\x00" as *u8) }
264 fo = fa_cat(frec, fo, " epoch=\x00" as *u8); fo = fa_catn(frec, fo, epoch)
265 fo = fa_cat(frec, fo, " resumed=\x00" as *u8); fo = fa_catn(frec, fo, resumed)
266 fo = fa_cat(frec, fo, " completed_skipped=\x00" as *u8); fo = fa_catn(frec, fo, completed)
267 fo = fa_cat(frec, fo, " stale_not_resumed=\x00" as *u8); fo = fa_catn(frec, fo, stale)
268 fo = fa_cat(frec, fo, " streams_seen=\x00" as *u8); fo = fa_catn(frec, fo, seen)
269 fo = fa_cat(frec, fo, " clean_boot_resumed=\x00" as *u8); fo = fa_catn(frec, fo, clean_resumed)
270 fo = fa_cat(frec, fo, " ledger_flagged=\x00" as *u8); fo = fa_catn(frec, fo, lflag)
271 fo = fa_cat(frec, fo, " hb_flagged=\x00" as *u8); fo = fa_catn(frec, fo, hflag)
272 fo = fa_cat(frec, fo, " tamper_flagged=\x00" as *u8); fo = fa_catn(frec, fo, tamper_lflag)
273 if green == 0 {
274 fo = fa_cat(frec, fo, " reason=\x00" as *u8)
275 if resumed != 2 { fo = fa_cat(frec, fo, "wrong-resume-count \x00" as *u8) }
276 if completed != 1 { fo = fa_cat(frec, fo, "completed-not-excluded \x00" as *u8) }
277 if stale != 1 { fo = fa_cat(frec, fo, "stale-handling-wrong \x00" as *u8) }
278 if has1 != 1 { fo = fa_cat(frec, fo, "ws1-not-journaled \x00" as *u8) }
279 if has2 != 1 { fo = fa_cat(frec, fo, "ws2-not-journaled \x00" as *u8) }
280 if has3 != 0 { fo = fa_cat(frec, fo, "ws3-done-spuriously-resumed \x00" as *u8) }
281 if has4 != 0 { fo = fa_cat(frec, fo, "ws4-stale-spuriously-resumed \x00" as *u8) }
282 if clean_resumed != 0 { fo = fa_cat(frec, fo, "CLEAN-BOOT-FABRICATED-RESUME \x00" as *u8) }
283 if tamper_lflag < 1 { fo = fa_cat(frec, fo, "corruption-swallowed \x00" as *u8) }
284 }
285 frec[fo] = 0 as u8
286 fa_appendz(scratch, frec, G_RECCAP)
287 fa_appendz(durable, frec, G_RECCAP)
288 gp(frec); gp("\n\x00" as *u8)
289
290 if green == 1 { sys_exit(0); return 0 }
291 sys_exit(1)
292 return 1
293}