[curves] new 25519 measurements of formally verified implementations

[D. J. Bernstein]

Tung Chou's sandy2x code was (as the name suggests) optimized for Sandy
Bridge. For Haswell and Skylake, the slides from Julio Lopez in

   https://hyperelliptic.org/tanja/lc17/ascrypto.html

report two followup implementations producing roughly 25% speedups for
Curve25519; see slide 67/83.

I do think that the hacl64 Curve25519 speeds are fast enough for pretty
much everybody, and verification is certainly a huge plus, but people
who want more speed should be aware of what's possible---and people
working on Curve25519 verification shouldn't think they're done yet!

---Dan