nx_eqsat_membership_proof_test.nx

nx_eqsat_membership_proof_test.nx -- proves the MEMBERSHIP-AS-PROOF CERTIFICATE for (mul x 8) == (shl x 3), and proves the certificate is LOAD-BEARING (it FAILS when a non-sound rule is used or the endpoints are not in the same e-class). FAIL LOUD known-answer; exit 0 iff every check holds. STRUCTURE (each step self-asserts; mismatch => sys_exit(nonzero)): STEP 1 SOUND SET: run the W=8 masked exhaustive battery for the SIX width-trivial unary rules + mul_pow2 in-range. Establishes the proven-sound set this run (total == 1536 + 2048 == 3584, all pass). BOTH witnesses (algebraic Witness A AND triangulated gsim Witness B) must agree on every vector. This is what JUSTIFIES the allow-list. STEP 0 LOCKSTEP: the membership organ's MP_RULE_* ids must equal the engine's NX_EQSAT_RULE_* (single source of truth) so the LIVE log the engine writes is never mislabeled against this allow-list. STEP 2 CERTIFICATE (positive, LIVE): build an e-graph, add (mul x 8) and (shl x 3), ENABLE provenance, run the REAL nx_eqsat_saturate (not a gated driver), and certify STRICTLY FROM THE LOG the engine wrote at its union chokepoint -- mul_pow2 fires at k=3<W, logs RULE_MUL_POW2, find(mul8)==find(shl3), every logged id sound + no overflow -> certified. This PROMOTES mul_pow2 into the proven-sound set, now exercised through the live engine + its k<W guard. STEP 3 LOAD-BEARING NEG-A (non-sound rule): the gated leg cites the BOGUS rule (mul x 3)==(shl x 1) -> recorder REFUSES + certificate FAILS; AND a LIVE leg -- the live engine has no bogus rule, so it never unions (mul x 4) with (shl x 1) => live membership/certificate FAIL. STEP 4 LOAD-BEARING NEG-B (endpoints not in same class): LIVE-certify (mul x 8) against (shl x 2) -- the live engine merges mul8 with (shl x 3), not (shl x 2), so membership FAILS and the certificate FAILS even though the log is sound. STEP 5 LOAD-BEARING NEG-C (k>=W boundary): the membership organ's k<MP_W side-condition (mp_mul_pow2_k_ok==0 at k==W) must REFUSE + FAIL the gated certificate; in the LIVE engine this class is discharged at union time by the k<NX_EQSAT_W guard (never logged). STEP 6 LOAD-BEARING NEG-D (log completeness): an UNDERSIZED prov buffer (cap=0) still lets the real merge happen (membership holds) but the overflow flag must POISON the certificate (FAIL CLOSED) -- a truncated log can never yield a passing-but-incomplete certificate. Known answer (FAIL LOUD): prints "<sound_passed> <sound_total> <cert> " where sound_total==3584, sound_passed==3584, cert==1 (cert is now the LIVE