kernel 设计说明

内核是 QED 的可信计算基：一个定理要被相信，只有这部分代码必须正确。本页解释它所实现的逻辑、它的接口为何使其他所有包都不必被信任，以及形式规范的可靠性论证如何对应到 src/kernel 中的代码。

设计目标

定理证明器的可信程度取决于能创建定理的代码。QED 遵循 LCF 方法，即 Milner 的 Edinburgh LCF 及其后继者 HOL Light 和 HOL4 的方法：¹1 R. Milner, “LCF: A way of doing proofs with a machine”, 1979; J. Harrison, “HOL Light: An overview”, TPHOLs 2009。QED 在原始规则的选择上最接近 HOL Light。 定理是抽象类型的值，其唯一构造子就是逻辑的推理规则。解析器、策略（tactic）、证明搜索和命令行工具可以含有任意多的缺陷，但其中的缺陷只会使证明失败，绝不会让假命题成为定理。

因此内核有三个目标：

• 用一组小而固定、可以手工阅读和检查的规则实现高阶逻辑（HOL）；
• 使 theorem 类型无法从包外伪造；
• 只通过可证明保守的扩张来扩展理论，并记录每次扩张以供审计。

数学背景

类型

类型由类型变量和具有固定元数的类型构造子生成：

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

构造子 bool（元数 0）、fun（元数 2，写作 $\sigma \to \tau$）和 ind（元数 0）是内建的。类型代换 $\theta$ 把类型变量映射到类型，并按同态方式作用。当对某个 $\theta$ 有 $\tau = \sigma\theta$ 时，类型 $\tau$ 是模式 $\sigma$ 的一个实例，记作 $\tau \preceq \sigma$；ty_is_instance_of 通过一阶匹配来判定这一点。

项

项是常量签名上的简单类型 λ 演算的项：

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

变量是名称和类型的二元组。当 $c$ 以模式 $\sigma$ 声明且 $\tau \preceq \sigma$ 时，常量出现 $c{:}\tau$ 是合法的。类型判断是通常的形式：

$$\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}$$

类型检查是语法导向的，每个良类型的项恰有一个类型，因此 type_of 是到 HolType? 的全函数，且在线性时间内运行。

核心中仅有的逻辑常量是相等和选择：

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

其他每个联结词都是这两者的定义，由 logic 包通过 DefOK 闸门做出；logic 设计说明给出了这些定义。把联结词放在内核之外使内核保持小巧：它对 $\wedge$ 或 $\to$ 一无所知。

α 等价与 De Bruijn 项

两个项仅在绑定变量的名称上不同时是 α 等价的：$\lambda x.\,x \equiv_\alpha \lambda y.\,y$。HOL 的规则不得依赖绑定名称，因此内核使用无名表示。De Bruijn 项把每个绑定出现替换为它与其绑定子之间的绑定子个数：²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}$$

转换 $\lceil\cdot\rceil$（to_db_term）满足 $t_1 \equiv_\alpha t_2 \iff \lceil t_1 \rceil = \lceil t_2 \rceil$，因此 α 等价变为结构相等（db_term_eq）。QED 的 De Bruijn 项是带类型的：绑定出现和绑定子都保留其类型。由此得到两个后果。其一，对不同类型的抽象永远不会合并，因为对 $\sigma \ne \tau$ 有 $\lceil \lambda (x{:}\sigma).\,x \rceil \ne \lceil \lambda (x{:}\tau).\,x \rceil$。其二，诸如 $\lambda (x{:}A).\,(x{:}B)$ 这样的项，其内部变量与绑定子同名但类型不同，完全没有转换：to_db_term 返回 None，每条规则都报告 BoundaryFailure。HOL Light 把内部的 x 视为一个单独的自由变量；QED 则拒绝该项，使得绑定子名称始终指向同一个变量。

代换与 β 归约

记 $\uparrow^d_c\,t$ 为对 $t$ 中每个 $\ge c$ 的索引加上 $d$ 的移位，记 $t[j \mapsto s]$ 为把索引 $j$ 替换为 $s$，并在 $s$ 经过绑定子时对其移位：

$$\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}$$

移位和替换对应用按同态方式作用，并保持自由变量和常量不变。于是 $(\lambda.\,t)\,u$ 的 β 收缩为

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

为什么这不会发生捕获：在 $t$ 内部，索引 $0$ 指被移除的绑定子，索引 $\ge 1$ 指其外部的绑定子。在插入 $u$ 之前把它上移一位，使 $u$ 的每个自由索引都跳过即将消失的那个绑定子；替换在每个内层绑定子之下再次移位，所以 $u$ 的索引始终统计真正包围它的绑定子。替换之后不再有索引 $0$ 的出现，因为每个都已被替换，所以最后的下移一位是有定义的，并把指向被移除绑定子之外的索引还原为其原值。具名的对应物是避免捕获的代换 $t[u/x]$；规范把这一对应陈述为引理“Well-Scoped Beta Contraction Safety”。内核对每个索引的计算都做溢出检查，并报告 CapacityExceeded 而不是回绕。

对自由变量的代换（db_subst_free_parallel，供 INST 使用）更简单：自由变量是名称，而不是索引，插入的项按当前绑定子深度移位，对于没有松散索引的项这是空操作。按构造不可能发生捕获，这就是 INST 不需要重命名步骤的原因。

相继式与定理

定理是相继式 $\Gamma \vdash p$：由命题（类型为 bool 的项）组成的有限集合 $\Gamma$，以及一个命题 $p$。内核把 $\Gamma$ 和 $p$ 存储为 De Bruijn 项，因此 $\Gamma$ 字面上就是 α 等价类的集合：插入一个与已有假设 α 等价的假设不会产生任何效果（db_hyps_union）。

其预期含义是 HOL 的标准语义：类型表示非空集合，$\mathit{bool}$ 表示 $\{\top, \bot\}$，$\sigma \to \tau$ 表示全体函数的集合，$=$ 表示同一性，$@$ 表示选择函数。当使 $\Gamma$ 全部为真的每个模型和自由变量的每个赋值也都使 $p$ 为真时，相继式是有效的。

设计决策

定理类型是抽象的

问题。 如果内核之外的代码可以构造 Thm，那么该代码中的任何缺陷或捷径都可能产生假定理。

选项。 LCF 风格的抽象类型；由独立检查器检查的证明项（Coq 和 Lean 的做法）；或带“已验证”标志的可信记录。

选择。 Thm 在接口中声明为 type Thm：其字段是私有的，没有公开构造函数。唯一返回 Thm 的函数是十一个规则函数（从 refl_checked 到 inst_checked，外加 add_assum_checked）、闸门 ks_define_const_thm 和 ks_specify_const、已存储定理的读取器 ks_definition_theorem、ks_typedef_contract 和 ks_ind_infinity_axiom，以及 thm_bind_const_ids，它在检查其参数后返回记录了常量标识的该参数。MoonBit 在编译期强制这一点。

原因。 有了抽象类型，可信基恰好就是这个包。证明项会增加第二个可信组件，即检查器，以及每个定理一个庞大的证明对象；QED 的规范把 LCF 纪律规定为规范性要求（义务“Interface safety”），并通过检查接口文件来验证它。

HOL Light 的原始规则

问题。 选择生成所有定理的规则。

选择。 HOL Light 的十条规则，这是以相等为唯一原始联结词的 HOL 的最小标准基：

$$\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}$$

前提的匹配（TRANS 的中间项、EQ_MP 的前件）是在 α 等价意义下进行的，并忽略常量标识（db_term_logical_eq），因为两个定理都已针对当前状态检查过。

一处偏离：QED 的 BETA 接受任何 redex $(\lambda x.\,t)\,u$，而 HOL Light 的原始 BETA 只接受 $(\lambda x.\,t)\,x$，并用 INST 导出一般形式。一般形式在 HOL Light 中是导出规则，所以这不会增加定理；它为内核省去一个重命名步骤，并且正是规范中所陈述的规则。

为什么用 HOL 而不用依赖类型。 HOL 有简单且被充分理解的集合论语义，在 HOL Light 中内核只有几百行，并且数十年的经验表明，十条规则配合定义足以支撑数学。内核保持得足够小，使其可靠性论证可以被完整阅读，这正是内核优先设计的意义所在。

弱化是原生提供的

add_assum_checked 实现弱化，即由 $\Gamma \vdash p$ 得到 $\Gamma \cup \{q\} \vdash p$。它不是那十条规则之一，规范也没有列出它，但它是导出规则，所以不会增加定理：

$$\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}$$

第 4 行的假设集合是 $\Gamma \cup \{q\}$：部分 $\{q\} \setminus \{p\}$ 包含于 $\{q\}$，且 $(\Gamma \setminus \{q\}) \cup \{q\} = \Gamma \cup \{q\}$。无论 $q \equiv_\alpha p$ 或 $q \in \Gamma$ 是否成立，该推导都有效。这条原生规则是 logic 包中的重放用来使假设集合精确匹配的捷径。

De Bruijn 核心之上的具名边界

问题。 用户和前端以具名项思考；规则必须与名称无关。

选项。 带显式重命名的具名项（HOL Light）；局部无名项；处处使用 De Bruijn 项。

选择。 接口接受并返回具名的 Term 值；每条规则用 to_db_term 转换其输入，在 DbTerm 上工作，只有当调用者请求假设或结论时才用 from_db_term 转换回来。转换失败是错误 BoundaryFailure，而不是一次推导。

原因。 α 等价变为相等，代换不需要新名称，假设集合自然就是 α 类的集合。代价是从定理读回的项带有生成的绑定子名称（_b0、_b1，……），所以调用者要用 term_alpha_eq 进行比较。规范证明了论证该边界的交换图：降级、运行 De Bruijn 规则再提升，所得结果与运行具名规则的结果 α 等价。

每条规则都针对一个状态检查

问题。 常量在作用域中声明，并且可以被遮蔽。在某个作用域中证明的关于常量 c 的定理，在内层作用域声明了另一个 c 之后不得被复用。

选择。 每条规则都接受 KernelState，并对其前提及其结果运行 ensure_thm_admissible。定理记录它所提到的每个常量的标识（ConstId）。当每个被记录的标识都是状态为该名称所解析到的标识、每个常量出现都是所声明模式的实例、每个类型只使用已接纳的构造子，且定义定理仍与其定义一致时，它在该状态中是可容许的。

原因。 随着作用域的压入和弹出，名称查找会变化，但被记录的标识不会。冻结标识使解析在作用域变动下保持稳定（规范中的“Resolution Freeze”定理），而该检查把过期的定理变成 InvalidInstantiation 失败，而不是含义的悄然改变。教程展示了一个在遮蔽作用域内被拒绝、作用域弹出后又被接受的定理。

扩张通过闸门进行

理论以三种方式增长，每种都由一个闸门把守，闸门检查附带条件并追加一个 ExtensionCert。

DefOK，常量定义。 ks_define_const(c, \tau, t) 添加常量 $c : \tau$ 和定理 $\vdash c = t$。每个附带条件都排除了一种已知破坏保守性的方式：

条件	错误	它所防止的反例
$t$ 是闭的	DefinitionNotClosed	$c = x$ 会给出 $\vdash c = x$，然后 INST 给出 $\vdash c = y$，于是对所有 $x, y$ 都有 $\vdash x = y$。
$c$ 不在 $t$ 中出现，即使通过更早的定义也不行	DefinitionIsCyclic	$c = \neg c$ 会给出 $\vdash c = \neg c$，这是矛盾。
$\mathrm{tyvars}(t) \subseteq \mathrm{tyvars}(\tau)$	GhostTypeVariable	带 $c : \mathit{bool}$ 的 $c = (\forall x{:}\alpha.\,\forall y{:}\alpha.\,x = y)$ 在 $\alpha = \mathit{unit}$ 时为真，在 $\alpha = \mathit{bool}$ 时为假，而两个实例却是同一个常量 $c$。
$c$ 是新的	DefinitionAlreadyExists	同一个名称的两个定义会给出 $\vdash c = t_1$ 和 $\vdash c = t_2$，于是 $\vdash t_1 = t_2$。

在这些条件下，定义是保守的：把每个 $c$ 的出现替换为 $t$，会把扩展理论中的每个证明映射为旧理论中的证明，并把不提及 $c$ 的定理映射为其自身。规范把它证明为“Definition-level conservativity”。

TypeDefOK，类型定义。 ks_register_type_definition 接纳一个与 $\{x : \rho \mid P\,x\}$ 双射的类型 $\kappa(\bar\alpha)$，前提是给出定理 $\vdash P\,w$。见证很重要，因为 HOL 类型表示非空集合：由空谓词定义的类型没有模型，并且把公理 $\vdash \mathit{abs}(\mathit{rep}\,a) = a$ 应用于空类型会使理论不一致。出于与 DefOK 禁止幽灵类型变量相同的理由，该闸门要求谓词的类型变量属于参数 $\bar\alpha$，并返回三个契约定理：

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

前两个说明 $\mathit{rep}$ 是单射且像落在 $P$ 内；第三个说明 $P$ 的每个元素都在像中。合起来，它们就是 HOL Light 对类型双射的刻画，其中等价式 $P\,r = (\mathit{rep}(\mathit{abs}\,r) = r)$ 被拆为两个方向。

SpecOK，常量规约。 给定 $\vdash P\,w$，ks_specify_const 引入具有性质 $\vdash P\,c$ 的 $c$。它不是新的原始构件：它通过 DefOK 定义 $c = @P$ 并返回 $\vdash P\,c$，而后者由选择公理

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

在 $x = w$ 处实例化得到。由于该扩张是一个定义，其保守性由 DefOK 的保守性推出；状态同时记录一个 DefOK 和一个 SpecOK 证书。

无穷锚点。 HOL 需要一个无穷类型来做算术。ks_register_ind_infinity_axiom 记录一个关于 ind 的定理来扮演这一角色，但只接受已经存在的定理；它标记规范中对模型类的限制，而不增加定理。

返回结果，而不是异常

每个内核函数都返回 Result 或 Option；没有一个会因错误输入而中止。无法应用的规则会用 LogicError 或 SigError 的构造子说明原因，由调用者决定怎么做。这正是前端失败即关闭（fail closed）的原因：tactics 和 prover 包把这些值转为结构化诊断，没有任何路径会把失败的规则变成定理。

正确性与不变量

为什么可靠性归结于内核

当一个定理值的相继式在当前理论的每个模型中都有效时，称它是可靠的。论证分三步。

1. 每条规则都保持有效性。 对每条原始规则，有效的前提给出有效的结论。以下两种情形展示了模式。

ABS。设 $M$ 是模型，$v$ 是满足 $\Gamma$ 的赋值。由于 $x \notin \mathrm{FV}(\Gamma)$，每个赋值 $v[x \mapsto a]$ 也满足 $\Gamma$，所以由前提的有效性，对每个 $a$ 有 $[\![s]\!]_{v[x \mapsto a]} = [\![t]\!]_{v[x \mapsto a]}$。因此

$$[\![\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$$

由标准模型中的函数外延性得到。没有该附带条件，“每个 $v[x \mapsto a]$ 都满足 $\Gamma$”这一步就会失败：由 $\{x = 0\} \vdash x = 0$ 可以推出 $\{x = 0\} \vdash (\lambda x.\,x) = (\lambda x.\,0)$，而只要 $x = 0$ 成立，它就是假的。

DEDUCT_ANTISYM_RULE。设 $v$ 满足 $(\Gamma \setminus \{q\}) \cup (\Delta \setminus \{p\})$。若 $[\![p]\!]_v = \top$，则 $v$ 满足 $\Delta$（从 $\Delta$ 中可能被移除的唯一假设是 $p$），所以 $[\![q]\!]_v = \top$。对称地，$[\![q]\!]_v = \top$ 蕴含 $[\![p]\!]_v = \top$。互相蕴含的两个布尔值相等，所以 $[\![p = q]\!]_v = \top$。

其余规则同样可证：REFL 和 TRANS 来自同一性的自反性和传递性，MK_COMB 来自应用的同余性，BETA 来自代换引理 $[\![t[u/x]]\!]_v = [\![t]\!]_{v[x \mapsto [\![u]\!]_v]}$，EQ_MP 来自 $=$ 在布尔值上的含义，ASSUME 是平凡的，INST 和 INST_TYPE 则是因为有效的相继式在每个赋值和类型变量的每个解释下都有效。规范证明了每一种情形（“Rule-level preservation”）。

2. 每次扩张都保持一致性。 如上所述，DefOK、TypeDefOK 和 SpecOK 都是保守的：旧理论的每个模型都可扩展为新理论的模型，所以旧语言中没有新的句子变得可证。

3. 接口安全。 由于 Thm 是抽象的，运行时存在的每个 Thm 都是一棵有限推导树的根，树的节点是规则应用和闸门输出。利用第 1、2 步，对该树的深度做归纳，即可证明每个 Thm 都是可靠的。

第 3 步是代码的性质，而不是逻辑的性质，这正是 src/kernel 之外的任何东西都不需要被信任的原因：logic、tactics 和 prover 包只能调用 kernel API 中的函数，所以无论它们算出什么，它们返回的任何 Thm 都有一个推导。规范陈述了六条义务及其依赖关系；formal_verification/ 中的符合性包在 Lean 中检查纸面部分。

代码所维持的不变量

• Thm 将其假设存储为按 α 去重的列表，将结论存储为 De Bruijn 项；每个规则的结果都要在构造它的状态中通过 ensure_thm_admissible。
• KernelState 是持久化的。闸门返回新状态，基础状态仍然有效，因此 ks_conservative_replay_ok(base, extended, th) 可以针对两者重新检查 th。
• 常量标识由理论状态中的计数器分配，即使作用域被弹出也不会复用。
• 定义头、类型定义头和无穷锚点都记录在理论历史中，ks_pop_scope 不会触及它们：名称一旦被定义，就不能再次定义。

复杂度

每条规则相对其前提的大小都是线性的，唯一的例外是假设集合的并集：它对假设做两两比较，复杂度是假设数量的平方。可容许性检查对每个常量出现遍历一次定理，并在带作用域的签名中查找名称，复杂度与声明数量成线性关系。已发布子集中的证明规模很小；内核更看重易于审计的检查，而非渐近速度。

被否决的替代方案

• 带重命名的具名项，如 HOL Light。 每条规则都需要一个正确的重命名函数，而这正是内核缺陷的经典来源。De Bruijn 内核完全避免了重命名。
• 将联结词作为内核原语。 把 $\wedge$、$\to$ 或 $\forall$ 作为带各自规则的原始常量，会扩大内核及其可靠性证明。它们改为基于 $=$ 的定义。
• 用异常表示规则失败。 HOL Light 会抛出 Failure。Result 让每个失败都体现在类型中，避免前端意外捕获并忽略失败。
• 不检查规则，另设验证阶段。 只在最后检查可容许性，会让不可容许的中间定理流入后续步骤。因此每条规则都检查其输入和输出。
• 任意公理。 不存在把项变成定理的函数。唯一的非派生定理是定义和类型定义契约，二者都由带保守性条件的闸门产生。

边界

• 内核不解析文本、不精化 (elaboration) 名称，也不运行策略 (tactic)；这些工作由 elab、parser 和 tactics 包完成，且它们都不受信任。
• 它除等词和选择外不实现任何联结词，也没有量词语法；其余部分由 logic 包定义。
• 它不按名称存储已证明的定理。定理名称属于前端的职责。
• 它没有元变量，也没有不完整的定理：证明脚本中的 hole 永远不会到达内核。
• 它不证明自身的可靠性。上文及规范中的论证是纸面证明；formal_verification/ 将规范与 Lean 对齐，而不是与 MoonBit 源码对齐。
• 它不把选择公理作为定理提供。@ 已声明并被 SpecOK 使用，但没有任何公开函数返回 $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 在原始规则的选择上最接近 HOL Light。 ↩

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