View project on GitHub

ADR-048: Verify-on-Ingest — Kernel-Verify Each Proof Once, Then Trust Immutability

Context

Gate A’s implicit model has been re-verify in CI: the full kernel replay (leanchecker) and axiom audit re-run over large module sets — on every push to main (full backstop) and, until now, on every archive-block PR (which re-replayed the archived proofs). On the available 16 GB heavy Namespace runner and constrained routine Namespace runner this is the dominant cost and the source of the exit-137 OOM class: each archive package is a separate Lake project whose leanchecker loads its own full mathlib image (>8 GB resident), so re-replaying a block OOM-killed even a 16 GB runner regardless of chunk size (#764). But the same proofs validate fine when active, because their kernel replay runs once on the larger push-to-main runner and PR-time replay is incremental and small.

The key observation: a proof module only needs a kernel replay when its trusted context changes — the proof file, its goal statement, its imports/dependencies, the Lean/mathlib/lake configuration, or the Gate A checker logic. If none of those changed, re-running leanchecker on the same immutable proof re-proves nothing. Archiving a proof is a file move + metadata change; it changes none of the above.

WH(Y) Decision Statement

In the context of a Gate A that re-verifies large proof sets in CI — re-replaying archived blocks and full-replaying on every push — at a cost that OOMs memory-bound runners and forces a 16 GB profile just to re-check already-verified, immutable proofs,

facing the fact that this re-verification is redundant whenever the proof artifact and its verification context are unchanged, and that the redundancy is precisely what blocks downscaling CI to the routine namespace profile,

we decided for a verify-on-ingest model: a proof is kernel-verified exactly once, by the trusted CI pipeline, at the PR that introduces it (the normal incremental Gate A: build, statement-binding, axiom audit, leanchecker replay). After it merges it is verified for that toolchain/mathlib context. Thereafter the system trusts the immutable artifact rather than re-deriving soundness: an archive move validates provenance + byte-identity (the archived file is byte-for-byte the already-verified active proof, ADR-018) plus packaging sanity (lake build --wfail), and does not re-run leanchecker,

and explicitly NOT “trust because the proving agent says it checked” — trust is “CI verified this exact artifact and the artifact is immutable since”, never a prover’s self-attestation,

and neglected making archive validation heavier / finding it a bigger runner (#838 — a tactical unblocker that re-checks what’s already verified), because verify-on-ingest matches what archives are (frozen, already-verified blocks),

to achieve removal of the archive-OOM class entirely, archive PRs that are provenance + packaging validation (cheap, fits the routine namespace profile), and — with the rollout below — downscaling routine CI from 16 GB to the routine profile and a faster pipeline,

accepting that the residual risk shifts from Lean soundness to bookkeeping soundness: the system must reliably know an archived proof is exactly the one CI verified (guardrails below), that a context change must still force re-verification, and that a scheduled full replay remains as defense-in-depth.

Policy

1. Active proof PRs pass normal Gate A: build, statement-binding, axiom audit, kernel replay (incremental — only the changed modules + their reverse-import closure, ADR-033).
2. After merge, the proof is verified for that toolchain/mathlib context.
3. Archive moves validate that the archived artifact is byte-identical to an already-verified version — proof modules (library/Unsorry/*.lean) via the archive_packages.archive_proof_provenance check (git-blob identity of each archived proof module against the base active module or the base archived copy), and goal statements via ADR-018 archive-aware immutability — plus lake build --wfail for packaging sanity. No leanchecker replay.
4. Re-verification (kernel replay) re-runs only when the trusted context changes: the proof file, its goal statement, its imports/deps, lean-toolchain/lakefile/lake-manifest.json, or the Gate A checker (tools/gate_a/**). These are exactly the ADR-033 full-replay triggers.
5. Full replay becomes scheduled or context-triggered, not a per-push / per-archive-PR step.

Guardrails (bookkeeping soundness)

• Treat the per-package lean-toolchain + lakefile as the pinned verification context (archive packages are self-contained and frozen, so their context never drifts).
• Reject an archive move whose proof-module content differs from the verified version. Enforced by archive_proof_provenance (git-blob identity of every archived library/Unsorry/*.lean against the base active module or the base archived copy) — a net-new or altered proof in an archive (which was never kernel-replayed) fails the gate. Goal statements are pinned by ADR-018.
• Force a full re-verify on toolchain / mathlib / lake / checker changes (ADR-033 triggers).
• Keep a scheduled full replay as defense-in-depth against bookkeeping or scoping bugs.

Rollout

• Phase 1 (this ADR): archive validation drops the leanchecker replay — provenance + lake build --wfail only. Removes the archive-OOM class; archive PRs fit the routine namespace profile. (Supersedes the #823 chunking and #838 16 GB-runner tactical fixes for archives.)
• Phase 2 (implemented — SPEC-048-B): the push-to-main replay + audit are now incremental (re-check only the pushed diff, base = github.event.before), with a scheduled daily full replay
  • audit + archive re-validation as the defense-in-depth backstop (.github/workflows/gate-a-full-replay.yml). Routine Gate A (proof PRs and push to main) routes by job role: prepare/archive to namespace-profile-unsorry-prepare, axiom audit to namespace-profile-unsorry-audit, and kernel replay to namespace-profile-unsorry-replay. An olean-invalidating change (forces_full_replay: toolchain/lakefile/manifest) still forces a FULL replay, but it runs in the replay lane rather than selecting a separate workflow profile. REPLAY_CHUNK_SIZE is overridable via UNSORRY_REPLAY_CHUNK so a full replay can be made to fit a constrained runner with a small chunk — the backstop uses 6. This realises the downscale + speed-up while letting operators adjust each bottleneck independently.

Soundness

Lean soundness is unchanged: every proof is still kernel-replayed by the trusted pipeline once, under the toolchain/mathlib it is verified against, and a context change re-triggers verification. What changes is that we stop re-deriving soundness for unchanged, immutable artifacts and instead carry it forward via provenance. The trust boundary is “CI verified this exact artifact + immutability,” not the prover. Defense-in-depth (scheduled full replay; context-change triggers; byte-identity enforcement) covers the bookkeeping risk.

References

Status History