Support for secp256k1

[smondet]

#101 says it requires "more thorough investigation"

is it planned?

[hannesm]

The good news is that the primitives (finite element operations) can be generated by fiat-crypto.

The missing bits are the group operations, and the DSA/DH (depending on what you need) on top of it -- this was easy (available) for the r1 curves (point_operations.h / inversion_template.h) -- if you find corresponding code somewhere in the public domain (under a permissive license), that should be straightforward. Maybe you want to follow up on mit-plv/fiat-crypto#1444? Or follow the discussion over there to find the right code?

I won't have much time to look into this, unfortunately.

[ansiwen]

@hannesm: I looked into this and have the plan to implement it. Some questions, before I dive deeper into this: in mit-plv/fiat-crypto#1444 (comment) the ecckiila project is mentioned, which creates the group operations for a=0 from OP3 files of the algorithms from https://eprint.iacr.org/2015/1060. Have you looked at these at that time already and ruled them out for some reason? Or would it be ok to use these?