kernel design

The kernel is the trusted computing base of QED: the only code that must be correct for a theorem to be believed. This page explains the logic it implements, why its interface makes every other package untrusted, and how the soundness argument of the formal specification maps onto the code in src/kernel.

Design goal

A theorem prover is only as trustworthy as the code that can create theorems. QED follows the LCF approach of Milner’s Edinburgh LCF and its descendants HOL Light and HOL4:¹1 R. Milner, “LCF: A way of doing proofs with a machine”, 1979; J. Harrison, “HOL Light: An overview”, TPHOLs 2009. QED follows HOL Light’s choice of primitive rules most closely. theorems are values of an abstract type whose only constructors are the inference rules of the logic. Parsers, tactics, proof search and the command-line tool may contain any number of bugs, but a bug there can only make a proof fail, never make a false statement a theorem.

The kernel therefore has three goals:

• implement higher-order logic (HOL) with a small, fixed set of rules that can be read and checked by hand;
• make the theorem type impossible to forge from outside the package;
• grow the theory only through extensions that are provably conservative, and record each one for audit.

Mathematical background

Types

Types are generated by type variables and type constructors with fixed arities:

$$\tau ::= \alpha \mid c(\tau_1, \dots, \tau_n)$$

The constructors bool (arity 0), fun (arity 2, written $\sigma \to \tau$) and ind (arity 0) are built in. A type substitution $\theta$ maps type variables to types and acts homomorphically. A type $\tau$ is an instance of a schema $\sigma$, written $\tau \preceq \sigma$, when $\tau = \sigma\theta$ for some $\theta$; ty_is_instance_of decides this by first-order matching.

Terms

Terms are those of the simply typed λ-calculus over a signature of constants:

$$t ::= x{:}\tau \mid c{:}\tau \mid t\,t \mid \lambda (x{:}\tau).\,t$$

A variable is a pair of a name and a type. A constant occurrence $c{:}\tau$ is legal when $c$ is declared with schema $\sigma$ and $\tau \preceq \sigma$. The typing judgement is the usual one:

$$\frac{}{x{:}\tau : \tau} \qquad \frac{}{c{:}\tau : \tau} \qquad \frac{f : \sigma \to \tau \quad u : \sigma}{f\,u : \tau} \qquad \frac{t : \tau}{\lambda (x{:}\sigma).\,t : \sigma \to \tau}$$

Typing is syntax-directed and every well-typed term has exactly one type, so type_of is a total function into HolType? that runs in linear time.

The only logical constants of the core are equality and choice:

$$= \;:\; \alpha \to \alpha \to \mathit{bool} \qquad @ \;:\; (\alpha \to \mathit{bool}) \to \alpha$$

Every other connective is a definition in terms of these two, made by the logic package through the DefOK gate; the logic design gives the definitions. Keeping connectives out of the kernel keeps the kernel small: it knows nothing about $\wedge$ or $\to$.

α-equivalence and De Bruijn terms

Two terms are α-equivalent when they differ only in the names of bound variables: $\lambda x.\,x \equiv_\alpha \lambda y.\,y$. The rules of HOL must not depend on bound names, so the kernel works on a nameless representation. A De Bruijn term replaces each bound occurrence by the number of binders between it and its binder:²2 N. G. de Bruijn, “Lambda calculus notation with nameless dummies”, Indagationes Mathematicae 34, 1972.

$$\lambda x.\,\lambda y.\,x \;\mapsto\; \lambda.\,\lambda.\,\underline{1} \qquad \lambda y.\,\lambda x.\,y \;\mapsto\; \lambda.\,\lambda.\,\underline{1}$$

The conversion $\lceil\cdot\rceil$ (to_db_term) satisfies $t_1 \equiv_\alpha t_2 \iff \lceil t_1 \rceil = \lceil t_2 \rceil$, so α-equivalence becomes structural equality (db_term_eq). QED’s De Bruijn terms are typed: bound occurrences and binders keep their types. Two consequences follow. Abstractions over different types never collapse, since $\lceil \lambda (x{:}\sigma).\,x \rceil \ne \lceil \lambda (x{:}\tau).\,x \rceil$ for $\sigma \ne \tau$. And a term such as $\lambda (x{:}A).\,(x{:}B)$, whose inner variable has the name of the binder but another type, has no conversion at all: to_db_term returns None and every rule reports BoundaryFailure. HOL Light reads the inner x as a separate free variable; QED rejects the term, so that a binder name always refers to one variable.

Substitution and β-reduction

Write $\uparrow^d_c\,t$ for the shift that adds $d$ to every index $\ge c$ in $t$, and $t[j \mapsto s]$ for the replacement of index $j$ by $s$, shifting $s$ as it passes under binders:

$$\begin{aligned} \uparrow^d_c \underline{k} &= \underline{k} \text{ if } k < c, \quad \underline{k+d} \text{ otherwise} \\ \uparrow^d_c (\lambda.\,t) &= \lambda.\,\uparrow^d_{c+1} t \\ \underline{k}[j \mapsto s] &= s \text{ if } k = j, \quad \underline{k} \text{ otherwise} \\ (\lambda.\,t)[j \mapsto s] &= \lambda.\,\big(t[j{+}1 \mapsto \uparrow^1_0 s]\big) \end{aligned}$$

Shifts and replacement act homomorphically on applications and leave free variables and constants alone. β-contraction of $(\lambda.\,t)\,u$ is then

$$\beta\big((\lambda.\,t)\,u\big) = \uparrow^{-1}_0\big(t[0 \mapsto \uparrow^1_0 u]\big).$$

Why this cannot capture: inside $t$, index $0$ refers to the binder being removed and indices $\ge 1$ to binders outside it. Shifting $u$ up by one before inserting it makes every free index of $u$ skip the binder that is about to disappear, and the replacement shifts again under each inner binder, so an index of $u$ always counts the binders that actually surround it. After replacement no occurrence of index $0$ remains, because each one was replaced, so the final shift down by one is defined and turns the indices that pointed past the removed binder back into their original values. The named counterpart is the capture-avoiding substitution $t[u/x]$; the specification states this correspondence as the lemma “Well-Scoped Beta Contraction Safety”. The kernel computes every index with overflow checks and reports CapacityExceeded instead of wrapping.

Substitution for free variables (db_subst_free_parallel, used by INST) is simpler: a free variable is a name, never an index, and the inserted term is shifted by the current binder depth, which is a no-op for a term with no loose indices. Capture is impossible by construction, which is why INST needs no renaming step.

Sequents and theorems

A theorem is a sequent $\Gamma \vdash p$: a finite set $\Gamma$ of propositions (terms of type bool) and a proposition $p$. The kernel stores $\Gamma$ and $p$ as De Bruijn terms, so $\Gamma$ is literally a set of α-equivalence classes: inserting a hypothesis that is α-equivalent to one already present does nothing (db_hyps_union).

The intended meaning is the standard semantics of HOL: types denote non-empty sets, $\mathit{bool}$ denotes $\{\top, \bot\}$, $\sigma \to \tau$ denotes the full set of functions, $=$ denotes identity and $@$ denotes a choice function. A sequent is valid when every model and every valuation of the free variables that make all of $\Gamma$ true also make $p$ true.

Design decisions

The theorem type is abstract

Problem. If code outside the kernel could construct a Thm, any bug or shortcut in that code could produce a false theorem.

Options. An LCF-style abstract type; proof terms checked by a separate checker (the approach of Coq and Lean); or a trusted record with a “verified” flag.

Choice. Thm is declared type Thm in the interface: its fields are private and it has no public constructor. The only functions that return a Thm are the eleven rule functions (refl_checked to inst_checked, plus add_assum_checked), the gates ks_define_const_thm and ks_specify_const, the stored-theorem readers ks_definition_theorem, ks_typedef_contract and ks_ind_infinity_axiom, and thm_bind_const_ids, which returns its argument with constant identities recorded after checking it. MoonBit enforces this at compile time.

Why. With an abstract type the trusted base is exactly this package. Proof terms would add a second trusted component, the checker, and a large proof object per theorem; QED’s specification makes the LCF discipline normative (obligation “Interface safety”) and checks it by inspecting the interface file.

HOL Light’s primitive rules

Problem. Choose the rules that generate all theorems.

Choice. The ten rules of HOL Light, the smallest standard basis for HOL with equality as the only primitive connective:

$$\begin{gathered} \frac{}{\vdash t = t}\,\textsf{REFL} \qquad \frac{}{\{p\} \vdash p}\,\textsf{ASSUME} \qquad \frac{\Gamma \vdash s = t \quad \Delta \vdash t = u}{\Gamma \cup \Delta \vdash s = u}\,\textsf{TRANS} \\[1ex] \frac{\Gamma \vdash f = g \quad \Delta \vdash x = y}{\Gamma \cup \Delta \vdash f\,x = g\,y}\,\textsf{MK\_COMB} \qquad \frac{\Gamma \vdash s = t \quad x \notin \mathrm{FV}(\Gamma)}{\Gamma \vdash \lambda x.\,s = \lambda x.\,t}\,\textsf{ABS} \qquad \frac{}{\vdash (\lambda x.\,t)\,u = t[u/x]}\,\textsf{BETA} \\[1ex] \frac{\Gamma \vdash p = q \quad \Delta \vdash p}{\Gamma \cup \Delta \vdash q}\,\textsf{EQ\_MP} \qquad \frac{\Gamma \vdash p \quad \Delta \vdash q}{(\Gamma \setminus \{q\}) \cup (\Delta \setminus \{p\}) \vdash p = q}\,\textsf{DEDUCT\_ANTISYM\_RULE} \\[1ex] \frac{\Gamma \vdash p}{\Gamma\theta \vdash p\theta}\,\textsf{INST\_TYPE} \qquad \frac{\Gamma \vdash p}{\Gamma\sigma \vdash p\sigma}\,\textsf{INST} \end{gathered}$$

Matching of premises (the middle term of TRANS, the antecedent of EQ_MP) is up to α-equivalence and ignores constant identities (db_term_logical_eq), because both theorems have already been checked against the current state.

One deviation: QED’s BETA accepts any redex $(\lambda x.\,t)\,u$, whereas HOL Light’s primitive BETA only accepts $(\lambda x.\,t)\,x$ and derives the general form with INST. The general form is a derived rule in HOL Light, so this adds no theorems; it saves the kernel a renaming step and is exactly the rule stated in the specification.

Why HOL and not dependent types. HOL has a simple, well-understood set-theoretic semantics, a kernel of a few hundred lines in HOL Light, and decades of experience showing that the ten rules suffice for mathematics when combined with definitions. The kernel stays small enough for its soundness argument to be read in full, which is the point of a kernel-first design.

Weakening is provided natively

add_assum_checked implements weakening, $\Gamma \vdash p$ gives $\Gamma \cup \{q\} \vdash p$. It is not one of the ten rules and the specification does not list it, but it is a derived rule, so it adds no theorems:

$$\begin{aligned} &1.\;\; \{q\} \vdash q && \textsf{ASSUME} \\ &2.\;\; \Gamma \vdash p && \text{premise} \\ &3.\;\; (\{q\} \setminus \{p\}) \cup (\Gamma \setminus \{q\}) \vdash q = p && \textsf{DEDUCT\_ANTISYM\_RULE}(1, 2) \\ &4.\;\; (\{q\} \setminus \{p\}) \cup (\Gamma \setminus \{q\}) \cup \{q\} \vdash p && \textsf{EQ\_MP}(3, 1) \end{aligned}$$

The hypothesis set of line 4 is $\Gamma \cup \{q\}$: the part $\{q\} \setminus \{p\}$ is contained in $\{q\}$, and $(\Gamma \setminus \{q\}) \cup \{q\} = \Gamma \cup \{q\}$. The derivation works whether or not $q \equiv_\alpha p$ or $q \in \Gamma$. The native rule is a shortcut used by replay in the logic package to make hypothesis sets match exactly.

A named boundary over a De Bruijn core

Problem. Users and the frontend think in named terms; the rules must be name-independent.

Options. Named terms with explicit renaming (HOL Light); locally nameless terms; De Bruijn terms everywhere.

Choice. The interface takes and returns named Term values; every rule converts its inputs with to_db_term, works on DbTerm, and converts back with from_db_term only when a caller asks for hypotheses or a conclusion. A failed conversion is the error BoundaryFailure, not a derivation.

Why. α-equivalence becomes equality, substitution needs no fresh names, and hypothesis sets are sets of α-classes for free. The cost is that terms read back from a theorem carry generated binder names (_b0, _b1, …), so callers compare with term_alpha_eq. The specification proves the commutation square that justifies the boundary: lowering, running the De Bruijn rule and lifting gives a result α-equivalent to running the named rule.

Every rule is checked against a state

Problem. Constants are declared in scopes and can be shadowed. A theorem about the constant c proved in one scope must not be reused after an inner scope declares a different c.

Choice. Every rule takes the KernelState and runs ensure_thm_admissible on its premises and on its result. A theorem records the identity (ConstId) of each constant it mentions. It is admissible in a state when each recorded identity is the one the state resolves the name to, each constant occurrence is an instance of the declared schema, each type uses only admitted constructors, and a definition theorem still agrees with its definition.

Why. Name lookup changes as scopes are pushed and popped, but a recorded identity does not. Freezing identities makes resolution stable under scope mutation (the specification’s “Resolution Freeze” theorem), and the check turns a stale theorem into an InvalidInstantiation failure instead of a silent change of meaning. The tutorial shows a theorem that is rejected inside a shadowing scope and accepted again after the scope is popped.

Extensions go through gates

The theory grows in three ways, each guarded by a gate that checks side conditions and appends an ExtensionCert.

DefOK, constant definition. ks_define_const(c, \tau, t) adds a constant $c : \tau$ and the theorem $\vdash c = t$. Each side condition rules out a known way to break conservativity:

Condition	Error	Counterexample it prevents
$t$ is closed	DefinitionNotClosed	$c = x$ would give $\vdash c = x$, then INST gives $\vdash c = y$ and so $\vdash x = y$ for all $x, y$.
$c$ does not occur in $t$, even through earlier definitions	DefinitionIsCyclic	$c = \neg c$ would give $\vdash c = \neg c$, a contradiction.
$\mathrm{tyvars}(t) \subseteq \mathrm{tyvars}(\tau)$	GhostTypeVariable	$c = (\forall x{:}\alpha.\,\forall y{:}\alpha.\,x = y)$ with $c : \mathit{bool}$ is true at $\alpha = \mathit{unit}$ and false at $\alpha = \mathit{bool}$, yet both instances are the same constant $c$.
$c$ is fresh	DefinitionAlreadyExists	Two definitions of one name would give $\vdash c = t_1$ and $\vdash c = t_2$, so $\vdash t_1 = t_2$.

Under these conditions a definition is conservative: replacing every occurrence of $c$ by $t$ maps each proof in the extended theory to a proof in the old theory, and maps a theorem that does not mention $c$ to itself. The specification proves this as “Definition-level conservativity”.

TypeDefOK, type definition. ks_register_type_definition admits a type $\kappa(\bar\alpha)$ in bijection with $\{x : \rho \mid P\,x\}$, given a theorem $\vdash P\,w$. The witness matters because HOL types denote non-empty sets: a type defined by an empty predicate would have no model, and the axiom $\vdash \mathit{abs}(\mathit{rep}\,a) = a$ applied to the empty type would make the theory inconsistent. The gate requires the predicate’s type variables to be among the parameters $\bar\alpha$ for the same reason that DefOK forbids ghost type variables, and returns three contract theorems:

$$\vdash \mathit{abs}(\mathit{rep}\,a) = a \qquad \vdash P(\mathit{rep}\,a) \qquad P\,r \vdash \mathit{rep}(\mathit{abs}\,r) = r$$

The first two say that $\mathit{rep}$ is injective with image inside $P$; the third says every element of $P$ is in the image. Together they are HOL Light’s characterisation of a type bijection, with the equivalence $P\,r = (\mathit{rep}(\mathit{abs}\,r) = r)$ split into the two directions.

SpecOK, constant specification. ks_specify_const introduces $c$ with the property $\vdash P\,c$, given $\vdash P\,w$. It is not a new primitive: it defines $c = @P$ through DefOK and returns $\vdash P\,c$, which follows from the choice axiom

$$P\,x \;\to\; P(@P)$$

instantiated at $x = w$. Because the extension is a definition, its conservativity follows from that of DefOK; the state records both a DefOK and a SpecOK certificate.

Infinity anchor. HOL needs an infinite type for arithmetic. ks_register_ind_infinity_axiom records a theorem about ind that plays this role, but only accepts a theorem that already exists; it marks the model-class restriction of the specification without adding a theorem.

Results, not exceptions

Every kernel function returns Result or Option; none aborts on bad input. A rule that cannot apply says why, with a constructor of LogicError or SigError, and the caller decides what to do. This is what makes the frontend fail closed: the tactics and prover packages turn these values into structured diagnostics, and no path turns a failed rule into a theorem.

Correctness and invariants

Why soundness reduces to the kernel

Call a theorem value sound when its sequent is valid in every model of the current theory. The argument has three steps.

1. Every rule preserves validity. For each primitive rule, valid premises give a valid conclusion. Two cases show the pattern.

ABS. Let $M$ be a model and $v$ a valuation that satisfies $\Gamma$. Since $x \notin \mathrm{FV}(\Gamma)$, every valuation $v[x \mapsto a]$ also satisfies $\Gamma$, so by validity of the premise $[\![s]\!]_{v[x \mapsto a]} = [\![t]\!]_{v[x \mapsto a]}$ for every $a$. Hence

$$[\![\lambda x.\,s]\!]_v = \big(a \mapsto [\![s]\!]_{v[x\mapsto a]}\big) = \big(a \mapsto [\![t]\!]_{v[x\mapsto a]}\big) = [\![\lambda x.\,t]\!]_v$$

by function extensionality in the standard model. Without the side condition the step “every $v[x \mapsto a]$ satisfies $\Gamma$” fails: from $\{x = 0\} \vdash x = 0$ one could derive $\{x = 0\} \vdash (\lambda x.\,x) = (\lambda x.\,0)$, which is false whenever $x = 0$ holds.

DEDUCT_ANTISYM_RULE. Let $v$ satisfy $(\Gamma \setminus \{q\}) \cup (\Delta \setminus \{p\})$. If $[\![p]\!]_v = \top$, then $v$ satisfies $\Delta$ (the only hypothesis that may have been removed from $\Delta$ is $p$), so $[\![q]\!]_v = \top$. Symmetrically $[\![q]\!]_v = \top$ implies $[\![p]\!]_v = \top$. Two booleans that imply each other are equal, so $[\![p = q]\!]_v = \top$.

The remaining rules follow the same way: REFL and TRANS from reflexivity and transitivity of identity, MK_COMB from congruence of application, BETA from the substitution lemma $[\![t[u/x]]\!]_v = [\![t]\!]_{v[x \mapsto [\![u]\!]_v]}$, EQ_MP from the meaning of $=$ on booleans, ASSUME trivially, and INST and INST_TYPE because a valid sequent is valid under every valuation and every interpretation of type variables. The specification proves each case (“Rule-level preservation”).

2. Every extension preserves consistency. DefOK, TypeDefOK and SpecOK are conservative, as argued above: every model of the old theory extends to a model of the new one, so no new sentence in the old language becomes provable.

3. Interface safety. Because Thm is abstract, every Thm that exists at run time is the root of a finite derivation tree whose nodes are rule applications and gate outputs. Induction on the depth of that tree, using steps 1 and 2, shows that every Thm is sound.

Step 3 is a property of the code, not of the logic, and it is why nothing outside src/kernel needs to be trusted: the logic, tactics and prover packages can only call the functions in the kernel API, so whatever they compute, any Thm they return has a derivation. The specification states the six obligations and their dependencies; the conformance pack in formal_verification/ checks the paper side in Lean.

Invariants maintained by the code

• A Thm stores its hypotheses as an α-deduplicated list and its conclusion as a De Bruijn term; every rule result passes ensure_thm_admissible in the state it was built in.
• KernelState is persistent. A gate returns a new state; the base state stays valid, so ks_conservative_replay_ok(base, extended, th) can re-check th against both.
• Constant identities are allocated from a counter in the theory state and never reused, even after a scope is popped.
• Definition heads, type-definition heads and the infinity anchor are recorded in the theory history, which ks_pop_scope does not touch: a name, once defined, cannot be defined again.

Complexity

Each rule is linear in the size of its premises, except for hypothesis-set union, which compares hypotheses pairwise and is quadratic in their number. Admissibility checks walk the theorem once per constant occurrence and look up names in the scoped signature, linear in the number of declarations. Proof sizes in the shipped subset are small; the kernel favours checks that are easy to audit over asymptotic speed.

Alternatives rejected

• Named terms with renaming, as in HOL Light. Every rule would need a correct renaming function, which is a classic source of kernel bugs. The De Bruijn core avoids renaming entirely.
• Connectives as kernel primitives. Adding $\wedge$, $\to$ or $\forall$ as primitive constants with their own rules would enlarge the kernel and its soundness proof. They are definitions over $=$ instead.
• Exceptions for rule failure. HOL Light raises Failure. Results make every failure visible in the type and keep the frontend from accidentally catching and ignoring one.
• Unchecked rules with a separate validation pass. Checking admissibility only at the end would let an inadmissible intermediate theorem feed later steps. Every rule checks its inputs and output instead.
• Arbitrary axioms. There is no function that turns a term into a theorem. The only non-derived theorems are definitions and type-definition contracts, both produced by gates with conservativity conditions.

Boundaries

• The kernel does not parse text, elaborate names or run tactics; those are the elab, parser and tactics packages, and none of them is trusted.
• It implements no connective other than equality and choice, and no quantifier syntax; the logic package defines the rest.
• It does not store proved theorems by name. Theorem names are a frontend concern.
• It has no metavariables and no incomplete theorems: a hole in a proof script never reaches the kernel.
• It does not prove its own soundness. The argument above and in the specification is a paper proof; formal_verification/ aligns the specification with Lean, not the MoonBit source.
• It does not provide the choice axiom as a theorem. @ is declared and used by SpecOK, but no public function returns $P\,x \to P(@P)$.

Footnotes

1. R. Milner, “LCF: A way of doing proofs with a machine”, 1979; J. Harrison, “HOL Light: An overview”, TPHOLs 2009. QED follows HOL Light’s choice of primitive rules most closely. ↩

2. N. G. de Bruijn, “Lambda calculus notation with nameless dummies”, Indagationes Mathematicae 34, 1972. ↩