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

Mike Hamburg's scalar multiplication with precomputation #196

Closed andres-erbsen closed 2 years ago

andres-erbsen commented 7 years ago

If anyone cared, we could make a verified clone of Mike Hamburg's scalar multiplication synthesis.

It accepts descriptions along the lines of:

The key generation algorithm uses the signed all-bits-set combs algorithm. On64-bit platforms it uses 15kiB of tables (5 comb tables, 5 teeth per comb, 3 coordinates per point,expanded to 32 bytes per coordinate). On 32-bit platforms it instead uses 12kiB of tables (8 combs,4 teeth per comb). (from https://eprint.iacr.org/2015/625.pdf)

Encoded as (from https://sourceforge.net/p/ed448goldilocks/code/ci/master/tree/src/generator/curve_data.py#l52):

comb_config = namedtuple("comb_config",["n","t","s"])
...
"combs":comb_config(5,5,18),
"wnaf":wnaf_config(5,3),
"window_bits":5,

And plugs them into the template https://sourceforge.net/p/ed448goldilocks/code/ci/master/tree/src/per_curve/decaf.tmpl.c#l996

I haven't yet figured how the parameters in the text correspond to the code, but it should be doable.

andres-erbsen commented 7 years ago

https://eprint.iacr.org/2012/309.pdf section 3.3 seems to explain it. IIRC, it is not actually "general" in the sense of encompassing other algorithms, but is fancy and fast.

andres-erbsen commented 2 years ago

this is https://github.com/mit-plv/fiat-crypto/pull/1225