mit-plv
Mike Hamburg's scalar multiplication with precomputation
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.
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.