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>

LICENSE

@@ -7,7 +7,8 @@ https://cla.developers.google.com/clas
 
 Some files from Intel are under yet another license, which is also included
 underneath. Files in third_party/ have their own licenses, as described
-therein.
+therein. The MIT license, for third_party/fiat, which, unlike other third_party
+directories, is compiled into non-test libraries, is included below.
 
 The OpenSSL toolkit stays under a dual license, i.e. both the conditions of the
 OpenSSL License and the original SSLeay license apply to the toolkit. See below
@@ -191,3 +192,27 @@ Some files from Intel carry the following license:
 # LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
 # NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
 # SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+
+
+The code in third_party/fiat carries the MIT license:
+
+Copyright (c) 2015-2016 the fiat-crypto authors (see
+https://github.com/mit-plv/fiat-crypto/blob/master/AUTHORS).
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.

third_party/fiat/LICENSE

@@ -0,0 +1,22 @@
+The MIT License (MIT)
+
+Copyright (c) 2015-2016 the fiat-crypto authors (see
+https://github.com/mit-plv/fiat-crypto/blob/master/AUTHORS).
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.

third_party/fiat/METADATA

@@ -0,0 +1,14 @@
+name: "fiat"
+description:
+    "Fiat-Crypto: Synthesizing Correct-by-Construction Code for Cryptographic Primitives".
+
+third_party {
+  url {
+    type: HOMEPAGE
+    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"
+}

third_party/fiat/README.md

@@ -0,0 +1,5 @@
+# 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.)

third_party/fiat/internal.h

@@ -1,16 +1,24 @@
-/* Copyright (c) 2015, Google Inc.
- *
- * Permission to use, copy, modify, and/or distribute this software for any
- * purpose with or without fee is hereby granted, provided that the above
- * copyright notice and this permission notice appear in all copies.
- *
- * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
- * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
- * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY
- * SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
- * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN ACTION
- * OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR IN
- * CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. */
+// The MIT License (MIT)
+//
+// Copyright (c) 2015-2016 the fiat-crypto authors (see the AUTHORS file).
+//
+// Permission is hereby granted, free of charge, to any person obtaining a copy
+// of this software and associated documentation files (the "Software"), to deal
+// in the Software without restriction, including without limitation the rights
+// to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+// copies of the Software, and to permit persons to whom the Software is
+// furnished to do so, subject to the following conditions:
+//
+// The above copyright notice and this permission notice shall be included in all
+// copies or substantial portions of the Software.
+//
+// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+// IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+// FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+// AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+// LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+// OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+// SOFTWARE.
 
 #ifndef OPENSSL_HEADER_CURVE25519_INTERNAL_H
 #define OPENSSL_HEADER_CURVE25519_INTERNAL_H
@@ -40,13 +48,13 @@ void x25519_NEON(uint8_t out[32], const uint8_t scalar[32],
 // fe means field element. Here the field is \Z/(2^255-19). An element t,
 // entries t[0]...t[9], represents the integer t[0]+2^26 t[1]+2^51 t[2]+2^77
 // t[3]+2^102 t[4]+...+2^230 t[9].
-// fe limbs are bounded by 1.1*2^25,1.1*2^24,1.1*2^25,1.1*2^24,etc.
+// fe limbs are bounded by 1.125*2^26,1.125*2^25,1.125*2^26,1.125*2^25,etc.
 // Multiplication and carrying produce fe from fe_loose.
-typedef struct fe { int32_t v[10]; } fe;
+typedef struct fe { uint32_t v[10]; } fe;
 
-// fe_loose limbs are bounded by 1.1*2^26,1.1*2^25,1.1*2^26,1.1*2^25,etc.
+// fe_loose limbs are bounded by 3.375*2^26,3.375*2^25,3.375*2^26,3.375*2^25,etc.
 // Addition and subtraction produce fe_loose from (fe, fe).
-typedef struct fe_loose { int32_t v[10]; } fe_loose;
+typedef struct fe_loose { uint32_t v[10]; } fe_loose;
 
 /* ge means group element.