nx_superopt.nx

nx_superopt.nx -- the AUTHOR leg of the Sovereign Invention Engine: a MECHANIZED SUPEROPTIMIZER. With NO LLM in the loop it runs one full invention tick over an arithmetic expression: PROPOSE -- nx_eqsat saturation generates the equivalence-class closure of the seed under the wired sound rewrite rules (the proposal space is materialized deterministically; no search policy, no LLM). SCORE -- TWO tiers, both honest. Tier-1 = the e-graph's bottom-up cost extractor (nx_eqsat_recompute_best / nx_eqsat_best_cost, the RV64IM op-cost model). Tier-2 = an INDEPENDENT width-weighted gate-level critical-path (nx_lat_honest over a lowered NxGsim netlist) so "cheaper" cannot be the unit-metric self-deception. VERIFY -- nx_triangulate equivalence-by-agreement: the candidate must compute the SAME value as the seed over a dense+random+edge battery (exhaustive at the small example width). Crucially the legs are GENUINELY INDEPENDENT realizations (see below), so a collusion among same-instruction legs cannot rubber-stamp an unsound rewrite -- and we prove the check CATCHES a planted non-equivalent candidate. EMIT -- only after VERIFY passes AND the cost strictly decreased on the honest metric do we accept the extracted cheapest DAG. This is mechanized superoptimization = the first rung of mechanized INVENTION (imitate -> match -> superopt/exceed). Honesty: equivalence is high-confidence AGREEMENT over a battery (exhaustive at small width), NOT a symbolic proof -- stated, per the racing doctrine. LEG INDEPENDENCE (the keystone defense). A naive triangulation of (mul x 2^k) -> (shl x k) would have every leg evaluate `x << k` on the same i64 ALU and collude: native MUL and SHL wrap identically on i64, so a shared-substrate battery passes by echoing one computation three times -- worthless. So our three legs do NOT share the candidate's arithmetic path: LEG 0 = interpret the CANDIDATE emit-DAG (native ops; the lowered form). LEG 1 = run the lowered CANDIDATE NxGsim netlist (independent gate-sim path). LEG 2 = the OPERAND-RECONSTRUCTING witness: recompute the SEED's value WITHOUT any shift fast-path -- a behavioral shift-add multiply that adds shifted partial products bit-by-bit. An off-by-one shift count, or a rule firing outside its proven width domain, makes LEG 2 disagree. The ORACLE is the SEED emit-DAG interpreted directly. (LEG 0 vs ORACLE already pits candidate-form against seed-form; LEG 2 is the cross-substrate check.)