Find the Shortest Sequence That Breaks an LRU Cache

Hypothesis stateful testing runs random sequences of operations on your code and on a model. When a sequence fails, Hypothesis shrinks it to a short one you can read. The grader cannot run Hypothesis, so here you write a small, deterministic version of that search. It tries every sequence up to a length limit, shortest first.

The cache is an LRU cache, short for least recently used. It holds at most capacity entries. When it is full and a new key arrives, it evicts the entry you used longest ago. The starter gives you four broken caches and a helper that compares a cache with your model.

Write the model

Model(capacity) starts empty, and capacity is zero or more.

• get(key) returns the stored integer and makes key the most recently used. For a missing key it returns None and leaves the order as it is.
• put(key, value) stores the value and makes key the most recently used. Updating a key that is already there replaces its value and evicts nothing. Adding a new key to a full cache evicts the least recently used entry.
• With capacity zero, the model stays empty, even after put.
• keys_in_lru_order() returns a new list of the keys, from least to most recently used.

Write the model from these rules, not from the caches in the starter. A model that copies a broken cache has the same bug, so the search can never find it.

Write the search

def find_counterexample(*, capacity, impl, alphabet, max_len) -> Report

• impl names a factory in IMPLEMENTATIONS. Call it with capacity to make a cache.
• alphabet is a list of operations. Each Op has a kind of "get" or "put", a string key and an integer value. A get ignores its value.
• Try every sequence of length 1, then every sequence of length 2, and so on up to max_len. A sequence can use the same operation more than once.
• Within one length, follow the order of itertools.product(range(len(alphabet)), repeat=length), which picks indices into alphabet. Keep the alphabet as given, without sorting it or removing duplicates.
• Give each sequence a fresh cache and a fresh model, and pass them to disagreement(cache, model, sequence). Stop at the first sequence for which it returns a nonempty string.
• Return {"found": True, "sequence": sequence, "reason": reason}, with the helper's string as reason, unchanged.
• If every sequence passes, return {"found": False, "sequence": [], "reason": ""}. An empty alphabet, or a max_len of zero or less, returns this without trying anything.

Leave the four caches, disagreement and solve as they are.

What disagreement checks

After a get, it compares the two return values first. After every operation, it compares the key order. It returns the first difference, with a step number that starts at 1, or "" if the two always agree.

It never compares stored values after a put. A cache that ignores an overwrite keeps the right key order, so only a later get shows the stale value. For silent_on_overwrite at capacity 2, this sequence:

put("a", 1), put("a", 9), get("a")

gives the reason step 3: get('a') -> 1, model says 9.

Why the first failure is a shortest one

The search tries every shorter sequence before any longer one, so its first failure has the fewest operations possible with this alphabet. The index order breaks ties. You need no shrinking step. If a sequence failed before its last step, that shorter prefix failed too, and the search tried it earlier. This relies on fresh state for every sequence. There are len(alphabet) ** length sequences of each length, so keep both limits small.

When nothing is found

The search can return found: False for a broken cache. The alphabet may have too few keys to fill the cache, or max_len may be too short to reach the bug. A get that does not refresh recency changes nothing at capacity 1. The result says only that no sequence within these limits failed.