Elliptic curve cryptography (ECC) is at the heart of some of the workhorse algorithms in TLS 1.3 and other important protocols. You may be shocked to hear that, for the modular big-integer arithmetic behind this kind of algorithm, expert implementers often write new assembly code from scratch for each new large prime modulus! The constant-factor performance win is so big that it makes sense to invest in that kind of specialization, compared to using, say, a standard bignum library based on dynamic allocation. But could we do the specialization automatically and save human engineers the trouble?

I will present Fiat Cryptography, a work-in-progress Coq library that can generate fast ECC code automatically from short descriptions of implementation strategies. While a particular run may spit out thousands of lines of low-level code, we also generate proofs of equivalence to the uncontroversial whiteboard-level math behind elliptic curves. The library’s architecture combines traditional manual proofs of data abstraction, generation of specialized code via partial evaluation, and some compiler verification. For curve 25519, the “hello world” of elliptic curves with a conveniently straightforward prime modulus, we are able to get within about 20% of the performance of the best known C implementation.