ltPtHCKN - Aleph Paste

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
#!/usr/bin/env python2

from z3 import *

def ULT_(a, b):
    return LShR(a ^ ((a ^ b) | ((a - b) ^ b)), 63)

h = [BitVec("h%u" % i, 32) for i in range(5)]
original_h = h[:]

reference = ZeroExt(192 - 32, h[4]) * 2**(26 * 4) + \
            ZeroExt(192 - 32, h[3]) * 2**(26 * 3) + \
            ZeroExt(192 - 32, h[2]) * 2**(26 * 2) + \
            ZeroExt(192 - 32, h[1]) * 2**(26 * 1) + \
            ZeroExt(192 - 32, h[0]) * 2**(26 * 0)

h[1] += LShR(h[0], 26)
h[0] &= 0x3ffffff
h[2] += LShR(h[1], 26)
h[1] &= 0x3ffffff
h[3] += LShR(h[2], 26)
h[2] &= 0x3ffffff
h[4] += LShR(h[3], 26)
h[3] &= 0x3ffffff

hs0 = (ZeroExt(32, h[2]) << 52) | \
      (ZeroExt(32, h[1]) << 26) | \
      (ZeroExt(32, h[0]) >>  0)
hs1 = (ZeroExt(32, h[4]) << 40) | \
      (ZeroExt(32, h[3]) << 14) | \
      (ZeroExt(32, h[2]) >> 12)
hs2 = (ZeroExt(32, h[4]) >> 24)

solve(
    UGE(Concat(hs2, hs1, hs0), 2**130 + 2**129),
    ULT(original_h[4], 2**26 + 2**25 - 2**4),
    ULT(original_h[0], 2**30),
    ULT(original_h[1], 2**30),
    ULT(original_h[2], 2**30),
    ULT(original_h[3], 2**30)
)

cy = (hs2 >> 2) + (hs2 & ~3)
hs2 &= 3
hs0 += cy
cy = ULT_(hs0, cy)
hs1 += cy
cy = ULT_(hs1, cy)
hs2 += cy

limit = 2**32 - 2**6 - 1

solve(
    URem(reference, 2**130 - 5) != URem(Concat(hs2, hs1, hs0), 2**130 - 5),
    ULT(original_h[4], limit),
    ULT(original_h[0], limit),
    ULT(original_h[1], limit),
    ULT(original_h[2], limit),
    ULT(original_h[3], limit)
)
solve(
    UGE(hs2, 2**3),
    ULT(original_h[4], limit),
    ULT(original_h[0], limit),
    ULT(original_h[1], limit),
    ULT(original_h[2], limit),
    ULT(original_h[3], limit)
)
solve(
    UGE(Concat(hs2, hs1, hs0), 2**130 + 2**129),
    ULT(original_h[4], limit),
    ULT(original_h[0], limit),
    ULT(original_h[1], limit),
    ULT(original_h[2], limit),
    ULT(original_h[3], limit)
)