From 9c8f404fb80662de66c4cb48b166e671ed1fcdb2 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 25 Aug 2026 13:05:59 +0000 Subject: [PATCH] Document lifecycle overhaul completion contract --- PLAN.md | 10 + docs/overhaul-completion-plan.md | 445 +++++++++++++++++++++++++++++ docs/overhaul-execution-runbook.md | 424 +++++++++++++++++++++++++++ 3 files changed, 879 insertions(+) create mode 100644 docs/overhaul-completion-plan.md create mode 100644 docs/overhaul-execution-runbook.md diff --git a/PLAN.md b/PLAN.md index 17d76949..ef57f847 100644 --- a/PLAN.md +++ b/PLAN.md @@ -4,6 +4,16 @@ Status: **accepted for staged implementation**. The original RFC was reviewed and merged in [lean-eval#536](https://github.com/leanprover/lean-eval/pull/536). Written 2026-08-19; status updated 2026-08-20. +> **Completion amendment, 2026-08-25.** The remaining work is governed by the +> [overhaul completion plan](docs/overhaul-completion-plan.md) and its +> [execution runbook](docs/overhaul-execution-runbook.md). The completion plan +> records later maintainer decisions and supersedes conflicting requirements +> below, in particular Formal Conjectures integration, disproof support, +> experimental independent kernels, the original phase ordering, and any +> requirement for a dedicated submission hostname. This file remains the +> design history and authority for product goals that the completion plan +> retains. + Terminology: unqualified **v1** and **v2** refer only to problem sets. This document calls the platform work the **lifecycle overhaul**, and the resulting system the **lifecycle-aware platform**. Versioned machine formats are always diff --git a/docs/overhaul-completion-plan.md b/docs/overhaul-completion-plan.md new file mode 100644 index 00000000..f9d8c9d6 --- /dev/null +++ b/docs/overhaul-completion-plan.md @@ -0,0 +1,445 @@ +# LeanEval lifecycle overhaul completion plan + +Status: **accepted scope for completing the overhaul** +Adopted: 2026-08-25 +Production posture at adoption: intake, general replay, production replay, and +automatic publication are disabled. + +## 1. Authority and use + +This document is the scope authority for all remaining lifecycle-overhaul work. +It is a maintainer amendment to [`PLAN.md`](../PLAN.md), not a new product RFC. +It narrows the original program after implementation experience exposed work +that was disproportionate or outside LeanEval's boundaries. + +The companion [`overhaul-execution-runbook.md`](overhaul-execution-runbook.md) +turns this scope into ordered gates and a mutable completion checklist. When +the two documents differ: + +1. this completion plan decides **what** is in scope and what counts as done; +2. the runbook decides the current order and status of that work; +3. tracked runtime configuration and current infrastructure inventories decide + the observed operational state, but cannot expand scope. + +The original plan remains authoritative for retained product details such as +problem lifecycle, structured metadata, immutable snapshots, two-calendar- +month release policy, append-only State, leaderboard behavior, and replay +measurements. The explicit amendments in this document take precedence over +conflicting original text. + +## 2. Two completion milestones + +The overhaul has two deliberately separate milestones. + +### 2.1 Production launch + +Production launch means that a new submission can: + +1. enter through the new server; +2. receive a per-submission encrypted archive before evaluation; +3. be evaluated from its immutable snapshot; +4. produce an immutable accepted or rejected result and append-only lifecycle + state; +5. appear correctly on the lifecycle-aware leaderboard; +6. be scheduled for automatic release under the two-calendar-month policy; +7. use the launch-approved owner and maintainer lifecycle functions; and +8. be paused or rolled back through a tested disable path. + +Historical-corpus replay is not a production-launch blocker. The old issue +intake also remains open during the overlap. + +### 2.2 Full overhaul completion + +The whole overhaul is complete only after production launch **and**: + +- every historical accepted result at the final cutoff has either a terminal + official-kernel-plus-nanoda replay record or a reviewed unavailable reason; +- recoverable historical private archives have the required per-submission + envelope for replay; +- the neutral open-problems tab exists (it may be empty initially); +- the retained software-verification and editorial work is in its agreed + state; and +- the four-week issue-intake overlap has completed and issue intake has been + retired under the incident and notice gates below. + +This distinction allows the useful new system to launch without pretending +that the historical migration is finished. + +## 3. Retained product scope + +The following remain part of the overhaul. + +### 3.1 Problems and leaderboard + +- Lifecycle metadata, immutable statement revisions, status history, tags, + visibility, and frozen-set membership. +- The frozen 128-member formalization-evaluation v1 set. +- Lifecycle-aware group and problem pages with stable URLs and visible problem + statements. +- Client-rendered data-heavy pages, unique-solve and total-solve standings, + recent solutions, metadata provenance, replay statistics, and released- + solution links. +- The software-verification group and its already reviewed draft problems. +- A neutrally named **open problems** tab. It has no FC dependency and may + launch empty. + +### 3.2 Submission lifecycle + +- Browser OAuth and the source-bound headless-agent path. +- Structured, self-reported model, human-involvement, prompt, compute, and + provenance metadata. +- Immutable source snapshots archived before evaluation. +- Append-only State transitions and immutable base Results records. +- Metadata backfill, result repair and retraction requests, maintainer + decisions, model aliases, and model renaming. +- Visible release opt-out and the automatic two-calendar-month release policy. +- An operator-controlled emergency pause and deterministic recovery path. + +### 3.3 Archive and release + +- A provider-neutral schema-version-3 sidecar with one fresh key envelope per + submission, strict submission/digest binding, and separated wrap/unwrap + authority. +- Automatic reconstruction and publication from the accepted immutable + snapshot, with source and credentials excluded from public logs and + artifacts. +- Existing grandfathering and opt-out policy for legacy submissions. + +### 3.4 Historical replay and statistics + +- Exact original source, benchmark, toolchain, and component pins. +- The ordinary Lean build/elaboration path (the official kernel) and nanoda. +- Terminal distinctions between acceptance, checker rejection, orchestration + failure, timeout, resource limit, and unavailability. +- Versioned checker identity/revision and measurement-series fields, so a + later project can replay old submissions with other kernels without another + archive migration. +- Build cost, checker cost, size, and other already specified measurements when + the pinned runtime can collect them. + +## 4. Explicit scope reductions + +The following are not requirements for launch or full overhaul completion. +They must not be revived merely because old planning text, a branch, or an +unchecked tracker item mentions them. + +### 4.1 Formal Conjectures and disproofs + +- No Formal Conjectures importer, FC100 integration, synchronization, external + coordination, or FC-owned content lane. +- No comparator disproof support. +- No dependency on any Formal Conjectures pull request. +- The open-problems tab remains provider-neutral and may be empty. + +### 4.2 Experimental kernels + +- No Lean Kernel Arena candidate work. +- No Mathgraph or other experimental checker integration. +- No checker-series, corpus-promotion report, source-free runner-attestation + protocol, candidate promotion decision, or checker-author workflow. +- No persistent qualification system for future kernels. + +The only obligation is not to make the replay and archive formats inherently +nanoda-only forever. A versioned schema extension point is sufficient. + +### 4.3 Disproportionate qualification machinery + +- Delete the persistent model-identity qualification harness, its private + Workers, Durable Objects, workflows, fixtures, generated types, recovery + protocol, and rebuild instructions. +- Do not replace it with another persistent qualification service. +- Do not require exhaustive failure injection, contention matrices, recurring + certification runs, or a dedicated qualification control plane for launch. + +Existing focused unit tests and ordinary security hardening remain valuable; +scope reduction is not permission to regress source-bound sessions, +authorization checks, State CAS/idempotency, or fail-closed behavior. + +### 4.4 Other deferrals + +- Automated copycat detection remains deferred. +- Provider-loss recovery and a second key provider remain out of scope. +- Verified-calculation performance infrastructure requires a later trusted- + runner specification. +- Agent-authored hints and flavour text remain prohibited; editorial text is + human work. +- Model consolidation need not be enabled for launch or completion. Preserve + the existing implementation only if it is inexpensive and safe to keep dark; + otherwise remove it and revisit consolidation separately. +- No new exhaustive infrastructure linter, drift service, or recurring + qualification harness without a new maintainer decision. + +## 5. Submission entry point and OAuth + +No dedicated LeanEval hostname is required. + +- Publish a stable static entry page at + `https://lean-lang.org/eval/submit/` in the existing leaderboard site. +- The entry page sends the user to the authenticated production application on + `lean-eval-submission-server.lean-eval.workers.dev`. +- Keep OAuth callbacks and session cookies on that Worker origin. The browser + address may change to `workers.dev` while the form is open. +- Do not involve the `lean-lang.org` DNS or Cloudflare-zone owners merely to + keep the form under the vanity path. + +Serving the interactive application literally at `/eval/submit/` would require +a same-origin dynamic route or proxy on the `lean-lang.org` zone and is outside +the launch plan. + +Temporary private ownership of the production OAuth application is acceptable +for initial launch. Record the owner, credential custodian, recovery method, +rotation method, and intended organization-transfer path, but organization +ownership is not a launch gate. + +## 6. Launch lifecycle functionality + +Launch with most of the implemented lifecycle surface available. + +| Function | Launch disposition | Minimum staging acceptance | +| --- | --- | --- | +| New browser submission | Enable | One successful private synthetic submission and one invalid/unauthorized request | +| Headless-agent submission | Enable | One source-bound successful submission and one challenge/source mismatch denial | +| Metadata backfill | Enable | One owner success and one non-owner denial | +| Repair and retraction requests | Enable | One valid owner request and one invalid or non-owner denial | +| Maintainer decisions | Enable | One configured-maintainer success and one non-maintainer denial | +| Model alias and rename | Enable | One owner success and one collision or non-owner denial | +| Release opt-out | Enable | One pre-release opt-out with scheduling consequence checked | +| Model consolidation | Keep disabled or remove | Not a launch test | + +This is intentionally a bounded smoke, not a qualification campaign. Existing +repository tests must stay green, but launch does not require a persistent +harness, a full combinatorial route matrix, repeated live contention, or +failure injection at every State write boundary. + +For each enabled route family, also prove that its tracked feature flag can +disable it and that public health reports the expected effective state. + +## 7. Production-launch gates + +Production remains disabled until all gates below are satisfied. + +### 7.1 Repository and documentation cleanup + +- Remove the scope-excluded harnesses, experimental-kernel framework, and stale + instructions that would tell a later agent to rebuild them. +- Remove historical run narratives, failed-attempt stories, and superseded + diagnostic artifacts that are not consumed by current operation. +- Keep canonical replay inputs, current infrastructure identifiers and scopes, + current rollback instructions, and tests protecting live behavior. + +### 7.2 Disabled-state baseline + +Read-only verification must establish the current exact versions and that: + +- production intake is effectively disabled; +- general and production replay are disabled; +- automatic publication is disabled; +- public lifecycle gates have not been enabled accidentally; +- the protected State heads and tracked runtime pins are coherent; and +- the live leaderboard still shows statements, stable problem URLs, group + views, and representative solution metadata. + +### 7.3 Credential and key boundary + +- Repair the staging release OIDC trust mismatch through an explicitly + approved infrastructure change. +- Complete one credentialed staging unwrap and reconstruction for an accepted + staging archive with publication and production permissions disabled. +- Prove exact one-submission scope, consume-before-unwrap, reuse refusal, + authority removal, source allowlisting, no plaintext artifact, and cleanup. +- Connect and verify the production archive **Wrap-only** role required for new + intake. It must have no unwrap permission. +- Reverify the production release role's trust and scope without decrypting or + publishing a production archive during preflight. + +Historical legacy-archive migration is not a launch gate for new submissions. + +### 7.4 Entry page and bounded lifecycle smoke + +- Publish and verify the no-DNS entry page. +- Complete the bounded route-family staging cases in section 6 against the + exact proposed launch commit. +- Complete one exact-version staging lifecycle from archive through accepted + result, State, scheduled release, staging reconstruction, and rollback. + +### 7.5 Human go/no-go + +Prepare a compact packet containing: + +- exact repository commits and deployed versions; +- current feature-flag states; +- the section 7.2-7.4 results; +- credential owners, scopes, rotation, and revocation; +- OAuth ownership and recovery information; +- submitter-facing security, licensing, and release-policy text; +- rollback and emergency-pause instructions; +- deferred functionality and known limitations; and +- the issue-intake overlap announcement. + +Production capability enablement requires an explicit maintainer go/no-go even +when all repository work is otherwise autonomous. + +## 8. Launch and overlap + +After go/no-go, make capability changes separately: + +1. enable the automatic release controller initially when no release is due; +2. enable the approved lifecycle route families; +3. enable production intake through the finite-lease controller; and +4. verify the public entry path, effective health, State consistency, release + scheduling, and leaderboard presentation read-only. + +Do not mix refactoring, replay expansion, documentation cleanup, or unrelated +features into an enablement change. + +The four-week issue-intake overlap begins only when server intake is publicly +announced. During the overlap: + +- keep issue intake available; +- monitor severity-high incidents, State consistency, archive completion, + release scheduling, submitter adoption, and the first automatic releases; +- pause new server intake through the documented disable path if safety + evidence fails; and +- extend the overlap if a serious incident or inadequate adoption makes closure + unreasonable. + +## 9. Historical completion after launch + +Historical work may proceed in parallel with the overlap and other completion +lanes, but it does not delay initial production launch. + +### 9.1 Freeze and classify the final corpus + +- At the announced issue-intake cutoff, generate the append-only delta from + the retained baseline inventory. +- Every accepted result must be classified as public-source replayable, + private-archive replayable, or unavailable for a reviewed reason. +- Use the smallest existing State event mechanism capable of recording the + terminal disposition. Do not create a new aggregate transaction system unless + an actual atomicity requirement is demonstrated. + +### 9.2 Private archive migration + +- Reconcile the recoverable private archive/result bindings and the explicit + orphan set. +- Use a dedicated migration Wrap role and custodian-supplied legacy identity. +- Rewrap the per-submission data key without changing archive bytes or stable + IDs. +- Verify the result; do not retain plaintext or migration credentials. + +### 9.3 Replay execution + +- Build or qualify only exact images needed by replayable results. +- Restore exact original source and benchmark pins. Never silently substitute a + newer toolchain. +- Execute the ordinary official-kernel build and nanoda check with bounded + retries and explicit terminal outcomes. +- Publish the redacted verdict and measurement projection to the leaderboard. +- Retain versioned checker identity/revision fields for future replay projects. + +Full historical completion means every result at the final cutoff has a +terminal replay record or reviewed unavailable reason. + +## 10. Open problems, editorial work, and retirement + +### 10.1 Open problems + +- Use the neutral name **open problems**. +- Launching the tab with zero problems is acceptable. +- Do not add an importer, external synchronization, disproof semantics, or FC + dependency. +- Future content is an ordinary LeanEval-owned catalog decision outside this + overhaul. + +### 10.2 Software verification and editorial work + +- Verify that the two reviewed software-verification drafts render correctly + with their draft/provisional policy. +- Complete human review of statements, citations, and background according to + maintainer availability. +- Keep hints human-written. +- Do not build verified-calculation execution infrastructure in this overhaul. + +### 10.3 Issue-intake retirement + +After at least four weeks of announced overlap, close issue intake only if: + +- there is no unresolved severity-high incident; +- server intake, archive, evaluation, release scheduling, and leaderboard + presentation are stable; +- submitter adoption is adequate; +- at least two weeks of public closure notice has been given; and +- the final historical cutoff and append-only delta have been recorded. + +## 11. Repository and authorization boundary + +Autonomous implementation is allowed only in this LeanEval repository family: + +- `leanprover/lean-eval`; +- `leanprover/lean-eval-submissions`; +- `leanprover/lean-eval-leaderboard`; +- `leanprover/lean-eval-state`; +- `leanprover/lean-eval-state-staging`; +- `leanprover/lean-eval-releases`; +- `leanprover/lean-eval-generator`; and +- `leanprover/lean-eval-audit` (private). + +Within that allowlist, agents may autonomously inspect, implement, test, create +branches and pull requests, address review, merge after required checks, and +run ordinary repository CI. Existing automatic disabled-state deployments +triggered by an ordinary merge are also allowed, provided the change cannot +enable a production capability. + +Explicit approval is required for: + +1. any push, PR, issue, comment, review, reviewer request, or merge in a + repository outside the allowlist; +2. AWS, Cloudflare-account/zone, DNS, OAuth-App, GitHub-App, credential, + ruleset, deploy-key, or protected-environment mutation; +3. production intake, replay, publication, or public owner/maintainer feature + enablement; and +4. a material product-scope expansion. + +No technical dependency is permission to work in an external repository. +Prepare a local compatibility workaround or stop and request authority. + +## 12. Recordkeeping policy + +Repository documentation should contain current contracts, current state, +current operating instructions, and canonical data needed to finish the +product. It should not become a chronicle of agent activity. + +- Do not add run-by-run evidence tables, failed-attempt stories, shard + provenance essays, or “war stories.” Git, PRs, and Actions retain that + history. +- Update a status or identifier in place when the current operational fact + changes. +- Keep only canonical machine-readable historical inventories, plans, + mappings, and unavailable classifications that are still consumed. +- Delete a superseded object after no current plan, profile, rollback, or + migration input references it. +- Record a test or run link in a PR when useful; do not duplicate it into a + permanent ledger unless it is itself a current operational identifier. + +## 13. Final completion criteria + +The lifecycle overhaul is finished when all of the following are true: + +- production server intake is the supported intake path; +- new submissions archive before evaluation with per-submission envelopes; +- accepted and rejected lifecycle transitions are coherent and recoverable; +- automatic two-calendar-month releases are operating with opt-out support; +- the launch-approved backfill, repair/retraction, maintainer, alias, and rename + functions are available; +- the leaderboard correctly exposes lifecycle, statements, standings, + metadata, statistics, and released solutions; +- every historical accepted result at the final cutoff has a terminal replay + or unavailable disposition using the official kernel and nanoda; +- the neutral open-problems tab exists, even if empty; +- the software-verification drafts and agreed editorial state are visible; +- the four-week overlap and notice gates have passed and issue intake is + closed; +- current rollback and pause procedures have been verified; and +- the repository contains no known instructions to resume scope-excluded FC, + disproof, experimental-kernel, or persistent-qualification work. + diff --git a/docs/overhaul-execution-runbook.md b/docs/overhaul-execution-runbook.md new file mode 100644 index 00000000..9cf759e6 --- /dev/null +++ b/docs/overhaul-execution-runbook.md @@ -0,0 +1,424 @@ +# LeanEval lifecycle overhaul execution runbook + +Status: **active companion to the completion plan** +Scope authority: [`overhaul-completion-plan.md`](overhaul-completion-plan.md) + +## 1. Purpose + +This runbook is the operational checklist for finishing the lifecycle overhaul. +It is intentionally updateable: check items off, replace stale current-state +values, and keep the next action obvious. Do not use it to add product scope. + +Before acting, read the completion plan in full. If an old tracker, branch, +comment, or original-plan clause conflicts with it, the completion plan wins. + +## 2. Starting posture + +At adoption, the intended safe posture is: + +- production intake disabled; +- staging general replay disabled except for explicitly approved isolated work; +- production replay disabled; +- automatic publication disabled; +- public result-owner, maintainer, and model-identity gates disabled; +- the lifecycle-aware leaderboard live with problem statements visible; and +- no FC, disproof, or experimental-kernel work authorized. + +Do not trust this paragraph as a live probe. Phase 1 re-verifies it read-only +and updates the current infrastructure inventory in place if necessary. + +## 3. Execution rules + +### 3.1 Work autonomously inside the allowlist + +Repository implementation, tests, PRs, review fixes, merges, ordinary CI, and +automatic disabled-state deployments are autonomous in the repository family +listed in completion-plan section 11. + +Parallelize independent repository work and use build time productively. Do not +sit polling one workflow while other in-scope tasks can advance. + +### 3.2 Stop at these gates + +Obtain explicit maintainer approval before: + +- changing AWS or Cloudflare resources or permissions; +- changing DNS, OAuth Apps, GitHub Apps, credentials, deploy keys, rulesets, or + protected environments; +- enabling production intake, replay, publication, or public lifecycle APIs; +- acting in any repository outside the allowlist; or +- expanding the completion-plan scope. + +At an approval gate, present the exact mutation, target, reason, rollback, and +read-only precondition. Do not bundle several approvals into an open-ended +request. + +### 3.3 Keep changes reviewable + +- One coherent purpose per PR. +- Do not mix feature enablement with cleanup or refactoring. +- Preserve unrelated work in dirty worktrees. +- Do not weaken security checks merely to make a smoke pass. +- Do not add a new framework when a bounded script or existing mechanism is + sufficient. +- Merge only after required checks are green and review threads are resolved. + +### 3.4 Record current state, not a narrative + +- Check off the item and update the current identifier or state. +- Do not append run-by-run histories or incident prose. +- Keep GitHub run links in the PR or handoff message. +- Retain only canonical machine-readable inputs consumed by later phases. + +## 4. Phase 0 — rebaseline and delete overgrowth + +Goal: make the repositories describe only the approved remaining program. + +- [ ] Inventory every open PR, active workflow, remote branch, and relevant + local worktree in the allowlisted repositories. +- [ ] Confirm the already identified escaped external branches are absent and + the stale LeanEval PRs are closed. +- [ ] Review any uncommitted local cleanup attempt as an untrusted candidate + diff. Keep useful pieces only after comparing them with current upstream. +- [ ] Delete the persistent model-identity qualification harness, private + qualification Workers, workflows, generated types, fixtures, tests, and + rebuild/recovery instructions. +- [ ] Delete experimental-kernel shadow smoke, Arena/Mathgraph assets, + checker-series and corpus-promotion machinery, wire/attestation protocols, + candidate adapters, and tests that exist only for them. +- [ ] Remove exact-byte solution-export capture hooks that existed only to feed + the removed experimental-kernel lane. +- [ ] Retain the existing official Lean build and nanoda replay path, its + generic checker identity/revision fields, and its focused tests. +- [ ] Preserve source-bound agent sessions, authorization boundaries, + idempotency, CAS conflict handling, and other generally useful security + hardening. +- [ ] Remove superseded run narratives, diagnostic artifacts, and tests whose + only purpose is preserving those narratives. +- [ ] Retain canonical replay inventories, final plans, exact toolchain/source + maps, unavailable-candidate data, current rollback contracts, and current + infrastructure identifiers. +- [ ] Retain an older canonical input set only while a live execution profile + references it; delete the whole linked set after replacement. +- [ ] Rewrite the submissions tracker, rollout runbook, and infrastructure + inventory to current state and remaining gates, without a chronology. +- [ ] Run repository tests, typechecks, linters with zero warnings, workflow + validation, action-pin audit, and all relevant dry-runs. +- [ ] Merge the cleanup in coherent repository-local PRs. + +Exit condition: no tracked instruction tells a future agent to implement FC, +disproofs, experimental kernels, or the persistent qualification harness. + +## 5. Phase 1 — read-only disabled-state reconciliation + +Goal: establish one exact safe baseline before launch work resumes. + +### 5.1 Repositories and automation + +- [ ] Record current protected `main` commits for every allowlisted repository. +- [ ] List open PRs and cross-referenced work; close or classify stale overhaul + PRs. +- [ ] Confirm no unplanned workflow dispatch is queued or running. +- [ ] Confirm required checks, protected branches, and immutable dispatch-tag + protections match current operating needs. + +### 5.2 Deployed services + +- [ ] Read staging and production intake health. +- [ ] Read staging and production broker/replay health and current versions. +- [ ] Verify production intake is configured and effectively disabled. +- [ ] Verify general and production replay are disabled. +- [ ] Verify publication is disabled. +- [ ] Verify public lifecycle feature gates are disabled before their launch + smoke and approval. +- [ ] Verify deployed commits, container image digests, and protected State pins + form one coherent current unit. + +### 5.3 State, credentials, and presentation + +- [ ] Verify protected State heads and validation status. +- [ ] Inventory credential names, owners, scopes, expiry, rotation, and + revocation without exposing values. +- [ ] Confirm production State contains no unexpected accepted server + submission or due release work. +- [ ] Smoke the live leaderboard root, group tabs, stable problem URLs, + problem statements, and representative solution metadata. + +Exit condition: current documentation states one coherent disabled baseline. +Any mismatch becomes a separate repository fix or an approval-gated +infrastructure correction. + +## 6. Phase 2 — repository launch preparation + +These lanes can proceed in parallel after Phase 1. + +### 6.1 No-DNS submission entry + +- [ ] Add `https://lean-lang.org/eval/submit/` to the leaderboard site. +- [ ] Explain that authentication continues on the LeanEval Worker origin. +- [ ] Link to the production `workers.dev` application. +- [ ] Verify navigation, accessibility, mobile layout, and return path to the + leaderboard. +- [ ] Keep OAuth callback and session handling on the Worker origin. + +### 6.2 Release and archive repository preparation + +- [ ] Reconfirm the exact staging release OIDC trust mismatch. +- [ ] Prepare the smallest reviewed infrastructure patch or operator command; + do not apply it yet. +- [ ] Reconfirm the production archive Wrap-only role requirement and prove the + desired policy excludes unwrap. +- [ ] Verify the release controller reconstructs deterministically with + publication disabled using credential-free fixtures. +- [ ] Verify submitter-facing license, release delay, and opt-out language. + +### 6.3 Lifecycle API launch surface + +- [ ] Confirm feature flags exist independently for the route families being + launched. +- [ ] Keep model consolidation disabled or remove it. +- [ ] Run all existing repository tests. +- [ ] Prepare one success and one authorization/validation denial fixture for + each launch route family: + - [ ] metadata backfill; + - [ ] repair/retraction request; + - [ ] maintainer decision; + - [ ] model alias/rename; and + - [ ] release opt-out. +- [ ] Verify every launch gate can be returned to disabled and health reports + the effective state. +- [ ] Do not build a persistent staging harness. + +### 6.4 Exact-version lifecycle rehearsal + +- [ ] Select the exact candidate commits across the repository family. +- [ ] Use synthetic private source repositories owned for staging. +- [ ] Prepare one browser and one source-bound headless submission. +- [ ] Include one deliberate invalid or unauthorized case. +- [ ] Confirm archive-before-evaluation and schema-version-3 binding. +- [ ] Confirm acceptance/rejection, immutable Result, append-only State, release + scheduling, and redacted leaderboard projection. +- [ ] Prepare the rollback/disable steps for the same exact version. + +Exit condition: repository changes and staging fixtures are ready; all external +mutations remain unapplied until the next gate. + +## 7. Approval gate A — staging credential boundary + +Present for approval: + +1. exact staging AWS trust mutation; +2. exact target role and OIDC subject; +3. proof that publication and production authority remain absent; +4. the single staging archive to be used; +5. expected State/Git non-mutation; and +6. rollback or removal steps. + +After approval: + +- [ ] Apply only the approved staging trust change. +- [ ] Run one credentialed staging release unwrap and reconstruction. +- [ ] Verify consume-before-unwrap and identical reuse refusal. +- [ ] Remove AWS authority before reconstruction execution. +- [ ] Verify source allowlist, no plaintext artifact, no State/Git mutation, + and cleanup. +- [ ] Revoke or remove temporary authority that is no longer required. + +Then present the production **Wrap-only** role connection separately: + +- [ ] Apply only after explicit approval. +- [ ] Prove the role can wrap for the exact production archive subject. +- [ ] Prove it cannot unwrap. +- [ ] Do not accept a production submission during this preflight. + +Exit condition: new production submissions can receive safe envelopes and the +release path has passed a credentialed staging boundary. + +## 8. Phase 3 — final staging acceptance + +- [ ] Deploy the exact candidate version to staging through the normal + protected path. +- [ ] Run one successful browser submission. +- [ ] Run one successful source-bound headless submission. +- [ ] Run the bounded lifecycle route-family cases from Phase 2. +- [ ] Run one deliberate rejection or authorization failure. +- [ ] Reconstruct one accepted archive through the credentialed staging release + path with publication disabled. +- [ ] Verify no source or credential appears in public logs or artifacts. +- [ ] Exercise the reviewed disable/rollback path. +- [ ] Confirm staging State validates after the rehearsal. + +Do not rerun broad historical matrices merely to obtain newer timestamps. + +## 9. Approval gate B — production launch + +Prepare one compact go/no-go packet specified by completion-plan section 7.5. + +The requested decisions must be explicit and separate: + +- [ ] enable automatic release controller; +- [ ] enable the approved public lifecycle APIs; +- [ ] enable production intake; and +- [ ] publish the overlap announcement. + +No approval is implied by a green staging run. + +## 10. Phase 4 — launch + +After explicit approval: + +### 10.1 Release controller + +- [ ] Confirm no release is currently due. +- [ ] Enable the controller in a single-purpose change. +- [ ] Verify configuration, protected State access, and publication posture. + +### 10.2 Lifecycle APIs + +- [ ] Enable only backfill, repair/retraction, maintainer decisions, + alias/rename, and release opt-out. +- [ ] Keep model consolidation disabled. +- [ ] Verify effective public health and one non-mutating authorization denial. + +### 10.3 Intake + +- [ ] Enable production intake through the finite-lease controller. +- [ ] Verify the exact active version, lease transition, durable state, and + protected State coherence. +- [ ] Submit one tightly controlled production canary only if it was part of + the approved go/no-go packet. +- [ ] Verify archive completion, evaluation dispatch, State, Result, + leaderboard presentation, and release scheduling. + +### 10.4 Announcement + +- [ ] Publish the server entry path and four-week overlap dates. +- [ ] State that issue intake remains available during the overlap. +- [ ] Give at least two weeks' notice before eventual issue-intake closure. + +Exit condition: new production submissions traverse the promised lifecycle and +the system can be paused through the documented path. + +## 11. Phase 5 — four-week overlap + +- [ ] Monitor severity-high incidents and readiness failures. +- [ ] Monitor State validation, archive completion, evaluation dispatch, + release scheduling, and automatic releases. +- [ ] Monitor submitter adoption of the new path. +- [ ] Keep issue intake available. +- [ ] Pause server intake if confidentiality, State consistency, or release + safety fails. +- [ ] Extend the overlap rather than closing on schedule if a serious incident + or inadequate adoption remains. +- [ ] Maintain the final append-only Results delta for issue submissions. + +Do not turn monitoring output into a permanent incident-history appendix. + +## 12. Phase 6 — historical completion + +Historical lanes can run in parallel with the overlap. + +### 12.1 Final inventory + +- [ ] Freeze the final issue-intake cutoff. +- [ ] Generate and validate the append-only inventory delta. +- [ ] Reconcile public, private, and unavailable counts against every accepted + Result. +- [ ] Ensure no accepted Result disappears or changes identity. + +### 12.2 Public source + +- [ ] Retain the final canonical public replay plan and exact toolchain/source + mappings. +- [ ] Review each `source_unavailable` classification for its terminal State + disposition. +- [ ] Build/qualify only images used by replayable results. + +### 12.3 Private archives + +- [ ] Reconcile exact archive/result bindings and explicit orphans. +- [ ] Prepare a dedicated migration Wrap role and exact OIDC trust. +- [ ] Obtain the legacy identity from its custodian only for the approved run. +- [ ] Stop for explicit infrastructure/credential approval. +- [ ] Rewrap recoverable archives without changing ciphertext archive bytes or + stable IDs. +- [ ] Verify and remove temporary authority and plaintext. + +### 12.4 Replay + +- [ ] Serialize or otherwise bound replay according to the existing controller. +- [ ] Restore exact original source, benchmark, toolchain, comparator, + lean4export, and nanoda pins. +- [ ] Execute the official Lean kernel path and nanoda only. +- [ ] Record terminal outcomes with bounded retries. +- [ ] Publish redacted verdicts and measurements. +- [ ] Confirm every final-cutoff Result has a replay or reviewed unavailable + disposition. + +No experimental checker or promotion work may be added to close this phase. + +## 13. Phase 7 — remaining product completion + +### 13.1 Open problems + +- [ ] Add or verify the neutral open-problems tab. +- [ ] Confirm the empty state is clear and visually intentional. +- [ ] Confirm it has no FC branding, importer, synchronization, or disproof + dependency. + +### 13.2 Software verification and editorial state + +- [ ] Verify both reviewed software-verification drafts render correctly. +- [ ] Verify provisional/draft policy text. +- [ ] Complete the maintainer-selected human statement/citation review. +- [ ] Confirm no agent-authored hints were introduced. +- [ ] Leave verified-calculation runner infrastructure unimplemented. + +### 13.3 Retire issue intake + +- [ ] Confirm at least four weeks of announced overlap. +- [ ] Confirm at least two weeks of closure notice. +- [ ] Confirm no unresolved severity-high incident. +- [ ] Confirm adequate adoption and stable end-to-end operation. +- [ ] Confirm the final historical cutoff/delta is recorded. +- [ ] Close issue intake in a single-purpose repository change. +- [ ] Verify the server path remains available and documented. + +## 14. Final audit and definition of done + +- [ ] Check every completion criterion in completion-plan section 13. +- [ ] Search every allowlisted repository for stale FC, disproof, + experimental-kernel, model-consolidation-launch, and persistent-harness + instructions. +- [ ] Confirm remaining mentions are historical context or explicit exclusions, + not TODOs. +- [ ] Confirm current infrastructure and rollback documents contain current + facts only. +- [ ] Confirm no unexplained open overhaul PR, active workflow, or local-only + required change remains. +- [ ] Run final repository validation with no errors or linter warnings. +- [ ] Mark this runbook complete and summarize current operation and ordinary + maintenance ownership. + +The overhaul is not complete merely because a token budget, agent session, or +calendar period ends. It is complete only when the completion-plan criteria are +actually satisfied. + +## 15. Compact status table + +Update this table in place; do not append a history beneath it. + +| Phase | State | Current blocker | +| --- | --- | --- | +| 0. Rebaseline cleanup | Not started | Review and merge scoped deletions | +| 1. Disabled baseline | Not started | Phase 0 | +| 2. Repository launch preparation | Not started | Phase 1 | +| Approval A. Staging credentials | Blocked on explicit approval | Exact mutation not yet presented | +| 3. Final staging acceptance | Not started | Approval A | +| Approval B. Production launch | Blocked on explicit approval | Go/no-go packet incomplete | +| 4. Launch | Not started | Approval B | +| 5. Four-week overlap | Not started | Production launch | +| 6. Historical completion | Not started | May begin after Phase 1; infrastructure steps approval-gated | +| 7. Remaining product completion | Not started | Independent lanes; issue closure waits for overlap and final delta | +| Final audit | Not started | All phases | +