kris/boringssl
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

add fiat-crypto code generation readme

Browse Source 
Change-Id: Ie4060121f6bc8da07d87db8ec8133ea17e99e1fe
Reviewed-on: https://boringssl-review.googlesource.com/24344
Reviewed-by: David Benjamin <davidben@google.com>
Commit-Queue: David Benjamin <davidben@google.com>
CQ-Verified: CQ bot account: commit-bot@chromium.org <commit-bot@chromium.org>
This commit is contained in:
Andres Erbsen 2017-12-21 12:28:57 -05:00 committed by CQ bot account: commit-bot@chromium.org
parent 6df6540766
commit 36fce983b6
1 changed files with 38 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

38
third_party/fiat/README.md vendored
View File

@ -3,3 +3,41 @@
Some of the code in this directory is generated by Some of the code in this directory is generated by
[Fiat](https://github.com/mit-plv/fiat-crypto) and thus these files are [Fiat](https://github.com/mit-plv/fiat-crypto) and thus these files are
licensed under the MIT license. (See LICENSE file.) 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 `c47f48268f15e202a28b556845f231b2038cb426`), 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>.