# Fiat Some of the code in this directory is generated by [Fiat](https://github.com/mit-plv/fiat-crypto) and thus these files are licensed under the MIT license. (See LICENSE file.) ## Curve25519 To generate the field arithmetic procedures in `curve25519.c` from a fiat-crypto checkout (as of `7892c66d5e0e5770c79463ce551193ceef870641`), run `make src/Specific/solinas32_2e255m19_10limbs/femul.c` (replacing `femul` with the desired field operation). The "source" file specifying the finite field and referencing the desired implementation strategy is `src/Specific/solinas32_2e255m19_10limbs/CurveParameters.v`, specifying roughly "unsaturated arithmetic modulo 2^255-19 using 10 limbs of radix 2^25.5 in 32-bit unsigned integers with a single carry chain and two wraparound carries" where only the prime is considered normative and everything else is treated as "compiler hints". The 64-bit implementation uses 5 limbs of radix 2^51 with instruction scheduling taken from curve25519-donna-c64. It is found in `src/Specific/solinas64_2e255m19_5limbs_donna`. ## P256 To generate the field arithmetic procedures in `p256.c` from a fiat-crypto checkout, run `make src/Specific/montgomery64_2e256m2e224p2e192p2e96m1_4limbs/femul.c`. The corresponding "source" file is `src/Specific/montgomery64_2e256m2e224p2e192p2e96m1_4limbs/CurveParameters.v`, specifying roughly "64-bit saturated word-by-word Montgomery reduction modulo 2^256 - 2^224 + 2^192 + 2^96 - 1". Again, everything except for the prime is untrusted. There is currently a known issue where `fesub.c` for p256 does not manage to complete the build (specialization) within a week on Coq 8.7.0. does manage to build that file, but the work on that branch was never finished (the correctness proofs of implementation templates still apply, but the now abandoned prototype specialization facilities there are unverified). ## Working With Fiat Crypto Field Arithmetic The fiat-crypto readme contains an overview of the implementation templates followed by a tour of the specialization machinery. It may be helpful to first read about the less messy parts of the system from chapter 3 of . There is work ongoing to replace the entire specialization mechanism with something much more principled .