44 lines
2.3 KiB
Markdown
44 lines
2.3 KiB
Markdown
|
# 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 `693d62c6fd7370bf71b8eb3b9a5825dfd071fcac`), 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".
|
||
|
|
|
||
|
|
## 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>.
|