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.