coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Jean-Marie Madiot <madiot AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Computations with big numbers: Square-and-Multiply (with mod reduce)
Date: Wed, 27 Feb 2019 18:16:53 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=madiot AT gmail.com; spf=Pass smtp.mailfrom=madiot AT gmail.com; spf=None smtp.helo=postmaster AT mail-io1-f49.google.com
Ironport-phdr: 9a23:dRh4VhGfUpQcKVFn6UEolp1GYnF86YWxBRYc798ds5kLTJ78o8ywAkXT6L1XgUPTWs2DsrQY07qQ6/iocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmDmwbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VC+85Kl3VhDnlCYHNyY48G7JjMxwkLlbqw+lqxBm3oLYfJ2ZOP94c6jAf90VWHBBU95eWCxPAIyyb4UBAekcM+hGs4bwvEEBoQekCAS2GO/j1j1Fi3nr1qM6yeQhFgTG0RQkEd0QqnvUqsz5OqAIXuCvzanH0yjIYfRM1jjg6YjIdQwhquyLULJ1a8Xe1EgvFwTZjliLpozlOima1uUJs2SB8+VgUuevhnchpgpsoTav3t8hhpfVio8R0FzJ9iV0zJwoKdC5SUN3e9GpHZ9WuiqHLYV5WNkiTHttuCsiyr0Jp5q7fC8SxZQi3RHfaviHf5GJ4hLkSeqdODl4iX1hdb6liBay9k+gyuL4VsaqylpFsi1FktzUunAM0Rzc9NSHR+Nj8ku93TuDzQPe5+FeLUwplKfWKoQtz7E0m5YLtETMBC72mEH4jK+McUUk//Cl6+H9bbr7p5+cMJN0hxrxMqQrgMO/AOA4PhISUGic/OSwzKfj8lHhQLVWkv02lbHUv4zdJcQCv6K2HwtV0ps45BukFDen0NEYnWEdI15feRKHiZLpO1DUL/ziA/e/mQfkrDA+7PffdpblH5+FenPEifLqeat3w09a0gs6i95FscF6ELYEddD+U0m0kdXCDxJxFgW4wuH7QIF4348fXn6nDaqQMaeUuliNsLF8a9KQbZMY7W6uY8Mu4OTj2DpgwQdELPuZmKAPYXX9JcxIZkCQYH7imNAESD5YsQ83Teisg1qHA2cKOySCGpkk7zR+M7qISJ/ZT9n00rOE1Sa/WJZRYzIeUw3eITLTb4yBHsw0RmeSL8tmyGFWULGgT8og0kjrulOrjbVgKeXQ92sTspexjNU=

Dear Benoît,

isn't modular exponentiation fast enough? On my computer, it takes 2 seconds with vm_compute (and 34 seconds with compute):

Require Import ZArith.

Require Import ZArith.Zpow_facts.

Open Scope Z_scope.

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

Proof.

rewrite <-Zpow_mod_correct. 2: vm_compute; congruence.

vm_compute.

reflexivity.

Qed.

Best,

Jean-Marie

On Wed, Feb 27, 2019 at 6:00 PM Benoît Viguier <beviguier AT gmail.com> wrote:

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