topic: eqsat
15 modules sharing the eqsat name family (derived from the tree's prefix discipline).
The 'eqsat' topic family in the Nishi sovereign ecosystem provides a framework for equality saturation, focusing on symbolic reasoning and rule-based transformations. The nx_eqsat module serves as the core equality-saturation framework, integrating techniques from the egg/SpEC family. Supporting this is nx_eqsat_bw_witness_gate, which manages bounded-width truncation for efficient rule application, and nx_eqsat_constfold_test, which validates constant folding through egg-style equivalence classes. These modules collectively enable rigorous structural and data-driven reasoning within the NishiLang environment.
auto-narrated by the local model from this topic's module headers; links verified against the wiki index.
narrated overview -- maintained by the narration lane, module links verified against this wiki.
| module | description | lines | funcs |
|---|---|---|---|
| nx_eqsat.nx | equality-saturation framework (egg/SpEC family). | 2201 | 56 |
| nx_eqsat_bw_witness_gate.nx | the BOUNDED-WIDTH TRUNCATION GATE underneath the whole mul_pow2 rule. | 72 | 1 |
| nx_eqsat_congruence_bench.nx | NON-TOY CONGRUENCE-HEAVY race vs egg 0.11.0. | 167 | 5 |
| nx_eqsat_congruence_test.nx | STRUCTURAL-WITNESS GATE for the egg-style | 205 | 4 |
| nx_eqsat_constfold_bench.nx | CONST-FOLD-HEAVY race vs egg 0.11.0. | 131 | 5 |
| nx_eqsat_constfold_test.nx | the CONST-FOLD GATE: proves the egg-style e-class | 211 | 5 |
| nx_eqsat_dsl_bench.nx | RULE-HEAVY race: the sovereign NishiLang DSL e-matcher | 139 | 6 |
| nx_eqsat_dsl_parity_test.nx | the 24th GATE: proves the egg-style DATA-driven | 328 | 8 |
| nx_eqsat_membership_proof.nx | MEMBERSHIP-AS-PROOF CERTIFICATE for the eqsat | 623 | 25 |
| nx_eqsat_membership_proof_test.nx | proves the MEMBERSHIP-AS-PROOF | 354 | 4 |
| nx_eqsat_race_bench.nx | RACE TIMING HARNESS vs egg 0.11.0 on the SAME task. | 151 | 5 |
| nx_eqsat_rule_proof_test.nx | SOVEREIGN soundness proof for the eqsat rewrite rules | 98 | 2 |
| nx_eqsat_test.nx | proof-of-life + correctness GATE for the equality- | 90 | 3 |
| nx_eqsat_vs_gcc_battery_test.nx | FAIR apples-to-apples op-count battery | 178 | 7 |
| nx_eqsat_wire_probe.nx | LN8 WIRING WITNESS (lang.plan rung LN8, symbol opt_eqsat_pass). | 32 | 3 |