code wiki / _hdl_build / nx_symjudge_gate.nx
`nx_symjudge_gate.nx` source

↩ module page · 215 lines · 11031 B
1// nx_symjudge_gate.nx -- gate for THE SYMBOLIC JUDGE (autonomous-builder lane, 2026-07-20).
2// On nx_gate_verdict (D001 migrate-on-touch law: new gates import THE lib). Proves the judge:
3//   T1  a CORRECT fn passes its property contract -> verdict=GREEN rc=0
4//   T1b domain fits budget -> mode=EXH (true bounded sweep, not a sample)
5//   T1c checked == full domain size (1201 for -600..600) = exhaustiveness is real
6//   T2  the OVERFIT-PATCH class is KILLED: a fn that passes its baked tests (dbl(2)=4, dbl(3)=6)
7//       but is wrong elsewhere -> property sweep RED rc=1 (the class test-only judging cannot see)
8//   T3  the first counterexample is REPORTED (SYMJVIOL line) = actionable, not just a verdict
9//   T4  a CRASHING fn (SIGFPE at x=0) -> detected -> rc=2 (the fuzz-crash finding class)
10//   T5  determinism: identical rerun -> byte-identical judge output
11//   T6  fn with no contract row -> REFUSED rc=3 (fail-closed, never silently green)
12// Requires /tmp/nx_symjudge.sov.elf staged (nx_sov_build_run nx_symjudge --build-only).
13// license_tier: ORIGINAL   No hw writes (Rule 26).   expect_exit: 0
14import "nx_store_seed_lib.nx"
15import "nx_seg_store.nx"
16import "nx_deploy_lib.nx"
17import "nx_gate_verdict.nx"
18import "nx_syscalls.nx"
19
20const SJG_CAP: i64 = 65536
21const SJG_TAB: i64 = 9
22const SJG_NL: i64 = 10
23
24func sjg_slen(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } return n }
25func sjg_has(q: *u8, n: i64, s: *u8) -> i64 {
  let sn: i64 = sjg_slen(s)
  if sn == 0 { return 1 }
  var i: i64 = 0
  while i + sn <= n {
      var hit: i64 = 1
      var j: i64 = 0
      while j < sn { if q[i+j] != s[j] { hit = 0; j = sn } else { j = j + 1 } }
      if hit == 1 { return 1 }
      i = i + 1
  }
  return 0
37}
38func sjg_eqbuf(a: *u8, an: i64, b: *u8, bn: i64) -> i64 {
  if an != bn { return 0 }
  var i: i64 = 0
  while i < an { if a[i] != b[i] { return 0 } i = i + 1 }
  return 1
43}
44// append one 7-col tab row + newline
45func sjg_row(d: *u8, o0: i64, c0: *u8, c1: *u8, c2: *u8, c3: *u8, c4: *u8, c5: *u8, c6: *u8) -> i64 {
  var o: i64 = ss_cat(d, o0, c0)
  d[o] = SJG_TAB as u8
  o = ss_cat(d, o + 1, c1)
  d[o] = SJG_TAB as u8
  o = ss_cat(d, o + 1, c2)
  d[o] = SJG_TAB as u8
  o = ss_cat(d, o + 1, c3)
  d[o] = SJG_TAB as u8
  o = ss_cat(d, o + 1, c4)
  d[o] = SJG_TAB as u8
  o = ss_cat(d, o + 1, c5)
  d[o] = SJG_TAB as u8
  o = ss_cat(d, o + 1, c6)
  d[o] = SJG_NL as u8
  return o + 1
61}
62
63func main() -> i64 {
  let ctr: *i64 = gv_ctr()
  gv_head("nx_symjudge gate -- symbolic judge: exhaustive sweep, overfit-kill, crash-detect, determinism, fail-closed" as *u8)
  let elf: *u8 = "/tmp/nx_symjudge.sov.elf" as *u8
67
  // fixtures: correct / overfit (passes its baked tests, wrong elsewhere) / crashing
  let fa: *u8 = "func sgn(x: i64) -> i64 { if x > 0 { return 1 } if x < 0 { return 0 - 1 } return 0 }\n" as *u8
  let fb: *u8 = "func dbl(x: i64) -> i64 { if x == 2 { return 4 } if x == 3 { return 6 } return x * x }\n" as *u8
  let fc: *u8 = "func inv(x: i64) -> i64 { return 100 / x }\n" as *u8
  // hang fixture: spins forever at x==0 (a whole-domain sweep hits it; baked tests wouldn't)
  let fh: *u8 = "func hng(x: i64) -> i64 { var k: i64 = 0 while x == 0 { k = k + 1 } return x }\n" as *u8
  // NB8 anchor fixtures: nid=identity (odd,lin2,fix0 ALL hold -> the algebraic gap), nng=correct
  // negation. Same contract odd,lin2,fix0,anchor:1:-1 -> the anchor is what separates them.
  let fn2: *u8 = "func nid(x: i64) -> i64 { return x }\nfunc nng(x: i64) -> i64 { return 0 - x }\n" as *u8
  let fm: *u8 = "func mx(a: i64, b: i64) -> i64 { if a > b { return a } return b }\n" as *u8
  ss_writefile("runtime/nx_symj_fixa.nx" as *u8, fa, sjg_slen(fa))
  ss_writefile("runtime/nx_symj_fixb.nx" as *u8, fb, sjg_slen(fb))
  ss_writefile("runtime/nx_symj_fixc.nx" as *u8, fc, sjg_slen(fc))
  ss_writefile("runtime/nx_symj_fixh.nx" as *u8, fh, sjg_slen(fh))
  ss_writefile("runtime/nx_symj_fixn.nx" as *u8, fn2, sjg_slen(fn2))
  ss_writefile("runtime/nx_symj_fixm.nx" as *u8, fm, sjg_slen(fm))
84
  // per-run-unique symprop- plane
  let rb: *u8 = sys_mmap(2048)
  var ro: i64 = 0
  ro = sjg_row(rb, ro, "sgn" as *u8, "1" as *u8, "-600" as *u8, "600" as *u8, "4096" as *u8, "odd,range:-1:1,fix0" as *u8, "gate-fixture" as *u8)
  ro = sjg_row(rb, ro, "dbl" as *u8, "1" as *u8, "-300" as *u8, "300" as *u8, "4096" as *u8, "lin2,odd" as *u8, "gate-overfit" as *u8)
  ro = sjg_row(rb, ro, "inv" as *u8, "1" as *u8, "-5" as *u8, "5" as *u8, "4096" as *u8, "nocrash" as *u8, "gate-crash" as *u8)
  ro = sjg_row(rb, ro, "hng" as *u8, "1" as *u8, "-2" as *u8, "2" as *u8, "4096" as *u8, "nocrash" as *u8, "gate-hang" as *u8)
  ro = sjg_row(rb, ro, "nid" as *u8, "1" as *u8, "-600" as *u8, "600" as *u8, "4096" as *u8, "odd,lin2,fix0,anchor:1:-1" as *u8, "gate-anchor-id" as *u8)
  ro = sjg_row(rb, ro, "nng" as *u8, "1" as *u8, "-600" as *u8, "600" as *u8, "4096" as *u8, "odd,lin2,fix0,anchor:1:-1" as *u8, "gate-anchor-neg" as *u8)
  ro = sjg_row(rb, ro, "mx" as *u8, "2" as *u8, "-30" as *u8, "30" as *u8, "4096" as *u8, "comm,idem2,anchor2:3:5:5" as *u8, "gate-anchor2" as *u8)
  let pfx: *u8 = sys_mmap(128)
  var po: i64 = ss_cat(pfx, 0, "/tmp/sjg" as *u8)
  po = ss_catn(pfx, po, sys_now_realtime_sec())
  po = ss_cat(pfx, po, "-" as *u8)
  pfx[po] = 0 as u8
  let sr: i64 = sts_seed(pfx, rb, ro)
  if sr != 7 { gv_check("T0 plane seeded 7 rows" as *u8, 0, ctr) } else { gv_check("T0 plane seeded 7 rows" as *u8, 1, ctr) }
102
  let av: *i64 = sys_mmap(64) as *i64
104
  // T1 correct fn -> GREEN, EXH, full-domain checked
  av[0] = "runtime/nx_symj_fixa.nx" as *u8 as i64
  av[1] = "sgn" as *u8 as i64
  av[2] = pfx as i64
  av[3] = "nx_symj_ga" as *u8 as i64
  let r1: i64 = dep_run_capture(elf, av, 4, "/tmp/sjg_t1.out" as *u8)
  let c1: *u8 = sys_mmap(SJG_CAP)
  let n1: i64 = dp_read("/tmp/sjg_t1.out" as *u8, c1, SJG_CAP - 4)
  var t1: i64 = 0
  if r1 == 0 { if sjg_has(c1, n1, "verdict=GREEN" as *u8) == 1 { t1 = 1 } }
  gv_check("T1 correct fn GREEN rc0" as *u8, t1, ctr)
  gv_check("T1b exhaustive mode EXH" as *u8, sjg_has(c1, n1, "mode=EXH" as *u8), ctr)
  gv_check("T1c checked full domain 1201" as *u8, sjg_has(c1, n1, "checked=1201" as *u8), ctr)
118
  // T2 overfit patch (passes its baked tests) -> properties kill it
  av[0] = "runtime/nx_symj_fixb.nx" as *u8 as i64
  av[1] = "dbl" as *u8 as i64
  av[2] = pfx as i64
  av[3] = "nx_symj_gb" as *u8 as i64
  let r2: i64 = dep_run_capture(elf, av, 4, "/tmp/sjg_t2.out" as *u8)
  let c2: *u8 = sys_mmap(SJG_CAP)
  let n2: i64 = dp_read("/tmp/sjg_t2.out" as *u8, c2, SJG_CAP - 4)
  var t2: i64 = 0
  if r2 == 1 { if sjg_has(c2, n2, "verdict=RED" as *u8) == 1 { t2 = 1 } }
  gv_check("T2 overfit patch RED rc1" as *u8, t2, ctr)
  gv_check("T3 counterexample SYMJVIOL reported" as *u8, sjg_has(c2, n2, "SYMJVIOL " as *u8), ctr)
131
  // T4 crashing fn -> rc2 crash class
  av[0] = "runtime/nx_symj_fixc.nx" as *u8 as i64
  av[1] = "inv" as *u8 as i64
  av[2] = pfx as i64
  av[3] = "nx_symj_gc" as *u8 as i64
  let r4: i64 = dep_run_capture(elf, av, 4, "/tmp/sjg_t4.out" as *u8)
  let c4: *u8 = sys_mmap(SJG_CAP)
  let n4: i64 = dp_read("/tmp/sjg_t4.out" as *u8, c4, SJG_CAP - 4)
  var t4: i64 = 0
  if r4 == 2 { if sjg_has(c4, n4, "reason=crash" as *u8) == 1 { t4 = 1 } }
  gv_check("T4 crash fn detected rc2" as *u8, t4, ctr)
143
  // T5 determinism: identical rerun byte-identical
  av[0] = "runtime/nx_symj_fixa.nx" as *u8 as i64
  av[1] = "sgn" as *u8 as i64
  av[2] = pfx as i64
  av[3] = "nx_symj_ga" as *u8 as i64
  let r5: i64 = dep_run_capture(elf, av, 4, "/tmp/sjg_t5.out" as *u8)
  let c5: *u8 = sys_mmap(SJG_CAP)
  let n5: i64 = dp_read("/tmp/sjg_t5.out" as *u8, c5, SJG_CAP - 4)
  var t5: i64 = 0
  if r5 == 0 { if sjg_eqbuf(c1, n1, c5, n5) == 1 { t5 = 1 } }
  gv_check("T5 deterministic byte-identical rerun" as *u8, t5, ctr)
155
  // T6 no contract row -> REFUSED (fail-closed)
  av[0] = "runtime/nx_symj_fixa.nx" as *u8 as i64
  av[1] = "nosuch" as *u8 as i64
  av[2] = pfx as i64
  av[3] = "nx_symj_gd" as *u8 as i64
  let r6: i64 = dep_run_capture(elf, av, 4, "/tmp/sjg_t6.out" as *u8)
  var t6: i64 = 0
  if r6 == 3 { t6 = 1 }
  gv_check("T6 missing contract REFUSED rc3" as *u8, t6, ctr)
165
  // T7 HANG class (NB4): fn that spins forever at x==0 -> watchdog kills -> rc2 timeout-hang
  av[0] = "runtime/nx_symj_fixh.nx" as *u8 as i64
  av[1] = "hng" as *u8 as i64
  av[2] = pfx as i64
  av[3] = "nx_symj_gh" as *u8 as i64
  let r7: i64 = dep_run_capture(elf, av, 4, "/tmp/sjg_t7.out" as *u8)
  let c7: *u8 = sys_mmap(SJG_CAP)
  let n7: i64 = dp_read("/tmp/sjg_t7.out" as *u8, c7, SJG_CAP - 4)
  var t7: i64 = 0
  if r7 == 2 { if sjg_has(c7, n7, "reason=timeout-hang" as *u8) == 1 { t7 = 1 } }
  gv_check("T7 hang fn watchdog-killed rc2" as *u8, t7, ctr)
177
  // T8 ANCHOR (NB8): identity passes odd,lin2,fix0 (verified GREEN w/o anchor) but the anchor:1:-1
  // point-oracle CATCHES it -> RED via SYMJVIOL anchor. Closes the neg-vs-identity gap.
  av[0] = "runtime/nx_symj_fixn.nx" as *u8 as i64
  av[1] = "nid" as *u8 as i64
  av[2] = pfx as i64
  av[3] = "nx_symj_gi" as *u8 as i64
  let r8: i64 = dep_run_capture(elf, av, 4, "/tmp/sjg_t8.out" as *u8)
  let c8: *u8 = sys_mmap(SJG_CAP)
  let n8: i64 = dp_read("/tmp/sjg_t8.out" as *u8, c8, SJG_CAP - 4)
  var t8: i64 = 0
  if r8 == 1 { if sjg_has(c8, n8, "SYMJVIOL anchor x=1" as *u8) == 1 { t8 = 1 } }
  gv_check("T8 anchor catches identity odd/lin2/fix0 missed" as *u8, t8, ctr)
190
  // T9 anchor GREEN on correct negation -> no false RED (anchor doesn't break correct fns)
  av[1] = "nng" as *u8 as i64
  av[3] = "nx_symj_gj" as *u8 as i64
  let r9: i64 = dep_run_capture(elf, av, 4, "/tmp/sjg_t9.out" as *u8)
  let c9: *u8 = sys_mmap(SJG_CAP)
  let n9: i64 = dp_read("/tmp/sjg_t9.out" as *u8, c9, SJG_CAP - 4)
  var t9: i64 = 0
  if r9 == 0 { if sjg_has(c9, n9, "verdict=GREEN" as *u8) == 1 { t9 = 1 } }
  gv_check("T9 anchor GREEN on correct negation" as *u8, t9, ctr)
200
  // T10 arity-2 anchor2 path works -> correct max2 GREEN on comm,idem2,anchor2:3:5:5
  av[0] = "runtime/nx_symj_fixm.nx" as *u8 as i64
  av[1] = "mx" as *u8 as i64
  av[3] = "nx_symj_gk" as *u8 as i64
  let r10: i64 = dep_run_capture(elf, av, 4, "/tmp/sjg_t10.out" as *u8)
  let c10: *u8 = sys_mmap(SJG_CAP)
  let n10: i64 = dp_read("/tmp/sjg_t10.out" as *u8, c10, SJG_CAP - 4)
  var t10: i64 = 0
  if r10 == 0 { if sjg_has(c10, n10, "verdict=GREEN" as *u8) == 1 { t10 = 1 } }
  gv_check("T10 arity-2 anchor2 GREEN on correct max2" as *u8, t10, ctr)
211
  let rc: i64 = gv_verdict("SYMJUDGE-GATE" as *u8, ctr, "symbolic judge: exhaustive sweep + overfit-kill + crash-detect + hang-watchdog + point-anchor + deterministic + fail-closed" as *u8)
  sys_exit(rc)
  return rc
215}
nx_symjudge_gate.nx source

`nx_symjudge_gate.nx` source
