Penny splits a restaurant bill between three friends. It gets it right almost every time.
This repo is about the times it doesn't, and about the difference between looking for bugs and knowing there are none left.
Testing tells you what you found. It never tells you what you missed.
That is fine when there are a handful of inputs. Penny has 226 billion. You cannot try them all, so every test you write leaves a gap, and you have no way to measure how big the gap is.
This page puts both approaches on the same screen, gives them the same job, and lets you watch one of them run out of road.
Nothing to configure. This is the space the board sweeps:
| People | 3 |
| Tax | 8.25% |
| Tip | 0% to 30%, each person picks their own |
| Bill | 10.00 to 10,000.00 |
Small enough to read in a morning. But each person picks a tip independently, and that is what makes it big:
61 tips (you)
x 61 tips (Alex)
x 61 tips (Sam)
= 226,981 tip combinations
x 999,001 bills
= 226,754,245,981 (combination, bill) pairs
Two parts of the app work out each person's tip, and they round differently.
flowchart LR
A["$19.70 bill<br/>tips 20% · 15% · 20%<br/>split 3 ways"] --> B["Alex's tip share is<br/><b>98.5 cents</b><br/>exactly half"]
B --> C["payments side<br/>rounds up<br/><b>99c</b>"]
B --> D["ledger side<br/>rounds to even<br/><b>98c</b>"]
C --> E["card charged<br/><b>$24.94</b>"]
D --> F["receipt says<br/><b>$24.93</b>"]
E --> G(["1 cent too much"])
F --> G
Money is kept in whole cents, so a share of 98.5 cents has to go one way or the other. Somebody has to decide which.
- The payments side rounds up. That is normal in money code, and deliberate.
- The ledger side rounds to the nearest even number, because that is what Python does by default and nobody chose it.
Both answers are correct. They just disagree, and when they do the card is charged a cent more than the receipt says.
No floating point is involved anywhere. This is not a rounding error. It is two teams answering the same question differently and never comparing notes.
How often: 1 of every 72 (combination, bill) pairs. When everyone tips 15%, 1 bill in 40.
| Approach | What you try | What happens |
|---|---|---|
| Pick examples | a small bill, a big one, a round one | all pass |
| Try the edges | $10.00, $10,000.00, 0% tip, 30% tip | all pass, the bug is in the middle |
| Random inputs | thousands of generated bills | finds a bad one in 0.11 seconds |
| Try everything | all 226 billion | 4.8 days |
Random input testing is genuinely good here. It finds the bug almost instantly.
Then it stops at the first failure and goes quiet. Is there one bad bill, or ten billion? Did the fix work, or did it just move the problem? It cannot say. And the only way to be certain by testing is the last row, which takes most of a week.
Press Find defects and the page runs both at once, on the same bills.
| Covers | Time | |
|---|---|---|
| Testing, one bill at a time | 0.0017% | 7 seconds |
| Asking Z3 | 100% | 0.27 seconds |
Testing | 0.0017% after 7 seconds
Z3 |################################### 100% after 0.27 seconds
The testing lane runs flat out for seven seconds, gets through 3.9 million pairs, and stops. The page then tells you what finishing would cost, measured from how fast it was actually going: 4.8 days. Then it runs that clock forward so you can watch the days go past.
The other lane answers for all 226 billion in a quarter of a second, and finds 3,161,415,420 pairs that overcharge.
It never checks bills one at a time.
The bad bills are not scattered at random. They fall in a regular pattern, evenly spaced. So rather than hunting for them, the page asks Z3 up to three questions about each tip:
- What is the smallest bill that breaks?
- What is the next one?
- Is there anything in between that we missed?
The gap between the first two answers gives the spacing. The third question is the one that matters: when Z3 reports that nothing else exists, the list is finished. Not "we looked and found no more", but "there are no more".
167 questions covers the whole thing. And the cost does not grow with the range. A hundred times more bills is still 167 questions.
That is the whole difference. One lane is looking. The other is knowing.
Some tips can never break. 8 of the 61: 0%, 4%, 8%, 12%, 16%, 20%, 24% and 28%. Every whole multiple of 4% is safe for every bill. Not "we tested it and it was fine" but "it cannot happen".
The tax never matters. Both sides work the tax out identically, so it cancels. Every bad cent comes from the tip. That was not the assumption going in.
The damage has a ceiling. At most one cent per person, so never more than three.
Needs Python 3.11+ and uv.
uv run python -m app.serverOpen http://127.0.0.1:8000 and press Find defects.
The two lanes are built from completely separate code and are checked against each other on every bill they both look at. If they ever disagreed, the page would say so instead of quietly showing you a number.
Here is the part that would be dishonest to leave out.
Halve the bill. If you can do it three times and still have whole cents, no tip can ever break that bill.
$10.00 is 1000 cents: 500, 250, 125. Three halvings, all whole. Safe forever. Every whole multiple of two dollars clears the same bar, which is why the values in every test plan ever written are the worst possible choices here.
$25.00 halves twice and stops. One short. It ties at a 1.5% tip.
The same arithmetic answers both questions the solver was asked. Whether a tip can ever tie is one check on the spacing it lands on, and 20% fails that check, which is where the immunity list comes from. Where it ties is one step to the first one and read off the interval. At 7% the ties start at $10.50 and repeat every $6.00.
That is app/closed_form.py. Nine lines, no solver, roughly 8,000 times faster
than asking Z3 the same question.
So Z3 was never necessary here. What it bought was not having to work any of that out. Nobody had to notice the condition was regular, derive the spacing, or handle the case where the arithmetic has no answer. You state the condition and you ask.
And the fragility is not in the constants. Moving to a currency with three
decimals changes a number. Nest the rounding, split the remainder unevenly, add
a fourth path, and the neat arithmetic stops applying at all while the model in
prover.py needs one line edited.
The closed form is not a rebuttal of the solver. It is how you check one.
tests/test_closed_form.py puts them in front of each other, and two methods
that share no code agree on all 61 tips. That agreement is worth more than
either answer alone.
A page about not trusting what you have not verified should not ask you to take its own tests on trust either.
uv run pytest # does the code do what it says?
uv run python tools/mutation.py # would the tests notice if it did not?The second breaks the code on purpose, fourteen ways, and fails if a mutant that should die survives. It runs the suite unmutated first, because a harness that grades a test suite has to know the suite was green before it started.
Whole cents everywhere. Round once at the end, not at every step. The same rounding rule on both sides of the wire. And when a cent is left over, hand it to someone on purpose rather than letting it appear out of nowhere.