diff options
| author | Samuel Neves <sneves@dei.uc.pt> | 2018-08-08 00:44:00 +0100 |
|---|---|---|
| committer | Jason A. Donenfeld <Jason@zx2c4.com> | 2018-08-07 18:13:22 -0700 |
| commit | 6eb23d0bfeb82b9fbebb43fc66a00cdde15c67c2 (patch) | |
| tree | 36df4e9bd9f3200d4170ee6d430f6db8c6726b8b | |
| parent | 913b4e55505b4ca638c025163ebf3a7ce01f8b9e (diff) | |
curve25519-hacl64: correct u64_gte_mask
Remove signed right shifts. Previously u64_gte_mask was only
correct for x < 2^63.
Z3 script proving correctness:
>>> from z3 import *
>>>
>>> x = BitVec("x", 64)
>>> y = BitVec("y", 64)
>>>
>>> t = LShR(x^((x^y)|((x-y)^y)), 63) - 1
>>>
>>> prove(If(UGE(x, y), BitVecVal(-1, 64), BitVecVal(0, 64)) == t)
proved
Signed-off-by: Samuel Neves <sneves@dei.uc.pt>
Signed-off-by: Jason A. Donenfeld <Jason@zx2c4.com>
| -rw-r--r-- | src/crypto/curve25519-hacl64.h | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/src/crypto/curve25519-hacl64.h b/src/crypto/curve25519-hacl64.h index 5631cde..d2637ac 100644 --- a/src/crypto/curve25519-hacl64.h +++ b/src/crypto/curve25519-hacl64.h @@ -17,9 +17,7 @@ static __always_inline u64 u64_eq_mask(u64 x, u64 y) static __always_inline u64 u64_gte_mask(u64 x, u64 y) { - u64 low63 = ~((u64)((s64)((s64)(x & 0x7fffffffffffffffLLU) - (s64)(y & 0x7fffffffffffffffLLU)) >> 63)); - u64 high_bit = ~((u64)((s64)((s64)(x & 0x8000000000000000LLU) - (s64)(y & 0x8000000000000000LLU)) >> 63)); - return low63 & high_bit; + return ((x ^ ((x ^ y) | ((x - y) ^ y))) >> 63) - 1; } static __always_inline void modulo_carry_top(u64 *b) |