Minimal counterexamples for an LRU cache

Example-based tests find the bugs you already thought of. A cache bug is almost never one of those — it is a sequence: put, put, get, put, and the wrong key comes back. Nobody writes that test, because nobody imagines it.

Hypothesis’s RuleBasedStateMachine does. You give it operations and invariants; it drives your object with random sequences and, when something breaks, shrinks the sequence to the shortest one that still breaks it. That last part is the whole value. A 200-step random failure is noise; the same failure reduced to three steps is a bug report.

This problem is the machine, built by hand and made deterministic so it has exactly one right answer.

What to write

class Model:  # get / put / keys_in_lru_order, the reference semantics

def find_counterexample(
    *, capacity: int, impl: str, alphabet: Sequence[Op], max_len: int
) -> Report

The model is a correct LRU cache: at most capacity entries; put of an existing key updates its value; both get (on a hit) and put make a key the most recently used; when full, the least recently used entry is evicted. keys_in_lru_order() lists live keys least-recently-used first.

Write it from that contract. Four implementations are given and every one of them is wrong in a different way — a model copied out of one of them agrees with it perfectly and finds nothing, which is the failure mode of every “test that mirrors the implementation” ever written.

The search is breadth-first over operation sequences: all sequences of length 1, then all of length 2, up to max_len. Within a length, enumerate in lexicographic order of indices into alphabet — exactly what itertools.product(range(len(alphabet)), repeat=length) yields. Run each sequence against a fresh implementation and a fresh model, and return the first one that disagrees.

disagreement(...) is provided: it steps both, compares get return values and then LRU order after every operation, and returns a message or "".

Return {"found": True, "sequence": [...], "reason": "..."} for the first disagreement, or {"found": False, "sequence": [], "reason": ""} if the space up to max_len is clean.

Why the first hit is already minimal

You do not need a shrinking pass, and the reason is worth internalising. If a sequence of length $L$ first diverges at step $k < L$, then its own $k$-step prefix diverges too — and breadth-first order already examined every sequence of length $k$. So by the time you are testing length $L$, no prefix can fail, and any divergence you see is at the final step. Breadth-first search returns minimal counterexamples for free. Hypothesis shrinks because it searches randomly rather than exhaustively; exhaustive search over a tiny alphabet gets minimality by construction, and pays for it in state space.

Read the “not found” cases carefully

Several test cases return found: False against an implementation that is definitely broken — because the alphabet cannot reach the bug. An off-by-one capacity needs enough distinct keys to overflow. A get that fails to refresh recency is invisible when the cache only ever holds one entry. This is the honest limit of every automated search, Hypothesis included: it explores the state space you described, not the one your users have. Choosing the operation alphabet is a modelling decision, and it is where the thinking actually happens.