diff --git a/README.md b/README.md index b1074fd3..862eaee2 100644 --- a/README.md +++ b/README.md @@ -316,6 +316,21 @@ Apache License 2.0 exactly two UTC calendar months after acceptance. A submitter who initially chooses private source may later change that choice once to scheduled release. +The service takes a problem ID and resolves its group and current statement +revision from the protected LeanEval catalog; clients do not supply those +canonical fields. Formalization problems must be visible and active. +Software-verification problems may be visible and draft or active. Public +source repositories must use scheduled publication; withholding is available +only for private repositories. + +Before acceptance, the submitter explicitly authorizes private fetch, archive, +build, and execution of the exact commit, indefinite encrypted retention even +after rejection or failure, and public display of the result and submitted +metadata. Do not submit secrets. Every new request is archived with a fresh +per-submission key envelope before evaluation, and the service evaluates only +the selected problem. Exact resubmissions by the same owner return the original +submission, and each owner may have at most four active submissions. + This repository (`leanprover/lean-eval`) holds only the problem set and the comparator/sandbox integration. diff --git a/docs/overhaul-execution-runbook.md b/docs/overhaul-execution-runbook.md index e4d28366..d0c7d55e 100644 --- a/docs/overhaul-execution-runbook.md +++ b/docs/overhaul-execution-runbook.md @@ -146,7 +146,7 @@ invalidate these bindings. Section 5.2 records the deployed runtime separately. | Repository | Durable checkpoint | Protection state | | --- | --- | --- | | `lean-eval` | Completion-plan and runbook checkpoint `59c0c18b2d14015589927b6e810386025c93ba4b` | Required `verify` | -| `lean-eval-submissions` | Protected main and deployed production Worker `0aef118adbe2e2e48917827839c6b37714cc7c50` | Required `verify` | +| `lean-eval-submissions` | Protected main and deployed production Worker `98d7172786fad65c02173d49eccf415a32e2285d` | Required `verify` | | `lean-eval-leaderboard` | Protected and deployed main `939d69c88292358adf60b124f29605215a1e422a` | Required `build`; exact Pages deployment and live readback complete | | `lean-eval-state` | Retained-baseline checkpoint `76b3b3e54f4be69161a00cd81576a58df8eae815` | Required `validate`; append-only descendants allowed | | `lean-eval-state-staging` | Launch-acceptance checkpoint `0849a95026ea3491ec55f1e0ef3b6ff2dff00fd5` | Required `validate`; append-only descendants allowed | @@ -157,7 +157,7 @@ invalidate these bindings. Section 5.2 records the deployed runtime separately. ### 5.2 Deployed services Production serves deployed submissions implementation -`0aef118adbe2e2e48917827839c6b37714cc7c50` with durable intake and exactly +`98d7172786fad65c02173d49eccf415a32e2285d` with durable intake and exactly the approved lifecycle routes enabled. Deployment, CI, readiness, health, and protected-State validation pass. Staging intake and public lifecycle routes remain disabled, with its promotion @@ -502,6 +502,24 @@ write-free no-op, and enabled no-due-work pass all succeed. - [x] State that any eventual issue-intake closure requires at least two weeks' notice. +### 10.5 Post-launch P0/P1 hardening + +- [x] Make server submissions evaluate only the catalog problem and statement + revision accepted into State; keep workspace scanning only in the + temporary legacy issue lane. +- [x] Align the public State projection and leaderboard adapter on all current + historical counter-unavailability reasons. +- [x] Add immutable exact-submission claims and per-owner intake indexes to + both production and staging State. +- [x] Deploy clean-break intake API schema version 2. The server resolves group + and revision from protected benchmark `main`, requires current terms, + rejects withheld publication for public repositories, deduplicates exact + submissions, and permits at most four active submissions per owner. +- [ ] Update the submission service, stable submit page, and repository guide + to describe the same contract and remove superseded overhaul narratives. +- [ ] Read back production health and exercise one bounded exact submission + after the hardened Worker is deployed. + Exit condition: the launch commit is live, new production submissions traverse the promised lifecycle, and the system can be paused through the documented path. @@ -553,6 +571,11 @@ binding has SHA-256 Non-v1 historical Results remain available for later replay work but do not block this overhaul. +The completed historical baseline contains 1,301 terminal in-scope records. +At the 2026-09-13 reconciliation, 80 later legacy issue-intake records formed +the append-only post-baseline delta. That delta may grow until issue intake is +frozen; keep it separate from the already terminal historical baseline. + ### 12.1 Frozen v1 scope - [x] Freeze and validate the v1 problem-set binding. @@ -669,7 +692,7 @@ checker or persistent qualification machinery may be added to this phase. Production launch restore `39b2e67f7583926a4f1d66b723b5d4cf4756dd32` is live through deployed descendant -`0aef118adbe2e2e48917827839c6b37714cc7c50` with durable intake. Full +`98d7172786fad65c02173d49eccf415a32e2285d` with durable intake. Full completion is deliberately calendar-bound and occurs only when every completion-plan criterion is actually satisfied. @@ -685,7 +708,7 @@ Update this table in place; do not append a history beneath it. | Credential boundary | Complete | — | | 3. Final staging acceptance | Complete | — | | Production launch readiness | Complete | — | -| 4. Launch | Complete: backend `0aef118adbe2e2e48917827839c6b37714cc7c50` live with durable intake; leaderboard `939d69c88292358adf60b124f29605215a1e422a` protected, deployed, and read back | — | +| 4. Launch | Live; clean-break intake v2 deployed | Merge the updated public guidance and complete one bounded production readback | | 5. Four-week overlap | In progress; automatic publication, durable server intake, and server-primary entry live; calendar-bound; future cutoff variable installed | Keep issue intake open through at least `2026-09-30T06:57:10Z`; the conditional closure notice matures `2026-09-16T23:06:35Z`, and the canary automatic-release checkpoint is `2026-11-02T03:50:01.002Z` | | 6. Historical completion | Complete: v1 public and private queues are terminal; no replay or task-scoped private resource remains; temporary controllers and qualification machinery are removed | — | | 7. Remaining product completion | In progress | Open problems and editorial work are complete; final live release/replay presentation and issue closure retain their calendar, stability, adoption, and readiness gates |