Overflow in mpz_cmp
guillaume.melquiond at inria.fr
Mon Feb 17 23:35:15 UTC 2020
Le 17/02/2020 à 22:59, Marco Bodrato a écrit :
>> The bug was noticed when formally verifying this function.
> Did you apply formal verification to other functions? Did they succeed?
Just so that there is no misunderstanding, we did not formally verify
GMP's C/ASM functions directly, but our understanding of them. More
concretely, we first translated them into a more palatable programming
language, and then we formally verified them.
Here is the list of verified functions:
mpz_set_ui, mpz_set_si, mpz_get_ui
mpz_cmp, mpz_cmp_ui, mpz_cmpabs, mpz_cmpabs_ui
mpz_add, mpz_add_ui, mpz_sub, mpz_sub_ui, mpz_ui_sub
mpz_mul, mpz_mul_si, mpz_mul_ui
mpn_add, mpn_add_n, mpn_sub, mpn_sub_n
mpn_add_1, mpn_sub_1, mpn_mul_1, mpn_addmul_1, mpn_submul_1
Note that multiplication is only verified up to Toom-3x2, and only the
schoolbook version of division is verified. Also, in presence of
conditional compilation, we only verified one possible version of the
code (e.g., we assume that HAVE_NATIVE_mpn_redc_2 is not defined). So,
what we have verified is kind of an intermediate code: more intricate
than Mini-GMP, but not as intricate as GMP.
A bit more details can be found there:
More information about the gmp-devel