kris/boringssl
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity
4702db6306
boringssl/third_party/fiat/METADATA

14 lines
409 B
Plaintext
Raw Normal View History

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
name: "fiat"
third_party: re-format METATADA files Change-Id: Ic2e9f54f5ced053c1463d5c09a74db5b2a3ea098 Reviewed-on: https://boringssl-review.googlesource.com/26224 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>
2018-02-27 19:28:47 +00:00
description: "Fiat-Crypto: Synthesizing Correct-by-Construction Code for Cryptographic Primitives."
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
third_party {
url {
change URL type in third_party METADATA files to GIT Change-Id: Ibaf1b4d64a651c39b073f3c4a7aa861d9c728f8b Reviewed-on: https://boringssl-review.googlesource.com/22704 Reviewed-by: David Benjamin <davidben@google.com>
2017-11-07 20:30:23 +00:00
type: GIT
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
value: "https://github.com/mit-plv/fiat-crypto"
}
version: "6c4d4afb26de639718fcac39094353ca7feec365"
last_upgrade_date { year: 2017 month: 11 day: 3 }
local_modifications: "Fiat-generated code has been integrated into existing BoringSSL code"
}
Reference in New Issue Copy Permalink