from z3 import *
table = [0x70,0x72,0x76,0x6f,0x39,0x43,0x48,0x53,0x4a,0x4f,0x63,0x50,0x49,0x62,0x36,0x78,0x52,0x56,0x55,0x58,0x51,0x7a,0x30,0x71,0x42,0x47,0x44,0x45,0x37,0x32,0x4c,0x4e,0x5a,0x64,0x75,0x61,0x65,0x66,0x59,0x54,0x35,0x4b,0x5f,0x38,0x2d,0x34,0x46,0x41,0x68,0x6c,0x69,0x6d,0x6a,0x6b,0x6e,0x67,0x74,0x31,0x79,0x4d,0x57,0x73,0x33,0x77,0x21]
A = Array('A', IntSort(), IntSort())
i = 0
for elem in table:
A = Store(A, i, elem)
i = i + 1
permute = lambda k:Select(A, BV2Int(k))
flag_len = 31
x = [BitVec('u%d'%i,8) for i in range(x_len)]
s = Solver()
i = 0
v = 0
xxx = []
while True:
k = x_len - i
if (k == 0):
break
if k == 1:
pos = (x[i] >> 2) & 0x3f
m0 = permute(pos)
pos = (16 * x[i]) & 0x3f
m1 = permute(pos)
pos = BitVecVal(0x40, 8)
m2 = permute(pos)
m3 = permute(pos)
elif k == 2:
pos = (x[i] >> 2) & 0x3f
m0 = permute(pos)
pos = ((x[i+1] >> 4) | (16 * x[i])) & 0x3f
m1 = permute(pos)
pos = (4 * x[i+1]) & 0x3f
m2 = permute(pos)
pos = BitVecVal(0x40, 8)
m3 = permute(pos)
else:
pos = (x[i] >> 2) & 0x3f
m0 = permute(pos)
pos = ((x[i+1] >> 4) & 0x3f | (16 * x[i])) & 0x3f
m1 = permute(pos)
pos = ((x[i+2] >> 6) | (4 * x[i+1])) & 0x3f
m2 = permute(pos)
pos = x[i+2] & 0x3f
m3 = permute(pos)
k = 3
xxx += [m0,m1,m2,m3]
i += k
cip = 'GYldGg-iIoJlPX9hPXpjPqfdEY21B01TBTzeGqfKNR!!'
j = 0
for t in xxx:
s.add(t==ord(cip[j]))
j+=1
res = s.check()
if res == z3.sat:
print(s.model())
model = s.model()
flag = ''
for i in range(0,flag_len):
flag += chr(model[x[i]].as_long().real)
print(flag)
else:
print('oh,no')
