Add CoqPrime to the Coq Platform

[palmskog]

CoqPrime is a library for certifying primality using Pocklington certificates and Elliptic Curve certificates. When the right options are used, the library can certify very large primes quickly, which is important in cryptographic applications. CoqPrime is used, e.g., in the Fiat-Crypto library which generates code for cryptographic primitives.

CoqPrime is to my knowledge the state of the art for practical primality checking in proof assistants (as opposed to reasoning about primality), so I think it is important to include it in the platform for this reason. It has releases going back several Coq versions and works on Coq 8.12.

The maintainer of CoqPrime is @thery.

[thery]

sorry I came back from holiday and I try to catch, not problem for me to move the library

[palmskog]

@thery as can be seen in the charter, inclusion in the Coq Platform doesn't require any changes to repository hosting, etc. It only implies an intention to actively maintain a project and make timely releases after a new stable Coq version appears.

Since CoqPrime has already had timely releases so far, the main reason I see for including it in the platform is better advertisement and convenience for potential users (as they will not have to actively seek it out or manually install it when they need prime certification, e.g., in crypto applications).

[thery]

The author(s) or current maintainer(s) of the package shall agree to the inclusion of their package in the Coq platform.

fine with me

[MSoegtropIMC]

@thery : sorry for the long delay - we first had to take care of general infrastructure issues in Coq Platform.

I am not sure how useful the coq package without the certificate generators is - for these there is no opam file.

One can easily generate opam packages for non OCaml code, e.g. I did an opam package for gappa and this was more convenient than one would think. There are a few issues with this, though:

• there is no opam conf package file for libecm which you appear to require - this is not much of an issue either (I already did quite a few opam conf packages for system libraries)
• in order to find the include and library path for GMP and ECM in a system independent way there is not much of a way around autotools. I can help you with setting this up in your project, but I would ask you to maintain it then (of course I can help with issues).

Would you like to follow this path or do you have other suggestions?

Btw.: what does the "o2v" tool do?

[MSoegtropIMC]

FTR: I included the coq library in Coq Platform 2021.09 8.13 and intend to include it in 8.14 beta.

The command line tools I did not include - I guess the library is still of some use.

As mentioned I am happy to prototype an automake of cmake based cross platform make mechanism for the command line tools but I would need a comment from @thery that this is what he wants.

[MSoegtropIMC]

I postponed the inclusion of the command line tools until the next release which will likely happen in November (for Coq 8.14). The Coq library is included.

[thery]

@MSoegtropIMC sorry I get too many messages from github and I overlook your request.
As you have noticed, the main makefile does not build the gencertif part.
I don't know whether this part can be made portable. There are currently two ways to get a certificate:

• our own generator pocklington that as you've noticed is using libecm.
• using the soft primo that generates a certificate name.o the command o2v translates it to a .v file.

If you think it could be done, I will be able to help and maintain it.

[MSoegtropIMC]

@thery : as mentioned I don't think it would be difficult. What needs to be done is:

• create an opam package for libecm - either compiling from sources or using depext and system libraries in case it is available on all relevant platforms via system package managers
• add a cmake or autotools based platform independent build mechanism for your certificate generator
• add an opam package for the above (I would keep it separate in opam from the Coq part)

In can do all this for the current version (assuming libecm is not more difficult than other libraries or requires a large number of prerequisites not yet in opam), but I would ask you to maintain it then. In case this is OK with you, would you prefer cmake or autotools for the platform independent build of your project?

P.S.: I use an email filter to filter github messages which contain @ into a separate email folder.

[thery]

Don't have a preference (I haven't been using any of them).
No problem I will maintain it whatever you choose.

[Zimmi48]

sorry I get too many messages from github and I overlook your request.

Consider tweaking your mailbox setting to display the messages where you are mentioned differently. See some advice at: https://github.blog/2017-07-18-managing-large-numbers-of-github-notifications/#prioritize-the-notifications-you-receive

[thery]

@Zimmi48 thanks

[MSoegtropIMC]

@thery : Ok I will use autotools then, afaik this is more popular in the research area. I likely can't make it for 2021.09, but it is no issue to have it for the November release.

[thery]

@MSoegtropIMC no problem

[spitters]

What is the status of this? It would be great to also have fiat included in platform.
mit-plv/fiat-crypto#925

[palmskog]

@spitters CoqPrime was included in the 2021.09.0 release for 8.13: https://github.com/coq/platform/blob/main/doc/README_2021.09.0_8.13.md#coq-platform-2021090-with-coq-8132-full-level

[thery]

coqprime is included but the update proposed by @MSoegtropIMC for the makefile to include the certificate generator is still to be done but this is not used by fiat crypto I guess

[MSoegtropIMC]

@spitters : yes Coq-prime is included in Coq Platform 2021.09 already, but only the proof checker, not the proof generator. With the latter the issue is that the make file is not platform independent - I have it on my ToDo list for 2021.11.

[Zimmi48]

@spitters About fiat-crypto, you should probably open a separate issue in the platform repo and secure agreement from the maintainers.

[spitters]

Thanks. I've already opened an issue on the fiat repo. I'm waiting for a response there. The ping here also triggered a ping there.

…

On Wed, Nov 17, 2021 at 2:20 PM Théo Zimmermann ***@***.***> wrote: @spitters <https://github.com/spitters> About fiat-crypto, you should probably open a separate issue in the platform repo and secure agreement from the maintainers. — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#28 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AABTNTSPPRYLIHXUQLCQ5MDUMOT3FANCNFSM4RLOGX6Q> . Triage notifications on the go with GitHub Mobile for iOS <https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675> or Android <https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub>.

[MSoegtropIMC]

@spitters : but please add a separate Coq Platform issue - I wouldn't like to have discussions on coq-prime and fiat crypto in this one issue.