{"id":"4aec5bc1-633c-402a-b2ab-0683088cf8a7","arxiv_id":"2509.09019","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":1,"one_line_summary":"The paper mechanizes in Vellvm/Rocq a correctness proof that the FMA intrinsic for a*b+c refines separate multiply then add within an epsilon error bound.","lead":"This paper describes a prototype proof in the Rocq theorem prover that LLVM's FMA optimization for the expression a*b+c is correct up to a rounding error bound. It is an early step toward verified fast-math optimizations for scientific computing compilers.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"double_refine is vacuously true for NaN/Inf, so the main lemma gives no guarantee in the non-finite cases where fast-math diverges.","rationale":"The reader correctly identified the finiteness restriction as the weakest assumption, but slightly mischaracterized its effect: for non-finite inputs double_refine does not return False; it holds vacuously because the finite premise is false. This sharpens the concern and makes it more central: the theorem does not just fail to cover non-finite cases, it certifies them without any value comparison. For a translation-validation setting, that is a real weakness if the optimization is applied without a separate finiteness guard. However, the paper is explicitly preliminary, scopes its contribution to finite inputs in multiple places, and is transparent about manual steps and missing automation. Therefore the concern supports, but does not move, the reader's CONDITIONAL verdict; it should be addressed by adding a finiteness precondition to the theorem or by treating non-finite behavior explicitly, and by releasing the Rocq proof artifact.","tokens_in":673,"tokens_out":2406,"duration_ms":158914,"concrete_test":"In the Rocq development, run: `Goal double_refine (UVALUE_Double NaN) (UVALUE_Double NaN). intros [H _].` (or the analogous script for two different non-finite values). If the goal closes trivially from the falsified finiteness premise, then double_refine holds for NaN regardless of the epsilon bound, confirming the vacuity.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The formal claim rests on Lemma fma_optim_correct (Fig. 5), whose value relation double_refine (Fig. 4) is, for UVALUE_Double p1 p2, the implication `is_finite p1 = true ∧ is_finite p2 = true ∧ is_finite (p1 ⊖ p2) = true -> |p1 ⊖ p2| ≤ epsilon_FMA`. When either value is NaN or ±Inf, or when the subtraction overflows, the premise is false, so the implication is trivially inhabited and double_refine holds without comparing the two results at all. Since fma_optim_correct has no finiteness hypothesis on the initial environment, it accepts the FMA/non-FMA pair even when the two computations return different non-finite values. This is not merely an excluded case; it is vacuous acceptance in exactly the NaN/Inf regime the paper motivates in Sec. 1 as risky for fast-math. The finite-value bound is also not machine-checked: epsilon_FMA is only given informally with free δ/ε in Sec. 3.4, and no Flocq derivation or proof artifact is shown.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper reports preliminary work toward verified floating-point optimization in the LLVM setting, specifically the FMA transformation of the expression a*b+c. It uses the Rocq/Coq Vellvm framework, ITrees for program denotations, and Flocq for floating-point semantics. The authors define LLVM IR blocks for the FMA and non-FMA versions, give semantics for the llvm.fmuladd.f64 intrinsic, and state a lemma fma_optim_correct claiming an eutt refinement between the two blocks under a value relation double_refine. The intended contribution is a translation-validation-style correctness proof for this one optimization, with a roadmap for generalizing to other fast-math transformations and larger programs.","tokens_in":8109,"tokens_out":3147,"duration_ms":40704,"significance":"If fully realized, this line of work would fill a real gap: Crellvm and similar frameworks have not been extended to floating-point fast-math optimizations, and the new Vellvm infrastructure is a natural basis. The paper's strengths are its use of ITrees/eutt for compositional reasoning, the reuse of Flocq for IEEE-754 semantics, and a concrete statement of what correctness should mean (returned values within an error bound). It is also honest about being preliminary. However, as submitted, the central lemma is not accompanied by a machine-checked proof, no artifact is provided, and the refinement relation is vacuously true for the non-finite cases that the paper itself identifies as the risky ones. The significance of the contribution depends on completing and checking those parts.","major_comments":[{"comment":"The definition of double_refine for UVALUE_Double p1 p2 is an implication with hypothesis is_finite p1 = true ∧ is_finite p2 = true ∧ is_finite (p1 ⊖_{RNE} p2) = true. When either value is NaN or ±Inf, or when the subtraction overflows, the hypothesis is false and the implication holds trivially. The main lemma fma_optim_correct is stated for arbitrary initial environments g l, with no finiteness side condition, so it accepts the FMA/non-FMA pair even when the two computations return different non-finite values. This is not an excluded case: it is vacuous acceptance in exactly the NaN/Inf regime that Section 1 motivates as dangerous for fast-math. The theorem should either include explicit finiteness hypotheses on all inputs and intermediate operations, or double_refine should be extended to require equality (or some meaningful relation) for non-finite values.","section":"§3.4, Fig. 4; §3.6, Fig. 5"},{"comment":"The proof of fma_optim_correct is only sketched: the text says that after desugaring interpretation levels, the relational principle eutt_Ret is applied to conclude the equivalence, and that local_refine and double_refine are established. No Rocq script, proof term, or artifact is provided. A reader cannot verify that the proof actually goes through in the current Vellvm version, in particular the alignment of the one FMA write with the two non-FMA writes and the use of Flocq's FMA correctness lemma. For a claim of 'verified compilation', the machine-checked proof is load-bearing and must be supplied.","section":"§3.6, Fig. 5"},{"comment":"The error bound epsilon_FMA is stated informally as (|a*b*c|δ+ε+|a*b|*(2δ+δ^2)+ε*(1+δ)+|c|*δ+ε)(1+δ)+ε, with free symbols δ and ε. It is not derived in the text, no Flocq lemmas are cited for its derivation, and it is not clear how δ and ε are instantiated for RNE double precision. The refinement relation is defined in terms of this bound, so the main lemma is only as meaningful as this bound. A formal derivation of the bound, or at least a precise statement of the error model and a pointer to the mechanized proof, is needed.","section":"§3.4"},{"comment":"The local_refine relation manually fixes the alignment between the FMA block's write to %4 and the non-FMA block's writes to %4 and %5. The paper acknowledges this is manual, and it is a reasonable first step. But for a translation-validation claim, the alignment relation is part of the correctness criterion: choosing it by hand means the theorem only shows equivalence under that particular mapping, and the mapping itself is not justified by the compiler's behavior. If the alignment is meant to be derived automatically in the future, the current proof should at least state this as a limitation in the main theorem, not only in future work.","section":"§3.5, Fig. 4"}],"minor_comments":[{"comment":"Several typos and small formatting issues: 'Fortan' should be 'Fortran'; 'acrp' should likely be 'arcp'; 'relationallogic' appears without a space; the δ−ε model notation in Section 2.3 is not typeset consistently.","section":"Throughout"},{"comment":"The expression for epsilon_FMA mixes the symbol ε as an error-model term and as the name of the overall bound. This makes the formula hard to read. Please use distinct names, e.g., epsilon_model and epsilon_FMA, and state the rounding mode explicitly for every operation.","section":"§3.4"},{"comment":"The semantic function llvm_fmuladd_f64 uses b64_fma with FT_Rounding but the refinement relation in Section 3.4 fixes rounding to RNE. The connection between FT_Rounding and the RNE hypothesis in double_refine should be made explicit.","section":"§3.2 / Fig. 3"},{"comment":"In the Vellvm block definitions, the identifiers a, b, c are declared as Variables but are used as EXP_Double constants in the instruction list. It would be clearer to state explicitly that these model the block's input values and how they are related to the actual LLVM function arguments.","section":"Fig. 2"}],"recommendation":"major_revision","confidential_remarks":"This is a preliminary work-in-progress report. The main correctness lemma is not fully verified in the manuscript and no artifact is included. The vacuous-truth issue for NaN/Inf is a correctness-relevant gap, not a presentation issue. I would require the authors to provide the complete Rocq development, including the formal error-bound derivation and a corrected theorem statement with appropriate finiteness or non-finite handling, before this can be accepted. If the venue explicitly encourages early reports, a major revision with the artifact would be appropriate."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Candidly: this is a genuine first step, but the proof as stated is weaker than the abstract suggests. The new piece is adding a fmuladd intrinsic to Vellvm, defining double_refine with an epsilon bound, and stating an eutt lemma relating an FMA block to a non-FMA block. That is real groundwork: it shows how to use Vellvm's interaction trees and Flocq's FP semantics together, and the paper is honest that this is a basic-block, single-optimization proof.\n\nThe main soft spot is the one the stress-test flagged, and it holds up. double_refine for doubles is an implication: if p1, p2, and their RNE subtraction are all finite, then the error bound holds. For NaN or Inf, the premise is false, so the implication is true no matter how different the two results are. The main lemma fma_optim_correct has no finiteness precondition, so it accepts pairs of computations that return completely different non-finite values. That isn't a harmless exclusion; it weakens the central claim in exactly the regime fast-math is known to be risky. The authors do mention the finiteness assumption in Section 3.6, so they are aware of it, but they don't address the vacuity.\n\nThe other gap is that the core proof is not actually shown. The error bound epsilon_FMA is stated informally with no Flocq derivation, and there is no artifact or Coq script. The eutt_Ret step is sketched. For a paper whose headline is a mechanized correctness result, that's a substantial omission.\n\nThat said, the paper doesn't overclaim. It calls itself preliminary, and the approach is sound for finite inputs, modulo the missing script. The alignment predicate is manual, and they say so. So I'd treat this as a foundation, not a verified result.\n\nThe reader's conditional verdict is about right. The stress-test shows a real, fixable flaw: add a finiteness precondition to the lemma or strengthen the relation so non-finite results must match exactly. And ship the proof.\n\nFor a reading group, it's a maybe — good for discussing what 'correctness' means for FP optimizations. I wouldn't cite it as a verified result, but I might cite it as prior work on Vellvm FP extensions.\n\nRecommendation: a serious referee should see this, but only with the expectation that the authors supply the actual proof and either fix the NaN/Inf gap or clearly state the theorem only covers finite executions. It is not desk-reject material, but it is not ready as-is.","headline":"A useful preliminary Vellvm/FMA proof sketch, but the refinement relation is vacuously true for NaN/Inf and the core proof isn't actually shipped.","tokens_in":8527,"tokens_out":2596,"would_cite":false,"duration_ms":30737,"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":"A machine-checked proof in a theorem prover establishes that LLVM's fused multiply-add optimization is correct for finite double-precision inputs, with results guaranteed to lie within a derived round-off error bound.","keywords":["floating-point correctness","fused multiply-add","compiler optimization verification","interaction trees","refinement relations","translation validation","fast-math optimizations","round-off error bounds"],"falsifier":"Enumerate or sample all finite double-precision triples (a,b,c) for which a*b and (a*b)+c are also finite, and verify that |fma(a,b,c) - round(round(a*b)+c)| <= epsilon_FMA under round-to-nearest-ties-to-even rounding; any violating triple would refute the lemma as stated.","tokens_in":7733,"feed_emoji":"🧮","tokens_out":8284,"duration_ms":88510,"temperature":0.7,"pith_summary":"This paper demonstrates a machine-checked proof of correctness for a floating-point compiler optimization—replacing a*b+c with a fused multiply-add—at the LLVM intermediate-representation level. The proof shows the transformed (FMA) block is weakly bisimilar to the original (two-instruction) block, with the returned values related by an explicit error bound derived from a standard round-off model. If correct, this opens a path toward producing verified certificates for fast-math optimizations that scientists can rely on, or toward documenting exactly when numerical divergence occurs. The central theorem covers only finite values: NaN, infinities, overflow, and underflow are excluded.","feed_headline":"Formal proof certifies FMA fast-math for finite floating-point inputs","feed_subtitle":"The FMA result is certified to stay within a derived round-off bound of the non-FMA version, for finite values only.","key_machinery":"The carrying mechanism is eutt, the weak bisimulation relation on interaction trees that equates programs up to silent steps, together with the user-supplied refinement relation double_refine. The error bound epsilon_FMA is derived by composing the per-operation round-off errors from the standard delta-epsilon model; double_refine discharges this bound only if the involved values are finite and rounding is to nearest, ties to even. The local environment alignment, local_refine, connects the single write of the FMA block to the two writes of the non-FMA block and then forces strict equality on all untouched variables.","core_discovery":"The central claim is a lemma, fma_optim_correct, which states that for any global memory and local environment, the denotation of the FMA block is weakly bisimilar to the denotation of the non-FMA block. The bisimulation relates the returned states by a refinement relation: global environments are identical, the local environments match after removing the blocks' working registers and pairing the FMA result with the final sum register, and the two returned double values satisfy a predicate that holds only when both are finite and the absolute difference between them is no greater than epsilon_FMA, a bound obtained by propagating the round-off error model across the operations. The proof is c","pith_inferences":["A practical extension would be to make the compiler insert runtime checks for non-finite values; the verified bound then applies on the finite path and the original (unoptimized) computation is used on exceptional inputs, preserving correctness everywhere.","The error-bound derivation could be reused as a certificate for numerical reproducibility: compare two builds and know exactly whether their differences are within the certified FMA bound or caused by other transformations.","One can test the approach on real scientific kernels by extracting the FMA transformation as a compiler pass and checking the emitted proofs; the paper's manual alignment step is the main obstacle and suggests an instrumentation target for LLVM."],"forward_implications":["If this proof style extends to other fast-math rewrites, compilers can emit per-run certificates that a verified checker accepts, yielding end-to-end assurance for floating-point optimizations even with an untrusted compiler.","For the specific pattern a*b+c, scientists using fast-math can now know exactly how much the FMA result may differ from separate multiply-then-add, provided the computation stays finite.","Because the certificate lives at the LLVM IR level, it covers any source language that lowers to this IR, including C, C++, Fortran, and Julia, without redoing the proof per language.","The manually defined alignment between FMA's single write and the non-FMA's two writes outlines what a compiler must emit to scale this approach to larger blocks and eventually whole control-flow graphs."],"fun_headline_variants":["Rocq proof certifies FMA optimization","FMA fast-math proven correct for finite floats","Verifying FMA: weak bisimulation and error bound","Finite float FMA verified with round-off bound","FMA certification: finite floats round-off guarantee"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"The load-bearing premise is that every input and every intermediate arithmetic result is a finite floating-point number (no NaN, infinity, overflow, or underflow) and that the rounding mode is round-to-nearest-ties-to-even; if any value falls outside the finite set, the certified refinement relation stops holding.","fun_headline_variants_meta":{"raw":{"variants":["Rocq proof certifies FMA optimization","FMA fast-math proven correct for finite floats","Verifying FMA: weak bisimulation and error bound","Finite float FMA verified with round-off bound","FMA certification: finite floats round-off guarantee"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001031,"raw_usage":{"total_tokens":4128,"prompt_tokens":642,"completion_tokens":3486,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":386,"completion_tokens_details":{"reasoning_tokens":3411}},"tokens_in":386,"tokens_out":3486,"duration_ms":26308,"temperature":1.0,"reasoning_tokens":3411,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-04T19:48:32.199001+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Enumerate or sample all finite double-precision triples (a,b,c) for which a*b and (a*b)+c are also finite, and verify that |fma(a,b,c) - round(round(a*b)+c)| <= epsilon_FMA under round-to-nearest-ties-to-even rounding; any violating triple would refute the lemma as stated.","supporting_citations":[],"review_version":1}