Zulip Chat Archive

Stream: Is there code for X?

Topic: Galois fields or Elliptic curves?


view this post on Zulip SnowFox (Sep 01 2020 at 10:23):

Hello world. I see mathlib has field, zmod and poly; but AFAICT does not have the common Galois Field extensions. I.e. Powers of primes and binary specializations. I'd like to implement ed25519 and ed448; and the ristretto255 and 448 groups on top of these. Have I missed anything relevant in mathlib? Can someone give me a push for how I should continue? Thank you in advance.

view this post on Zulip Johan Commelin (Sep 01 2020 at 10:59):

@SnowFox That's about right. There is a branch finite-fields trying to implement the other Galois fields, but it has been dormant for a while.

view this post on Zulip Johan Commelin (Sep 01 2020 at 10:59):

But recently we've had a lot of new stuff about separable extensions and such, so it should be rather easy to get those fields working now.

view this post on Zulip Johan Commelin (Sep 01 2020 at 11:00):

About two months ago, some people defined the group law on Weierstrass elliptic curves, but I don't think anyone has done edwards curves.

view this post on Zulip SnowFox (Sep 01 2020 at 12:05):

Thanks @Johan Commelin . Did you mean the finite-fields-exist branch? I'll need to poke around the branches.. many! :)

view this post on Zulip Johan Commelin (Sep 01 2020 at 12:14):

@SnowFox My bad, that must have been the branch name.


Last updated: May 19 2021 at 00:40 UTC