curve25519: fiat-crypto field arithmetic.
Each operation was translated from fiat-crypto output using fiat-crypto
prettyprint.py. For example fe_mul is synthesized in
https://github.com/mit-plv/fiat-crypto/blob/master/src/Specific/X25519/C32/femul.v,
and shown in the last Coq-compatible form at
https://github.com/mit-plv/fiat-crypto/blob/master/src/Specific/X25519/C32/femulDisplay.log.
Benchmarks on Google Cloud's unidentified Intel Xeon with AVX2:
git checkout $VARIANT && ( cd build && rm -rf * && CC=clang CXX=clang++ cmake -GNinja -DCMAKE_TOOLCHAIN_FILE=../util/32-bit-toolchain.cmake -DCMAKE_BUILD_TYPE=Release .. && ninja && ./tool/bssl speed -filter 25519 )
this branch:
Did 11382 Ed25519 key generation operations in 1053046us (10808.6 ops/sec)
Did 11169 Ed25519 signing operations in 1038080us (10759.3 ops/sec)
Did 2925 Ed25519 verify operations in 1001346us (2921.1 ops/sec)
Did 12000 Curve25519 base-point multiplication operations in 1084851us (11061.4 ops/sec)
Did 3850 Curve25519 arbitrary point multiplication operations in 1085565us (3546.5 ops/sec)
Did 11466 Ed25519 key generation operations in 1049821us (10921.9 ops/sec)
Did 11000 Ed25519 signing operations in 1013317us (10855.4 ops/sec)
Did 3047 Ed25519 verify operations in 1043846us (2919.0 ops/sec)
Did 12000 Curve25519 base-point multiplication operations in 1068924us (11226.2 ops/sec)
Did 3850 Curve25519 arbitrary point multiplication operations in 1090598us (3530.2 ops/sec)
Did 10309 Ed25519 key generation operations in 1003320us (10274.9 ops/sec)
Did 11000 Ed25519 signing operations in 1017862us (10807.0 ops/sec)
Did 3135 Ed25519 verify operations in 1098624us (2853.6 ops/sec)
Did 9000 Curve25519 base-point multiplication operations in 1046608us (8599.2 ops/sec)
Did 3132 Curve25519 arbitrary point multiplication operations in 1038963us (3014.5 ops/sec)
master:
Did 11564 Ed25519 key generation operations in 1068762us (10820.0 ops/sec)
Did 11104 Ed25519 signing operations in 1024278us (10840.8 ops/sec)
Did 3206 Ed25519 verify operations in 1049179us (3055.7 ops/sec)
Did 12000 Curve25519 base-point multiplication operations in 1073619us (11177.1 ops/sec)
Did 3550 Curve25519 arbitrary point multiplication operations in 1000279us (3549.0 ops/sec)
andreser@linux-andreser:~/boringssl$ build/tool/bssl speed -filter 25519
Did 11760 Ed25519 key generation operations in 1072495us (10965.1 ops/sec)
Did 10800 Ed25519 signing operations in 1003486us (10762.5 ops/sec)
Did 3245 Ed25519 verify operations in 1080399us (3003.5 ops/sec)
Did 12000 Curve25519 base-point multiplication operations in 1076021us (11152.2 ops/sec)
Did 3570 Curve25519 arbitrary point multiplication operations in 1005087us (3551.9 ops/sec)
andreser@linux-andreser:~/boringssl$ build/tool/bssl speed -filter 25519
Did 11438 Ed25519 key generation operations in 1041115us (10986.3 ops/sec)
Did 11000 Ed25519 signing operations in 1012589us (10863.2 ops/sec)
Did 3312 Ed25519 verify operations in 1082834us (3058.6 ops/sec)
Did 12000 Curve25519 base-point multiplication operations in 1061318us (11306.7 ops/sec)
Did 3580 Curve25519 arbitrary point multiplication operations in 1004923us (3562.5 ops/sec)
squashed: curve25519: convert field constants to unsigned.
import re, sys, math
def weight(i):
return 2**int(math.ceil(25.5*i))
def convert(t):
limbs = [x for x in t.groups() if x.replace('-','').isdigit()]
v = sum(weight(i)*x for (i,x) in enumerate(map(int, limbs))) % (2**255-19)
limbs = [(v % weight(i+1)) // weight(i) for i in range(10)]
assert v == sum(weight(i)*x for (i,x) in enumerate(limbs))
i = 0
ret = ''
for s in t.groups():
if s.replace('-','').isdigit():
ret += str(limbs[i])
i += 1
else:
ret += s
return ret
fe_re = re.compile(r'(\s*,\s*)'.join(r'(-?\d+)' for i in range(10)))
print (re.sub(fe_re, convert, sys.stdin.read()))
Change-Id: Ibd4f7f5c38e5c4d61c9826afb406baebe2be5168
Reviewed-on: https://boringssl-review.googlesource.com/22385
Reviewed-by: Adam Langley <agl@google.com>
Commit-Queue: Adam Langley <agl@google.com>
CQ-Verified: CQ bot account: commit-bot@chromium.org <commit-bot@chromium.org>
2017-11-03 19:03:13 +00:00
|
|
|
# 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.)
|
2017-12-21 17:28:57 +00:00
|
|
|
|
|
|
|
|
## Curve25519
|
|
|
|
|
|
|
|
|
|
To generate the field arithmetic procedures in `curve25519.c` from a fiat-crypto
|
2018-01-09 22:27:21 +00:00
|
|
|
checkout (as of `7892c66d5e0e5770c79463ce551193ceef870641`), run
|
2017-12-21 17:28:57 +00:00
|
|
|
`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".
|
|
|
|
|
|
2018-01-09 22:27:21 +00:00
|
|
|
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`.
|
|
|
|
|
|
2017-12-21 17:28:57 +00:00
|
|
|
## 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>.
|
