◧Puzzle15

The board, and where its numbers come from

The state is one fixed-size array: [[Option<u8>; 4]; 4]. No heap, cheap to copy — which matters later, because the search clones boards by the thousand. The empty square is not a magic 0; it is None, so the type system knows an empty square is not a tile you can read.

The layout is worth a moment. Rather than typing out sixteen assignments, I read three known cells off the finished grid, wrote them as three simultaneous equations, and solved for the coefficients — the derivation is still sitting in the source as a comment. What comes back is one expression that fills the whole board.

The one thing to keep straight is that x is the column and y is the row, so the array is indexed tile_array[x][y] — and Display transposes it back on the way out, printing row by row so the string matches how a human reads a grid.

Four moves, named for the tile

The Move enum is where I got caught first, and where reading the tests carefully paid for itself. A variant is named for what the tile does, not what the hole does. LeftToRight does not move the hole to the right. It takes the tile sitting to the left of the hole and slides it rightward into the gap — so the hole ends up one column further left.

Once that clicks, perform_move is short: find the None, check the bound in the direction the hole is about to travel, swap. If the bound fails, the move returns false and the board is untouched.

perform_moves then plays a whole slice and returns how many moves succeeded, not whether all of them did. That is a deliberately forgiving contract — an illegal move in the middle of a sequence is skipped, not fatal — and the tests lean on it: a five-move sequence that returns 3 is the assertion, not a failure.

Parsing a board without trusting it

from_str reads the same text Display writes, which sounds trivial and isn't. A row splits on | into six fields, not four: the delimiters at each end produce empty strings that have to be stepped over. Four spaces mean the hole. Anything else has to parse as a number and land in range.

The real work is the last gate. After sixteen cells are read, the whole board goes into a HashSet and the count has to be exactly 16 — which rejects a duplicated tile and a second hole with the same check, because two Nones collapse into one entry just like two 7s do.

Every one of those rejects is a fixture in the test file. Writing the failing cases turned out to be more instructive than writing the happy path: it forced the question of what "a valid board" actually means, rather than what the parser happened to accept.

Finding the shortest path, not just a path

find_shortest_path walks from one board to another. The interesting constraint is in the doc comment: it might run forever if no path exists, so the guarantee has to come from the traversal itself rather than from a bound on the work.

It is breadth-first, and the reason it returns a minimal path is entirely structural. The frontier is strictly first-in-first-out, so states are reached in nondecreasing order of depth, and the first time you touch a state is also the cheapest way to have touched it. Marking each state as seen at enqueue time rather than at visit time keeps duplicates out of the queue instead of merely ignoring them later.

Two things I would change if this were more than an exercise. The frontier is a Vec used as a deque — pop() from the back, insert(0, …) at the front — and that front insert shifts the whole buffer, so it is O(n) per push where a VecDeque would be O(1). And with 16!/2 ≈ 10.5 billion reachable boards, plain BFS is fine for the shallow cases the tests ask for and hopeless for a scrambled board; that is where an A* with a Manhattan-distance heuristic would belong.

What the search does give you for free is GameState's Hash and Eq implementations doing real work. The board being a small, ordinary, comparable value is what makes the visited set possible at all.

In Rust, a move is one swap, and I find the hole by scanning for it. A circuit cannot scan. There is no loop and no "then"; there is only what every register evaluates to on the same clock edge. So the question stops being "which two squares do I swap?" and becomes "for each of the sixteen squares independently, what does it become?" — and the answer for most of them, most of the time, is the same thing it already was.

None of that machinery is mine. The exercise hands you three crates and expects the modelling to happen in them:

Learning the primitives on three counters

The file walks you in through counters, and the progression is well chosen. The first is given: a register that adds one to itself forever. The second has to stop at a configurable maximum. The third gains an en input that decides whether it ticks at all.

The hint that unlocks it is that ctx.bv_ite — pick a or b based on a condition — is a multiplexer. Which means the second counter is not "an if-statement in a circuit"; the comparator and the mux are the circuit, and the if was only ever a way of talking about them.

Those expressions are the real output of the test run — patronus serialises each system, so you can read back the thing you just described and check it says what you meant. Watching a nested ite appear where I had written nested conditionals is the moment the mental model flipped for me: control flow in hardware is structure, not sequence. The enabled counter passes 20,000 simulated cycles against a reference count, toggling the enable every other one.

Sixty-four bits, sixty-four muxes

The board becomes sixteen bv<4> registers named pos_x_y, with 0 standing in for the hole — four bits is exactly enough for 0–15, so the encoding is tight rather than convenient. The move is a 2-bit input decoded into four one-hot conditions, and is_empty for each square is just a comparison against zero.

Then the next-state function. For one square, it is a chain of four muxes — one per direction — each defaulting to "hold" and only overriding when its direction is selected, the square is in bounds, and the neighbour it would trade with is the hole:

That structure is repeated sixteen times, and the shape of the result is the lesson. In software, an illegal move is something you detect and reject. Here there is nothing to reject: an illegal move is simply a set of select conditions that all evaluate false, and every register quietly holds its value. The bounds check isn't a guard clause — it's a wire that never asserts.

Where it stands

The software half is done and green. The circuit half is where the work stopped, and I would rather show that accurately than tidy it up after the fact.

The failure is not mysterious, and it is a genuinely Rust-flavoured mistake. Each mux arm is built inside a closure that patronus evaluates eagerly — it is constructing an expression graph, not deferring a branch. So even though the guard correctly refuses to read a neighbour when x == 0, the other arm still calls pos_to_index(x - 1, y) on an unsigned x, and 0 - 1 panics before the guard is ever consulted. That is precisely the "overflow error" the last commit is named after.

There is a second problem queued up behind it: where the guard falls back it yields c.zero(4), a four-bit zero, and that gets and-ed with a one-bit move condition. Mismatched widths — the same class of bug, caught by the type system of the bit-vector library rather than by Rust's.

The fix is to hoist the neighbour lookup out of the closure so the index is only computed when it exists, and to make the fallback a one-bit false. What I would build on top, given the time, is the thing the easy-smt dependency is sitting there for: stop simulating single moves and start proving properties — that tile values are a permutation at every step, that exactly one square is ever empty, that the circuit and the Rust model agree for every move from every reachable board.

Why I built it this way

• Read the tests before writing the code. The move names, the six-field row format, the "count the successes" contract — none of that is stated anywhere else. The test file was the specification.
• Let the type system carry the hole. Option<u8> instead of a sentinel means an empty square can never be mistaken for a tile, and it makes the uniqueness check catch two holes for free.
• Get the guarantee from the structure. BFS returns a minimal path because the frontier is FIFO, not because anything measures or compares lengths afterwards.
• Build the second model to find out what the first assumed. Writing the puzzle as a circuit exposed every place the Rust version quietly relied on doing one thing at a time.
• Report the state honestly. Four tests pass, one fails, and I can name the line and the fix. An exercise you can diagnose is worth more than one you can only claim.