nx_eqsat_rule_proof_test.nx

nx_eqsat_rule_proof_test.nx -- SOVEREIGN soundness proof for the eqsat rewrite rules (algebraic-normal-form leg). Models nx_alu_divider_proof_test.nx: a machine-checked exhaustive small-width check, cross-checked by triangulation legs that all run through nx_gsim (independent of NishiLang `*`/`<<` codegen, because they go via the netlist). WORKED EXAMPLE: certify mul x 8 == shl x 3 BY PROOF (not by battery): build the LHS netlist (MUL x 8) and the RHS netlist (SHL x 3), sweep x over a representative width, and require both legs to equal a third independent oracle on EVERY vector. MIGRATED OFF A HAND-ROLLED VERDICT 2026-08-14, and it had NEVER BEEN COMPILED before that day -- nor had nx_eqsat.nx itself, which did not compile at all (a module const read 470 lines above its declaration). So this proof existed on disk, fully written, and had never once run. A NEGATIVE CONTROL WAS ADDED IN THE SAME PASS. The original asserted only that the sound pair AGREES on all 256 vectors. A triangulator that returned pass for everything would have scored full marks -- the gates-green-on-garbage class. The control sweeps an UNSOUND pair (mul x 8 vs shl x FOUR, off by one bit) through the same machinery and requires it to DISAGREE, so a pass on the sound pair now means the comparison can actually fail. license_tier: ORIGINAL expect_exit: 0