code wiki / _hdl_build / nx_ws_board_html_gate.nx
nx_ws_board_html_gate.nx source
↩ module page · 332 lines · 15439 B
1// nx_ws_board_html_gate.nx -- THE REFEREE for WMS rung M2.5 (the viewable HTML board).
2//
3// Proves nx_ws_board_html EMITS a correct, derive-from-truth HTML view of the M2 board,
4// AND that it is NEVER silently wrong -- the negative controls prove the emitter refuses
5// rather than rendering a wrong table (no-false-green). Every assertion is over the REAL
6// EMITTED BYTES on disk (the wheeler flip: the artifact is the verified OUTPUT), not over
7// claims. The same HERMETIC fixtures the M2 gate uses are re-seeded idempotently here.
8//
9// HERMETIC fixtures (controlled, NOT production claims):
10// prefix wsboard- : ws:empires=E-A,E-B,E-C ; ids B-1..B-4 (4 complete streams)
11// B-1 E-A DONE / B-2 E-A ACTIVE / B-3 E-B BLOCKED / B-4 E-C DONE
12// prefix wsboard2- : ids list B2-1 + B2-LOST, but ws:B2-LOST is NEVER committed.
13//
14// POSITIVE (all must hold for GREEN):
15// T1 emit-table : wbh_emit_p(wsboard-, refpath=0) returns WBH_TABLE(1) and
16// status[1]==3 empires status[2]==4 total.
17// T2 head-well-formed : emitted file begins with "<!DOCTYPE html>" and contains
18// the <table> open and the </html> close (a real document).
19// T3 per-empire-rows : the bytes contain the EXACT per-empire cells for all three
20// empires (E-A 2/1/1/0, E-B 1/0/0/1, E-C 1/1/0/0) as the
21// SAME numbers the M2 board derives -- the HTML cannot lie.
22// T4 summary-row : the bytes contain the SUMMARY footer "<th>4</th>" total.
23//
24// NEGATIVE CONTROLS (a GREEN with no working neg-control is INVALID):
25// N1 incomplete->REFUSED : wbh_emit_p(wsboard2-, 0) returns WBH_REFUSED(2), the bytes
26// contain the "BOARD REFUSED" banner AND contain NO <table>
27// (a wrong table was NOT silently emitted). TABLE => RED.
28// N2 torn-reflog->REFUSED: wbh_emit_p(wsboard-, refpath=torn) returns WBH_REFUSED(2)
29// with a REFUSED banner and NO <table>. Same idiom as the M2
30// gate's torn reflog (good records + one line MISSING " END").
31// N3 detector-sees-diff : the GOOD emit (T1) contains "<table>" and the REFUSED emit
32// (N1) does NOT -- proving the byte detector is not a constant
33// (it actually distinguishes a table page from a banner page).
34// N4 unregistered-absent : the token "B-NEVER" (a never-registered stream) appears in
35// ZERO bytes of the good emitted HTML.
36//
37// GREEN only if T1..T4 AND N1..N4 all hold. Evidence rows + verdict -> ws_board_html_gate.log
38// via the MANDATORY fa_appendz one-buffer-one-locked-write discipline (eat-own-dogfood);
39// fixture emits use UNIQUE epoch+pid /tmp paths so concurrent gate runs never collide.
40// Exit 0 GREEN / 1 RED. Sovereign: WMS/HAL stack + nx_syscalls only (no gcc). license_tier: ORIGINAL
41import "nx_ws_board_html.nx"
42import "nx_ws_board.nx"
43import "nx_workstream_store.nx"
44import "nx_ws_ledger.nx"
45import "nx_framed_append.nx"
46import "nx_seg_store.nx"
47import "nx_syscalls.nx"
48
49const WBHG_LOG: *u8 = "knowledge/status/ws_board_html_gate.log"
50const WBHG_PREFIX: *u8 = "knowledge/store/wsboard-"
51const WBHG_PREFIX2: *u8 = "knowledge/store/wsboard2-"
52const WBHG_RECCAP: i64 = 512
53const WBHG_RDCAP: i64 = 65536
54
55func wbhg_len(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } return n }
56
57func wbhg_streq(a: *u8, b: *u8) -> i64 {
58 var i: i64 = 0
59 while a[i] != (0 as u8) { if a[i] != b[i] { return 0 } i = i + 1 }
60 if b[i] != (0 as u8) { return 0 }
61 return 1
62}
63
64// 1 if store value for key under `prefix` byte-equals val (idempotent seed helper).
65func wbhg_streq_store(prefix: *u8, key: *u8, val: *u8) -> i64 {
66 let pq: *i64 = sys_mmap(16) as *i64
67 let lq: *i64 = sys_mmap(16) as *i64
68 if ss_get(prefix, key, pq, lq) != 1 { return 0 }
69 let b: *u8 = pq[0] as *u8
70 let n: i64 = lq[0]
71 let vl: i64 = wbhg_len(val)
72 if n != vl { return 0 }
73 var i: i64 = 0
74 while i < n { if b[i] != val[i] { return 0 } i = i + 1 }
75 return 1
76}
77
78// commit one (key,val) into `prefix`, idempotent (same idiom as the M2 gate).
79func wbhg_seed_one(prefix: *u8, key: *u8, val: *u8) -> i64 {
80 if wbhg_streq_store(prefix, key, val) == 1 { return 1 }
81 let w: *i64 = ss_begin()
82 ss_add(w, 1, key, val, wbhg_len(val))
83 let segid: i64 = ws_seg_next(prefix)
84 return ss_commit(prefix, w, segid)
85}
86
87// read a whole file into buf (bounded); returns byte count or negative.
88func wbhg_readfile(path: *u8, buf: *u8, cap: i64) -> i64 {
89 let fd: i64 = sys_openat_rd(path)
90 if fd < 0 { return 0 - 1 }
91 var n: i64 = 0
92 var go: i64 = 1
93 while go == 1 {
94 let r: i64 = sys_read(fd, ((buf as i64) + n) as *u8, cap - n)
95 if r <= 0 { go = 0 } else { n = n + r }
96 if n >= cap { go = 0 }
97 }
98 sys_close(fd)
99 return n
100}
101
102// substring search: 1 if needle (NUL-term) occurs in buf[0..n), else 0.
103func wbhg_contains(buf: *u8, n: i64, needle: *u8) -> i64 {
104 let nl: i64 = wbhg_len(needle)
105 if nl == 0 { return 1 }
106 if nl > n { return 0 }
107 var i: i64 = 0
108 while i <= n - nl {
109 var j: i64 = 0
110 var ok: i64 = 1
111 while j < nl { if buf[i + j] != needle[j] { ok = 0; j = nl } else { j = j + 1 } }
112 if ok == 1 { return 1 }
113 i = i + 1
114 }
115 return 0
116}
117
118// decimal/string builders for unique /tmp paths.
119func wbhg_catn(dst: *u8, off: i64, v: i64) -> i64 {
120 var m: i64 = v; var o: i64 = off
121 if m < 0 { m = 0 - m }
122 let t: *u8 = sys_mmap(28); var k: i64 = 0
123 if m == 0 { t[0] = 48 as u8; k = 1 }
124 while m > 0 { t[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 }
125 var i: i64 = 0
126 while i < k { dst[o + i] = t[k - 1 - i]; i = i + 1 }
127 return o + k
128}
129func wbhg_cat(dst: *u8, off: i64, s: *u8) -> i64 {
130 var i: i64 = 0
131 while s[i] != (0 as u8) { dst[off + i] = s[i]; i = i + 1 }
132 return off + i
133}
134func wbhg_tmppath(out: *u8, stem: *u8, epoch: i64, pid: i64, ext: *u8) -> i64 {
135 var o: i64 = 0
136 o = wbhg_cat(out, o, stem)
137 o = wbhg_catn(out, o, epoch)
138 o = wbhg_cat(out, o, "." as *u8)
139 o = wbhg_catn(out, o, pid)
140 o = wbhg_cat(out, o, ext)
141 out[o] = 0 as u8
142 return o
143}
144
145// MANDATORY WRITE DISCIPLINE: one PASS/FAIL row in one buffer, ONE locked fa_appendz.
146func wbhg_row(name: *u8, pass: i64) -> i64 {
147 let buf: *u8 = sys_mmap(WBHG_RECCAP + 16)
148 var o: i64 = 0
149 o = wbhg_cat(buf, o, "WSBH row=\x00" as *u8)
150 o = wbhg_cat(buf, o, name)
151 if pass == 1 { o = wbhg_cat(buf, o, " verdict=PASS\x00" as *u8) } else { o = wbhg_cat(buf, o, " verdict=FAIL\x00" as *u8) }
152 buf[o] = 0 as u8
153 fa_appendz(WBHG_LOG, buf, WBHG_RECCAP)
154 sys_write(1, " \x00" as *u8, 2)
155 var n: i64 = 0; while name[n] != (0 as u8) { n = n + 1 } sys_write(1, name, n)
156 if pass == 1 { sys_write(1, " PASS\n\x00" as *u8, 6) } else { sys_write(1, " FAIL\n\x00" as *u8, 6) }
157 return 0
158}
159
160func main() -> i64 {
161 let epoch: i64 = sys_now_realtime_sec()
162 let pid: i64 = __syscall(39, 0, 0, 0, 0, 0, 0)
163
164 // ===== seed the HERMETIC stores (idempotent / additive; same as the M2 gate). =====
165 wbhg_seed_one(WBHG_PREFIX, "ws:empires" as *u8, "E-A\tE-B\tE-C" as *u8)
166 wbhg_seed_one(WBHG_PREFIX, "ws:ids" as *u8, "B-1\tB-2\tB-3\tB-4" as *u8)
167 wbhg_seed_one(WBHG_PREFIX, "ws:B-1" as *u8, "B-1\tE-A\tDONE\t100\tmem\torgan\t-" as *u8)
168 wbhg_seed_one(WBHG_PREFIX, "ws:B-2" as *u8, "B-2\tE-A\tACTIVE\t200\tmem\torgan\t-" as *u8)
169 wbhg_seed_one(WBHG_PREFIX, "ws:B-3" as *u8, "B-3\tE-B\tBLOCKED\t300\tmem\torgan\t-" as *u8)
170 wbhg_seed_one(WBHG_PREFIX, "ws:B-4" as *u8, "B-4\tE-C\tDONE\t400\tmem\torgan\t-" as *u8)
171 wbhg_seed_one(WBHG_PREFIX2, "ws:empires" as *u8, "E-A\tE-B" as *u8)
172 wbhg_seed_one(WBHG_PREFIX2, "ws:ids" as *u8, "B2-1\tB2-LOST" as *u8)
173 wbhg_seed_one(WBHG_PREFIX2, "ws:B2-1" as *u8, "B2-1\tE-A\tDONE\t1\tmem\torgan\t-" as *u8)
174 // ws:B2-LOST intentionally NOT seeded (the lost segment -> board must REFUSE).
175
176 let st: *i64 = sys_mmap(64) as *i64
177 let st2: *i64 = sys_mmap(64) as *i64
178 let rd: *u8 = sys_mmap(WBHG_RDCAP)
179
180 // unique /tmp output paths so concurrent gate runs never collide.
181 let goodhtml: *u8 = sys_mmap(256)
182 wbhg_tmppath(goodhtml, "/tmp/wsbh_good." as *u8, epoch, pid, ".html" as *u8)
183 let badhtml: *u8 = sys_mmap(256)
184 wbhg_tmppath(badhtml, "/tmp/wsbh_bad." as *u8, epoch, pid, ".html" as *u8)
185 let tornhtml: *u8 = sys_mmap(256)
186 wbhg_tmppath(tornhtml, "/tmp/wsbh_torn." as *u8, epoch, pid, ".html" as *u8)
187
188 // ---- T1: emit a real TABLE for the complete store. ----
189 let r1: i64 = wbh_emit_p(WBHG_PREFIX, 0 as *u8, goodhtml, st)
190 var t1: i64 = 0
191 if r1 == WBH_TABLE { if st[1] == 3 { if st[2] == 4 { t1 = 1 } } }
192
193 // read the good emitted bytes back for byte-level assertions.
194 let gn: i64 = wbhg_readfile(goodhtml, rd, WBHG_RDCAP)
195
196 // ---- T2: head well-formed (real HTML document). ----
197 var t2: i64 = 0
198 if gn > 0 {
199 if wbhg_contains(rd, gn, "<!DOCTYPE html>" as *u8) == 1 {
200 if wbhg_contains(rd, gn, "<table>" as *u8) == 1 {
201 if wbhg_contains(rd, gn, "</html>" as *u8) == 1 { t2 = 1 }
202 }
203 }
204 }
205
206 // ---- T3: per-empire rows EXACT (derive-from-truth cells). ----
207 // E-A row: <td>E-A</td><td>2</td><td class="done">1</td><td class="active">1</td><td class="blocked">0</td>
208 var t3: i64 = 0
209 if gn > 0 {
210 var ok3: i64 = 1
211 if wbhg_contains(rd, gn, "<td>E-A</td><td>2</td><td class=\"done\">1</td><td class=\"active\">1</td><td class=\"blocked\">0</td>" as *u8) == 0 { ok3 = 0 }
212 if wbhg_contains(rd, gn, "<td>E-B</td><td>1</td><td class=\"done\">0</td><td class=\"active\">0</td><td class=\"blocked\">1</td>" as *u8) == 0 { ok3 = 0 }
213 if wbhg_contains(rd, gn, "<td>E-C</td><td>1</td><td class=\"done\">1</td><td class=\"active\">0</td><td class=\"blocked\">0</td>" as *u8) == 0 { ok3 = 0 }
214 if ok3 == 1 { t3 = 1 }
215 }
216
217 // ---- T4: summary footer row (total=4). ----
218 var t4: i64 = 0
219 if gn > 0 {
220 if wbhg_contains(rd, gn, "<tr><th>SUMMARY</th><th>4</th>" as *u8) == 1 { t4 = 1 }
221 }
222
223 // ---- N1: incomplete registry -> REFUSED banner, NO table. ----
224 let rn1: i64 = wbh_emit_p(WBHG_PREFIX2, 0 as *u8, badhtml, st2)
225 var n1: i64 = 0
226 if rn1 == WBH_REFUSED {
227 let bn: i64 = wbhg_readfile(badhtml, rd, WBHG_RDCAP)
228 if bn > 0 {
229 if wbhg_contains(rd, bn, "BOARD REFUSED" as *u8) == 1 {
230 if wbhg_contains(rd, bn, "<table>" as *u8) == 0 { n1 = 1 }
231 }
232 }
233 }
234
235 // ---- N2: torn reflog -> REFUSED banner, NO table. ----
236 // build a torn reflog: good records + one raw line MISSING the " END" sentinel.
237 let tornlog: *u8 = sys_mmap(256)
238 wbhg_tmppath(tornlog, "/tmp/wsbh_tornlog." as *u8, epoch, pid, ".log" as *u8)
239 let t0: i64 = sys_openat_wr(tornlog, 0x1a4)
240 if t0 > 0 { sys_close(t0) }
241 var ti: i64 = 0
242 while ti < 3 { ledger_append(tornlog, ti, 0, 1, 7, ti, ti); ti = ti + 1 }
243 let tfd: i64 = sys_openat_append(tornlog, 0x1a4)
244 if tfd > 0 {
245 sys_write(tfd, "WSX ws=0 old=1 new=2 actor=7 reason=9 ev=0 epoch=0 BROKEN\n\x00" as *u8, 58)
246 sys_close(tfd)
247 }
248 let rn2: i64 = wbh_emit_p(WBHG_PREFIX, tornlog, tornhtml, st2)
249 var n2: i64 = 0
250 if rn2 == WBH_REFUSED {
251 let tn: i64 = wbhg_readfile(tornhtml, rd, WBHG_RDCAP)
252 if tn > 0 {
253 if wbhg_contains(rd, tn, "BOARD REFUSED" as *u8) == 1 {
254 if wbhg_contains(rd, tn, "<table>" as *u8) == 0 { n2 = 1 }
255 }
256 }
257 }
258
259 // ---- N3: detector-sees-diff (good has <table>, refused does not). ----
260 // re-read good + bad, confirm the byte detector actually distinguishes them.
261 var n3: i64 = 0
262 let gn2: i64 = wbhg_readfile(goodhtml, rd, WBHG_RDCAP)
263 var good_has_table: i64 = 0
264 if gn2 > 0 { good_has_table = wbhg_contains(rd, gn2, "<table>" as *u8) }
265 let bn2: i64 = wbhg_readfile(badhtml, rd, WBHG_RDCAP)
266 var bad_has_table: i64 = 0
267 if bn2 > 0 { bad_has_table = wbhg_contains(rd, bn2, "<table>" as *u8) }
268 if good_has_table == 1 { if bad_has_table == 0 { n3 = 1 } }
269
270 // ---- N4: unregistered stream token absent from good HTML. ----
271 var n4: i64 = 0
272 let gn3: i64 = wbhg_readfile(goodhtml, rd, WBHG_RDCAP)
273 if gn3 > 0 { if wbhg_contains(rd, gn3, "B-NEVER" as *u8) == 0 { n4 = 1 } }
274
275 // ===== flat pass-tally. =====
276 var passes: i64 = 0
277 if t1 == 1 { passes = passes + 1 }
278 if t2 == 1 { passes = passes + 1 }
279 if t3 == 1 { passes = passes + 1 }
280 if t4 == 1 { passes = passes + 1 }
281 if n1 == 1 { passes = passes + 1 }
282 if n2 == 1 { passes = passes + 1 }
283 if n3 == 1 { passes = passes + 1 }
284 if n4 == 1 { passes = passes + 1 }
285 var green: i64 = 0
286 if passes == 8 { green = 1 }
287
288 sys_write(1, "WMS-M2.5 ws-board-html gate (Nishi-emitted view + 4 neg-controls)\n\x00" as *u8, 65)
289 wbhg_row("T1-emit-table \x00" as *u8, t1)
290 wbhg_row("T2-head-well-formed \x00" as *u8, t2)
291 wbhg_row("T3-per-empire-rows \x00" as *u8, t3)
292 wbhg_row("T4-summary-row \x00" as *u8, t4)
293 wbhg_row("N1-incomplete-refused \x00" as *u8, n1)
294 wbhg_row("N2-torn-reflog-refused \x00" as *u8, n2)
295 wbhg_row("N3-detector-sees-diff \x00" as *u8, n3)
296 wbhg_row("N4-unregistered-absent \x00" as *u8, n4)
297
298 // verdict line: one buffer, one locked atomic fa_appendz (eat-own-dogfood).
299 let vb: *u8 = sys_mmap(WBHG_RECCAP + 16)
300 var o: i64 = 0
301 o = wbhg_cat(vb, o, "WS-BOARD-HTML verdict=\x00" as *u8)
302 if green == 1 { o = wbhg_cat(vb, o, "GREEN\x00" as *u8) } else { o = wbhg_cat(vb, o, "RED\x00" as *u8) }
303 o = wbhg_cat(vb, o, " passes=\x00" as *u8)
304 o = wbhg_catn(vb, o, passes)
305 o = wbhg_cat(vb, o, "/8 t1=\x00" as *u8); o = wbhg_catn(vb, o, t1)
306 o = wbhg_cat(vb, o, " t2=\x00" as *u8); o = wbhg_catn(vb, o, t2)
307 o = wbhg_cat(vb, o, " t3=\x00" as *u8); o = wbhg_catn(vb, o, t3)
308 o = wbhg_cat(vb, o, " t4=\x00" as *u8); o = wbhg_catn(vb, o, t4)
309 o = wbhg_cat(vb, o, " n1=\x00" as *u8); o = wbhg_catn(vb, o, n1)
310 o = wbhg_cat(vb, o, " n2=\x00" as *u8); o = wbhg_catn(vb, o, n2)
311 o = wbhg_cat(vb, o, " n3=\x00" as *u8); o = wbhg_catn(vb, o, n3)
312 o = wbhg_cat(vb, o, " n4=\x00" as *u8); o = wbhg_catn(vb, o, n4)
313 if green == 0 {
314 o = wbhg_cat(vb, o, " reason=\x00" as *u8)
315 if t1 == 0 { o = wbhg_cat(vb, o, "table-not-emitted \x00" as *u8) }
316 if t2 == 0 { o = wbhg_cat(vb, o, "head-malformed \x00" as *u8) }
317 if t3 == 0 { o = wbhg_cat(vb, o, "per-empire-rows-wrong \x00" as *u8) }
318 if t4 == 0 { o = wbhg_cat(vb, o, "summary-row-wrong \x00" as *u8) }
319 if n1 == 0 { o = wbhg_cat(vb, o, "incomplete-rendered-table \x00" as *u8) }
320 if n2 == 0 { o = wbhg_cat(vb, o, "torn-reflog-rendered-table \x00" as *u8) }
321 if n3 == 0 { o = wbhg_cat(vb, o, "detector-blind \x00" as *u8) }
322 if n4 == 0 { o = wbhg_cat(vb, o, "unregistered-appeared \x00" as *u8) }
323 }
324 o = wbhg_cat(vb, o, " END\x00" as *u8)
325 vb[o] = 0 as u8
326 fa_appendz(WBHG_LOG, vb, WBHG_RECCAP)
327 sys_write(1, vb, o)
328 sys_write(1, "\n\x00" as *u8, 1)
329
330 if green == 1 { return 0 }
331 return 1
332}