[lifecycle overhaul] implementation tracker

[kim-em]

[lifecycle overhaul] implementation tracker

Tracks implementation and production rollout of the plan in
lean-eval#536 and the
public implementation program.

Terminology: unqualified v1 and v2 name problem sets. The platform
work is the lifecycle overhaul; machine-format versions are always
qualified as schema version 2. Frozen identifiers and filenames remain
unchanged.

The detailed decision and operator procedures live in
docs/overhaul-rollout-runbook.md. Use this single tracker rather than opening
one issue per lane.

Decisions

• D1: keep raw production and staging State private and publish a
  reproducible, schema-validated public projection.
• D2: mechanical base rule selected: visible formalization-evaluation
  problems with fewer than three accepted solves and no public submission
  (118 at the audited snapshot). Ten later merged problems were explicitly
  approved as additions; the final frozen v1 set has 128 members.
• D3: approve both software-verification statements; retain both problems,
  apply the researched title/prose/citation corrections, and add the three
  agreed anti-vacuity requirements before publication.
• D4: use isolated temporary account lean-eval
  (a46b90978a1c29cc4795f30677e7e4b8) and exact
  lean-eval.workers.dev endpoints for the intake-disabled bootstrap;
  never reuse or rename the Palomar subdomain. Kim Morrison is
  administrator and temporary cost owner. A later organization-account or
  provider migration is supported by the stable contracts, not required
  for this bootstrap. This decision authorizes only the intake-disabled
  bootstrap; production intake still requires either the locked
  organization-owned hostname/OAuth design or an explicit recorded
  amendment to that launch requirement.
• D5: bootstrap with separate Kim-owned fine-grained PATs for staging and
  production State, each single-repository scoped and at most 90 days;
  rotate at least 14 days before expiry. The bootstrap is approved for
  initial staging and production intake once each token and its narrowly
  named ruleset bypass pass an environment-specific write test.
• D6: approve key lifecycle, one-submission capability, contributor
  acknowledgement, and license wording before private intake/release. D6a
  selects a new dedicated AWS account with AWS KMS behind a
  provider-neutral wrap/unwrap adapter; migration rewraps identities without
  changing archives or stable IDs. D6b accepts no provider-loss recovery.
  The capability implementation is delegated to the implementation review;
  concise contributor/release wording is approved.
• D7: approve fresh dry run 32569220655 at source ddc0e4ec, source
  digest 884c3837, 1,298 records, and output digest b78fb207; apply run
  32569936026 completed as c3491661 and independent validation passed.
• D8: acknowledge UUID-prefix State paths and the durable Git writer lock
  as correctness-preserving deviations from the literal program text.
• D9: use two least-privilege GitHub Apps behind an organization-operated
  token broker; implementation identifiers are recorded when provisioned.
• D10: use a two-UTC-calendar-month embargo and initially plan a four-week
  issue-intake overlap. A later explicit maintainer decision may shorten
  the issue overlap and must be announced before closure.

Repository and contract foundations

• Create and publish lean-eval-generator.
• Create and publish production State with the D1 visibility.
• Create and publish staging State with the D1 visibility.
• Create and publish disabled lean-eval-releases tooling.
• Replace LeanEval's local generator path with an exact public commit SHA.
• Verify generator byte parity after the remote pin (theorem- and
  definition-hole fixtures, 10/10 files each).
• Merge generator fixes lean-eval-generator#1 / #2 and synchronization
  PR #3, advance exact pins, rerun corpus parity, and merge the
  embedded-core removal in lean-eval#553. All three generator PRs merged
  into exact main commit 77373a53; consumer #553 merged as
  b91d4757, after local parity/build/test checks and hosted run
  32559642804 passed all eight catalog shards, the inventory aggregate,
  repository checks, and security/scoring smoke tests.
• Configure State rulesets and append-only validation.
• Publish the schema-validated public projection of private production
  State without exposing private source or operational metadata
  (lean-eval-state#4; staging mirror lean-eval-state-staging#4).
• Complete lifecycle-aware leaderboard consumption and publish the exact
  validated projection (lean-eval-leaderboard#72, merge dd5d508d; Pages
  deployment run 32557778003).

Existing-repository PRs

• Open catalog lifecycle/tags/audit PR.
• Open results schema version 2 compatibility and migration-tooling PR.
• Open intake-disabled Worker, deployment, rollback, threat-model, and
  infrastructure-ledger PR.
• Open lifecycle-aware leaderboard preview PR.
• Open software-verification draft PR after D3 review.
• Open LeanEval generator-consumer PR after the public generator pin exists.
• Open independent-kernel shadow smoke lean-eval-submissions#1207 and
  AWS one-submission key-adapter staging smoke #1208; both merged and
  deployed intake-disabled as exact commit a34b2053.
• Provision dedicated AWS account 161072922960, exact GitHub OIDC
  provider, and isolated staging/production key-adapter stacks. Only the
  staging wrap and replay-invoker role variables are connected; production
  remains dormant and intake-disabled.
• Pass the synthetic staging key-adapter round trip from protected immutable
  commit d487c9d5 (run 32568604230): Encrypt-only wrap, source-free
  handoff, Invoke-only unwrap, second-use rejection, authority removal, and
  local decryption. This is not a private replay/backend demonstration.
• Merge disabled release terminology lean-eval-releases#3, planner #1,
  and reconstruction smoke #2; final main is f1f83344, all hosted
  validation is green, and publication remains disabled.

Lifecycle product contracts

These are required by the authoritative product plan and remain separate from
the already implemented owner status, metadata, and publication routes.

• Add the production State representation for legacy result claims and
  metadata backfill without rewriting historical facts
  (lean-eval-state#8, merge 6ba71d2a). The v1 public projection remains
  byte-for-byte stable and the redacted lifecycle metadata is opt-in v2.
• Add the authenticated owner writer/API for those State events, including
  owner verification and exact results-Git tuple/digest recomputation;
  preserve the stable result identifier and grandfathered release policy.
• Add model-alias, rename, consolidation, and new-canonical-identity
  request events, authorization, materialization, collision tests, and
  lifecycle-aware public projection behavior.
• Add problem-repair requests and maintainer repair events with explicit
  revision/causation rules; do not rewrite prior accepted records.
• Add owner retraction requests and public maintainer override/retraction
  events, including release and leaderboard consequences.
• Add hostile-input, owner/maintainer authorization, idempotence, causal
  conflict, and public-redaction tests for every amendment flow.

Cloudflare bootstrap

• Create protected cloudflare-staging and cloudflare-production GitHub
  environments.
• Install the Cloudflare account ID in both environments.
• Install distinct scoped deployment API tokens in those environments.
• Add Containers: Edit to both existing account-scoped deployment tokens;
  operator-confirmed 2026-08-22, retaining Workers Scripts: Edit and no
  other account or zone permission. Live verification remains part of the
  first staging container deployment.
• Create the protected submission-dispatch-promotion environment and the
  immutable lean-eval-dispatch/* tag ruleset.
• Install distinct random AUTH_TOKEN_SECRET and READINESS_TOKEN values.
• Create distinct staging/production GitHub OAuth Apps with exact callback
  URLs and install their credentials.
• Deploy staging manually with intake disabled and record the Worker,
  workers.dev endpoint, account, subdomain, and version identifiers.
• Promote the same commit to production and verify the structured health
  response.
• Install distinct readiness secrets in each Worker.
• Obtain organization approval for the installed, distinct State-writer
  credentials and test each with its matching ruleset bypass (preflight
  runs 32465890236 and 32465892118).
• Implement the D9 private service-binding broker and separate source and
  dispatch authority paths.
• Deploy both private brokers and bind the intake-disabled staging and
  production Workers to them.
• Create both Apps, install the dispatcher on only the submissions
  repository, and provision both broker environments; keep the local static
  verification/dispatch-token hooks absent in production.
• Complete the ownership transfers of both broker GitHub Apps to
  leanprover; public records and protected preflights verify unchanged
  App IDs, working private keys, and dispatcher installation 155329316.
• Replace the credentialed private-gist assumption with anonymous exact-ID
  verification of GitHub's unlisted secret gist, while retaining exact
  owner/content/visibility/truncation checks and keeping the broker closed
  to /gists/.

Data and product rollout

• Produce a fresh results schema version 2 dry-run artifact.
• Review and approve dry run 32569220655 and its exact source commit,
  source digest, 1,298-record count, and canonical output digest (D7).
• Execute authorized run 32569936026; main c3491661 contains 44/44
  schema-version-2 files, the writer lock is absent, no record was lost or
  duplicated, no submission writer is queued, and main CI is green.
• Define and audit the approved mechanical 118-member v1 base set.
• Freeze the v1 set when its reviewed PR merges (lean-eval#540,
  merge commit 547b00ed345bc0737dd94847d6b67cb681b6178a).
• Add the ten explicitly approved post-audit problems in lean-eval#548;
  final v1 membership is 128 at merge 21c6c021.
• Complete staging OAuth/agent intake and exact-ref dispatch. Hosted run
  32546606639 archived the exact private fixture, produced the deliberate
  rejection, and recorded archive completion plus evaluation start/reject
  events through staging State commit b2160515; no accepted result was
  written.
• Demonstrate credential-free historical public replay (hosted run
  32499490261, workflow commit 757b0831).
• Demonstrate isolated private replay. Protected deployment run
  32573880099 and source-free acceptance run 32574078784 prove the
  12 GiB, max-one-instance, SSH-off, network-disabled Cloudflare Sandbox,
  exact GitHub OIDC boundary, fixed-command decrypt, and destruction. The
  provider-neutral contract and automatic deployment are live; general and
  production replay remain disabled.
• Verify synthetic single-archive decrypt, second-use and wrong-archive
  refusal, blocked egress, and sandbox destruction before enabling private
  replay. Evidence is recorded in INFRASTRUCTURE.md.
• Prove the same boundary with a real accepted schema-version-3 staging
  archive. Immutable-tag run 32618166048 selected submission
  01a02cb4-5e7c-7fb3-a4ab-b6fabbb72584 from State, consumed and refused
  reuse of its exact KMS capability, verified the plaintext digest and safe
  archive shape only inside the network-disabled Sandbox, and confirmed
  destruction without any write authority. Authoritative queue execution
  and production replay remain disabled.
• Demonstrate release reconstruction separately without enabling release
  or publication. Protected lean-eval-releases run 32574614106 at exact
  main commit f1f83344 planned one due synthetic release, reconstructed
  and validated its manifest, enforced the public-file allowlist, excluded
  a private fixture file, and left Git and State unchanged.
• Run the one authorized receipt-backed authoritative staging replay. Run
  32694194843 reached an explicit retryable replay.failed terminal at
  staging State commit c3c677cc with reason runner_lost; no successful
  replay evidence was fabricated. Replay was immediately disabled again in
  both environments by lean-eval-submissions#1299 at ffd9a473, deploy
  run 32700136536 passed, both live health endpoints report disabled, and
  Cloudflare reports zero active or assigned replay containers.
• Inventory every historical accepted result at the migration cutoff and
  deterministically classify it as public-source replayable,
  private-archive replayable, or explicitly unavailable with a reviewed
  reason.
• Enqueue and execute the complete historical replay corpus under exact
  original pins, recording terminal verdicts/statistics or explicit
  unavailability; the isolated staging proofs above do not satisfy this
  corpus gate.
• Expand independent-kernel validation from the one-result shadow smoke to
  a checker-series/corpus report with separately recorded
  accept/reject/decline/crash/timeout outcomes and an explicit promotion
  decision.
• Enable production intake and begin the four-week issue-intake adoption
  window.
• Complete leaderboard preview review and cut over with rollback retained
  (lean-eval-leaderboard#72; Pages run 32557778003).
• Close issue intake only after the time, incident, submitter, adoption, and
  announcement gates in the implementation program pass.

Production and operational readiness

• Make production intake enablement, normal deploy smoke, credential
  preflight, and rollback agree on one explicit expected intake state;
  keep the tracked production value disabled until the launch review.
• Provide a commit-coherent rollback procedure for the intake Worker,
  private broker, and replay Worker/container deployment unit. The
  qualified protected workflow merged as lean-eval-submissions#1300 at
  f5f830d0; main deploy run 32700644989 passed staging and production
  with intake and replay disabled. State stays append-only and
  forward-corrected.
• Add the exact staging promotion canary required by the program: GitHub
  connectivity, synthetic intake, CAS contention, and scheduled
  reconciliation before a production candidate is promoted.
• Validate the release controller's State and release-repository write
  credentials without AWS decrypt or publication. Protected run
  32694754911 at release commit 2a4cdff2 passed both exact-ref dry-run
  pushes while publication remained absent.
• Pass the credentialed staging release smoke after the live AWS OIDC trust
  update. Keep publication disabled until its separate launch gate.
• Add the publication-disabled confidentiality-incident recovery planner
  (lean-eval-releases#8, merge d66c8dd), including strict original
  publication bindings, canonical shared-path classification, and a
  fail-closed remediation plan that performs no mutation.
• Complete and merge the immutable release.removed State correction
  contract, then bind the recovery planner to it and qualify the protected
  repository-removal/history-cleanup procedure without rewriting results.
• Record and deploy the readiness monitor, alert destination, severity
  owner, support contact, emergency intake-pause owner, and response
  procedure (lean-eval-submissions#1301, merge 58d88268). Main deploy
  run 32701229915 passed in both environments with intake/replay disabled;
  protected live monitor run 32701461244 then verified the exact deployed
  commit and reconciled the bot-owned incident state.
• Move the production hostname and OAuth Apps to organization ownership as
  required by the locked program, or record an explicit reviewed amendment
  authorizing the temporary workers.dev/owner arrangement for launch.
• Reconcile the rollout runbook, infrastructure current-version table,
  credential rotation/revocation data, and public implementation tracker
  after each remaining protected rollout.

External coordination

• Coordinate the published generator contract through lean-eval#533 and
  formal-conjectures#4951.
• Close the whole-FC100 extraction findings in the FC-owned importer:
  current formal-conjectures#4951 imports, verifies, classifies, and
  generates all 100 declarations (92 research-open and 8 research-solved).
  Its pinned baseline builds 97/100 at LeanEval pins with three exact known
  failures; generator PRs #1 / #2 retire Erdos125, and the independently
  verified FC toolchain bump retires the remaining two.
• Reproduce the FC100 dependency audit before import: 100/100 declarations
  resolved, 280 closure edges, no target-to-target dependency, and one
  fail-closed Erdos324.erdos_324.match_1 orphan recorded upstream.
• Obtain a compatible FC-owned importer/output contract with strict,
  deterministic provenance as a reference implementation
  (formal-conjectures#4951, previously green at head
  2654e42de2026de6cdb248ad5ed0f1c7d659c8fa). The draft must still be
  reconciled with current FC main, current Lean pins, and maintainer
  review before it is launch-ready.
• Launch FC100/open-conjectures only after generator pins advance, the
  importer receives FC maintainer review, and the production launch gates
  are satisfied.
• Complete the human-authored flavour-text/hint audit; tooling may inventory
  missing or stale text, but agents do not author hints.
• After FC100 proof-only launch, coordinate comparator disproof support and
  add the generator/manifest disproof contract once the upstream comparator
  integration lands.

[kim-em]

Initial implementation links:

• plan and catalog/generator/software foundations: feat: implement catalog and generator overhaul foundations #540
• results schema-version-2, intake-disabled Worker, archive, and replay foundations: feat: add intake server and results schema version 2 foundations lean-eval-submissions#1165
• lifecycle-aware leaderboard preview: feat: add lifecycle-aware leaderboard preview lean-eval-leaderboard#69
• public generator: https://github.com/leanprover/lean-eval-generator
• private production and staging State repositories have been created
• disabled release tooling: https://github.com/leanprover/lean-eval-releases

D7 migration remains unapplied pending the post-merge exact checksum confirmation.

[kim-em]

Overnight checkpoint (2026-08-20):

• lean-eval-leaderboard#69 is merged at 8150f8e556743bb1b1773bc441c90258f0bc7e03.
• The post-merge Pages run completed successfully: https://github.com/leanprover/lean-eval-leaderboard/actions/runs/32386338792 (catalog visibility, schema-version-2 artifacts, and internal links all passed). The existing / remains the default; /eval/preview/ is deployed for review, so cutover remains intentionally pending.
• Production/staging State operational-contract heads 89cdf9b / 6bfc9eb both have green append-only validation.
• The public implementation gist was corrected to remove every chonk dependency and the unrequested recovery-drill requirements. Private replay is a disabled, provider-neutral LeanEval boundary pending a dedicated backend and D6 capability approval: https://gist.github.com/kim-em/cd6ac1c049f459ef9aa37d6cf551d9e4
• Trusted regeneration from the frozen catalog merge is still running; results migration D7 remains unapplied.

[kim-em]

Regeneration/snapshot checkpoint:

• Trusted regeneration succeeded: https://github.com/leanprover/lean-eval/actions/runs/32386142028
• Bot-generated main commit: 5b63d702014cc96670599d2ec0aaf284e708547c (generated/ refreshed; 300 files changed). The generated index has lifecycle metadata, eight hidden entries, and no legacy test field.
• Automatic leaderboard snapshot advance succeeded: https://github.com/leanprover/lean-eval-leaderboard/actions/runs/32393202854
• Leaderboard main is now a438b83ffd400eecfc5a701115597366ba4809cc, with .benchmark-commit pinned exactly to 5b63d702014cc96670599d2ec0aaf284e708547c.
• Fresh main CI and the post-snapshot Pages deployment are running. D7 remains unapplied.

[kim-em]

Final overnight validation:

• Regenerated LeanEval main CI is fully green: https://github.com/leanprover/lean-eval/actions/runs/32393191801
• Snapshot-pinned leaderboard Pages build/deploy is fully green: https://github.com/leanprover/lean-eval-leaderboard/actions/runs/32393944197
• Live smoke: /eval/ serves the existing default with no preview banner; /eval/preview/ serves the lifecycle-aware preview.
• lean-eval#542 is merged at 5aa9a51e2f423e7aeb164e40641e2ee08acf9567, marking the RFC accepted and making the implementation program/tracker authoritative; its follow-up CI is green: https://github.com/leanprover/lean-eval/actions/runs/32395926280
• lean-eval-submissions#1165 remains deliberately unmerged and green pending the manual credentials in docs/overhaul-manual-setup.md. D7 remains deliberately unapplied.

[kim-em]

Approval and rollout checkpoint (2026-08-21):

• Both State-writer fine-grained PATs are approved. Live protected-main preflights passed without tree changes: staging run 32465890236 at 6bfc9eb; production run 32465892118 at 89cdf9b.
• GitHub Apps 4666604 and 4666633 now publicly report owner leanprover with the reviewed permission split and unchanged IDs.
• The post-archive State reconciliation landed in lean-eval-submissions#1182, merge bfc8a68. Its source-free callback is live in staging and production, protected by distinct environment secrets; deployment 32467344618 passed both exact-commit intake-disabled smoke gates.
• A protected staging-only intake-state workflow landed in lean-eval-submissions#1183, merge c87c77c. It has no production target.
• The final v1 named set is 128 members after lean-eval#548, merge 21c6c021 (mechanical 118 plus ten explicitly approved additions).
• Private staging fixture kim-em/lean-eval-intake-fixture@ae38f4d is ready with a deliberately rejected proof, so the staging exercise cannot add a successful public result. Source Reader installation on that single fixture and browser OAuth execution remain.

Production intake remains disabled. D7 remains unapplied.

[kim-em]

Staging-control checkpoint:

• Protected staging control merged in lean-eval-submissions#1183; the false-alarm Cloudflare convergence window discovered on first use was fixed in #1184.
• Exact-commit deploy run 32468264421 is green at 60f7ef62.
• Protected staging enable run 32468488368 passed. Live health now reports staging intake_enabled=true at 60f7ef62; production remains intake_enabled=false at the same commit.
• The staging OAuth start route returns the exact registered client ID and callback URL.

Remaining human step before the synthetic browser submission: install lean-eval-source-reader only on private fixture kim-em/lean-eval-intake-fixture. D7 remains untouched.

[kim-em]

Source Reader installation is now conclusively verified. Run 32470794718 used the transferred App private key through the deployed staging service-binding broker and read exact private fixture kim-em/lean-eval-intake-fixture; identity and private=true both matched. The durable staging-only preflight landed in lean-eval-submissions#1185, merge 2cfc0a77. Staging intake was re-enabled at that exact commit by run 32470823574; production remains disabled.

[kim-em]

Staging browser intake is now deployed and ready for the human OAuth smoke:

• browser UI: Add minimal browser submission page lean-eval-submissions#1186, merged as 42f9d1989ff825dde862a660fdaa9f358dce2972
• exact-revision deploy: https://github.com/leanprover/lean-eval-submissions/actions/runs/32471730369 (green; immutable dispatch tag resolves to the same commit)
• protected staging enable: https://github.com/leanprover/lean-eval-submissions/actions/runs/32471971561 (green)
• live staging /healthz: commit 42f9d198..., intake_enabled: true
• live production /healthz: same commit, intake_enabled: false; production root exposes no form
• OAuth start redirects to the staging OAuth App/client and exact configured callback.

No staging submission has been recorded yet: the staging State head is still 6bfc9eb... (2026-08-20), and no new server-dispatched submission workflow exists. The remaining step for this smoke is the human GitHub OAuth authorization and submission of the prefilled private fixture.

[kim-em]

Headless-agent checkpoint (2026-08-21):

• Credential-free secret-gist proof landed in lean-eval-submissions#1187, merge fe6a43cd. GitHub documents secret gists as unlisted rather than private; the Worker anonymously fetches only the exact ID and still requires public: false, exact owner, untruncated file, signed expiry, and one-use nonce. A temporary live gist confirmed anonymous REST behavior and was deleted.
• The first live attempt exposed a workerd-only native-fetch receiver failure. Redacted stage tracing and production-decoder coverage landed in #1188; the actual binding fix landed in #1189, merge b0c0a822.
• Live staging then accepted and dispatched headless submission 01a02427-9e09-7b63-9ab7-5ff6b9ef8a09. State commits d391990 / 83e63d9 passed append-only validation; the dispatch outbox is gone and the targeted view records attempt 1 as succeeded. Production intake remains false.
• The dispatched evaluation failed at source fetch because the private fixture has the new source-reader App but not the existing lean-eval-bot evaluation App. No archive or result was fabricated; State remains accurately pending. Installing lean-eval-bot on the one fixture is the remaining external prerequisite before retrying the same source through archive/evaluation.

Deployment runs: 32477479946, 32478308045, 32478758684. Live agent workflow: 32478988233.

[kim-em]

Lifecycle-status checkpoint (2026-08-21):

• merged State submission-view schema-version-2 validators into production and staging State (lean-eval-state#1, lean-eval-state-staging#1);
• merged submission lifecycle callbacks in lean-eval-submissions#1190 at 344ae1dbd5aaf53985b20511a770caa3c52b5626;
• deployed and smoke-tested that exact commit in staging and production;
• staging intake is enabled; production intake remains disabled;
• status reads now authenticate referenced immutable archive/evaluation/result events and no longer require a full-ledger scan;
• protected workflow callbacks now persist archive failures and evaluation accepted/rejected/failed outcomes.

The existing private-fixture submission was retried without creating a duplicate. App-token minting succeeds, but repository fetch still returns 404, so kim-em/lean-eval-intake-fixture is not yet accessible to the lean-eval-bot installation. Evidence: https://github.com/leanprover/lean-eval-submissions/actions/runs/32478988233/attempts/3

[kim-em]

D6 autonomous implementation checkpoint (2026-08-21): the provider-neutral archive writer is merged in lean-eval-submissions PR #1194 (f2e4e455c1b410ef156524ecadb60707dc63a2f2). It generates one fresh native age identity per archive (age-keygen -pq by default), encrypts a standard age v1 ciphertext, binds the wrapped identity to the exact archive digest and stable ak1_ identity, passes plaintext only to a strict adapter over stdin, suppresses adapter diagnostics, and atomically publishes the ciphertext/envelope pair. The real age 1.3.1 PQ integration check and all repository/Worker/workflow checks passed.

This does not provision AWS, implement an unwrap service, wire the writer into submission.yml, enable production intake, or start D7. Those gates remain held.

[kim-em]

Archive-before-evaluation foundation is now landed, deployed, and recorded.

• Deployment-environment inventory/runbook: docs: record AWS workload environments lean-eval-submissions#1197 (merged as b58419350f8684b986372598cc5f7c3702dcac6b)
• Trusted archive-before-evaluation workflow and immutable-dispatch deployment trigger: ci: archive sources before evaluation lean-eval-submissions#1198 (merged as b64a30293e82e77cc76da1f74e6f1633747e1bf0)
• Reconciled infrastructure ledger: docs: record archive-before-evaluation deployment lean-eval-submissions#1199 (merged as aa212eea13946cbc5f17a0dd66545149d4e0836f)

Deployment evidence:

• Immutable dispatch tag: lean-eval-dispatch/b64a30293e82e77cc76da1f74e6f1633747e1bf0
• Deployment run: https://github.com/leanprover/lean-eval-submissions/actions/runs/32488170650
• Staging broker version: edeb2d01-5acf-4099-8329-cf3e52f431e1
• Staging intake initial version: 366c8c6d-671b-4c53-b488-e2cb86320dd3
• Production broker version: 1ebdfbe1-57be-4ee4-ba80-23a9bf740fc6
• Production intake version: 3d2658ec-0fda-4bf1-9619-e7500fa61d52
• Protected staging re-enable run: https://github.com/leanprover/lean-eval-submissions/actions/runs/32488534189
• Current staging intake version: 39e8392d-dcc4-46e4-9bc7-afaff28b01a5

Current live posture: staging serves exact commit b64a3029… with intake enabled; production serves the same commit with intake disabled. The six archive/replay/release GitHub environment shells are configured but carry no AWS role values or authority yet. D7 remains explicitly held and has not been applied.

The remaining staging E2E check is blocked only on lean-eval-bot repository selection for the private fixture; attempt 6 still received a repository-scoped 404 after successfully minting the installation token: https://github.com/leanprover/lean-eval-submissions/actions/runs/32478988233/attempts/6

[kim-em]

Overhaul implementation update (2026-08-21):

• Documentation reconciliation merged: docs: reconcile current overhaul deployment lean-eval-submissions#1200 (f074a5240f3cdfb389ba723ff4f2a0e14b550e56). This records the current b64a3029... Worker deployment/version IDs, the archive-before-evaluation rollout, the still-pending private-fixture verification, and the v1 set as 118 mechanical entries plus 10 explicit additions = 128.
• Disabled release/embargo State contracts merged in production State: leanprover/lean-eval-state#2 (4227463d9b60569d14e38c12d20d1d71c894fcb1) and staging State: leanprover/lean-eval-state-staging#2 (608959c0b2255cea7cb96e5afa787c3c194d8241). Post-merge live-tree validation passes (1 production event; 4 staging events).
• Deterministic disabled release planner is green in feat: add deterministic release planner lean-eval-releases#1. Its repository rules require one independent write-access approval and define no bypass actor, so review has been requested from @Kha and @leodemoura.
• No release event was appended, no publication was enabled, production intake remains disabled, and D7 remains held.
• Private fixture rerun attempt 7 is currently queued for an unassigned GitHub-hosted ubuntu-latest runner: https://github.com/leanprover/lean-eval-submissions/actions/runs/32478988233/attempts/7

[kim-em]

Public replay checkpoint (2026-08-21):

• merged the credential-free historical replay workflow in lean-eval-submissions#1201;
• fixed nested component metadata stripping in #1202, bound the legacy evaluator’s statement revision in the reviewed fixture in #1203, and aligned retained dependency metadata with the credential-free public-cache contract in #1204;
• definitive hosted run succeeded: https://github.com/leanprover/lean-eval-submissions/actions/runs/32499490261 at workflow commit 757b0831018dd6ad88092eff8a2f4b3245a456d6;
• exact source KitaKen1/lean-eval-two-plus-two@a7cf16ee..., benchmark leanprover/lean-eval@3f3786f3... / Lean v4.32.2, and evaluator lean-eval-submissions@7e48191e... were restored;
• landrun/environment probes passed; nanoda and Lean’s default kernel accepted two_plus_two, statement revision 1;
• downloaded artifact contains exactly evidence.json, results.json, and summary.json—no source files—and independently revalidates;
• fixture digest ccc258ee482809d54b3c2559269a413accc642cc6804e3ac23e5aabb31511dc0; hosted runner ubuntu24 image 20260816.277.1, AMD EPYC 9V74, wall time 1,765,458 ms; retired-instruction counter was explicitly unavailable (counter_not_reported).

This completes the credential-free public smoke only. It appends no State, writes no result, uses no private source/capability, and does not satisfy the isolated private-replay or production-backend gate.