{"id":"abae57f3-76f3-45b5-8a94-3b3258a45a29","arxiv_id":"2506.02290","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"high","formal_verification":"none","parameter_count":0,"one_line_summary":"HEC verifies MLIR program equivalence after control-flow and datapath transformations using hybrid static and dynamic e-graph rewriting, and flags two mlir-opt transformation bugs.","lead":"This paper presents HEC, a tool that checks whether two MLIR programs are functionally equivalent after compiler transformations such as loop unrolling, tiling, and fusion. It uses e-graph rewriting and reports two bugs it found in mlir-opt.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Non-equivalence verdicts for the two mlir-opt bugs rest on saturation failure, not a proof of inequality; the paper's own incompleteness caveat makes these bug-detection claims unsupported without a counterexample witness.","rationale":"The reader's weakest_assumption focuses on the soundness of the dynamic rule conditions (Table 2) for positive equivalence verdicts, which is a real concern. My primary load-bearing concern is different: even if all dynamic rules and their Z3 checks are sound, HEC's negative verdicts for the two mlir-opt bugs are inferred from saturation failure, which is not a proof of non-equivalence. The paper even acknowledges incompleteness, making the negative inference self-undermining. The reader's rationale does mention that \"non-equivalence verdicts are based on saturation failure rather than proofs,\" so there is partial agreement, but the formal weakest_assumption field does not identify this as the central issue. I do not recommend moving the verdict because the paper has genuine strengths: the motivating examples are clear, the static rules are sourced from algebraic identities, the scalability data is concrete, and the two bug reports are plausibly correct as manually argued. The weakness is addressable by adding counterexample witnesses or proof certificates for negative results, which is exactly what a conditional acceptance should demand. Therefore the reader's CONDITIONAL verdict remains appropriate without change.","tokens_in":22840,"tokens_out":4844,"duration_ms":49307,"concrete_test":"Run the two Section 5.4 case studies through HEC with logging of all attempted dynamic rules, and require HEC to return a concrete counterexample witness (e.g., for Case 1, a binding %0=5 with the differing execution counts; for Case 2, the final contents of %arg0 after executing both functions) or an SMT-generated certificate proving semantic inequivalence. If HEC only reports \"not equivalent\" without a witness, the bug-detection claim is not supported by the tool and should be reworded to \"flags suspicious pairs for manual analysis.\"","verdict_should_be":"UNCHANGED","load_bearing_attack":"Section 4.3 states that if saturation terminates with the two programs in different e-classes and the rule generator cannot create new dynamic rules, \"HEC will conclude that the input MLIR codes are not equivalent.\" In an e-graph, a saturation fixpoint with distinct e-classes only proves that the given rule set cannot rewrite the two programs to a common form; it does not prove semantic inequality. The paper itself concedes incompleteness: \"HEC, like any verification system based on rewriting rules, is inherently incomplete.\" Consequently, the negative direction of HEC is unsupported. Both bug reports in Section 5.4 are negative verdicts: the loop-boundary case is reported because the unrolling rule cannot merge the two programs, and the fusion case is reported because the fusion rule's no-RAW condition fails. The textual counterexamples (%0 = 5 for Case 1; the linearly increasing memory sequence for Case 2) are supplied by the authors' manual reasoning, not produced by HEC. Thus the claim that \"HEC identified two critical compilation errors\" is not justified by the tool's own output; at best HEC flags suspicious pairs for human inspection. Until HEC emits a distinguishing witness, or an independently checkable certificate of non-equivalence, for each reported bug, the bug-detection claim rests on an unsound inference.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The manuscript proposes HEC, an equivalence checking framework for MLIR programs built on equality saturation. It converts input MLIR into a graph representation, constructs an e-graph, and applies a hybrid ruleset: 62 static datapath rewriting rules plus dynamic loop transformation rules generated at runtime for unrolling, tiling, fusion, and coalescing. Equivalence is established when the two program roots are united in one e-class after saturation. The paper evaluates HEC on PolyBenchC kernels, reports runtime and e-class scaling for various unrolling and tiling factors, and presents two case studies where mlir-opt transformations (loop unrolling and loop fusion) change program semantics; the paper claims HEC identified these compiler bugs.","tokens_in":23126,"tokens_out":6590,"duration_ms":56174,"significance":"Assuming the dynamic rules are sound and the graph representation faithfully models memory and control flow, HEC is a promising addition to the verification landscape: it targets MLIR directly, combines datapath and loop-level reasoning, and is evaluated on a nontrivial benchmark set and real mlir-opt failures. The two bug case studies are concrete and likely useful to the MLIR community. The main weaknesses are that the dynamic rule conditions and Z3 encoding are under-specified, the negative-verdict inference from saturation failure is not sound as a proof of inequality, and the memory-ordering semantics are not formalized; these issues directly affect the paper's soundness and bug-detection claims.","major_comments":[{"comment":"The tiling pattern's second condition, 'n2 = min(%1 + k1, %2)', is ill-formed because %2 is introduced in the right-hand side as the inner loop induction variable, not as a bound of the transformed loop; as written, the condition cannot be evaluated by Z3 and does not express the usual tiling constraint n2 = min(%1 + k1, n1). Consequently, the manuscript does not contain a precise, checkable specification of the tiling dynamic rule. Please rewrite each condition in Table 2 with all variables explicitly quantified and show the corresponding SMT-LIB encoding, or state that this condition is not enforced and explain how tiling equivalence is checked without it.","section":"Section 4.2, Table 2"},{"comment":"The soundness argument is incomplete. The paper states (Section 4.2) 'we assume that all integrated rewriting rules and transformation patterns are correct' and that Z3 checks whether the input code meets the pattern conditions, but it does not provide a formal semantics for the MLIR affine dialect subset, a definition of what 'k1/k2 times replication' means, or a proof that satisfaction of the pattern conditions implies semantic equivalence for arbitrary loop bodies. In particular, the unrolling and fusion conditions in Table 2 are partly syntactic statements about loop bodies, not arithmetic formulas, so the claim that Z3 verifies the conditions is not substantiated for those parts. Without this formalization, the paper's guarantee that HEC 'will never produce false positives' (Section 4.3) is not established.","section":"Section 4.2 and Section 4.3"},{"comment":"The negative direction is unsound as stated. The paper says that if saturation terminates with the two programs in different e-classes and no new dynamic rule can be created, 'HEC will conclude that the input MLIR codes are not equivalent.' In an e-graph, a saturation fixpoint only proves that the given rewrite rules cannot prove equivalence; without a completeness theorem or a produced counterexample, this is not a proof of semantic inequality. Section 4.3 itself acknowledges HEC is 'inherently incomplete,' which directly contradicts using saturation failure as a non-equivalence verdict.","section":"Section 4.3"},{"comment":"The two reported mlir-opt bugs are presented as detections by HEC, but the manuscript only shows manual counterexamples. For Case study 1, the counterexample %0 = 5 is not output by HEC; for Case study 2, the linearly increasing memory sequence is derived by the authors' reasoning about the two loops. In both cases, the tool's verdict appears to be a saturation failure or a failed dynamic-rule condition, which, per Major Comment 3, does not prove non-equivalence. To support the statement that 'HEC identified two critical compilation errors,' the paper should either augment HEC with a witness generator that produces a concrete distinguishing input along with the expected and observed outputs, or explicitly reframe the contribution as flagging transformations for human inspection rather than automatically identifying bugs.","section":"Section 5.4"},{"comment":"The paper does not explain how memory side effects are modeled in the e-graph. The graph representation records operation order inside a block, but the e-graph data structure represents expressions modulo congruence and does not natively preserve ordering; affine.store is given a 'pseudo output term' to maintain tracking, but the manuscript does not state how loads and stores are ordered or how read-after-write dependencies are detected when the e-graph runner unifies e-classes. Since Case study 2 in Section 5.4 is a memory-ordering bug, this missing formalization is load-bearing for the tool's ability to detect that bug.","section":"Section 4.1"}],"minor_comments":[{"comment":"The phrase 'interchangable' should be spelled 'interchangeable'.","section":"Table 2 heading"},{"comment":"The term 'a rit h_ co ns ta nt_ i1 1)' contains stray spaces and is difficult to read; please correct the formatting.","section":"Listing 7"},{"comment":"The terms 'pseudo combine node' and 'pseudocombine' are used inconsistently; please choose one spelling and apply it consistently.","section":"Section 4.2 and Figure 7"},{"comment":"The affine maps #map1 through #map3 are not explained in the caption or the body text; a brief description of how these maps implement nested unrolling by factors 2 and 3 would improve readability.","section":"Figure 6"},{"comment":"The text says the case studies concern 'optimized HLS programs,' but the transformations in Listings 9-12 are produced by mlir-opt on MLIR kernels, not by an HLS tool; please rephrase to match the experimental setup.","section":"Section 5.4"}],"recommendation":"major_revision","confidential_remarks":"The paper addresses a relevant problem and the evaluation is substantial. The main issue is that the soundness of the negative direction and the formalization of the dynamic rules need work, but these appear addressable within the manuscript's scope. The two bug reports are the most valuable part of the paper; providing HEC-generated witnesses or clearly reframing them as human-in-the-loop findings would resolve my main concern."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague,\n\nThe paper is worth a look, but the bug-detection claims need to be read with a dose of salt. The genuinely new piece is the hybrid rule set: static datapath rewriting plus dynamic loop-transformation rules generated at runtime inside an e-graph. That combination is not in the cited prior work, and the graph representation that unifies variable renaming and loop decomposition is a reasonable engineering contribution. The two bug case studies (loop boundary in unrolling, RAW violation in fusion) are real, and the manual analysis in Section 5.4 is convincing.\n\nThe soft spots are where the claims outrun the evidence. First, the negative verdict is unsound: HEC concludes \"not equivalent\" when saturation reaches a fixpoint without merging the two programs. That proves nothing about semantics; the paper even concedes incompleteness. So saying HEC \"identified\" the bugs overstates what the tool does. It flags candidates; the counterexamples come from the authors' manual reasoning. That is the crux, and it should be reframed as \"bug hunting\" with human confirmation, or paired with a witness generator.\n\nSecond, the dynamic rule conditions in Table 2 are under-specified. Tiling has \"n2 = min(%1 + k1, %2)\" with %2 undefined. The unrolling replication condition is hand-wavy. Z3 can only check what is formalized; without a precise encoding, the soundness claim is unsubstantiated.\n\nThird, there is no artifact. For a tool paper, that is a big omission — no code, no benchmark scripts, no way to reproduce the 108,000 LOC result. I would not accept claims of performance or bug detection without that.\n\nThat said, the core method is promising, and the authors are transparent about the incompleteness. The paper deserves serious peer review, but it needs major revision: sharpen the rule formalization, either implement a witness-based inequality check or change the language to \"reports potential non-equivalence\", and release the artifact. As it stands, I would not rely on its negative results, but the positive verification results (tiling, unrolling, fusion with existing rules) are plausible. For a compiler verification reading group, it's a good basis for a discussion about what counts as a proof of inequality in e-graph systems.\n\nRecommendation: send to peer review, but expect heavy revision.","headline":"Hybrid static/dynamic e-graph rewriting is a real novelty, but the two 'identified' mlir-opt bugs rest on saturation failure rather than a proof of inequality, and the rule conditions are not formalized enough to support the soundness claims.","tokens_in":23630,"tokens_out":3774,"would_cite":true,"duration_ms":34298,"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":"Hybrid e-graph rules verify MLIR rewrites and expose two optimizer bugs","keywords":["equivalence checking","e-graph","equality saturation","MLIR","loop unrolling","loop tiling","loop fusion","compiler bug detection"],"falsifier":"Instantiate Listing 9 and its unrolled Listing 10 with %0 = 5, execute both, and compare HEC's verdict with observed behavior: the original loop runs zero iterations while the unrolled version runs one, so any 'equivalent' verdict from HEC would refute its soundness guarantee.","tokens_in":22641,"feed_emoji":"🐛","tokens_out":6675,"duration_ms":55724,"temperature":0.7,"pith_summary":"HEC is a verification tool that checks whether a transformed MLIR program is functionally equivalent to its original by encoding both programs in an e-graph and saturating it with rewriting rules. The paper claims this covers datapath transformations through static algebraic rules and control-flow transformations such as unrolling, tiling, and fusion through rules generated dynamically for each input. On PolyBenchC benchmarks, HEC verifies these transformations in minutes and scales to more than 100,000 lines of MLIR in about 40 minutes. The practical payoff is that HEC caught two real mlir-opt bugs: an unrolling boundary error that executes iterations it should not, and a loop-fusion read-after-write violation that changes program results.","feed_headline":"E-graph checker verifies MLIR rewrites, exposes two optimizer bugs","feed_subtitle":"HEC unifies static datapath and dynamic loop rules in one saturation engine, catching real unrolling and fusion errors in mlir-opt.","key_machinery":"The e-graph (equivalence graph) is the central object: a compact data structure whose nodes are expressions and whose equivalence classes are closed under congruence, allowing many equivalent program forms to be represented and unified simultaneously. HEC builds this graph from a custom MLIR graph representation that renames variables globally, decomposes each for loop into a loop-value component and an order-sensitive block, and tracks pseudo outputs for stores. The argument is carried by a hybrid ruleset: 62 static datapath rewrite rules, plus dynamic rules produced at runtime for control-flow patterns such as unrolling, tiling, fusion, and coalescing, with pattern conditions discharged by Z3. The machinery turns program equivalence into e-class membership after saturation, because any sequence of sound rewrites that unifies the two programs in one equivalence class witnesses their functional equivalence.","core_discovery":"The central claim is that holistic equivalence checking of source-to-source transformations can be reduced to equality saturation over a graph representation of MLIR, provided the rule set is hybrid: static rewrite rules for datapath identities plus dynamic rules synthesized per input for loop transformations. The discovery HEC embodies is that control-flow transformations, normally hard to express as static term rewrites because their parameters and introduced variables are runtime-dependent, can be handled by a rule generator that inspects the input's graph representation, emits code-specific rewriting patterns, and checks the patterns' conditions with the Z3 SMT solver. On this basis, HEC reports functional equivalence when the original and transformed programs end up in the same e-class, and the paper demonstrates this on loop unrolling, tiling, and fusion over PolyBenchC, including nested unrolling. The paper further claims that this verification caught two genuine compiler bugs in mlir-opt: loop boundary errors in unrolling that cause unintended executions, and a loop-fusion read-after-write violation that alters memory state.","pith_inferences":["The informal dynamic-rule conditions in Table 2 are not a complete formal specification; in particular the tiling condition prints as \"n2 = min(%1 + k1, %2)\" with %2 undefined, so the soundness guarantee for loop transformations would need a repaired formalization before being relied on.","The same saturation machinery could be run in reverse as a synthesis engine: after equivalence is established, extracting the cheapest program from the saturated e-graph would yield an optimization, not just a verification.","The unrolling boundary bug suggests a cheap fuzzing strategy for MLIR: generate loops with symbolic bounds where the start can exceed the end and check that unrolled versions execute exactly the same trip count.","Since HEC's graph representation automatically normalizes loop-body-independent hoisting, it may already cover invariant-code-motion-style rewrites that the paper does not list as separate patterns."],"forward_implications":["MLIR affine-dialect pass developers can use HEC as a regression oracle, since it checks whole transformations rather than single rewrites.","Equivalence checking no longer needs separate tools for control flow and datapath; one saturated e-graph can witness both at once.","The reported bugs mean mlir-opt's unrolling can add iterations when the loop start exceeds the end, and its fusion can reorder memory accesses illegally, so users of these default passes should guard those cases.","The dynamic-rule design makes the verifier extensible: adding a new loop transformation only requires formalizing its pattern and conditions."],"supporting_citations":[{"why":"Supplies the egg equality-saturation engine that HEC uses to build and saturate the e-graph.","marker":"[53]"},{"why":"Defines equality saturation, the optimization technique HEC adapts for equivalence checking.","marker":"[46]"},{"why":"PolyCheck, the prior affine-only verifier whose limited scope motivates HEC's holistic design.","marker":"[7]"},{"why":"MLIR-TV, the prior MLIR-level verifier that fails to support the affine dialect and is HEC's comparison point.","marker":"[6]"},{"why":"Defines the MLIR infrastructure that serves as HEC's frontend and input language.","marker":"[29]"},{"why":"Polygeist, used to convert the PolyBenchC C code into MLIR for evaluation.","marker":"[35]"},{"why":"Provides the Z3 SMT solver used to check the conditions of dynamic loop-transformation rules.","marker":"[20, 21]"},{"why":"Supplies the PolyBench benchmark suite used for unrolling and tiling experiments.","marker":"[40]"},{"why":"Supplies the CNN-forward benchmark from PolyBench-NN included in the evaluation.","marker":"[50]"}],"fun_headline_variants":["E-graph equivalence checking catches two mlir-opt bugs","Hybrid e-graph rewriting verifies loop transformations, finds bugs","HEC: equality saturation proves MLIR transforms, exposes errors","Same e-class, same program: HEC checks code transformations","E-graph checker validates unrolling, fusion; finds real compiler bugs"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The soundness of every loop-transformation verdict rests on the correctness of the dynamic rules in Table 2 and of the Z3 encoding of their conditions; those conditions are stated informally, and one tiling condition in the paper references an undefined variable.","fun_headline_variants_meta":{"raw":{"variants":["E-graph equivalence checking catches two mlir-opt bugs","Hybrid e-graph rewriting verifies loop transformations, finds bugs","HEC: equality saturation proves MLIR transforms, exposes errors","Same e-class, same program: HEC checks code transformations","E-graph checker validates unrolling, fusion; finds real compiler bugs"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000242,"raw_usage":{"total_tokens":1554,"prompt_tokens":1000,"completion_tokens":554,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":616,"completion_tokens_details":{"reasoning_tokens":465}},"tokens_in":616,"tokens_out":554,"duration_ms":4460,"temperature":1.0,"reasoning_tokens":465,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-07T11:27:01.517183+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Instantiate Listing 9 and its unrolled Listing 10 with %0 = 5, execute both, and compare HEC's verdict with observed behavior: the original loop runs zero iterations while the unrolled version runs one, so any 'equivalent' verdict from HEC would refute its soundness guarantee.","supporting_citations":[{"cited_title":"Egg: Fast and extensible equality saturation","cited_arxiv_id":null,"evidence_quote":"Supplies the egg equality-saturation engine that HEC uses to build and saturate the e-graph."},{"cited_title":"Equality saturation: a new approach to optimiza- tion","cited_arxiv_id":null,"evidence_quote":"Defines equality saturation, the optimization technique HEC adapts for equivalence checking."},{"cited_title":"Polycheck: Dynamic verification of iteration space transformations on affine programs","cited_arxiv_id":null,"evidence_quote":"PolyCheck, the prior affine-only verifier whose limited scope motivates HEC's holistic design."},{"cited_title":"Smt-based trans- lation validation for machine learning compiler","cited_arxiv_id":null,"evidence_quote":"MLIR-TV, the prior MLIR-level verifier that fails to support the affine dialect and is HEC's comparison point."},{"cited_title":"Mlir: Scaling compiler infrastructure for do- main specific computation","cited_arxiv_id":null,"evidence_quote":"Defines the MLIR infrastructure that serves as HEC's frontend and input language."},{"cited_title":"Polygeist: Raising c to polyhedral mlir","cited_arxiv_id":null,"evidence_quote":"Polygeist, used to convert the PolyBenchC C code into MLIR for evaluation."},{"cited_title":"Polybench: The poly- hedral benchmark suite","cited_arxiv_id":null,"evidence_quote":"Supplies the PolyBench benchmark suite used for unrolling and tiling experiments."},{"cited_title":"Polybench-nn","cited_arxiv_id":null,"evidence_quote":"Supplies the CNN-forward benchmark from PolyBench-NN included in the evaluation."}],"review_version":1}