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