Document Open Access Logo

Primitive Floats in Coq

Authors Guillaume Bertholon , Érik Martin-Dorel , Pierre Roux

PDF
Thumbnail PDF

File

LIPIcs.ITP.2019.7.pdf
  • Filesize: 0.6 MB
  • 20 pages

Document Identifiers

Author Details

Guillaume Bertholon
  • École Normale Supérieure, Paris, France
Érik Martin-Dorel
  • Lab. IRIT, University of Toulouse, CNRS, France
Pierre Roux
  • ONERA, Toulouse, France

Acknowledgements

The authors would like to thank Maxime Dénès and Guillaume Melquiond for helpful discussions.

Cite AsGet BibTex

Guillaume Bertholon, Érik Martin-Dorel, and Pierre Roux. Primitive Floats in Coq. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 7:1-7:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.ITP.2019.7

Abstract

Some mathematical proofs involve intensive computations, for instance: the four-color theorem, Hales' theorem on sphere packing (formerly known as the Kepler conjecture) or interval arithmetic. For numerical computations, floating-point arithmetic enjoys widespread usage thanks to its efficiency, despite the introduction of rounding errors. Formal guarantees can be obtained on floating-point algorithms based on the IEEE 754 standard, which precisely specifies floating-point arithmetic and its rounding modes, and a proof assistant such as Coq, that enjoys efficient computation capabilities. Coq offers machine integers, however floating-point arithmetic still needed to be emulated using these integers. A modified version of Coq is presented that enables using the machine floating-point operators. The main obstacles to such an implementation and its soundness are discussed. Benchmarks show potential performance gains of two orders of magnitude.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Mathematics of computing → Numerical analysis
  • General and reference → Performance
Keywords
  • Coq formal proofs
  • floating-point arithmetic
  • reflexive tactics
  • Cholesky decomposition

Metrics

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

Supplementary Materials

References

  1. Michaël Armand, Benjamin Grégoire, Arnaud Spiwack, and Laurent Théry. Extending Coq with Imperative Features and Its Application to SAT Verification. In Matt Kaufmann and Lawrence C. Paulson, editors, Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, volume 6172 of Lecture Notes in Computer Science, pages 83-98. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-14052-5_8.
  2. Henk Barendregt and Herman Geuvers. Proof-Assistants Using Dependent Type Systems. In John Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning (in 2 volumes), pages 1149-1238. Elsevier and MIT Press, 2001. Google Scholar
  3. Mathieu Boespflug, Maxime Dénès, and Benjamin Grégoire. Full Reduction at Full Throttle. In Jean-Pierre Jouannaud and Zhong Shao, editors, Certified Programs and Proofs - First International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings, volume 7086 of Lecture Notes in Computer Science, pages 362-377. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-25379-9_26.
  4. Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, and Guillaume Melquiond. A Formally-Verified C Compiler Supporting Floating-Point Arithmetic. In Alberto Nannarelli, Peter-Michael Seidel, and Ping Tak Peter Tang, editors, 21st IEEE Symposium on Computer Arithmetic, ARITH 2013, Austin, TX, USA, April 7-10, 2013, pages 107-115. IEEE Computer Society, 2013. URL: https://doi.org/10.1109/ARITH.2013.30.
  5. Sylvie Boldo and Guillaume Melquiond. Flocq: A Unified Library for Proving Floating-Point Algorithms in Coq. In Elisardo Antelo, David Hough, and Paolo Ienne, editors, 20th IEEE Symposium on Computer Arithmetic, ARITH 2011, Tübingen, Germany, 25-27 July 2011, pages 243-252. IEEE Computer Society, 2011. URL: https://doi.org/10.1109/ARITH.2011.40.
  6. Sylvie Boldo and Guillaume Melquiond. Computer Arithmetic and Formal Proofs: Verifying Floating-point Algorithms with the Coq System. Elsevier, 2017. Google Scholar
  7. Samuel Boutin. Using Reflection to Build Efficient and Certified Decision Procedures. In Martín Abadi and Takayasu Ito, editors, Theoretical Aspects of Computer Software, Third International Symposium, TACS '97, Sendai, Japan, September 23-26, 1997, Proceedings, volume 1281 of Lecture Notes in Computer Science, pages 515-529. Springer, 1997. URL: https://doi.org/10.1007/BFb0014565.
  8. Cyril Cohen, Maxime Dénès, and Anders Mörtberg. Refinements for free! In Georges Gonthier and Michael Norrish, editors, Certified Programs and Proofs, volume 8307 of Lecture Notes in Computer Science, pages 147-162. Springer, 2013. URL: http://dx.doi.org/10.1007/978-3-319-03545-1_10.
  9. Simon Colin, Rodolphe Lepigre, and Gabriel Scherer. Unboxing Mutually Recursive Type Definitions in OCaml. In Proceedings of JFLA, Les Rousses, France, 30th January to 2nd February 2019., 2019. Google Scholar
  10. Catherine Daramy-Loirat, David Defour, Florent De Dinechin, Matthieu Gallet, Nicolas Gast, Christoph Lauter, and Jean-Michel Muller. CR-libm. A library of correctly rounded elementary functions in double-precision. Technical report, LIP, ENS Lyon, 2006. URL: https://hal-ens-lyon.archives-ouvertes.fr/ensl-01529804/.
  11. T. J. Dekker. A floating-point technique for extending the available precision. Numerische Mathematik, 18(3):224-242, 1971. Google Scholar
  12. Maxime Dénès. Towards primitive data types for COQ 63-bits integers and persistent arrays. In Coq-5, the Coq Workshop 2013, Rennes, France, July 2013. Extended abstract. URL: https://coq.inria.fr/files/coq5_submission_2.pdf.
  13. Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds, and Clark W. Barrett. SMTCoq: A Plug-In for Integrating SMT Solvers into Coq. In Rupak Majumdar and Viktor Kuncak, editors, Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II, volume 10427 of Lecture Notes in Computer Science, pages 126-133. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-63390-9_7.
  14. Georges Gonthier. Formal Proof - The Four-Color Theorem. Notices of the American Mathematical Society, 55(11):1382-1393, 2008. URL: http://www.ams.org/notices/200811/tx081101382p.pdf.
  15. Benjamin Grégoire and Xavier Leroy. A compiled implementation of strong reduction. In Mitchell Wand and Simon L. Peyton Jones, editors, Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming (ICFP '02), Pittsburgh, Pennsylvania, USA, October 4-6, 2002., pages 235-246. ACM, 2002. URL: https://doi.org/10.1145/581478.581501.
  16. Benjamin Grégoire and Laurent Théry. A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers. In Ulrich Furbach and Natarajan Shankar, editors, IJCAR, volume 4130 of Lecture Notes in Computer Science, pages 423-437. Springer, 2006. URL: https://doi.org/10.1007/11814771_36.
  17. Thomas Hales, Mark Adams, Gertrud Bauer, Tat Dat Dang, John Harrison, Le Truong Hoang, Cezary Kaliszyk, Victor Magron, Sean Mclaughlin, Tat Thang Nguyen, and et al. a formal proof of the Kepler conjecture. Forum of Mathematics, Pi, 5:e2, 2017. 29 pages. URL: https://doi.org/10.1017/fmp.2017.1.
  18. Nicholas Higham. Accuracy and Stability of Numerical Algorithms. Society for Industrial and Applied Mathematics, Philadelphia, PA, USA, 1996. Google Scholar
  19. IEEE Computer Society. IEEE Standard for Floating-Point Arithmetic. IEEE Standard 754-2008, 2008. Google Scholar
  20. Claude-Pierre Jeannerod and Siegfried M. Rump. On relative errors of floating-point operations: Optimal bounds and applications. Math. Comput., 87(310):803-819, 2018. URL: https://doi.org/10.1090/mcom/3234.
  21. D. Knuth. The Art of Computer Programming, volume 2. Addison Wesley, Reading, MA, 1973. Google Scholar
  22. Peter Kornerup, Vincent Lefèvre, Nicolas Louvet, and Jean-Michel Muller. On the Computation of Correctly Rounded Sums. IEEE Trans. Computers, 61(3):289-298, 2012. URL: https://doi.org/10.1109/TC.2011.27.
  23. Andreas Lochbihler. Fast Machine Words in Isabelle/HOL. In Jeremy Avigad and Assia Mahboubi, editors, Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings, volume 10895 of Lecture Notes in Computer Science, pages 388-410. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-94821-8_23.
  24. Victor Magron, Xavier Allamigeon, Stéphane Gaubert, and Benjamin Werner. Formal Proofs for Nonlinear Optimization. Journal of Formalized Reasoning, 8(1):1-24, 2015. URL: http://jfr.unibo.it/article/view/4319.
  25. É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, October 2016. URL: https://doi.org/10.1007/s10817-015-9350-4.
  26. Érik Martin-Dorel and Pierre Roux. A reflexive tactic for polynomial positivity using numerical solvers and floating-point computations. In Yves Bertot and Viktor Vafeiadis, editors, Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017, pages 90-99. ACM, 2017. URL: https://doi.org/10.1145/3018610.3018622.
  27. Micaela Mayero. Formalisation et automatisation de preuves en analyses réelle et numérique. PhD thesis, Université Paris VI, December 2001. Google Scholar
  28. O. Møller. Quasi Double-Precision in Floating-Point Addition. BIT, 5:37-50, 1965. Google Scholar
  29. David Monniaux. The pitfalls of verifying floating-point computations. ACM Trans. Program. Lang. Syst., 30(3):12:1-12:41, 2008. URL: https://doi.org/10.1145/1353445.1353446.
  30. Jean-Michel Muller, Nicolas Brisebarre, Florent de Dinechin, Claude-Pierre Jeannerod, Vincent Lefèvre, Guillaume Melquiond, Nathalie Revol, Damien Stehlé, and Serge Torres. Handbook of Floating-Point Arithmetic. Birkhäuser, 2010. URL: https://doi.org/10.1007/978-0-8176-4705-6.
  31. César Muñoz. Rapid prototyping in PVS. Technical Report CR-2003-212418, NASA, 2003. Google Scholar
  32. Henri Poincaré. La science et l'hypothèse. Flammarion, Paris, 1902. Google Scholar
  33. Pierre Roux. Formal Proofs of Rounding Error Bounds - With Application to an Automatic Positive Definiteness Check. J. Autom. Reasoning, 57(2):135-156, 2016. URL: https://doi.org/10.1007/s10817-015-9339-z.
  34. Siegfried M. Rump. Verification of positive definiteness. BIT Numerical Mathematics, 46:433-452, 2006. Google Scholar
  35. Siegfried M. Rump. Verification methods: Rigorous results using floating-point arithmetic. Acta Numerica, 19:287-449, 2010. Google Scholar
  36. Siegfried M Rump, Takeshi Ogita, Yusuke Morikura, and Shin'ichi Oishi. Interval arithmetic with fixed rounding mode. Nonlinear Theory and Its Applications, IEICE, 7(3):362-373, 2016. Google Scholar
  37. Siegfried M. Rump, Takeshi Ogita, and Shin'ichi Oishi. Accurate Floating-Point Summation Part I: Faithful Rounding. SIAM J. Scientific Computing, 31(1):189-224, 2008. URL: https://doi.org/10.1137/050645671.
  38. Siegfried M. Rump, Paul Zimmermann, Sylvie Boldo, and Guillaume Melquiond. Computing predecessor and successor in rounding to nearest. BIT Numerical Mathematics, 49(2):419-431, June 2009. URL: https://doi.org/10.1007/s10543-009-0218-z.
  39. Arnaud Spiwack. Verified Computing in Homological Algebra. (Calculs vérifiés en algèbre homologique). PhD thesis, École Polytechnique, Palaiseau, France, 2011. URL: https://tel.archives-ouvertes.fr/pastel-00605836.
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
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact