Uses verified code generated by fiat-crypto for field arithmetic, and complete formulas to avoid side channels.

There's still plenty of room for optimizations, especially with a fixed base. But this gives us a framework to easily add other similar curves.