nx_symjudge.nx

nx_symjudge.nx -- THE SYMBOLIC JUDGE (autonomous-builder lane, 2026-07-20). The non-LLM half of the neuro-symbolic builder loop: a maker's patch that PASSES the baked tests can still be wrong on every untested input (the overfit-patch class) or crash on edge inputs. This organ judges ONE pure integer function against a DATA-DRIVEN property contract (a symprop- plane row, store-law: no flat files) by GENERATING a sweep harness, compiling it fresh with the sovereign toolchain, running it: - domain fits budget -> EXHAUSTIVE sweep = bounded-model-check style proof over the whole domain - larger -> deterministic stride sample (never random-flaky; step derived from budget) - crash/SIGFPE/no-output -> RED (the fuzz-crash finding class, sovereign + deterministic) Property NAMES are plane data (odd,even,fix0,lin2,idem,mono,nocrash,range:a:b,comm,idem2); checker bodies are code here; domains/budget live in the row (rule 11: no magic numbers). symprop- row schema (7 col, tab): fn arity lo hi budget props note Verdict: SYMJUDGE fn=<f> mode=EXH|SAMP checked=<n> viol=<v> verdict=GREEN|RED [reason=...] exit: 0 GREEN | 1 property violation | 2 crash-or-nocompile | 3 refused (fail-closed) argv: <srcfile> <fn> <planeprefix> [harnessname] (harness written runtime/<name>.nx) v1 scope: the judged fn must be self-contained (no calls into other candidate fns) -- the multi-fn closure extraction is a filed rung, not silently wrong (unknown props REFUSE too). license_tier: ORIGINAL No hw writes (Rule 26).