curve25519-hacl64: simplify u64_eq_mask

Avoid signed right shift.

Z3 script showing equivalence:

>>> from z3 import *
>>>
>>> x = BitVec("x", 64)
>>> y = BitVec("y", 64)
>>>
>>> # Before
... x_ = ~(x ^ y)
>>> x_ &= x_ << 32
>>> x_ &= x_ << 16
>>> x_ &= x_ <<  8
>>> x_ &= x_ <<  4
>>> x_ &= x_ <<  2
>>> x_ &= x_ <<  1
>>> x_ >>= 63
>>>
>>> # After
... y_ = x ^ y
>>> y_ = y_ | -y_
>>> y_ = LShR(y_, 63) - 1
>>>
>>> prove(x_ == y_)
proved

Signed-off-by: Samuel Neves <sneves@dei.uc.pt>

1 files changed, 3 insertions, 8 deletions

diff --git a/src/crypto/curve25519-hacl64.h b/src/crypto/curve25519-hacl64.h
index 4fd95cb..5631cde 100644
--- a/src/crypto/curve25519-hacl64.h
+++ b/src/crypto/curve25519-hacl64.h
@@ -10,14 +10,9 @@
 typedef __uint128_t u128;
 static __always_inline u64 u64_eq_mask(u64 x, u64 y)
 {
-	x = ~(x ^ y);
-	x &= x << 32;
-	x &= x << 16;
-	x &= x << 8;
-	x &= x << 4;
-	x &= x << 2;
-	x &= x << 1;
-	return ((s64)x) >> 63;
+	x ^= y;
+	x |= -x;
+	return (x >> 63) - 1;
 }
 
 static __always_inline u64 u64_gte_mask(u64 x, u64 y)