from z3 import Solver, BitVec, sat

def rng(x, size):
    return (x*A+B) & ((2**size)-1)

def gen_random(seed, bits, mask):
    state = seed
    while True:
        state = rng(state, bits)
        yield state & mask

A = BitVec("A", 56)
B = BitVec("B", 56)
SEED = BitVec("seed", 56)
BITS = 56 
MASK = 0xFF

state = SEED 

with open("./msg.txt", "r") as f:
    nums = [int(n) for n in f.readlines()[1:]]
    print(nums)

flag_bytes = [BitVec(f'flag_{i}', 56) for i in range(142)]

solver = Solver()

for i, n in enumerate(nums):
    state = rng(state, BITS)
    cur_num = state & MASK
    solver.add(n == cur_num ^ flag_bytes[i])
    solver.add(flag_bytes[i] >= 32, flag_bytes[i] <= 126)

if solver.check() == sat:
    model = solver.model()
    flag = ''.join([chr(model[flag_bytes[i]].as_long()) for i in range(142)])
    print(model)
    print(flag)
else:
    print("Not solveable")