Skip to content

Document post-launch intake hardening #635

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
kim-em merged 3 commits into from
Sep 13, 2026
Merged

Document post-launch intake hardening #635

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
3291ce3
Document post-launch intake hardening
kim-em Sep 13, 2026
e5a47b2
docs: distinguish historical delta from baseline
kim-em Sep 13, 2026
0a4296b
docs: record hardened intake deployment
kim-em Sep 13, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
15 changes: 15 additions & 0 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down
31 changes: 27 additions & 4 deletions docs/overhaul-execution-runbook.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 |
Expand All @@ -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
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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.

Expand All @@ -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 |
Expand Down