coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Computations with big numbers: Square-and-Multiply (with mod reduce)

From: Benoît Viguier <beviguier AT gmail.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Computations with big numbers: Square-and-Multiply (with mod reduce)
Date: Wed, 27 Feb 2019 17:59:36 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=beviguier AT gmail.com; spf=Pass smtp.mailfrom=beviguier AT gmail.com; spf=None smtp.helo=postmaster AT mail-ed1-f46.google.com
Ironport-phdr: 9a23:/fk+XxFSaOBdB38OBsFc0J1GYnF86YWxBRYc798ds5kLTJ78o8SwAkXT6L1XgUPTWs2DsrQY07qQ6/iocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmDmwbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5KlpVRDokj8KOSA5/m/KicJ+gqxUrx29qBJw2IPUfIOYOeBicq/Bc94XR2xMVdtRWSxbBYO8apMCAvcfMuZeqInlqUcOogOxCgmtC+Pv1z5IiWHs3aYn1OkuCh/J3BIhH9IBrXTUrcv6NL0JXOC6yanH1zTDb/dM1Tjh74jIdwksrPeRVrxzacrc0VcjGx/Bg1mKqoHoPymZ2voRv2WY9eZtWuOih3Y6pwx+ojWj3NoghpTIi44P11zJ+zt1zJwrKdC3SkN2Z8OvHoFKuCGALYR2R9svQ2F2tyY+zb0LoZu7czILyJQj3hLQdeGIf5WR7hLtW+ucIC10hH1ieLK4iBay9VavxvfgWcmz1VZGtitFkt/SuXARzxHf9NSLR/9n8kqi2TuDzR7f5v1HLEwumqfWKoYtwrsqmZoStUTDEDX2mELzjKKObUor5Pao6+XoYrX7p5+TKZV0hxrxMqQrgMO/AOA4PhISUGic/OSwzKfj8lHhQLVWkv02lbHUv4zdJcQCv6K2HwtV0ps45BukFDen0NEYnWEdI15feRKHiZLpO1DUL/ziA/e/mQfkrDA+jfvBJ/jqBojHBnnFirboO7hnoQYIww0qiNtb+ph8C7cbIfu1VFWn5/LCCRpsGQGyxGD7P+t82Z4fVHjHVqWULqLdrF6F/MogJuCNYMkevzOreKtt3OLnkXJswQxVRqKux5ZCMCnpTMQjGF2QZD/XuvlEFG4LugQkS+mz0Q+NVDdSYzC5WKduv2hnWrLjNp/KQ8WWuJLExD2yR8QEaWVPC1TKGnDtJd3dBqU8LRmKK8okqQQqELisT4h7iEOrvQ7+jrdrd6/apnNeupXk29x4oebUkENq+A==

Dear Coq-club.

I need to prove the following equality in Coq:

-1 mod (2 ^ 255 - 19) = 236839902240 ^ ((2 ^ 255 - 19) - 1) / 2) mod (2
^ 255 - 19).

While usually a simple `compute;reflexivity` would do the trick. Here
the computation of the power may take a bit too long...

Has someone implemented a square-and-multiply somewhere (or do I need to
reprove it) ?

Best Regards.

Benoit Viguier.

[Coq-Club] Computations with big numbers: Square-and-Multiply (with mod reduce), Benoît Viguier, 02/27/2019
- Re: [Coq-Club] Computations with big numbers: Square-and-Multiply (with mod reduce), Jean-Marie Madiot, 02/27/2019