nx_rule_soundness.nx

nx_rule_soundness.nx -- SOVEREIGN soundness prover for the nx_eqsat rewrite rules. Each rule in nx_eqsat.nx does a union that ASSERTS an algebraic equivalence; this organ PROVES that equivalence holds for ALL inputs in W-bit (mod 2^W) arithmetic, via the winning strategy: (1) WIDTH-INDEPENDENT INDUCTION (reuses the nx_alu_divider_proof_test.nx template): prove a per-element invariant EXHAUSTIVELY at a representative width W, plus a width-independence argument (per_rule comments) that lifts the W=8 machine-check to ANY W. For the SIX width-trivial unary rules {add_zero, sub_self, add_self, and_self, or_zero, mul_one} the lift is genuine: identity-element / group-inverse / per-bit-idempotence / k=1-shift laws DO NOT depend on W. For mul_pow2 it is k-induction with the side-condition k+1<W (base k=0, step *2 == <<1 mod 2^W). (2) EXHAUSTIVE SMALL-WIDTH: enumerate every x in [0,2^W) (and, for mul_pow2, every k in [0,W)) -- a real proof over the rule's full local operand space at W, NOT sampling. (3) nx_triangulate AS INDEPENDENT CROSS-CHECK: two independent gsim legs (LHS-eval, RHS-eval) plus an independent oracle, fed to nx_tri_pass_strict (unanimity, k_min = n_legs). Defense in depth. TWO INDEPENDENT WITNESSES, ANDed (honoring the design's two-witness claim): - WITNESS A (algebraic, SEPARATELY CODED): a NishiLang-native masked-arith computation of the rule's invariant, computed WITHOUT reading the gsim legs (so it is independent of the gsim truncation behavior). Asserts the masked identity directly. - WITNESS B (triangulation over gsim legs): the two netlist evaluators must BOTH equal the masked oracle. A rule vector is CERTIFIED iff WITNESS A holds AND WITNESS B passes. TRUNCATION-GAP DEFENSE (adversarial trap #1): nx_gsim_eval_cell computes a*b, a<<b, a+b, a-b in FULL i64 with ZERO truncation. So this organ MASKS every evaluator output (and the oracle) to (1<<W)-1 BEFORE comparison -- the check then tests the real mod-2^W identity, not a coincidental i64 identity. The algebraic witness also masks. No rule is certified on raw unmasked i64. k>=W BOUNDARY DEFENSE (adversarial trap #2): mul_pow2 fires unbounded in nx_eqsat.nx (NO k<W guard -- owed). For k>=W the identity is FALSE (2^k mod 2^W == 0 so x*2^k mod 2^W == 0 for all x, but x<<k is an out-of-range