40 lines
713 B
Python
40 lines
713 B
Python
import random
|
|
import z3
|
|
|
|
_ROL_ = lambda x, i : ((x << i) | (x >> (N-i))) & (2**N - 1)
|
|
|
|
|
|
N = 128
|
|
|
|
def parity(x):
|
|
res = 0
|
|
while x:
|
|
res ^= x & 1
|
|
x >>= 1
|
|
return res
|
|
|
|
|
|
while True:
|
|
x = random.randint(0, 2**128)
|
|
if parity(x) == 0:
|
|
break
|
|
|
|
# Compute y and c, such that y ^ _ROL_(y,c) == x
|
|
# Hint: to implement _ROL_, z3 already has the function z3.RotateLeft
|
|
def compute_yc(x):
|
|
s = z3.Solver()
|
|
y = z3.BitVec("y", N)
|
|
c = z3.BitVec("c", N)
|
|
s.add((y ^ z3.RotateLeft(y,c)) == x)
|
|
s.check()
|
|
m = s.model()
|
|
|
|
return m[y].as_long(), m[c].as_long()
|
|
|
|
|
|
y, c = compute_yc(x)
|
|
|
|
print(f'{y=}, {c=}')
|
|
print(f'{x=}, {y ^ _ROL_(y, c)=}')
|
|
print(f'{x==y ^ _ROL_(y, c)=}')
|