[curves] new 25519 measurements of formally verified implementations

[Jason A. Donenfeld]

Hey Armando,

Thanks for taking the time to fix things up.

I've loaded this into my kbench9000 software
<https://git.zx2c4.com/kbench9000/about/>, in the branch
"jd/curve-comparison", and tested it on two Skylake systems -- a
laptop and a server. With turbo disabled, results are fairly similar
between the two:

Intel(R) Xeon(R) CPU E3-1505M v5 @ 2.80GHz
     donna64: 160942 cycles per call
      hacl64: 140902 cycles per call
      fiat64: 144106 cycles per call
     sandy2x: 136074 cycles per call
precomp_bmi2: 121350 cycles per call
 precomp_adx: 117676 cycles per call
       amd64: 143628 cycles per call
      fiat32: 307971 cycles per call
     donna32: 544254 cycles per call

Intel(R) Xeon(R) Gold 5120 CPU @ 2.20GHz
     donna64: 162308 cycles per call
      hacl64: 141948 cycles per call
      fiat64: 146188 cycles per call
     sandy2x: 135502 cycles per call
precomp_bmi2: 121061 cycles per call
 precomp_adx: 117636 cycles per call
       amd64: 146382 cycles per call
      fiat32: 307777 cycles per call
     donna32: 548081 cycles per call

Your implementations are the two precomp_ ones. I split it into
separate paths for adx and for bmi2, so that we could test it together
on one system.

Regards,
Jason