We introduce a new approach for implementing cryptographic
arithmetic in short high-level code with machine checked proofs
of functional correctness. We further demonstrate that simple
partial evaluation is sufficient to transform such initial code
into the fastest-known C code, breaking the decades old pattern
that the only fast implementations are those whose
instruction-level steps were written out by hand. These
techniques were used to build an elliptic-curve library that
achieves competitive performance for 80 prime fields and
multiple CPU architectures, showing that implementation and
proof effort scales with the number and complexity of
conceptually different algorithms, not their use cases. As one
outcome, we present the first verified high-performance
implementation of P-256, the most widely used elliptic curve.
Implementations from our library were included in BoringSSL to
replace existing specialized code, for inclusion in several
large deployments for Chrome, Android, and CloudFlare.
