[kim-em]

Accepted submissions lack acceptance-build compute receipts, and owners cannot conveniently add production token/time information later. This measures the actual toolchain Lake comparator and adds a GitHub-authenticated metadata editor for optional per-problem tokens, production elapsed time, estimated API-equivalent cost, models, harness and notes.

The adapter forwards the real bubblewrap arguments and sandbox file descriptors unchanged. It measures solution build/export separately from nanoda plus Lean's own checker, reusing the existing counter implementation in best-effort mode. Observer setup/import/counter/persistence failures preserve sandbox execution and the child verdict; the perf control FD is never inherited by untrusted code. Collection lives in the existing reusable attempt job and records the successful standard or larger runner correctly. The real native comparator fixture test shares the existing sandbox CI setup.

Source-free receipts are bound to the immutable accepted source and published only after credit is recorded. Reporting has short bounded retries in a separate best-effort job, so it cannot fail an otherwise successful submission workflow. This new job covers server and issue-form runs using the lifecycle callback credential in the protected environment; it executes no submission source. Receipts are retained for 90 days for manual publication retries. There is no scheduled reconciler. Manual historical coverage/backfill tools are separate in #2169.

The editor reads current State metadata for server-owned results, preserving deletions. Legacy edits send only changed fields. Saving refreshes the server-clock key, checks the revision and sends If-Match; concurrent edits during claiming also preserve the user's draft. Current metadata and per-field dates are public; superseded values are not republished. Ranking rules are unchanged.

Prerequisites: https://github.com/leanprover/lean-eval-state/pull/51 and https://github.com/leanprover/lean-eval-state-staging/pull/25. The Worker pins their current contract commits and callback compatibility digest. Merge/deploy those contracts first, then this producer, then leanprover/lean-eval-leaderboard#105. See docs/compute-reporting.md. No production deployment or historical replay has been performed.

Validation: 1,164 Python tests (four platform skips), 405 Worker tests, TypeScript/generated types, zero-warning ESLint, staging/production dry runs and npm audit (zero vulnerabilities). Behavioral tests cover ownership, deleted fields, legacy deltas, fresh keys, stale/claim-race drafts, exact accepted-source binding, observer failures, single execution and sandbox FD preservation. Native accepted/rejected fixture tests, workflow actionlint/pin audit, real-data State-v7 generation and site-schema validation pass. Backend/Worker CI is green; the full replay-image build is a separate check.

[kim-em]

Prerequisites: merge https://github.com/leanprover/lean-eval-state/pull/51 and https://github.com/leanprover/lean-eval-state-staging/pull/25 before merging/deploying this writer. This PR targets main and pins the contract commits from those PRs; preserve those commits when merging so the contract ancestry check remains valid (or repin and requalify after a squash). The leaderboard consumer follows this writer. Deployment and exact-profile historical backfill still require the steps in docs/compute-reporting.md.

[kim-em]

Validation at 00ad54c: CI, including the real sandbox smoke, and Worker checks pass.

The Ubuntu smoke accepted the valid proof with complete build/export and checker elapsed times, and rejected the invalid proof without publishing partial totals. The GitHub runner denied PMU access, so the receipt correctly reports counter_permission_denied; the local smoke obtained actual instruction counts. Counts therefore remain genuinely best effort under the existing runner policy.

The planner also runs against real State/Results: with an empty qualification map it emits no events, routes 690 outstanding issue rows to the existing historical planners and requires a reviewed exact-profile map for 85 server rows. This did not mutate State or run historical submissions. The dependent UI is leanprover/lean-eval-leaderboard#105.

[kim-em]

The implementation now follows the merged Namespace / toolchain-Lake comparator migration. The current receipt contract commits are production e5ca38ef7c2427ee1b06f152b77477b47e119494 and staging 84a67577279884f5ca9b8ab92db990295443d09a, from the same prerequisite State PRs. Preserve these pinned commits when merging, or repin and requalify after a squash.

At the current implementation, all 1,144 Python tests pass locally (four platform skips), along with 398 Worker tests, type/lint checks and deployment dry runs. The real native accepted/rejected smoke also passes in Ubuntu CI. Worker CI is green. The benchmark CLI / comparator-installation test build and its regression test pass locally without warnings.

The native bubblewrap adapter forwards sandbox arguments unchanged; it times solution build/export and both nanoda and Lean checker invocations. The shared receipt schema, fixture, State contract pins and rollback digest now identify the bundled toolchain and actual bubblewrap binary. Full Pages/image builds remain separate CI checks. Deployment and historical replay have not been performed.

[kim-em]

The revised stack has had a fresh independent read-only review covering this PR, leanprover/lean-eval-state#51, leanprover/lean-eval-state-staging#25, leanprover/lean-eval-leaderboard#105 and manual-history follow-up #2169. No blocking core correctness issue remained after resolving the review's two operational/documentation questions:

• Verified cloudflare-production has a protected-branch policy without reviewer protection rules, and main is protected. The new source-free issue-lane reporting job therefore adds no approval wait; its use of the lifecycle credential is explicit in the docs.
• The manual planner explicitly trusts the reviewed operator map rather than claiming to verify profile artifacts. Its nanoda checker matches the existing replay controller.

The scheduler is removed, historical tooling is separated, and the native accepted/rejected fixture test now shares the existing sandbox CI setup. Editor tests execute save/sign-in flows, preserve deleted fields and unchanged text, reject stale/claim-race updates, and refresh the server key before writing. Public v7 exposes current values plus per-field origins, never past metadata payloads. Optional receipt errors cannot abort accepted-result publication.

Current core CI is green: backend and sandbox fixtures, Worker, production State, staging State. Full Pages/image builds are separate checks. Formal State reviews and the documented deployment order still apply; no production deployment or historical replay has been performed.