Rules

1. One-time signatures

A signature scheme is three algorithms. Key generation makes a secret key sk and a public key pk. Signing turns sk and a message m into a signature σ. Verification accepts or rejects (pk, m, σ). The scheme is one-time when a key signs a single message: an attacker who sees pk and one signature, on a message of its choice, must not be able to produce any other pair that verifies.

One key, one message. The verifier sees only pk, m and σ.

One-time signatures are the building block of hash-based signatures such as XMSS and SPHINCS+: a Merkle tree holds many one-time keys, and every verification pays for the one-time part. That cost is what this competition minimises.

A hash-based one-time signature uses nothing but a hash function. Lamport hashes secret strings and reveals one per message bit; Winternitz replaces the secrets of a group of message bits by one hash chain and reveals the value at the position the message dictates. Both follow one pattern: key generation runs a fixed computation on secret random inputs, a signature reveals a few intermediate values, and the verifier recomputes the final hash and compares it with the public key.

Lamport and Winternitz as graphs, with one signature lit. revealed recomputed by the verifier never touched

2. The hash function and its price

The only cryptographic tool is a hash function H, modelled as a random oracle: each new query, a label and an input, receives an independent uniform 256-bit answer, and a repeated query receives the same answer. Signer, verifier and attacker learn H only by querying it. A query on an input u costs

c(u) = ⌈ (|u| + 192) / 512 ⌉ compressions.

Hash functions absorb their input in 512-bit blocks, one call of the compression function per block, and that call is the unit of work in software, in hardware and in a SNARK circuit. The 192 extra bits are what a deployed tweakable hash prepends to every input, a 128-bit public parameter and a 64-bit tweak, and the model charges for them without representing them: its labels play the tweak's role. So a chain step over 128 bits costs one compression, the index hash over message and nonce costs two, and the root of the baseline scheme, over 41 chain ends, costs eleven.

Everything else is free, for everyone: concatenating, splitting, comparing, drawing randomness. Only queries to H count, and nothing else bounds the attacker's computation.

Four inputs against 512-bit blocks. The hatched prefix is the overhead of every query; the cost is the number of blocks started.

3. A scheme is a graph of computations

A scheme is a fixed, public, finite directed acyclic graph. Each node holds a bit string of a fixed length, computed from its parents' values, and is one of three kinds.

Secret sources have no parents and hold uniformly random strings, of any length.
Deterministic nodes apply any public function to any number of parents and produce any length: concatenate, select bits, split, combine, look up a table, anything computable without H. They cost nothing.
Hash nodes have one parent and their own label. Their value is H(label, parent), 256 bits, at cost c of the parent's length. The parent may be a concatenation of many values, so a hash node absorbs inputs of any size, at a price.

A value may feed any number of nodes. One hash node is designated the root. Key generation samples the sources, evaluates the graph in order, within 1024 compressions, keeps every value as the secret key, and publishes the first 128 bits of the root as pk.

Bits on the move. Each bar is a value, as wide as it is long; the ribbons carry slices of it upwards. Deterministic nodes split, select, reuse and concatenate slices for free, and each H compresses whatever reaches it into 256 fresh bits at the cost written beside it. The first 128 bits of the root are the public key.

A small graph with every freedom of the model. It is not a tree: two values feed two nodes each, and three deterministic nodes gather two or three values. Every hash node carries its cost.

Lamport, Winternitz, chains under trees: the hash-based one-time signatures of the literature are such graphs, and so is anything else built from a hash function whose signatures consist of node values.

4. Signing reveals a cut

Besides the graph, a scheme fixes M = 2¹¹⁵ disclosure sets A₀, …, A_M−1. Each is a cut: a set of nodes that excludes the root and meets every path from a secret source to the root. To sign m, the signer draws a 256-bit nonce η, reads the index i from the first 128 bits of H(enc, m ‖ η), and tries fresh nonces until i < M: about 2¹³ trials on average and at most 2²¹, after which signing fails. The signature is η followed by the values of A_i in a fixed order: at most 5248 bits of values, so at most 5504 bits in all. The message chooses what is revealed; the signer computes nothing new.

The graph above with one disclosure set lit. Every path from a source to the root crosses a revealed value, the root stays hidden, and the number beside each recomputed hash node is its cost.

5. Verification and the score

The verifier recomputes i from m and η, two compressions, rejects if i ≥ M or if the revealed string has the wrong length, splits it into the values of A_i, evaluates every node between the cut and the root, and accepts if the first 128 bits of the recomputed root equal pk. With E_i the hash nodes it evaluates, the signature of index i costs

C_i = 2 + Σ_{g ∈ E_i} c_g compressions,

and the score of a scheme is max_i C_i, its most expensive signature. The signature in the figure costs 2 + 8 = 10. In the baseline scheme, 41 chains of length 20 hashed together into the root, every signature recomputes 96 chain hashes and the 11-compression root: 2 + 96 + 11 = 109.

6. Security

The attacker receives pk, queries H at will, asks for one signature on a message of its choice, and outputs a message and a signature. It wins if the pair verifies and differs from the one it received. Let B bound the compressions spent in the whole experiment on every run, key generation, signing and the final verification included. The scheme is secure when every attacker wins with probability below B / 2¹²⁷: a forgery costs about 2¹²⁷ compressions per unit of success probability. This is Scheme.Secure in the statement, strong unforgeability. The weak form, Scheme.WeaklySecure, counts only forgeries on a message other than the signed one; every secure scheme is weakly secure.

The forgery experiment. Every query to H, by either party, counts towards B; the attacker's other computation is unbounded.

7. Two tracks, one number

Between the two records lies the answer: the least worst-case verification cost of a secure scheme with these parameters. The upper track attacks it from above: a scheme, a proof that it is secure, and a proof that every signature verifies within the claimed cost. Smaller wins. The lower track attacks it from below: a proof that every weakly secure scheme, and so every secure one, has a signature at least that expensive. Larger wins. Both are Lean theorems about the same pinned statement, formal/OptimalOTS/Statement.lean, checked by the kernel.

Parameters

Fixed in paperParams; a submission cannot change them.

Hash output	256 bits
Block, and overhead per query	512 bits, and 192 bits
Public key	128 bits, the first bits of the root
Message, nonce	256 bits each; the index is the first 128 bits of `H(enc, m ‖ η)`
Revealed bits per signature	at most 5248, so signatures of at most 5504 bits
Key generation	at most 1024 compressions
Disclosure sets	`2¹¹⁵`
Signing trials	at most `2²¹` nonces
Security	forging with cost `B` succeeds with probability below `B / 2¹²⁷`

How to play

Fork the contract repository and edit one submission root: formal/Submissions/Lower/ or formal/Submissions/Upper/.
Export the track's declarations, put your claim in claim.txt, and check locally with verifier/verify.py.
Open a pull request. The verifier fetches your commit, keeps only the submission root, and answers on the pull request. A verified claim that strictly beats the record is merged; the merge is the promotion.

The repository is the source of truth: each submission root holds the current record.

Submission rules

Layout

formal/                      the Lean project (lake root)
  OptimalOTS/Statement.lean  the contract: Scheme, Secure, verifyCost, paperParams
  OptimalOTS/Challenge/      stubs (*.lean.in), rendered with your claim
  Submissions/Lower/         lower-track root; baseline: the paper's proof, claim 25
  Submissions/Upper/         upper-track root; baseline: 41 flat chains, claim 109
verifier/                    checks, contract pin, comparator configs, verify.py
challenges.json              tracks, limits, protected files

Protected files (listed in challenges.json, pinned in verifier/protected.sha256) always come from the contract, never from a submission. A submission is the content of one submission root and nothing else.

What a submission exports

The verifier renders the track's stub with your claim and compares your declarations against it. Names and statements must match exactly; copy them from the rendered stub.

Lower track (formal/Submissions/Lower/, larger is better; a record needs claim ≥ record + 1):

theorem OptimalOTS.Challenge.Lower.candidate :
    VerificationLowerBound paperParams <claim> := ...

VerificationLowerBound quantifies over WeaklySecure schemes (forgeries on a new message only), a larger class than the Secure schemes of the upper track, so a lower bound also covers malleable schemes. The attacker of a lower-bound proof must therefore forge on a message other than the signed one.

Upper track (formal/Submissions/Upper/, smaller is better; a record needs claim ≤ record − 1):

noncomputable def OptimalOTS.Challenge.Upper.scheme : Scheme paperParams := ...
theorem OptimalOTS.Challenge.Upper.secure : scheme.Secure := ...
theorem OptimalOTS.Challenge.Upper.cost :
    ∀ i : Fin paperParams.numSets, scheme.verifyCost i ≤ <claim> := ...

scheme is a definition hole: any term of type Scheme paperParams is admissible, and the two theorems pin it down. Describe the scheme in the pull request; the leaderboard shows the description.

Rules for the submission root

Flat. Only .lean files named as identifiers, claim.txt, and optionally README.md. No subdirectories. Solution.lean is required: it is the module the verifier exports from.
Imports. Only Mathlib, VCVio, OptimalOTS.Statement, and sibling files of the same root as Submissions.<Track>.<File>. Nothing else: not OptimalOTS, not the stubs, not the other track.
Claim. claim.txt holds one non-negative integer without leading zeros, at most 1,000,000, with at most one trailing newline. It is rendered into the statement the kernel checks, so it cannot lie.
Axioms. The exported declarations may depend only on propext, Quot.sound and Classical.choice. native_decide adds Lean.ofReduceBool and is refused; so is sorry.
Limits. 200 files, 8 MiB per file, 16 MiB per root. Verification: 20 minutes of wall clock, 24 GiB of memory, no network, Mathlib and VCVio prebuilt. The baseline proofs verify in under three minutes on 16 cores; a decide over large naturals is the usual way to blow the budget.
Toolchain. Exactly formal/lean-toolchain and formal/lake-manifest.json. Both are protected.

Check locally before submitting

verifier/setup_tools.sh                        # once
cd formal && lake exe cache get && lake build OptimalOTS Submissions  # once
cd ..
python3 verifier/check_submission.py lower     # policy checks
python3 verifier/verify.py lower --source .    # the full pipeline

setup_tools.sh installs comparator and lean4export (and landrun on Linux); the lake build line fetches Mathlib and builds VCVio, the contract and the two baselines. check_submission.py runs the policy checks: flat root, imports, sizes, claim. verify.py copies the trusted tree, lays your submission root over it, attaches a fresh clone of the warm .lake, renders the stub, and runs comparator under the contract's limits; on macOS it runs unsandboxed, for development only. A verified result locally is what the hosted verifier will reproduce.

Submitting

There is one way in: a pull request against the contract repository that changes only your track's submission root. The verifier fetches the head commit, keeps only that root, verifies it on the trusted tree, and answers on the pull request with a commit status and a comment linking to the submission page. Pushing to the pull request re-queues its new head.

Attribution comes from the pull request: its author, plus two optional lines in the body (the template has them):

Assisted by: Claude Fable 5.1 max
Co-authors: alice, bob

The rest of the body is the public description. A verified claim that strictly beats the record is merged, and the merge is the promotion: the submission root in the repository is always the current record. Other verified submissions appear on their solver's page, and their pull requests are closed.

Limits in force

Wall clock	20 min
Memory	24 GiB
Files per root	200
Per file / per root	8 MiB / 16 MiB
Axioms	`propext`, `Quot.sound`, `Classical.choice`