nx_eqsat_constfold_test.nx

nx_eqsat_constfold_test.nx -- the CONST-FOLD GATE: proves the egg-style e-class ANALYSIS (constant folding / propagation) newly integrated into nx_eqsat.nx is (a) SOUND BY EVALUATION (folds via the PROVEN nx_gsim_eval_cell oracle), (b) CERTIFIED through membership-as-proof (cites NX_EQSAT_RULE_CONSTFOLD, admitted to the proven-sound allow-list + lockstep), and (c) LOAD-BEARING (a wrong fold / unmapped op / unproven rule is REFUSED). FAIL LOUD known-answer; exit 0 iff every check holds. STEPS (each self-asserts; mismatch => sys_exit(nonzero)): STEP 0 LOCKSTEP: MP_RULE_CONSTFOLD == NX_EQSAT_RULE_CONSTFOLD (and the whole id table agrees), so the live log the engine writes is never mislabeled. Also: MP_RULE_CONSTFOLD must be in the proven-sound allow-list. STEP 1 POSITIVE (add 2 3)->5, LIVE + CERTIFIED: enable prov + constfold, run the REAL saturator, assert find(add23)==find(5), the log contains RULE_CONSTFOLD, and mp_certify_live CERTIFIES (member && sound). STEP 2 MORE OPS: (mul 6 7)->42 and (shl 1 4)->16 fold + certify (same engine path). STEP 3 NEGATIVE -- WRONG FOLD REFUSED: (a) an unmapped op (DIV) never folds even with const children (nx_eqsat_op_to_gate_kind(DIV) < 0) -- find stays distinct from any const; (b) an UNPROVEN rule id (BOGUS) is NOT in the allow-list so mp_log_all_sound would refuse it -- a back-door wrong fold cannot certify; (c) folding is OFF by default (no enable => no fold => no CONSTFOLD in the log) so the feature is opt-in by construction. Known answer (FAIL LOUD): prints "5 42 16 1 1 1 " == folded(add 2 3), folded(mul 6 7), folded(shl 1 4), cert_add, cert_mul, cert_shl. exit 0 iff all steps hold.