| # 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. |
| <https://github.com/JasonGross/fiat-crypto/tree/3e6851ddecaac70d0feb484a75360d57f6e41244/src/Specific/montgomery64_2e256m2e224p2e192p2e96m1_4limbs> |
| 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 <https://github.com/mit-plv/fiat-crypto#arithmetic-core> |
| 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 <http://adam.chlipala.net/theses/andreser.pdf>. |
| There is work ongoing to replace the entire specialization mechanism with |
| something much more principled <https://github.com/mit-plv/fiat-crypto/projects/4>. |
