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}