coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Proving p: Z is prime for large p

From: Benoît Viguier <beviguier AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Proving p: Z is prime for large p
Date: Tue, 5 Apr 2022 12:39:20 +0200
Authentication-results: mail3-smtp-sop.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-f53.google.com
Ironport-data: A9a23:M0+N6K/8g5EekjVR5b5tDrUDvXiTJUtcMsCJ2f8bNWPcYEJGY0x3y WUbCGzQOvbfZjHzct53YYzl8UICu5LRzNc3GVFp/CtEQiMRo6IpJ/zJdxaqZ3v6wu7rFR88s Z1GMrEsCOhuExcwcz/0auCJQUFUjP3OHvylYAL9EngZqTVMEU/Nsjo+3b9h6mJUqYLhWVnV5 Yuv+5S31GKNglaYDEpEs8pvlzs05JweiBtA1rDpTa0jUPf2zhH5PbpHTU2DByOQrrp8QoZWc 93+IISRpQs1yfuC5uSNyd4XemVSKlLb0JPnZnB+A8BOiTAazsA+PzpS2Pc0MS9qZzu1c99Z5 NwdtIC3ZFoTIazBycI/fzBTTg9mBPgTkFPHCSDXXc27ykTHdz7hz6wrAhxte4If/elzDCdF8 vlwxDIlNEjSwbLrhujjGq8x3azPL+GzVG8bkntt0zDWEPcrW7jMRqzL4ZlT2zJYasVmRK6AP pZENmsHgBLoaSBDOGYXGdEHn8yGinb5aRF99Wm3jP9ii4TU5FUpjOKF3MDuUteNXIBemluSj nnX+nzwRBAcLt2WjzSfmk9AncfKlCL/HY8eTfi2q6Usj1qUyWgeThYRUDNXvMVVlGaSUoJeN 0s5pxAxrKVj0m6HZ9KgcQWB9SvsUgEnZ/JcFOgz6Qeow6XS4hqECmVsctKnQIx53CPRbWx6v mJlj+8FFhQ07+LIESP1GqO86GLtaXJMfAfucAddFVNdi+QPtr3fmf4mczqOOKu8j9mwFD2ph j7X924xgLIcicNN3KK+lbwmv95OjsiQJuLWzl+PNo5A0u+fTND/D2BPwQaAhcus1K7DEjG8U IEswqByFtwmA5CXjzCqS+4QBryv7PvtGGSC3Q83Rsh9qW72pybLkWVsDNdWdBgB3iEsKW+BX aMvkV45CGJ7YCP6PPYvPepd9exzlfK7SYuNug/ogipmO8AtLmdrDQlhYkmf222FraTfufBXB HtvSu71VSxyIf0/klKeHr5FuZdyn3xW7T6NGPjTkkv/uZLDNSb9YepUazOmM7FphIva+lm92 4gEbKOilU4PONASlwGNrub/23hRfSZlbX03wuQLHtO+zv1OQzh7UaKOmO9/IOSIXc19z4/1w 510YWcAoHKXuJENAVzihqlLZOy9UJBhg2g8OCBwb1+k12JyM4mq5aYbMZAweOB/puBkyPd1S dgDetmBUqwfEGSZp2xFYMmvtpFmeTSqmRmKYHiobT05SJhqGF7E99riSQ3w+XRcFSGwr8Y// +at21qDE5oOTghvFujMb/erww/jtHQRgrMgUE7BI90Vc0LpqdA4Jyv0h/4xAscNNRSTnmvAh 1jKWU8V/LCfrZU0/d/FgbG/g72oS+YuTFBHG2T77KqtMXaI82emx7hGWrnacD3YUlTy5/z+N +hYyvfLMMoHkkxPhIxyHus51qk5/dbu++ZXwwk4TnXGa1OnVuFpLnWch5Ids6RMwvpUtVLzV B/UvNZdPrqNNYXuF1tIfFgpaeGK1Pc1nDjO7KRqfB+runcvpLfXA19POxSsiTBGKOcnOo0Sx +p86tUd7Bayi0Z3P9va3DpY8X+Aci4JX6k97MpIBYbqjk8mxggHb8GHTCDx556LZpNHNUxze m2Yg6/LhrJ9wEvecipsSSKcg7IF3Zle6gpXyFIiJkiSnoaXjPEA2hAMoy88SR5Yz0ka3u9+U oSx25aZ+UlTE/ZUaMl/s6SEHghAAFiU9hW0xQZS0mLeSEasWyrGK2hV1SNhOqwG2zo0Q9SZ1 OjwJKXZvfLCc8T43y90UklgwxAmZcIk7RXMwahLAOzcd6TXolPZbmuGam8Bqh+hCsQ07KECS S+G484oAZDG2eUsT2HXxmVUOXn8iPxJGYCafcxcwQ==
Ironport-hdrordr: A9a23:gQFdZ6hEEDPLteMTF4kuG/ElzHBQXvcji2hC6mlwRA09TyXqrb HWoB17726WtN91YhsdcL+7Scy9qB/nhORICMwqTMqftWrdyQ+VxeNZnOnfKlTbckWUltK1l5 0QCJSWYOeQMbEQt7ed3ODXKadZ/DDKytHOuQ4c9RtQpMNRBp2IIz0XNu9TKCNLeDU=
Ironport-phdr: A9a23:gClbfBHX7iTQ1u1TiIYp+J1Gf/NGhN3EVzX9CrIZgr5DOp6u447ld BSGo6k31hmQAtmQsawMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7G MNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+5YPfbx9ViDe/br5+I wu6oATMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2Q rxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v6 bpgRh31hycdLzM27GLZhMJ/g61VvRyvuRJ/zY7Wb4yOLvVyYrnQcMkGSWdPXMtcUTFKDIOmb 4sICuoMJftVoJf7p1sJowO+GRGjC+zuyj9Hm3/23LM10/48GgzBxwMvAcwOsHXbrNXoNacdT /q1wbLHzTXGdfxW2DP95JLUfRAmpPGBRLR9etfexkczDQ3KlEmQqZD7MDOP0OQAq2yW4vRhW O+zhGMppQN8riazy8otlITEiZ4Zx1TH+Ch43Is4Jtm1RUplbdO4DJZdtj+WOoh5TM0iQmxlu ic3x7MAtJWmciYKz5EnyATea/yBa4WI7RPjVPqRITdln31pYq6whxG38US4xOz8V8q00FdSr iVbj9bMt2oC2wbU6sidRftw+Fqq1zWX1w3L9O1IPUQ5mbDYJpMh2LI8iIYfvEfZEiL2lkj6l LGaeV849uS27unoeLrrq5CTOoJxiAzxL6sjltK6DOglNwUCQXaU9Ouh2LDm+UD1XahFg/kzn 6bFrJzVO9kUq6u7DgNI0osu5BCyBCq83tsCh3kINldFdQqHj4f3P1HOJ+j1DfKljFStlDdn3 u7JMaD8DpnUIHjOkLnscaxy605bzwozwtRf6IxOBr4dJ/LzX1f9tN3eDhAnLwy52/jrBMl52 48EWm+CArWVPL3OvVKL/O4iI+eBaJcQuDnnKvgl4/DujWU+mV8YZaSmxoUYaG65HvRpPkWZY GTjgs0aHGcFuwoxVu3qiFmYXTFPYHayWrow5jcgB42+F4fMWpitgKCd3Ce8BpBae3hKCkqQH nfwa4WER/AMZTqOLc9mizwITKSuS4s81R61rwL60LpmLu/M+iICr57j1d515/fSlR4o7zB0A d6dgCmxSDR/mXpNTDsr1oh+p1Z8wxGNy/tWmftdQPZe4fTPTjAENJHBzuFgQ4T4VxzAccqIR UyOTdCvADV3RdU0lYxdK31hEsmv20iQlxGhBKUYwuTj7P0c96vd2yO0PMNh0zPd07FniVA6Q 8xJPGngh6hl9gGVCZSa216BmfOMcqIRlDXI6H/F1XCH6UtVTg9/TKTIR1gQY0LXqZLy4UaRB 6S2B+EfOxBagdWHNrMMb9ToiVtcQ/K2MtnAYm2smmqqLRmNz7KIKoHtfjZVxz3TXW4DlQ1b5 nOaLU4+CyOm9nrZFyBrHEnzblnE9OB/rDa2QhZxwVzRKUJm0LWx91gegvn0p+o7+LUCtW9hr jx1GA34xNfKE5+boBIneqxAYNQ76VMB1GTDtgU7MIbyZ6ZlzkUTdQh6pSaMn11+F5lAnM42r Xgr0Bs6KKSW10lEfi+Z2pa4M6PeK2379hSiI6DM3VSW3NGT86YJoPM2zjer9AukCEst7nRqy fFa1nKd4tPBCw9TGZP9X0Ar9gRr8qnAa3p17IfV2HtwdKis52WaipR5Wa1/kkbmIowMVcHMX BX/GMAbGcW0fekjmlzyKwkBIPgX76ksecWva/qB3qeveudmhjOvy2pds+UfmgqB8TRxTunQ0 tML2fadi0GNWin9g0qgv9rfloVNZDVUFW26g3uBZsYZduhpcIAHBH37ace62NRxmp/gQVZX8 VeiAxUN38rjKlKCKlf62wNXz0Eep3eqzDC5wzJDmDYstqOD3SbKzowObTI/M3VQDClnhFboe s2viswCGVOvd04vnQek4kDzw+5aor5+Ji/dWxUAcy/zJmBkGqy+09jKK8RC9pInrCRaSsyzZ FmbTvj2pB5S3y74HmRYzSw2bHnw4sS/z0E80jrNaiso5HPCMdl93xLe+MDRSZszlnIdSS90h COWTlmwMt+1/MmFwpLKs+SwTWWkBdVYdSjmy5/FtTPuvzU7R03i2arrypu6Sltfs2ezzdRhW CTWoQypZ4Dq0///Kud7ZgxzA0e67cNmG4Z4m492hZcK2HFciI/GmBhP2Wr1L9hf3rrzKXQXQ jteidTY/gnqxUxuNFqGwov4UjOWxc4rNLzYKisGnzkw6cxHEvLe5rFanCRoo1eihQ3UaPl52 DwazLF9jRxSy/FMsw0rwCKHB7kUFkQNJi3gmSOD6NWmpblWbmKiIvCgkVBzlte7APSesxlRD TznL4w6E3Y6vaAdeBrclWf+4Yb+dJzMYMIP41eKxgzYgbEdKYptxKFXw3M2YSSn4SJjk6lh0 VRvxc3o4tTBcT42uvvnWlgAcWSkAqFbsjD10fQAwIDPh9rpRtM5XW9TFJrwEaD2TnRI6aWhZ 17ISHpm8j+aAeaNQlXZsRsg9iOVVcjsbiHyRjFRzM0+FkbBYhUF3UZMGm19x8BxFxj2lpW5I AEguW9Xthig7UEVguNwa0umDTyZ/Vb0LG9yEN/Gcn80pklD/xuHa5TPqLIuWXgCrtv561XSY m2DO1YSVD9PBxzCXgG5eOHpvIiI8vDEVLDncb2UOuTI8rYYD7DRlPfNmsNw9jKIfK1jJ1FEC Ps2kgpGVHF9QIHCnikXDjcQj2TLZtKaoxG1/mt2qNq++bLlQlCn44zHELZUPdh1nnL+ya6eK +6dgjp4IjdEx9sNw3HP0r0WwF8VjWlnaTCsFb0KsSOFQrjXn+dbCBsSaiU7M8Utjep0xg5WJ cvSkc/4zJZ9h/8xTlpJDBnvx5rvassNLGWwcljAAQfDNbiLIyHK39CiYa64Tu417q0cvBmxt DCHVk77a27bxn+5Clb1abEK0XrIWX4W8JuweRtsF2X5GdfvaxngdcRykSVz2roswHXDKW8bN zF4NUJLtLyZqy1C0ZAdUyRM6GRoKe6clmOX9e7df9wcvOVqDTl1mvhy73Ezyr8T5yZBDq8Q+ mOavpt1rleqn/PagCJgSwZLoy1XiZijuExjPeDU+sAFVyufuh0K6mqUBlIBoN4vWbiN8+hAj 9PIkqz0MjJL9dnZqNAdC8bjI8WCKHM9MBDtFVY87SMARD+vcGzT3glTzarU+XqSoZw37JPrn chWIle0fFMwH/IeTE9iGY5bSH+SdjwhmL+fysUP4CjmxCQ=
Ironport-sdr: HPboWJA/nkiRFETrrXt931jkcJ9n6u7z5rOPTeOAcTPKa8OIWkq+Jb1mTEQkUtT3BcOU+syapn VJu8caW1hFEYeqRMJbzA/7RyfsXtJEGYdfDuAt3vgBTSIt5ZWUAMzFepkazwV6Iul2W/7OmPvq EQ4MYzAoXSyZsd7o0W+c2I5Wyin9MRQrVQRDr5+JI1Bx24EaUUVe610wiSxYzo1rvS6xa5frWI 1OeQ62cKtdS9HT+hHS+u2f9OiFWtAry+IK1G25iRK1qCPkyGhhkmheh8PrJNUF4qdTVlFoGWjv mSMVi2CUlaTn8Vk8ahz1MFkN

Hi Tim,

here is an example of using CoqPrime.
We verified that 2^255 - 19 --definitively bigger than 32 bits-- is a prime number:

https://github.com/ildyria/coq-verif-tweetnacl/blob/master/proofs/spec/High/prime_and_legendre.v
https://github.com/ildyria/coq-verif-tweetnacl/blob/master/proofs/spec/High/prime_cert.v
https://github.com/ildyria/coq-verif-tweetnacl/blob/master/proofs/spec/High/prime_ssrprime.v

Kind Regards.

Benoit.

On 4/5/22 03:14, roux cody wrote:

I'm sure someone will have already posted this by the time I send it, but here's a nice approach from a few years ago that probably still compiles: https://github.com/thery/coqprime originally from Werner, Gregoire and Thierry, which formalizes this: https://en.wikipedia.org/wiki/Pocklington_primality_test

The idea involves running (fast) C code to generate *certificates*, which then are checked by verified Coq code in P time.

This is actually the "right" way to do it IMHO, since AKS is still pretty slow as far as I know.

On Mon, Apr 4, 2022 at 4:06 PM Timothy Carstens <intoverflow AT gmail.com> wrote:

Let p: Z be a 32-bit positive literal. Suppose p happens to be prime. What’s the best way in Coq to prove that it’s prime?

The standard library provides a definition of primality for Z, and even provides a decision procedure, but the decision procedure does not seem very fast.

At a glance it appears mathcomp-extras provides a proof of the AKS primality test, but I’m a mathcomp novice and to my novice eyes their definition appears to be for nat (not N or Z).

Does anyone have a trick for this?

Thanks in advance,
-t

[Coq-Club] Proving p: Z is prime for large p, Timothy Carstens, 04/04/2022
- Re: [Coq-Club] Proving p: Z is prime for large p, roux cody, 04/05/2022
  - Re: [Coq-Club] Proving p: Z is prime for large p, Benoît Viguier, 04/05/2022
    - Re: [Coq-Club] Proving p: Z is prime for large p, Timothy Carstens, 04/05/2022
  - Re: [Coq-Club] Proving p: Z is prime for large p, Michael Soegtrop, 04/05/2022
- Re: [Coq-Club] Proving p: Z is prime for large p, mukesh tiwari, 04/05/2022