ILIKETRAINS

The only attachment is an OpenTTD savegame with a truly stupid amount of railway in it. The trains, tracks, and signals are a 32-input logic circuit; whichever input bits make the output true become the flag.

I treated it like a redstone circuit: begin at the lonely output rail, walk backward, recognize gates, and hand the finished expression to a solver. First I had to turn an OpenTTD save into something less hostile than a giant railway map.

Finding the map inside the savegame

OpenTTD uses its own chunked save format. Reading the whole game source is possible, but a smaller project called OpenTTD Surveyor already demonstrates how the map chunks are found. Its parser searches for names such as MAPT, MAPH, MAPO, MAP2, M3LO and MAP5, then reads one or two bytes per tile from each chunk.

The first eight bytes belong to the save header. The remaining data is LZMA-compressed, so the basic extraction is straightforward.

import lzma

savefile = open("challenge.sav", "rb").read()
data = lzma.decompress(savefile[8:])

ncols = 4096
nrows = 4096

def chunk(name, bytes_per_tile=1):
    start = data.find(name)
    offset = start + 8
    size = ncols * nrows * bytes_per_tile
    return data[offset:offset + size]

tile_type = chunk(b"MAPT")
tile_meta = chunk(b"MAP5")

MAPT tells us what kind of object occupies a tile. MAPH holds height, MAPO ownership and other chunks cover signals and extended metadata. For tracing this challenge, MAPT plus the rail bits in MAP5 are the important pair.

def get_tile_at(x, y):
    return tile_type[y * ncols + x]

def get_meta_at(x, y):
    return tile_meta[y * ncols + x]

Probing coordinates in the game and comparing them to the extracted bytes gives the tile IDs we need:

GRASS       = 0x00
RAIL        = 0x10
RAIL_UNDER  = 0x14  # rail below a bridge
RAIL_BRIDGE = 0x90  # bridge end

A straight rail and a split share the same tile type, so MAPT alone cannot tell us which way the track continues. For that I turned to src/rail_cmd.cpp and src/track_type.h in the OpenTTD source. The lower six bits describe the available rail segments.

TRACK_BIT_X     = 1
TRACK_BIT_Y     = 1 << 1
TRACK_BIT_UPPER = 1 << 2
TRACK_BIT_LOWER = 1 << 3
TRACK_BIT_LEFT  = 1 << 4
TRACK_BIT_RIGHT = 1 << 5

TRACK_BIT_CROSS = TRACK_BIT_X | TRACK_BIT_Y
TRACK_BIT_HORZ  = TRACK_BIT_UPPER | TRACK_BIT_LOWER
TRACK_BIT_VERT  = TRACK_BIT_LEFT | TRACK_BIT_RIGHT

TRACK_BIT_3WAY_NE = TRACK_BIT_Y | TRACK_BIT_UPPER | TRACK_BIT_RIGHT
TRACK_BIT_3WAY_SE = TRACK_BIT_X | TRACK_BIT_LOWER | TRACK_BIT_RIGHT
TRACK_BIT_3WAY_SW = TRACK_BIT_Y | TRACK_BIT_LOWER | TRACK_BIT_LEFT
TRACK_BIT_3WAY_NW = TRACK_BIT_X | TRACK_BIT_UPPER | TRACK_BIT_LEFT

Counting the set direction bits distinguishes a single track from a junction.

track_bits = [
    TRACK_BIT_X, TRACK_BIT_Y,
    TRACK_BIT_UPPER, TRACK_BIT_LOWER,
    TRACK_BIT_LEFT, TRACK_BIT_RIGHT,
]

def is_single_track(meta):
    count = sum(1 for bit in track_bits if meta & bit == bit)
    return count == 1

Following one rail

I used four logical directions and their coordinate changes. The map’s first coordinate is the vertical axis in this script, which is why moving up changes x.

direction_diffs = {
    "up":    (-1,  0),
    "down":  ( 1,  0),
    "left":  ( 0, -1),
    "right": ( 0,  1),
}

On straight rails and bridges the direction stays the same. On a corner, the current direction and the metadata bit determine the new heading.

def get_new_direction(tile, meta, previous):
    if tile == RAIL_BRIDGE:
        return previous
    if meta & TRACK_BIT_X == TRACK_BIT_X:
        return previous
    if meta & TRACK_BIT_Y == TRACK_BIT_Y:
        return previous

    if meta & TRACK_BIT_LOWER:
        if previous == "up":   return "right"
        if previous == "left": return "down"
    if meta & TRACK_BIT_UPPER:
        if previous == "right": return "up"
        if previous == "down":  return "left"
    if meta & TRACK_BIT_LEFT:
        if previous == "up":    return "left"
        if previous == "right": return "down"
    if meta & TRACK_BIT_RIGHT:
        if previous == "left": return "up"
        if previous == "down": return "right"

The first version of trace() repeatedly reads the current tile, updates the heading and advances one coordinate. It stops when it reaches grass, an unsupported tile or a junction. That was enough to verify that the parser could follow a simple line across the map, including curves and bridge tiles.

def trace_line(x, y, direction):
    while True:
        tile = get_tile_at(x, y)
        meta = get_meta_at(x, y)

        if tile in (RAIL, RAIL_UNDER) and is_single_track(meta):
            direction = get_new_direction(tile, meta, direction)
            dx, dy = direction_diffs[direction]
            x, y = x + dx, y + dy
            continue

        return x, y, direction

Recognizing the logic gates

In this savegame every gate has the same orientation and every output reaches a split rail. That consistency makes visual pattern matching much easier than building a general OpenTTD signal simulator.

I wrote small matrices containing only grass and rail tiles for the NOT, OR and AND layouts.

not_gate = [
    [GRASS, RAIL,  GRASS],
    [RAIL,  RAIL,  RAIL ],
    [RAIL,  RAIL,  RAIL ],
    [RAIL,  RAIL,  RAIL ],
]

or_gate = [
    [RAIL, GRASS, GRASS, RAIL],
    [RAIL, RAIL,  RAIL,  RAIL],
    [RAIL, RAIL,  RAIL,  RAIL],
]

and_gate = [
    [RAIL,  GRASS, RAIL],
    [RAIL,  RAIL,  RAIL],
    [GRASS, RAIL,  RAIL],
]

When the tracer reaches a split, it collects the surrounding tile types and compares them to those templates. A NOT gate has one upstream input; AND and OR each have two. The known orientation gives the relative coordinates of those inputs.

if surroundings == not_gate:
    return trace(x - 2, y - 1, "up")

if surroundings == and_gate:
    left = trace(left_x, left_y, "up")
    right = trace(right_x, right_y, "up")
    return left, right

if surroundings == or_gate:
    left = trace(left_x, left_y, "up")
    right = trace(right_x, right_y, "up")
    return left, right

Choosing which branch actually leads toward a gate input needs one more helper. Because all inputs are north of the output, I test whether following the left branch eventually reaches a rail that can move upward. If it encounters a forced downward turn first, the other branch is the correct one.

def test_left_leads_north(x, y):
    tile = get_tile_at(x, y)
    meta = get_meta_at(x, y)

    while tile in (RAIL, RAIL_UNDER):
        neighbor_up = get_tile_at(x - 1, y)
        can_turn_up = (
            meta & TRACK_BIT_3WAY_NE == TRACK_BIT_3WAY_NE
            or meta & TRACK_BIT_X == TRACK_BIT_X
            or meta & TRACK_BIT_RIGHT == TRACK_BIT_RIGHT
        )

        if neighbor_up in (RAIL, RAIL_UNDER, RAIL_BRIDGE) and can_turn_up:
            return True

        forced_down = (
            meta & TRACK_BIT_LOWER == TRACK_BIT_LOWER
            and meta ^ TRACK_BIT_LOWER == 0
        )
        if forced_down:
            return False

        x, y = x, y - 1
        tile = get_tile_at(x, y)
        meta = get_meta_at(x, y)

    return False

At this stage the script can move backward through straight tracks, bridges and junctions and identify the three kinds of gate. The last step is representing the circuit instead of only printing its route.

Building the circuit with Z3

Z3 is a theorem prover that can solve Boolean constraints. I created 32 Boolean values for the input tracks. When the tracer reaches the end of an input line it returns the matching variable. When it reaches a gate, it recursively traces the input line or lines and wraps their results in Not, And or Or.

from z3 import *

INPUTS = Bools(" ".join(
    f"input_{index}" for index in range(32)
))

CACHED_GATES = {}

The map reuses some subcircuits, so tracing the same gate more than once wastes a lot of time. I cache the simplified expression by gate type and coordinates.

def trace_not(x, y):
    key = f"NOT_{x}_{y}"
    if key in CACHED_GATES:
        return CACHED_GATES[key]

    expression = simplify(Not(trace(x - 2, y - 1, "up")))
    CACHED_GATES[key] = expression
    return expression

def trace_and(x, y, left_input, right_input):
    key = f"AND_{x}_{y}"
    if key in CACHED_GATES:
        return CACHED_GATES[key]

    expression = simplify(And(
        trace(*left_input),
        trace(*right_input),
    ))
    CACHED_GATES[key] = expression
    return expression

simplify() removes redundant Boolean structure as the recursion returns. The final result of tracing from the last rail tile is one Z3 expression connecting all relevant input variables.

Solving for the input tracks

The output track ends at coordinates (3740, 7). I start there heading upward, constrain the returned circuit to be true and ask Z3 for a model.

start_x = 3740
start_y = 7

circuit = trace(start_x, start_y, "up")

solver = Solver()
solver.add(circuit == True)

print(solver.check())  # sat
model = solver.model()

The model assigns true or false to every input needed by the solution. Converting those values to 1 and 0 in input order creates the flag.

bits = [
    bool(model[INPUTS[index]])
    for index in range(32)
]

flag = "CTF{" + "".join(
    str(int(bit)) for bit in bits
) + "}"

print(flag)