Rules

A one-time signature (OTS) uses a key pair to sign one message securely. This competition is about hash-based OTS, whose security rests on a hash function alone. For examples, see Lamport signatures, which reveal selected secrets, and target-sum Winternitz signatures, which use hash chains.

We fix a budget for the public-key size, signature size, security, key generation and signing, and try to minimize the verification cost:

Fixed requirements and the verification objective

Parameter	Requirement
Public key	128 bits
Message	256 bits
Signature	At most 5,504 bits
Key generation	At most 220 compressions
Signing	At most 220 compressions
Security	127 bits
Verification	Minimize the worst-case cost, in compressions, RISC-V cycles or leanISA cycles

Every track requires a Lean-kernel-checked proof.

Upper bounds

Construct a provably secure hash-based OTS and prove an upper bound on its worst-case verification cost. Any oracle algorithm is allowed, as long as it satisfies the requirements above. Smaller claims are better.

• By compressions. The cost is the number of hash compressions.
• By RISC-V cycles. Implement the verifier in RISC-V, prove it computes exactly the Lean verifier, and bound the cycles of every execution, accepting or rejecting.
• By leanISA cycles. Implement the verifier in leanISA, prove it accepts exactly the valid signatures even with malicious hints, and bound the cycles of every accepting execution.

Lower bound

Prove that every secure whole-word DAG scheme needs at least the claimed worst-case verification cost, in compressions. Larger claims are better. This lower bound applies to the restricted class below; upper-bound constructions may use any admissible oracle algorithm.

All parties share one random oracle: every distinct bit string gets an independent uniform 256-bit answer. Hashing is the only cryptographic primitive.

A hash call costs one compression per started 512-bit block of its input: hashing a bit string x costs max(1, ⌈|x| / 512⌉) compressions.

A per-key public parameter, useful for multi-user security, costs (almost) nothing: a block-based hash can pad the parameter to a full block, absorb it once and cache the internal state, so every later call starts from that state for free (thanks Justin Drake for this idea).

The attacker sees the public key, queries the oracle at will, receives one signature on a message of its choice, and then outputs a forgery. If the whole experiment (key generation, signing, the attacker's queries and the final verification) costs at most B compressions, the attacker must win with probability below B / 2127.

Winning means strong unforgeability: the forgery is any accepted message-signature pair other than the one the signer produced. If signing failed, any accepted pair wins.

A scheme consists of three terminating oracle programs: key generation, signing and verification. Key generation and signing may use private randomness; verification is deterministic. Whenever honest signing returns a signature, verification accepts with probability one. Signing may fail, but only with probability at most 2⁻¹²⁸, for any message.

Signatures are bit strings. Every possible signer output has at most 5,504 bits, and verification rejects longer strings. A compression claim bounds the verifier's cost on every input, whether it accepts or rejects.

Verification itself costs at most 2²⁰ compressions on every input and every oracle-answer path, like key generation and signing. This is a requirement, not the score: the security budget is measured over the whole experiment, which ends with a verification, so an unbounded verifier would inflate the budget instead of resisting an attack. No honest verifier comes close to this cap.

Submit an OTS meeting the algorithm requirements above, together with a fixed RV64IM verifier. Prove that its execution implements the Lean specification: the same oracle computation and decision for every public key, message and raw signature bit string. Every execution must terminate, including malformed and rejected inputs.

The fixed program image must be strictly less than 1 MiB (1,048,576 bytes): four bytes per instruction plus all embedded data.

The claim bounds cycles on every execution, accepting or rejecting, for every input and oracle answer. Each ordinary instruction and the halt cost one cycle. The HASH call costs max(1, ⌈n / 512⌉) cycles for an n-bit input, with no additional instruction charge. It uses the same random oracle as the OTS security experiment.

Submit an OTS meeting the requirements above, fixed leanISA bytecode, a memory size, an honest prover's strategy for filling memory, and a step count. The prover supplies memory before execution; instructions check its contents without changing them.

• Faithful: the honest run reaches the halt address exactly when the Lean verifier accepts, for every public key, message and signature bit string.
• Sound: no malicious memory contents or allowed memory size can make the program accept an input the Lean verifier rejects.

The bytecode has at most 262,144 instructions and no JUMP in its halt slot. Memory sizes range from 2¹⁶ to 2³² words. The announced memory cells plus bytecode slots must total fewer than 1,048,576.

Bound cycles on every completing execution, for all allowed memory sizes, contents and step counts. Rejected inputs have no completing execution and incur no score. Instructions cost one cycle; BLAKE2S costs ten. Add a fixed 120 cycles for public-input binding. Scores exclude memory setup and finalization and are not directly comparable with RISC-V.

Both proofs use the shared random oracle. BLAKE2S queries it on 896 bits: 256 chaining bits, a 512-bit block and 128 metadata bits. This models hashing rather than executing RFC 7693 BLAKE2s. Full specification.

The scheme is described by a public directed acyclic graph (DAG) built from whole 128-bit words. Each node holds one value, a bit string of fixed length, and comes in one of three kinds: a source holds an independent uniform 128-bit word, a hash node holds the 256-bit hash of its single parent's value, and a deterministic node outputs a fixed public 128-bit word, selects the fixed low or high half directly from a hash output, or concatenates complete earlier values. Concatenations may reorder, repeat, group or be empty. Parents come before children, and a value may feed several nodes. Key generation draws the sources, evaluates every node once and stores all the values; the public key is the low 128 bits of the root hash.

A signature reveals a cut: stored values meeting every source-to-root path, excluding the root. Verification follows all declared parent edges backwards to the cut, then evaluates required nodes forwards, once each.

1. Select a cut. The scheme supplies 2115 indexed cuts. Read the low 128 bits of H(message ‖ nonce) as an integer; it is valid below 2115. Try up to 220 uniformly sampled 128-bit nonces without replacement, stopping at the first valid index or failing.
2. Reveal. Send the nonce and the cut's node values in node order, with at most 5,376 payload bits.
3. Verify. Reject invalid indices or wrong payload lengths; otherwise reconstruct the root and compare its low 128 bits with the public key.

The score is the maximum over all indexed cuts: one compression for the message-and-nonce query, plus the costs of reconstructed hash nodes.

Submit an upper-bound construction or a lower-bound proof for whole-word DAGs.

1. Read the notes of earlier submissions: their ideas, results and dead ends.
2. Fork the submissions repository and follow its setup instructions. Create or change one submission root: formal/Submissions/LowerGenerality1/, formal/Submissions/UpperCompressions/, formal/Submissions/UpperRiscv/ or formal/Submissions/UpperLeanIsa/.
3. Put your claim in claim.txt and export the required declarations from Solution.lean. Add a NOTES.md beside them: the idea, the result, what did not work and what you would try next.
4. Run python3 .contract/verifier/verify.py lower-generality-1 --source . (or upper-compressions, upper-riscv or upper-leanisa), then open a pull request from your fork's proof branch to leanEthereum/ots.golf-submissions, with base branch main. Its author and description supply attribution; optional Assisted by: and Co-authors: lines credit collaborators. Each new head is rechecked. A verified improvement becomes the record.

Submissions that do not beat the record are welcome too, and so are attempts that fail: their notes join the journal, and every checked head stays fetchable from the submissions repository, so others can build on it.

Use a flat root: identifier-named .lean files, claim.txt, optional README.md and NOTES.md, and required Solution.lean. The claim is an integer from zero to 1000000, without leading zeros and with at most one trailing newline. Use the pinned toolchain and dependencies; submissions cannot alter protected definitions.

In every source header, use one ordinary import Module.Name per line, with dot-separated, unquoted ASCII identifiers. Header imports may name Mathlib, VCVio, permitted contract modules and siblings, as specified in the submission specification. Dependencies of permitted modules are available transitively. This source-header restriction does not restrict runtime module loads by Lean metaprograms or certify where a proof was obtained. Every exported proof must pass statement comparison, axiom checks and kernel replay.

The verifier checks the exact claim and exported declarations. No sorry or extra axioms: only propext, Quot.sound, Classical.choice. native_decide introduces an unpermitted axiom. Limits: 200 files, 8 MiB per file, 16 MiB total, 20 minutes, 24 GiB and no network. Combined standard output and standard error, including compiler and verifier messages, must stay within 4 MiB (4,194,304 bytes). Output beyond this limit is truncated and can cause rejection even if the proof is correct.

The core repository defines the model and verifier: constants and oracle, generic interface and statements, DAG contract, whole-word condition, verifier configuration and submission specification.