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 | 0a483a9b431d87eca1b275463c632f8d5551978a (patch) | |
| tree | 26a29a67295b794c7de9bb5f6462af8286ac7606 /src/crypto/curve25519-hacl64.h | |
| parent | curve25519-hacl64: simplify u64_eq_mask (diff) | |
| download | wireguard-monolithic-historical-0a483a9b431d87eca1b275463c632f8d5551978a.tar.xz wireguard-monolithic-historical-0a483a9b431d87eca1b275463c632f8d5551978a.zip | |
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>
Diffstat (limited to '')
| -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) |