code wiki / _hdl_build / nx_tex_gate.nx
nx_tex_gate.nx source
↩ module page · 309 lines · 16484 B
1// nx_tex_gate.nx -- REFEREE for the sovereign LaTeX-math -> MathML renderer (nx_tex).
2// Proves the renderer is CORRECT + produces WELL-FORMED MathML on a battery of hand-verified
3// Known-Answer Tests, and degrades GRACEFULLY on bad input. GREEN iff every check holds.
4//
5// CHECKS (all on REAL tx_render output, nothing hand-faked):
6// A. EXACT-MATHML KATs (11): each LaTeX input must render byte-for-byte to the hand-verified
7// expected MathML. Covers: x^2 (msup), \frac{a}{b} (mfrac), \sqrt{x+1} (msqrt over mrow),
8// \sum_{i=1}^{n} i (munderover, sum-style limits), \int_{0}^{\infty} x (msubsup, integral
9// limits + greek \infty), \alpha+\beta (greek entities), the BM25-style \frac{f}{f+k}
10// (the exact shape of the ranker the wiki search uses), a_i^2 (msubsup -- sub AND sup on one
11// base, NOT nested), a relations chain (\le \neq \approx as proper <mo> entities), and
12// \left( a+b \right) (fenced mrow).
13// B. WELL-FORMEDNESS: every KAT output passes a balanced-tag check (a tag stack: every opener
14// is closed by the matching closer in order, no underflow, empty at end) AND is wrapped in a
15// single <math>...</math>. This is asserted INDEPENDENTLY of the exact-string check, so even
16// a future renderer change that still produces balanced output is verified structurally.
17// C. NEGATIVE CONTROL (graceful degradation): an UNSUPPORTED command (\badcmd{x}) must NOT crash
18// and must yield balanced MathML containing an <merror> fallback (no malformed bytes). A
19// second teeth case proves the well-formedness checker has TEETH: a deliberately UNBALANCED
20// string (<math><mrow></math>) must be REJECTED by the checker (else greens are fabricatable).
21//
22// VERIFICATION DOCTRINE: MathML is a STANDARD (non-novel) format. The renderer is sovereign; rigor
23// comes from these hand-verified expected-MathML KATs + the balanced-tag well-formedness proof.
24// A 3rd-party structural cross-check (latexml / node+mathjax) is the NEXT rigor step -- this gate
25// probes for those tools and logs the cross-check as PENDING when (as here) none is runnable. We do
26// NOT claim a 3rd-party comparison was made. Evidence -> knowledge/status/tex_gate.log.
27// Sovereign: imports nx_tex + nx_framed_append + nx_syscalls. license_tier: ORIGINAL
28import "nx_tex.nx"
29import "nx_framed_append.nx"
30import "nx_syscalls.nx"
31
32const TG_LOG: *u8 = "knowledge/status/tex_gate.log"
33const TG_RECCAP: i64 = 1024
34const TG_OUT_CAP: i64 = 65536
35
36// ---- stdout helpers -----------------------------------------------------------
37func tg_w(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 }
38func tg_num(v: i64) -> i64 {
39 let bb: *u8 = sys_mmap(28); var m: i64 = v
40 if m < 0 { sys_write(1, "-" as *u8, 1); m = 0 - m }
41 let t: *u8 = sys_mmap(28); var k: i64 = 0
42 if m == 0 { t[0] = 48 as u8; k = 1 }
43 while m > 0 { t[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 }
44 var i: i64 = 0; while i < k { bb[i] = t[k - 1 - i]; i = i + 1 }
45 sys_write(1, bb, k); return 0
46}
47func tg_cat(dst: *u8, off: i64, s: *u8) -> i64 { var i: i64 = 0; while s[i] != 0 as u8 { dst[off + i] = s[i]; i = i + 1 } return off + i }
48func tg_catn(dst: *u8, off: i64, v: i64) -> i64 {
49 var m: i64 = v; var o: i64 = off
50 if m < 0 { m = 0 - m }
51 let t: *u8 = sys_mmap(28); var k: i64 = 0
52 if m == 0 { t[0] = 48 as u8; k = 1 }
53 while m > 0 { t[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 }
54 var i: i64 = 0; while i < k { dst[o + i] = t[k - 1 - i]; i = i + 1 }
55 return o + k
56}
57func tg_slen(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } return n }
58func tg_streq(a: *u8, b: *u8) -> i64 {
59 var i: i64 = 0
60 while 1 == 1 { let ca: u8 = a[i]; let cb: u8 = b[i]; if ca != cb { return 0 } if ca == (0 as u8) { return 1 } i = i + 1 }
61 return 0
62}
63
64// ---- ASCII codes used by the well-formedness checker --------------------------
65const C_LT: i64 = 60 // <
66const C_GT: i64 = 62 // >
67const C_SLASH: i64 = 47 // /
68const C_SP: i64 = 32 // space
69const C_NUL: i64 = 0
70
71// =============================================================================
72// well_formed: a balanced-tag checker over MathML. Walks tags; pushes the name of
73// each opening tag onto a stack; on a closing tag, pops and requires the name to
74// match; rejects on underflow or a mismatched name; requires an EMPTY stack at end
75// (everything closed). Tag NAME = bytes after '<' (or '</') up to the first space
76// or '>'. Numeric/character entities (&#x...;) are plain text and ignored. Returns
77// 1 (well-formed) or 0 (malformed). Bounded stack -> never spins.
78// =============================================================================
79const WF_STACK_MAX: i64 = 256
80const WF_NAME_MAX: i64 = 32
81func well_formed(s: *u8) -> i64 {
82 // stack of name pointers into a names arena (each name NUL-terminated)
83 let names: *u8 = sys_mmap(WF_STACK_MAX * WF_NAME_MAX)
84 let sp_stack: *i64 = sys_mmap(WF_STACK_MAX * 8) as *i64 // holds arena offsets
85 var sp: i64 = 0
86 var arena: i64 = 0
87 var i: i64 = 0
88 let n: i64 = tg_slen(s)
89 while i < n {
90 if s[i] == (C_LT as u8) {
91 var closing: i64 = 0
92 i = i + 1
93 if i < n { if s[i] == (C_SLASH as u8) { closing = 1; i = i + 1 } }
94 // read the tag name into a temp (up to '>' or space)
95 let nm: *u8 = sys_mmap(WF_NAME_MAX)
96 var k: i64 = 0
97 var go: i64 = 1
98 while go == 1 {
99 if i >= n { go = 0 } else {
100 let c: i64 = s[i] as i64
101 if c == C_GT { go = 0 } else {
102 if c == C_SP { go = 0 } else {
103 if k < WF_NAME_MAX - 1 { nm[k] = c as u8; k = k + 1 }
104 i = i + 1
105 }
106 }
107 }
108 }
109 nm[k] = 0 as u8
110 // advance past the rest of the tag to '>'
111 var g2: i64 = 1
112 while g2 == 1 {
113 if i >= n { g2 = 0 } else {
114 if s[i] == (C_GT as u8) { i = i + 1; g2 = 0 } else { i = i + 1 }
115 }
116 }
117 if closing == 0 {
118 // push name into arena + stack
119 if sp >= WF_STACK_MAX { return 0 } // overflow -> malformed (too deep)
120 var j: i64 = 0
121 let base: i64 = arena
122 while nm[j] != (0 as u8) { names[base + j] = nm[j]; j = j + 1 }
123 names[base + j] = 0 as u8
124 sp_stack[sp] = base
125 sp = sp + 1
126 arena = base + j + 1
127 } else {
128 if sp == 0 { return 0 } // underflow -> malformed
129 sp = sp - 1
130 let top: *u8 = (names as i64 + sp_stack[sp]) as *u8
131 if tg_streq(top, nm) == 0 { return 0 } // mismatched close -> malformed
132 }
133 } else { i = i + 1 }
134 }
135 if sp != 0 { return 0 } // unclosed tags -> malformed
136 return 1
137}
138
139// =============================================================================
140// one KAT row: render `latex`, compare EXACTLY to `expect`, AND require the output
141// to be well-formed. Logs + prints PASS/FAIL. Returns 1 on full pass.
142// =============================================================================
143func tg_kat(name: *u8, latex: *u8, expect: *u8) -> i64 {
144 let out: *u8 = sys_mmap(TG_OUT_CAP)
145 let nb: i64 = tx_render(latex, out)
146 var exact: i64 = 0
147 var wf: i64 = 0
148 if nb >= 0 {
149 if tg_streq(out, expect) == 1 { exact = 1 }
150 if well_formed(out) == 1 { wf = 1 }
151 }
152 var pass: i64 = 0
153 if exact == 1 { if wf == 1 { pass = 1 } }
154
155 // human line
156 tg_w(" "); tg_w(name)
157 if pass == 1 { tg_w(" PASS") } else { tg_w(" FAIL") }
158 tg_w(" (exact="); tg_num(exact); tg_w(" wf="); tg_num(wf); tg_w(")\n")
159 if pass == 0 {
160 tg_w(" in='"); tg_w(latex); tg_w("'\n")
161 tg_w(" got='"); if nb >= 0 { tg_w(out) } else { tg_w("<ERR>") } tg_w("'\n")
162 tg_w(" exp='"); tg_w(expect); tg_w("'\n")
163 }
164 // log line
165 let lb: *u8 = sys_mmap(TG_RECCAP + 64)
166 var o: i64 = 0
167 o = tg_cat(lb, o, "TGATE kat=" as *u8); o = tg_cat(lb, o, name)
168 if pass == 1 { o = tg_cat(lb, o, " verdict=PASS" as *u8) } else { o = tg_cat(lb, o, " verdict=FAIL" as *u8) }
169 o = tg_cat(lb, o, " exact=" as *u8); o = tg_catn(lb, o, exact)
170 o = tg_cat(lb, o, " wf=" as *u8); o = tg_catn(lb, o, wf)
171 lb[o] = 0 as u8
172 fa_appendz(TG_LOG, lb, TG_RECCAP)
173 return pass
174}
175
176func main() -> i64 {
177 tg_w("=== nx_tex_gate: LaTeX-math -> MathML KATs + well-formedness + graceful-degradation ===\n")
178 let m: *u8 = sys_mmap(64) // reusable scratch (unused placeholder)
179
180 var passes: i64 = 0
181 var total: i64 = 0
182
183 // ---- A. exact-MathML KATs (hand-verified expected strings) ----
184 // K1 superscript
185 total = total + 1
186 if tg_kat("K1-msup-x^2 \x00" as *u8,
187 "x^2" as *u8,
188 "<math xmlns=\"http://www.w3.org/1998/Math/MathML\" display=\"block\"><mrow><msup><mi>x</mi><mn>2</mn></msup></mrow></math>" as *u8) == 1 { passes = passes + 1 }
189 // K2 fraction
190 total = total + 1
191 if tg_kat("K2-mfrac-a/b \x00" as *u8,
192 "\\frac{a}{b}" as *u8,
193 "<math xmlns=\"http://www.w3.org/1998/Math/MathML\" display=\"block\"><mrow><mfrac><mi>a</mi><mi>b</mi></mfrac></mrow></math>" as *u8) == 1 { passes = passes + 1 }
194 // K3 sqrt over a sum
195 total = total + 1
196 if tg_kat("K3-msqrt-x+1 \x00" as *u8,
197 "\\sqrt{x+1}" as *u8,
198 "<math xmlns=\"http://www.w3.org/1998/Math/MathML\" display=\"block\"><mrow><msqrt><mrow><mi>x</mi><mo>+</mo><mn>1</mn></mrow></msqrt></mrow></math>" as *u8) == 1 { passes = passes + 1 }
199 // K4 summation with both limits (munderover)
200 total = total + 1
201 if tg_kat("K4-munderover-sum \x00" as *u8,
202 "\\sum_{i=1}^{n} i" as *u8,
203 "<math xmlns=\"http://www.w3.org/1998/Math/MathML\" display=\"block\"><mrow><munderover><mo>∑</mo><mrow><mi>i</mi><mo>=</mo><mn>1</mn></mrow><mi>n</mi></munderover><mi>i</mi></mrow></math>" as *u8) == 1 { passes = passes + 1 }
204 // K5 integral with both limits (msubsup) + \infty
205 total = total + 1
206 if tg_kat("K5-msubsup-int-infty \x00" as *u8,
207 "\\int_{0}^{\\infty} x" as *u8,
208 "<math xmlns=\"http://www.w3.org/1998/Math/MathML\" display=\"block\"><mrow><msubsup><mo>∫</mo><mn>0</mn><mi>∞</mi></msubsup><mi>x</mi></mrow></math>" as *u8) == 1 { passes = passes + 1 }
209 // K6 greek
210 total = total + 1
211 if tg_kat("K6-greek-alpha+beta \x00" as *u8,
212 "\\alpha + \\beta" as *u8,
213 "<math xmlns=\"http://www.w3.org/1998/Math/MathML\" display=\"block\"><mrow><mi>α</mi><mo>+</mo><mi>β</mi></mrow></math>" as *u8) == 1 { passes = passes + 1 }
214 // K7 BM25-style fraction f/(f+k) -- the exact shape the wiki ranker uses
215 total = total + 1
216 if tg_kat("K7-bm25-frac-f/(f+k) \x00" as *u8,
217 "\\frac{f}{f + k}" as *u8,
218 "<math xmlns=\"http://www.w3.org/1998/Math/MathML\" display=\"block\"><mrow><mfrac><mi>f</mi><mrow><mi>f</mi><mo>+</mo><mi>k</mi></mrow></mfrac></mrow></math>" as *u8) == 1 { passes = passes + 1 }
219 // K8 sub AND sup on one base -> msubsup (NOT nested)
220 total = total + 1
221 if tg_kat("K8-msubsup-a_i^2 \x00" as *u8,
222 "a_i^2" as *u8,
223 "<math xmlns=\"http://www.w3.org/1998/Math/MathML\" display=\"block\"><mrow><msubsup><mi>a</mi><mi>i</mi><mn>2</mn></msubsup></mrow></math>" as *u8) == 1 { passes = passes + 1 }
224 // K9 relations chain (proper mo entities)
225 total = total + 1
226 if tg_kat("K9-relations-le-neq-approx \x00" as *u8,
227 "x \\le y \\neq z \\approx w" as *u8,
228 "<math xmlns=\"http://www.w3.org/1998/Math/MathML\" display=\"block\"><mrow><mi>x</mi><mo>≤</mo><mi>y</mi><mo>≠</mo><mi>z</mi><mo>≈</mo><mi>w</mi></mrow></math>" as *u8) == 1 { passes = passes + 1 }
229 // K10 fenced mrow \left( ... \right)
230 total = total + 1
231 if tg_kat("K10-left-right-fence \x00" as *u8,
232 "\\left( a + b \\right)" as *u8,
233 "<math xmlns=\"http://www.w3.org/1998/Math/MathML\" display=\"block\"><mrow><mrow><mo>(</mo><mi>a</mi><mo>+</mo><mi>b</mi><mo>)</mo></mrow></mrow></math>" as *u8) == 1 { passes = passes + 1 }
234 // K11 unsupported command degrades to <merror> (still exact + well-formed)
235 total = total + 1
236 if tg_kat("K11-merror-badcmd \x00" as *u8,
237 "\\badcmd{x}" as *u8,
238 "<math xmlns=\"http://www.w3.org/1998/Math/MathML\" display=\"block\"><mrow><merror><mtext>\\badcmd</mtext></merror><mi>x</mi></mrow></math>" as *u8) == 1 { passes = passes + 1 }
239
240 // ---- C. graceful-degradation teeth (beyond the K11 exact check) ----
241 // C1: the bad-command output must contain an <merror> AND be well-formed (no crash, no
242 // malformed bytes). We re-render and check structurally (independent of K11's exact match).
243 total = total + 1
244 let bo: *u8 = sys_mmap(TG_OUT_CAP)
245 let bn: i64 = tx_render("\\nonsense_{??}^{##} + 7" as *u8, bo) // unknown cmd + odd scripts
246 var c1: i64 = 0
247 if bn >= 0 { if well_formed(bo) == 1 { c1 = 1 } }
248 // require an <merror> substring (graceful fallback present)
249 var has_err: i64 = 0
250 var i: i64 = 0
251 let bl: i64 = tg_slen(bo)
252 while i + 7 < bl {
253 if bo[i] == (60 as u8) { if bo[i+1] == (109 as u8) { if bo[i+2] == (101 as u8) { if bo[i+3] == (114 as u8) { if bo[i+4] == (114 as u8) { if bo[i+5] == (111 as u8) { if bo[i+6] == (114 as u8) { has_err = 1 } } } } } } }
254 i = i + 1
255 }
256 var c1pass: i64 = 0
257 if c1 == 1 { if has_err == 1 { c1pass = 1 } }
258 if c1pass == 1 { passes = passes + 1 }
259 tg_w(" C1-graceful-merror+wf "); if c1pass == 1 { tg_w("PASS") } else { tg_w("FAIL") }
260 tg_w(" (wf="); tg_num(c1); tg_w(" merror="); tg_num(has_err); tg_w(")\n")
261
262 // C2: the well-formedness checker must REJECT a deliberately UNBALANCED string (teeth: greens
263 // can't be fabricated). <math><mrow></math> is missing a </mrow> -> must be malformed.
264 total = total + 1
265 var c2pass: i64 = 0
266 if well_formed("<math><mrow></math>" as *u8) == 0 {
267 if well_formed("<math></mrow></math>" as *u8) == 0 { // stray close -> underflow
268 if well_formed("<math><mrow></mrow></math>" as *u8) == 1 { // sanity: balanced -> accepted
269 c2pass = 1
270 }
271 }
272 }
273 if c2pass == 1 { passes = passes + 1 }
274 tg_w(" C2-wf-checker-has-teeth "); if c2pass == 1 { tg_w("PASS") } else { tg_w("FAIL") }
275 tg_w("\n")
276
277 // ---- B summary already folded into each KAT (wf asserted per row) ----
278
279 // ---- 3rd-party reference cross-check: probe + log PENDING (none runnable here) ----
280 // (Doctrine: MathML is a standard; the next rigor step is a structural compare vs latexml or
281 // node+mathjax. Neither is installed in this environment -> we log PENDING, do NOT claim it.)
282 tg_w(" 3rd-party-cross-check: PENDING (no latexml/node in env; KAT+well-formedness only)\n")
283 let pb: *u8 = sys_mmap(TG_RECCAP)
284 var po: i64 = 0
285 po = tg_cat(pb, po, "TGATE xref=PENDING reason=no-latexml-no-node-in-env method=hand-verified-KAT+balanced-tags\x00" as *u8)
286 pb[po] = 0 as u8
287 fa_appendz(TG_LOG, pb, TG_RECCAP)
288
289 var green: i64 = 0
290 if passes == total { green = 1 }
291
292 // verdict line (stdout + log)
293 tg_w("nx_tex_gate verdict="); if green == 1 { tg_w("GREEN") } else { tg_w("RED") }
294 tg_w(" passes="); tg_num(passes); tg_w("/"); tg_num(total); tg_w("\n")
295
296 let vb: *u8 = sys_mmap(TG_RECCAP)
297 var vo: i64 = 0
298 vo = tg_cat(vb, vo, "TEX-RENDER verdict=" as *u8)
299 if green == 1 { vo = tg_cat(vb, vo, "GREEN" as *u8) } else { vo = tg_cat(vb, vo, "RED" as *u8) }
300 vo = tg_cat(vb, vo, " passes=" as *u8); vo = tg_catn(vb, vo, passes)
301 vo = tg_cat(vb, vo, "/" as *u8); vo = tg_catn(vb, vo, total)
302 vo = tg_cat(vb, vo, " xref=PENDING END" as *u8)
303 vb[vo] = 0 as u8
304 fa_appendz(TG_LOG, vb, TG_RECCAP)
305
306 if green == 1 { sys_exit(0); return 0 }
307 sys_exit(1)
308 return 1
309}