Towards Verified Compilation of Floating-point Optimization in Scientific Computing Programs

John Sarracino; Mohit Tekriwal

REVIEW 4 major objections 4 minor 9 references

Towards Verified Compilation of Floating-point Optimization in Scientific Computing Programs

T0 review · 4 major / 4 minor · reviewed 2026-08-04 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read 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.

desk verdict 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. read the letter →

arxiv 2509.09019 v1 pith:E5KWTETO submitted 2025-09-10 cs.PL

Mohit Tekriwal , John Sarracino This is my paper · ORCID

classification cs.PL

keywords floating-pointcorrectnessfusedmultiply-addcompileroptimizationverificationinteractiontreesrefinementrelationstranslationvalidationfast-mathoptimizationsround-offerrorbounds

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

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.

What carries the argument

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.

What would settle it

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.

Watch

Extended reading notes

Core claim

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

Load-bearing premise

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.

Editorial extensions

If this is right

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.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

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.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the 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.

The 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.

The 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.

That 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.

The 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.

For 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.

Recommendation: 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.

Referee Report

4 major / 4 minor

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.

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 (4)

[§3.4, Fig. 4; §3.6, Fig. 5] 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.
[§3.6, Fig. 5] 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.
[§3.4] 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.
[§3.5, Fig. 4] 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.

minor comments (4)

[Throughout] 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.
[§3.4] 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.
[§3.2 / Fig. 3] 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.
[Fig. 2] 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.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the correctness criterion is independently grounded in Flocq's standard error model, and the main equivalence does not reduce to its inputs by construction.

full rationale

The paper's central claim — that the FMA block refines the non-FMA block for `a*b+c` — is not circular. The correctness predicate `double_refine` is defined using an explicit epsilon bound `epsilon_FMA` that is derived from the standard delta-epsilon floating-point error model in Flocq, not fitted to the program outputs or to the target theorem. The theorem `fma_optim_correct` is a genuine formal statement about the relationship between two independent Vellvm ITree denotations, and the proof relies on Flocq's semantics for `Bfma`, `Bmult`, and `Bplus`, which are external, machine-checked libraries. No load-bearing self-citation appears: the cited prior work (Vellvm, ITrees, Flocq, Crellvm) provides infrastructure, not the optimization correctness itself. The only notable caveat is that `double_refine` is an implication whose antecedent requires finiteness of the compared values and their difference; for NaN or Inf inputs the antecedent is false, so the relation holds vacuously. This means the lemma as stated does not give a meaningful guarantee for non-finite cases, and in that sense it is weaker than one might expect from the informal motivation. However, this is a soundness/strength limitation, not a circular derivation: the paper explicitly states the finiteness assumption in Section 3.4 and Section 3.6, and the finite case — the actual focus — is a substantive mathematical claim, not a renaming or a presupposition of the conclusion. The manual alignment predicate is a design choice, not a circular step. Overall, the derivation chain is self-contained against external formal libraries, and there is no reduction of a prediction to a fitted parameter or to a self-citation chain.

Assumptions & free parameters 1 free parameters · 5 assumptions · 0 invented entities

No new physical or semantic entities are postulated. The fmuladd intrinsic is an existing LLVM construct, and the refinement relations are proof artifacts rather than invented entities. The main free input is the chosen error bound epsilon_FMA, which the paper derives informally from Flocq's model rather than from a fixed external specification.

free parameters (1)

epsilon_FMA = symbolic expression in the delta-epsilon error model
Introduced by hand to define the refinement relation in Section 3.4; the proof is meant to show the two computations are within this bound.

assumptions (5)

domain assumption Input values and intermediate operations are finite
double_refine requires is_finite p1 and p2; Sections 3.4 and 3.6. Excludes NaN/Inf cases where fast-math optimization is contentious.
domain assumption Rounding mode is RNE (round-to-nearest, ties to even)
The error bound is derived with rounding mode fixed to RNE, the default LLVM mode.
domain assumption Flocq delta-epsilon error model for floating-point operations
The epsilon_FMA bound is derived using the standard error model from Flocq (Section 3.4).
domain assumption Vellvm's ITree semantics and eutt relation faithfully model LLVM program behavior
The equivalence proof relies on Vellvm's denote_block and eutt, which are trusted foundations.
ad hoc to paper The manually defined alignment predicate correctly relates one FMA write to two non-FMA writes
Section 3.5 defines local_refine by hand; if the alignment is wrong, the equivalence statement is mis-specified.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Towards Verified Compilation of Floating-point Optimization in Scientific Computing Programs." pith.science (2026). https://pith.science/paper/E5KWTETO

@misc{pith2026250909019,
  author       = {Pith},
  title        = {Pith review of: Towards Verified Compilation of Floating-point Optimization in Scientific Computing Programs},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/E5KWTETO}},
  note         = {Machine review of arXiv:2509.09019}
}

abstract

Scientific computing programs often undergo aggressive compiler optimization to achieve high performance and efficient resource utilization. While performance is critical, we also need to ensure that these optimizations are correct. In this paper, we focus on a specific class of optimizations, floating-point optimizations, notably due to fast math, at the LLVM IR level. We present a preliminary work, which leverages the Verified LLVM framework in the Rocq theorem prover, to prove the correctness of Fused-Multiply-Add (FMA) optimization for a basic block implementing the arithmetic expression $a * b + c$ . We then propose ways to extend this preliminary results by adding more program features and fast math floating-point optimizations.

Figures

Figures reproduced from arXiv: 2509.09019 by the authors.

**Figure 1.** FMA v/s non-FMA code for the arithmetic expression 𝑎 ∗ 𝑏 + 𝑐 in LLVM. This are the inputs to the Vellvm framework. Definition fma_blk := {| blk_id := (Anon (3)%Z); blk_phis := []; blk_code := [((IId (Anon (4)%Z)), (INSTR_Call (DTYPE_Double, (EXP_Ident (ID_Global (Name "llvm.fmuladd.f64")))) [((DTYPE_Double, EXP_Double a), []); ((DTYPE_Double, EXP_Double b), []); ((DTYPE_Double, EXP_Double c), []) ] [ANN_tail Tail] )… view at source ↗

**Figure 2.** Vellvm definition for FMA and non-FMA blocks 3.2 Extending intrinsics in Vellvm with fmuladd We add an intrinsic definition for FMA to Vellvm, depicted in Figure 3. This definition consists of two parts: a declaration consisting of the intrinsic’s LLVM function prototype (argument types, return type, etc), fmul_add_64; and a semantic definition of the function’s behavior in Rocq, llvm_fmuladd_f64. Our semantic defi… view at source ↗

**Figure 3.** Vellvm definition for FMA intrinsic. are finite, where we fix the rounding mode to RNE (rounding to nearest with ties to even), which is the default rounding mode. Here, 𝜖𝐹𝑀𝐴 = (| (𝑎∗𝑏 ∗𝑐)|𝛿 +𝜖+ |𝑎∗𝑏| ∗ (2𝛿 +𝛿 2 ) +𝜖 ∗ (1+𝛿) + |𝑐| ∗ 𝛿 +𝜖) (1+𝛿) +𝜖, is a tight error bound for FMA operation. We derive this bound by collecting an upper bound on the absolute round off error associated with each operation, using the stan… view at source ↗

Figures from the paper (2 more)

**Figure 4.** Figure 4: Refinement relations for Vellvm doubles and local environments. Lemma fma_optim_correct: forall g l, eutt (fun '(l1, (g1, u1)) '(l2, (g2, u2)) ⇒ // Neither block changes globals g1 = g2 ∧ local_refine l1 l2 ∧ // refinement relation for floats match u1, u2 with | inr u1…

**Figure 5.** Figure 5: Equivalence between FMA and non-FMA blocks. computations increase, manually defining such alignment predicates becomes challenging. Therefore, our immediate future work will be to instrument the compiler to compute these alignment predicates, which can then be used to…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

9 extracted references

[1]

Dong H Ahn, Allison H Baker, Michael Bentley, Ian Briggs, Ganesh Gopalakr- ishnan, Dorit M Hammerling, Ignacio Laguna, Gregory L Lee, Daniel J Milroy, and Mariana Vertenstein. 2021. Keeping science on keel when software moves. Commun. ACM64, 2 (2021), 66–74

2021
[2]

Andrew W Appel. 2011. Verified Software Toolchain: (Invited Talk). InEuropean Symposium on Programming. Springer, 1–17

2011
[3]

Bruno Barras, Samuel Boutin, Cristina Cornes, Judicaël Courant, Yann Coscoy, David Delahaye, Daniel de Rauglaudre, Jean-Christophe Filliâtre, Eduardo Giménez, Hugo Herbelin, et al. 1999. The Coq proof assistant reference manual. INRIA, version6, 11 (1999), 17–21

1999
[4]

Michael Bentley, Ian Briggs, Ganesh Gopalakrishnan, Dong H Ahn, Ignacio La- guna, Gregory L Lee, and Holger E Jones. 2019. Multi-level analysis of compiler- induced variability and performance tradeoffs. InProceedings of the 28th Inter- national Symposium on High-Performance Parallel and Distributed Computing. 61–72

2019
[5]

Sylvie Boldo and Guillaume Melquiond. 2011. Flocq: A unified library for proving floating-point algorithms in Coq. In2011 IEEE 20th Symposium on Computer Arithmetic. IEEE, 243–252

2011
[6]

Hui Guo, Ignacio Laguna, and Cindy Rubio-González. 2020. pLiner: isolating lines of floating-point code for compiler-induced variability. InSC20: International Conference for High Performance Computing, Networking, Storage and Analysis. IEEE, 1–14

2020
[7]

Jeehoon Kang, Yoonseung Kim, Youngju Song, Juneyoung Lee, Sanghoon Park, Mark Dongyeon Shin, Yonghyun Kim, Sungkeun Cho, Joonwon Choi, Chung-Kil Hur, et al. 2018. Crellvm: verified credible compilation for LLVM. InProceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation. 631–645

2018
[8]

Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Ben- jamin C Pierce, and Steve Zdancewic. 2019. Interaction trees: representing re- cursive and impure programs in Coq.Proceedings of the ACM on Programming Languages4, POPL (2019), 1–32

2019

Show all 9 references

[9]

Jianzhou Zhao, Santosh Nagarakatte, Milo MK Martin, and Steve Zdancewic. 2012. Formalizing the LLVM intermediate representation for verified program transfor- mations. InProceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. 427–440

2012

Pith tools

Reviewed August 4, 2026 · model on record in the stance chip above.

[1] [1]

Dong H Ahn, Allison H Baker, Michael Bentley, Ian Briggs, Ganesh Gopalakr- ishnan, Dorit M Hammerling, Ignacio Laguna, Gregory L Lee, Daniel J Milroy, and Mariana Vertenstein. 2021. Keeping science on keel when software moves. Commun. ACM64, 2 (2021), 66–74

2021

[2] [2]

Andrew W Appel. 2011. Verified Software Toolchain: (Invited Talk). InEuropean Symposium on Programming. Springer, 1–17

2011

[3] [3]

Bruno Barras, Samuel Boutin, Cristina Cornes, Judicaël Courant, Yann Coscoy, David Delahaye, Daniel de Rauglaudre, Jean-Christophe Filliâtre, Eduardo Giménez, Hugo Herbelin, et al. 1999. The Coq proof assistant reference manual. INRIA, version6, 11 (1999), 17–21

1999

[4] [4]

Michael Bentley, Ian Briggs, Ganesh Gopalakrishnan, Dong H Ahn, Ignacio La- guna, Gregory L Lee, and Holger E Jones. 2019. Multi-level analysis of compiler- induced variability and performance tradeoffs. InProceedings of the 28th Inter- national Symposium on High-Performance Parallel and Distributed Computing. 61–72

2019

[5] [5]

Sylvie Boldo and Guillaume Melquiond. 2011. Flocq: A unified library for proving floating-point algorithms in Coq. In2011 IEEE 20th Symposium on Computer Arithmetic. IEEE, 243–252

2011

[6] [6]

Hui Guo, Ignacio Laguna, and Cindy Rubio-González. 2020. pLiner: isolating lines of floating-point code for compiler-induced variability. InSC20: International Conference for High Performance Computing, Networking, Storage and Analysis. IEEE, 1–14

2020

[7] [7]

Jeehoon Kang, Yoonseung Kim, Youngju Song, Juneyoung Lee, Sanghoon Park, Mark Dongyeon Shin, Yonghyun Kim, Sungkeun Cho, Joonwon Choi, Chung-Kil Hur, et al. 2018. Crellvm: verified credible compilation for LLVM. InProceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation. 631–645

2018

[8] [8]

Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Ben- jamin C Pierce, and Steve Zdancewic. 2019. Interaction trees: representing re- cursive and impure programs in Coq.Proceedings of the ACM on Programming Languages4, POPL (2019), 1–32

2019