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 /src/crypto/chacha20.h | |
| 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>
Diffstat (limited to 'src/crypto/chacha20.h')
0 files changed, 0 insertions, 0 deletions