Kingsroad generates its maps, so it has to prove each one beatable before showing it. It does that by playing a reference build through the real game.
The interesting decision is not that the proof exists. It is what the proof is not allowed to use.
The reference build plays with one hand tied
It never builds a Barracks. It never collects a gold crate.
Both are real mechanics that a real player will use, and both make the game easier. Excluding them from the proof means the guarantee we can make is: this map is beatable even if you ignore the Barracks entirely and never pick up a single crate.
That is a floor. The alternative — letting the proof use everything — gives you a ceiling: "beatable if you play it the way our reference build happens to play it", which is a much weaker claim and a much easier one to accidentally overfit to.
The floor also does something nice to the two excluded mechanics. They stop being systems we hope are balanced and become provably upside: they can only help, because the game is already winnable without them.
Why it has to be an assertion, not a comment
A proof that quietly leans on the systems your copy calls optional is a lie in the most difficult shape to notice. Everything passes. The pipeline is green. The manifest text is false and nothing anywhere disagrees with it.
So the exclusion is enforced:
check('the reference build collected zero crates', sweep.every(r => r.cratesTaken === 0))
check('the reference build built zero Barracks', sweep.every(r => r.barracks === 0))
Two lines. Without them, the day someone "improves" the reference build by letting it grab a crate is the day the guarantee silently becomes a different, weaker guarantee, with the same words on the page.
Four ways a generate-then-prove guarantee fails silently
Each of these needs its own test, because none of them shows up as an error.
1. Proved against arithmetic instead of against the game. If the prover
computes damage from a formula while the game runs a simulation, you have proven
something about the formula. Run the real step() at the real fixed timestep,
and assert that a live run and a headless run of the same seed agree.
2. Spending money the player never gets. A prover with an unchecked wallet
will happily build a solution nobody can afford. Assert
spent <= startGold + earned.
3. Leaning on "optional" systems. The two checks above.
4. Incapable of failing. This is the one people skip. A proof that can never go red is not a proof, and you cannot tell the difference by looking at it. So sabotage it — set the health multiplier to 3, or forbid building at all — and require a failure.
The trap inside the trap: a sabotage wider than its guard passes for the wrong reason. If you break five things at once and something goes red, you have not learned which of the five the guard catches. Break exactly the thing the guard claims to catch, and nothing more.
Two habits that made the whole thing hold
Use a fixed timestep in the live loop too. Kingsroad runs an accumulator at
1/60 in the real game, not just in the prover. With a variable delta from
requestAnimationFrame, the proof describes a game nobody plays — it describes
the game as it runs on the machine that ran the proof.
Keep random streams separable. Marcher spawns consume no randomness at all; they are schedule-driven. That is what makes "crates were never collected" provably a statement about crates, rather than a statement about having accidentally rolled a different wave. A shared stream would have entangled the two and made the assertion meaningless while still passing.
And one small thing that cost us time
When your codebase has a convention, read the signature before calling it.
GD.sfx.play(cue, semitones) takes a pitch, not a gain. GD.best(key).record(v)
returns {value, isNew}, not a boolean. GD.share.score takes
{score, unit, isBest}. None of those fail loudly.
Play it: Kingsroad · how to play
Related reading: every repair rung fired at once · five wrong ways to prove a racing game is fair
