History

David Benjamin 0c1eafc6fe Add additional constants to make_curve25519_tables.py. These are also constants that depend on the field representation. Change-Id: I22333c099352ad64eb27fe15ffdc38c6ae7c07ff Reviewed-on: https://boringssl-review.googlesource.com/24746 Commit-Queue: David Benjamin <davidben@google.com> CQ-Verified: CQ bot account: commit-bot@chromium.org <commit-bot@chromium.org> Reviewed-by: Adam Langley <agl@google.com>		2018-01-23 21:35:03 +00:00
..
BUILD.gn	Add files in third_party/fiat for Chromium to pick up.	2018-01-10 22:02:03 +00:00
CMakeLists.txt
curve25519_tables.h	Add additional constants to make_curve25519_tables.py.	2018-01-23 21:35:03 +00:00
curve25519.c	Add additional constants to make_curve25519_tables.py.	2018-01-23 21:35:03 +00:00
internal.h	Remove some outdated preconditions and postconditions.	2018-01-03 23:03:32 +00:00
LICENSE
make_curve25519_tables.py	Add additional constants to make_curve25519_tables.py.	2018-01-23 21:35:03 +00:00
METADATA	change URL type in third_party METADATA files to GIT	2017-11-07 21:38:33 +00:00
p256.c	Align various point_get_affine_coordinates implementations.	2018-01-08 20:03:42 +00:00
README.chromium	Add files in third_party/fiat for Chromium to pick up.	2018-01-10 22:02:03 +00:00
README.md	Use fiat-crypto's freeze function for fe_tobytes.	2018-01-05 23:38:26 +00:00

README.md

Fiat

Some of the code in this directory is generated by Fiat 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.