def dump_bin(bin):
    d = []
    pc = 0
    while pc < len(bin):
        op = bin[pc]
        # print('#', pc, op)
        # print('b = func[%d]()' % (op | 0x100))
        type = bin[pc + 1]
        if type == 2 or type == 0:
            # missing bin[pc + 2]
            # print('a = func[%d](%d)' % (op, bin[pc + 3]))
            key = bin[pc + 3]
            pc += 4
        elif type == 1:
            size = bin[pc + 2]
            s = bin[pc + 3: pc + 3 + size]
            # print('a = func[%d](%s)' % (op, repr(s)))
            # print('b = xor(b)')
            key = 0
            for i in s: key ^= i
            pc += 3 + size
        else:
            pc += 3
            assert False
        d.append((op, key))
    return d

def g(x, n):
    return (x >> n) & 1

def s(x, n):
    return (x & 1) << n

def swapbit(x, m, n):
    if m == n: return x
    return s(g(x, m), n) | s(g(x, n), m) | (x & ~(s(1, n) | s(1, m)))

def swapkeep(x, mask):
    swapbits = ~mask & 0xff
    m = swapbits.bit_length() - 1
    assert 0 <= m < 8
    swapbits ^= 1 << m
    n = swapbits.bit_length() - 1
    assert 0 <= n < 8
    swapbits ^= 1 << n
    assert swapbits == 0
    return swapbit(x, m, n)

def ror1(x, n):
    n &= 7
    if isinstance(x, int):
        x &= 0xff
        return (x >> n) | (x << (8 - n)) & 0xff
    else:
        return LShR(x, n) | (x << (8 - n)) & 0xff

entries = [
    0x2efa,
    0x42e9,
    0x3428,
    0x38fd,
    0x2522,
    0x480d,
    0x4cc6,
    0x3df6,
    0x51df
]

bin = open('./bin', 'rb').read()
_seq = dump_bin(bin)
# print(_seq)

import ctypes

lib = ctypes.cdll.LoadLibrary('./lib')
# extern void setup();
lib.setup()

def encrypt(array, seq):
    for op, key in seq:
        for i in range(38):
            v = lib.bf_round(key, entries[op], i)
            type, val0, val1 = v >> 16, (v >> 8) & 0xff, v & 0xff
            if type == 0:
                assert val0 == 0
                # print(i, 'c ^= 0x%x' % val1)
                array[i] ^= val1
            elif type == 1:
                # print(i, 'c = ror1(c, %d) ^ 0x%x' % (val0, val1))
                array[i] = ror1(array[i], val0) ^ val1
            elif type == 2:
                # print(i, 'c = swapkeep(c, 0x%x) ^ 0x%x' % (val0, val1))
                array[i] = swapkeep(array[i], val0) ^ val1
            else:
                assert False, type

from z3 import *
_array = [BitVec('x%d' % i, 8) for i in range(38)]
array = _array[:]
encrypt(array, _seq)

result = [226, 125, 77, 72, 55, 231, 235, 154, 118, 5, 125, 135, 49, 162, 160, 77, 248, 159, 61, 164, 56, 139, 225, 229, 136, 139, 89, 191, 4, 222, 40, 234, 126, 202, 215, 252, 133, 165]
# print(len(result))

s = Solver()
for i in range(38):
    s.add(array[i] == result[i])

assert s.check() == sat
model = s.model()
# print(model)
flag = []
for i in _array:
    flag.append(model[i].as_long())

print(bytes(flag))
# flag{3da8767cfb9424b9bbcc09008e36642d}
