Invariants in practice: proving a goal unreachable without searching

What an invariant is — the chessboard proof

Take an 8 × 8 chessboard and cut off two opposite corners — both the same color, say both white, since opposite corners of a chessboard match. 62 squares remain. Can 31 dominoes tile them, each domino covering two adjacent squares? People try layouts for a long time; every attempt strands two squares somewhere. The proof that every attempt must fail fits in three sentences.

A domino covers two adjacent squares, and adjacent squares always differ in color — so every placed domino covers exactly one black and one white square, wherever it lands. Therefore, at any moment of any attempted tiling, the count of covered black squares equals the count of covered white squares: that equality is our invariant — a property that every allowed move preserves. But the mutilated board has 32 black and only 30 white squares, so a complete tiling would need covered-black to equal 32 and covered-white to equal 30 — violating the invariant. No tiling exists.

Notice what just happened: we ruled out all tilings — every layout anyone will ever try — without trying any. That is the entire job description of an invariant: a property of a system’s state that holds at the start and is preserved by every allowed move. If the goal state lacks the property, the goal is unreachable, period.

Two more machines: sign-flip and water jugs

The sign-flip game. A whiteboard shows four signs: +, +, −, +. The allowed move: pick any two entries and flip both. Goal: all four positive. The invariant: count the minus signs and look at its parity. A move flips two entries, and there are only three cases: both were plus (minus-count rises by 2), both were minus (falls by 2), one of each (net 0). In every case the minus-count changes by −2, 0, or +2: its parity never changes. The start has one minus — odd. The goal has zero — even. Unreachable, after any number of moves, in any order. Note the upgrade from the chessboard: the invariant quantity is allowed to change, as long as something about it (here, parity) cannot.

The water jugs. Two jugs, 12 liters and 8 liters, a tap and a drain; moves are fill a jug, empty a jug, or pour one into the other until source is empty or target is full. Can you measure exactly 6 liters? Every amount you ever see is a multiple of 4. That is no accident: 4 is the greatest common divisor of 12 and 8 — both capacities are multiples of 4, the start (0) is a multiple of 4, and each move only adds, subtracts, or transfers amounts built from the capacities and current contents, so multiples of 4 stay multiples of 4. The reachable amounts are exactly 12, and 6 is not among them. Goal differs from start on the invariant property “every amount is a multiple of gcd” — unreachable.

The method as a checklist

Every puzzle above followed the same script, and it is worth writing down:

1. List every allowed move, exhaustively — an invariant argument is only as good as its move list.
2. Hunt for a quantity each move preserves — a fixed total, a parity, a “multiple of d”, a color balance, or a quantity that moves only one direction (only grows, only shrinks).
3. Verify the candidate against each move — a single move that breaks it kills the candidate, and this verification is the actual work.
4. Compare start and goal on the invariant — if they differ, the goal is unreachable, and you are holding a proof, not a hunch.

Loop invariants and conservation asserts in code

You have been writing invariants all along. The accumulator argument is one: in a summation loop, “acc equals the sum of the first i elements” holds before the loop starts (i = 0, acc = 0) and is re-established by every iteration:

let acc = 0;                      // invariant holds: sum of first 0 items is 0
for (let i = 0; i < xs.length; i++) {
  // invariant here: acc === xs[0] + … + xs[i-1]
  acc += xs[i];                   // the move re-establishes it for i + 1
}
// loop ends with i === xs.length, so: acc === sum of the entire array

The Hook’s migration is the conservation flavor — the same invariant as the jugs, wearing production clothes:

// Conservation invariant: a transfer moves cents; it never mints or burns them.
function transfer(from, to, cents) {
  from.cents -= cents;
  to.cents += cents;              // debit equals credit — the move preserves the total
}

const total = (accs) => accs.reduce((sum, a) => sum + a.cents, 0);

const before = total(accounts);
applyAllMoves(accounts);          // millions of transfers, any order whatsoever
console.assert(total(accounts) === before, "cents created or destroyed");

The assert is the invariant made executable. It does not check any particular sequence of moves — it checks the property that every legal sequence must preserve, which is why it catches bugs that example-based tests cannot: the rounding bug minted a cent on one move out of millions, and the total ratted it out.

Limitation: invariants prove unreachability only

One honest limitation: an invariant proves unreachability when start and goal differ on it. When they agree, the invariant alone proves nothing — the goal might be reachable or blocked by some other obstruction. Six liters is provably impossible with the 12-and-8 jugs; that 4 liters is reachable still has to be shown by exhibiting moves (fill 12, pour into 8, four remain — done). Impossibility proofs and constructions are different deliverables.

This closes the logic track, and each of its three tools is a down payment on the algorithms track. Counting becomes complexity analysis. The pigeonhole principle becomes lower bounds: any hash with fewer outputs than inputs must collide, any comparison sort must spend on the order of n·log n comparisons to tell n! orderings apart. Invariants become correctness proofs: every loop you will prove correct — binary search, partitioning, graph traversal — is proved with a loop invariant. The puzzles were never the point; the forms of argument were.