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 _______________________________________________ gmp-devel mailing list gmp-devel@gmplib.org https://gmplib.org/mailman/listinfo/gmp-devel
