{"id":"d01d7324-3d2a-491f-81cf-6cb1c63cf4d8","arxiv_id":"2506.12760","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":5.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"IDOL detects Solidity compiler optimization errors by differentially compiling semantically equivalent contract variants and found three confirmed bugs.","lead":"This paper proposes IDOL, a testing method for the Solidity compiler that rewrites smart contracts into semantically equivalent forms to expose optimization bugs. The authors report that IDOL found three confirmed compiler bugs across 160,000 generated contracts.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Semantic-equivalence assumption for the reverse transformations is unvalidated, and the three reported bugs lack reproducers or bug IDs, so the central claim cannot be independently confirmed from the preprint.","rationale":"The reader's weakest assumption—that the reverse transformations preserve exact semantics—is indeed the most load-bearing point. If a transformation changes behavior, the observed optimization-level discrepancy could be caused by the transformation itself, invalidating all three bug reports. The reader further notes the lack of artifact and reproducers, which compounds the issue. My stress-test concurs with this reading and with the CONDITIONAL verdict. The paper's central claim is plausible and the approach is a reasonable extension of DOL, but the lack of transformation specifications, semantic-equivalence validation, and reusable evidence for the 'confirmed' bugs prevents independent verification. A CONDITIONAL verdict is appropriate: acceptance should be contingent on the authors releasing minimized test cases, bug IDs, solc versions, and either a formal or empirical demonstration that the transformations preserve semantics. The concrete test I propose would settle whether the concern actually lands: disable optimization entirely and compare original versus transformed contracts; if they differ, the transformation is the cause, not the compiler. This directly tests the weakest assumption without requiring a full formal proof. The verdict remains UNCHANGED because my concern aligns with the reader's and does not alter the recommended conditionality.","tokens_in":3222,"tokens_out":2822,"duration_ms":38650,"concrete_test":"Obtain the three minimized test programs that trigger the reported bugs. For each, compile the original and the reverse-transformed variant with solc using `--optimize=false` and execute both on the same inputs; if any output differs, the transformation is not semantics-preserving. Then check the Solidity issue tracker for the reported bugs: if issue numbers and affected solc versions are supplied, re-run the reproducer on an unaffected version to confirm the bug is compiler-caused and not an artifact of the transformation. Also run the original DOL approach on the same transformed variants without the reverse transformation to verify that the bugs are indeed missed by DOL.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim is that IDOL finds three Solidity compiler optimization bugs that standard DOL misses. This claim depends on two linked assumptions: (1) the reverse optimization transformations preserve exact program semantics, and (2) the observed output discrepancies are genuine compiler bugs rather than artifacts of the transformations. The paper asserts semantic preservation in Section 2, 'without altering the program semantics,' but gives no formal argument or empirical check. The two example transformations (loop-invariant code motion, loop inversion) are only described informally; no conditions are stated under which they are safely applicable. For instance, moving `x = y + z` out of a loop is only valid if `y` and `z` are not modified by any loop iteration; if Solsmith-generated contracts contain such modifications, the 'equivalent variant' would change behavior, and a differential output would be a false positive. Likewise, loop inversion into an `if`-`do..while` form is generally valid, but the paper gives no detail on how loops with `break`/`continue` or side-effecting conditions are handled. The three reported bugs are each described in a single sentence, with no solidity version, no minimized input, no issue tracker reference, no executable artifact, and no evidence of how the bugs were 'confirmed.' Because the manuscript provides no way to reproduce the discrepancies or to verify that the variants are semantically equivalent, the comparison between IDOL and DOL is not auditable. Without this evidence, the central claim could be true but remains unverified, or the reported bugs could be caused by the transformation tool rather than the compiler.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"IDOL is a differential testing method for the Solidity compiler. Starting from contracts generated by Solsmith, it applies transformations that are the reverse of known compiler optimizations (e.g., moving loop-invariant code back into the loop and converting a do-while back into a while loop) to create semantically equivalent variants, then compiles and runs each variant under three solc configurations (--optimize=false, --optimize-runs=1, and --optimize-runs=200) and compares execution outputs. The paper reports a preliminary evaluation of 160,000 Solsmith-generated programs in which IDOL found three compiler optimization bugs, named Keccak cache, traditional code-generation pipeline, and FullInliner parameter evaluation order, and states that the original DOL approach did not detect these bugs. The contribution is a heuristic for increasing the chance that differential testing triggers compiler optimization logic, with the central claim being that this heuristic finds real Solidity compiler bugs that plain DOL misses.","tokens_in":3482,"tokens_out":5474,"duration_ms":60785,"significance":"If the three reported bugs are genuine and reproducible, the result is a useful and credible data point: IDOL is a lightweight extension of DOL, built on top of an existing contract generator, and it found optimization bugs that plain DOL missed on the same corpus. The method has no fitted parameters, and the differential oracle is external (comparing solc behavior at different optimization levels), so the core design is not circular. However, the evidence in the manuscript is at the level of a preliminary report: none of the three bug descriptions includes enough information to be independently reproduced, and there is no false-positive analysis, no trigger-rate measurement, and no validation that the reverse transformations preserve semantics on the executed inputs. The contribution is therefore plausible but not yet established at the standard of a full research paper.","major_comments":[{"comment":"The semantic-equivalence assumption is the load-bearing premise of IDOL, but the paper provides only informal examples and no side conditions. Loop-invariant code motion is valid only if the moved computation (e.g., x = y + z and x * x in Figure 1) has no operands modified in the loop and no side effects; loop inversion as shown in Figure 2 is not semantics-preserving for arbitrary while loops containing break, continue, or conditions with side effects. The manuscript never explains how the transformations are guarded, nor does it report any validation (e.g., differential execution of the original and variant at the same optimization level) that the generated variants are equivalent on the executed inputs. Without such validation, an output discrepancy could be caused by the transformation itself rather than by a compiler bug, which would make the three reported bugs false positives.","section":"Section 2, Figures 1 and 2"},{"comment":"The three central bug reports are single-sentence descriptions with no solc version, no minimized contract, no issue-tracker identifier, no diff of the affected bytecode, and no executable reproducer. Since the claim that these are 'confirmed' bugs is the paper's main evidence of effectiveness, these details must be supplied (or provided in a supplementary artifact) before the claim can be independently checked. The phrase 'at the time of writing' in the abstract and in Section 3 is also not verifiable; the authors should name a specific solc release and provide linkable bug reports.","section":"Section 3, bug descriptions"},{"comment":"The comparison with the original DOL approach is under-specified. The paper reports only that DOL 'does not detect' the three bugs on the same 160,000 programs; it does not state how many test executions or output comparisons were performed, how many discrepancy candidates DOL found, whether the same compilation and execution oracle was used for both methods, or how many IDOL variants were generated per original program. Reporting trigger rates and the total number of discrepancy candidates for both methods would let the reader judge whether the improvement is real or an artifact of small numbers.","section":"Section 3, final paragraph"},{"comment":"The testing process is described only at the level of a flow diagram: 'Compilation and Deployment' and 'Test Results' are mentioned, but the paper never defines what is executed (which functions, with what arguments and transaction sequence) or how output results are compared. This missing oracle definition makes the experiment impossible to reproduce from the manuscript text alone, and it also leaves unspecified how discrepancies are triaged. The authors should state the exact comparison procedure and the criterion for classifying a discrepancy as a confirmed compiler bug.","section":"Section 3, Figure 3"}],"minor_comments":[{"comment":"The text 'sloc compiles them' appears to be a typo; it should read 'solc compiles them'.","section":"Section 3, first paragraph"},{"comment":"The labels 'Optimization Level L1' and 'Optimization Level L2' are undefined; the paper should map these to the three concrete configurations (--optimize=false, --optimize-runs=1, --optimize-runs=200) described in Section 2.","section":"Figure 3"},{"comment":"Reference [3] is missing a publication venue and year, and reference [4] appears to be a preprint or accepted paper with no bibliographic details; both should be completed for reproducibility of the related-work discussion.","section":"References"},{"comment":"The name 'Traditional Code Generation Pipeline Bug' is vague and does not identify a specific solc component or optimization pass; consider using a more precise description or the actual issue title if the bug is tracked.","section":"Section 3, bug names"}],"recommendation":"major_revision","confidential_remarks":"The paper reads like a short or workshop-style report, and the core idea is reasonable. The missing artifacts and equivalence validation are fixable in revision, but for a journal-level claim of 'confirmed compiler bugs', the authors should link to actual issue-tracker entries, provide minimized reproducers, and formalize or empirically validate the transformation guards. If those artifacts cannot be provided, the claims should be downgraded to 'potential discrepancies' rather than 'confirmed bugs'."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague,\n\nThis is a short preprint on differential testing of the Solidity compiler. The new bit is concrete: take Solsmith-generated contracts, apply reverse optimization transformations (loop-invariant code motion, loop inversion, a few Solidity-specific ones), compile at different optimization levels, and compare execution results. The authors report three confirmed optimizer bugs that plain DOL misses on the same 160k programs. If true, that is a useful result for the compiler-testing community.\n\nCredit where due: the two worked examples are clear, the control comparison with DOL is the right experiment, and the three bug descriptions are plausible (Keccak caching, a code-generation pipeline issue, and a FullInliner evaluation-order problem). The paper also cites the prior optimization-guided equivalence work [4] rather than pretending the idea is new. That is honest scholarship.\n\nThe soft spots are real and fairly large. The evaluation is three single-sentence bug reports with no solidity version, no minimized input, no issue tracker ID, no artifact, and no trigger-rate or false-positive analysis. The semantic-equivalence assumption is asserted, not demonstrated. For loop-invariant code motion, moving `x = y + z` out of the loop is only valid if `y` and `z` are not modified by any iteration; the paper never states the safety conditions or how loops with break/continue or side-effecting conditions are handled. A differential output could therefore be an artifact of the transformation rather than a compiler bug. That is the load-bearing weakness, and the stress-test note is right to put it at the center.\n\nThe central argument does not collapse, though. The method is a straightforward extension of an established paradigm, and the bugs could well be genuine. But as a standalone preprint, the evidence is too thin for an independent reader to confirm the claim. The authors call it preliminary; I agree.\n\nWho is this for? People working on compiler testing or Solidity tooling. A serious referee could help by pushing for an artifact and precise transformation semantics. I would not desk-reject it, but I would expect heavy revision. If the authors ship the code and reproducers, this becomes a genuinely useful data point.\n\nRecommendation: send to peer review with a request for artifact evaluation. My own verdict is conditional: I'd want to see the missing materials before citing it as evidence.\n\nBest,\n[You]","headline":"A plausible Solidity-specific extension of DOL testing with three reported compiler bugs, but the preprint gives too little detail to verify the central claim; worth sending to review only if the authors can supply artifacts and precise transformation rules.","tokens_in":4002,"tokens_out":1661,"would_cite":true,"duration_ms":22278,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"Rewriting Solidity contracts back into unoptimized form before differential compilation exposes three real compiler optimization bugs.","keywords":["Solidity compiler testing","smart contracts","different optimization levels","differential testing","compiler optimization bugs","semantic equivalence","reverse optimization transformations","blockchain"],"falsifier":"Take any one of the three reported bugs, compile the same variant with optimization disabled, and compare its execution result with the original untransformed contract also compiled with optimization disabled; any difference in behavior between variant and original would show that a transformation changed semantics, making the reported bug a false positive rather than a compiler defect.","tokens_in":3046,"feed_emoji":"🐞","tokens_out":4515,"duration_ms":46135,"temperature":0.7,"pith_summary":"IDOL tests the Solidity compiler by generating smart contracts, rewriting each into a semantically equivalent \"unoptimized\" form that mirrors the input side of a compiler optimization, and then compiling and executing the variant under different optimization levels. The paper's claim is that this reverse-optimization step forces the compiler to re-run optimization logic in ways that ordinary different-optimization-level (DOL) testing does not, thereby finding bugs DOL would miss. In a preliminary run over 160,000 generated contracts, IDOL found three confirmed optimization bugs, and the same set of contracts tested with plain DOL detected none of them. If the claim holds, IDOL is a practical way to surface optimization defects in a widely deployed compiler for immutable blockchain contracts.","feed_headline":"Reverse-optimized contracts expose 3 Solidity compiler bugs","feed_subtitle":"Mutating contracts into pre-optimization form catches bugs that ordinary optimization-level testing misses.","key_machinery":"The engine of IDOL is the reverse optimization transformation: a rewrite that takes a code shape that looks like the output of an optimization and turns it back into the unoptimized input shape, for example moving a loop-invariant computation back inside a loop, or converting an inverted loop back into a plain while loop. These rewrites are claimed to preserve the contract's semantics exactly, while presenting the compiler with code that is not already in optimized form. When the compiler is then run with different --optimize settings, the variant forces it to perform the corresponding optimization from scratch, maximizing the chance that a defect in that optimization path will produce an observable output difference.","core_discovery":"The paper's central discovery is stated in Section 3: over 160,000 test programs generated from Solidity contracts, IDOL identified three confirmed compiler optimization bugs, whereas the original DOL approach detected none of these three. The three bugs are the optimizer Keccak cache bug, the traditional code generation pipeline bug, and the FullInliner non-expression split parameter evaluation order bug. Each shows up only when a semantically equivalent variant, created by reversing a known optimization (such as loop-invariant code motion or loop inversion), is compiled and executed at different optimization settings. The author's conclusion is that deliberately feeding the optimizer its own \"input side\" expands the set of triggerable optimization paths.","pith_inferences":["Editorial inference: the same reverse-optimization recipe should transfer to other smart-contract compilers, such as Vyper, or to general-purpose compilers if the transformation rules are instantiated per target.","Editorial inference: because the paper does not prove semantic equivalence, a fair re-check should run each variant against its original under identical settings; until then the three bug reports carry a hidden assumption.","Editorial inference: the number of bugs found could be used as a rough sensitivity measure, and expanding the rule set with more Solidity-specific reverse transformations should raise the hit rate; this is testable by rerunning IDOL with an expanded rule set."],"forward_implications":["IDOL can serve as an oracle-free testing pipeline for Solidity compiler releases, since it requires no hand-written expected outputs.","The three confirmed bugs point to concrete defect-prone optimizer components: Keccak caching, the traditional code-generation pipeline, and FullInliner expression splitting.","Compiler developers can add IDOL-generated variants to regression suites to prevent these classes of miscompilation from reappearing.","The results suggest that reverse optimization transformations increase the diversity of optimization-triggering inputs compared with raw generated programs."],"supporting_citations":[{"why":"Defines different optimization level (DOL) testing and provides the empirical baseline that IDOL is compared against.","marker":"[5]"},{"why":"Motivates optimization-guided equivalence transformations, which IDOL reverses to generate test variants.","marker":"[4]"},{"why":"Introduces randomized differential testing, the underlying oracle-free testing strategy that IDOL builds on.","marker":"[3]"}],"fun_headline_variants":["Reverse-optimizing Solidity contracts finds 3 compiler bugs","IDOL: Flipping compiler optimizations to uncover 3 Solidity bugs","3 Solidity compiler bugs found via reverse-optimization testing","Reverse optimization transforms expose 3 Solidity compiler bugs","Feeding Solidity compilers their own optimizations finds 3 bugs"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The method assumes that the reverse optimization transformations never change the behavior of a contract, including edge cases like overflow, gas, and storage, so any output difference must come from the compiler.","fun_headline_variants_meta":{"raw":{"variants":["Reverse-optimizing Solidity contracts finds 3 compiler bugs","IDOL: Flipping compiler optimizations to uncover 3 Solidity bugs","3 Solidity compiler bugs found via reverse-optimization testing","Reverse optimization transforms expose 3 Solidity compiler bugs","Feeding Solidity compilers their own optimizations finds 3 bugs"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000727,"raw_usage":{"total_tokens":3215,"prompt_tokens":860,"completion_tokens":2355,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":476,"completion_tokens_details":{"reasoning_tokens":2263}},"tokens_in":476,"tokens_out":2355,"duration_ms":16340,"temperature":1.0,"reasoning_tokens":2263,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-07T00:42:27.072643+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take any one of the three reported bugs, compile the same variant with optimization disabled, and compare its execution result with the original untransformed contract also compiled with optimization disabled; any difference in behavior between variant and original would show that a transformation changed semantics, making the reported bug a false positive rather than a compiler defect.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Defines different optimization level (DOL) testing and provides the empirical baseline that IDOL is compared against."},{"cited_title":"Groce et al","cited_arxiv_id":null,"evidence_quote":"Motivates optimization-guided equivalence transformations, which IDOL reverses to generate test variants."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Introduces randomized differential testing, the underlying oracle-free testing strategy that IDOL builds on."}],"review_version":1}