Pith. sign in

REVIEW 4 major objections 5 minor 22 references

eqsat: An Equality Saturation Dialect for Non-destructive Rewriting

T0 review · 4 major / 5 minor · reviewed 2026-08-15 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read E-graphs can live natively in the compiler's intermediate representation, letting stock CSE and pattern-matching passes implement e-graph rebuilding and e-matching.

desk verdict The new idea is representing e-graphs natively as SSA ops in MLIR-style IR, but the central claim that stock CSE closes congruence in cyclic graph regions is unproven and likely wrong without adaptation. read the letter →

arxiv 2505.09363 v2 pith:GEL5SMO2 submitted 2025-05-14 cs.PL

Jules Merckx , Alexandre Lopoukhine , Samuel Coward , Jianyi Cheng , Bjorn De Sutter , Tobias Grosser This is my paper · ORCID
classification cs.PL
keywords equalitysaturatione-graphseqsatdialectcompilerintermediaterepresentationcommonsubexpressioneliminatione-matchingnon-destructiverewritinggraphregions
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

Equality saturation normally runs in an external library: a compiler exports code to the e-graph library, rewrites inside a sealed graph, and imports back a single optimized expression. This paper proposes making the e-graph itself part of the compiler's intermediate representation through a new dialect, eqsat, in which each e-class is an SSA value and the graph lives in a region. The paper's central claim is that once e-graphs are embedded this way, ordinary compiler machinery can run equality saturation: common subexpression elimination (CSE) restores the congruence invariant after e-classes are merged, and the pdl pattern language, extended with backtracking, performs e-matching. If the claim holds, equality saturation becomes just another compiler transformation that can be applied to any domain-specific IR and kept alive across other passes, instead of an isolated external step with translation overhead.

What carries the argument

The load-bearing mechanism is the eqsat dialect's representation of e-classes as SSA values: each eqsat.eclass operation names one e-class, its operands are the equivalent e-node results, and consuming operations take e-class values as operands, so the IR's use-def graph is the e-graph. This mapping carries the whole argument: CSE, a pass that already deduplicates operations with identical operands, becomes e-graph rebuilding; an adapted interpreter over the lower-level pattern-matching operations becomes e-matching by backtracking through the operands of an eqsat.eclass; and graph-region semantics let rewrites such as $a+0 \to a$ introduce cycles that ordinary SSA would forbid.

What would settle it

Construct an eqsat.egraph region that contains a cycle, e.g., the $a+0 \to a$ case, and in which two parent operations have identical operands but should remain in separate e-classes; run the stock CSE pass over the region. If CSE merges the parents when it should not, fails to terminate on the cycle, or fails to merge parents that the congruence invariant requires to be merged, the central claim that CSE subsumes e-graph rebuilding is refuted. A broader falsification would be a randomized differential comparison of CSE-based rebuilding against a reference e-graph implementation on cyclic and nested-region inputs.

Watch

Extended reading notes

Core claim

The paper establishes a claim about representation: an e-graph can be written directly in SSA-based IR using three operations — eqsat.eclass, which collects the results of equivalent operations into a single e-class value; eqsat.egraph, whose region contains the graph and permits cyclic def-use edges; and eqsat.yield, which exposes chosen classes to the surrounding program. In this encoding, the use-def edges of the IR are the edges of the e-graph, so no separate data structure is needed. The paper then claims that two stock pieces of compiler infrastructure become the core algorithms of equality saturation: applying CSE over the region rebuilds the congruence closure, and running the pdl pattern-matching interpreter with retries across e-class members performs e-matching. The consequence is that the barrier between equality saturation and compiler passes is lifted, allowing rewrites to be non-destructive while equality information persists through the compilation flow.

Load-bearing premise

The strongest load-bearing premise is that the stock CSE pass, designed for ordinary acyclic SSA code, still preserves the congruence invariant when run over eqsat's graph regions—including regions with cyclic def-use edges and nested regions—a point the paper supports with a single two-node example and no proof or exhaustive test.

Editorial extensions

If this is right

  • No translation layer between the compiler IR and an external e-graph library is needed, since the e-graph is the IR.
  • The e-graph state can persist through the compiler pipeline, so equality information survives later transformations such as inlining.
  • A stock CSE pass can restore the congruence invariant after e-class merges, replacing a bespoke congruence-closure algorithm.
  • Existing rewrite patterns written in pdl can be applied non-destructively to e-graphs, with the interpreter backtracking over equivalent values inside an e-class.
  • Cyclic e-graphs, which arise naturally from rules like $a+0 \to a$, are representable in the IR through graph regions.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • An implication the authors leave implicit is that any pass that preserves equality of values could run directly on the e-graph IR, so the phase-ordering problem between rewriting and passes like inlining can be attacked by running those passes while equality information is still live.
  • A testable extension is to add region-matching to the pattern interpreter; once that exists, rewrites can target entire control-flow operations, extending equality saturation from expression trees to structured control flow itself.
  • A natural verification step would be a randomized differential test of CSE-as-rebuilding against a reference e-graph implementation on cyclic and nested-region inputs, turning the paper's single-example evidence into broader empirical coverage.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

4 major / 5 minor

Summary. This paper proposes a new MLIR dialect, eqsat, that represents e-graphs directly in an SSA-based compiler IR. The authors introduce three operations (eqsat.eclass, eqsat.egraph, eqsat.yield) to encode e-classes and e-graphs, and argue that existing compiler infrastructure—specifically the CSE pass and the PDL pattern-matching dialect—can be reused to implement e-graph rebuilding and e-matching. The paper presents a mapping from e-graph concepts to IR concepts, illustrates cycles and control-flow representation through graph regions, and describes a prototype implementation in xDSL. The central technical claim is that a standard CSE pass, applied after an equality merge, restores the congruence invariant, thereby subsuming explicit e-graph rebuilding.

Significance. If the central claim holds, this is a valuable conceptual contribution: it would let equality saturation be integrated into a production compiler IR without an external e-graph library, and it would allow other compiler passes to preserve and exploit equality information. The paper's strengths are its clear exposition of the mapping between e-graphs and SSA IR, its reuse of existing infrastructure instead of inventing a parallel framework, and its open-source prototype. These strengths, however, are offset by the lack of a correctness argument and the absence of any experimental validation; the paper currently reads as a well-motivated design proposal rather than a demonstrated system.

major comments (4)
  1. [Section 4, Listing 6 (and Section 3, Listing 4)] The load-bearing claim that stock MLIR CSE performs congruence-closing rebuild is supported only by a single acyclic example. The paper itself acknowledges (Section 3, Listing 4) that equality saturation must handle cycles, and represents them by allowing an eclass result to be used before its defining operation in a graph region. Standard CSE is designed for ordinary SSA IR with dominance/ordering: it replaces a use only when a redundant definition is recognized and the replacement definition dominates the use (or is otherwise order-safe). In a graph region, a duplicated parent operation can have an operand that is a cyclic eclass value defined later, and the CSE's scoped table and dominance checks will not rewrite that earlier use. The paper offers no proof, no exhaustive test, and no discussion of how CSE's dominance assumptions interact with graph regions or nested control-flow regions. Because the 'reuse existing compiler passes' pitch depends entirely on this mechanism, this gap is load-bearing.
  2. [Section 4] The paper does not address the fixpoint or cascade aspect of congruence closure. After merging two e-classes, the congruence invariant can propagate transitively: if argument e-classes merge, parent e-classes must merge, then grandparent e-classes, and so on. Standard e-graph rebuilding uses a worklist to close under congruence. The paper claims that a single application of CSE restores the invariant, but gives no argument that one pass of CSE reaches the closure; it is not even stated whether the equality saturation loop iterates CSE to a fixpoint. This matters for both correctness and termination, and the single example in Listing 6 cannot demonstrate the cascade behavior.
  3. [Sections 1, 6, and 8] The paper claims a framework that 'maintains the e-graph state across compiler transformations,' but it presents no experimental evaluation, no end-to-end demonstration on a nontrivial rewrite, and no benchmarks. The implementation is in xDSL, a Python-native SSA IR that 'closely mirrors' MLIR, not in MLIR itself; the behavior of the actual MLIR CSE pass in graph regions is therefore not verified. The manuscript should either provide such evidence or clearly state that the contribution is a design proposal, and should discuss the fidelity of xDSL's CSE to MLIR's CSE with respect to region and dominance handling.
  4. [Section 5] The description of the custom pdl_interp interpreter for e-matching leaves a completeness question open. The interpreter is said to backtrack and try all possible values in an e-class for pdl_interp.get_defining_op, but the paper does not argue that this strategy explores all combinations of e-class members (which can interact across multiple occurrences of get_defining_op in a pattern) or terminates. Since e-matching is one of the two central algorithms that the paper claims to reuse, a correctness or completeness argument is needed.
minor comments (5)
  1. [Section 3, Listings 2 and 3] The labels 'Listing 2 - top' and 'Listing 2 - bottom' are informal; consider splitting the listing into two numbered listings or using a consistent in-text reference.
  2. [Section 4, Listing 6] The caption 'CSE subsumes egraph rebuilding' is slightly misleading, since the depicted transformation also includes an explicit equality merge step; the caption should make clear that the claim is about the rebuilding part only.
  3. [Section 5] The paragraph explaining pdl_interp.get_defining_op is unclear about when the interpreter decides to abandon a backtracking branch: it says the interpreter 'keeps track' of the operation, but not what triggers switching to the next operand. A short pseudocode or state-machine description would help.
  4. [Section 7] The comparison to Cranelift's acyclic e-graphs would be stronger if it cited the specific Cranelift paper or technical report on ægraphs rather than only the general Cranelift website.
  5. [Section 6] The statement that region-based control flow operations 'do not inhibit equality saturation' is contradicted later in the same section, where the authors note that pdl cannot yet match complete control-flow operations; the wording should be softened to reflect the current limitation.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the design claims are constructive and argued from independently defined MLIR infrastructure, not derived from the paper's own conclusions.

full rationale

The paper makes no empirical predictions and fits no parameters. Its central claim is that e-graphs can be embedded in MLIR via eqsat.eclass, eqsat.egraph, and eqsat.yield operations, and that existing compiler infrastructure, notably CSE and pdl, can implement e-graph rebuilding and e-matching. I checked each load-bearing step for definitional circularity. The embedding in Section 3 defines new IR primitives and graph regions; the CSE-as-rebuilding argument in Section 4 (Listing 6) observes that after an equality merge, duplicated applications of a function on the merged e-class can be removed by stock CSE. This is not circular: CSE's redundancy criterion and the eqsat dialect are specified independently, and the invariant restoration is demonstrated on a concrete example rather than assumed. The pdl-based e-matching in Section 5 is a mapping from pdl_interp operations to e-class semantics, not a renaming of the desired result. Self-citations to xDSL, SEER, and related group work are contextual or infrastructural, and none is invoked as the sole justification for the central mechanism. The skeptical concern that stock CSE may not preserve congruence on cyclic graph regions or nested regions is a correctness/robustness question, not a circularity: a weak or unproven claim is different from a claim true by construction or by self-reference. No equation in the paper reduces to its own inputs, no fitted value is relabeled as a prediction, and no uniqueness theorem is imported from the authors' prior work. The paper is therefore self-contained with respect to circularity concerns.

Assumptions & free parameters 0 free parameters · 3 assumptions · 1 invented entities

No mathematical derivation or data fitting is used; the paper is a systems design, so there are no fitted parameters. The main assumptions are about the behavior of existing compiler infrastructure when applied to the new dialect.

assumptions (3)
  • domain assumption MLIR/xDSL graph regions can represent cyclic e-graph use-def structures without breaking IR validity.
    The paper relies on MLIR's graph-region feature to encode cycles such as a+0 -> a (Listing 4, Section 3).
  • ad hoc to paper Standard CSE preserves the congruence invariant for eqsat-encoded e-graphs, including in the presence of cycles.
    The Section 4 rebuilding argument assumes CSE subsumes e-graph rebuilding based on the Listing 6 example; no proof is given.
  • domain assumption pdl_interp operations can be adapted to e-graph matching with backtracking while preserving the semantics of destructive rewrites.
    Section 5 assumes the adapted interpreter correctly handles get_result, get_defining_op, create_operation, and replace against the eqsat eclass indirection.
invented entities (1)
  • eqsat dialect operations (eqsat.eclass, eqsat.egraph, eqsat.yield)
    purpose: Represent e-graphs as native MLIR/xDSL IR so equality saturation can be integrated into compiler passes.
    These are new IR primitives introduced by the paper; they have no external validation outside the prototype described here.

how reviews work

0 comments
Cite this review

Pith. "Pith review of eqsat: An Equality Saturation Dialect for Non-destructive Rewriting." pith.science (2026). https://pith.science/paper/GEL5SMO2

@misc{pith2026250509363,
  author       = {Pith},
  title        = {Pith review of: eqsat: An Equality Saturation Dialect for Non-destructive Rewriting},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/GEL5SMO2}},
  note         = {Machine review of arXiv:2505.09363}
}
read the original abstract

With recent algorithmic improvements and easy-to-use libraries, equality saturation is being picked up for hardware design, program synthesis, theorem proving, program optimization, and more. Existing work on using equality saturation for program optimization makes use of external equality saturation libraries such as egg, typically generating a single optimized expression. In the context of a compiler, such an approach uses equality saturation to replace a small number of passes. In this work, we propose an alternative approach that represents equality saturation natively in the compiler's intermediate representation, facilitating the application of constructive compiler passes that maintain the e-graph state throughout the compilation flow. We take LLVM's MLIR framework and propose a new MLIR dialect named eqsat that represents e-graphs in MLIR code. This not only provides opportunities to rethink e-matching and extraction techniques by orchestrating existing MLIR passes, such as common subexpression elimination, but also avoids translation overhead between the chosen e-graph library and MLIR. Our eqsat intermediate representation (IR) allows programmers to apply equality saturation on arbitrary domain-specific IRs using the same flow as other compiler transformations in MLIR.

Figures

Figures reproduced from arXiv: 2505.09363 by the authors.

Figure 1
Figure 1. (left) In MLIR’s default, destruc￾tive rewriting, pdl_interp.get_result and pdl_interp.get_defining_op are each other’s in￾verse. (right) In equality saturation, this is not the case because each value comes from one of multiple equivalent operations. In order to reuse this existing rewrite infrastructure for matching patterns in the IR that has been extended with eqsat operations, we have implemented an alternative… view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

22 extracted references · 8 canonical work pages

  1. [1]

    GCC, the GNU Compiler Collection - GNU Project

    2024. GCC, the GNU Compiler Collection - GNU Project. https: //gcc.gnu.org/

    work page 2024

  2. [2]

    Bytecode Alliance. 2024. Cranelift. https://cranelift.dev

    work page 2024

  3. [3]

    Apple Inc. 2024. The Swift Programming Language . https://docs.swift. org/swift-book/documentation/the-swift-programming-language/ Version 6.1

    work page 2024

  4. [4]

    Aart Bik, Penporn Koanantakool, Tatiana Shpeisman, Nicolas Vasi- lache, Bixia Zheng, and Fredrik Kjolstad. 2022. Compiler support for sparse tensor computations in MLIR.ACM Transactions on Architecture and Code Optimization (TACO) 19, 4 (2022), 1–25

    work page 2022

  5. [5]

    Jianyi Cheng, Samuel Coward, Lorenzo Chelini, Rafael Barbalho, and Theo Drane. 2024. SEER: Super-Optimization Explorer for HLS using E-graph Rewriting with MLIR. In Proceedings of the 29th ACM Interna- tional Conference on Architectural Support for Programming Languages and Operating Systems. Association for Computing Machinery, La Jolla, CA, 1029–1044. d...

    arXiv 2024

  6. [6]

    Constantinides, and Theo Drane

    Samuel Coward, George A. Constantinides, and Theo Drane. 2023. Combining E-Graphs with Abstract Interpretation. In Proceedings of the 12th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis. Association for Computing Machinery, Orlando, FL, 1–7. doi:10.1145/3589250.3596144

    arXiv 2023

  7. [7]

    Samuel Coward, Theo Drane, and George A Constantinides. 2024. ROVER: RTL Optimization via Verified E-Graph Rewriting.IEEE Trans- actions on Computer-Aided Design of Integrated Circuits and Systems 43 (2024), 4687–4700. doi:10.1109/TCAD.2024.3410154

    arXiv 2024

  8. [8]

    Coward, L

    S. Coward, L. Paulson, T. Drane, and E. Morini. 2022. Formal Verifica- tion of Transcendental Fixed- and Floating-point Algorithms using an Automatic Theorem Prover. Formal Aspects of Computing 34, 2 (2022). doi:10.1145/3543670

    work page doi:10.1145/3543670 2022

Show all 22 references
  1. [9]

    Leonardo De Moura and Nikolaj Bjørner. 2007. Efficient E-matching for SMT solvers. In Proceedings of the 21st International Conference on Automated Deduction: Automated Deduction, Vol. 4603 LNAI. Springer- Verlag, Bremen, 183–198. doi: 10.1007/978-3-540-73595-3{_}13

    2007 doi

  2. [11]

    Chris Lattner and Vikram Adve. 2004. LLVM: A compilation frame- work for lifelong program analysis & transformation. In International Symposium on Code Generation and Optimization, CGO . IEEE, 75–86. doi:10.1109/CGO.2004.1281665

    2004 arXiv

  3. [12]

    Chris Lattner, Mehdi Amini, Uday Bondhugula, Albert Cohen, Andy Davis, Jacques Pienaar, River Riddle, Tatiana Shpeisman, Nicolas Vasi- lache, and Oleksandr Zinenko. 2021. MLIR: Scaling Compiler Infras- tructure for Domain Specific Computation. In 2021 IEEE/ACM Interna- tional ...

    2021

  4. [14]

    Charles Gregory Nelson. 1980. Techniques for program verification . Ph. D. Dissertation. Stanford University

    1980

  5. [15]

    Rachit Nigam, Samuel Thomas, Zhijing Li, and Adrian Sampson. 2021. A compiler infrastructure for accelerator generators. In Proceedings of the 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems (Virtual, USA) (ASPLOS ’21)...

    2021

  6. [16]

    Pavel Panchekha, Alex Sanchez-Stern, James R Wilcox, and Zachary Tatlock. 2015. Automatically improving accuracy for floating point expressions. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation , Vol. 50. Associa- tion for Com...

    2015

  7. [17]

    Brett Saiki, Jackson Brough, Jonas Regehr, Jesus Ponce, Varun Pradeep, Aditya Akhileshwaran, Zachary Tatlock, and Pavel Panchekha. 2025. Target-Aware Implementation of Real Expressions. InProceedings of the 30th ACM International Conference on Architectural Support for Program...

    2025

  8. [18]

    Ross Tate, Michael Stepp, Zachary Tatlock, and Sorin Lerner. 2009. Equality saturation: A new approach to optimization. InProceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Pro- gramming Languages, Vol. 44. Association for Computing Machinery, 264–276...

    2009

  9. [19]

    Nicolas Vasilache, Oleksandr Zinenko, Aart JC Bik, Mahesh Ravis- hankar, Thomas Raoux, Alexander Belyaev, Matthias Springer, Tobias Gysi, Diego Caballero, Stephan Herhut, et al. 2022. Composable and modular code generation in MLIR: A structured and retargetable ap- proach to t...

    2022 arXiv

  10. [20]

    Max Willsey, Chandrakana Nandi, Yisu Remy Wang, Oliver Flatt, Zachary Tatlock, and Pavel Panchekha. 2021. Egg: Fast and extensible equality saturation. In Proceedings of the ACM on Principles of Pro- gramming Languages, Vol. 5. Association for Computing Machinery. doi:10.1145/3434304

    2021 doi

  11. [21]

    Abd-El-Aziz Zayed and Christophe Dubach. 2025. DialEgg: Dialect- Agnostic MLIR Optimizer using Equality Saturation with Egglog. In Proceedings of the 23rd ACM/IEEE International Symposium on Code Generation and Optimization (Las Vegas, NV, USA) (CGO ’25) . As- sociation for Co...

    2025

  12. [22]

    Yihong Zhang, Yisu Remy Wang, Oliver Flatt, David Cao, Philip Zucker, Eli Rosenthal, Zachary Tatlock, and Max Willsey. 2023. Better Together: Unifying Datalog and Equality Saturation. Proceedings of the ACM on Programming Languages 7, PLDI (2023), 468–492. doi: 10.1145/3591239

    2023 doi

  13. [23]

    Yihong Zhang, Yisu Remy Wang, Max Willsey, and Zachary Tatlock

  14. [2022]

    Relational e-matching. Proc. ACM Program. Lang. 6, POPL, Article 35 (Jan. 2022), 22 pages. doi:10.1145/3498696

    2022 doi

Pith tools

Reviewed August 15, 2026 · model on record in the stance chip above.