1# Fiat 2 3Some of the code in this directory is generated by 4[Fiat](https://github.com/mit-plv/fiat-crypto) and thus these files are 5licensed under the MIT license. (See LICENSE file.) 6 7## Curve25519 8 9To generate the field arithmetic procedures in `curve25519.c` from a fiat-crypto 10checkout (as of `7892c66d5e0e5770c79463ce551193ceef870641`), run 11`make src/Specific/solinas32_2e255m19_10limbs/femul.c` (replacing `femul` with 12the desired field operation). The "source" file specifying the finite field and 13referencing the desired implementation strategy is 14`src/Specific/solinas32_2e255m19_10limbs/CurveParameters.v`, specifying roughly 15"unsaturated arithmetic modulo 2^255-19 using 10 limbs of radix 2^25.5 in 32-bit 16unsigned integers with a single carry chain and two wraparound carries" where 17only the prime is considered normative and everything else is treated as 18"compiler hints". 19 20The 64-bit implementation uses 5 limbs of radix 2^51 with instruction scheduling 21taken from curve25519-donna-c64. It is found in 22`src/Specific/solinas64_2e255m19_5limbs_donna`. 23 24## P256 25 26To generate the field arithmetic procedures in `p256.c` from a fiat-crypto 27checkout, run 28`make src/Specific/montgomery64_2e256m2e224p2e192p2e96m1_4limbs/femul.c`. 29The corresponding "source" file is 30`src/Specific/montgomery64_2e256m2e224p2e192p2e96m1_4limbs/CurveParameters.v`, 31specifying roughly "64-bit saturated word-by-word Montgomery reduction modulo 322^256 - 2^224 + 2^192 + 2^96 - 1". Again, everything except for the prime is 33untrusted. There is currently a known issue where `fesub.c` for p256 does not 34manage to complete the build (specialization) within a week on Coq 8.7.0. 35<https://github.com/JasonGross/fiat-crypto/tree/3e6851ddecaac70d0feb484a75360d57f6e41244/src/Specific/montgomery64_2e256m2e224p2e192p2e96m1_4limbs> 36does manage to build that file, but the work on that branch was never finished 37(the correctness proofs of implementation templates still apply, but the 38now abandoned prototype specialization facilities there are unverified). 39 40## Working With Fiat Crypto Field Arithmetic 41 42The fiat-crypto readme <https://github.com/mit-plv/fiat-crypto#arithmetic-core> 43contains an overview of the implementation templates followed by a tour of the 44specialization machinery. It may be helpful to first read about the less messy 45parts of the system from chapter 3 of <http://adam.chlipala.net/theses/andreser.pdf>. 46There is work ongoing to replace the entire specialization mechanism with 47something much more principled <https://github.com/mit-plv/fiat-crypto/projects/4>. 48