boringssl/third_party/fiat
David Benjamin cfd50c63a1 Route the tuned add/dbl implementations out of EC_METHOD.
Some consumer stumbled upon EC_POINT_{add,dbl} being faster with a
"custom" P-224 curve than the built-in one and made "custom" clones to
work around this. Before the EC_FELEM refactor, EC_GFp_nistp224_method
used BN_mod_mul for all reductions in fallback point arithmetic (we
primarily support the multiplication functions and keep the low-level
point arithmetic for legacy reasons) which took quite a performance hit.

EC_FELEM fixed this, but standalone felem_{mul,sqr} calls out of
nistp224 perform a lot of reductions, rather than batching them up as
that implementation is intended. So it is still slightly faster to use a
"custom" curve.

Custom curves are the last thing we want to encourage, so just route the
tuned implementations out of EC_METHOD to close this gap. Now the
built-in implementation is always solidly faster than (or identical to)
the custom clone.  This also reduces the number of places where we mix
up tuned vs. generic implementation, which gets us closer to making
EC_POINT's representation EC_METHOD-specific.

Change-Id: I843e1101a6208eaabb56d29d342e886e523c78b4
Reviewed-on: https://boringssl-review.googlesource.com/c/32848
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-11-06 00:17:19 +00:00
..
BUILD.gn Add files in third_party/fiat for Chromium to pick up. 2018-01-10 22:02:03 +00:00
curve25519_tables.h Use 51-bit limbs from fiat-crypto in 64-bit. 2018-01-23 22:25:07 +00:00
curve25519.c Document that ED25519_sign only fails on allocation failure 2018-08-29 18:35:12 +00:00
internal.h Remove x86_64 x25519 assembly. 2018-02-01 21:44:58 +00:00
LICENSE
make_curve25519_tables.py Use 51-bit limbs from fiat-crypto in 64-bit. 2018-01-23 22:25:07 +00:00
METADATA third_party: re-format METATADA files 2018-02-27 19:57:12 +00:00
p256.c Route the tuned add/dbl implementations out of EC_METHOD. 2018-11-06 00:17:19 +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 51-bit limbs from fiat-crypto in 64-bit. 2018-01-23 22:25:07 +00:00

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 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.