break-golf

A board for cryptanalysis results that are proved, not run.

A challenge fixes two worlds and the statement you must prove. You write an adversary and a proof that it distinguishes them. The win is the proof: nothing is executed, sampled, or replayed, and no human reads the submission to decide whether it counts.

Status: proof-of-concept. The site is static, submissions open a GitHub issue, and a human decides. There is no Lean verifier behind it yet.

Layout

python3 tools/manifest.py          # rewrite the manifest
python3 tools/manifest.py --check  # fail if stale
python3 tools/ledger.py            # rewrite the ledger with scores and frontier
python3 tools/lint_challenges.py   # configs are complete
python3 tools/check_site.py        # the site can render what the tools generate

printf '%s' "$BODY" | python3 tools/verify.py spoc128    # one submission

CI

verify.yml runs on push and pull request: the --check gates, the config lint, the site check, and a battery of submissions the verifier must accept and must reject — a sorry, a native_decide, an unknown challenge, a zero advantage, a body with no Lean block. workflow_dispatch verifies one submission on demand without opening an issue.

submission.yml handles a verify: issue in two jobs. The first parses untrusted input and holds no write scopes; the second downloads its verdict and posts the comment. That split is lean-golf's and it is the reason an issue body cannot reach a token.

The submitter never writes the statement

This is the whole mechanism, and it is the same one trailofbits/lean-golf uses for proof golf. The verifier builds its own copy of Challenge.lean. A submission supplies only:

def strategy : game.Param → PFunDDS.DDE game.Query game.Response
def verdict  : List (game.Query × Option game.Response) → Bool
theorem attackWins : attack.Wins score.budget score.advantage

plus budget and advantage on the form. attack and score are assembled from those numbers in Challenge.lean, so a submission cannot spend a larger budget than it is scored for, or prove a weaker bound than it claims — not because we check, but because it never holds the pen on either object.

Four rejections a verifier makes without reading anything:

native_decide, maxHeartbeats and maxRecDepth are rejected too: a proof that only closes with a raised limit is a proof the verifier cannot afford.

Scoring

Nothing is fixed in advance. On a scheme nobody has studied, what advantage is reachable at what cost is the research question, so any target is a guess — and a target set too high scores a genuine 2⁻³⁰ distinguisher as zero. The board measures the result instead:

score = log₂( budget / advantage^e )

Queries per unit advantage; its log base two is the security level in bits the attack refutes. Lower is better. Understating your advantage raises the score, so there is nothing to gain by claiming less than you can prove.

e is per challenge and has no default. e = 2 for a decision game — an advantage α needs about α⁻² repetitions to amplify — and e = 1 for a search-flavoured one. Both conventions are in the literature and the inconsistency is known (Micciancio–Walter, On the Bit Security of Cryptographic Primitives), so a challenge states which it uses.

Par is the designer's own claim, taken from the specification, so no guess about attack difficulty appears anywhere. Under par is a break of the claim.

The frontier is the primary record: a result joins it when nothing else beats it on both queries and advantage at once. The bit score is the ranked column beside it, and two checked lemmas in the Lean layer (Score.workFactor_lt_of_dominates, Score.onFrontier_of_workFactor_min) guarantee the ranking never buries a result that wins on both axes.

Challenges

spoc128 — SpoC-128 as submitted to NIST LWC Round 2. Broken: three queries, advantage 1, 1.58 bits. load key n puts the nonce in the rate and tagInput XORs tagControl into the same rate, so tagInput (load key n) = load key (n ^^^ tagControl). One permutation input is reachable by two queries, and since the permutation is public and invertible, half of it leaks in a tag and half in a ciphertext block; join, invert, take the capacity, and that is the key.

spoc128-ds — the same mode with the four control bits reserved in the nonce, so n ^^^ tagControl is not a legal nonce. Open: no attack is known. The restriction lives in the type of a query, so the published attack is not merely unsuccessful here — it cannot be presented as an adversary at all (SpoC128DS.attack_second_query_illegal).

This is deliberately not a second copy of the mode. Hardening DDC.lean would mean a parallel model to keep in sync; restricting the query domain is one predicate, and every existing theorem about the mode still applies.

Nothing here claims the variant is secure. Closing one published route into a mode is not an argument that no other route exists — which is the point of putting it up.

Adding a challenge

Supply a Golf.Game in the Lean layer — a public parameter type, a query and response type, and the two worlds — then a config.json here. The generic layer lives in RandomSystems/Golf/Game.lean; RandomSystems/Golf/Instances/SpoC128/ is the worked example, and doubles as the check that the abstraction is faithful: its adequacy receipts are rfl and its reference submission is discharged by the existing attack_distinguishing_advantage with no restatement.

What this does not score

• Offline work, by decision. The adversary is a symbolic object and the board scores query complexity, the information-theoretic setting that indifferentiability and the PRP/PRF switching lemma already live in. A challenge needing computational feasibility must say so and pin a cost-bearing form.
• Amplification is assumed available: q/α^e is the cost of repeating an attack to confidence.
• Ties are not equivalences. The same bit level can hold very different results, which is why the frontier sits beside the ranking rather than being replaced by it.