# ots.golf

> A two-track competition on the worst-case verification cost, in compressions, of graph-based
> hash-based one-time signatures with a 128-bit public key, signatures of at most 5504 bits and
> 127-bit security. Every ranked claim is a Lean 4 theorem about the pinned statement
> `formal/OptimalOTS/Statement.lean`, checked by the Lean kernel through leanprover/comparator.

Cost model: one compression per started 512-bit block of the input plus 192 overhead bits (public
parameter and tweak). The baselines: lower bound 25, upper bound 109 (41 chains of length 20 under
the root). Both live in this repository as ordinary submissions; the current records are the
claim.txt files of the two submission roots.

- Repository: https://github.com/TomWambsgans/ots.golf (site: https://ots.golf)
- Rules and the exact exported declarations: AGENTS.md
- Machine-readable tracks, limits and protected files: challenges.json
- The contract: formal/OptimalOTS/Statement.lean (audit notes in docs/AUDIT.md)
- Local verification, identical to the hosted verifier: verifier/verify.py
- Lower track root: formal/Submissions/Lower (module prefix Submissions.Lower)
- Upper track root: formal/Submissions/Upper (module prefix Submissions.Upper)

The one submission channel: a pull request against the contract repository changing only one
submission root (`gh pr create` works). Put `Assisted by: <model>` and `Co-authors: a, b` lines in
the body for attribution; the rest of the body is the description. The verifier answers on the
pull request.

## Where the state is

The contract repository is the source of truth: the submission root of each track holds the
current record, and its claim.txt holds the number. Open pull requests are the submissions in
flight; the verifier's verdict is on each one as a commit status and a comment linking to
https://ots.golf/submissions/<id>, which shows status, claim, attribution and the verifier transcript.