{"id":"cfad3e6d-f4d1-4580-a6d2-22eed0551eab","arxiv_id":"2602.16707","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":3,"one_line_summary":"E-graphs become first-class compiler IR via the eqsat dialect, enabling persistent equality saturation; a partial Herbie reimplementation matches accuracy but is ~400× slower.","lead":"This paper introduces eqsat, a new MLIR/xDSL dialect that stores equality-saturation e-graphs directly inside a compiler's IR so the graphs can persist across compilation passes. It demonstrates the idea by re-implementing part of Herbie's floating-point accuracy optimizer, matching Herbie's accuracy on most benchmarks but running roughly 400× slower.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Central persistence claim is unsupported: the only evaluation is a single-pass Herbie replication at one abstraction level, and the abstract's promised software/hardware speedups are absent from the full text.","rationale":"The reader's weakest assumption identifies the straight-line restriction as the main limitation, and I agree that control flow is a genuine scope gap. However, the more immediately load-bearing issue is that even within the pure straight-line subset, the paper never tests the central 'persistence across abstraction levels' claim. The Herbie replication is a single-shot saturation-and-extract pipeline at one abstraction level; no ordinary compiler transformation is interleaved with a live e-graph, and no multi-abstraction flow is evaluated. This is not an internal logical inconsistency, but it is a mismatch between the central claim and the evidence. Additionally, the abstract promises concrete software and hardware results that do not appear in the full text, which is a factual inconsistency that should be corrected. The paper does have real independent support: the Herbie replication and the combined-matcher speedup (2.57x geometric mean) show the eqsat encoding works as an equality-saturation engine. Those results justify a conditional verdict, not acceptance, because the distinctive persistence/interleaving contribution remains untested. My read thus supports the reader's CONDITIONAL verdict without changing it.","tokens_in":19521,"tokens_out":6705,"duration_ms":72786,"concrete_test":"Implement a minimal multi-phase experiment: create an eqsat.egraph on a high-level expression, apply a real lowering or canonicalization pass (not an eqsat rewrite) while the e-graph is live, then resume saturation and extract; compare the result against a baseline that extracts before the interleaved pass. If eqsat cannot survive such interleaving, or the retained equalities never change the final output, the persistence claim fails. Also check the full text for the abstract's promised software/hardware case studies; if they are absent, the claimed demonstrations must be removed or provided.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim is that an e-graph embedded in the compiler IR can persist across phases and abstraction levels, enabling interleaving with other compiler transformations. For that claim to hold, the eqsat representation must survive and remain useful when ordinary MLIR passes run around or inside it, and it must be exercised at multiple abstraction levels in one flow. The submission does not demonstrate either. The Section 5 case study constructs one eqsat.egraph from FPCore, runs equality saturation to a 4000-e-node limit, extracts, and stops; no lowering, inlining, or unrelated pass is interleaved with a live e-graph. The motivating complex-number example only combines lowering and optimization rewrites inside a single saturation loop, which is not the same as persistence across compiler phases. The abstract additionally promises a software case study improving performance by 1.18x on average and a hardware case study reducing circuit delay by up to 11%, but neither experiment appears in the full text. The reader's control-flow limitation is valid, but even within straight-line code the core persistence/interleaving claim is not yet tested. This is the load-bearing gap: if eqsat is only used as a single isolated pass, it is a new encoding of equality saturation, not a persistent compiler abstraction.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"This paper proposes representing e-graphs directly in the compiler IR by introducing an `eqsat` dialect in MLIR/xDSL, with operations `eqsat.egraph`, `eqsat.eclass`, `eqsat.const_eclass`, and `eqsat.yield`. The authors reinterpret PDL-based pattern matching as e-matching, add a `choose` operation and eager semantic checks to avoid backtracking blowup, implement rebuilding and extraction as compiler passes, and lift existing dataflow analyses to e-class analyses. As the main evaluation, they replicate Herbie's equality saturation phase on 31 FPBench benchmarks, reporting accuracy close to Herbie on most benchmarks, a 2.57x speedup from combined matching, and a 401x overall slowdown relative to Herbie. The paper claims that this design enables persistent e-graphs across compilation phases and abstraction levels, helping mitigate the phase-ordering problem.","tokens_in":19835,"tokens_out":4053,"duration_ms":46147,"significance":"If the central claim holds, the paper makes a useful systems contribution: embedding e-graphs in an extensible SSA-based IR and reusing existing rewrite infrastructure (PDL) and dataflow analyses is a promising way to lower the barrier to equality saturation in real compilers. The Herbie replication is a nontrivial feasibility demonstration, and the careful description of the matcher reordering and the `choose` extension shows real engineering insight. I also see no circularity in reusing Herbie's rules and benchmarks; that is a legitimate replication test. However, the paper's headline claim — that the e-graph persists across phases and abstraction levels, interleaved with other compiler transformations — is not actually demonstrated by the included experiments. The abstract also promises software and hardware speedups that do not appear in the full text. The significance is therefore conditional on either adding the missing experiments or substantially narrowing the claims.","major_comments":[{"comment":"The abstract claims a software case study improving performance by 1.18x on average and a hardware case study reducing circuit delay by up to 11% over standard equality saturation. Neither experiment appears anywhere in the full text. Section 5 contains only the Herbie accuracy/runtime study. These are not presentation details: the claimed speedups are the concrete evidence for the persistence/interleaving benefit. The authors must either include the missing experiments or remove/qualify these claims in the abstract and introduction.","section":"Abstract, §1, §5"},{"comment":"The case study does not exercise persistence across compilation phases or abstraction levels. The flow in Figure 6 creates one eqsat.egraph from FPCore input, runs equality saturation to a 4000 e-node limit, extracts, and stops. No unrelated MLIR pass (e.g., inlining, CSE, or a lowering pass) is interleaved with a live e-graph, and all rewrites occur at essentially one level of abstraction. The §2 motivating example combines lowering and optimization rules inside a single saturation loop, but simultaneous multi-abstraction rewriting is not the same as persistence across pipeline phases. Since the central claim is that the e-graph persists and is interleavable with other transformations, this is a load-bearing gap that needs a direct experiment.","section":"§5, Figure 6"},{"comment":"The implementation is explicitly restricted to pure, straight-line functions; the authors state that rewriting processes and extraction are not yet aware of scopes, and §8 says the pdl dialect cannot currently match regions or rewrite control-flow operations. This is an acknowledged limitation, but it directly narrows the paper's headline generality. Real MLIR pipelines routinely contain loops, branches, and nested regions, so the abstraction's persistence across a realistic compilation flow remains unsubstantiated. The paper should either demonstrate a control-flow-containing example or clearly reposition the contribution as a straight-line subset.","section":"§4.1, §8"},{"comment":"The accuracy comparison appears to be a single run per benchmark, with no confidence intervals, repeated trials, or error bars. The paper itself notes nondeterminism introduced by the e-node limit and possible ordering effects: 'It is possible that a different ordering of rewrites would lead to other rules being applied, leading to a more accurate result by chance.' With such nondeterminism, the claim that the implementation 'matches Herbie's accuracy on most benchmarks' needs statistical support, or at the very least a discussion of run-to-run variance.","section":"§5, Figure 7"},{"comment":"The 401x geometric-mean slowdown is explained by Python/xDSL overhead and the fixed 1024-bit MPFR evaluation, with only 18.6% of runtime spent in equality saturation. This is acceptable as a feasibility demonstration, and the 2.57x speedup from combined matching is a meaningful micro-result. However, the large slowdown means the practical benefits of the persistent-e-graph approach remain speculative until an optimized implementation exists. The paper should make this caveat more prominent in the abstract and conclusion, not only in the runtime paragraph.","section":"§5, Figure 8"}],"minor_comments":[{"comment":"'expressability' should be 'expressibility'.","section":"§1"},{"comment":"'perfomance' is a typo for 'performance'.","section":"§5 Runtime"},{"comment":"'Alleqsat.eclass operations' should be 'All eqsat.eclass operations'.","section":"§4.1"},{"comment":"The semantics of eqsat_pdl_interp.choose are described only schematically; a small concrete example showing how the choose operation interacts with the existing pdl_interp backtracking stack would make the presentation much clearer.","section":"§4.2.1"},{"comment":"The benchmark names on the x-axes are small and may be unreadable after typesetting; a table with the exact NMSE values and timings would improve reproducibility.","section":"§5, Figures 7-9"},{"comment":"The paper says all benchmarks hit the 4000 e-node limit and thus saturation is never reached. This should be stated more prominently, since it means the comparison is against Herbie with a resource-limited run, not a saturating equality saturation.","section":"§5"}],"recommendation":"major_revision","confidential_remarks":"The abstract/full-text mismatch is serious: the 1.18x software and 11% hardware results are promised but absent. If those experiments do not exist, the authors must rewrite the abstract. The persistence/interleaving claim also needs a direct test; as written, the paper demonstrates a new encoding of equality saturation in MLIR, not a persistent compiler abstraction. I see no authorship or citation-policy concerns, but the scope of the submission needs to be aligned with what is actually evaluated."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The eqsat dialect is a genuinely new design point: e-graphs represented natively in MLIR IR via eqsat.egraph, eqsat.eclass, and graph regions for cycles, plus a non-destructive reinterpretation of PDL for e-matching. It is distinct from DialEgg's external egglog orchestration and Cranelift's custom acyclic e-graph, and it sensibly reuses existing MLIR infrastructure. The matcher optimizations (eager semantic checks, choose operation) are concrete. The Herbie replication is a real feasibility demonstration, not circular: reusing Herbie's rules and benchmarks to show parity is a replication test, and the authors are candid about the 401x slowdown and the straight-line-only scope.\n\nNow the soft spots, in proportion. The abstract promises a software speedup of 1.18x and a hardware delay reduction of up to 11 percent, but neither experiment appears in the full text. That is a serious mismatch and should be fixed before publication. More importantly, the central claim - persistence across abstraction levels and interleaving with other passes - is not actually tested. The Section 5 flow builds one e-graph from FPCore, saturates it to a 4000 e-node limit, extracts, and stops. No lowering, inlining, or unrelated pass runs while the e-graph is alive. The motivating complex-number example only combines lowering and optimization rewrites inside a single saturation loop, which is not the same as persistence across compiler phases. So what is demonstrated is a new encoding of equality saturation, not yet a persistent compiler abstraction. The reader's control-flow concern is valid, but even within straight-line code the load-bearing persistence/interleaving claim is untested. The accuracy evaluation is single-run with no error bars, and the authors acknowledge non-determinism from the e-node limit. These are addressable, but they currently prevent an accept.\n\nWho should read this: compiler people working on equality saturation or MLIR infrastructure. The design idea is worth engaging with, and the implementation details are generally solid and honestly scoped in Sections 4.1 and 8. It deserves a serious referee. I would want the abstract aligned with the evidence, an artifact released, and either a demonstration of interleaving/persistence or a clearly scaled-back claim before accepting.","headline":"The eqsat dialect is a genuinely new design for embedding e-graphs in MLIR, but the paper's central persistence claim is not demonstrated; the evaluation is a single isolated saturation pass, and the abstract promises results the full text never reports.","tokens_in":756,"tokens_out":2425,"would_cite":true,"duration_ms":48666,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68N20"],"pacs":[],"model":"deepseek-v4-flash","headline":"This paper argues that an e-graph — the data structure that records all equivalent expressions found by equality saturation — can be embedded directly into a compiler's intermediate representation and persist across the whole compilation fl","keywords":["equality saturation","e-graph","compiler intermediate representation","SSA","pattern rewriting","phase-ordering problem","e-class analysis","floating-point accuracy"],"falsifier":"Run the proposed pipeline on a loop-carried computation, with equality saturation before and after a loop transformation such as unrolling: if the second saturation phase cannot see (or reconstruct) the equalities created in the first, because the intervening transformation destroyed the e-class structure, then the e-graph did not actually persist across the compilation flow.","tokens_in":19371,"feed_emoji":"⚙️","tokens_out":9671,"duration_ms":100571,"temperature":0.7,"pith_summary":"Equality saturation usually lives outside the compiler: a tool builds an e-graph, rewrites it, extracts one best expression, and hands back a single answer, discarding all other equivalences. The paper tries to change that by encoding the e-graph itself as operations in the compiler's intermediate representation, introducing a small dialect — e-graph wrapper, e-class, constant e-class, and yield — so the e-graph persists across passes. If this works, compiler developers can interleave equality saturation with other transformations such as lowering, inlining, and constant folding, mitigating the phase-ordering problem because alternatives are never lost. The authors support the idea by reimplementing the equality-saturation stage of a floating-point accuracy tool, matching the original's accuracy on most benchmarks and showing that combined pattern matching gives speedups over per-pattern matching.","feed_headline":"E-graphs move inside the compiler and survive every pass","feed_subtitle":"Embedding equivalences in the IR lets compilers interleave rewriting with lowering, inlining, and constant folding.","key_machinery":"The load-bearing machinery is the eqsat dialect built on SSA: eqsat.egraph wraps a region in a graph region (allowing cyclic use-def edges, which appear when rewriting x+0 to x folds into a cycle); eqsat.eclass groups one or more equivalent values into an e-class; eqsat.const_eclass wraps constants so existing constant folding works; eqsat.yield exposes chosen e-classes to surrounding code. Rewriting is done by a reinterpreted pattern-language interpreter: it backtracks over e-class members, reorders semantic checks to avoid exponential backtracking blowup, inserts a choose operation to isolate backtracking between different patterns, and converts destructive replace into constructive 'add t","core_discovery":"The central claim is that an e-graph need not be a separate data structure that the compiler talks to; it can be the IR itself. The paper's eqsat dialect represents each equivalence class as an operation, ordinary compute operations point at e-class results, and a graph-region wrapper permits cycles, so the full equality-saturation machinery — matching, congruence rebuilding, extraction — operates directly on the program. Because the e-graph is made of ordinary IR operations, existing analyses and passes can see it, and extraction can be partial: a cost model can select the best member of some e-classes now and others later. The case study demonstrates the approach can reproduce the core of","pith_inferences":["If region-level rewrites are enabled (the paper names this as future work), equality saturation could restructure loops and conditionals themselves, not just straight-line bodies — that would be a genuinely new capability for compiler IRs.","A persistent e-graph opens the door to multi-stage, multi-cost extraction: a high-level pass could pick a numerically stable form, lower it, and a later pass with the same e-graph could revisit the choice when actual hardware costs are known.","The large slowdown measured against the specialized reference implementation stems largely from the Python prototype and 1024-bit high-precision evaluation; a compiled implementation along the lines the paper sketches would likely bring the persistent-e-graph approach into practical range."],"forward_implications":["E-classes remain in the IR after equality saturation ends, so a later pass can exploit equalities that an earlier extraction ignored.","The same declarative rewrite patterns used for ordinary lowering work for equality saturation, with no separate ruleset or translation layer.","Existing dataflow analyses become e-class analyses by defining e-class as the meet of its members, so interval analysis and friends run on e-graphs without new infrastructure.","Extraction is composable: greedy or integer-linear-programming selection can be run now, and a different cost model can finish the job later, enabling trade-offs such as performance versus floating-point accuracy.","Combining all patterns into a single matching routine is measurably faster than applying them one at a time — the paper measures 2.34× on a small ported test suite and 2.57× on the floating-point case study's saturation phase."],"fun_headline_variants":["Make the IR an e-graph: equivalences survive every pass","Persistent e-graphs: the IR itself is the equivalence structure","E-graph as IR: rewriting interleaves with all compiler passes","No throwaway e-graphs: it’s the IR, alive per pass"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"The whole approach is only implemented and tested for pure, straight-line functions; the paper explicitly leaves loops, branches, and control-flow rewrites for future work, so the broader claim that the e-graph persists across abstraction levels rests on the assumption that real pipelines can be handled without these.","fun_headline_variants_meta":{"raw":{"variants":["Make the IR an e-graph: equivalences survive every pass","Persistent e-graphs: the IR itself is the equivalence structure","E-graph as IR: rewriting interleaves with all compiler passes","No throwaway e-graphs: it’s the IR, alive per pass"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.00015,"raw_usage":{"total_tokens":1019,"prompt_tokens":718,"completion_tokens":301,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":462,"completion_tokens_details":{"reasoning_tokens":220}},"tokens_in":462,"tokens_out":301,"duration_ms":3802,"temperature":1.0,"reasoning_tokens":220,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-04T05:56:43.480503+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run the proposed pipeline on a loop-carried computation, with equality saturation before and after a loop transformation such as unrolling: if the second saturation phase cannot see (or reconstruct) the equalities created in the first, because the intervening transformation destroyed the e-class structure, then the e-graph did not actually persist across the compilation flow.","supporting_citations":[],"review_version":1}