code wiki / _hdl_build / nx_ws_board_html_gate.nx
nx_ws_board_html_gate.nx
buildroot/runtime/_hdl_build/nx_ws_board_html_gate.nx
about
nx_ws_board_html_gate.nx -- THE REFEREE for WMS rung M2.5 (the viewable HTML board).
Proves nx_ws_board_html EMITS a correct, derive-from-truth HTML view of the M2 board,
AND that it is NEVER silently wrong -- the negative controls prove the emitter refuses
rather than rendering a wrong table (no-false-green). Every assertion is over the REAL
EMITTED BYTES on disk (the wheeler flip: the artifact is the verified OUTPUT), not over
claims. The same HERMETIC fixtures the M2 gate uses are re-seeded idempotently here.
HERMETIC fixtures (controlled, NOT production claims):
prefix wsboard- : ws:empires=E-A,E-B,E-C ; ids B-1..B-4 (4 complete streams)
B-1 E-A DONE / B-2 E-A ACTIVE / B-3 E-B BLOCKED / B-4 E-C DONE
prefix wsboard2- : ids list B2-1 + B2-LOST, but ws:B2-LOST is NEVER committed.
POSITIVE (all must hold for GREEN):
T1 emit-table : wbh_emit_p(wsboard-, refpath=0) returns WBH_TABLE(1) and
status[1]==3 empires status[2]==4 total.
T2 head-well-formed : emitted file begins with "<!DOCTYPE html>" and contains
the <table> open and the </html> close (a real document).
T3 per-empire-rows : the bytes contain the EXACT per-empire cells for all three
empires (E-A 2/1/1/0, E-B 1/0/0/1, E-C 1/1/0/0) as the
SAME numbers the M2 board derives -- the HTML cannot lie.
T4 summary-row : the bytes contain the SUMMARY footer "<th>4</th>" total.
NEGATIVE CONTROLS (a GREEN with no working neg-control is INVALID):
N1 incomplete->REFUSED : wbh_emit_p(wsboard2-, 0) returns WBH_REFUSED(2), the bytes
contain the "BOARD REFUSED" banner AND contain NO <table>
(a wrong table was NOT silently emitted). TABLE => RED.
N2 torn-reflog->REFUSED: wbh_emit_p(wsboard-, refpath=torn) returns WBH_REFUSED(2)
with a REFUSED banner and NO <table>. Same idiom as the M2
gate's torn reflog (good records + one line MISSING " END").
N3 detector-sees-diff : the GOOD emit (T1) contains "<table>" and the REFUSED emit
(N1) does NOT -- proving the byte detector is not a constant
(it actually distinguishes a table page from a banner page).
N4 unregistered-absent : the token "B-NEVER" (a never-registered stream) appears in
ZERO bytes of the good emitted HTML.
GREEN only if T1..T4 AND N1..N4 all hold. Evidence rows + verdict -> ws_board_html_gate.log
via the MANDATORY fa_appendz one-buffer-one-locked-write discipline (eat-own-dogfood);
fixture emits use UNIQUE epoch+pid /tmp paths so concurrent gate runs never collide.
Exit 0 GREEN / 1 RED. Sovereign: WMS/HAL stack + nx_syscalls only (no gcc). license_tier: ORIGINAL
dependencies 7 imports · 0 importers
imports: nx_ws_board_html.nxnx_ws_board.nxnx_workstream_store.nxnx_ws_ledger.nxnx_framed_append.nxnx_seg_store.nxnx_syscalls.nx
imported by: nobody (leaf or entry point)
call flow from main pre-order; caps 40 nodes / depth 6 declared; ↻ = already shown
structs
| none |
consts
| 49 | const WBHG_LOG: *u8 = "knowledge/status/ws_board_html_gate.log" |
| 50 | const WBHG_PREFIX: *u8 = "knowledge/store/wsboard-" |
| 51 | const WBHG_PREFIX2: *u8 = "knowledge/store/wsboard2-" |
| 52 | const WBHG_RECCAP: i64 = 512 |
| 53 | const WBHG_RDCAP: i64 = 65536 |
functions
| 55 | func wbhg_len(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } return n } |
| 57 | func wbhg_streq(a: *u8, b: *u8) -> i64 |
| 65 | func wbhg_streq_store(prefix: *u8, key: *u8, val: *u8) -> i64 |
| 79 | func wbhg_seed_one(prefix: *u8, key: *u8, val: *u8) -> i64 |
| 88 | func wbhg_readfile(path: *u8, buf: *u8, cap: i64) -> i64 |
| 103 | func wbhg_contains(buf: *u8, n: i64, needle: *u8) -> i64 |
| 119 | func wbhg_catn(dst: *u8, off: i64, v: i64) -> i64 |
| 129 | func wbhg_cat(dst: *u8, off: i64, s: *u8) -> i64 |
| 134 | func wbhg_tmppath(out: *u8, stem: *u8, epoch: i64, pid: i64, ext: *u8) -> i64 |
| 146 | func wbhg_row(name: *u8, pass: i64) -> i64 |
| 160 | func main() -> i64 |