Autoresearch competition · draft rules for review
An open search for stateless hash-based signatures for Ethereum accounts, with Lean proofs of security in the classical, pure random-oracle model.
Stage 1 is academic research; Stage 2 is the Ethereum selection. Academic research includes one-time and few-time signatures, encodings, authentication structures, composition and complete constructions. Stage 2 evaluates complete stateless account signatures against every deployment gate. Improving a component does not automatically improve the resulting signature scheme: authentication paths, key derivation, domain separation and serialization must be included when evaluating the complete construction.
The leanSPHINCS repository contains the protected pure-ROM statement, a working local verification harness and experimental OTS foundations. The statement enforces a 32-byte public-key cap, exact signature size, weighted verification work, total-query security floors and same-scheme lifetime decay. No complete OTS security certificate or accepted SPHINCS⁻ baseline #0 exists yet. Full-program metering, signing/keygen budget certificates, external audit and registered verification remain launch work. Local receipts are unranked; product scores are diagnostic and confer no deployment eligibility.
Workstream plan · Implementation contract · Harness evidence and launch gates
Which signature should a quantum-resistant Ethereum account use? Accounts need keys that can be restored and used on multiple devices, bounded signing latency, small transmitted signatures and economical verification. This competition explores that execution-layer design space. It complements leanSig on the consensus layer; it does not select Ethereum's consensus signature or decide protocol adoption.
SPHINCS⁻ motivates the full-scheme baseline, but the search is not restricted to its construction. Hash chains are not assumed optimal. Public encodings and algebraic computations are allowed if the complete security argument is proved in the pure ROM and their actual costs are accounted for.
Human researchers and autonomous agents work against the same pinned statement. A compiler can check a formal theorem; it cannot establish that our chosen game models the intended application or that a cost profile predicts deployment performance. Those modeling choices require review before launch and before adoption.
The planned competition uses a public, cumulative frontier and reproducible verification, drawing on better.codes' protected-target harness. Each submission supplies algorithms and a Lean proof of security in the pinned pure ROM. The pipeline checks:
Numerical ranking is automatic; research credit is human-curated. Organizers may credit useful lemmas, attacks, negative results and lower bounds separately, with reasons and the model/family to which each result applies. A checked impossibility theorem does not make its relevance a machine-decided question. These credits do not change a submission's numerical score.
The harness needs an external audit before launch and a rules-exploit reporting process. The zk.golf launch discussion illustrates why carefully specifying the optimization target matters. Proof checking is not a substitute for reviewing that specification. Human review remains required before any award or adoption.
For both stages, |σ| is the complete signature size in bytes and V is verification work in the selected profile. Their product has byte × verification-work units. It measures the joint size/work trade-off: halving signature size offsets doubling verification work. This returns to the original objective and supports exploration of size/verification trade-offs.
No bandwidth price or conversion coefficient is required. The scoring rule and meter are organizer-owned. Retain both coordinates and the full Pareto frontier alongside the product: one scalar ordering does not describe every nondominated trade-off. Different security games or meters are not directly comparable. Product scores are research metrics; deployment still requires every eligibility gate.
Signing and key generation are eligibility constraints. The complete account profile sets normal latency targets of 1.5 s signing, 1 minute keygen: the probability of exceeding either target must be at most 2−40 per operation, under the game specified in R9. Exceptionally unlucky runs may continue up to the absolute worst-case caps of 2 minutes signing and 6 minutes keygen. Those absolute limits admit no overrun allowance. Working RAM remains bounded by 64 KiB on every path. Stage 1 component budgets must be stated for each experiment; the full account budget is not automatically assigned independently to every component.
The academic hash-work view and full-program execution views remain separate. A Reed–Solomon encoding can improve hash work while adding substantial field arithmetic. That is useful research evidence, not a demonstrated latency improvement; the execution profile must charge that arithmetic. Preserve the frontier so the price and profile can be revisited without discarding useful constructions.
These rules define the intended Stage 2 target. The protected statement implements the mathematical clauses described below, but the execution and wallet certificates remain unfinished. Stage 1 has separately pinned component or construction games (§7), not an implicit claim that a one-time signature satisfies every rule here.
A submission instantiates a protected signature-scheme structure with Keygen() → (pk, sk), Sign(sk, m) → σ or ⊥ and Verify(pk, m, σ) → 0 or 1. There is no mutable state or epoch argument/output. Key generation and signing may use fresh randomness; verification is deterministic given the shared oracle.
All cryptographic security must be proved in the pure ROM: one arbitrary-byte-input, 32-byte-output random oracle, plus independent uniform sampling. No additional cryptographic assumptions, conjectural reductions or scheme-security hypotheses are admissible. Polynomial and Reed–Solomon coding are permitted; a family name is neither an exemption nor a reason for rejection. Domain separation is part of the actual oracle input and proof.
Prove SUF-CMA: the adversary cannot produce a new valid message/signature pair, including a different valid signature on an already-signed message. Only an exact successful signing response is a replay. Every signing request counts, including repeats and responses returning ⊥.
Let qH bound raw hash calls across the whole experiment: key generation, adversarial hashing, honest signing and final forgery verification. It excludes uniform sampling. Let qS bound signing requests and define Q = qH + qS. These are pathwise query bounds, not expected costs. Raw hash queries are distinct from the input-weighted verification meter.
For the declared bound B, prove AdvSUF-CMA ≤ B(Q, qS). At up to 220 signing requests, certify B(Q, 220) ≤ Q / 2124 for 1 ≤ Q ≤ 2124. This is the competition's concrete 124-bit classical work/probability floor, not a NIST-category or quantum-security certificate.
This security condition must be accompanied by the resource bounds in R9. If key generation always makes 2128 hash queries, every admissible experiment has Q ≥ 2128, so even Adv ≤ Q / 2128 follows from Adv ≤ 1. Such query padding does not establish useful security. The runtime and raw-query caps must exclude it in key generation, signing and verification.
B(Q, s) is a fixed explicit sum of 1–128 monomials (num / den) * Q^a * s^b / 2^k, with positive rational coefficients and natural exponents. The list length, coefficients and exponents must not depend on Q or s. In particular, a sum whose number of terms scales with a query budget is not this format.
All constants remain in the bound. There is no constants-dropping eligibility rule. For a signing cap S and bit threshold b, the protected certificate checks B(1, S) ≤ 2^-b and B(2^b, S) ≤ 1. Convexity proves the required inequality throughout the interval; nonnegative coefficients make the fixed signing cap conservative for smaller request budgets.
This fixed-cap certificate also checks numerical points with Q < S, even though a run using S signing requests cannot have total budget Q < S. It is a conservative sufficient gate, not a claim to compute the tightest possible security level over feasible budget pairs. Arithmetic and the format limits are exact, not floating-point estimates.
The same scheme, parameters and bound B must retain a 100-bit floor at 232 signing requests: B(Q, 232) ≤ Q / 2100 for 1 ≤ Q ≤ 2100. The security theorem itself must cover that extended request range. Evaluating a polynomial outside a theorem's scope is insufficient; a reparameterized scheme cannot supply this certificate.
A QROM theorem is not an entry requirement. A classical ROM proof does not establish a generic “classical bits divided by two” quantum guarantee. Further quantum analysis is desirable evidence for deployment review, not a promised post-competition formalization by the organizers.
The serialized public key is at most 32 bytes on every key-generation path. A construction may hash a larger key and reveal it inside each signature, but must include those bytes, verification work and the domain-separated commitment's security reduction. A generic 256-bit collision allowance is of order Q² / 2256; it is not a free transformation or an automatically accepted bound.
Provide an end-to-end Lean proof for the protected scheme and pure-ROM game. Internal modular reductions are welcome, but all their premises must be discharged in that final theorem. There are no separate assumption-registry or proof-style exceptions. The theorem and algorithm axiom closures may use only propext, Classical.choice and Quot.sound; no sorry, conjectural axioms or unproved cryptographic premises.
Messages are 32-byte digests. Public keys and signatures are actual byte strings. Every successful signature has exactly the declared length, including padding, and verifies with probability one in the fresh key-generation/signing experiment. Separately prove Pr[Sign returns ⊥] ≤ 2−128 for each fixed message, over fresh key generation, signing randomness and their shared ROM. A 2−256 certificate also qualifies.
Additionally, prove adaptive availability: at every permitted request position i, the unconditional probability that request i occurs and returns ⊥ is at most 2−128. Messages may depend on the public key, earlier responses and the shared ROM. Average over key generation, the shared ROM and all participant randomness; do not condition on a key or transcript. An absent position is not a failure. This holds both for at most 220 requests with Q ≤ 2124 and for at most 232 requests with Q ≤ 2100. Here Q counts keygen, participant and honest-signing raw hash calls plus all signing requests, including repeated and failed requests; final forgery verification is excluded from this availability interaction. The fresh-key, fixed-message certificate remains an additional obligation.
The lifetime union bound for 232 requests is at most 2−96, not 2−128. Worst-case failure analysis is separate from work metering. Failed attempts must still fit the absolute resource caps. Exceeding the normal latency target is not itself a signing failure.
Immutable precomputation may be part of sk and must be charged to key generation and storage. There is no required separate cache or presign channel. Public disclosure or adversarial replacement of auxiliary data would require an explicitly modeled extension; it is not covered merely by calling that data non-secret.
Every eligible complete scheme must prove Pr[T_keygen > 60 s] ≤ 2^-40 and Pr[T_sign > 1.5 s] ≤ 2^-40 on the reference execution profile. A slow run may continue up to the absolute limits of 120 s signing and 360 s keygen. Crossing the normal latency target does not require aborting the operation.
The keygen probability is over fresh randomness and the shared ROM. The signing bound must cover each request position under permitted adaptive message selection, with probability over key generation, the shared ROM and execution randomness. Averaging over random messages is insufficient. The exact performance game and adversarial query budgets are to be pinned before ranking. The allowance is per operation: a proved per-position bound gives at most min(1, N · 2−40) probability of any late signature in N requests by a union bound, without assuming independence. At 220 requests this is 2−20; at 232 requests it is 2−8 (1/256), not a lifetime 2−40 guarantee.
Absolute runtime and raw-query caps still apply on every path, including exceptionally slow paths: T_keygen ≤ 360 s and T_sign ≤ 120 s, with no probabilistic exception. Keygen must return a usable key within its absolute cap; signing must return a signature or explicit failure within its absolute cap for every generated secret key and every message. Working RAM is at most 64 KiB on every path. The late-run allowance does not permit unbounded work or a rare 2128-query branch: the current security query bound is pathwise, so even such a rare branch could make it vacuous.
Charge all setup and precomputation required to produce the usable key, and all work performed before a signing request returns: hashing, randomness handling, encoding, finite-field and integer arithmetic, memory access, authentication and every retry, including failed attempts. Moving setup outside the named keygen function does not exempt it. Expected runtime or sample averages alone do not establish the tail-probability guarantee.
Late completion, signing failure and forgery are separate events. A late signature must still be valid. Any failure caused by reaching the absolute timeout must be included in the R8 failure probability, which remains at most 2−128 in its stated experiment. The 2−40 latency allowance cannot be substituted for that bound or used to discard slow executions from the security proof.
Every ranked Stage 1 profile must also fix its latency guarantees and absolute budgets before admitting entries. Profiles must cap raw oracle calls by key generation, each signing invocation and verification, including repeated and empty-input calls, and keep total honest work within the nontrivial security ranges of R2/R4 or the component's pinned game. This requirement also applies to academic hash-work profiles, where a zero-length input has zero weighted cost.
The signing and keygen absolute time limits are fixed above. Reference hardware calibration, raw-query caps, persistent secret/precomputation storage limits and the verification execution cap are to be pinned. A fixed conversion from abstract hash units to seconds cannot establish the time guarantees. There is no separate free 4 KiB cache allowance.
A submission without the required resource certificates is ineligible for ranking or promotion. These resource gates are not enforced by the current statement/harness; implementing their binding to the complete executable and Lean scheme is required before opening submissions. Passing the current mathematical claim alone cannot certify competition eligibility.
Deployment eligibility is blocked in this release. Organizer-owned resource profiles must calibrate reference execution, verification limits, raw keygen/sign/verify query caps, persistent secret and precomputation storage, and executable size. Unset values or absent certificate validators fail closed. Execution evidence must bind the submitted algorithms and executable, covering malformed-input rejection, parsing, arithmetic, randomness handling, retries and setup. Raw-query bounds must cover every structural response path, including impossible ROM responses; ROM-consistent runtime measurements alone do not suffice. Count serialized secret/precomputation storage and document key restoration; the 64 KiB RAM cap establishes neither.
Side-channel eligibility requires independently reviewed implementation evidence under a stated timing/memory-access leakage model, bound to the executable and resource profile. This is not a formal noninterference theorem. Executable resource validation remains unimplemented.
This is an explanatory summary, not Lean source. The normative implemented structure is SchemeClaim; it also includes the correctness, failure, size and verification obligations above.
for the same scheme S and fixed bound B:
for every adversary with raw whole-game hash budget qH
and signing-request budget qS ≤ 2^32:
Adv_SUFCMA(S, A) ≤ B(qH + qS, qS)
for every 1 ≤ Q ≤ 2^124: B(Q, 2^20) ≤ Q / 2^124
for every 1 ≤ Q ≤ 2^100: B(Q, 2^32) ≤ Q / 2^100
publicKeyBytes ≤ 32
successfulSignatureBytes = declaredSigma
verificationWork ≤ declaredHVerify // malformed inputs included
correctnessOnSuccess
freshKeyFixedMessageFailureProbability ≤ 2^-128Eligibility additionally requires the R9 certificates for the same implementation: Pr[T_keygen > 60 s] ≤ 2^-40, Pr[T_sign > 1.5 s] ≤ 2^-40, and pathwise bounds T_keygen ≤ 360 s, T_sign ≤ 120 s, raw-query caps and workingRAM ≤ 64 KiB. These clauses and the performance game still need implementation in the protected resource contract.
The oracle has arbitrary byte-string input and a 32-byte output. Meter rom256-input64-ceil-v1 charges ceil(inputBytes / 64) for each query, including domain separation and every other supplied byte. Sum the per-call ceilings, not the ceiling of total input bytes. Repeated calls are charged again even when the ROM returns an already cached answer.
| Input bytes per call | Hash-work units | Raw security queries |
|---|---|---|
| 0 | 0 | 1 |
| 1–64 | 1 | 1 |
| 65–128 | 2 | 1 |
| 129 | 3 | 1 |
The empty-input case follows the literal ceiling. Zero hash-work weight does not mean zero raw queries or execution cost. An abstract unit is not a concrete compression block or an instruction: padding, output expansion and a real hash implementation belong to a separately specified execution profile.
The planned RISC-V profile records hash operations, instructions and memory work in one deterministic environment. It must bind the executable to the proved algorithms and cover key generation, signing and verification, including malformed inputs and failed retries. Benchmark samples are useful for calibration but would not alone prove a worst-case bound.
Execution prices, verifier limits and wallet calibration remain unfinished. No aggregate hash-throughput estimate certifies the 1.5-second or 60-second gate. An encoding saving 5% of hash work while adding expensive arithmetic must retain both sets of measurements; it is not automatically an execution improvement.
The planned Cost tab ranks signatureBytes * verificationWork after all profile gates pass. The current hash-work profile computes the product with exact integer arithmetic. The Pareto tab retains nondominated size/verification points at matched signing, keygen and memory budgets. Neither tab mixes games or metering profiles.
Keep the full keygen/signing/verification, size, memory and failure evidence with each result, along with source hashes, dependencies, verifier provenance, stage and profile. An entrant cannot change the organizer's scoring rule or promote its own receipt. Ties break by smaller signatures and then earlier accepted submission time.
Promotions are credited to the solver and, where used, the model. Research and rules-bounty credit are curated separately from numeric rank (§2). Awards and adoption require human review with published reasons. Prizes, timeline, protected-module governance and independent verifier registration remain open.
Draft v0.22 retains adaptive availability and separates hostile compilation from proof checking. Compilation runs in its own constrained service; the runner confirms process-tree termination, captures regular module artifacts into a private snapshot, and checks and exports those same read-only bytes. Receipts distinguish mathematical verification, resource certification, side-channel review and deployment eligibility. All remain unranked; diagnostic scores are explicitly non-eligible. Historical receipts must be reverified under suf-cma-total-work-pk32-adaptive-availability-v2, never relabeled.
Stage 1 is the academic research track. It includes one-time and few-time primitives, message encodings, authentication structures, domain-separated composition and complete constructions. OTS is an initial experiment, not the boundary of the academic competition. Each board needs its own pinned security game, request/instance budgets and resource profile; only comparable entries share a ranking.
Standard hybrid arguments can lift suitable single-instance security to multiple instances, generally with a loss. State and account for that loss and the conditions under which the argument applies. Shared random-oracle domains, seed-derived keys and the way a component is actually used in SPHINCS still need to match the reduction; an internal OTS is not automatically used as a fully black-box standalone scheme.
The experimental OTS library supplies graph evaluation, reconstruction, cost arithmetic and conditional failure envelopes. It is not a protected OTS security target. Direct pure-ROM proofs must remain possible beyond any optional construction template; lower-bound results must name the family and cost model they cover.
Stage 2 is the Ethereum selection track. It measures complete stateless constructions, with SUF-CMA, the normal and extended-lifetime floors and all deployment gates. Size includes the whole serialized signature, not just a WOTS component or authentication fragment.
The three-file declaration contract remains sigma.txt, hverify.txt and bound.txt, alongside the scheme and proof sources. The revised protected statement uses total work Q, a 32-byte public key and same-scheme decay. The product rule is stored in organizer-owned scoring configuration, not in a fourth entrant file.
The runner is explicitly unranked, and does not yet bind the signing and keygen budget certificates or full-program execution costs. Successful verification and integrity checks yield a diagnostic product score; resource certification, side-channel review and deployment eligibility remain separate and blocked. Positive metric canaries test comparator matching only. No cryptographic baseline yet: passing those fixtures is not an accepted signature scheme or a launch decision.
The intended first accepted entry is a SPHINCS⁻ variant meeting these requirements. The pinned PR #19 review and local reproduction establish a useful 126-bit classical SUF-CMA theorem at up to 224 signing requests, not an accepted competition entry.
The adapter still needs byte serialization, game/query transport, weighted verification and signing-failure certificates. In particular, a theorem capped at 224 requests does not establish R4 at 232; the same-scheme extended-lifetime proof is additional work. Seed derivation, storage and wallet bounds also remain. Upstream work stays coordinated with Emile rather than silently changing the audited revision.
Useful directions include incomparable encodings, bounded grinding, coded disclosures, few-time components, authentication multiproofs, tree layouts, tighter reductions and lower bounds in explicit models. Every claimed security improvement retains its constants; every practical improvement retains the full execution and storage costs.
Emile's polynomial-coding exploration motivates keeping the model open to unusual constructions. The technical annex review records the supplied construction, re-metering assumptions and unproved obligations. A shape that wins in one abstract cost model is not thereby globally optimal or deployable.