nx_eqsat_dsl_parity_test.nx

nx_eqsat_dsl_parity_test.nx -- the 24th GATE: proves the egg-style DATA-driven rule DSL + general e-matcher (nx_eqsat_apply_dsl_table) is BEHAVIORALLY-IDENTICAL to the 7 hand-coded inline rules, AND proves ONE genuinely-new sound rule ((xor x x)==0) is admitted-only-after-proof, applied via the DSL, and CERTIFIES through membership-as-proof -- with a load-bearing NEGATIVE control showing an UNPROVEN/un-admitted rule is REFUSED. WHY behavioral-parity (not byte-identity) for the DSL path: the inline saturate runs verbatim whenever g.dsl==null (byte-identity by construction, proven by the four frozen organs staying 1:1). This gate proves the OPT-IN DSL path produces the SAME observable result -- same canonical partition, same extracted op+cost, same provenance multiset, same saturate return code -- over multiple graphs, so the data table genuinely DRIVES saturation (it is not a no-op shim). STRUCTURE (each step self-asserts; mismatch => sys_exit(nonzero)): STEP 1 PARITY over eqsat_test Case 1 (add (mul x x) 0): inline vs DSL agree on find-partition + recompute_best op/cost + provenance multiset + sat rc. STEP 2 PARITY over eqsat_test Case 2 (mul x 8 -> shl x 3): same checks; this exercises the mul_pow2 side-condition + real-merge counting AS DATA. STEP 3 PARITY over a RULE-DENSE graph touching all 7 rules at once. STEP 4 NEW RULE soundness: run the W=8 masked exhaustive two-witness battery for xor_self; assert passed==total==256 (this JUSTIFIES the allow-list arm). Without this passing, mp_is_sound_rule(9) must not be trusted. STEP 5 NEW RULE applied via DSL + CERTIFIED: build (xor v v), enable prov+DSL with the 8-row table (7 builtins + xor_self), saturate; the e-matcher merges the xor-class with const-0 citing id 9; mp_certify_live==1. STEP 6 NEGATIVE CONTROL (load-bearing): a graph whose only merge cites an UN-admitted rule id must REFUSE. We drive the certifier's log scan with a hand-forged log containing an un-admitted id (200) and assert mp_log_all_sound==0 -> certificate refused; AND assert the engine's xor_self merge, if its id were NOT in the allow-list, would refute (mp_is_sound_rule on a bogus id == 0). Proves the gate is load-bearing. KNOWN ANSWER (FAIL LOUD), one line: "<p1> <p2> <p3> <xor_passed> <xor_total> <xor_cert> <neg_refused>" = "1 1 1 256 256 1 1 " exit 0 iff every assertion holds. SOVEREIGN: no SMT, no .sh; runs on the pinned NishiLang compiler. license_tier: ORIGINAL