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)=}')