docs: recalibrate overhaul approval gates

docs/overhaul-completion-plan.md

@@ -241,8 +241,8 @@ Read-only verification must establish the current exact versions and that:
 
 ### 7.3 Credential and key boundary
 
-- Repair the staging release OIDC trust mismatch through an explicitly
-  approved infrastructure change.
+- Repair the staging release OIDC trust mismatch through a reviewed,
+  fail-closed 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,
@@ -276,8 +276,11 @@ Prepare a compact packet containing:
 - 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.
+Production capability enablement requires one explicit maintainer go/no-go even
+when all preparation work is otherwise autonomous. The packet must make the
+release controller, lifecycle APIs, intake and production canary, and overlap
+announcement separately visible, but the maintainer may approve them together
+in one response.
 
 ## 8. Launch and overlap
 
@@ -386,19 +389,42 @@ Autonomous implementation is allowed only in this LeanEval repository family:
 
 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.
+run ordinary repository CI. They may also autonomously make reviewed,
+reversible infrastructure and credential-boundary changes when all of the
+following are true:
+
+- the change is confined to LeanEval-owned resources;
+- production intake, replay, publication, and public lifecycle capabilities
+  remain disabled;
+- the change cannot affect the old issue-intake path or an existing user;
+- it does not disclose, destroy, or irreversibly rotate a credential or key;
+- it does not make an irreversible canonical production-data change; and
+- a tested rollback or fail-closed recovery exists.
+
+This includes isolated staging and qualification resources, disabled-state
+deployments, narrowly scoped role-trust repair, Wrap-only connection and
+synthetic preflight, and dedicated migration infrastructure while its consumer
+remains disabled. The mere fact that an operation uses AWS, Cloudflare, GitHub
+environments, deploy keys, or scoped credentials is not by itself a reason to
+interrupt the maintainer.
 
 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.
+2. enabling production intake, replay, publication, or public owner/maintainer
+   behavior, including the production canary and the public launch
+   announcement;
+3. an irreversible or destructive production-data, credential, or key change,
+   including final destruction of the legacy archive identity;
+4. retiring the old issue-intake path; and
+5. a material product-scope expansion.
+
+An authenticated maintainer action needed because the agent lacks access is an
+operator handoff, not an approval gate. Present the reviewed command and its
+expected readback, but do not describe the maintainer's login as permission for
+an otherwise autonomous isolated change. Safety-preserving disable and rollback
+actions never wait for approval.
 
 No technical dependency is permission to work in an external repository.
 Prepare a local compatibility workaround or stop and request authority.
@@ -442,4 +468,3 @@ The lifecycle overhaul is finished when all of the following are true:
 - 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.
-

docs/overhaul-execution-runbook.md

@@ -17,7 +17,7 @@ comment, or original-plan clause conflicts with it, the completion plan wins.
 At adoption, the intended safe posture is:
 
 - production intake disabled;
-- staging general replay disabled except for explicitly approved isolated work;
+- staging general replay disabled except for bounded isolated work;
 - production replay disabled;
 - automatic publication disabled;
 - public result-owner, maintainer, and model-identity gates disabled;
@@ -35,23 +35,36 @@ 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.
 
+Reviewed and reversible LeanEval infrastructure preparation is also autonomous
+when production capabilities remain disabled, existing users and old issue
+intake cannot be affected, no canonical production data or credential is
+destroyed, and rollback is tested. This includes isolated Cloudflare
+qualification, staging enable/disable windows, narrowly scoped AWS trust
+repair, Wrap-only connection and synthetic preflight, and disabled migration
+infrastructure. Do not turn a missing local login into a permission question:
+prepare an operator handoff when authenticated execution is required.
+
 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
+- enabling production intake, replay, publication, public lifecycle APIs, or a
+  production canary;
+- publishing the launch announcement that starts the old-intake overlap;
+- making an irreversible or destructive production-data, credential, or key
+  change;
+- retiring old issue intake; 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.
+At a genuine approval gate, present the exact mutation, target, user impact,
+rollback, and read-only precondition. One coherent go/no-go may cover a
+declared production launch or historical replay program; do not split it into
+ceremonial approvals for each reversible implementation step. Safety-preserving
+disable and rollback actions proceed immediately.
 
 ### 3.3 Keep changes reviewable
 
@@ -226,6 +239,10 @@ staging acceptance gate.
 
 - [x] Select the exact candidate commits across the repository family.
 - [x] Use synthetic private source repositories owned for staging.
+- [ ] Prefer an allowlisted source fixture for the final rehearsal. If the
+      source-bound protocol genuinely requires an external repository, stop
+      only for the exact runtime-generated repository, ref, and proof-file
+      mutation; do not ask for broader standing authority.
 - [x] Prepare one browser and one source-bound headless submission.
 - [x] Include one deliberate invalid or unauthorized case.
 - [x] Confirm archive-before-evaluation and schema-version-3 binding.
@@ -238,18 +255,10 @@ staging acceptance gate.
 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:
+## 7. Autonomous credential-boundary preparation
 
-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:
+The staging boundary has been exercised with production and publication
+authority absent:
 
 - [x] Apply only the approved staging trust change.
 - [x] Run one credentialed staging release unwrap and reconstruction.
@@ -260,20 +269,21 @@ After approval:
 - [x] Confirm the one-use grant was consumed and workflow AWS credentials were
       cleared before reconstruction.
 
-Then present the production **Wrap-only** role connection separately:
+Complete the production **Wrap-only** connection autonomously while intake
+remains disabled:
 
-- [ ] After explicit approval, connect repository environment
+- [ ] Connect repository environment
       `archive-production` variable `AWS_WRAP_ROLE_ARN` to
       `arn:aws:iam::161072922960:role/lean-eval-archive-wrap-production`.
 - [ ] Dispatch the immutable-tag preflight that encrypts a synthetic key for the
       exact production archive subject.
 - [ ] Require that same preflight to prove decrypt is denied.
 - [ ] Do not accept a production submission during this preflight.
 
-Present the production release-role trust repair as a second, independent
-approval:
+Complete the isolated production release-role trust repair autonomously while
+publication remains disabled:
 
-- [ ] After separate explicit approval, change only the trust on
+- [ ] Change only the trust on
       `lean-eval-release-unwrap-invoker-production` from the obsolete name-only
       subject to
       `repo:leanprover@7233018/lean-eval-releases@1340741242:environment:release-production`.
@@ -301,18 +311,20 @@ release path has passed a credentialed staging boundary.
 
 Do not rerun broad historical matrices merely to obtain newer timestamps.
 
-## 9. Approval gate B — production launch
+## 9. Genuine approval gate — production launch
 
 Prepare one compact go/no-go packet specified by completion-plan section 7.5.
 
-The requested decisions must be explicit and separate:
+The packet must show these decisions separately, but they form one coherent
+launch go/no-go and may be approved in one response:
 
 - [ ] 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.
+No approval is implied by a green staging run. Ordinary preparatory changes do
+not consume or imply this user-impact approval.
 
 ## 10. Phase 4 — launch
 
@@ -369,6 +381,11 @@ Do not turn monitoring output into a permanent incident-history appendix.
 
 Historical lanes can run in parallel with the overlap.
 
+Old issue intake remains live during the overlap and can append Results-only
+commits to submissions `main`. Process the retained baseline now using immutable
+dispatch tags; do not demand a quiet protected branch. Maintain an append-only
+delta, and treat only the announced issue-intake cutoff as the final corpus.
+
 ### 12.1 Final inventory
 
 - [ ] Freeze the final issue-intake cutoff.
@@ -394,19 +411,31 @@ terminal State dispositions.
 - [ ] Review each `source_unavailable` classification for its terminal State
       disposition.
 - [ ] Build/qualify only images used by replayable results.
+- [x] Qualify the final missing image from the retained baseline plan in an
+      isolated replay-disabled Worker.
+- [ ] Commit and validate its generated qualification profile.
 
 ### 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.
+- [ ] Obtain the legacy identity from its custodian only for the bounded run;
+      this is an authenticated operator action, not a ceremonial approval.
+- [ ] Build and qualify only the exact private replay images used by the
+      retained baseline inventory.
 - [ ] Rewrap recoverable archives without changing ciphertext archive bytes or
       stable IDs.
 - [ ] Verify and remove temporary authority and plaintext.
+- [ ] Keep every legacy identity copy until the final issue-intake delta is
+      closed; obtain explicit approval before irreversible destruction.
 
 ### 12.4 Replay
 
+- [ ] Prepare one exact historical replay go/no-go packet covering the reviewed
+      public and private queues, append-only State effects, redacted public
+      projection, controller scopes, and rollback.
+- [ ] Obtain one explicit approval before enabling production replay or
+      appending the approved canonical terminal-disposition program.
 - [ ] Serialize or otherwise bound replay according to the existing controller.
 - [ ] Restore exact original source, benchmark, toolchain, comparator,
       lean4export, and nanoda pins.
@@ -442,6 +471,8 @@ No experimental checker or promotion work may be added to close this phase.
 - [ ] Confirm no unresolved severity-high incident.
 - [ ] Confirm adequate adoption and stable end-to-end operation.
 - [ ] Confirm the final historical cutoff/delta is recorded.
+- [ ] Obtain one explicit closure decision because this removes the path used
+      by existing issue-intake users.
 - [ ] Close issue intake in a single-purpose repository change.
 - [ ] Verify the server path remains available and documented.
 
@@ -474,11 +505,11 @@ Update this table in place; do not append a history beneath it.
 | 0. Rebaseline cleanup | Complete | — |
 | 1. Disabled baseline | Complete | — |
 | 2. Repository launch preparation | In progress | Complete the exact-version bounded lifecycle rehearsal |
-| Approval A. Staging credentials | Staging complete; production pending | Separate explicit approvals for the production Wrap-role environment connection/preflight and release-role trust repair/preflight |
+| Credential boundary | Staging complete; production preparation pending | Complete autonomous Wrap-only and release-trust preflights while production remains disabled |
 | 3. Final staging acceptance | In progress | Complete only the missing final-candidate lifecycle cases, then return every gate to disabled |
-| Approval B. Production launch | Blocked on explicit approval | Go/no-go packet incomplete |
-| 4. Launch | Not started | Approval B |
+| Production launch go/no-go | Not ready | Finish the exact final staging packet and current launch readbacks |
+| 4. Launch | Not started | One production launch go/no-go |
 | 5. Four-week overlap | Not started | Production launch |
-| 6. Historical completion | In progress | Record terminal State dispositions for the current source-unavailable public cases, execute the reviewed byte-preserving private rewrap and official-kernel-plus-nanoda replay, and freeze the final cutoff; credential steps remain gated |
+| 6. Historical completion | In progress | Finish baseline profiles and private rewrap preparation; production replay and canonical dispositions wait for one exact go/no-go; final delta waits for cutoff |
 | 7. Remaining product completion | In progress | Only issue closure remains, waiting for overlap and final delta; catalog lifecycle cutover, open-problems, and editorial work are complete |
 | Final audit | Not started | All phases |