形式化验证

MoonBit 通过 moon prove 提供实验性的形式化验证支持。你可以编写可执行的 MoonBit 代码，为这些代码陈述逻辑性质，并借助 SMT 求解器证明生成的证明任务。

从整体上看，工作流程如下：

1. 在 .mbt 文件中编写可执行代码。

2. 在 .mbtp 文件中编写谓词、逻辑辅助函数和引理。

3. 在包中启用证明模式。

4. 运行 moon prove。

概览示例：二分查找

下面这个包简要展示了 MoonBit 中各项验证机制如何配合工作。它展示了：

• 在包级别启用证明

• .mbtp 中的逻辑侧谓词

• .mbt 中的程序侧函数

• 前置条件与后置条件

• 循环不变量与 proof_yield

• 局部的 proof_assert 步骤

• 用 proof_reasoning 对循环进行面向证明的说明

首先，为该包启用证明：

options(
  "proof-enabled": true,
)

然后在 .mbtp 中定义逻辑侧规范：

predicate in_bounds(xs : FixedArray[Int], i : Int) {
  (0 <= i) && (i < xs.length())
}

predicate sorted(xs : FixedArray[Int]) {
  ∀ i : Int, ∀ j : Int,
    in_bounds(xs, i) && in_bounds(xs, j) && (i <= j) →
      xs[i] <= xs[j]
}

predicate binary_search_ok(xs : FixedArray[Int], key : Int, result : Option[Int]) {
  match result {
    None => ∀ i : Int, in_bounds(xs, i) → xs[i] != key
    Some(result) => in_bounds(xs, result) && xs[result] == key
  }
}

最后，在 .mbt 中实现可执行函数：

pub fn binary_search(
  xs : FixedArray[Int],
  key : Int,
) -> Int? where {
  proof_require: sorted(xs),
  proof_ensure: result => binary_search_ok(xs, key, result),
} {
  for i = 0, j = xs.length(); i < j; {
    let h = i + (j - i) / 2
    if xs[h] < key {
      proof_assert ∀ idx : Int,
        (0 <= idx) && (idx < h + 1) → xs[idx] < key
      continue h + 1, j
    } else if key < xs[h] {
      proof_assert ∀ idx : Int,
        (h <= idx) && (idx < xs.length()) → key < xs[idx]
      continue i, h
    } else {
      proof_assert xs[h] == key
      break Some(h)
    }
  } nobreak {
    None
  } where {
    proof_invariant: 0 <= i,
    proof_invariant: i <= j,
    proof_invariant: j <= xs.length(),
    proof_invariant: ∀ idx : Int, (0 <= idx) && (idx < i) → xs[idx] < key,
    proof_invariant: ∀ idx : Int, (j <= idx) && (idx < xs.length()) → key < xs[idx],
    proof_yield: res => binary_search_ok(xs, key, res),
    proof_reasoning: (
      #| The loop maintains a candidate window `[i, j)`.
      #| Every index before `i` is known to hold a value `< key`, and every
      #| index from `j` onward is known to hold a value `> key`.
      #|
      #| At midpoint `h` there are three cases:
      #|   - `xs[h] < key`: move the left boundary to `h + 1`
      #|   - `key < xs[h]`: move the right boundary to `h`
      #|   - otherwise, the element at `h` is equal to `key`
      #|
      #| If the loop exits normally, the exclusion invariants cover the whole
      #| array, so no index can contain `key`.
    ),
  }
}

这个示例已经展示了经过验证的 MoonBit 代码的主要结构：

• sorted 与 binary_search_ok 是逻辑侧谓词

• binary_search 是可执行的程序侧代码

• where { ... } 块将逻辑侧契约附加到函数上

• proof_assert 记录有助于证明器求解的局部条件

• 循环不变量描述逐步收缩的搜索窗口

• proof_reasoning 用结构化文字记录证明思路

本页后续部分会更详细地解释这些组成部分，并介绍 #proof_pure、proof_decrease、proof_axiomatized、基于模型的验证，以及可信边界等附加特性。

环境准备

环境配置

moon prove 依赖外部的 Why3 验证工具链。MoonBit 会将启用了证明的包转换为 Why3，随后由 Why3 将证明任务分派给一个或多个外部求解器。

Why3

在 MoonBit 中运行形式化验证必须安装 Why3。

• 推荐通过 opam 安装 Why3。

• 推荐固定使用的版本为 1.7.2。

使用 opam 更容易让 Why3 与当前 MoonBit 证明流水线所期望的版本保持一致。

外部求解器

还必须至少安装一个外部求解器。

MoonBit 当前支持：

• z3

• cvc5

• alt-ergo

安装多个求解器有助于提高证明覆盖率，但一个可用的环境只需要其中任意一个即可。

在包中启用证明

证明支持是按包在 moon.pkg 中启用的，如上面的概览示例所示。

启用后，该包既可以包含普通的 MoonBit 源文件，也可以包含面向证明的 .mbtp 文件。如果一个模块中的多个包都包含证明，那么每个这样的包都必须分别启用它。

包含验证的代码的结构

源码布局

面向验证的包通常会分成两层：

• .mbt：可执行代码、契约、循环不变量和局部证明步骤

• .mbtp：谓词、抽象模型、不变量和引理

这种拆分方式在保持运行时代码可读性的同时，也让证明结构更加明确。在 二分查找概览示例 中，谓词位于 .mbtp 中，而可执行的搜索函数位于 .mbt 中。

程序侧与逻辑侧

MoonBit 的验证系统明确区分程序侧与逻辑侧。

• 程序侧是可执行的 MoonBit 代码。

• 逻辑侧用于编写规范与证明，它可能根本不对应任何运行时代码。

.mbt 文件中的定义属于程序侧，.mbtp 文件中的定义属于逻辑侧。

这种区分很重要，因为程序侧定义与逻辑侧定义是分离的：

• 程序侧定义是可执行的，可以被普通 MoonBit 代码调用

• 逻辑侧定义用于规范与证明

• .mbtp 中的逻辑侧定义不是普通的运行时函数

• 程序侧代码在执行过程中不会调用逻辑侧定义

• 逻辑侧规范通常也不会任意调用程序侧定义

正因为有这种分离，带证明的包通常会同时包含：

• 供执行时使用的程序侧辅助函数

• 供契约使用的逻辑侧谓词或模型函数

当某个定义需要同时在两侧可见时，就可以使用 #proof_pure。

在 .mbt 文件中，契约和证明注解是逻辑侧推理嵌入程序代码的位置。具体来说：

• proof_require 和 proof_ensure 是附加在程序函数上的逻辑侧规范

• proof_assert 声明一个必须在该位置被证明的逻辑事实

• 诸如 proof_invariant、proof_yield 和 proof_reasoning 之类的循环注解，都是关于可执行循环的逻辑侧陈述

编写规范与证明

.mbt 中的契约

MoonBit 使用 where { ... } 子句来编写函数契约。在二分查找概览示例中，函数契约直接写在程序侧定义上：

• proof_require 声明前置条件。

• proof_ensure 声明后置条件。

• result 指代函数结果。

在可执行代码内部，可以用 proof_assert 记录中间事实，帮助证明器把实现与规范关联起来。

这通常就是把程序侧实现事实连接到逻辑侧谓词和后置条件的地方。

证明专用注解

除了 proof_require、proof_ensure 和 proof_assert 之外，MoonBit 还提供了一些证明专用注解，用于控制证明流水线如何处理这些定义。

#proof_pure

#proof_pure 从验证器的角度将一个函数标记为纯函数。这适用于那些计算逻辑量的辅助函数：它们会出现在谓词和后置条件中，同时又需要在程序侧可见。

#proof_pure
fn height(t : Tree) -> Int {
  match t {
    Empty => 0
    Node(_, _, _, h) => h
  }
}

同一个辅助函数随后就可以在规范中使用：

predicate cached_height_ok(t : Tree, result : Int) {
  result == height(t)
}

#proof_pure 的动机在于，有些计算天然同时属于两侧。例如树的 height 这样的辅助函数，在可执行代码中很有用，而规范也可能需要引用同一个量。

如果没有 #proof_pure，通常就意味着：

• 写一个供执行使用的程序侧定义

• 再写一个供规范使用的逻辑侧定义

• 在使用之前还要证明这两个定义是等价的

#proof_pure 允许一个无副作用的 MoonBit 定义被程序代码和面向证明的逻辑共同使用，从而避免这种重复。

在更大的验证包中，#proof_pure 常用于诸如高度这类结构度量、排序函数、汇总函数，以及其他应当像数学函数一样工作的面向证明的计算。

目前，#proof_pure 辅助函数更适合视为纯规范辅助函数，而不是带完整契约的已验证函数。尤其是，直接给 #proof_pure 定义附加普通验证契约的支持仍然有限。

proof_decrease

proof_decrease 为递归定义提供终止度量。

pub fn countdown(n : Int) -> Int where {
  proof_decrease: n,
  proof_require: 0 <= n,
  proof_ensure: result => 0 <= result,
} {
  if n <= 0 {
    0
  } else {
    countdown(n - 1)
  }
}

当证明器无法仅从函数体中直接看出结构递归或数值度量时，这个注解尤其重要。

proof_axiomatized

proof_axiomatized 将一个带契约的函数或引理标记为“被假定成立”，而不是“被证明成立”。

当某个定义需要供后续证明使用，但其实现或证明被有意留在当前验证边界之外时，这会很有用。

在实践中，应当谨慎使用 proof_axiomatized：

• 用于函数时，表示验证器会直接假定所声明的契约成立

• 用于引理时，表示验证器会直接假定所声明的结论成立

例如：

pub fn assumed_nonnegative(x : Int) -> Int where {
  proof_axiomatized: true,
  proof_require: 0 <= x,
  proof_ensure: result => 0 <= result,
} {
  x
}

当证明仍在开发过程中时，这类声明可以作为临时桥梁；或者当可信边界是有意且明确设定时，也可以使用它。关键在于，moon prove 会把该契约当作假设来使用，而不是从函数体出发对其进行证明。

由于这些假设不会被 moon prove 消解，它们就会成为已验证包可信边界的一部分。

.mbtp 中的谓词与引理

逻辑性质定义在 .mbtp 文件中。在 二分查找概览示例 中，逻辑侧定义了：

• 把 in_bounds 作为基本索引谓词

• 把 sorted 作为输入数组的前置条件

• 把 binary_search_ok 作为把结果与数组及键值关联起来的后置条件

例如，.mbtp 中的谓词可以定义契约所使用的逻辑词汇：

predicate in_bounds(xs : FixedArray[Int], i : Int) {
  (0 <= i) && (i < xs.length())
}

predicate sorted(xs : FixedArray[Int]) {
  ∀ i : Int, ∀ j : Int,
    in_bounds(xs, i) && in_bounds(xs, j) && (i <= j) →
      xs[i] <= xs[j]
}

predicate binary_search_ok(xs : FixedArray[Int], key : Int, result : Option[Int]) {
  match result {
    None => ∀ i : Int, in_bounds(xs, i) → xs[i] != key
    Some(result) => in_bounds(xs, result) && xs[result] == key
  }
}

对于更大的验证包，.mbtp 还会包含：

• 如 model(x) 这样的抽象模型函数

• 如 bridge_inv(x) 或 sparse_array_inv(x) 这样的表示不变量

• 如 deposit_post(...) 这样的具名后置条件

• 可复用的引理

引理是仅用于证明的声明，用来表达可复用的事实。当证明器可以直接消解时，较小的引理可以拥有空函数体；而更大的引理则可以使用递归的证明结构：

lemma height_nonneg_lemma(t : Tree) where {
  proof_decrease: t,
  proof_require: avl_inv(t),
  proof_ensure: 0 <= height(t),
} {
  match t {
    Empty => ()
    Node(l, _x, r, _h) => {
      height_nonneg_lemma(l)
      height_nonneg_lemma(r)
    }
  }
}

在这个例子中，avl_inv 是 AVL 树的表示不变量，而这个引理通过对 t 进行结构递归来证明 height(t) 非负。

引理体会随着求解器所需的证明引导程度而有所不同：

• 有些引理的函数体为空，因为验证器可以直接完成证明

• 有些引理会使用一连串 proof_assert 步骤来显式给出中间事实

• 递归引理还可以调用其他引理，包括在更小输入上递归调用自身

循环不变量

循环通过循环的 where { ... } 块中的证明专用子句来验证。在 二分查找概览示例 中，循环不变量说明了：

• 当前搜索窗口始终是一个合法的区间 [i, j)

• i 之前的每个索引都包含 < key 的值

• 从 j 开始的每个索引都包含 > key 的值

最常见的循环证明注解有：

• proof_invariant：在每次迭代边界都必须成立的事实

• proof_yield：对由 break 产出的值必须成立的事实

• proof_reasoning：解释循环为何正确的面向证明的说明

在实践中，好的循环不变量通常描述当前搜索窗口、前缀或已处理区域，而不是一次性描述整个算法。

基于模型的验证

对于数据结构和有状态系统，最有用的模式通常是：

1. 定义一个抽象模型，

2. 定义一个表示不变量，

3. 针对该抽象模型来为每个操作编写规范。

AVL 树就是这种风格的一个代表性例子：

fn Tree::model(self : Tree) -> Fset[Int] {
  match self {
    Empty => Fset::empty()
    Node(l, x, r, _) => l.model().union(r.model()).add(x)
  }
}

predicate avl_inv(t : Tree) {
  match t {
    Empty => true
    Node(l, x, r, h) =>
      avl_inv(l) &&
      avl_inv(r) &&
      (∀ y : Int, l.model().mem(y) → y < x) &&
      (∀ y : Int, r.model().mem(y) → x < y) &&
      h == 1 + max2(height(l), height(r)) &&
      -1 <= height(l) - height(r) &&
      height(l) - height(r) <= 1
  }
}

这里：

• model() 把具体的树映射为它的抽象有限集合视图

• the quantified conditions inline the ordering constraints over that abstract model

• avl_inv 将递归的良构性、搜索树顺序以及缓存高度的正确性绑定在一起

与在每个契约中直接写庞大的内联布尔公式相比，这种风格的可扩展性要好得多。每个操作都可以基于抽象模型和不变量来编写规范，而实现部分则通过证明局部事实，最终推出相应的具名后置条件。

推荐风格

• 把可执行逻辑放在 .mbt 中，把证明逻辑放在 .mbtp 中。

• 将程序侧和逻辑侧视为两个不同的层次，它们之间只通过一个狭窄的桥梁连接。

• 优先使用具名谓词，而不是大型内联公式。

• 使用小而稳定的不变量和后置条件，例如 *_inv 与 *_post。

• 当证明器需要帮助时，在重要的构造步骤、分支和循环更新之后加入 proof_assert。

• 从简单的算法证明开始，然后再过渡到针对数据结构和协议的基于模型的验证。

• 谨慎设计递归辅助函数：#proof_pure 和 proof_decrease 往往决定了一个证明是否仍然易于维护。

运行验证

moon prove 会检查什么

运行 moon prove 会要求验证器证明如下几类义务：

• 函数前置条件足以保证函数体可以安全执行

• 后置条件在每一条返回路径上都成立

• proof_assert 语句是有效的

• 循环不变量初始成立，并且在循环过程中得以保持

• 当循环形式支持时，循环的终止度量会递减

• 证明所需的边界检查和类似的安全性质

运行验证器

在模块根目录下运行：

moon prove

这会尝试证明当前模块中所有启用了证明的包。

如果只想证明一个包，可以传入它的路径：

moon prove path/to/package

在这种定向模式下，MoonBit 只会尝试证明被选中的包；它的依赖会被当作假设，而不会作为同一条命令的一部分重新证明。

MoonBit 会把启用了证明的包转换为 Why3，并调用已配置的证明器处理生成的验证条件。

moon check 和 moon prove 在这里承担不同的职责。moon check 负责把包作为 MoonBit 代码进行校验，而 moon prove 则尝试消解它的证明义务。

可信模型与限制

受信假设

和任何验证系统一样，MoonBit 的证明体系也有一个可信边界：某些事实由前端和后端直接假定，而不是在用户代码内部加以证明。

任何用户编写且标记为 proof_axiomatized 的项目，也属于这个可信边界。

当前主要的可信假设包括：

• 验证所推理的是数学整数，而不是机器整数

• 任何标记为 proof_axiomatized 的项目都会被当作假设，而不是被证明

对整数来说，这意味着证明义务是在一个无界整数模型下进行检查的。因此：

• 算术证明目前不会建模运行时溢出

• 一个程序在证明模型中可能是正确的，但在实际执行时仍然需要显式的范围约束

• 机器整数验证已经在计划中，但目前还不是默认模型

当前状态

MoonBit 中的形式化验证仍处于实验阶段。表面语法、证明器集成和证明易用性都还在快速演进，因此最好把它视为一种高级特性，主要面向那些确实能从强而可机检的保证中受益的包。

推荐的验证风格

MoonBit 当前的验证器最适合函数式的证明风格，以及基于模型的规范。

诸如局部可变状态和原地 FixedArray 更新这样的命令式特性虽然受支持，但它们在验证中的使用限制更多：

• 可变状态应当保持为局部使用

• FixedArray 的逃逸式使用目前还不受支持

• 当两种写法都可行时，优先选择函数式风格的程序

进一步阅读

如果想查看更多已验证程序和可复用的面向证明的库，请参考 moonbit-community/verified 仓库。