Formal verification: resurrect fiat-crypto with formally verified assembly

[mratsim]

This PR resurrects the old formally verified fiat-crypto backend from fafebac

• https://github.com/mit-plv/fiat-crypto
  And also combines it with CryptOpt, https://github.com/0xADE1A1DE/CryptOpt, an optimizer for x86-64 field assembly.
• https://0xade1a1de.github.io/CryptOpt/papers/KuepperEWGCSTCCGWY23-PLDI23-full.pdf
• https://arxiv.org/abs/2305.19586

This is to explore formally verified and correct-by-construction EVM / Ethereum with the push from the Ethereum Foundation.

Note: assembly files must be named .S instead of .asm or the Nim compiler (or gcc) doesn't want to compile them properly.

Performance

Unfortunately autogenerated assembly from CryptOpt is still significantly lagging behind Constantine's

AMD Ryzen 7840U (laptop 15W to 30W CPU)

Warmup: 0.7911 s, result 224 (displayed to avoid compiler optimizing warmup away)


⚠️ Measurements are approximate and use the CPU nominal clock: Turbo-Boost and overclocking will skew them.
==========================================================================================================

Addition        FiatCrypto[BLS12_381]         5 ns        18 cycles
Substraction    FiatCrypto[BLS12_381]         5 ns        18 cycles
Negation        FiatCrypto[BLS12_381]         4 ns        15 cycles
Multiplication  fiat_bls12_381_fp_mul        49 ns       161 cycles
Multiplication  cryptopt_bls12_381_fp_mul_18980        32 ns       108 cycles
Multiplication  cryptopt_bls12_381_fp_mul_18433        34 ns       113 cycles
Squaring        FiatCrypto[BLS12_381]        45 ns       148 cycles

Addition                                                               Fp[BLS12_381]        500000000.000 ops/s             2 ns/op             7 CPU cycles (approx)
Substraction                                                           Fp[BLS12_381]        500000000.000 ops/s             2 ns/op             7 CPU cycles (approx)
Negation                                                               Fp[BLS12_381]       1000000000.000 ops/s             1 ns/op             6 CPU cycles (approx)
Conditional Copy                                                       Fp[BLS12_381]       1000000000.000 ops/s             1 ns/op             4 CPU cycles (approx)
Division by 2                                                          Fp[BLS12_381]        200000000.000 ops/s             5 ns/op            18 CPU cycles (approx)
Multiplication                                                         Fp[BLS12_381]         43478260.870 ops/s            23 ns/op            78 CPU cycles (approx)
Squaring                                                               Fp[BLS12_381]         41666666.667 ops/s            24 ns/op            79 CPU cycles (approx)
--------
Multiplication 2x unreduced                                            Fp[BLS12_381]         83333333.333 ops/s            12 ns/op            41 CPU cycles (approx)
Squaring 2x unreduced                                                  Fp[BLS12_381]        125000000.000 ops/s             8 ns/op            29 CPU cycles (approx)
Redc 2x                                                                Fp[BLS12_381]         71428571.429 ops/s            14 ns/op            47 CPU cycles (approx)
--------
Linear combination                                                     Fp[BLS12_381]         26315789.474 ops/s            38 ns/op           127 CPU cycles (approx)
--------
BigInt <- field conversion                                             Fp[BLS12_381]         71428571.429 ops/s            14 ns/op            48 CPU cycles (approx)
BigInt -> field conversion                                             Fp[BLS12_381]         24390243.902 ops/s            41 ns/op           135 CPU cycles (approx)
--------
Inversion (constant-time)                                              Fp[BLS12_381]           498256.104 ops/s          2007 ns/op          6609 CPU cycles (approx)
Inversion (variable-time)                                              Fp[BLS12_381]           751879.699 ops/s          1330 ns/op          4380 CPU cycles (approx)
isSquare (constant-time)                                               Fp[BLS12_381]           569800.570 ops/s          1755 ns/op          5779 CPU cycles (approx)
Square Root (constant-time p ≡ 3 (mod 4) with addition chain)          Fp[BLS12_381]            92876.382 ops/s         10767 ns/op         35464 CPU cycles (approx)
Fused SquareRoot+Division+isSquare sqrt(u/v)                           Fp[BLS12_381]            91340.884 ops/s         10948 ns/op         36059 CPU cycles (approx)
Exp curve order (constant-time) - 255-bit                              Fp[BLS12_381]            88589.653 ops/s         11288 ns/op         37178 CPU cycles (approx)
Exp by curve order (vartime) - 255-bit                                 Fp[BLS12_381]           112145.340 ops/s          8917 ns/op         29370 CPU cycles (approx)

23ns in Constantine vs 32ns for CryptOpt for Fp mul :/.