nx_ws_board_gate.nx source

1// nx_ws_board_gate.nx -- THE REFEREE for WMS rung M2 (the live status board). 2// 3// Proves nx_ws_board DERIVES the correct per-empire/per-stream view from the WMS-R1 4// registry, AND that it is NEVER silently wrong -- the four mandatory negative controls 5// prove the detector can actually SEE failure (no-false-green): 6// 7// HERMETIC fixtures (controlled, NOT production claims): 8// prefix wsboard- : ws:empires = E-A,E-B,E-C ; ws:ids = B-1..B-4 ; 4 complete streams 9// B-1 E-A DONE / B-2 E-A ACTIVE / B-3 E-B BLOCKED / B-4 E-C DONE 10// prefix wsboard2- : ws:ids lists B2-1 + B2-LOST, but ws:B2-LOST is NEVER committed 11// (the lost-segment fault, twin of registry-gate T5). 12// 13// POSITIVE (all must hold for GREEN): 14// T1 enumerate-exact : wb_board_p(wsboard-, refpath=0) returns empires=3. 15// T2 per-empire counts EXACT : E-A streams=2 done=1 active=1 blocked=0 ; 16// E-B streams=1 blocked=1 ; E-C streams=1 done=1. 17// T3 summary EXACT : total=4 done=2 active=1 blocked=1. 18// T4 clean-reflog overlay : a /tmp reflog of good ledger_append records (flagged=0) 19// -> wb_board_p(..., refpath=good) returns >=0 (accepted). 20// 21// NEGATIVE CONTROLS (a GREEN with no working neg-control is INVALID): 22// N1 unregistered-absent : ws_get_p(wsboard-, ws:B-NEVER) == WS_UNKNOWN(-1) AND 23// "B-NEVER" appears in ZERO board empire rows. 24// N2 torn-reflog REJECTED : a /tmp reflog = good records + one raw line MISSING the 25// " END" sentinel -> wb_board_p(..., refpath=torn) == -3 26// (rejected, NOT silently rendered). >=0 => RED. 27// N3 incomplete-registry REJECTED : wb_board_p(wsboard2-, 0) == -1 (lost segment -> 28// board refuses). >=0 => RED. 29// N4 detector-sees-difference : N2's -3 and T4's >=0 are DIFFERENT return values on 30// contrasting inputs (proves the guard is not a constant). 31// 32// GREEN only if T1..T4 AND N1..N4 all hold. Evidence rows + verdict go to 33// knowledge/status/ws_board_gate.log via the MANDATORY fa_appendz one-buffer-one-locked- 34// write discipline (eat-own-dogfood); fixture /tmp reflogs use epoch+pid-suffixed names 35// so concurrent gate runs never collide. Exit 0 GREEN / 1 RED. 36// Sovereign: imports only the WMS stack + nx_syscalls (no gcc). license_tier: ORIGINAL 37import "nx_ws_board.nx" 38import "nx_workstream_store.nx" 39import "nx_ws_ledger.nx" 40import "nx_framed_append.nx" 41import "nx_seg_store.nx" 42import "nx_syscalls.nx" 43 44const WBG_LOG: *u8 = "knowledge/status/ws_board_gate.log" 45const WBG_PREFIX: *u8 = "knowledge/store/wsboard-" 46const WBG_PREFIX2: *u8 = "knowledge/store/wsboard2-" 47const WBG_RECCAP: i64 = 512 48 49func wbg_len(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } return n } 50 51func wbg_streq(a: *u8, b: *u8) -> i64 { 52 var i: i64 = 0 53 while a[i] != (0 as u8) { if a[i] != b[i] { return 0 } i = i + 1 } 54 if b[i] != (0 as u8) { return 0 } 55 return 1 56} 57 58// 1 if store value for key under `prefix` byte-equals val (idempotent seed helper). 59func wbg_streq_store(prefix: *u8, key: *u8, val: *u8) -> i64 { 60 let pq: *i64 = sys_mmap(16) as *i64 61 let lq: *i64 = sys_mmap(16) as *i64 62 if ss_get(prefix, key, pq, lq) != 1 { return 0 } 63 let b: *u8 = pq[0] as *u8 64 let n: i64 = lq[0] 65 let vl: i64 = wbg_len(val) 66 if n != vl { return 0 } 67 var i: i64 = 0 68 while i < n { if b[i] != val[i] { return 0 } i = i + 1 } 69 return 1 70} 71 72// commit one (key,val) into `prefix`, idempotent (wrg_seed_one idiom). 73func wbg_seed_one(prefix: *u8, key: *u8, val: *u8) -> i64 { 74 if wbg_streq_store(prefix, key, val) == 1 { return 1 } 75 let w: *i64 = ss_begin() 76 ss_add(w, 1, key, val, wbg_len(val)) 77 let segid: i64 = ws_seg_next(prefix) 78 return ss_commit(prefix, w, segid) 79} 80 81// find empire row e in rows[] whose empire-id == name; return its base index, or -1. 82func wbg_find(rows: *i64, ecount: i64, name: *u8) -> i64 { 83 var e: i64 = 0 84 while e < ecount { 85 let base: i64 = e * WB_ROWW 86 if wbg_streq(rows[base + 0] as *u8, name) == 1 { return base } 87 e = e + 1 88 } 89 return 0 - 1 90} 91 92// decimal of v into dst at off (for building the unique /tmp path suffix). 93func wbg_catn(dst: *u8, off: i64, v: i64) -> i64 { 94 var m: i64 = v; var o: i64 = off 95 if m < 0 { m = 0 - m } 96 let t: *u8 = sys_mmap(28); var k: i64 = 0 97 if m == 0 { t[0] = 48 as u8; k = 1 } 98 while m > 0 { t[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 } 99 var i: i64 = 0 100 while i < k { dst[o + i] = t[k - 1 - i]; i = i + 1 } 101 return o + k 102} 103func wbg_cat(dst: *u8, off: i64, s: *u8) -> i64 { 104 var i: i64 = 0 105 while s[i] != (0 as u8) { dst[off + i] = s[i]; i = i + 1 } 106 return off + i 107} 108 109// build a unique /tmp path = <stem><epoch>.<pid>.log into out (NUL-term). 110func wbg_tmppath(out: *u8, stem: *u8, epoch: i64, pid: i64) -> i64 { 111 var o: i64 = 0 112 o = wbg_cat(out, o, stem) 113 o = wbg_catn(out, o, epoch) 114 o = wbg_cat(out, o, "." as *u8) 115 o = wbg_catn(out, o, pid) 116 o = wbg_cat(out, o, ".log" as *u8) 117 out[o] = 0 as u8 118 return o 119} 120 121// MANDATORY WRITE DISCIPLINE: one PASS/FAIL row assembled into one buffer, ONE locked 122// fa_appendz (eat-own-dogfood). Also mirrored to stdout (terminal, uncontended). 123func wbg_row(name: *u8, pass: i64) -> i64 { 124 let buf: *u8 = sys_mmap(WBG_RECCAP + 16) 125 var o: i64 = 0 126 o = wbg_cat(buf, o, "WSB row=\x00" as *u8) 127 o = wbg_cat(buf, o, name) 128 if pass == 1 { o = wbg_cat(buf, o, " verdict=PASS\x00" as *u8) } else { o = wbg_cat(buf, o, " verdict=FAIL\x00" as *u8) } 129 buf[o] = 0 as u8 130 fa_appendz(WBG_LOG, buf, WBG_RECCAP) 131 // stdout mirror 132 sys_write(1, " \x00" as *u8, 2) 133 var n: i64 = 0; while name[n] != (0 as u8) { n = n + 1 } sys_write(1, name, n) 134 if pass == 1 { sys_write(1, " PASS\n\x00" as *u8, 6) } else { sys_write(1, " FAIL\n\x00" as *u8, 6) } 135 return 0 136} 137 138func main() -> i64 { 139 let epoch: i64 = sys_now_realtime_sec() 140 let pid: i64 = __syscall(39, 0, 0, 0, 0, 0, 0) 141 142 // ===== seed the HERMETIC complete store (idempotent / additive). ===== 143 wbg_seed_one(WBG_PREFIX, "ws:empires" as *u8, "E-A\tE-B\tE-C" as *u8) 144 wbg_seed_one(WBG_PREFIX, "ws:ids" as *u8, "B-1\tB-2\tB-3\tB-4" as *u8) 145 wbg_seed_one(WBG_PREFIX, "ws:B-1" as *u8, "B-1\tE-A\tDONE\t100\tmem\torgan\t-" as *u8) 146 wbg_seed_one(WBG_PREFIX, "ws:B-2" as *u8, "B-2\tE-A\tACTIVE\t200\tmem\torgan\t-" as *u8) 147 wbg_seed_one(WBG_PREFIX, "ws:B-3" as *u8, "B-3\tE-B\tBLOCKED\t300\tmem\torgan\t-" as *u8) 148 wbg_seed_one(WBG_PREFIX, "ws:B-4" as *u8, "B-4\tE-C\tDONE\t400\tmem\torgan\t-" as *u8) 149 150 // ===== seed the INCOMPLETE store (N3): ws:B2-LOST listed but never committed. ===== 151 wbg_seed_one(WBG_PREFIX2, "ws:empires" as *u8, "E-A\tE-B" as *u8) 152 wbg_seed_one(WBG_PREFIX2, "ws:ids" as *u8, "B2-1\tB2-LOST" as *u8) 153 wbg_seed_one(WBG_PREFIX2, "ws:B2-1" as *u8, "B2-1\tE-A\tDONE\t1\tmem\torgan\t-" as *u8) 154 // NOTE: ws:B2-LOST intentionally NOT seeded (the lost/torn segment). 155 156 let rows: *i64 = sys_mmap(8 * WB_MAXEMP * WB_ROWW) as *i64 157 let ec: *i64 = sys_mmap(16) as *i64 158 let sm: *i64 = sys_mmap(64) as *i64 159 160 // ---- T1: enumerate-exact (empires=3) ---- 161 let r1: i64 = wb_board_p(WBG_PREFIX, 0 as *u8, rows, WB_MAXEMP, ec, sm) 162 var t1: i64 = 0 163 if r1 == 3 { if ec[0] == 3 { t1 = 1 } } 164 165 // ---- T2: per-empire counts EXACT ---- 166 var t2: i64 = 0 167 let ba: i64 = wbg_find(rows, ec[0], "E-A" as *u8) 168 let bb: i64 = wbg_find(rows, ec[0], "E-B" as *u8) 169 let bc: i64 = wbg_find(rows, ec[0], "E-C" as *u8) 170 if ba >= 0 { if bb >= 0 { if bc >= 0 { 171 var ok2: i64 = 1 172 // E-A: streams=2 done=1 active=1 blocked=0 173 if rows[ba + 1] != 2 { ok2 = 0 } 174 if rows[ba + 2] != 1 { ok2 = 0 } 175 if rows[ba + 3] != 1 { ok2 = 0 } 176 if rows[ba + 4] != 0 { ok2 = 0 } 177 // E-B: streams=1 blocked=1 178 if rows[bb + 1] != 1 { ok2 = 0 } 179 if rows[bb + 4] != 1 { ok2 = 0 } 180 // E-C: streams=1 done=1 181 if rows[bc + 1] != 1 { ok2 = 0 } 182 if rows[bc + 2] != 1 { ok2 = 0 } 183 if ok2 == 1 { t2 = 1 } 184 } } } 185 186 // ---- T3: summary EXACT (total=4 done=2 active=1 blocked=1) ---- 187 var t3: i64 = 0 188 if sm[0] == 4 { if sm[1] == 2 { if sm[2] == 1 { if sm[3] == 1 { t3 = 1 } } } } 189 190 // ---- T4: clean-reflog overlay accepted (>=0) ---- 191 // build a unique /tmp good reflog with a few well-formed ledger_append records. 192 let goodp: *u8 = sys_mmap(256) 193 wbg_tmppath(goodp, "/tmp/wsb_good." as *u8, epoch, pid) 194 let g0: i64 = sys_openat_wr(goodp, 0x1a4) // truncate fresh 195 if g0 > 0 { sys_close(g0) } 196 var gi: i64 = 0 197 while gi < 5 { ledger_append(goodp, gi, 0, 1, 7, gi, gi); gi = gi + 1 } 198 let r4: i64 = wb_board_p(WBG_PREFIX, goodp, rows, WB_MAXEMP, ec, sm) 199 var t4: i64 = 0 200 if r4 >= 0 { t4 = 1 } 201 202 // ---- N1: unregistered-stream-absent ---- 203 // a never-registered id returns WS_UNKNOWN, AND "B-NEVER" appears in no empire row. 204 let pq: *i64 = sys_mmap(16) as *i64 205 let lq: *i64 = sys_mmap(16) as *i64 206 var n1: i64 = 0 207 if ws_get_p(WBG_PREFIX, "ws:B-NEVER" as *u8, pq, lq) == WS_UNKNOWN { 208 // re-render the board and scan every empire-id row for the token (must be 0 hits). 209 let r1b: i64 = wb_board_p(WBG_PREFIX, 0 as *u8, rows, WB_MAXEMP, ec, sm) 210 var hits: i64 = 0 211 var e: i64 = 0 212 while e < ec[0] { 213 let base: i64 = e * WB_ROWW 214 if wbg_streq(rows[base + 0] as *u8, "B-NEVER" as *u8) == 1 { hits = hits + 1 } 215 e = e + 1 216 } 217 if r1b == 3 { if hits == 0 { n1 = 1 } } 218 } 219 220 // ---- N2: torn/old reflog REJECTED (wb_board_p returns -3) ---- 221 let tornp: *u8 = sys_mmap(256) 222 wbg_tmppath(tornp, "/tmp/wsb_torn." as *u8, epoch, pid) 223 let t0: i64 = sys_openat_wr(tornp, 0x1a4) 224 if t0 > 0 { sys_close(t0) } 225 var ti: i64 = 0 226 while ti < 3 { ledger_append(tornp, ti, 0, 1, 7, ti, ti); ti = ti + 1 } 227 // append one raw line MISSING the " END" sentinel (the R2 gate's tamper idiom). 228 let tfd: i64 = sys_openat_append(tornp, 0x1a4) 229 if tfd > 0 { 230 sys_write(tfd, "WSX ws=0 old=1 new=2 actor=7 reason=9 ev=0 epoch=0 BROKEN\n\x00" as *u8, 58) 231 sys_close(tfd) 232 } 233 let rn2: i64 = wb_board_p(WBG_PREFIX, tornp, rows, WB_MAXEMP, ec, sm) 234 var n2: i64 = 0 235 if rn2 == WB_TORNREFLOG { n2 = 1 } // -3 : rejected (NOT silently rendered) 236 237 // ---- N3: incomplete-registry REJECTED (wb_board_p returns -1) ---- 238 let rn3: i64 = wb_board_p(WBG_PREFIX2, 0 as *u8, rows, WB_MAXEMP, ec, sm) 239 var n3: i64 = 0 240 if rn3 == WB_INCOMPLETE { n3 = 1 } // -1 : lost segment -> refuse 241 242 // ---- N4: detector-sees-difference (rn2 != r4 on contrasting reflog inputs) ---- 243 var n4: i64 = 0 244 if rn2 != r4 { if rn2 == WB_TORNREFLOG { if r4 >= 0 { n4 = 1 } } } 245 246 // ===== flat pass-tally ===== 247 var passes: i64 = 0 248 if t1 == 1 { passes = passes + 1 } 249 if t2 == 1 { passes = passes + 1 } 250 if t3 == 1 { passes = passes + 1 } 251 if t4 == 1 { passes = passes + 1 } 252 if n1 == 1 { passes = passes + 1 } 253 if n2 == 1 { passes = passes + 1 } 254 if n3 == 1 { passes = passes + 1 } 255 if n4 == 1 { passes = passes + 1 } 256 var green: i64 = 0 257 if passes == 8 { green = 1 } 258 259 sys_write(1, "WMS-M2 ws-board gate (derived view + 4 neg-controls)\n\x00" as *u8, 52) 260 wbg_row("T1-enumerate-exact \x00" as *u8, t1) 261 wbg_row("T2-per-empire-counts \x00" as *u8, t2) 262 wbg_row("T3-summary-exact \x00" as *u8, t3) 263 wbg_row("T4-clean-reflog-overlay \x00" as *u8, t4) 264 wbg_row("N1-unregistered-absent \x00" as *u8, n1) 265 wbg_row("N2-torn-reflog-rejected \x00" as *u8, n2) 266 wbg_row("N3-incomplete-rejected \x00" as *u8, n3) 267 wbg_row("N4-detector-sees-diff \x00" as *u8, n4) 268 269 // verdict line: one buffer, one locked atomic fa_appendz (eat-own-dogfood). 270 let vb: *u8 = sys_mmap(WBG_RECCAP + 16) 271 var o: i64 = 0 272 o = wbg_cat(vb, o, "WS-BOARD verdict=\x00" as *u8) 273 if green == 1 { o = wbg_cat(vb, o, "GREEN\x00" as *u8) } else { o = wbg_cat(vb, o, "RED\x00" as *u8) } 274 o = wbg_cat(vb, o, " passes=\x00" as *u8) 275 o = wbg_catn(vb, o, passes) 276 o = wbg_cat(vb, o, "/8 t1=\x00" as *u8); o = wbg_catn(vb, o, t1) 277 o = wbg_cat(vb, o, " t2=\x00" as *u8); o = wbg_catn(vb, o, t2) 278 o = wbg_cat(vb, o, " t3=\x00" as *u8); o = wbg_catn(vb, o, t3) 279 o = wbg_cat(vb, o, " t4=\x00" as *u8); o = wbg_catn(vb, o, t4) 280 o = wbg_cat(vb, o, " n1=\x00" as *u8); o = wbg_catn(vb, o, n1) 281 o = wbg_cat(vb, o, " n2=\x00" as *u8); o = wbg_catn(vb, o, n2) 282 o = wbg_cat(vb, o, " n3=\x00" as *u8); o = wbg_catn(vb, o, n3) 283 o = wbg_cat(vb, o, " n4=\x00" as *u8); o = wbg_catn(vb, o, n4) 284 if green == 0 { 285 o = wbg_cat(vb, o, " reason=\x00" as *u8) 286 if t1 == 0 { o = wbg_cat(vb, o, "enumerate-wrong \x00" as *u8) } 287 if t2 == 0 { o = wbg_cat(vb, o, "per-empire-counts-wrong \x00" as *u8) } 288 if t3 == 0 { o = wbg_cat(vb, o, "summary-wrong \x00" as *u8) } 289 if t4 == 0 { o = wbg_cat(vb, o, "clean-reflog-rejected \x00" as *u8) } 290 if n1 == 0 { o = wbg_cat(vb, o, "unregistered-appeared \x00" as *u8) } 291 if n2 == 0 { o = wbg_cat(vb, o, "torn-reflog-silently-rendered \x00" as *u8) } 292 if n3 == 0 { o = wbg_cat(vb, o, "incomplete-registry-rendered \x00" as *u8) } 293 if n4 == 0 { o = wbg_cat(vb, o, "detector-blind \x00" as *u8) } 294 } 295 o = wbg_cat(vb, o, " END\x00" as *u8) 296 vb[o] = 0 as u8 297 fa_appendz(WBG_LOG, vb, WBG_RECCAP) 298 // stdout verdict 299 sys_write(1, vb, o) 300 sys_write(1, "\n\x00" as *u8, 1) 301 302 if green == 1 { return 0 } 303 return 1 304}