coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Timothy Carstens <intoverflow AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Proving p: Z is prime for large p
Date: Tue, 5 Apr 2022 10:09:39 -0700
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=intoverflow AT gmail.com; spf=Pass smtp.mailfrom=intoverflow AT gmail.com; spf=None smtp.helo=postmaster AT mail-pj1-f44.google.com
Ironport-data: A9a23:0uGvua1tPG95J6C9v/bD5ex3kn2cJEfYwER7XKvMYLTBsI5bp2YOx zZLUWmBPf+NamSgco9zbdnioRhTu5bTnII3GgA+3Hw8FHgiRejtVY3IdB+oV8+xBpSeFxw/t 512hv3odp1coqr0/0/1WlTZhSAgk/nOH9IQMcacUsxLbVYMpBwJ1FQyw4bVvqYy2YLjW1/V5 IuoyyHiEAbNNwBcYjp8B52r80sHUMTa4Fv0aXRjDRzjlAa2e0g9VPrzF4npR5fLatU88tqBe gr25OrRElU1UPsaIojNfr7TKiXmS1NJVOSEoiI+t6OK2nCuqsGuu0o2HKJ0VKtZt9mGt/pr8 u11l8eociI4B5DQg6c4CEUAOT4raMWq+JefSZS+mcmazkmDa3m1hvsyUAc5OooX/usxCmZLn RAaAGpVP1bT2qTsmez9FrUEascLdKEHOKsevG1n0zzDA/IhXrjMRqzL4ZlT2zJYasVmRq6EP 5pHMmoHgBLoXBdCHWYMFtEHp/qHuXqvdyFIoXuKuv9ii4TU5FUpjOKF3MDuUteNXIBemluSj nnX+nzwRBAcLt2WjzSfmk9AncfKlCL/HZoQTfi2qqIsj1qUyWgeThYRUDNXvMVVlGaUQehnE 25P4hELvJEP6Ffoa4KhBzen9SvsUgEnZ/JcFOgz6Qeow6XS4hqECmVsctKnQIx53CPRbWx6v mJlj+8FFhQ07+LIESP1GqO86GLtaXJMfAfucAddFVNdi+QPtr3fmf4mczqOOKu8j9mwATOph j7W8G4xgLIcicNN3KK+lbwmv95OjsiZJuLWzl+PNo5A0u+fTND/D2BPwQaBhcus1K7DEjG8U 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++ZXwwk4TnXGa1OnVuFpLnWch5Ids6RMwvpBu1LzV B7TvNZdPrqNNYXuF1tIfFgpaeGK1Pc1nDjO7KRqfB+runcvpLfXA19POxSsiTBGKOcnOo0Sx +p86tUd7Bayi0Z3P9va3DpY8X+Aci4JX6k97MpIBYbqjk8zyAgHb8CATCDx556LZpNHNUxze m2Yg6/LhrJ9wEvecipsSSKcg7IF3Zle6gpXyFIiJkiSnoaXjPEA2hAMoy88SR5Yz0ka3u9+U oSx25aZ+UlTE/ZUaMl/s6SEHghAAFiB+BW0xQdV0mLeSEasWyrGK2hV1SNhOqwG2zo0Q9SZ1 OjwJKXZvfLCc8T43y90UklgwxAmZcIk7RXMwahLAOzcd6TXolPZbmuGam8Bqh+hCsQ07KECS S+G484oAZDG2eUsT2HXxmVUOXn8iPxJGYCafcxcwQ==
Ironport-hdrordr: A9a23:rcCmN6nyzNdaF84g/a7XEnENw5jpDfIV3DAbv31ZSRFFG/Fw9v re5cjzsCWftN9/YgBEpTntAtjjfZqYz+8X3WBzB9aftWvdyQ+VxehZhOOI/9SjIU3DH4VmpM BdmsZFebvN5JtB4foSIjPULz/t+ra6GWmT69vj8w==
Ironport-phdr: A9a23:Lk47sBDp2Cs3tfL1tV/AUyQUzUkY04WdBeb1wqQuh78GSKm/5ZOqZ BWZua83ygaWAc6Cs64MotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7G MNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+5YPfbx9ViDe/br5+I wi6oRneu8ILnYZsN6E9xwfTrHBVYepW32RoJVySnxb4+Mi9+YNo/jpTtfw86cNOSL32cKskQ 7NWCjQmKH0169bwtRbfVwuP52ATXXsQnxFVHgXK9hD6XpP2sivnqupw3TSRMMPqQbwoXzmp8 rxmQwH0higZKzE58XnXis1ug6JdvBKhvAF0z4rNbI2IKPZyYqbRcNUHTmRDQ8lRTTRMDYyyb 4QND+QPM+VWoZTjqVQSthaxHxWgCfn1xzNUmnP736s32PkhHwHc2wwgGsoDvmrVrNXwM6cST eC1zanVxjjddfxWwyz96JTWfRAnuvGHQLV9ccvXyUkzEAPFkEufqZbrPzOR0eQMvXOW7+VlV e21im4nrxt9rSSoxscpk4TEgJ8exV/Y+ytj2ok1OcG4R1BhYd6iCJZcqT+XOoR1T848R2xlu To3x7IYtJC1YiUG1pQpyh3BZvGFb4SF4QzvWuiSLDtmgH9reKyyigqu/US8xOPxWNe43VBXp SRLldnMs2oC1x3V6sWfRft9/1uh2TaS1w/I8O1LPUc0la/DJ58vw74wlZsTsVzdESDrmUX5l rWadkI++uin7ensf7bopoeEOoNqlg3zNr4il8+/DOgiLAQCQmmW9f6z2bDs+0DyXa9Egecsk qbDtZDXPcQbqbC9Aw9Syosj7gywDzai0NgBhXkHLk9JdAuJj4XmNFzCOv/4DfC4g1SjlDdk2 erKMaHmApXINnTDkbHhcqhh60NE1gY/0dRS64hXB7wBOv7/RFL9ud3CAhI2PAG42+PnB8981 oMaV2KPGKiZMKbKvF+J4OIvP+6MZJELtzbnJfgl4/nujHEilF8SeKmmx5oXaHSiEvt6JEWZZ GLggtEaHmgSpAoxUPTqiEGeUT5Uf3u+Qrow5isnB4K+EYfDWoetjaSd0ye8B51af3xJClSRE XjzbIiEQPcNaCeKIsB7iDAEVL6hS5Ug1R60rgP6xaBnfaLo/Xgzsour/9xo7aWHnhYrsDdwE s610meXTmgykHleFBEs26UqnU14zUuDwOBTiuZDCdFV/LsdUwEmMoDR1eJ+DM/aVQfIf9PPQ 1GjFIb1SQotR848loddK312HM+v21Wah3LC6949krWKAMZx6afAxz3rIM07zX/a1a4nhl1gQ 81VNGTgiLQsvxPLCdvvlEOU372vabxaxDTEoWaF0W2QsVtWVAlvearAVHEbIEDRqIex/VvMG oenEq9vKQ5d0YiHI6pOZMfuiABHQuvkJtnEbWa2hE+/AB+JwvWHa4+5M34F0nD7D04J2xsW4 W7ANQU6AXK5pHnCCTV1CV/1S0bl8O07sHHiC0Fok0eFaEpu07fz8RkQ7RCFY9UU2L9M+CIoq jEuWU24w8qTEd2L4QxoYKRbZ9o5plZBz2PQ8QJnbNSmKOh5i1gSfh4S3Qum3ghrCohGjckhr W87hAt0J6WC1VpddjSelZnuM7zTI2P28VihcanTkl3Z1d+X/O8I5pFa4x3iuh2uCEc4/XFgz PFa1nKd4tPBCw9TGZP9X0Ar9gRr8qnAa3p17IfV2HtwdKis52WaipR5Wa1/k0jmI4sMVcHMX BX/GMAbGcW0fekjmlzzKwkBIPgX7qk/ecWva/qB3qeveudmhjOvy2pds+UfmgqB8TRxTunQ0 tML2fadi0GGUSv7klq7vMTwhqhLYDgTGiy0zi2uV+szLuViOJ0GD2ujOZj9x9NigIDgQXBc8 0GLCFYP2cvvch2XJQ+Yv0UYxQEcpnqpnjG9xjp/nmQyr6aR6yfJxvzraBsNPmMjqHBKtV73O sD0itkbWBLtdA01jF6/4k28waFHpaN5Jm2VQEFSfiGwIXswGqe3s7ODZYZI5vZK+W1WVvi7f 12ARLr6vDMV1iriGy1VwzVzezyxu5r/lgB3kyrHdCc1/CefI5gug0uDrNXHDeZcxD8HWDV1h Vy1ThCnMt+l8M/V35bPv+aiVn6wA5hacC3l14SF52Ow4WxnBwH6nujmwIW2V1hnl3WiiZ82C Xatzl60eITg2qWkPPgye0BpAAW58M9mAsRklYB2gpgM2H8cj5HT/HwdkG61P88IvMC2JHcLW zMPxMbYpQb/30g2ZHOP24XnW2+Txsx+T9a/a2ISnCk66ooZbcXcpKwBhiZzrlei+EjQZ+R6g DoHx/8p91YVhugIvEwmySDXUdVwVQFIeCfrkRqP9dW3qq5aMX2ufbaH3017hdm9DbuGr1IUS DPjd5wlByM18tRnPQeGzijo8o+9Moq1D5pbpliOnhzHleQQNJ8hiq9Am398IWyk9Xw9l7xg0 Fo3jMn85tTYbT0qpv7xAwYEZGOpIZlIoXe00/4YxoHPjuXNVt1gAmlZAsWuFKryVmpU7bO9b 06PCGFu9CndQ+aOW1/Hrh8h9SqHEoj3ZS7NYiBFi4wzHl/FYxUP5WJcFDQiwsxmSkbznpGnK AEhoWlPrl/g9kkVkrIubkagFDeZ/EDyM381UMTNdUUNqFgTuwGNd5TZt7wWfWkQ/4X9/lbVe yrLOkIRVzFPAgvdWBjiJuX8v4CetbXIQLPvdb2WJuzf4e1GC6XSnMzpiNA3uW3WcJ3IZygHb bVzzENHWToR993xvTIJRmRXkivMa5TevxKg4mhtqcv59v33WQXp7I/JCr1IMNwp9QrkyaGEf /Wdgip0M1M6ntsF2GPIxb4D3VUTlzAmdj+jFq4FvDLMS6SYk7FeDhoSYSd+fMVS6Kd00g5IM M/dwtT7s9wwxuYyEEtAXEf9l9uBYMULJySlNgqCChrXcruBIjLPzof8Zqb9AbxcgeNItgGh7 DaWF0iwW1bL3zLtVh2pLaRNlHTBZE0Y6Nz7KE8zTzS/H7eEIlWhPdR6jCM72+gxj3LObysHN CRkNllKpfuW5D9ZhfN2HypA6GBkJK+KgXX8jaGQJ5AIvP9sGikxmfhd5SFwyr1J6z9JXvJxn zT6odtnolXgme6KgGkCMlIGunNQiYSHsF83c73e7YVFUG3Y8Qgl6GyRD1ESpYIgBIGz/a9Xz dfLmeT4LzIIoLe2tYMMQsPTLsyAKn8oNxHkTSXVAAUyRjmuLWjDhkZZnZl6GVWaq5E7rt7nn 59cE9eztXQwH/IeT1xnRZkMfMsxUTQjnrqWysUP4CjmxPE0bMpft5HDEPmVBKe3QAs=
Ironport-sdr: dNpPQKfVeDVvYKn9Og9UeX5llUh0KQZVZxY4U4uxjIcEWTyWmXtATfMiMauhavobAgSAgf36r3 VOUUpUmVZBT/mGAGxZKtsQtRoZHH4mvXS445I9G+fYI04LoX+29qYL0m7IU7KT3Wt/OYnxGns/ 1JTUbnXcUgHab8SawvgHA9EjoFABkMCZTBejTfZSu11PAgJFB88/bqowoye582f7fdQ50CF/93 GmVgmtN2WwYdL5OENHEDjdeydtYV+xkSyRwjTIz3YQEIxnv6JXdfE2cg9osodhYx39MhBB7zNw gtGo9897G3CquM9Ew8LdCR6a

Thank you for the helpful replies! The coqprime package worked brilliantly.

On Tue, Apr 5, 2022 at 3:39 AM Benoît Viguier <beviguier AT gmail.com> wrote:

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