How cheaply can a hash-based one-time signature be verified?
ots.golf is a competition in which every claim is a Lean proof about a pinned contract. This repository, ots.golf-dev, is the core: the Lean model, the verifier and the website. It holds no track proofs; those are submitted as pull requests to ots.golf-submissions.
Rules: read them on ots.golf/rules. AGENTS.md is the precise specification: exact exports, submission-root rules, limits and the submission workflow.
| Track | Folder | Check it with |
|---|---|---|
| Upper bound · compressions | formal/Submissions/UpperCompressions/ |
verify.py upper-compressions |
| Upper bound · RISC-V cycles | formal/Submissions/UpperRiscv/ |
verify.py upper-riscv |
| Upper bound · leanISA cycles | formal/Submissions/UpperLeanIsa/ |
verify.py upper-leanisa |
| Lower bound · Whole-word DAGs | formal/Submissions/LowerGenerality1/ |
verify.py lower-generality-1 |
Roots live at formal/Submissions/<Root>/ in the submissions repository. Current records are
on ots.golf. The submissions repository's main carries the four current record
roots and records.json, which links each claim to its original checked commit, PR and trusted
core. After publishing a new record's verdict, the bot copies its checked root into main with a
separate commit; proof PRs are never merged or closed. Each submission's Code link opens its
folder on GitHub at the original checked SHA, independent of later main updates.
Build the contract and check a submission root from a submissions checkout next to this one:
verifier/setup_tools.sh
(cd formal && lake exe cache get && lake build OptimalOTS && lake env lean scripts/check-axioms.lean)
python3 verifier/verify.py lower-generality-1 --source ../ots.golf-submissionsverify.py takes only the track's root from --source; the contract and tooling come from this
checkout. macOS verification runs unsandboxed, for trusted local development; hosted verification
requires the Linux isolation in the deployment guide.
For optional local website development, opt into the committed demo fixtures:
cd service
uv sync --frozen
OTS_PHONY=1 ./run-local.sh # http://localhost:8000Maintainer updates follow commit, push, then deployment to h2; no localhost preview is required.
Production shows real submissions only (OTS_PHONY=0). GitHub retains each admitted commit under
refs/tags/ots-source/<submission-id> and stores frozen receipt/verdict comments. The server is
disposable: python -m app.rebuild restores metadata; --sources also rebuilds optional source ZIPs
without rechecking historical proofs. Retained tags and verdict comments remain the history
authority; the current-record snapshot on submissions main can be republished from checked
sources. GitHub retries do not rerun a finished proof. Original logs are disposable. See the
deployment guide for the credentialed
rebuild command, source-tag protection and launch checks.
Maintainers can add optional signature diagrams
and RISC-V instruction tables by committing owner
metadata to submissions main. They are pinned to exact checked submissions and refresh automatically.
| Path | Contents |
|---|---|
AGENTS.md |
submission specification |
challenges.json |
track metadata, limits, protected files |
formal/OptimalOTS/ |
the contract: Model.lean, Dag.lean, WholeWords.lean, OracleAlgorithm.lean, Riscv.lean, RiscvMachine.lean, and the challenge stubs in Challenge/ |
formal/Witnesses/ |
internal maintainer check that the whole-word class is non-empty (lake build Witnesses); not a track |
verifier/ |
verify.py, policy checks, contract pin, comparator configs |
service/ |
website and hosted verifier; deployment |
docs/ |
proof guides, contract audit, repository setup |
tools/ |
numerical research tools, repository checks, submissions-repo preparation |
See repository setup for how the core and submissions repositories fit together.
The competition and chart were inspired by better.codes, zk.golf and yukon.org. License: Apache 2.0.