diff options
author | Samuel Neves <sneves@dei.uc.pt> | 2018-08-08 00:23:27 +0100 |
---|---|---|
committer | Jason A. Donenfeld <Jason@zx2c4.com> | 2018-08-07 17:25:07 -0700 |
commit | 2e60bb395c1f589a398ec606d611132ef9ef764b (patch) | |
tree | 193f566a172313edde56946c187b84ee20a1f274 /src/hashtables.c | |
parent | chacha20: use memmove in case buffers overlap (diff) | |
download | wireguard-monolithic-historical-2e60bb395c1f589a398ec606d611132ef9ef764b.tar.xz wireguard-monolithic-historical-2e60bb395c1f589a398ec606d611132ef9ef764b.zip |
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>
Diffstat (limited to 'src/hashtables.c')
0 files changed, 0 insertions, 0 deletions