search

mit-plv / fiat-crypto

Cryptographic Primitive Code Generation by Fiat
http://adam.chlipala.net/papers/FiatCryptoSP19/FiatCryptoSP19.pdf
Other
714 stars 147 forks source link

Using abstract fields in Bedrock specs #1150

Open RasmusHoldsbjergCSAU opened 2 years ago

RasmusHoldsbjergCSAU commented 2 years ago

I asked about this here: #1113 , but am not sure if anyone has seen it.

The question is about the specs for Bedrock2 field operations in Bedrock/Specs/Field.v. Currently these depend on Arithmetic/PrimeFieldTheorems.v, allowing only fields of prime order. Is there any reason to prefer this?

For me, it would be more convenient to have the specs depend on arbitrary finite fields, rather than just those of prime order.

I suggest the following changes: Splitting the Bedrock/Specs/Field.v file in two; one that is similar to the current version, but using abstract fields from Algebra/Hierarchy.v instead of prime order fields from PrimeFieldTheorems.v. The other file would specialize the specs from the first one to a field from PrimeFieldTheorems.v, much like the current version, and be used in the synthesis pipeline.

Although I am not sure to what extent this change would interfere with the ongoing work of others; @JasonGross, @andres-erbsen, @jadephilipoom?

If you are happy with these changes, I will gladly make them.

andres-erbsen commented 2 years ago

I'm honestly not sure what the appropriate factoring of field structure assumptions and bedrock2 specifications is. What are you looking to use the extension-field specifications for -- our montgomery ladder derivation?

RasmusHoldsbjergCSAU commented 2 years ago

I made these a while ago;

https://github.com/AU-COBRA/AUCurves/blob/c854f5502106a021921f92309e55b52f7c45a734/src/Bedrock/Curve/BLS12Curve_G1.v https://github.com/AU-COBRA/AUCurves/blob/c854f5502106a021921f92309e55b52f7c45a734/src/Bedrock/Curve/BLS12Curve_G2.v

Implementations of subgroups G1 and G2 of Weierstrass curves used in the BLS signature scheme. These use the same curve addition formula, so the only difference between them is the underlying field. A lot of work has been duplicated by doing both of these by hand. Ideally I would want to abstract over the underlying field so that one implementation could be used for both of these groups, and other Weierstrass curves as well. Since G2 is defined over a quadratic extension of a prime-order field the field specifications used for this should be general enough to cover extension-fields as well.

I am not aware of any use-case for Montgomery curves over extension-fields; so i suppose the Montgomery ladder derivation can be left as is and still be used for e.g. Curve25519.