Tags: circuit z3

Rating:

### Challenge Description:
I've stumbled upon this weird minetest map, can you make sense out of it? Minetest + mesecons required Non-standard flag format (enter bits as 0 and 1).

The problem solving steps are straightforward.

1. Get minetest + mesecons, take a look around the map. Note that there are 40 levers (input bits), 1 lamp (output bit), wires & and/or/xor/not gates only at Y=2. Also, it looks as if for every circuit slice of same Z value, input comes from -Z direction and outputs to +Z direction (Strictly speaking, this is false. Nevertheless, it gives us a very good POV of how we can analyze the circuit).
2. [Parse](https://github.com/AndrejIT/map_unexplore) the circuit.
3. Use [Z3](https://github.com/Z3Prover/z3) to solve for some input that results in the lamp to turn on.

Below is the parsing + solving code, modified from the [parser](https://github.com/AndrejIT/map_unexplore). Pardon me for the messy code :D
python
#!/usr/bin/env python
#Licence LGPL v2.1

import sys #to get parameters
import sqlite3
import mt_block_parser
import re
import os.path
import pickle
from z3 import *

#It is possible to get X, Y, Z directly by SQLite!
#for row in sourcecursor.execute(" SELECT "+
# " CASE WHEN X < 2048 THEN X ELSE X - 4096 END AS X, "+
# " CASE WHEN Y < 2048 THEN Y ELSE Y - 4096 END AS Y, "+
# " CASE WHEN Z < 2048 THEN Z ELSE Z - 4096 END AS Z "+
# " FROM ("+"SELECT "+
# " (pos) & 4095 AS X, "+
# " ((pos) & 16773120)>>12 AS Y, "+
# " ((pos) & 68702699520)>>24 AS Z "+
# " FROM blocks"+
# ")"):

source = r'../map.sqlite'

#use compiled regular expression to filter blocks by block content. it is faster that checking "in array".
useful_block_evidence = re.compile(
#"default:cobble|"+"bones:bones|"+
"mesecon"
)

sourceconn = sqlite3.connect(source)
sourcecursorXZ = sourceconn.cursor()
sourcecursor = sourceconn.cursor()

#X and Z min and max to know image size
for rowMinMax in sourcecursorXZ.execute(" SELECT "+
" MIN( CASE WHEN X < 2048 THEN X ELSE X - 4096 END ) AS minX, "+
" MIN( CASE WHEN Z < 2048 THEN Z ELSE Z - 4096 END ) AS minZ, "+
" MAX( CASE WHEN X < 2048 THEN X ELSE X - 4096 END ) AS maxX, "+
" MAX( CASE WHEN Z < 2048 THEN Z ELSE Z - 4096 END ) AS maxZ "+
" FROM ("+"SELECT "+
" (pos) & 4095 AS X, "+
" ((pos) & 68702699520)>>24 AS Z "+
" FROM blocks"+
")"):
minX = rowMinMax[0]
minZ = rowMinMax[1]
maxX = rowMinMax[2]
maxZ = rowMinMax[3]
width = maxZ - minZ
height = maxX - minX

print(width, height)

if os.path.isfile('data.pickle'):
with open('data.pickle', 'rb') as f:
else:
print("data.pickle nonexistent, fallback to parsing.")
data = [[None]*((height+1)*16) for _ in range((width+1)*16)] # data[z][x]
blockdict = {b'mesecons_walllever:wall_lever_off': 0, # always towards +Z
b'mesecons_lamp:lamp_off': 1, # always from -Z
b'mesecons_insulated:insulated_on': 2,
b'mesecons_insulated:insulated_off': 2, # param2 0: X (ofs 1), 3: Z (ofs 0)
b'mesecons_extrawires:crossover_01': 4,
b'mesecons_extrawires:crossover_10': 4,
b'mesecons_extrawires:crossover_on': 4,
b'mesecons_extrawires:crossover_off': 4,
b'mesecons_extrawires:tjunction_on': 5, # param2 0 = excl. +Z, 1 = excl. +X, 2 = excl. -Z, 3 = excl. -X
b'mesecons_extrawires:tjunction_off': 5,
b'mesecons_extrawires:corner_on': 9, # param2 0 = -Z -X, 1 = -X +Z, 2 = +Z +X, 3 = +X -Z
b'mesecons_extrawires:corner_off': 9,
b'mesecons_gates:and_on': 13,
b'mesecons_gates:and_off': 13,
b'mesecons_gates:or_on': 14,
b'mesecons_gates:or_off': 14,
b'mesecons_gates:xor_on': 15,
b'mesecons_gates:xor_off': 15,
b'mesecons_gates:not_on': 16,
b'mesecons_gates:not_off': 16}

total_chunks = height * width
parsed_chunks = 0
print("Parsing block data...")
#assuming that map is moustly flat limit Y coordinate
for row in sourcecursor.execute(" SELECT "+
" CASE WHEN X < 2048 THEN X ELSE X - 4096 END AS X, "+
" CASE WHEN Y < 2048 THEN Y ELSE Y - 4096 END AS Y, "+
" CASE WHEN Z < 2048 THEN Z ELSE Z - 4096 END AS Z, "+
" pos, "+
" data "+
" FROM ("+"SELECT "+
" pos, "+
" (pos) & 4095 AS X, "+
" ((pos) & 16773120)>>12 AS Y, "+
" ((pos) & 68702699520)>>24 AS Z, "+
" data "+
" FROM blocks"+
")"+
" WHERE Y == 0; "):
block = mt_block_parser.MtBlockParser(row[4])
if row[0] - minX < 0 or width <= row[0] - minX or height - row[2] + minZ < 0 or height <= height - row[2] + minZ:
print("Do not fit:", row[0], row[1], row[2])
else:
block.nodeDataParse()
block.nameIdMappingsParse()
chunk_blockdict = {k: blockdict[v] for k, v in block.nameIdMappings.items() if blockdict.get(v) is not None}
for z in range(16):
for x in range(16):
blockmap = chunk_blockdict.get(block.arrayParam0[z*256 + 2*16 + x])
if blockmap == 5 or blockmap == 9:
blockmap += block.arrayParam2[z*256 + 2*16 + x]
elif blockmap == 2 and block.arrayParam2[z*256 + 2*16 + x] == 0:
blockmap += 1
data[row[2]*16 + z][row[0]*16 + x] = blockmap
parsed_chunks += 1
if parsed_chunks % 1000 == 0:
print("Parsed {0:.2f}%".format(parsed_chunks * 100 / total_chunks))

sourceconn.close()
print("Parsing complete.")

print("dumping to data.pickle...")
with open('data.pickle', 'wb') as f:
pickle.dump(data, f, pickle.HIGHEST_PROTOCOL)
print("Dump complete.")

MAX_Z = 1938
MAX_X = -1
for i in range(MAX_Z):
for j in range((height+1)*16-1, -1, -1):
if data[i][j] is not None:
MAX_X = max(MAX_X, j)
break

print(MAX_Z, MAX_X)

assert(data[MAX_Z][1] == 1) # LAMP

z = 1
for i in range(40):
assert(data[z][i] == 0) # 40 levers
for i in range(40, MAX_X + 1):
assert(data[z][i] is None) # and nothing else
z += 1

func_input = input

LEVER = BoolVector('lever', 40)
input = LEVER + [None]*(MAX_X + 1 - 40) # prev layer's output

S = Solver()
LAMP = None
while LAMP is None:
print("Processing Z = {} / {}".format(z, MAX_Z))

"""
output[x]
layer[x-1] data[z][x] layer[x]
input[x]
"""

layer = [None]*MAX_X
output = [None]*(MAX_X + 1) # next layer's input

# 1. create BoolVector for blocks in current layer
for x in range(MAX_X):
if data[z][x] is not None or data[z][x+1] is not None:
layer[x] = Bool('l{}_{}'.format(z, x))
for x in range(MAX_X + 1):
if data[z][x] is not None:
output[x] = Bool('o{}_{}'.format(z, x))

# 2. put appropriate restrictions on current layer, connecting input & output
for x in range(MAX_X + 1):
if data[z][x] is not None:
b = data[z][x]
if b == 1:
LAMP = input[x]
break
elif b == 2:
elif b == 3:
elif b == 4:
elif b == 5:
assert(False)
elif b == 6:
elif b == 7:
assert(False)
elif b == 8:
elif b == 9:
elif b == 10:
elif b == 11:
elif b == 12:
elif b == 13:
elif b == 14:
elif b == 15:
elif b == 16:

# 4. set output layer as input layer, increment z
input = output
z += 1

print(LAMP)

print(S.check())
m = S.model()
print([m[LEVER[i]] for i in range(40)])


**FLAG: CTF{1110010101000101110010111110000110011001}**

P.S.: The statement *"it looks as if for every circuit slice of same Z value, input comes from -Z direction and outputs to +Z direction"*, is false since the circuits are not uni-directional, i.e. there are no diodes blocking flow towards -Z. This is why the solver code creates bool variables for every output of some layer, and then creates appropriate restrictions rather than just saying, for example, elif b == 2: output[x] = input[x].