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/timers.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 '')
0 files changed, 0 insertions, 0 deletions