Overflow in mpz_cmp

Marco Bodrato bodrato at mail.dm.unipi.it
Tue Feb 18 12:01:25 UTC 2020

Il 2020-02-18 00:35 Guillaume Melquiond ha scritto:
> Le 17/02/2020 à 22:59, Marco Bodrato a écrit :

>> Did you apply formal verification to other functions? Did they 
>> succeed?

> Here is the list of verified functions:

> mpn_powm

> mpn_sqrtrem

Those are particularly interesting for me!

I recently committed some special flavours of powm: special cases for 
base=2 or when the base is a single limb. It would be really interesting 
to check if they are formally correct.

Moreover year ago, or maybe more, I wrote a possible variation for 
sqrt1. I never moved it to the main repository, because I did not have 
the time to analyse its correctness. Again, an instrument to check, 
would be nice.

> A bit more details can be found there:
> https://gitlab.inria.fr/why3/whymp

I'll look into your work, thanks.



More information about the gmp-devel mailing list