King Halo was a crypto challenge at WannaGame Championship 2025, where our team blackpinker took first place in the international division. It looks like a simulation problem and is really a soundness problem: the server proves Merkle membership with a Halo2 circuit, and the circuit leaves out one constraint. This write-up first appeared on HackMD.
The game
A Rust service runs a horse race. Each round it publishes sixteen horses with their stats, a race distance, and a Merkle root over the sixteen leaves; a leaf is built from a horse's name, strategy, stats, seed, slot and distance, hashed into a binary tree of depth four with Poseidon. To win a round you must submit the index of the horse that wins the simulated race and a Merkle proof that the horse at that index is in the tree. Fifty consecutive wins print the flag.
Two things stand between a player and the flag: knowing who wins, and proving membership. The second one turns out not to stand there at all.
The missing constraint
Verification runs the submitted index, leaf, path_elements and path_indices through a Halo2 MerkleCircuit. The circuit hashes the leaf with each path element in turn and constrains the final value to equal the public root:
cur = leaf
for k in 0 .. len(path_elements):
cur = poseidon(order(cur, path_elements[k], path_indices[k]))
assert cur == root
For a tree of depth four, an honest proof carries four path elements and four direction bits, and the assertion is a real statement about membership. But the circuit never constrains len(path_elements) to be four, and nothing ties index to the path that was actually walked.
Give it an empty path. The loop body never executes, cur is still leaf, and the assertion becomes:
leaf == root
That is a statement the prover can satisfy by choosing the leaf, because the root is public. Set leaf to the announced root, send empty arrays for both path fields, and the proof verifies for any index:
{ "index": winner_idx, "leaf": root, "path_elements": [], "path_indices": [] }
The circuit is still sound about what it says; it just says almost nothing. A proof that leaf == root is not a proof of membership, and because the index is only carried alongside the proof rather than bound into it, the winning slot is free.
TIP
In a circuit, the statement you prove is exactly the set of constraints you wrote, and everything a verifier assumes but does not constrain is an input the prover chooses. Variable-length inputs are the usual place this goes wrong: a fixed-depth tree should constrain the path to the depth, and the index should be derived from the same bits the walk used, not accepted as a separate number.
Still having to win the race
The proof is free; the prediction is not. The server simulates the race itself with a deterministic RNG seeded per round, and compares the submitted index with its own winner. The seed is not published, so the race cannot be replayed exactly.
What it can be is approximated. The simulation in racing.rs is a loop over frames in which each horse's speed is nudged by a per-horse random "wiggle" around a target that depends on its stats, its strategy and the race distance. The randomness perturbs the finish times, but the stats dominate: over many seeds, one horse wins most of the time.
So the solver mirrors the simulation in Python and runs it for many seeds, counting winners:
def predict_winner(entries, distance, samples=1000):
counts = [0] * len(entries)
for seed in range(samples):
rng = random.Random(seed)
sources = [WiggleSource(rng) for _ in entries]
times = simulate(entries, distance, sources)
counts[min(range(len(times)), key=lambda i: times[i])] += 1
# stop once no one can catch the leader with the samples that remain
leader = max(range(len(entries)), key=lambda i: counts[i])
second = max(counts[j] for j in range(len(entries)) if j != leader)
if counts[leader] > second + (samples - seed - 1):
break
return leader
The early exit matters more than the sample count: once the leader's margin exceeds the samples left, more simulation cannot change the answer, and in practice the leader separated well before the thousandth seed. Around 800 to 1,000 samples per round was enough to carry fifty rounds in a row.
The rest of the solver is plumbing: parse the round banner for the distance, the root and the horse table, predict the winner, send the forged proof, and repeat until the flag appears.
W1{I-f0rG07_tO-CH3ck-PAtH-l3NG7H_0f_Th3_m3rkl3-TR3322f622}
Two lessons, one per half
For the circuit. Fix it by constraining the shape of the witness, not by checking it outside the circuit. A depth-four tree takes exactly four path elements and four direction bits; the circuit should lay out exactly four rows of hashing and bind index to the direction bits it used, so that a proof for index i is a proof about the leaf at position i. Length checks written in the service around the circuit are worth having too, but they are the second line: anything the circuit does not constrain is not proved, no matter what the caller validated first.
For the game. The race prediction only worked because the outcome was concentrated: a deterministic simulation whose randomness does not change the ranking is, in effect, public. If the winner is supposed to be unknowable until the round is scored, the seed has to do real work, which means committing to it and revealing it afterwards rather than keeping it secret while its effect is small.
