nx_superopt_test.nx

nx_superopt_test.nx -- GATE + proof for the mechanized superoptimizer organ (nx_superopt.nx, the AUTHOR leg of the Sovereign Invention Engine). Proves, with NO LLM in the loop, one full PROPOSE/SCORE/VERIFY/EMIT invention tick on the smallest end-to-end-provable example: SEED (mul x 8) --> EMIT (shl x 3). It self-asserts a known answer + sys_exit(0), establishing: (1) the loop FOUND a cheaper equivalent of the seed (cand_count==3, root=SHL, shift=3) -- PROPOSE via nx_eqsat saturation, EMIT via the extractor. (2) the cheaper form is TRIANGULATED-EQUIVALENT to the seed over a dense(exhaustive small-width) + random + edge battery via THREE genuinely independent legs -- AND we prove the check would CATCH a non-equivalent candidate (the (shl x 2) negative control is REJECTED by the same battery). (3) the cost STRICTLY decreased on the honest metric, twice independently: Tier-1 e-graph op-cost 3 -> 1, AND Tier-2 honest gate-level latency at W=64: MUL = 2*ceil(log2 64) = 12 -> SHL = ceil(log2 64) = 6. LEG INDEPENDENCE (the keystone honesty defense -- legs must not collude on the same i64 instruction): LEG0 = candidate emit-DAG interp; LEG1 = candidate lowered-NxGsim gate-sim (independent code path); LEG2 = the SEED's value via a shift-FREE repeated-doubling multiply (never takes the candidate's `<<` path). ORACLE = the SEED emit-DAG (mul x 8) interpreted directly. A wrong shift count makes LEG2 (and the oracle) disagree with LEG0/LEG1 -- exactly what the negative control demonstrates is CAUGHT. KNOWN ANSWER (FAIL LOUD), one line: "<found> <seed_cost> <cand_cost> <seed_lat> <cand_lat> <root_op> <cand_count> <bpass> <btotal> <neg_rejected> <neg_first_bad_leg>" = "1 3 1 12 6 11 3 <N> <N> 1 0 " where N = battery vector count, root_op 11 = SHL, neg_rejected 1 = the (shl x 2) wrong candidate FAILED the battery, neg_first_bad_leg 0 = leg 0 (emit-interp of the wrong candidate) first diverged. Expected: "1 3 1 12 6 11 3 585 585 1 0 " run=0