Overflow in mpz_cmp

[Guillaume Melquiond]

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
mpz_mul2exp, mpz_tdiv_q_2exp

mpn_cmp
mpn_copyi, mpn_copyd
mpn_zero_p, mpn_zero
mpn_add, mpn_add_n, mpn_sub, mpn_sub_n
mpn_mul, mpn_mul_n
mpn_lshift, mpn_rshift
mpn_powm
mpn_get_str, mpn_set_str
mpn_add_1, mpn_sub_1, mpn_mul_1, mpn_addmul_1, mpn_submul_1
mpn_divrem_1, mpn_tdiv_qr
mpn_sqrtrem

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:

https://gitlab.inria.fr/why3/whymp

Best regards,

Guillaume