Case Study: Auditing a Sharding Rule with Direct Proof and Contraposition

DataField.Dev

Case Study: Auditing a Sharding Rule with Direct Proof and Contraposition

"It passed every test we tried" is the most expensive sentence in software. — a maxim for on-call engineers

Executive Summary

A production service routes user records to one of two database shards by a one-line rule: even user IDs go to shard 0, odd IDs to shard 1. On top of that, a caching layer claims a "balance invariant" and an access-control layer claims a "consistency property." All three layers were shipped green — every unit test passed. Then a data-migration ticket asks the uncomfortable question: are these properties actually true for every user ID, or just for the IDs the tests happened to use?

This is an analysis-heavy case study: you will not build a new system. You will take an existing one, extract the precise claims hidden in its docstrings and comments, and decide — claim by claim — whether each is a theorem (provable for all inputs) or merely a conjecture (true on the tests, unproved in general). The ones that are theorems you will prove, choosing direct proof or contraposition as the shape of the claim demands. The ones that are false you will kill with a counterexample. By the end you will have done exactly what §4.1's opening promised: turned "it passed every test" into "it is correct, always" — or exposed where that upgrade is impossible.

Skills applied

Extracting a precise mathematical claim from informal code comments (§4.1, §4.2).
Distinguishing a theorem from a conjecture before trying to prove anything (§4.1).
Writing complete direct proofs of divisibility and parity claims (§4.3).
Recognizing when a direct attack stalls and switching to contraposition (§4.4).
Reading a flawed proof critically and producing a counterexample (§4.5, §4.6).

Background

The system

The service stores user records. To spread load, it splits records across two shards using the parity of the integer user ID:

def shard_of(user_id):
    """Route a record. Even user_id -> shard 0, odd user_id -> shard 1.
    Precondition: user_id is a nonnegative integer."""
    return user_id % 2   # 0 if even, 1 if odd

print(shard_of(0), shard_of(7), shard_of(42))
# Expected output:
# 0 1 0

Three claims travel with this code, scattered across comments and a design doc:

Claim A (the routing contract). "Shard 0 holds exactly the records whose ID is even; shard 1 holds exactly the odd ones."
Claim B (the cache-prefetch rule). "If a user ID is divisible by 6, its record lives on shard 0." (A prefetcher uses this to warm shard 0 with every 6th ID.)
Claim C (the audit invariant), as originally written. "Two records collide in the audit log only if their IDs are equal — because the audit key is id // 2, and equal audit keys force equal IDs."

💡 Intuition: Every one of these is a universally quantified conditional in disguise — "for every user ID $n$, if … then …". That is precisely the shape §4.3 taught us to attack with a direct proof, and §4.4 taught us to attack by contraposition when the direct route stalls. The work of this case study is mostly seeing the conditional inside the prose.

Why this matters

A sharding rule that is merely probably correct is a latent outage. If even one user ID violates Claim A, that user's record can be written to one shard and read from the other — a silent data-loss bug that no amount of "it worked in staging" prevents. Theme two of this book is the whole point here: a passing test suite suggests correctness; only a proof guarantees it. The IDs in production are unbounded; the IDs in the test suite are a handful. The gap between them is exactly where a proof earns its keep.

Phase 1: Turn the prose into precise claims

Before proving anything, we translate each claim into the chapter's vocabulary, using the exact definitions from §4.2 ($n$ even iff $n = 2k$; $a \mid b$ iff $b = ac$ for some integer $c$).

Claim A, precisely. "Shard 0 holds exactly the even IDs" is a biconditional: for every nonnegative integer $n$, $$\texttt{shard\_of}(n) = 0 \iff n \text{ is even}.$$ The word exactly is the tell that this is an "if and only if," not a one-way "if." Per §4.3, a biconditional must be proved in both directions.

Claim B, precisely. For every integer $n$, if $6 \mid n$, then $n$ is even (equivalently $\texttt{shard\_of}(n) = 0$). This is a one-way conditional about divisibility — a direct-proof target.

Claim C, precisely. The doc says "equal audit keys force equal IDs," where the audit key is the integer $\lfloor n/2 \rfloor$ (Python's n // 2). As a conditional: for all nonnegative integers $m, n$, if $\lfloor m/2 \rfloor = \lfloor n/2 \rfloor$, then $m = n$.

🔄 Check Your Understanding Which of Claims A, B, C is a biconditional, and how can you tell from the English before doing any math?

Answer

Claim A is the biconditional — signaled by "exactly the records whose ID is even" (shard 0 is all and only the even IDs). Claims B and C are one-way conditionals ("if … then …"); B says nothing about whether every even ID is divisible by 6 (it isn't), and C asserts one direction only.

⚠️ Common Pitfall: Skipping this translation step is the single most common way audits go wrong. If you start "proving" Claim A while still picturing it as a one-directional "even IDs go to shard 0," you will prove half of it and declare victory — exactly the converse error of §4.4. Write the conditional (or biconditional) out symbolically first.

Phase 2: Prove Claim A (the routing contract) — both directions

Claim A is a biconditional, so we owe two proofs. We will lean on a fact the chapter used freely: for an integer $n$, n % 2 == 0 is true exactly when $n$ is even, and n % 2 == 1 exactly when $n$ is odd (every integer is one or the other). We make the witness explicit.

Theorem (Claim A). For every nonnegative integer $n$, $\texttt{shard\_of}(n) = 0$ if and only if $n$ is even.

The strategy first. Both directions are clean direct proofs — unpack the definition on one side, read off the other. Forward: from "$n$ even" produce "$n \% 2 = 0$." Reverse: from "$n \% 2 = 0$" produce a witness $k$ with $n = 2k$. No contraposition needed; the claim hands us equations on both sides.

Proof (forward: even $\Rightarrow$ shard 0). Let $n$ be an arbitrary nonnegative integer and assume $n$ is even. By the definition of even, there is an integer $k$ with $n = 2k$. Then $n$ is a multiple of $2$, so dividing $n$ by $2$ leaves remainder $0$; that is, $n \bmod 2 = 0$. Hence $\texttt{shard\_of}(n) = n \% 2 = 0$. $\blacksquare$ (forward)

Proof (reverse: shard 0 $\Rightarrow$ even). Assume $\texttt{shard\_of}(n) = 0$, i.e. $n \bmod 2 = 0$. By the division algorithm, $n = 2q + r$ with remainder $r = n \bmod 2 = 0$, so $n = 2q$ for the integer $q$. Taking $k = q$ exhibits an integer with $n = 2k$, so by the definition of even, $n$ is even. $\blacksquare$ (reverse)

Both directions hold, so the biconditional holds: shard 0 is exactly the even IDs. By the same argument with remainder $1$, shard 1 is exactly the odd IDs. Claim A is a theorem — true for every nonnegative integer, not just the tested ones.

🔗 Connection. We invoked the division algorithm ("$n = 2q + r$ with $0 \le r < 2$") informally here; Chapter 22 states and proves it in full and makes it the foundation of the Euclidean algorithm. For now, the takeaway is that "even" and "remainder 0 mod 2" are two faces of the same fact, and a proof can move between them by exhibiting the witness $k = q$.

Phase 3: Prove Claim B (the prefetch rule) by direct proof

Claim B says divisibility by 6 implies the record is on shard 0, i.e. the ID is even. This is the divisibility-composes pattern from §4.3, Example 2.

Theorem (Claim B). For every integer $n$, if $6 \mid n$, then $n$ is even.

The strategy first. One hypothesis, existential in disguise: "$6 \mid n$" gives a witness $c$ with $n = 6c$. Rewrite $6c$ to expose a factor of $2$, then repackage into the definition of even. Unpack, regroup, repackage — the master habit.

Proof. Let $n$ be an arbitrary integer and assume $6 \mid n$. By the definition of divides, there is an integer $c$ with $n = 6c$. Then $$n = 6c = 2(3c).$$ Let $k = 3c$. Since $c$ is an integer, $k$ is an integer, and $n = 2k$. By the definition of even, $n$ is even. Since $n$ was arbitrary, the implication holds for all integers $n$. $\blacksquare$

So the prefetcher is safe: every ID divisible by 6 really does land on shard 0. Claim B is a theorem.

🔄 Check Your Understanding The converse of Claim B is "if $n$ is even, then $6 \mid n$." Is it true? What does its truth or falsehood mean for the prefetcher's coverage of shard 0?

Answer

The converse is false: $n = 4$ is even but $6 \nmid 4$. So while every multiple of 6 is on shard 0 (Claim B), the multiples of 6 do not cover all of shard 0 — the prefetcher warms only some of shard 0's records, not all. Confusing Claim B with its converse would lead an engineer to wrongly believe the prefetcher covers the whole shard. This is the §4.4 converse trap, caught by one counterexample.

Phase 4: Audit Claim C — read the "proof" critically, then break it

Claim C arrived in the design doc with a proof. Here it is, verbatim:

"Claim C. For all nonnegative integers $m, n$, if $\lfloor m/2 \rfloor = \lfloor n/2 \rfloor$, then $m = n$. Proof. Suppose $\lfloor m/2 \rfloor = \lfloor n/2 \rfloor$. Write $m = 2\lfloor m/2 \rfloor$ and $n = 2\lfloor n/2 \rfloor$. Since the two floors are equal, $m = 2\lfloor m/2 \rfloor = 2\lfloor n/2 \rfloor = n$. $\blacksquare$"

Run the §4.6 reading routine on it.

Form of the claim. A universally quantified conditional over two variables. Fine.
Strategy. A direct proof: assume the hypothesis (equal floors), derive $m = n$. Reasonable plan.
Setup. Variables are arbitrary, hypothesis assumed correctly (not the converse). Still fine.
Justify each step. Here it breaks. The line "$m = 2\lfloor m/2 \rfloor$" is false for odd $m$: if $m = 7$, then $\lfloor 7/2 \rfloor = 3$ and $2 \cdot 3 = 6 \neq 7$. The correct identity is $m = 2\lfloor m/2 \rfloor + (m \bmod 2)$ — the remainder term was silently dropped.
The close therefore rests on a false step; the conclusion is unsupported.

Worse, the claim itself is false. Hunt for the dropped case the way §4.6 taught — look where the remainder differs:

def audit_key(n):
    return n // 2

# Search for a counterexample: equal audit keys but different IDs.
counterexample = None
for m in range(0, 20):
    for n in range(0, 20):
        if m != n and audit_key(m) == audit_key(n):
            counterexample = (m, n)
            break
    if counterexample:
        break

print(counterexample)
# Expected output:
# (0, 1)

Hand-trace it: the inner loops scan $m, n$ in increasing order. The first pair with $m \neq n$ and equal keys is $m = 0, n = 1$, since $\lfloor 0/2 \rfloor = 0 = \lfloor 1/2 \rfloor$. The code returns $(0, 1)$.

So $m = 0$ and $n = 1$ have the same audit key ($0$) but are different IDs — a flat counterexample (Chapter 2) to Claim C. The audit invariant as written is wrong: records $0$ and $1$ collide in the audit log without being the same record. Every consecutive even/odd pair $(2t, 2t+1)$ collides the same way.

🐛 Find the Error (your turn). The doc's author, shown the counterexample, proposes a patch: "Restrict to even IDs only; then the floor proof works." Is the patched claim — "for all nonnegative even integers $m, n$, if $\lfloor m/2 \rfloor = \lfloor n/2 \rfloor$ then $m = n$" — true? Sketch why or find a counterexample.

Answer

The patched claim is true. For even $m$, $m \bmod 2 = 0$, so the dropped remainder term vanishes and $m = 2\lfloor m/2 \rfloor$ does hold; likewise for even $n$. Then equal floors give $m = 2\lfloor m/2\rfloor = 2\lfloor n/2\rfloor = n$. The fix is exactly to restore the precondition that makes the once-false step true — a reminder that a claim's hypotheses are load-bearing.

The corrected audit invariant

The honest invariant is a biconditional with a remainder: for nonnegative integers $m, n$, $$m = n \iff \big(\lfloor m/2 \rfloor = \lfloor n/2 \rfloor \ \text{and}\ m \bmod 2 = n \bmod 2\big).$$ In words: two IDs are equal exactly when they share both an audit key and a parity. The original doc kept only half the key. The audit system needs to log the parity bit alongside the floor.

💡 Intuition: The bug in Claim C is the proof-world twin of an off-by-one in code review. The author "knew" that dividing by two and multiplying back gets you home — true for even numbers, silently false for odd ones, exactly the unhandled case a good reviewer hunts for. Treating the doc's proof like a pull request — challenging every line with "why does this follow?" — is what surfaced it.

Discussion Questions

Claim A needed both directions; Claim B needed only one. Looking at the English of each, what is the linguistic signal that told you "biconditional" versus "conditional"? Why does missing that signal lead to the converse error?
In Phase 2 we proved both directions of Claim A directly. Could either direction have been done by contraposition instead? Write the contrapositive of the reverse direction and decide whether it would be easier or harder.
The counterexample to Claim C was $(0, 1)$, but $(2, 3)$, $(4, 5)$, … all work too. Does exhibiting one counterexample suffice to refute a $\forall$ claim, or must you characterize all of them? Justify from Chapter 2.
Suppose the test suite for shard_of only ever used even IDs. Which of Claims A, B, C would still have passed every test while being false? What does this say about choosing test inputs versus writing proofs?
The corrected audit invariant is a biconditional with an "and." If you had to prove it, how many sub-proofs would you write, and which strategy (direct or contraposition) would each likely use?

Your Turn: Extensions

Option A (three shards). Generalize shard_of to n % 3 (three shards by ID mod 3). State and prove the analogue of Claim B: "if $12 \mid n$, then $n$ goes to shard 0." Identify the witness.
Option B (the prefetch converse). Write a precise statement of the prefetcher's actual coverage of shard 0 (which even IDs it warms and which it misses), and prove that it misses, e.g., every ID of the form $6t + 2$. (This is a direct proof that a certain set of evens is not divisible by 6 — be careful: you are proving a non-divisibility, so think about what you must exhibit.)
Option C (audit, fully). Prove the corrected audit biconditional in full. The forward direction is trivial; the reverse direction splits into using both the floor-equality and the parity-equality. Note which textbook pitfalls (reusing a variable, dropping a case) you had to consciously avoid.
Option D (test, then prove). Use the chapter's find_counterexample to test Claim B on range(0, 200) before re-reading your Phase 3 proof. Explain in one sentence what a None result adds to a proof you already have, and what it would have meant if it had returned a value.

Key Takeaways

Translate before you prove. Most of the audit was reading prose carefully enough to see the conditional (or biconditional) inside it. The word "exactly" turned Claim A into a two-direction obligation; missing it would have produced the converse error.
Decide theorem vs. conjecture first. Claims A and B were theorems and earned full proofs; Claim C looked proved but was false, and one counterexample settled it. "Shipped green" told us nothing about which was which.
Direct proof for constructive claims, contraposition when extraction stalls. Every claim here handed us equations on the hypothesis side, so direct proofs sufficed — but recognizing that is the judgment §4.3–4.4 builds.
Read a proof like a code review. The bug in Claim C was a dropped remainder term — the proof-world equivalent of an off-by-one — and only line-by-line skepticism (§4.6) surfaced it.
A counterexample is a complete refutation. Against a universal claim, the single pair $(0,1)$ did what no number of passing tests could do in reverse: it proved the claim false (Chapter 2).