End-To-End Formal Verification of a Fast and Accurate Floating-Point Approximation

Authors Florian Faissole , Paul Geneau de Lamarlière , Guillaume Melquiond



PDF
Thumbnail PDF

File

LIPIcs.ITP.2024.14.pdf
  • Filesize: 0.74 MB
  • 18 pages

Document Identifiers

Author Details

Florian Faissole
  • Mitsubishi Electric R&D Centre Europe, 35700 Rennes, France
Paul Geneau de Lamarlière
  • Mitsubishi Electric R&D Centre Europe, 35700 Rennes, France
  • Université Paris-Saclay, CNRS, ENS Paris-Saclay, Inria, LMF, 91190 Gif-sur-Yvette, France
Guillaume Melquiond
  • Université Paris-Saclay, CNRS, ENS Paris-Saclay, Inria, LMF, 91190 Gif-sur-Yvette, France

Cite As Get BibTex

Florian Faissole, Paul Geneau de Lamarlière, and Guillaume Melquiond. End-To-End Formal Verification of a Fast and Accurate Floating-Point Approximation. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 14:1-14:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.ITP.2024.14

Abstract

Designing an efficient yet accurate floating-point approximation of a mathematical function is an intricate and error-prone process. This warrants the use of formal methods, especially formal proof, to achieve some degree of confidence in the implementation. Unfortunately, the lack of automation or its poor interplay with the more manual parts of the proof makes it way too costly in practice. This article revisits the issue by proposing a methodology and some dedicated automation, and applies them to the use case of a faithful binary64 approximation of exponential. The peculiarity of this use case is that the target of the formal verification is not a simple modeling of an external code; it is an actual floating-point function defined in the logic of the Coq proof assistant, which is thus usable inside proofs once its correctness has been fully verified. This function presents all the attributes of a state-of-the-art implementation: bit-level manipulations, large tables of constants, obscure floating-point transformations, exceptional values, etc. This function has been integrated into the proof strategies of the CoqInterval library, bringing a 20× speedup with respect to the previous implementation.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Formal software verification
  • Theory of computation → Interactive proof systems
  • Theory of computation → Automated reasoning
  • Mathematics of computing → Mathematical software performance
  • Mathematics of computing → Interval arithmetic
Keywords
  • Program verification
  • floating-point arithmetic
  • formal proof
  • automated reasoning
  • mathematical library

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. Andrew Appel and Ariel Kellison. VCFloat2: Floating-point error analysis in Coq. In 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 14-29, London, United Kigdom, 2024. URL: https://doi.org/10.1145/3636501.3636953.
  2. Mathieu Boespflug, Maxime Dénès, and Benjamin Grégoire. Full reduction at full throttle. In 1st International Conference on Certified Programs and Proofs, pages 362-377, Kenting, Taiwan, December 2011. URL: https://doi.org/10.1007/978-3-642-25379-9_26.
  3. Sylvie Boldo and Guillaume Melquiond. Computer Arithmetic and Formal Proofs. ISTE Press - Elsevier, 2017. Google Scholar
  4. William J. Cody, Jr. and William Waite. Software Manual for the Elementary Functions. Prentice-Hall, Englewood Cliffs, NJ, 1980. Google Scholar
  5. Maxime Dénès. Towards primitive data types for Coq 63-bits integers and persistent arrays. In 5th Coq Workshop, Rennes, France, July 2013. URL: https://coq.inria.fr/files/coq5_submission_2.pdf.
  6. Paul Geneau de Lamarlière and Guillaume Melquiond. CoqInterval. Software, version 4.10.0., (visited on 2024-08-22). URL: https://gitlab.inria.fr/coqinterval/interval.git
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.22454
  7. Paul Geneau de Lamarlière, Guillaume Melquiond, and Florian Faissole. Slimmer formal proofs for mathematical libraries. In Theo Drane and Anastasia Volkova, editors, 30th IEEE International Symposium on Computer Arithmetic, Portland, OR, USA, September 2023. URL: https://doi.org/10.1109/ARITH58626.2023.00026.
  8. John Harrison. Floating-point verification in HOL Light: The exponential function. Technical Report 428, University of Cambridge Computer Laboratory, 1997. Google Scholar
  9. John Harrison. Formal verification of floating point trigonometric functions. In Warren A. Hunt and Steven D. Johnson, editors, 3rd International Conference on Formal Methods in Computer-Aided Design, volume 1954 of Lecture Notes in Computer Science, pages 217-233, 2000. Google Scholar
  10. Tom Hubrecht, Claude-Pierre Jeannerod, Paul Zimmermann, Laurence Rideau, and Laurent Théry. Towards a correctly-rounded and fast power function in binary64 arithmetic, 2024. URL: https://inria.hal.science/hal-04159652.
  11. Érik Martin-Dorel and Guillaume Melquiond. Proving tight bounds on univariate expressions with elementary functions in Coq. Journal of Automated Reasoning, 57(3):187-217, 2016. URL: https://doi.org/10.1007/s10817-015-9350-4.
  12. Érik Martin-Dorel, Guillaume Melquiond, and Pierre Roux. Enabling floating-point arithmetic in the Coq proof assistant. Journal of Automated Reasoning, 67, 2023. URL: https://doi.org/10.1007/s10817-023-09679-x.
  13. Mariano Moscato, Laura Titolo, Aaron Dutle, and César A. Muñoz. Automatic estimation of verified floating-point round-off errors via static analysis. In Stefano Tonetta, Erwin Schoitsch, and Friedemann Bitsch, editors, 36th International Conference on Computer Safety, Reliability, and Security, volume 10488 of Lecture Notes in Computer Science, pages 213-229, Trento, Italy, 2017. URL: https://doi.org/10.1007/978-3-319-66266-4_14.
  14. Jean-Michel Muller. Elementary Functions, Algorithms and Implementation. Birkhäuser, Boston, MA, 3rd edition, 2016. URL: https://doi.org/10.1007/978-1-4899-7983-4.
  15. Jean-Michel Muller, Nicolas Brunie, Florent de Dinechin, Claude-Pierre Jeannerod, Mioara Joldes, Vincent Lefèvre, Guillaume Melquiond, Nathalie Revol, and Serge Torres. Handbook of Floating-Point Arithmetic. Birkhäuser Basel, 2nd edition, 2018. URL: https://doi.org/10.1007/978-3-319-76526-6.
  16. Pierre Roux. Formal proofs of rounding error bounds - with application to an automatic positive definiteness check. Journal of Automated Reasoning, 57(2):135-156, 2016. URL: https://doi.org/10.1007/s10817-015-9339-z.
  17. Siegfried M. Rump. Verification methods: Rigorous results using floating-point arithmetic. Acta Numerica, 19:287-449, May 2010. URL: https://doi.org/10.1017/S096249291000005X.
  18. David M. Russinoff. Formal Verification of Floating-Point Hardware Design. Springer Cham, 2nd edition, 2022. URL: https://doi.org/10.1007/978-3-030-87181-9.
  19. Alexey Solovyev, Marek S. Baranowski, Ian Briggs, Charles Jacobsen, Zvonimir Rakamarić, and Ganesh Gopalakrishnan. Rigorous estimation of floating-point round-off errors with symbolic Taylor expansions. ACM Transactions on Programming Languages and Systems, 41(1), December 2018. URL: https://doi.org/10.1145/3230733.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail