Expand description
Independently re-checkable proof certificates — the De Bruijn criterion.
A proof in LOGOS is a Term. A certificate bundles that term with the
proposition it claims to prove, so anyone can re-validate it against the
prelude axioms — with no access to the parser, the proof-search engine,
the certifier, or any oracle. The entire trusted surface of a re-check is
this crate (logicaffeine_kernel) plus its single dependency
(logicaffeine_base).
§The integrity rule
A certificate carries only the proof term and the claimed type — never a
context. recheck rebuilds the trusted axiom context itself via
StandardLibrary::register, so a malicious certificate cannot smuggle in a
bogus axiom (e.g. a free proof of False). You trust the prelude’s primitives
and the type-checker; you do not trust the certificate’s provenance.
§Three kinds, one family
Certificate— a proof in the bare prelude.TheoremCertificate— a proof from a disclosed environment delta over the prelude.EnvironmentCertificate(logos-environment-certificate/1or/2) — a proof together with every declaration it needs (inductives, constructors, recursors, universe-polymorphic definitions, opaque theorems carried with their proofs, structure η, quotient primitives, assumptions), rebuilt from a declared base with every entry kernel-validated. This is what a Lean import is packaged as.
read_certificate reads any of them by one door. Every struct refuses unknown fields, and a
certificate minted against a retired prelude (logos-coc-1 …) is refused as incompatible — the
tag is never rewritten to fit.
This module is available under the serde feature.
Re-exports§
pub use crate::prelude::axiom_dependencies;pub use crate::prelude::axiom_dependencies_of;pub use crate::prelude::is_admitted_axiom;pub use crate::prelude::AxiomUsage;pub use crate::prelude::ADMITTED_AXIOMS;
Structs§
- Capture
Request - Cert
Declaration - A declaration in a theorem’s disclosed environment: a
name : typeassumption (a premise hypothesis, or a declared predicate/constant) that the proof cites. - Cert
Definition - A transparent definition in a theorem’s disclosed environment:
name : type := body, δ-unfoldable during re-checking exactly as the prover registered it. - Certificate
- A self-contained, re-checkable proof certificate.
- Constructor
Claim - One constructor of an inductive type: its name and full type (parameters included).
- Environment
Certificate - A proof together with the complete environment it needs, rebuilt and re-checked from nothing but the declared base.
- Environment
Error - A refusal: its code and a sentence saying what was refused.
- Environment
Limits - Limits enforced on a certificate BEFORE any term is built or checked.
- Inductive
Type - One member of an inductive block.
- Rebuilt
Environment - A rebuilt environment: the checked context and what the checks found.
- Recheck
Report - What
recheck <certificate.json>reports: its outcome and one line per finding. - Theorem
Certificate - A self-contained, re-checkable certificate for a theorem proved FROM premises.
- Theorem
Recheck - The outcome of independently re-checking a
TheoremCertificate.
Enums§
- AnyCertificate
- Every certificate this module defines, read from JSON by one door.
- Binder
Kind - A binder annotation, as Lean’s
BinderInforecords it. - Conversion
Discipline - How declared types are compared with inferred ones.
- Environment
Base - The trusted base an environment is rebuilt on. The checker builds it; the certificate only names it.
- Environment
Entry - One declaration of an environment, in dependency order.
- Environment
Error Code - Why an environment certificate was refused. Each code is one kind of refusal, so a caller — and a tamper test — can say not only THAT a certificate failed but which check refused it.
- Independent
Verdict - How one declaration fared under the second, independent kernel (
crate::recheck). - Quotient
Primitive - Lean’s four quotient primitives, as the kernel certifies them.
- Recheck
Outcome - How an independent re-check of one certificate document ended.
- Term
Node - One row of a certificate’s term table: a
Termconstructor whose children are earlier rows.
Constants§
- ENVIRONMENT_
SCHEMA - The original format, supported unchanged for certificates containing its original entry kinds.
- OPAQUE_
ENVIRONMENT_ SCHEMA - The latest environment-certificate format. Version 2 adds checked opaque declarations. Capture writes the oldest supported format that can represent its entries: version 1 for original entry kinds, version 2 when an opaque occurs. Readers never retag existing evidence.
- PRELUDE_
VERSION - The prelude/axiom-set version a certificate was produced against. A re-checker may refuse certificates minted against an axiom set it does not recognise. Bump this whenever the trusted prelude changes.
- RETIRED_
PRELUDE_ VERSIONS - Prelude tags this checker knows it is NOT. A certificate carrying one of them is refused with an explicit incompatibility — the axiom sets differ and no migration exists — rather than the generic “unknown version” a typo would get. The tag is never rewritten to make it fit.
Functions§
- check_
prelude_ version - Refuse any prelude tag but this checker’s own, explicitly for a retired one.
- read_
certificate - Read a certificate of any kind from JSON.
- recheck
- Independently re-validate a certificate.
- recheck_
document - Re-check a certificate document of any kind, dispatched by its schema.
- recheck_
theorem - Independently re-validate a
TheoremCertificate.
Type Aliases§
- NodeRef
- A reference to an earlier row of a certificate’s term table.