{"id":"2ced7e93-8cbb-4a5d-b477-79edaf4992c0","arxiv_id":"2505.09363","paper_version":2,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"The paper introduces the eqsat MLIR dialect, encoding e-graphs as SSA operations so that standard passes like CSE and pdl can implement equality saturation natively in a compiler.","lead":"This paper proposes a new MLIR dialect, eqsat, that represents equality saturation's e-graphs directly inside compiler IR, using existing compiler passes for the core algorithms. It argues this makes equality saturation a first-class compiler transformation and describes a prototype in xDSL.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The load-bearing claim that stock CSE performs congruence-closing rebuild is unverified and suspect in cyclic graph regions: CSE relies on dominance/ordering, which eqsat.egraph's graph regions intentionally violate (Section 4, Listings 4/6).","rationale":"The reader identified the weakest assumption as the claim that stock CSE preserves the congruence invariant in eqsat's graph regions, including cycles and nested regions. I agree: this is the single most load-bearing point because the paper's stated contribution, reusing existing compiler passes to implement equality saturation core algorithms, rests on it. The paper provides only a simple acyclic illustration and no proof or systematic test. My stress-test sharpens the concern by pointing to the concrete mechanism by which CSE should fail: graph regions allow use-before-def, and CSE's dominance-based canonicalization logic is not designed for that regime. The paper's own Listing 4 shows that cycles are not hypothetical, so the gap is material. I also note the fixpoint aspect: congruence closure is inherently a transitive closure, and nothing in the paper shows that one application of CSE computes that closure rather than requiring an outer iteration. This does not make the paper uninteresting or reject-worthy; the design is elegant, the writing is clear, and the xDSL prototype is real evidence of intent. But the central reuse claim needs verification before it can be accepted as a demonstrated property of MLIR. The reader's CONDITIONAL verdict is therefore appropriate, and my concern does not move it in a different direction.","tokens_in":9843,"tokens_out":6857,"duration_ms":78498,"concrete_test":"Construct a minimal eqsat example in xDSL/MLIR: take Listing 4's cyclic eclass (arith.addi %c_a, %zero with %c_a = eqsat.eclass %a, %sum) and duplicate the addi so two congruent addi nodes feed two distinct result eclasses; run the stock CSE pass and check whether (1) it terminates, (2) the two result eclasses are merged, and (3) the cyclic use-before-def edge is preserved. If any check fails, Section 4's central mechanism does not hold for cyclic e-graphs. As a second arm, enumerate all small e-graphs up to four e-classes with random rewrites and compare congruence after one CSE pass against a reference union-find closure; any mismatch refutes the claim.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The paper's central mechanism (Section 4) is that applying stock MLIR CSE after an equality merge restores the congruence invariant, so CSE subsumes e-graph rebuilding. This is load-bearing because the entire 'reuse existing compiler passes' pitch depends on it. The evidence is a single two-operand acyclic example (Listing 6). The paper itself states that equality saturation must handle cycles and represents them by placing an eclass result before its defining operation in a graph region (Listing 4). Stock CSE was designed for ordinary SSA: it replaces a use only when a redundant definition is recognized and the replacement definition dominates the use (or at least is order-safe). In a graph region, use-before-def is legal, so a duplicated parent operation can have one occurrence whose operand is the cyclic eclass value defined later; CSE's scoped table and dominance checks will not rewrite that earlier use, so the parent result eclasses are not merged and the invariant is not restored. 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. The same gap affects the fixpoint aspect: congruence can cascade (merging argument eclasses makes parent eclasses merge, which makes grandparent eclasses merge), and it is not shown that a single pass of CSE rather than an outer fixpoint loop closes this. Additionally, the prototype is in xDSL, so even the single example is not direct evidence about MLIR's stock CSE behavior. Thus the central claim is conditional on an unverified property that may fail in exactly the cyclic cases the paper explicitly introduces.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":10181,"tokens_out":2991,"duration_ms":32804,"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":[{"comment":"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.","section":"Section 4, Listing 6 (and Section 3, Listing 4)"},{"comment":"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.","section":"Section 4"},{"comment":"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.","section":"Sections 1, 6, and 8"},{"comment":"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.","section":"Section 5"}],"minor_comments":[{"comment":"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.","section":"Section 3, Listings 2 and 3"},{"comment":"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.","section":"Section 4, Listing 6"},{"comment":"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.","section":"Section 5"},{"comment":"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.","section":"Section 7"},{"comment":"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.","section":"Section 6"}],"recommendation":"major_revision","confidential_remarks":"This is a well-written design/position paper with a plausible high-level idea, but the central correctness claim about CSE preserving congruence in cyclic graph regions is not established, and there is no experimental validation. The gap is fixable in principle (by adding proofs or tests and possibly a fixpoint argument), so I recommend major revision rather than rejection. The paper might fit better at a workshop such as EGRAPHS or a systems venue that accepts design proposals; for a journal, the authors should be asked to substantiate the main mechanism."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Actually new: the representation. E-classes become SSA ops, the e-graph lives in a graph region, and the pitch is that MLIR's existing CSE and pdl infrastructure can do rebuilding and e-matching. That is a real departure from translation-layer approaches like DialEgg and SEER, and the comparison with Cranelift's acyclic e-graphs is useful. The paper is clearly written, the examples are consistent, and the authors are honest that the implementation is a prototype in xDSL, not MLIR itself.\n\nWhere it gets shaky is Section 4. The claim that CSE subsumes e-graph rebuilding is load-bearing, but the evidence is a single two-operand acyclic example (Listing 6). CSE in MLIR is designed for ordinary SSA dominance; it replaces a redundant value only when the replacement dominates (or is otherwise order-safe for) the use. eqsat.egraph regions are graph regions, so use-before-def is legal, and the paper itself introduces cycles that way (Listing 4). If a duplicated parent operation has one occurrence whose operand is a cyclic e-class value defined later, stock CSE will not rewrite that earlier use, so the parent e-classes do not merge and congruence is not restored. The cascade/fixpoint aspect—merging argument e-classes forces parent e-classes to merge, and so on—is also left open; one CSE pass may not close that in a single sweep. 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. That is the soft spot.\n\nThe lack of evaluation is proportionate for a workshop design paper, but it matters more here because the CSE claim is empirical and the prototype is in xDSL, so even the existence proof is indirect. I don't think this is fatal. The design is plausible, the writing is honest, and the related-work positioning is careful. Citations look fair, including self-citations to xDSL.\n\nWho gets value? Compiler folks working on equality saturation inside MLIR-like IRs, and e-graph researchers interested in in-compiler integration. It deserves a serious referee. A revision that either proves the CSE-rebuilding property under graph-region semantics or narrows the claim would be worth publishing. I'd send it out rather than desk-reject.","headline":"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.","tokens_in":822,"tokens_out":1691,"would_cite":true,"duration_ms":28430,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"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.","keywords":["equality saturation","e-graphs","eqsat dialect","compiler intermediate representation","common subexpression elimination","e-matching","non-destructive rewriting","graph regions"],"falsifier":"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.","tokens_in":9679,"feed_emoji":"⚙️","tokens_out":11562,"duration_ms":108341,"temperature":0.7,"pith_summary":"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.","feed_headline":"Put e-graphs in the compiler IR, not a library","feed_subtitle":"The eqsat dialect turns e-graphs into SSA values, so ordinary compiler passes can run equality saturation.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"supplies the region-based SSA intermediate representation and pattern infrastructure that the eqsat dialect builds on.","marker":"[12]"},{"why":"defines the standard e-graph data structure and the explicit rebuilding step that the paper reimplements with CSE.","marker":"[20]"},{"why":"introduces equality saturation and motivates it as a fix for the phase-ordering problem.","marker":"[18]"},{"why":"is the closest prior embedding of equality saturation in a compiler IR, providing the acyclic baseline the paper contrasts with graph regions.","marker":"[2]"},{"why":"is a translation-layer approach whose overhead and extensibility limits motivate representing e-graphs natively.","marker":"[21]"},{"why":"is the implementation vehicle in which the prototype is built.","marker":"[10]"},{"why":"supplies the backtracking e-matching strategy that the eqsat interpreter adapts to e-classes.","marker":"[9]"},{"why":"frames the integrated matcher's flexibility relative to database-style relational e-matching.","marker":"[23]"}],"fun_headline_variants":["E-graphs as SSA values in MLIR","CSE becomes congruence closure, no library","Equality saturation via standard compiler passes","In-IR e-graphs for non-destructive rewrites","No e-graph library, just IR and passes"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["E-graphs as SSA values in MLIR","CSE becomes congruence closure, no library","Equality saturation via standard compiler passes","In-IR e-graphs for non-destructive rewrites","No e-graph library, just IR and passes"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001145,"raw_usage":{"total_tokens":4742,"prompt_tokens":930,"completion_tokens":3812,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":546,"completion_tokens_details":{"reasoning_tokens":3738}},"tokens_in":546,"tokens_out":3812,"duration_ms":27524,"temperature":1.0,"reasoning_tokens":3738,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-15T21:32:52.158598+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"is the closest prior embedding of equality saturation in a compiler IR, providing the acyclic baseline the paper contrasts with graph regions."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"frames the integrated matcher's flexibility relative to database-style relational e-matching."}],"review_version":1}