ots.golf submissions

Before preparing a proof, read the rules, also available as plain text. Open proof PRs from your fork's branch into leanEthereum/ots.golf-submissions, base branch main. With GitHub CLI, set the destination explicitly: gh pr create --repo leanEthereum/ots.golf-submissions --base main --head YOUR_LOGIN:YOUR_BRANCH (replace the login and branch placeholders).

Proof submissions for ots.golf. A submission is a pull request to this repository that creates or changes one submission root below. Pull requests are verified, never merged or closed: a verified improvement becomes the record after its verdict is recorded on GitHub. The bot then commits only that checked root and its records.json entry to main, preserving other tracks and repository files. main contains the four current record proof roots; the registry links each claim to its checked commit, PR and trusted core. When a maintainer ports an existing proof to updated rules, record_origin preserves the original record holder, submission and date; the certificate fields identify the adapted checked source. A proof port does not transfer credit or set a new record.

The hosted service retains the admitted commit under refs/tags/ots-source/<submission-id> and freezes attribution in a pending receipt before verification starts. The submission page's Code link opens the submitted folder on GitHub at that exact checked SHA. The model, verifier and website are developed in leanEthereum/ots.golf-dev.

Rules: read them on ots.golf/rules. The precise specification (exports, root rules, limits, attribution and records) is AGENTS.md in the pinned core, also available locally as .contract/AGENTS.md.

Track	Folder	Check it with
Upper bound · compressions	formal/Submissions/UpperCompressions/	.contract/verifier/verify.py upper-compressions --source .
Upper bound · RISC-V cycles	formal/Submissions/UpperRiscv/	.contract/verifier/verify.py upper-riscv --source .
Upper bound · leanISA cycles	formal/Submissions/UpperLeanIsa/	.contract/verifier/verify.py upper-leanisa --source .
Lower bound · Whole-word DAGs	formal/Submissions/LowerGenerality1/	.contract/verifier/verify.py lower-generality-1 --source .

Protected source tags and verdict comments remain the historical authority; main is the convenient current-record snapshot. Its publication retries without rerunning the proof. Optional source ZIPs are rebuildable caches, with any recorded digest checked during recovery. pull/<N>/head moves, so historical links use the original checked SHA retained by its source tag. The serialized admission receipt is capped at 48 KiB; put longer prose in NOTES.md. Original verification logs are disposable. Before starting, read the notes journal: the ideas, results and dead ends of every checked submission, newest first, in plain Markdown.

Check your proof

Fork this repository and clone your fork with --recurse-submodules (for an existing clone, run git submodule update --init --recursive). Install elan, then, from the root of the checkout:

.contract/verifier/setup_tools.sh
(cd .contract/formal && lake exe cache get && lake build OptimalOTS)
python3 .contract/verifier/verify.py upper-compressions --source .   # see the table for other tracks

Change only your chosen track's root; do not edit records.json, another track or .contract in a proof PR. A PR based on an older main remains eligible: later base-branch record updates do not count as changes made by that PR. Each root must remain self-contained under the import rules.

New RISC-V proof PRs also export OptimalOTS.Challenge.UpperRiscv.image_size, proving submission.image.byteSize < 1048576: four bytes per instruction plus embedded-data bytes, strictly below 1 MiB. When extending a pre-rule record snapshot, add this theorem to Solution.lean. Historical snapshots retain their checked source; their image sizes were separately audited without changing their scores or attribution.

The verifier checks only your submission root from the working tree against the trusted contract. macOS verification is for trusted local development; Linux requires the isolation described in the deployment guide.

Contract pin

.contract is a Git submodule of the core repository, pinned to commit 20c5b5d061fb41235ff6e20c378e0f256d83525e (contract ID d3684f44469781b7c19d3f540e0b780f17ff5090595377445faeea0fc425279e). Maintainers update the pin when the contract changes; the hosted verifier uses its own trusted checkout.

Local website

The core submodule includes the website and its fictional demo leaderboard:

cd .contract/service
uv sync --frozen
OTS_PHONY=1 ./run-local.sh        # http://localhost:8000

The default OTS_PHONY=0 shows only real submissions; 1 opts into the demo entries.

RISC-V profiles

Maintainers can attach a measured per-instruction table to a checked RISC-V submission by editing riscv-profiles.json on main. See the profile guide. These optional owner profiles do not affect verification or scores and are separate from proof PRs.

Signature diagrams

Maintainers can attach a drawing to either upper-bound track through signature-diagrams.json and an SVG in signature-diagrams/. See the diagram guide. Drawings are optional and pinned to exact checked submissions.

Credits

The competition and chart were inspired by better.codes, zk.golf and yukon.org. License: Apache 2.0.