Stream: math-comp users

Topic: Elliptic curves


view this post on Zulip Bas Spitters (Jun 30 2023 at 12:03):

There are at least the following libraries on EC in Coq:
https://github.com/thery/EdwardsEllipticCurve
https://github.com/thery/coqprime by @Laurent Théry
https://github.com/strub/elliptic-curves-ssr by @Pierre-Yves Strub

and https://github.com/mit-plv/fiat-crypto by @Andres Erbsen and @Jason Gross , which uses Coq prime.
I understand the history of these libraries. I know @Andres Erbsen has been working on integrating libraries.

Are there any plans on how to use/develop these libraries in the future?
I see some of these libraries could be added to Awesome Coq...

view this post on Zulip Karl Palmskog (Jun 30 2023 at 12:06):

CoqPrime and Fiat Crypto are in Awesome Coq and in the Coq Platform. I didn't add elliptic-curves-ssr since unsure if maintained, and the Edwards one is likely new?

view this post on Zulip Karl Palmskog (Jun 30 2023 at 12:20):

it's not obvious to me how one can group these other than by dependency on MathComp (elliptic-curves-ssr, Edwards)

view this post on Zulip Pierre-Yves Strub (Jun 30 2023 at 12:48):

My lib is in maintenance mode only

view this post on Zulip Pierre-Yves Strub (Jun 30 2023 at 12:49):

Having to running with the last version of mathcomp should be easy.

view this post on Zulip Pierre-Yves Strub (Jun 30 2023 at 12:49):

But there won't be any new results added (by me)

view this post on Zulip Bas Spitters (Jun 30 2023 at 13:22):

The Edwards one is from four years ago. It formalizes the elegant proof by Tom Hales.

view this post on Zulip Karl Palmskog (Jun 30 2023 at 17:00):

is it really all that easy to port elliptic-curves-ssr to MC 2.0? For insiders maybe.

view this post on Zulip Pierre Roux (Jun 30 2023 at 17:33):

The difference between MC 1 and MC 2 is really in the use of Hierarchy-Builder for the structures. Apparently, elliptic-curve-ssr contains 4 structures and 173 instances so I'd expect the port to be relatively easy.

view this post on Zulip Karl Palmskog (Jul 01 2023 at 20:55):

recall that our door is open for proposing to move/consolidate projects. We try to facilitate discussions with original authors for getting useful packages/code on track to releases and/or Platform. However, without a volunteer maintainer, a proposal likely won't get far.

view this post on Zulip Laurent Théry (Jul 13 2023 at 08:36):

Bas Spitters said:

There are at least the following libraries on EC in Coq:
....
https://github.com/thery/coqprime by Laurent Théry
....

just for completness I have also ported the elliptic curve of coqprime in mathcomp here

view this post on Zulip Bas Spitters (Jul 13 2023 at 09:15):

Nice! I didn't know about math-comp-extra.
Is there a good overview of the math-comp ecosystem somewhere? Including information about what is hoped to be maintained in the longer run, CI, etc ? I looked here:
https://github.com/math-comp/math-comp
https://math-comp.github.io/
But didn't see it.

I see it's mentioned here. Maybe the MC libraries should also be grouped together (also search works OK).
https://github.com/coq-community/awesome-coq

view this post on Zulip Karl Palmskog (Jul 13 2023 at 09:27):

MathComp Extra is listed in Awesome Coq. However, grouping by MathComp doesn't fit the format of Awesome lists, which are usually by domain. What I can do is consistently add "Mathematical Components" somewhere in the description for projects that are explicitly based on MathComp. There are also projects that have some optional MathComp support, such as Relation Algebra, Autosubst, and these are difficult to classify

view this post on Zulip Karl Palmskog (Jul 13 2023 at 09:33):

as for maintained in the long run, I think there are now two ways a project can be considered this way:

  1. it's in the Coq Platform
  2. the maintainers say it will be maintained in the long run

I'd say it's very rare to get a statement like 2. from any project, so a list of such projects seems unfeasible.

view this post on Zulip Bas Spitters (Jul 13 2023 at 12:16):

So, maybe mathcomp extra should be in the extended edition of the platform (I forgot the name).
[ I have no immediate plans of using it myself. ]

view this post on Zulip Karl Palmskog (Jul 13 2023 at 12:26):

my view: results of general MathComp interest from MathComp Extra and similar smaller projects could go into [Platform project] CoqEAL by request, example: https://github.com/coq-community/coqeal/pull/70

Results in CoqEAL can then in turn be considered for inclusion into "proper" MathComp projects in the mathcomp logpath prefix, or MathComp itself.

view this post on Zulip Karl Palmskog (Jul 13 2023 at 12:28):

the MathComp wiki might be one way to link/document some of the smaller projects: https://github.com/math-comp/math-comp/wiki

view this post on Zulip Bas Spitters (Jul 13 2023 at 12:48):

Makes sense. Is there a reason to choose coqeal in particular for this? I guess because it's already in platform?

view this post on Zulip Karl Palmskog (Jul 13 2023 at 12:50):

yes, it's already in the Platform, but also, it's already a collection of "utility" results of sorts, rather than a completely focused package

view this post on Zulip Karl Palmskog (Jul 13 2023 at 12:58):

also a Coq-community project, so there less of a chance of results getting stuck in limbo

view this post on Zulip Bas Spitters (Jul 14 2023 at 07:14):

Coqeal was developed in the formath project as an Effective Algebra Library. I guess it's OK to shift focus if that's what the maintainers want.

view this post on Zulip Karl Palmskog (Jul 14 2023 at 07:35):

"algebra" is a big subject, arguably a lot of CS is logic + algebra

view this post on Zulip Karl Palmskog (Jul 14 2023 at 09:22):

for example, this repo description in my view covers quite a lot:

developments in algebra [...], and optimized algorithms on MathComp data structures.


Last updated: Jul 25 2024 at 15:02 UTC