An Efficient Arbitrary-Precision Integer Library
An arbitrary-precision integer library in the style of GMP, designed to be both efficient and formally proved correct.
Authors: Raphaël Rieu-Helft
Topics: Arithmetic / Pointer Programs / Proofs by reflection / Non-linear Arithmetic
Tools: Why3
see also the index (by topic, by tool, by reference, by year)
download ZIP archive
This library implements arbitrary-precision integers in the style of GMP. Supported operations are addition, multiplication, division, comparisons, shifts square root and modular exponentiation on non-negative integers, as well as some basic operations on relative integers.
More detailed information on the C library is available in the WhyMP repository, as well as in the papers:
- "How to Get an Efficient yet Verified Arbitrary-Precision Integer Library" by Raphaël Rieu-Helft, Claude Marché and Guillaume Melquiond, published in VSTTE'2017 proceedings, Springer LNCS.
- "A Why3 framework for reflection proofs and its application to GMP's algorithms" by Guillaume Melquiond and Raphaël Rieu-Helft, published in IJCAR'2018 proceedings, Springer LNAI.
- "Formal Verification of a State-of-the-Art Integer Square Root" by Guillaume Melquiond and Raphaël Rieu-Helft, published in ARITH'2019 proceedings.
- "A Why3 proof of GMP algorithms" by Raphaël Rieu-Helft, published in Journal of Formalized Reasoning, ASDD-AlmaDL, 2019.