Overflow in mpz_cmp

[Marco Bodrato]

Ciao,
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.

Ĝis,
m

-- 
http://bodrato.it/papers/