LeanEval Lifecycle-Overhaul Implementation Program

Summary

Implement the full lifecycle overhaul through production rollout: immutable v1, problem lifecycle metadata, results schema version 2, append-only state, replay and kernel validation, a Cloudflare submission server, automatic publication, the lifecycle-aware leaderboard, generator extraction, software verification, FC100 integration, and later comparator disproof support.

Terminology: unqualified v1 and v2 refer only to problem sets. This program calls the platform work the lifecycle overhaul, and the resulting system the lifecycle-aware platform. Versioned machine formats are always qualified, for example results schema version 2; frozen identifiers and filenames may retain strings such as results-v2.

Completion requires:

Every problem on leanprover/lean-eval@main at migration time is classified under the new metadata model.
A human-approved v1 membership is frozen and enforced by CI.
Every result present when the migration lock is acquired is losslessly converted to results schema version 2.
Every historical accepted submission is replayed or explicitly marked unavailable.
The submission Worker automatically deploys through staging to production.
Issue intake initially targets a four-week overlap and closes only after the adoption gates pass; a maintainer may explicitly shorten the overlap after announcing the revised closure date.
The lifecycle-aware leaderboard replaces the existing site after hosted-preview parity validation.
Software-verification and FC100/open-conjectures groups launch under their respective policies.
All edited Lean files build without errors or linter warnings.

PR #536 is the authoritative product direction. Repository creation, commits, pushes, PRs, merges, infrastructure provisioning, and external publication remain explicit authorization points.

Architecture and Public Contracts

Repository ownership

Create four repositories with explicit visibility:

Private leanprover/lean-eval-state: production events, schemas, validator, materializer, and operator CLI, plus a reproducible schema-validated public projection.
Private leanprover/lean-eval-state-staging: synthetic staging events only, plus the same public-projection contract where useful for testing.
Public leanprover/lean-eval-generator: the extracted Lean generator.
Public leanprover/lean-eval-releases: automatically published solution snapshots.

Existing ownership remains:

lean-eval: problem sources, metadata, frozen sets, and generator consumption.
lean-eval-submissions: results, Worker source, intake/evaluation workflows, replay orchestration, and infrastructure documentation.
lean-eval-leaderboard: presentation-oriented site data and frontend.
lean-eval-audit: encrypted snapshots and security-sensitive replay/release operations.

Use one public [overhaul] implementation tracker issue in lean-eval; do not create per-workstream tracking issues.

Stable identifiers

Freeze the identifier specification before any schema migration or state events.

result_id is:

"r2_" + lowercase_hex(
  SHA256(
    UTF8("lean-eval-result-v2\0") +
    RFC8785_CANONICAL_JSON([
      lowercase_github_login,
      verbatim_declared_model,
      problem_id,
      statement_revision
    ])
  )
)

Rules:

Intake or submission IDs are not inputs.
A retry or improved submission for the same tuple remains a sticky no-op.
A new statement revision produces a distinct result.
Model aliases and renames never alter the base ID.
Two declared labels later merged into one canonical identity retain distinct base records.
Legacy and server-originated records use the same derivation.
Fixtures cover legacy migration, retries, revisions, aliases, and merge collisions.

Other identifiers:

submission_id: cryptographically random UUIDv7 after successful authentication.
event_id: cryptographically random UUIDv7.
replay_task_id: deterministic SHA-256 of result_id plus measurement-configuration digest.
Retries retain the same task ID and receive monotonic attempt numbers.

Problem metadata and frozen sets

After a compatibility migration, replace test with required manifest fields:

group: formalization-evaluation, software-verification, or open-conjectures.
status: draft, active, or archived.
visible: boolean; current tests and Sandbox examples become hidden.
statement_revision: monotonic positive integer.
tags: validated hand-applied tags.
Status and revision histories with effective dates, reason categories, and statement digests.

Add:

A tag registry with stable names, display labels, and descriptions.
Derived topic tags based on module paths.
Named-set manifests containing (problem_id, statement_revision) membership.
An immutable frozen marker for published sets.
CI comparison against the default branch to reject frozen membership changes and same-revision statement changes.
Retraction metadata that preserves historical membership while excluding a retracted revision and its solves from current standings.

The v1 audit generates JSON and Markdown evidence covering solve counts, public leaks, issue history, and misformalisation risk. Agents produce recommendations; a maintainer selects v1.

Results schema version 2 and live migration

Rewrite each per-user file as:

{
  "schema_version": 2,
  "user": "github-login",
  "results": [
    {
      "result_id": "r2_…",
      "problem_id": "…",
      "statement_revision": 1,
      "declared_model": "…",
      "accepted_at": "…",
      "benchmark_commit": "…",
      "intake": {
        "kind": "issue",
        "issue_number": 123
      },
      "submission": {
        "kind": "github_repo",
        "repo": "owner/repo",
        "ref": "40-char-sha",
        "public": false
      },
      "production_metadata": {}
    }
  ]
}

Server records use intake.kind = "server" and submission_id. Structured production metadata includes credit identity, component models, harness, human involvement, web access, wall time, token counts, cost and billing mode, optional prompts, and notes.

Migration sequence:

Update all current consumers—including the existing leaderboard generator—and writers to accept results schema versions 1 and 2.
Give migration and normal record jobs the same durable Git writer-lock protocol. Do not use a static Actions concurrency group as a queue: GitHub retains only one pending run per group and may cancel an older pending run.
Produce and review a dry-run artifact containing the source commit, live record count, canonical output digest, duplicate report, and field-preservation report.
Explicitly authorize the migration workflow with apply=true.
The workflow acquires the durable writer lock; normal record jobs wait and retry without being dropped while intake and evaluation remain live.
Re-read current main, capture its count and SHA, migrate deterministically, validate exact preservation, and push one recorder-App commit.
Verify every file uses schema version 2 before releasing the lock; queued record jobs then resume using the schema-version-2 writer.
Keep schema-version-1 fixtures for historical compatibility tests, but require schema version 2 in the live store.

Rollback is permitted only before a schema-version-2-only record lands. After that point, recovery uses a forward repair generated from the captured source SHA rather than reverting the store.

Append-only state and materialization

Store one immutable JSON event per file under UUID-prefix-partitioned events/<first-two-UUID-hex>/<event-UUIDv7>.json. Every event contains:

Schema version, event ID, canonical UTC timestamp, and authenticated actor.
Submission, result, or task subject.
Optional causation event.
A versioned type-specific payload.

Initial event types cover:

Intake, snapshot archival, evaluation dispatch/completion/failure, and result recording.
Metadata amendments, aliases, repairs, retractions, and maintainer interventions.
Publication scheduling, opt-out/opt-in, release attempts, releases, and failures.
Replay enqueue, claim, attempt, verdict, measurement, adjudication, and unavailable status.

Branch protection on production state must:

Forbid force-pushes and branch deletion.
Permit only the narrowly scoped state-writer principal to append. Initial staging and production use distinct single-repository fine-grained PATs with a 90-day maximum lifetime and a rotation deadline at least 14 days before expiry. The approved D9 Apps/broker separately authorize source reads and workflow dispatch; they neither replace nor broaden the State writer. If a later State-writer App/broker is adopted, remove the user bypass when the PATs are revoked.
Require schema validation for human PRs.
Preserve a linear default branch.
Prevent modification or deletion of existing event paths.

The Python materializer and operator CLI:

Validate the complete event graph and result store.
Fail closed on unknown schemas, duplicates, causal gaps, invalid actors, or conflicting terminal states.
Reconstruct the current public view deterministically.
Produce canonical domain-view fixtures consumed by the leaderboard.
Materialize release and replay queues without rewriting source events.
Append operator events through non-forced compare-and-swap commits.

The state/replay agent owns the canonical materialized domain contract. The leaderboard agent owns only the presentation transformation from that contract to site-data files.

Submission server

Implement a TypeScript port of Palomar’s atomic Git-state patterns under lean-eval-submissions/server/.

Expose versioned /api/v1 routes for:

Browser OAuth intake.
Agent challenge creation and submission.
Authenticated submission status.
Metadata amendments and backfill.
Model aliases and new canonical-identity requests.
Repairs, retractions, and publication choices.

Authentication:

Browser OAuth tokens are verified and discarded.
Agent challenges are signed, expiring, and bound to a tag at the submitted commit plus a secret gist owned by the asserted account.
Only consumed nonce digests are recorded.
Amendments require the GitHub identity owning the base record.
Maintainer overrides become public events.

The Worker does not handle source and uses no KV, D1, R2, Durable Objects, Containers, or Cloudflare Sandbox SDK. Durable facts live in Git events; Cloudflare’s rate-limit binding is documented as transient abuse-control state.

After intake, the Worker dispatches the existing secure Actions pipeline. That pipeline:

Mints a read-only GitHub App token.
Fetches only Submission.lean and Submission/ at the exact commit.
Archives the exact snapshot before evaluation.
Removes repository metadata and credentials.
Runs sandbox and environment probes.
Evaluates untrusted Lean with no network or write credentials.
Passes only verdicts and public statistics to separate recording jobs.
Writes results using schema version 2 and appends state events.

Policies:

Evaluation-group sources must be private.
Open-conjecture sources must be public.
Release occurs two UTC calendar months after acceptance, using end-of-month clamping.
Submitters may opt out before the ordered release event.
Released files use Apache-2.0 after final human/legal wording review.
Legacy submissions remain grandfathered unless their owners opt in.

Release repository and key security

Publish each solution under:

releases/YYYY/MM/<result_id>/
  Submission.lean
  Submission/…
  metadata.json
  LICENSE

The state release event records the exact release-repository commit and tree digest.

An erroneous publication is removed from the releases repository without rewriting results or state. A true confidentiality incident may require history cleanup only in lean-eval-releases; the immutable state log records the incident and corrective action.

A combined replay/release key-design gate precedes production intake:

New snapshots use a per-submission capability: a release or replay job may receive authority for exactly one submission, and no archive-wide private key enters a runner that builds untrusted Lean.
Initial key custody uses AWS KMS in a dedicated LeanEval AWS account behind a provider-neutral wrap/unwrap interface. Stable archive paths, ciphertext, submission IDs, and capability claims do not encode AWS; moving providers rewraps per-submission data keys without changing those identities.
Provider-loss recovery is explicitly out of scope. Document key ownership, expiry, rotation, and revocation; no provider-loss drill or second-provider system is required.
Production intake, private replay, and automatic release remain disabled until the one-submission capability and concise contributor/release wording receive human security approval.

Trusted replay infrastructure

Public-source historical submissions may replay from their exact public commits immediately.

Private or no-longer-public replay is a separate LeanEval service and has no dependency on another project's runner. Its provider-neutral boundary accepts an immutable execution request and one-submission decrypt capability, launches one fresh isolated environment, returns only a schema-validated verdict and statistics, and tears the environment down. Plaintext never crosses an Actions artifact or job boundary. The initial implementation remains disabled until a dedicated backend and the D6 capability design are approved; no particular VM, cloud, or CI provider is part of the durable contract.

The selected backend must pin its image, CPU, architecture, kernel, tool versions, cache state, measurement commands, and network policy. Initial concurrency is one; increasing it requires a separate capacity and isolation review.

For every result:

Restore the exact benchmark commit, toolchain, dependencies, exporter, and source.
Overlay only accepted submission files.
Build/export once and fan out to pinned checkers.
Record accept/reject/decline/crash/timeout separately.
Record wall time, build cost, LOC, file count, and retired instructions when available.
Never silently substitute newer toolchains.

Wave 1 probes hardware performance counters on the reference replay VM. If unavailable, instruction fields are explicitly unavailable; runner-specific wall time remains displayed but is not relabeled as instruction cost or used as the default ranking metric.

Cloudflare deployment and infrastructure ledger

Use:

Production Worker: lean-eval-submission-server.
Production route: eval-submit.lean-lang.org.
Staging Worker: lean-eval-submission-server-staging.
Staging route: eval-submit-staging.lean-lang.org.
Separate state repositories, OAuth apps, GitHub Apps, fixture repositories, and secrets.

wrangler.jsonc owns Worker code/configuration: environment-specific names and routes, current compatibility date, generated binding types, nodejs_compat, observability, cron, static assets, and rate limiting. Disable workers_dev and preview URLs.

Add lean-eval-submissions/INFRASTRUCTURE.md as the human-readable ledger for both Cloudflare and replay infrastructure. Record:

Account/zone IDs, Worker names, routes, DNS, cron, bindings, and observability.
Secret names—but never values—owners, scopes, storage, and rotation.
GitHub Actions environments and deployment-token blast radius.
OAuth callback URLs and GitHub App IDs, permissions, and installations.
State, audit, releases, and staging repositories.
Private-replay provider, isolation lifecycle, runner images, network policy, capacity, and cleanup.
Concise bootstrap, deployment, rollback, key-rotation, incident, and decommission procedures.
Last manual verification date and maintainer.

Do not initially build an exhaustive Markdown/config linter or weekly drift workflow. PR review requires infrastructure-affecting changes to update the ledger; normal tests validate the actual Wrangler configuration and hostname policy.

Deployment:

PRs run dependency audit, zero-warning lint, TypeScript checking, unit/contract tests, workerd runtime tests, security tests, and Wrangler dry-run.
A protected-main merge is the production authorization.
The merge automatically deploys staging.
Staging smoke tests exercise health, GitHub connectivity, synthetic intake, CAS contention, and scheduled reconciliation.
The same source commit automatically deploys production only after staging passes.
Production smoke tests verify health/configuration without submitting a real proof.
Deployment jobs are serialized and never cancelled midway.
A manual rollback workflow uses Cloudflare version rollback and is documented in the ledger.

Use the official Cloudflare GitHub Actions deployment model and Worker rollback mechanism.

Generator, FC, and comparator

lean-eval-generator exposes a deterministic Lean CLI with a versioned JSON contract:

Input: marked-up module content, resolved holes, manifest metadata, templates, and LeanEval-owned target pins.
Output: complete workspace file map with paths and digests.
Stdout is machine-readable; diagnostics use stderr.
Both projects pin an exact generator revision.

Migration:

Extract the generator without changing existing output.
Add corpus-wide and FC golden tests.
Pin it from lean-eval.
Remove the old embedded core only after byte-for-byte parity.
Publish the CLI contract and fixtures for FC contributors.
Coordinate through issue #533 and PR #4951; do not take ownership of the FC importer.
Re-resolve answer-slot types under LeanEval’s target environment.
Reproduce the FC100 dependency audit in CI before import.
Launch FC100 proof-only once the importer owners supply compatible output.

Comparator disproof work moves to the open-conjectures phase. It does not consume a Wave 2 agent slot or block the first FC100 import.

Software verification and editorial work

Explicitly hand the current untracked seed files to the catalog agent by content digest, copying them into an isolated worktree while leaving the original checkout untouched.

Both seed problems enter as draft.
Trusted statements require human review.
Verified calculations require a separate specification for inputs, sandboxing, hardware, repetitions, resource limits, and anti-specialization rules before intake opens.
Agents may audit prose, citations, and consistency.
Agents do not author hints.

Copycat detection remains deferred; egregious cases use append-only retraction events.

Lifecycle-aware leaderboard

The canonical materializer emits a normalized domain view. The leaderboard converts it into:

index.json: source commits, group summaries, scopes, and feed links.
groups/<group>.json: problem rows and standings.
problems/<id>.json: lifecycle, revisions, sets, solutions, metadata, measurements, and release links.
Recent-solutions JSON and RSS feeds.

Keep Verso for shell/navigation/prose. Use framework-free TypeScript browser modules for data-heavy surfaces.

Required behavior:

Group tabs with policy text.
Scope selector defaulting to the current flagship set.
URL-persistent tag filters.
Unique, first, and total solve counts; unique is the default ordering.
No combined cross-group ranking.
Stable problem URLs and visible revision/retraction history.
Canonical identity and alias handling.
Deterministic first-solve order.
Escaping of every submitter-controlled field.
Explicit unavailable states for missing replay data.

Publish the lifecycle-aware leaderboard under a preview path in the existing Pages artifact while the old site remains default. Cut over only after complete-store parity, link/accessibility checks, and stakeholder review. Retain the previous deployment for rollback.

Parallel Agent Program

Use one root coordinator plus three agents. Each lane works in isolated worktrees or clones; no agent edits the dirty primary checkout.

Wave 0: authorization and contracts

Root coordinator:

Obtain explicit authorization for the tracker and four repository creations.
Create the tracker and repository bootstraps.
Record dependencies, approvals, PRs, CI state, and rollout gates.
Hash and hand off the untracked software-verification drafts.

State/replay agent:

Write the stable identifier specification and cross-language fixtures.
Define the results schema-version-2 and event envelopes.

Exit gate: identifier examples and schema fixtures pass in Python, TypeScript, and Lean-facing consumers.

Wave 1: foundations

Owner	Deliverables
Root	Worker scaffold, Cloudflare configurations, automatic deployment pipeline, infrastructure ledger, and GitHub/OAuth threat model.
Catalog/site agent	Problem metadata schema, tag registry, migration, frozen-set validation, and v1 evidence audit.
State/replay agent	Results schema-version-2 compatibility and locked migration workflow; state schemas, validator, materializer, operator CLI, branch rules, and performance-counter probe.
Generator/FC agent	Generator repository, deterministic CLI, golden tests, and LeanEval consumer migration.

Exit gate:

Existing leaderboard and writers support results schema version 2.
Dry migration preserves the captured live store exactly.
State materialization is deterministic and fail-closed.
Generator output is byte-for-byte unchanged.
Staging Worker deploys automatically.
Replay runner feasibility and instruction-counter availability are known.

Wave 2: product implementation

Owner	Deliverables
Root	OAuth/agent intake, dispatch, amendments, publication state machine, dual intake, release-repo integration, and combined key-security review packet.
Catalog/site agent	Leaderboard domain adapter, site-data schema version 2, client UI, preview path, stable pages, and recent/RSS feeds.
State/replay agent	Results schema-version-2 live migration, public-source replay, provider-neutral private-replay boundary, measurements, shadow checker integration, and corpus report.
Generator/FC agent	LeanEval-side FC contract, fixtures, target-environment validation, and coordination with FC importer owners.

Exit gate:

Staging intake completes end to end using synthetic repositories.
The current site remains live while the lifecycle-aware replacement is developed.
Leaderboard preview materializes the complete production corpus.
Public replay works; private replay isolation is demonstrated without an archive-wide key.
Key and release design has human security approval.

Wave 3: production rollout

Human approves v1 membership, software-verification statements, Apache-2.0 acknowledgement text, key ceremony, and any checker promotions.
Freeze v1 and merge software-verification drafts.
Provision production Cloudflare, GitHub App, OAuth, state, release, and replay resources exactly as documented.
Automatically deploy the Worker with intake initially disabled.
Run the production health smoke test.
Enable server intake and start the initially planned four-week issue-intake overlap.
Deploy the lifecycle-aware leaderboard preview and complete parity review.
Cut over to the lifecycle-aware leaderboard.
Replay private historical submissions through the approved per-submission key path.

Issue intake closes only when:

Four weeks have elapsed, unless a maintainer explicitly selects and announces a shorter overlap before closure.
There are no unresolved severity-high server incidents.
Each of the five most active submitters from the preceding 60 days has completed a server-path submission or explicitly confirmed no migration dependency.
At least 90% of submissions in the final 14 days use the server path when there are at least ten submissions; otherwise a maintainer records a manual adoption assessment.
The migration has been announced on Zulip and in repository documentation for at least two weeks.

Wave 4: open conjectures and follow-through

Import FC100 through the FC-owned importer.
Launch the open-conjectures tab and public-only intake.
Begin comparator disproof work with comparator contributors.
Add generator/manifest disproof support after comparator lands.
Finish replay or mark unrecoverable submissions unavailable with reasons.
Complete the flavour-text audit without agent-written hints.
Review whether infrastructure drift automation is justified by operational experience.

At every boundary, agents return their diff, tests, warnings, risks, and dependency state. The root reviews cross-repository contracts before requesting authorization for commits, pushes, PRs, merges, or infrastructure actions. PRs target upstream default branches; dependent PRs remain draft and are rebased after prerequisites rather than targeting stacked fork branches.

Test and Acceptance Gates

Required tests include:

Results: deterministic IDs, exact migration preservation, queued writer behavior, idempotence, aliases, revisions, and rollback boundary.
Metadata: groups, statuses, visibility, tags, frozen membership, revision changes, retractions, and warning-free Lean builds.
State: malformed/unknown events, duplicates, causal gaps, actor validation, CAS contention, branch protection, and deterministic replay.
Server: OAuth, agent proof, nonce reuse, exact refs, source-visibility policy, hostile metadata, rate limiting, retries, and provider failures.
Security: no source or credentials in public logs/artifacts; untrusted jobs carry no write credentials; sandbox probes remain mandatory.
Release: calendar-month edge cases, opt-out races, idempotent retries, exact file allowlist, license metadata, incident removal, and stable links.
Replay: disposable VM cleanup, per-submission key scope, original pins, missing toolchains, checker outcomes, retries, and unavailable counters.
Generator: corpus and FC byte parity, malformed requests, answer-slot mismatches, and deterministic output.
Leaderboard: alias collisions, unique/first/total standings, filtered scopes, retractions, feed order, escaping, stable URLs, and unavailable statistics.
Deployment: staging/production isolation, hostname restrictions, documented credentials, automatic promotion, smoke tests, and a validated rollback command.

Final acceptance requires green CI, zero linter warnings, a current tracker and infrastructure ledger, successful staging smoke tests, documented human approvals, and a documented rollback command for each production cutover.

Locked Assumptions

Workstreams 1–11 are managed; hints remain human-written.
PR #536 is authoritative.
Four new repositories are created: private production and staging State, public generator, and public releases; State publishes only its reproducible, schema-validated projection.
Historical results are fully rewritten to flat schema version 2 under a serialized writer lock.
State uses immutable event files.
Generator implementation remains Lean with a JSON CLI.
Production hostname is eval-submit.lean-lang.org.
Default embargo is two UTC calendar months.
Released source uses Apache-2.0 after wording review.
Private replay uses a dedicated provider-neutral isolation boundary; the backend is deliberately unselected and unrelated to other projects' runners.
Replay and release share one least-privilege key-design gate.
Cloudflare uses Wrangler configuration plus INFRASTRUCTURE.md, not Terraform.
Protected-main merges automatically deploy staging and then production.
Leaderboard preview shares the existing Pages artifact.
Issue intake initially targets four weeks, retains the adoption gates, and may be shortened only by an explicit announced maintainer decision.
Comparator disproof support is deferred to the open-conjectures phase.
Completion continues through production cutover, issue-intake retirement, replay backfill, and FC100 launch.

kim-em/lean-eval-overhaul-implementation-plan.md

Select an option

No results found

Select an option

No results found

LeanEval Lifecycle-Overhaul Implementation Program

Summary

Architecture and Public Contracts

Repository ownership

Stable identifiers

Problem metadata and frozen sets

Results schema version 2 and live migration

Append-only state and materialization

Submission server

Release repository and key security

Trusted replay infrastructure

Cloudflare deployment and infrastructure ledger

Generator, FC, and comparator

Software verification and editorial work

Lifecycle-aware leaderboard

Parallel Agent Program

Wave 0: authorization and contracts

Wave 1: foundations

Wave 2: product implementation

Wave 3: production rollout

Wave 4: open conjectures and follow-through

Test and Acceptance Gates

Locked Assumptions