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