bedrock2 platform, tests, 64-bit p256_coord_sub
This change adds the scaffolding to integrate code proven in Rocq using
Bedrock and Fiat Cryptography to libcrypto, in particular for optimized
elliptic-curve and finite-field arithmetic. A new implementation of p256
coordinate subtracton is added as an initial demonstration.
Change-Id: I73b3bd8258a33681a2e5b6532e389151e157985b
Reviewed-on: https://boringssl-review.googlesource.com/c/boringssl/+/79208
Auto-Submit: Andres Erbsen <andreser@google.com>
Reviewed-by: David Benjamin <davidben@google.com>
Commit-Queue: David Benjamin <davidben@google.com>
diff --git a/build.json b/build.json
index 641e0d4..152a991 100644
--- a/build.json
+++ b/build.json
@@ -565,7 +565,10 @@
"third_party/fiat/curve25519_64_msvc.h",
"third_party/fiat/p256_32.h",
"third_party/fiat/p256_64.h",
- "third_party/fiat/p256_64_msvc.h"
+ "third_party/fiat/p256_64_msvc.h",
+ "third_party/fiat/p256_bedrock.c.inc",
+ "third_party/fiat/bedrock_unverified_bareminimum.c.inc",
+ "third_party/fiat/bedrock_unverified_platform.c.inc"
],
"err_data": [
"crypto/err/*.errordata"
@@ -881,7 +884,9 @@
"crypto/trust_token/trust_token_test.cc",
"crypto/x509/x509_test.cc",
"crypto/x509/x509_time_test.cc",
- "crypto/xwing/xwing_test.cc"
+ "crypto/xwing/xwing_test.cc",
+ "third_party/fiat/bedrock_platform_test.cc",
+ "third_party/fiat/bedrock_polyfill_platform.c.inc"
],
"data": [
"crypto/blake2/blake2b256_tests.txt",
diff --git a/gen/sources.bzl b/gen/sources.bzl
index 6811bc0..9f976f0 100644
--- a/gen/sources.bzl
+++ b/gen/sources.bzl
@@ -661,6 +661,8 @@
"crypto/spake2plus/internal.h",
"crypto/trust_token/internal.h",
"crypto/x509/internal.h",
+ "third_party/fiat/bedrock_unverified_bareminimum.c.inc",
+ "third_party/fiat/bedrock_unverified_platform.c.inc",
"third_party/fiat/curve25519_32.h",
"third_party/fiat/curve25519_64.h",
"third_party/fiat/curve25519_64_adx.h",
@@ -668,6 +670,7 @@
"third_party/fiat/p256_32.h",
"third_party/fiat/p256_64.h",
"third_party/fiat/p256_64_msvc.h",
+ "third_party/fiat/p256_bedrock.c.inc",
]
crypto_sources_asm = [
@@ -782,6 +785,8 @@
"crypto/x509/x509_test.cc",
"crypto/x509/x509_time_test.cc",
"crypto/xwing/xwing_test.cc",
+ "third_party/fiat/bedrock_platform_test.cc",
+ "third_party/fiat/bedrock_polyfill_platform.c.inc",
]
crypto_test_data = [
diff --git a/gen/sources.cmake b/gen/sources.cmake
index 913bf97..978ada9 100644
--- a/gen/sources.cmake
+++ b/gen/sources.cmake
@@ -679,6 +679,8 @@
crypto/spake2plus/internal.h
crypto/trust_token/internal.h
crypto/x509/internal.h
+ third_party/fiat/bedrock_unverified_bareminimum.c.inc
+ third_party/fiat/bedrock_unverified_platform.c.inc
third_party/fiat/curve25519_32.h
third_party/fiat/curve25519_64.h
third_party/fiat/curve25519_64_adx.h
@@ -686,6 +688,7 @@
third_party/fiat/p256_32.h
third_party/fiat/p256_64.h
third_party/fiat/p256_64_msvc.h
+ third_party/fiat/p256_bedrock.c.inc
)
set(
@@ -806,6 +809,8 @@
crypto/x509/x509_test.cc
crypto/x509/x509_time_test.cc
crypto/xwing/xwing_test.cc
+ third_party/fiat/bedrock_platform_test.cc
+ third_party/fiat/bedrock_polyfill_platform.c.inc
)
set(
diff --git a/gen/sources.gni b/gen/sources.gni
index f2022e6..4a7947c 100644
--- a/gen/sources.gni
+++ b/gen/sources.gni
@@ -661,6 +661,8 @@
"crypto/spake2plus/internal.h",
"crypto/trust_token/internal.h",
"crypto/x509/internal.h",
+ "third_party/fiat/bedrock_unverified_bareminimum.c.inc",
+ "third_party/fiat/bedrock_unverified_platform.c.inc",
"third_party/fiat/curve25519_32.h",
"third_party/fiat/curve25519_64.h",
"third_party/fiat/curve25519_64_adx.h",
@@ -668,6 +670,7 @@
"third_party/fiat/p256_32.h",
"third_party/fiat/p256_64.h",
"third_party/fiat/p256_64_msvc.h",
+ "third_party/fiat/p256_bedrock.c.inc",
]
crypto_sources_asm = [
@@ -782,6 +785,8 @@
"crypto/x509/x509_test.cc",
"crypto/x509/x509_time_test.cc",
"crypto/xwing/xwing_test.cc",
+ "third_party/fiat/bedrock_platform_test.cc",
+ "third_party/fiat/bedrock_polyfill_platform.c.inc",
]
crypto_test_data = [
diff --git a/gen/sources.json b/gen/sources.json
index 9184e23..6284d04 100644
--- a/gen/sources.json
+++ b/gen/sources.json
@@ -643,13 +643,16 @@
"crypto/spake2plus/internal.h",
"crypto/trust_token/internal.h",
"crypto/x509/internal.h",
+ "third_party/fiat/bedrock_unverified_bareminimum.c.inc",
+ "third_party/fiat/bedrock_unverified_platform.c.inc",
"third_party/fiat/curve25519_32.h",
"third_party/fiat/curve25519_64.h",
"third_party/fiat/curve25519_64_adx.h",
"third_party/fiat/curve25519_64_msvc.h",
"third_party/fiat/p256_32.h",
"third_party/fiat/p256_64.h",
- "third_party/fiat/p256_64_msvc.h"
+ "third_party/fiat/p256_64_msvc.h",
+ "third_party/fiat/p256_bedrock.c.inc"
],
"asm": [
"crypto/curve25519/asm/x25519-asm-arm.S",
@@ -762,7 +765,9 @@
"crypto/trust_token/trust_token_test.cc",
"crypto/x509/x509_test.cc",
"crypto/x509/x509_time_test.cc",
- "crypto/xwing/xwing_test.cc"
+ "crypto/xwing/xwing_test.cc",
+ "third_party/fiat/bedrock_platform_test.cc",
+ "third_party/fiat/bedrock_polyfill_platform.c.inc"
],
"data": [
"crypto/blake2/blake2b256_tests.txt",
diff --git a/gen/sources.mk b/gen/sources.mk
index 37ff3bc..944b9dc 100644
--- a/gen/sources.mk
+++ b/gen/sources.mk
@@ -653,13 +653,16 @@
crypto/spake2plus/internal.h \
crypto/trust_token/internal.h \
crypto/x509/internal.h \
+ third_party/fiat/bedrock_unverified_bareminimum.c.inc \
+ third_party/fiat/bedrock_unverified_platform.c.inc \
third_party/fiat/curve25519_32.h \
third_party/fiat/curve25519_64.h \
third_party/fiat/curve25519_64_adx.h \
third_party/fiat/curve25519_64_msvc.h \
third_party/fiat/p256_32.h \
third_party/fiat/p256_64.h \
- third_party/fiat/p256_64_msvc.h
+ third_party/fiat/p256_64_msvc.h \
+ third_party/fiat/p256_bedrock.c.inc
boringssl_crypto_sources_asm := \
crypto/curve25519/asm/x25519-asm-arm.S \
@@ -770,7 +773,9 @@
crypto/trust_token/trust_token_test.cc \
crypto/x509/x509_test.cc \
crypto/x509/x509_time_test.cc \
- crypto/xwing/xwing_test.cc
+ crypto/xwing/xwing_test.cc \
+ third_party/fiat/bedrock_platform_test.cc \
+ third_party/fiat/bedrock_polyfill_platform.c.inc
boringssl_crypto_test_data := \
crypto/blake2/blake2b256_tests.txt \
diff --git a/third_party/fiat/README.md b/third_party/fiat/README.md
index 1035e7f..4595ba6 100644
--- a/third_party/fiat/README.md
+++ b/third_party/fiat/README.md
@@ -1,6 +1,6 @@
# Fiat Cryptography
-The files in this directory are generated using [Fiat
+Most files in this directory are generated using [Fiat
Cryptography](https://github.com/mit-plv/fiat-crypto) from the associated
library of arithmetic-implementation templates. These files are included under
the Apache 2.0 license. (See LICENSE file.)
@@ -21,3 +21,15 @@
translation validator that is included in the Fiat-Cryptography repository.
Correct unwinding and manual assembler-directive changes related to object-file
conventions are validated using unit tests.
+
+# Bedrock
+
+Routines for which assembly-level optimization is not necessary are written in
+[Bedrock2](https://github.com/mit-plv/bedrock2) and tranlated to C. The file
+`bedrock_unverified_platform.c.inc` provides the platform functionality code
+thus translated expects.
+
+The P256 coordinate subtraction function in 64-bit C code generated by Fiat
+Cryptography has been manually replaced with a version written in Bedrock.
+This is an early step towards using Bedrock more widely, both on its own and as
+an alternative pathway from Fiat Cryptography to C.
diff --git a/third_party/fiat/bedrock_platform_test.cc b/third_party/fiat/bedrock_platform_test.cc
new file mode 100644
index 0000000..74c0d21
--- /dev/null
+++ b/third_party/fiat/bedrock_platform_test.cc
@@ -0,0 +1,105 @@
+// Copyright 2025 The BoringSSL Authors
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+// https://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+#include <gtest/gtest.h>
+#include <openssl/rand.h>
+
+#include "bedrock_unverified_platform.c.inc"
+namespace ref {
+#include "bedrock_unverified_bareminimum.c.inc" // currently unused but planned
+#include "bedrock_polyfill_platform.c.inc"
+}
+
+namespace {
+
+#define SECRET_EQ_W(a, b) EXPECT_EQ(br_declassify(a), br_declassify(b))
+
+TEST(BedrockTest, ArithmeticAndBroadcast) {
+ std::vector<br_word_t> test_values = {
+ 0,
+ 1,
+ 1024,
+ 12345,
+ 32000,
+ 0xffffffff / 2 - 1,
+ 0xffffffff / 2,
+ 0xffffffff / 2 + 1,
+ 0xffffffff - 1,
+ 0xffffffff,
+ std::numeric_limits<br_word_t>::max() / 2 - 1,
+ std::numeric_limits<br_word_t>::max() / 2,
+ std::numeric_limits<br_word_t>::max() / 2 + 1,
+ std::numeric_limits<br_word_t>::max() - 1,
+ std::numeric_limits<br_word_t>::max(),
+ };
+
+ for (int i = 0; i < 100; i++) {
+ br_word_t word;
+ RAND_bytes(reinterpret_cast<uint8_t *>(&word), sizeof(word));
+ test_values.push_back(word);
+ }
+
+ auto broadcast = [](bool b) { return b ? 0u-(br_word_t)1 : (br_word_t)0; };
+
+ for (br_word_t a : test_values) {
+ SCOPED_TRACE(a);
+
+ EXPECT_EQ(a, br_value_barrier(a));
+ EXPECT_EQ(a, ref::br_value_barrier(a));
+ EXPECT_EQ(a, br_declassify(a));
+ EXPECT_EQ(a, ref::br_declassify(a));
+ EXPECT_EQ(broadcast(a != 0), br_broadcast_nonzero(a));
+ EXPECT_EQ(broadcast(a != 0), ref::br_broadcast_nonzero(a));
+ EXPECT_EQ(broadcast((br_signed_t)a < 0), br_broadcast_negative(a));
+ EXPECT_EQ(broadcast((br_signed_t)a < 0), ref::br_broadcast_negative(a));
+
+ CONSTTIME_SECRET(&a, sizeof(a));
+
+ br_word_t t = broadcast(true);
+ SECRET_EQ_W(br_broadcast_negative(a) | br_broadcast_negative(~a), t);
+ SECRET_EQ_W(br_broadcast_nonzero(a) | br_broadcast_nonzero(~a), t);
+
+ for (br_word_t b : test_values) {
+ SCOPED_TRACE(b);
+ CONSTTIME_SECRET(&b, sizeof(b));
+
+ SECRET_EQ_W(a, br_cmov(broadcast(true), a, b));
+ SECRET_EQ_W(b, br_cmov(broadcast(false), a, b));
+
+ br_word_t lo = 0, lr = 0;
+ SECRET_EQ_W(br_full_mul(a, b, &lo), ref::br_full_mul(a, b, &lr));
+ SECRET_EQ_W(lo, lr);
+ SECRET_EQ_W(lo, a * b);
+
+ for (br_word_t c : {0, 1}) {
+ SCOPED_TRACE(c);
+ CONSTTIME_SECRET(&c, sizeof(c));
+
+ SECRET_EQ_W(br_declassify(a) ? b : c, br_cmov(a, b, c));
+ SECRET_EQ_W(br_declassify(a) ? c : b, br_cmov(a, c, b));
+
+ SECRET_EQ_W(br_full_add(a, b, c, &lo), ref::br_full_add(a, b, c, &lr));
+ SECRET_EQ_W(lo, lr);
+ SECRET_EQ_W(lo, a + b + c);
+
+ SECRET_EQ_W(br_full_sub(a, b, c, &lo), ref::br_full_sub(a, b, c, &lr));
+ SECRET_EQ_W(lo, lr);
+ SECRET_EQ_W(lo, a - b - c);
+ }
+ }
+ }
+}
+
+#undef SECRET_EQ_W
+} // namespace
diff --git a/third_party/fiat/bedrock_polyfill_platform.c.inc b/third_party/fiat/bedrock_polyfill_platform.c.inc
new file mode 100644
index 0000000..ec6c3a5
--- /dev/null
+++ b/third_party/fiat/bedrock_polyfill_platform.c.inc
@@ -0,0 +1,66 @@
+// Generated from Bedrock code in Fiat Cryptogrpahy. Avoid editing directly.
+
+static inline br_word_t br_full_add(br_word_t x, br_word_t y, br_word_t carry, br_word_t* _sum) {
+ br_word_t carry_out, sum;
+ x = x+carry;
+ carry_out = (br_word_t)(x<carry);
+ sum = x+y;
+ carry_out = carry_out+((br_word_t)(sum<y));
+ *_sum = sum;
+ return carry_out;
+}
+
+static inline br_word_t br_full_sub(br_word_t x, br_word_t y, br_word_t borrow, br_word_t* _diff) {
+ br_word_t out_borrow, diff;
+ out_borrow = (br_word_t)(x<y);
+ diff = x-y;
+ out_borrow = out_borrow+((br_word_t)(diff<borrow));
+ diff = diff-borrow;
+ *_diff = diff;
+ return out_borrow;
+}
+
+static inline br_word_t br_full_mul(br_word_t a, br_word_t b, br_word_t* _low) {
+ br_word_t high, hh, lh, hl, low, second_halfword_w_oflow, n, ll, M;
+ n = ((((0u-(br_word_t)1)>>27)&63)+1)>>1;
+ M = ((br_word_t)1<<(n&(sizeof(br_word_t)*8-1)))-1;
+ ll = (a&M)*(b&M);
+ lh = (a&M)*(b>>(n&(sizeof(br_word_t)*8-1)));
+ hl = (a>>(n&(sizeof(br_word_t)*8-1)))*(b&M);
+ hh = (a>>(n&(sizeof(br_word_t)*8-1)))*(b>>(n&(sizeof(br_word_t)*8-1)));
+ second_halfword_w_oflow = ((ll>>(n&(sizeof(br_word_t)*8-1)))+(lh&M))+(hl&M);
+ high = ((hh+(lh>>(n&(sizeof(br_word_t)*8-1))))+(hl>>(n&(sizeof(br_word_t)*8-1))))+(second_halfword_w_oflow>>(n&(sizeof(br_word_t)*8-1)));
+ low = (second_halfword_w_oflow<<(n&(sizeof(br_word_t)*8-1)))+(ll&M);
+ *_low = low;
+ return high;
+}
+
+static inline br_word_t br_value_barrier(br_word_t a) {
+ /*skip*/
+ return a;
+}
+
+static inline br_word_t br_declassify(br_word_t a) {
+ /*skip*/
+ return a;
+}
+
+static inline br_word_t br_broadcast_negative(br_word_t x) {
+ br_word_t y;
+ y = (br_word_t)((br_signed_t)x>>((((0u-(br_word_t)1)>>27)&63)&(sizeof(br_word_t)*8-1)));
+ y = br_value_barrier(y);
+ return y;
+}
+
+static inline br_word_t br_broadcast_nonzero(br_word_t x) {
+ br_word_t y;
+ y = br_broadcast_negative(x|(0u-x));
+ return y;
+}
+
+static inline br_word_t br_cmov(br_word_t c, br_word_t vnz, br_word_t vz) {
+ br_word_t r, m;
+ m = br_broadcast_nonzero(c);
+ r = (m&vnz)|((~m)&vz);
+ return r;
+}
diff --git a/third_party/fiat/bedrock_unverified_bareminimum.c.inc b/third_party/fiat/bedrock_unverified_bareminimum.c.inc
new file mode 100644
index 0000000..a03388b
--- /dev/null
+++ b/third_party/fiat/bedrock_unverified_bareminimum.c.inc
@@ -0,0 +1,47 @@
+#ifndef BEDROCK_UNVERIFIED_BAREMINIMUM_INC_H_
+#define BEDROCK_UNVERIFIED_BAREMINIMUM_INC_H_
+
+static_assert(sizeof(br_word_t) == sizeof(br_signed_t), "");
+static_assert(UINTPTR_MAX <= BR_WORD_MAX, "");
+
+// "An object shall have its stored value accessed only ... a character type."
+
+static inline br_word_t _br_load1(br_word_t a) {
+ return *((uint8_t *)a);
+}
+
+static inline br_word_t _br_load2(br_word_t a) {
+ uint16_t r = 0;
+ memcpy(&r, (void *)a, sizeof(r));
+ return r;
+}
+
+static inline br_word_t _br_load4(br_word_t a) {
+ uint32_t r = 0;
+ memcpy(&r, (void *)a, sizeof(r));
+ return r;
+}
+
+static inline br_word_t _br_load(br_word_t a) {
+ br_word_t r = 0;
+ memcpy(&r, (void *)a, sizeof(r));
+ return r;
+}
+
+static inline void _br_store1(br_word_t a, uint8_t v) {
+ *((uint8_t *)a) = v;
+}
+
+static inline void _br_store2(br_word_t a, uint16_t v) {
+ memcpy((void *)a, &v, sizeof(v));
+}
+
+static inline void _br_store4(br_word_t a, uint32_t v) {
+ memcpy((void *)a, &v, sizeof(v));
+}
+
+static inline void _br_store(br_word_t a, br_word_t v) {
+ memcpy((void *)a, &v, sizeof(v));
+}
+
+#endif // BEDROCK_UNVERIFIED_BAREMINIMUM_INC_H_
diff --git a/third_party/fiat/bedrock_unverified_platform.c.inc b/third_party/fiat/bedrock_unverified_platform.c.inc
new file mode 100644
index 0000000..fbfe90f
--- /dev/null
+++ b/third_party/fiat/bedrock_unverified_platform.c.inc
@@ -0,0 +1,121 @@
+#ifndef BEDROCK_UNVERIFIED_PLATFORM_INC_H_
+#define BEDROCK_UNVERIFIED_PLATFORM_INC_H_
+
+// This file is a manually maintained and audited replacement for
+// bedrock_polyfill_platform.c.inc with tests in bedrock_platform_test.cc
+
+#include "../../crypto/internal.h"
+
+#if defined(OPENSSL_64_BIT)
+#define BR_WORD_MAX UINT64_MAX
+typedef uint64_t br_word_t;
+typedef int64_t br_signed_t;
+#elif defined(OPENSSL_32_BIT)
+#define BR_WORD_MAX UINT32_MAX
+typedef uint32_t br_word_t;
+typedef int32_t br_signed_t;
+#else
+#error "Must define either OPENSSL_32_BIT or OPENSSL_64_BIT"
+#endif
+
+static_assert(sizeof(br_word_t) == sizeof(crypto_word_t));
+
+// Scalar memory operations
+
+#include "../../third_party/fiat/bedrock_unverified_bareminimum.c.inc"
+
+// Bulk memory operations
+
+static inline void br_memcpy(br_word_t d, br_word_t s, br_word_t n) {
+ OPENSSL_memcpy((void *)d, (const void *)s, n);
+}
+
+static inline void br_memset(br_word_t d, br_word_t v, br_word_t n) {
+ OPENSSL_memset((void *)d, v, n);
+}
+
+// CPU Arithmetic
+
+static inline br_word_t br_full_add(br_word_t x, br_word_t y, br_word_t carry,
+ br_word_t *_sum) {
+ br_word_t carry_out = 0;
+ static_assert(sizeof(br_word_t) == sizeof(crypto_word_t));
+ *_sum = CRYPTO_addc_w(x, y, carry, &carry_out);
+ return carry_out;
+}
+
+static inline br_word_t br_full_sub(br_word_t x, br_word_t y, br_word_t borrow,
+ br_word_t *_diff) {
+ br_word_t borrow_out = 0;
+ static_assert(sizeof(br_word_t) == sizeof(crypto_word_t));
+ *_diff = CRYPTO_subc_w(x, y, borrow, &borrow_out);
+ return borrow_out;
+}
+
+static inline br_word_t br_full_mul(br_word_t a, br_word_t b, br_word_t *_low) {
+#if BR_WORD_MAX == UINT32_MAX
+ uint64_t r = (uint64_t)a * b;
+ *_low = r;
+ return r >> 32;
+#elif defined(BORINGSSL_HAS_UINT128)
+ uint128_t r = (uint128_t)a * b;
+ *_low = r;
+ return r >> 64;
+#elif defined(_M_X64)
+ uint64_t hi;
+ *_low = _umul128(a, b, &hi);
+ return hi;
+#elif defined(_M_ARM64)
+ *_low = a * b;
+ return __umulh(a, b);
+#else
+#error "need 64 x 64 -> 128 multiplication"
+#endif
+}
+
+// Constant-time computations
+
+static inline br_word_t br_value_barrier(br_word_t a) {
+ static_assert(sizeof(br_word_t) == sizeof(crypto_word_t));
+ return value_barrier_w(a);
+}
+
+static inline br_word_t br_declassify(br_word_t a) {
+ static_assert(sizeof(br_word_t) == sizeof(crypto_word_t));
+ return constant_time_declassify_w(a);
+}
+
+static inline br_word_t br_broadcast_negative(br_word_t x) {
+ return br_value_barrier((br_signed_t)x >> (sizeof(br_word_t) * 8 - 1));
+}
+
+static inline br_word_t br_broadcast_nonzero(br_word_t x) {
+ return br_broadcast_negative(x | (0u - x));
+}
+
+static inline br_word_t br_cmov(br_word_t c, br_word_t vnz, br_word_t vz) {
+#if !defined(OPENSSL_NO_ASM) && (defined(__GNUC__) || defined(__clang__)) && \
+ defined(__x86_64__)
+ __asm__(
+ "testq %[c], %[c]\n"
+ "cmovzq %[vz], %[vnz]"
+ : [vnz] "+r"(vnz)
+ : [vz] "r"(vz), [c] "r"(c)
+ : "cc");
+ return vnz;
+#elif !defined(OPENSSL_NO_ASM) && (defined(__GNUC__) || defined(__clang__)) && \
+ defined(__i386__)
+ __asm__(
+ "testl %[c], %[c]\n" // test%z[c] gives "invalid operand" on clang 16.0.6
+ "cmovzl %[vz], %[vnz]"
+ : [vnz] "+r"(vnz)
+ : [vz] "r"(vz), [c] "r"(c)
+ : "cc");
+ return vnz;
+#else
+ br_word_t m = br_broadcast_nonzero(c);
+ return (m & vnz) | (~m & vz);
+#endif
+}
+
+#endif // BEDROCK_UNVERIFIED_PLATFORM_INC_H_
diff --git a/third_party/fiat/p256_64.h b/third_party/fiat/p256_64.h
index 48a1560..21f7a98 100644
--- a/third_party/fiat/p256_64.h
+++ b/third_party/fiat/p256_64.h
@@ -1,4 +1,6 @@
#include <openssl/base.h>
+#include "bedrock_unverified_platform.c.inc"
+#include "p256_bedrock.c.inc"
#include "../../crypto/internal.h"
#if !defined(OPENSSL_NO_ASM) && defined(__GNUC__) && defined(__x86_64__)
@@ -857,36 +859,7 @@
*
*/
static FIAT_P256_FIAT_INLINE void fiat_p256_sub(fiat_p256_montgomery_domain_field_element out1, const fiat_p256_montgomery_domain_field_element arg1, const fiat_p256_montgomery_domain_field_element arg2) {
- uint64_t x1;
- fiat_p256_uint1 x2;
- uint64_t x3;
- fiat_p256_uint1 x4;
- uint64_t x5;
- fiat_p256_uint1 x6;
- uint64_t x7;
- fiat_p256_uint1 x8;
- uint64_t x9;
- uint64_t x10;
- fiat_p256_uint1 x11;
- uint64_t x12;
- fiat_p256_uint1 x13;
- uint64_t x14;
- fiat_p256_uint1 x15;
- uint64_t x16;
- fiat_p256_uint1 x17;
- fiat_p256_subborrowx_u64(&x1, &x2, 0x0, (arg1[0]), (arg2[0]));
- fiat_p256_subborrowx_u64(&x3, &x4, x2, (arg1[1]), (arg2[1]));
- fiat_p256_subborrowx_u64(&x5, &x6, x4, (arg1[2]), (arg2[2]));
- fiat_p256_subborrowx_u64(&x7, &x8, x6, (arg1[3]), (arg2[3]));
- fiat_p256_cmovznz_u64(&x9, x8, 0x0, UINT64_C(0xffffffffffffffff));
- fiat_p256_addcarryx_u64(&x10, &x11, 0x0, x1, x9);
- fiat_p256_addcarryx_u64(&x12, &x13, x11, x3, (x9 & UINT32_C(0xffffffff)));
- fiat_p256_addcarryx_u64(&x14, &x15, x13, x5, 0x0);
- fiat_p256_addcarryx_u64(&x16, &x17, x15, x7, (x9 & UINT64_C(0xffffffff00000001)));
- out1[0] = x10;
- out1[1] = x12;
- out1[2] = x14;
- out1[3] = x16;
+ p256_coord_sub((br_word_t)out1, (br_word_t)arg1, (br_word_t)arg2);
}
/*
diff --git a/third_party/fiat/p256_64_msvc.h b/third_party/fiat/p256_64_msvc.h
index 8b65a37..3e8a129 100644
--- a/third_party/fiat/p256_64_msvc.h
+++ b/third_party/fiat/p256_64_msvc.h
@@ -17,6 +17,8 @@
/* twos_complement_eval z = let x1 := z[0] + (z[1] << 64) + (z[2] << 128) + (z[3] << 192) in */
/* if x1 & (2^256-1) < 2^255 then x1 & (2^256-1) else (x1 & (2^256-1)) - 2^256 */
+#include "bedrock_unverified_platform.c.inc"
+#include "p256_bedrock.c.inc"
#include <stdint.h>
#include <intrin.h>
#if defined(_M_X64)
@@ -824,36 +826,8 @@
*
*/
static FIAT_P256_FIAT_INLINE void fiat_p256_sub(fiat_p256_montgomery_domain_field_element out1, const fiat_p256_montgomery_domain_field_element arg1, const fiat_p256_montgomery_domain_field_element arg2) {
- uint64_t x1;
- fiat_p256_uint1 x2;
- uint64_t x3;
- fiat_p256_uint1 x4;
- uint64_t x5;
- fiat_p256_uint1 x6;
- uint64_t x7;
- fiat_p256_uint1 x8;
- uint64_t x9;
- uint64_t x10;
- fiat_p256_uint1 x11;
- uint64_t x12;
- fiat_p256_uint1 x13;
- uint64_t x14;
- fiat_p256_uint1 x15;
- uint64_t x16;
- fiat_p256_uint1 x17;
- fiat_p256_subborrowx_u64(&x1, &x2, 0x0, (arg1[0]), (arg2[0]));
- fiat_p256_subborrowx_u64(&x3, &x4, x2, (arg1[1]), (arg2[1]));
- fiat_p256_subborrowx_u64(&x5, &x6, x4, (arg1[2]), (arg2[2]));
- fiat_p256_subborrowx_u64(&x7, &x8, x6, (arg1[3]), (arg2[3]));
- fiat_p256_cmovznz_u64(&x9, x8, 0x0, UINT64_C(0xffffffffffffffff));
- fiat_p256_addcarryx_u64(&x10, &x11, 0x0, x1, x9);
- fiat_p256_addcarryx_u64(&x12, &x13, x11, x3, (x9 & UINT32_C(0xffffffff)));
- fiat_p256_addcarryx_u64(&x14, &x15, x13, x5, 0x0);
- fiat_p256_addcarryx_u64(&x16, &x17, x15, x7, (x9 & UINT64_C(0xffffffff00000001)));
- out1[0] = x10;
- out1[1] = x12;
- out1[2] = x14;
- out1[3] = x16;
+ // NOTE: edited by hand, see third_party/fiat/README.md
+ p256_coord_sub((br_word_t)&out1, (br_word_t)&arg1, (br_word_t)&arg2);
}
/*
diff --git a/third_party/fiat/p256_bedrock.c.inc b/third_party/fiat/p256_bedrock.c.inc
new file mode 100644
index 0000000..fb8c3de
--- /dev/null
+++ b/third_party/fiat/p256_bedrock.c.inc
@@ -0,0 +1,21 @@
+// Generated from Bedrock code in Fiat Cryptography. Avoid editing directly.
+
+static_assert(BR_WORD_MAX == UINT64_MAX, "");
+
+static inline void p256_coord_sub(br_word_t out, br_word_t x, br_word_t y) {
+ br_word_t borrow, t0, t1, t2, t3, mask, carry, r0, r1, r2, r3;
+ borrow = br_full_sub(_br_load(x), _br_load(y), (br_word_t)0, &t0);
+ borrow = br_full_sub(_br_load(x+8), _br_load(y+8), borrow, &t1);
+ borrow = br_full_sub(_br_load((x+8)+8), _br_load((y+8)+8), borrow, &t2);
+ borrow = br_full_sub(_br_load(((x+8)+8)+8), _br_load(((y+8)+8)+8), borrow, &t3);
+ mask = br_value_barrier(0u-borrow);
+ carry = br_full_add(t0, mask, (br_word_t)0, &r0);
+ carry = br_full_add(t1, mask&0xffffffff, carry, &r1);
+ carry = br_full_add(t2, (br_word_t)0, carry, &r2);
+ carry = br_full_add(t3, mask&0xffffffff00000001, carry, &r3);
+ _br_store(out, r0);
+ _br_store(out+8, r1);
+ _br_store((out+8)+8, r2);
+ _br_store(((out+8)+8)+8, r3);
+ return;
+}
