code wiki / _hdl_build / nx_symjudge.nx
nx_symjudge.nx source
↩ module page · 655 lines · 29026 B
1// nx_symjudge.nx -- THE SYMBOLIC JUDGE (autonomous-builder lane, 2026-07-20). The non-LLM half of
2// the neuro-symbolic builder loop: a maker's patch that PASSES the baked tests can still be wrong on
3// every untested input (the overfit-patch class) or crash on edge inputs. This organ judges ONE pure
4// integer function against a DATA-DRIVEN property contract (a symprop- plane row, store-law: no flat
5// files) by GENERATING a sweep harness, compiling it fresh with the sovereign toolchain, running it:
6// - domain fits budget -> EXHAUSTIVE sweep = bounded-model-check style proof over the whole domain
7// - larger -> deterministic stride sample (never random-flaky; step derived from budget)
8// - crash/SIGFPE/no-output -> RED (the fuzz-crash finding class, sovereign + deterministic)
9// Property NAMES are plane data (odd,even,fix0,lin2,idem,mono,nocrash,range:a:b,comm,idem2);
10// checker bodies are code here; domains/budget live in the row (rule 11: no magic numbers).
11// symprop- row schema (7 col, tab): fn arity lo hi budget props note
12// Verdict: SYMJUDGE fn=<f> mode=EXH|SAMP checked=<n> viol=<v> verdict=GREEN|RED [reason=...]
13// exit: 0 GREEN | 1 property violation | 2 crash-or-nocompile | 3 refused (fail-closed)
14// argv: <srcfile> <fn> <planeprefix> [harnessname] (harness written runtime/<name>.nx)
15// v1 scope: the judged fn must be self-contained (no calls into other candidate fns) -- the
16// multi-fn closure extraction is a filed rung, not silently wrong (unknown props REFUSE too).
17// license_tier: ORIGINAL No hw writes (Rule 26).
18import "nx_store_seed_lib.nx"
19import "nx_itoa_lib.nx" // shared MSB-first emitter (zero-alloc)
20import "nx_seg_store.nx"
21import "nx_deploy_lib.nx"
22import "nx_syscalls.nx"
23
24const SJ_ROWCAP: i64 = 65536
25const SJ_FNCAP: i64 = 8192
26const SJ_HCAP: i64 = 131072
27const SJ_CAPCAP: i64 = 262144
28const SJ_TAB: i64 = 9
29const SJ_NL: i64 = 10
30const SJ_COMMA: i64 = 44
31const SJ_COLON: i64 = 58
32const SJ_QUOTE: i64 = 34
33const SJ_MAXPROPS: i64 = 12
34const SJ_MAXCOLS: i64 = 16
35const SJ_PROPCAP: i64 = 512
36const SJ_PATHCAP: i64 = 256
37const SJ_EXIT_VIOL: i64 = 1
38const SJ_EXIT_CRASH: i64 = 2
39const SJ_EXIT_REFUSE: i64 = 3
40// hang-class ceiling (NB4): a whole-domain sweep hits inputs the baked tests never do, so a maker
41// fix with an unbounded loop hangs HERE where tests wouldn't. The watchdog is a SOUNDNESS bound
42// (never-hang guarantee), not a tuning knob -- pinned like autofix's best-of-N contract consts.
43const SJ_TIMEOUT_MS: i64 = 20000
44const SJ_POLL_MS: i64 = 50
45const SJ_TIMEOUT_RC: i64 = 0 - 99
46const SJ_P_ODD: i64 = 1
47const SJ_P_EVEN: i64 = 2
48const SJ_P_FIX0: i64 = 3
49const SJ_P_LIN2: i64 = 4
50const SJ_P_IDEM: i64 = 5
51const SJ_P_MONO: i64 = 6
52const SJ_P_NOCRASH: i64 = 7
53const SJ_P_RANGE: i64 = 8
54const SJ_P_COMM: i64 = 9
55const SJ_P_IDEM2: i64 = 10
56// NB8: point-anchor oracle -- a spec-derived value at ONE point. Alone it's a test; COMBINED with
57// odd/lin2 it pins the whole function (f(1)=-1 + f(2x)=2f(x) + odd => f(x)=-x everywhere). Closes the
58// neg-vs-identity gap algebraic properties can't see. Checked OUTSIDE the sweep (always fires).
59const SJ_P_ANCHOR: i64 = 11
60const SJ_P_ANCHOR2: i64 = 12
61
62func sj_w(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 }
63// MIGRATED to the shared emitter (debt 1785563586). The old body mmapped a scratch buffer
64// per call and never freed it. At PAGE granularity that is 4096B leaked PER CALL -- the
65// defect that took 28.5GB of a 36GB host in nx_ts_lumadiff (2MB input, ~3.66M calls).
66// nxi_* is MSB-first, allocates NOTHING, and emits identical bytes including the sign.
67func sj_wn(v: i64) -> i64 { nxi_out(v); return 0 }
68func sj_slen(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } return n }
69func sj_find(hay: *u8, hn: i64, needle: *u8, from: i64) -> i64 {
70 let m: i64 = sj_slen(needle)
71 if m == 0 { return 0 - 1 }
72 var i: i64 = from
73 while i + m <= hn {
74 var j: i64 = 0
75 var ok: i64 = 1
76 while j < m { if hay[i+j] != needle[j] { ok = 0; j = m } else { j = j + 1 } }
77 if ok == 1 { return i }
78 i = i + 1
79 }
80 return 0 - 1
81}
82func sj_slice_eq(q: *u8, a: i64, b: i64, s: *u8) -> i64 {
83 let sn: i64 = sj_slen(s)
84 if b - a != sn { return 0 }
85 var i: i64 = 0
86 while i < sn { if q[a + i] != s[i] { return 0 } i = i + 1 }
87 return 1
88}
89func sj_atoi_span(b: *u8, a0: i64, e: i64) -> i64 {
90 var i: i64 = a0
91 var neg: i64 = 0
92 if i < e { if b[i] == (45 as u8) { neg = 1; i = i + 1 } }
93 var v: i64 = 0
94 while i < e {
95 let c: i64 = b[i] as i64
96 if c >= 48 { if c <= 57 { v = v * 10 + (c - 48); i = i + 1 } else { i = e } } else { i = e }
97 }
98 if neg == 1 { return 0 - v }
99 return v
100}
101func sj_num_after(b: *u8, n: i64, pat: *u8) -> i64 {
102 let at: i64 = sj_find(b, n, pat, 0)
103 if at < 0 { return 0 - 1 }
104 var i: i64 = at + sj_slen(pat)
105 var v: i64 = 0
106 var any: i64 = 0
107 while i < n {
108 let c: i64 = b[i] as i64
109 if c >= 48 { if c <= 57 { v = v * 10 + (c - 48); any = 1; i = i + 1 } else { i = n } } else { i = n }
110 }
111 if any == 0 { return 0 - 1 }
112 return v
113}
114// tab columns of row [ls,le): sp[2k]=start sp[2k+1]=end ; returns ncols
115func sj_cols(q: *u8, ls: i64, le: i64, sp: *i64) -> i64 {
116 var nc: i64 = 0
117 var s: i64 = ls
118 while s <= le {
119 var e: i64 = s
120 var go: i64 = 1
121 while go == 1 { if e >= le { go = 0 } else { if q[e] == (SJ_TAB as u8) { go = 0 } else { e = e + 1 } } }
122 if nc < SJ_MAXCOLS { sp[nc + nc] = s; sp[nc + nc + 1] = e; nc = nc + 1 }
123 if e >= le { s = le + 1 } else { s = e + 1 }
124 }
125 return nc
126}
127// brace-clip the `func <name>...` definition out of the source file (autofix extract pattern)
128func sj_extract(path: *u8, name: *u8, fnbuf: *u8) -> i64 {
129 let lb: *i64 = sys_mmap(8) as *i64
130 let src: *u8 = sys_read_file(path, lb)
131 if (src as i64) == 0 { return 0 }
132 let n: i64 = lb[0]
133 let needle: *u8 = sys_mmap(128)
134 var no: i64 = 0
135 no = ss_cat(needle, no, "func " as *u8)
136 no = ss_cat(needle, no, name)
137 needle[no] = 0 as u8
138 let fs: i64 = sj_find(src, n, needle, 0)
139 if fs < 0 { return 0 }
140 var fe: i64 = fs
141 var depth: i64 = 0
142 var seen: i64 = 0
143 var go: i64 = 1
144 while go == 1 {
145 if fe >= n { go = 0 }
146 else {
147 let c: i64 = src[fe] as i64
148 if c == 123 { depth = depth + 1; seen = 1 }
149 if c == 125 { depth = depth - 1 }
150 fe = fe + 1
151 if seen == 1 { if depth == 0 { go = 0 } }
152 }
153 }
154 var fl: i64 = 0
155 var z: i64 = fs
156 while z < fe { if fl < SJ_FNCAP - 2 { fnbuf[fl] = src[z]; fl = fl + 1 } z = z + 1 }
157 fnbuf[fl] = 0 as u8
158 return fl
159}
160// emit a possibly-negative integer as compilable source text: N or (0 - N)
161func sj_catsrc_num(d: *u8, o0: i64, v: i64) -> i64 {
162 if v < 0 {
163 var o: i64 = ss_cat(d, o0, "(0 - " as *u8)
164 o = ss_catn(d, o, 0 - v)
165 o = ss_cat(d, o, ")" as *u8)
166 return o
167 }
168 return ss_catn(d, o0, v)
169}
170func sj_catq(d: *u8, o: i64) -> i64 { d[o] = SJ_QUOTE as u8; return o + 1 }
171// the shared violation block: opens the failing cond's brace, bumps viol, reports the FIRST
172// counterexample (SYMJVIOL <prop> x=<x> [y=<y>] r=<r>), closes both braces. Self-balanced.
173func sj_emit_viol(hb: *u8, o0: i64, pname: *u8, arity: i64) -> i64 {
174 var o: i64 = ss_cat(hb, o0, " { viol = viol + 1\n if vrep == 0 { vrep = 1\n sjh_w(" as *u8)
175 o = sj_catq(hb, o)
176 o = ss_cat(hb, o, "SYMJVIOL " as *u8)
177 o = ss_cat(hb, o, pname)
178 o = ss_cat(hb, o, " x=" as *u8)
179 o = sj_catq(hb, o)
180 o = ss_cat(hb, o, " as *u8)\n sjh_n(x)\n" as *u8)
181 if arity == 2 {
182 o = ss_cat(hb, o, " sjh_w(" as *u8)
183 o = sj_catq(hb, o)
184 o = ss_cat(hb, o, " y=" as *u8)
185 o = sj_catq(hb, o)
186 o = ss_cat(hb, o, " as *u8)\n sjh_n(y)\n" as *u8)
187 }
188 o = ss_cat(hb, o, " sjh_w(" as *u8)
189 o = sj_catq(hb, o)
190 o = ss_cat(hb, o, " r=" as *u8)
191 o = sj_catq(hb, o)
192 o = ss_cat(hb, o, " as *u8)\n sjh_n(r)\n sjh_nl() } }\n" as *u8)
193 return o
194}
195func sj_refuse(msg: *u8) -> i64 {
196 sj_w("SYMJUDGE REFUSED " as *u8)
197 sj_w(msg)
198 sj_w("\n" as *u8)
199 sys_exit(SJ_EXIT_REFUSE)
200 return SJ_EXIT_REFUSE
201}
202// run the staged harness elf under a wall-clock watchdog (NB4). stdout+stderr -> outf. Polls
203// non-blocking (WNOHANG); on timeout SIGKILLs the child and reaps it -> returns SJ_TIMEOUT_RC.
204// A directly-owned child (build-only produced the elf; we exec it) = we can actually kill the
205// hanging process, unlike killing nx_sov_build_run and orphaning the grandchild harness.
206func sj_run_timed(elfp: *u8, outf: *u8, timeout_ms: i64, poll_ms: i64) -> i64 {
207 let pid: i64 = sys_fork()
208 if pid < 0 { return 0 - 3 }
209 if pid == 0 {
210 let fd: i64 = sys_openat_wr(outf, 0x1a4)
211 if fd >= 0 { sys_dup3(fd, 1, 0); sys_dup3(fd, 2, 0) }
212 let argv: *i64 = sys_mmap(16) as *i64
213 argv[0] = elfp as i64
214 argv[1] = 0
215 let envp: *i64 = sys_mmap(16) as *i64
216 envp[0] = 0
217 sys_execve(elfp, argv, envp)
218 sys_exit(127)
219 return 0
220 }
221 let st: *i64 = sys_mmap(16) as *i64
222 var waited: i64 = 0
223 while waited < timeout_ms {
224 let r: i64 = sys_wait4(pid, st, WNOHANG)
225 if r == pid { return (st[0] >> 8) & 0xff }
226 if r > 0 { return (st[0] >> 8) & 0xff }
227 if r < 0 { return 0 - 4 }
228 sys_sleep_ms(poll_ms)
229 waited = waited + poll_ms
230 }
231 nx_kill(pid, 9)
232 sys_wait4(pid, st, 0)
233 return SJ_TIMEOUT_RC
234}
235
236func main(argc: i64, argv: *i64) -> i64 {
237 if argc < 4 { return sj_refuse("usage: nx_symjudge <srcfile> <fn> <planeprefix> [harness]" as *u8) }
238 let srcf: *u8 = argv[1] as *u8
239 let fnn: *u8 = argv[2] as *u8
240 let pfx: *u8 = argv[3] as *u8
241 var hname: *u8 = "nx_symj_h1" as *u8
242 if argc >= 5 { hname = argv[4] as *u8 }
243
244 // 1) property contract row from the sovereign plane (fail-closed on absence)
245 let rows: *u8 = sys_mmap(SJ_ROWCAP)
246 let rn: i64 = sts_load(pfx, rows, SJ_ROWCAP)
247 if rn <= 0 { return sj_refuse("plane-empty" as *u8) }
248 let sp: *i64 = sys_mmap(8 * SJ_MAXCOLS * 2) as *i64
249 var arity: i64 = 0 - 1
250 var lo: i64 = 0
251 var hi: i64 = 0
252 var budget: i64 = 0
253 let props: *u8 = sys_mmap(SJ_PROPCAP)
254 var propn: i64 = 0 - 1
255 var i: i64 = 0
256 while i < rn {
257 var le: i64 = i
258 var s: i64 = 1
259 while s == 1 { if le >= rn { s = 0 } else { if rows[le] == (SJ_NL as u8) { s = 0 } else { le = le + 1 } } }
260 let nc: i64 = sj_cols(rows, i, le, sp)
261 var hit: i64 = 0
262 if nc >= 6 { if sj_slice_eq(rows, sp[0], sp[1], fnn) == 1 { hit = 1 } }
263 if hit == 1 {
264 arity = sj_atoi_span(rows, sp[2], sp[3])
265 lo = sj_atoi_span(rows, sp[4], sp[5])
266 hi = sj_atoi_span(rows, sp[6], sp[7])
267 budget = sj_atoi_span(rows, sp[8], sp[9])
268 var t: i64 = sp[10]
269 propn = 0
270 while t < sp[11] { if propn < SJ_PROPCAP - 1 { props[propn] = rows[t]; propn = propn + 1 } t = t + 1 }
271 props[propn] = 0 as u8
272 i = rn
273 }
274 if i < rn { i = le + 1 }
275 }
276 if propn < 0 { return sj_refuse("row-missing" as *u8) }
277 if arity < 1 { return sj_refuse("bad-arity" as *u8) }
278 if arity > 2 { return sj_refuse("bad-arity" as *u8) }
279 if hi < lo { return sj_refuse("bad-domain" as *u8) }
280 if budget < 1 { return sj_refuse("bad-budget" as *u8) }
281
282 // 2) classify properties (unknown = REFUSE, never silently pass)
283 let pk: *i64 = sys_mmap(8 * SJ_MAXPROPS) as *i64
284 let pra: *i64 = sys_mmap(8 * SJ_MAXPROPS) as *i64
285 let prb: *i64 = sys_mmap(8 * SJ_MAXPROPS) as *i64
286 let prc: *i64 = sys_mmap(8 * SJ_MAXPROPS) as *i64
287 var np: i64 = 0
288 var q: i64 = 0
289 while q < propn {
290 var qe: i64 = q
291 var go2: i64 = 1
292 while go2 == 1 { if qe >= propn { go2 = 0 } else { if props[qe] == (SJ_COMMA as u8) { go2 = 0 } else { qe = qe + 1 } } }
293 var kind: i64 = 0
294 var ra: i64 = 0
295 var rb: i64 = 0
296 var rc: i64 = 0
297 if sj_slice_eq(props, q, qe, "odd" as *u8) == 1 { kind = SJ_P_ODD }
298 if sj_slice_eq(props, q, qe, "even" as *u8) == 1 { kind = SJ_P_EVEN }
299 if sj_slice_eq(props, q, qe, "fix0" as *u8) == 1 { kind = SJ_P_FIX0 }
300 if sj_slice_eq(props, q, qe, "lin2" as *u8) == 1 { kind = SJ_P_LIN2 }
301 if sj_slice_eq(props, q, qe, "idem" as *u8) == 1 { kind = SJ_P_IDEM }
302 if sj_slice_eq(props, q, qe, "mono" as *u8) == 1 { kind = SJ_P_MONO }
303 if sj_slice_eq(props, q, qe, "nocrash" as *u8) == 1 { kind = SJ_P_NOCRASH }
304 if sj_slice_eq(props, q, qe, "comm" as *u8) == 1 { kind = SJ_P_COMM }
305 if sj_slice_eq(props, q, qe, "idem2" as *u8) == 1 { kind = SJ_P_IDEM2 }
306 if kind == 0 {
307 if qe - q > 6 {
308 if sj_slice_eq(props, q, q + 6, "range:" as *u8) == 1 {
309 kind = SJ_P_RANGE
310 var c2: i64 = q + 6
311 var go3: i64 = 1
312 while go3 == 1 { if c2 >= qe { go3 = 0 } else { if props[c2] == (SJ_COLON as u8) { go3 = 0 } else { c2 = c2 + 1 } } }
313 if c2 >= qe { return sj_refuse("bad-range" as *u8) }
314 ra = sj_atoi_span(props, q + 6, c2)
315 rb = sj_atoi_span(props, c2 + 1, qe)
316 }
317 }
318 }
319 if kind == 0 {
320 if qe - q > 8 {
321 if sj_slice_eq(props, q, q + 8, "anchor2:" as *u8) == 1 {
322 kind = SJ_P_ANCHOR2
323 var e1: i64 = q + 8
324 var ge1: i64 = 1
325 while ge1 == 1 { if e1 >= qe { ge1 = 0 } else { if props[e1] == (SJ_COLON as u8) { ge1 = 0 } else { e1 = e1 + 1 } } }
326 if e1 >= qe { return sj_refuse("bad-anchor2" as *u8) }
327 var e2: i64 = e1 + 1
328 var ge2: i64 = 1
329 while ge2 == 1 { if e2 >= qe { ge2 = 0 } else { if props[e2] == (SJ_COLON as u8) { ge2 = 0 } else { e2 = e2 + 1 } } }
330 if e2 >= qe { return sj_refuse("bad-anchor2" as *u8) }
331 ra = sj_atoi_span(props, q + 8, e1)
332 rb = sj_atoi_span(props, e1 + 1, e2)
333 rc = sj_atoi_span(props, e2 + 1, qe)
334 }
335 }
336 }
337 if kind == 0 {
338 if qe - q > 7 {
339 if sj_slice_eq(props, q, q + 7, "anchor:" as *u8) == 1 {
340 kind = SJ_P_ANCHOR
341 var d1: i64 = q + 7
342 var gd1: i64 = 1
343 while gd1 == 1 { if d1 >= qe { gd1 = 0 } else { if props[d1] == (SJ_COLON as u8) { gd1 = 0 } else { d1 = d1 + 1 } } }
344 if d1 >= qe { return sj_refuse("bad-anchor" as *u8) }
345 ra = sj_atoi_span(props, q + 7, d1)
346 rb = sj_atoi_span(props, d1 + 1, qe)
347 }
348 }
349 }
350 if kind == 0 { return sj_refuse("unknown-property" as *u8) }
351 if arity == 1 {
352 if kind == SJ_P_COMM { return sj_refuse("prop-arity-mismatch" as *u8) }
353 if kind == SJ_P_IDEM2 { return sj_refuse("prop-arity-mismatch" as *u8) }
354 if kind == SJ_P_ANCHOR2 { return sj_refuse("prop-arity-mismatch" as *u8) }
355 }
356 if arity == 2 {
357 if kind == SJ_P_ODD { return sj_refuse("prop-arity-mismatch" as *u8) }
358 if kind == SJ_P_EVEN { return sj_refuse("prop-arity-mismatch" as *u8) }
359 if kind == SJ_P_FIX0 { return sj_refuse("prop-arity-mismatch" as *u8) }
360 if kind == SJ_P_LIN2 { return sj_refuse("prop-arity-mismatch" as *u8) }
361 if kind == SJ_P_IDEM { return sj_refuse("prop-arity-mismatch" as *u8) }
362 if kind == SJ_P_MONO { return sj_refuse("prop-arity-mismatch" as *u8) }
363 if kind == SJ_P_ANCHOR { return sj_refuse("prop-arity-mismatch" as *u8) }
364 }
365 if np < SJ_MAXPROPS { pk[np] = kind; pra[np] = ra; prb[np] = rb; prc[np] = rc; np = np + 1 }
366 q = qe + 1
367 }
368 if np < 1 { return sj_refuse("no-properties" as *u8) }
369
370 // 3) extract the fn under judgment
371 let fnb: *u8 = sys_mmap(SJ_FNCAP)
372 let fl: i64 = sj_extract(srcf, fnn, fnb)
373 if fl <= 0 { return sj_refuse("fn-not-found" as *u8) }
374
375 // 4) derive sweep step from the row's budget (deterministic; EXH = true bounded check)
376 let span: i64 = hi - lo + 1
377 var step: i64 = 1
378 var exh: i64 = 1
379 if arity == 1 { if span > budget { step = (span + budget - 1) / budget; exh = 0 } }
380 if arity == 2 {
381 var an: i64 = 1
382 while (an + 1) * (an + 1) <= budget { an = an + 1 }
383 if span > an { step = (span + an - 1) / an; exh = 0 }
384 }
385
386 // 5) generate the harness source
387 let hb: *u8 = sys_mmap(SJ_HCAP)
388 var o: i64 = 0
389 o = ss_cat(hb, o, "// GENERATED by nx_symjudge -- sweep harness, do not edit\nimport " as *u8)
390 o = sj_catq(hb, o)
391 o = ss_cat(hb, o, "nx_syscalls.nx" as *u8)
392 o = sj_catq(hb, o)
393 o = ss_cat(hb, o, "\n" as *u8)
394 var fz: i64 = 0
395 while fz < fl { hb[o] = fnb[fz]; o = o + 1; fz = fz + 1 }
396 o = ss_cat(hb, o, "\nfunc sjh_w(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 }\n" as *u8)
397 o = ss_cat(hb, o, "func sjh_nl() -> i64 { let b: *u8 = sys_mmap(8); b[0] = 10 as u8; sys_write(1, b, 1); return 0 }\n" as *u8)
398 o = ss_cat(hb, o, "func sjh_n(v: i64) -> i64 {\n var m: i64 = v\n if m < 0 { let nb: *u8 = sys_mmap(8); nb[0] = 45 as u8; sys_write(1, nb, 1); m = 0 - m }\n let t: *u8 = sys_mmap(24)\n var k: i64 = 0\n if m == 0 { t[0] = 48 as u8; k = 1 }\n while m > 0 { t[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 }\n let ob: *u8 = sys_mmap(24)\n var i: i64 = 0\n while i < k { ob[i] = t[k - 1 - i]; i = i + 1 }\n sys_write(1, ob, k)\n return 0\n}\n" as *u8)
399 o = ss_cat(hb, o, "func main() -> i64 {\n var viol: i64 = 0\n var checked: i64 = 0\n var vrep: i64 = 0\n" as *u8)
400 var hasmono: i64 = 0
401 var pm: i64 = 0
402 while pm < np { if pk[pm] == SJ_P_MONO { hasmono = 1 } pm = pm + 1 }
403 if hasmono == 1 { o = ss_cat(hb, o, " var mprev: i64 = 0\n var mhave: i64 = 0\n" as *u8) }
404 // NB8: standalone point-anchor checks -- run ONCE before the sweep so they ALWAYS fire
405 // (a SAMP-stride sweep could skip the anchor point; a direct call cannot).
406 var pa: i64 = 0
407 while pa < np {
408 if pk[pa] == SJ_P_ANCHOR {
409 o = ss_cat(hb, o, " let anch" as *u8)
410 o = ss_catn(hb, o, pa)
411 o = ss_cat(hb, o, ": i64 = " as *u8)
412 o = ss_cat(hb, o, fnn)
413 o = ss_cat(hb, o, "(" as *u8)
414 o = sj_catsrc_num(hb, o, pra[pa])
415 o = ss_cat(hb, o, ")\n if anch" as *u8)
416 o = ss_catn(hb, o, pa)
417 o = ss_cat(hb, o, " != " as *u8)
418 o = sj_catsrc_num(hb, o, prb[pa])
419 o = ss_cat(hb, o, " { viol = viol + 1\n if vrep == 0 { vrep = 1\n sjh_w(" as *u8)
420 o = sj_catq(hb, o)
421 o = ss_cat(hb, o, "SYMJVIOL anchor x=" as *u8)
422 o = sj_catq(hb, o)
423 o = ss_cat(hb, o, " as *u8)\n sjh_n(" as *u8)
424 o = sj_catsrc_num(hb, o, pra[pa])
425 o = ss_cat(hb, o, ")\n sjh_w(" as *u8)
426 o = sj_catq(hb, o)
427 o = ss_cat(hb, o, " r=" as *u8)
428 o = sj_catq(hb, o)
429 o = ss_cat(hb, o, " as *u8)\n sjh_n(anch" as *u8)
430 o = ss_catn(hb, o, pa)
431 o = ss_cat(hb, o, ")\n sjh_nl() } }\n" as *u8)
432 }
433 if pk[pa] == SJ_P_ANCHOR2 {
434 o = ss_cat(hb, o, " let anch" as *u8)
435 o = ss_catn(hb, o, pa)
436 o = ss_cat(hb, o, ": i64 = " as *u8)
437 o = ss_cat(hb, o, fnn)
438 o = ss_cat(hb, o, "(" as *u8)
439 o = sj_catsrc_num(hb, o, pra[pa])
440 o = ss_cat(hb, o, ", " as *u8)
441 o = sj_catsrc_num(hb, o, prb[pa])
442 o = ss_cat(hb, o, ")\n if anch" as *u8)
443 o = ss_catn(hb, o, pa)
444 o = ss_cat(hb, o, " != " as *u8)
445 o = sj_catsrc_num(hb, o, prc[pa])
446 o = ss_cat(hb, o, " { viol = viol + 1\n if vrep == 0 { vrep = 1\n sjh_w(" as *u8)
447 o = sj_catq(hb, o)
448 o = ss_cat(hb, o, "SYMJVIOL anchor2 r=" as *u8)
449 o = sj_catq(hb, o)
450 o = ss_cat(hb, o, " as *u8)\n sjh_n(anch" as *u8)
451 o = ss_catn(hb, o, pa)
452 o = ss_cat(hb, o, ")\n sjh_nl() } }\n" as *u8)
453 }
454 pa = pa + 1
455 }
456 o = ss_cat(hb, o, " var x: i64 = " as *u8)
457 o = sj_catsrc_num(hb, o, lo)
458 o = ss_cat(hb, o, "\n while x <= " as *u8)
459 o = sj_catsrc_num(hb, o, hi)
460 o = ss_cat(hb, o, " {\n" as *u8)
461 if arity == 2 {
462 o = ss_cat(hb, o, " var y: i64 = " as *u8)
463 o = sj_catsrc_num(hb, o, lo)
464 o = ss_cat(hb, o, "\n while y <= " as *u8)
465 o = sj_catsrc_num(hb, o, hi)
466 o = ss_cat(hb, o, " {\n let r: i64 = " as *u8)
467 o = ss_cat(hb, o, fnn)
468 o = ss_cat(hb, o, "(x, y)\n" as *u8)
469 } else {
470 o = ss_cat(hb, o, " let r: i64 = " as *u8)
471 o = ss_cat(hb, o, fnn)
472 o = ss_cat(hb, o, "(x)\n" as *u8)
473 }
474 var p: i64 = 0
475 while p < np {
476 let k: i64 = pk[p]
477 if k == SJ_P_ODD {
478 o = ss_cat(hb, o, " let rn" as *u8)
479 o = ss_catn(hb, o, p)
480 o = ss_cat(hb, o, ": i64 = " as *u8)
481 o = ss_cat(hb, o, fnn)
482 o = ss_cat(hb, o, "(0 - x)\n if rn" as *u8)
483 o = ss_catn(hb, o, p)
484 o = ss_cat(hb, o, " != (0 - r)" as *u8)
485 o = sj_emit_viol(hb, o, "odd" as *u8, arity)
486 }
487 if k == SJ_P_EVEN {
488 o = ss_cat(hb, o, " let rn" as *u8)
489 o = ss_catn(hb, o, p)
490 o = ss_cat(hb, o, ": i64 = " as *u8)
491 o = ss_cat(hb, o, fnn)
492 o = ss_cat(hb, o, "(0 - x)\n if rn" as *u8)
493 o = ss_catn(hb, o, p)
494 o = ss_cat(hb, o, " != r" as *u8)
495 o = sj_emit_viol(hb, o, "even" as *u8, arity)
496 }
497 if k == SJ_P_FIX0 {
498 o = ss_cat(hb, o, " if x == 0 { if r != 0" as *u8)
499 o = sj_emit_viol(hb, o, "fix0" as *u8, arity)
500 o = ss_cat(hb, o, " }\n" as *u8)
501 }
502 if k == SJ_P_LIN2 {
503 o = ss_cat(hb, o, " if x >= " as *u8)
504 o = sj_catsrc_num(hb, o, lo / 2)
505 o = ss_cat(hb, o, " { if x <= " as *u8)
506 o = sj_catsrc_num(hb, o, hi / 2)
507 o = ss_cat(hb, o, " { let rl" as *u8)
508 o = ss_catn(hb, o, p)
509 o = ss_cat(hb, o, ": i64 = " as *u8)
510 o = ss_cat(hb, o, fnn)
511 o = ss_cat(hb, o, "(x + x)\n if rl" as *u8)
512 o = ss_catn(hb, o, p)
513 o = ss_cat(hb, o, " != (r + r)" as *u8)
514 o = sj_emit_viol(hb, o, "lin2" as *u8, arity)
515 o = ss_cat(hb, o, " } }\n" as *u8)
516 }
517 if k == SJ_P_IDEM {
518 o = ss_cat(hb, o, " let ri" as *u8)
519 o = ss_catn(hb, o, p)
520 o = ss_cat(hb, o, ": i64 = " as *u8)
521 o = ss_cat(hb, o, fnn)
522 o = ss_cat(hb, o, "(r)\n if ri" as *u8)
523 o = ss_catn(hb, o, p)
524 o = ss_cat(hb, o, " != r" as *u8)
525 o = sj_emit_viol(hb, o, "idem" as *u8, arity)
526 }
527 if k == SJ_P_MONO {
528 o = ss_cat(hb, o, " if mhave == 1 { if r < mprev" as *u8)
529 o = sj_emit_viol(hb, o, "mono" as *u8, arity)
530 o = ss_cat(hb, o, " }\n mprev = r\n mhave = 1\n" as *u8)
531 }
532 if k == SJ_P_RANGE {
533 o = ss_cat(hb, o, " var bad" as *u8)
534 o = ss_catn(hb, o, p)
535 o = ss_cat(hb, o, ": i64 = 0\n if r < " as *u8)
536 o = sj_catsrc_num(hb, o, pra[p])
537 o = ss_cat(hb, o, " { bad" as *u8)
538 o = ss_catn(hb, o, p)
539 o = ss_cat(hb, o, " = 1 }\n if r > " as *u8)
540 o = sj_catsrc_num(hb, o, prb[p])
541 o = ss_cat(hb, o, " { bad" as *u8)
542 o = ss_catn(hb, o, p)
543 o = ss_cat(hb, o, " = 1 }\n if bad" as *u8)
544 o = ss_catn(hb, o, p)
545 o = ss_cat(hb, o, " == 1" as *u8)
546 o = sj_emit_viol(hb, o, "range" as *u8, arity)
547 }
548 if k == SJ_P_COMM {
549 o = ss_cat(hb, o, " let rc" as *u8)
550 o = ss_catn(hb, o, p)
551 o = ss_cat(hb, o, ": i64 = " as *u8)
552 o = ss_cat(hb, o, fnn)
553 o = ss_cat(hb, o, "(y, x)\n if rc" as *u8)
554 o = ss_catn(hb, o, p)
555 o = ss_cat(hb, o, " != r" as *u8)
556 o = sj_emit_viol(hb, o, "comm" as *u8, arity)
557 }
558 if k == SJ_P_IDEM2 {
559 o = ss_cat(hb, o, " if x == y { if r != x" as *u8)
560 o = sj_emit_viol(hb, o, "idem2" as *u8, arity)
561 o = ss_cat(hb, o, " }\n" as *u8)
562 }
563 p = p + 1
564 }
565 o = ss_cat(hb, o, " checked = checked + 1\n" as *u8)
566 if arity == 2 {
567 o = ss_cat(hb, o, " y = y + " as *u8)
568 o = ss_catn(hb, o, step)
569 o = ss_cat(hb, o, "\n }\n x = x + " as *u8)
570 o = ss_catn(hb, o, step)
571 o = ss_cat(hb, o, "\n }\n" as *u8)
572 } else {
573 o = ss_cat(hb, o, " x = x + " as *u8)
574 o = ss_catn(hb, o, step)
575 o = ss_cat(hb, o, "\n }\n" as *u8)
576 }
577 o = ss_cat(hb, o, " sjh_w(" as *u8)
578 o = sj_catq(hb, o)
579 o = ss_cat(hb, o, "SYMJ " as *u8)
580 o = ss_cat(hb, o, fnn)
581 o = ss_cat(hb, o, " checked=" as *u8)
582 o = sj_catq(hb, o)
583 o = ss_cat(hb, o, " as *u8)\n sjh_n(checked)\n sjh_w(" as *u8)
584 o = sj_catq(hb, o)
585 o = ss_cat(hb, o, " viol=" as *u8)
586 o = sj_catq(hb, o)
587 o = ss_cat(hb, o, " as *u8)\n sjh_n(viol)\n sjh_nl()\n return 0\n}\n" as *u8)
588
589 // 6) write harness + compile+run via the sovereign toolchain
590 let hpath: *u8 = sys_mmap(SJ_PATHCAP)
591 var hpo: i64 = ss_cat(hpath, 0, "runtime/" as *u8)
592 hpo = ss_cat(hpath, hpo, hname)
593 hpo = ss_cat(hpath, hpo, ".nx" as *u8)
594 hpath[hpo] = 0 as u8
595 if ss_writefile(hpath, hb, o) != 0 { return sj_refuse("harness-write-fail" as *u8) }
596 let outf: *u8 = sys_mmap(SJ_PATHCAP)
597 var ofo: i64 = ss_cat(outf, 0, "/tmp/sj_" as *u8)
598 ofo = ss_cat(outf, ofo, hname)
599 ofo = ss_cat(outf, ofo, ".out" as *u8)
600 outf[ofo] = 0 as u8
601 // build-only (compiler is bounded on our contracts) -> stage /tmp/<hname>.sov.elf
602 let av: *i64 = sys_mmap(32) as *i64
603 av[0] = hname as i64
604 av[1] = "--build-only" as *u8 as i64
605 dep_run_capture("_offc/nx_sov_build_run.elf" as *u8, av, 2, "/tmp/sj_build.log" as *u8)
606 let helf: *u8 = sys_mmap(SJ_PATHCAP)
607 var heo: i64 = ss_cat(helf, 0, "/tmp/" as *u8)
608 heo = ss_cat(helf, heo, hname)
609 heo = ss_cat(helf, heo, ".sov.elf" as *u8)
610 helf[heo] = 0 as u8
611 // run the harness under the wall-clock watchdog (NB4 hang-class ceiling)
612 let rrc: i64 = sj_run_timed(helf, outf, SJ_TIMEOUT_MS, SJ_POLL_MS)
613 let cap: *u8 = sys_mmap(SJ_CAPCAP)
614 let cn: i64 = dp_read(outf, cap, SJ_CAPCAP - 4)
615
616 // 7) judge: no SYMJ line = the harness never reached its summary = crash, no-compile, or HANG
617 let sjat: i64 = sj_find(cap, cn, "SYMJ " as *u8, 0)
618 if sjat < 0 {
619 sj_w("SYMJUDGE fn=" as *u8)
620 sj_w(fnn)
621 if exh == 1 { sj_w(" mode=EXH" as *u8) } else { sj_w(" mode=SAMP" as *u8) }
622 sj_w(" checked=0 viol=0 verdict=RED reason=" as *u8)
623 if rrc == SJ_TIMEOUT_RC { sj_w("timeout-hang" as *u8) } else { sj_w("crash-or-nocompile" as *u8) }
624 sj_w(" rc=" as *u8)
625 sj_wn(rrc)
626 sj_w("\n" as *u8)
627 sys_exit(SJ_EXIT_CRASH)
628 return SJ_EXIT_CRASH
629 }
630 let checked: i64 = sj_num_after(cap, cn, "checked=" as *u8)
631 let viol: i64 = sj_num_after(cap, cn, " viol=" as *u8)
632 let vp: i64 = sj_find(cap, cn, "SYMJVIOL " as *u8, 0)
633 if vp >= 0 {
634 var ve: i64 = vp
635 var g4: i64 = 1
636 while g4 == 1 { if ve >= cn { g4 = 0 } else { if cap[ve] == (SJ_NL as u8) { g4 = 0 } else { ve = ve + 1 } } }
637 sys_write(1, ((cap as i64) + vp) as *u8, ve - vp)
638 sj_w("\n" as *u8)
639 }
640 sj_w("SYMJUDGE fn=" as *u8)
641 sj_w(fnn)
642 if exh == 1 { sj_w(" mode=EXH" as *u8) } else { sj_w(" mode=SAMP" as *u8) }
643 sj_w(" checked=" as *u8)
644 sj_wn(checked)
645 sj_w(" viol=" as *u8)
646 sj_wn(viol)
647 if viol == 0 {
648 sj_w(" verdict=GREEN\n" as *u8)
649 sys_exit(0)
650 return 0
651 }
652 sj_w(" verdict=RED\n" as *u8)
653 sys_exit(SJ_EXIT_VIOL)
654 return SJ_EXIT_VIOL
655}