View project on GitHub

ADR-096: Phase 3 — Declaration-Scoped Export + Independent Checker as a Kernel-Diverse Anchor

Context

ADR-049 / SPEC-049-A §6 left Phase 3 — a cheap, portable, mathlib-free re-check via lean4export + an independent checker — pilot-gated behind two empirical open questions (Q2 cross-machine export determinism; Q3 independent-checker wall-clock / no >100× pathology). ADR-093 / SPEC-093-A ran that pilot. This ADR records the decision that follows from the pilot data: the mechanism that makes Phase 3 real and the conservative way to adopt it.

The pilot (issue #5684, runs 1–7) established, on the live library:

• The blocker was the export shape, not the tooling. A whole-module export is ~5.9 GB because each Unsorry.* module is import Mathlib — it drags in all of mathlib. A declaration-scoped export (lean4export Module -- <theorem>) of the proof’s own theorem + its transitive declaration closure is 2.7–46.5 MB (126×–2194× smaller).
• Independent checking is fast and bounded (Q3). nanoda (an independent Rust Lean kernel) checks a scoped export in 0.08–2.6 s — 4×–160× faster than leanchecker, which pays a fixed full-environment cost. No >100× pathology.
• Export is deterministic (Q2, same-runner). 38/38 exports byte-identical across re-runs. (Cross-machine determinism is still to confirm — see acceptance gates.)
• It accepts valid proofs (positive control). 20/20 modules: nanoda accepted the scoped export and the target theorem was confirmed present in the checked environment (via pp_declars + unknown_pp_declar_hard_error).
• It rejects invalid proofs (negative control). 5/5 modules: nanoda rejected a deliberately ill-typed export (two theorems’ proof values swapped, so a proof term no longer matches its claimed statement — the SPEC-049-A “claims X, proves Y” / weakened-statement class). nanoda genuinely type-checks; it does not rubber-stamp.

So the Phase-3 mechanism is now empirically demonstrated: scoped-export + an independent checker is a cheap, portable, mathlib-free, sound-on-tested-cases, fast verification of a proof. What remains is breadth of validation, not whether the door is open.

WH(Y) Decision Statement

In the context of ADR-049’s Phase 3 (the only verification-throughput slope-changer — a re-check that needs no mathlib resident and so parallelises and ports without bound), pilot-gated behind Q2/Q3, where the ADR-093 pilot has now shown that a declaration-scoped lean4export (2.7–46.5 MB, not 5.9 GB) checked by an independent kernel (nanoda) is deterministic, fast (4×–160× faster than leanchecker), accepts valid proofs (target-confirmed), and rejects ill-typed ones (negative control 5/5),

facing the fact that this is strong but bounded evidence — one invalid class tested, a 0.4.10-beta checker not yet code-reviewed, cross-machine determinism unconfirmed, and only sourced-tier proofs sampled — so adopting it as a gating or p < 1 mechanism now would over-trust the data,

we decided for adopting the declaration-scoped-export + independent-checker mechanism as Phase 3’s validated direction, introduced conservatively as a non-gating, kernel-diverse defense-in-depth anchor (Phase 3a): a scheduled / sampled second check that exports each promoted proof’s declaration closure and re-verifies it with an independent checker, recording agreement with leanchecker as an auditable signal — strictly subordinate to ADR-049: the Lean kernel via leanchecker-on-locally-rebuilt-environment remains the sole p = 1 truth oracle at the promotion boundary; the independent checker is additive, never a replacement, and gates nothing,

and neglected (a) making the independent checker merge-gating now (rejected — SPEC-049-A §4: a non-kernel signal is advisory until proven across the full red-team and a checker code review; premature on one invalid class + a beta checker); (b) lowering the central re-check below p = 1 / sampling the promotion gate (rejected and explicitly out of scope — a separate ADR amending ADR-049’s p = 1 invariant, gated on this anchor’s production track record); (c) whole-module export (rejected — the ~5.9 GB artifact that made Phase 3 look infeasible; declaration scoping is the load-bearing insight); and (d) treating “nanoda is fast + accepts valid proofs” as sufficient (rejected — the negative control was the make-or-break test, and broader red-team + a checker review remain acceptance gates),

to achieve the first concrete, evidence-backed step toward Phase 3 — a kernel-diverse verification anchor (a proof both Lean and an independent kernel accept is stronger evidence, guarding a hypothetical bug in either) that is also the groundwork for the eventual cheap portable gate — without taking on the soundness risk of gating on an under-validated checker,

accepting that an independent checker introduces a new dependency to maintain and pin (it must track the toolchain, ADR-002); that the anchor spends some compute on defense-in-depth that admits no proofs; that the strong pilot result is on sourced-tier proofs and one invalid class, so the acceptance gates below (broader red-team, checker code review, cross-machine determinism, hardest-proof stress) must pass before any move toward gating; and that p = 1 on the trusted Lean gate is unchanged and non-negotiable here (ADR-049).

Phasing

• Phase 3a — kernel-diverse anchor (this ADR; non-gating). Scoped-export + independent-checker re-check runs as a scheduled / sampled defense-in-depth pass; agreement with leanchecker is recorded and audited. Gates nothing. Adopted once the acceptance gates below are green.
• Phase 3b — portable cheap gate (future ADR). Once the anchor has a production track record, the scoped-export + independent-checker becomes a portable form of the p = 1 gate (runnable off the mathlib-resident lane), cutting central cost — still p = 1, still kernel-authoritative.
• Phase 3c — sampling central p < 1 (separate ADR amending ADR-049). Explicitly out of scope here; requires its own decision and the anchor’s reputation data.

Acceptance gates (must pass before Phase 3a is enabled)

1. Broader red-team. Beyond the value-swap (type-mismatch) class: structurally- corrupt exports, the same-name weakened-statement vacuity (the ADR-011 / PR-#64 class), and axiom-sneaking (a sorryAx-bearing export with sorryAx not permitted must be rejected). The independent checker must reject every class.
2. Independent-checker code/soundness review. nanoda is 0.4.10-beta; behavioural agreement + reject-invalid is strong evidence, not a substitute for a review of the checker itself, and it enters the ADR-019 trust surface if it ever becomes load-bearing.
3. Cross-machine determinism (true Q2). Export the same module on two distinct runners and confirm byte/hash identity — required if export-hash is ever used as a cross-machine oracle (not required for the “ship export, re-check anywhere” use, where the check is the oracle, not the hash).
4. Hardest-proof stress. The sample is sourced-tier; confirm scoped-export size + checker wall-clock stay tractable on the deepest library proofs (the trend is strongly favourable: a 12,195-declaration proof exported to 46 MB and checked in 2.6 s).

Consequences

• Positive. Phase 3’s mechanism is decided on evidence; unsorry gains a kernel-diverse verification anchor (defense-in-depth against a kernel bug) and the groundwork for a cheaper portable gate — the path to the throughput slope-changer.
• Positive. Zero soundness risk on adoption: non-gating, p = 1 Lean gate unchanged, independent checker additive.
• Negative. A new pinned dependency (the independent checker) and some compute spent on defense-in-depth. Phase 3a is gated behind four acceptance validations, so the throughput win (3b/3c) is still a few steps out.
• Negative. If the broader red-team or the checker review fails, the anchor stays advisory-only or is dropped — the pilot evidence is necessary, not sufficient, for gating.

References

Status History