From 1131629b19f19d1458db8bc1f2ceb17bf6f49f8a Mon Sep 17 00:00:00 2001 From: "Jason A. Donenfeld" Date: Mon, 27 Aug 2018 22:37:37 -0600 Subject: curve25519-hacl64: use formally verified C for comparisons The previous code had been proved in Z3, but this new code from upstream KreMLin is directly generated from the F*, which is preferable. The assembly generated is identical. --- src/crypto/curve25519-hacl64.h | 25 +++++++++++++++++++------ 1 file changed, 19 insertions(+), 6 deletions(-) (limited to 'src/crypto/curve25519-hacl64.h') diff --git a/src/crypto/curve25519-hacl64.h b/src/crypto/curve25519-hacl64.h index 7d9d734..1b05bc9 100644 --- a/src/crypto/curve25519-hacl64.h +++ b/src/crypto/curve25519-hacl64.h @@ -8,16 +8,29 @@ */ typedef __uint128_t u128; -static __always_inline u64 u64_eq_mask(u64 x, u64 y) + +static __always_inline u64 u64_eq_mask(u64 a, u64 b) { - x ^= y; - x |= -x; - return (x >> 63) - 1; + u64 x = a ^ b; + u64 minus_x = ~x + (u64)1U; + u64 x_or_minus_x = x | minus_x; + u64 xnx = x_or_minus_x >> (u32)63U; + u64 c = xnx - (u64)1U; + return c; } -static __always_inline u64 u64_gte_mask(u64 x, u64 y) +static __always_inline u64 u64_gte_mask(u64 a, u64 b) { - return ((x ^ ((x ^ y) | ((x - y) ^ y))) >> 63) - 1; + u64 x = a; + u64 y = b; + u64 x_xor_y = x ^ y; + u64 x_sub_y = x - y; + u64 x_sub_y_xor_y = x_sub_y ^ y; + u64 q = x_xor_y | x_sub_y_xor_y; + u64 x_xor_q = x ^ q; + u64 x_xor_q_ = x_xor_q >> (u32)63U; + u64 c = x_xor_q_ - (u64)1U; + return c; } static __always_inline void modulo_carry_top(u64 *b) -- cgit v1.2.3-59-g8ed1b