C*：开发与证明一体化

验证条件生成

EN | 中文

上一节中，我们已经为程序写好了契约、循环不变式与内联断言。接下来要回答的是：符号执行引擎如何处理这些断言？它将“程序满足规约”这个命题机械地归结为有限条形如 p |-- qp |-- q 的分离逻辑蕴含，称为验证条件（Verification Conditions，VC）。只要每条 VC 都得到证明，就能保证函数满足契约。本节先回顾经典的最弱前置条件演算，说明它用于 C* 时有哪些不够直观的地方；再介绍 C* 实际采用的前向符号执行，并通过三个例子逐条解释生成的 VC。如何证明这些 VC，是后续章节的主题。

回顾：最弱前置条件演算

回想基于分离逻辑的规约中的霍尔三元组 。契约与不变式写好之后，剩下的是一个可以机械求解的问题：如何从带标注的程序中，计算出需要证明的逻辑命题？一个经典方法是 Dijkstra 提出的最弱前置条件（Weakest Precondition，WP）演算： 是“执行语句 后 成立”所需的最弱前置条件，沿程序结构递归定义：

对于循环，则借助标注的不变式 ：取 ，并额外生成两条证明义务——保持 与出口 。这样，检查整个函数就归结为证明一条蕴含：

这就是经典的验证条件生成器（VCGen），不少演绎验证工具正是按这个思路工作的。

看一个具体例子。下面的程序计算 （），目标后置条件是 ：

给循环标注不变式 ，然后按规则展开 wp。先由循环规则得到 及两条证明义务，再应用两次赋值规则，将 中的 、 依次替换为 、。最终，整个函数的验证归并为一条公式：

逐一检查这三个部分，入口与保持都成立，但是出口无法证明： 只说明循环已经停止，并不意味着 ；若 为负， 无法推出 。实际执行时， 不会为负（，且每轮减一），但不变式中没有记录这条信息，WP 演算便无从利用。将不变式加强为 ，三个部分就都成立了。这也说明了上一节为何要求将边界事实一并纳入不变式。

WP 演算的三个不直观之处

WP 演算简洁而优雅，但直接用于 C* 这样的工具时，有三点不太符合用户编写和验证程序的习惯。

其一，方向与程序相反。 先计算 再计算 ：从 ensureensure 出发，逐句向后代换，而人们编写、阅读和调试程序时通常都是自上而下。在上面 的例子中，只有算完整条公式，才能发现出口无法证明。因此，验证失败时通常很难定位到程序中的某一行。

其二，一个函数一条大 VC。 WP 将整个函数体归并为一条公式。计算 的程序只有五行，生成的 VC 就已经不小；实际的 C 函数还包含指针、结构体与分支，每一步对内存的影响都要编码到公式中，公式规模可能迅速增长。这样一条庞大的 VC 若无法证明（或自动求解超时），用户几乎没有线索可以判断问题出在哪里。

其三，分离逻辑需要魔术棒。在分离逻辑中定义 WP 时，处理堆读写语句需要引入新的连接词。以基于分离逻辑的规约中的写入语句 为例，其最弱前置条件是：

其含义是：可以从当前堆中分离出地址 处的单元，因此写入是安全的；将 处单元的内容改为 ，再与剩余的堆拼接后， 成立。这里的 正是上上节记号表里的魔术棒（Magic Wand）： 表示“再拼接上一块满足 的堆，就得到满足 的堆”。借助魔术棒，在分离逻辑中仍然可以按程序结构计算 WP，但如何自动求解含有魔术棒的蕴含，目前仍是难题。

这三点促使我们考虑另一种做法：从后置条件向后计算，改为让断言沿执行方向向前推进。这样，每行都有一个“当前状态”，证明义务也在相应的代码行生成。在 VSCode 中逐行查看符号状态时，看到的正是这一过程。

QCP 与前向符号执行

C* 当前默认启用的符号执行引擎由 QCP（Qualified C Programming）提供。 QCP 的计算方向与 WP 相反：从 requirerequire 出发，沿程序执行方向逐句计算最强后置条件（Strongest Postcondition），在此过程中生成多条较小的 VC。 QCP 的前向风格源自 VST-Floyd：证明的每一步都向前推进一条“当前断言”，任意时刻的证明目标都是“当前断言 + 剩余程序”，相当于自上而下填写一份证明大纲。 QCP 将这套方法从交互式证明引入自动化工具，用代码标注引导执行。选择前向符号执行的一个直接动机是实时反馈：每写一行代码，就能立即对其进行符号执行，查看执行后的状态；即使函数尚未写完，也能增量验证。

对引擎而言，符号状态（Symbolic State）就是一条分离逻辑断言，也就是在 VSCode 中逐行查看到的断言：它包含 existsexists 绑定的逻辑变量、factfact 表示的纯事实，以及由 data_atdata_at 与表示谓词组成的空间部分。执行从 requirerequire 出发，参数用 __pre__pre 等表示。每种语句都按固定规则推进符号状态：

  • 声明与赋值：从状态中获取表达式内各变量的当前值，再更新目标变量所对应 data_atdata_at 的内容；
  • 读内存（*p*p、v->tailv->tail）：在空间部分查找目标单元对应的 data_atdata_at，并读出其中的值；若未找到，就报错并停止执行。引擎不会自行按定义展开表示谓词，下文的例子二、三会说明这一点；
  • 写内存：同样先找到目标单元，再替换其内容；
  • 分支：将状态分为两份，分别与条件及其否定合取，再各自推进；
  • 循环：以不变式为割点。执行到循环头时，生成一条 VC（“当前状态 |--|-- 不变式”）；随后只保留不变式，与循环条件合取后进入循环体；从循环体末尾回到循环头时，再生成一条 VC，检查不变式是否保持；退出循环后，以“不变式 **** 条件的否定”继续推进；
  • 内联断言：生成一条 VC（当前状态 |--|-- 断言），随后以断言作为新状态，这一点上一节已经讨论过；
  • 函数调用：在当前状态中逐项匹配并移除被调用函数 requirerequire 声明的资源，将其替换为 ensureensure 给出的资源，其余部分保持不变。这就是框架规则在引擎中的应用；匹配后剩余的纯事实则形成 VC；
  • 函数出口：移除当前状态中的局部资源，并将 ensureensure 中的 __return__return 替换为返回值，生成一条 VC：当前状态 |--|-- ensureensure。

这些 VC 的形式都是 p |-- qp |-- q：左边是引擎逐步计算出的符号状态，右边是你写的断言（不变式、内联断言、被调用函数的 requirerequire 或本函数的 ensureensure）。每条 VC 都附有生成它的源代码行号。引擎还会生成第二类 VC，即安全 VC：在可能发生算术溢出、除零、移位越界等 C 未定义行为的位置，生成相应的纯事实证明义务，例子一会说明这一点。

前向符号执行过程：符号状态（右列）沿程序（左列）逐句推进，遇到标注时生成一条 VC（红色）；循环头是割点，经过该处后只保留不变式。

前向符号执行分别解决了 WP 中不够直观的三个问题：

  • 前向：状态沿执行方向推进，每一行都有一个可查看的符号状态，因而 VSCode 面板可以提供“写一行、看一行”的实时反馈；
  • 小而多：VC 在标注处生成，各自附有行号，哪条无法证明，就可以回到对应的代码行检查；
  • 无需魔术棒：读写内存依靠状态中已有的 data_atdata_at，函数调用依靠逐项匹配，整个过程都不需要魔术棒。

还有一点值得说明：并非每条蕴含都会成为你看到的 VC。 QCP 引擎内置了蕴含求解器，结合基于规则的匹配策略与轻量算术求解：它逐项对齐堆部分，当场卸除平凡的纯事实义务。能够自动解决的蕴含不会显示出来。最终看到的 VC 就是自动化尚未解决的证明义务。通常，空间部分已经对齐，剩下的是需要人工证明的纯事实，或是需要按定义展开谓词的步骤。

例子一：算术循环的验证条件

下面回到实际程序，先看上一节的 Gauss 求和：

int sum(int n)
    [[cst::require(`fact(0i <= n) ** fact(n <= 1000i)`)]]
    [[cst::ensure(`fact(2i * __return == n * (n + 1i))`)]]
{
  int s = 0;
  int i = 0;
  while (i < n)
      [[cst::invariant(`exists sv iv.
                          data_at n__addr Tint n__pre **
                          data_at s__addr Tint sv **
                          data_at i__addr Tint iv **
                          fact(0i <= iv) ** fact(iv <= n__pre) **
                          fact(2i * sv == iv * (iv + 1i)) **
                          fact(n__pre <= 1000i)`)]]
  {
    i = i + 1;
    s = s + i;
  }
  return s;
}
int sum(int n)
    [[cst::require(`fact(0i <= n) ** fact(n <= 1000i)`)]]
    [[cst::ensure(`fact(2i * __return == n * (n + 1i))`)]]
{
  int s = 0;
  int i = 0;
  while (i < n)
      [[cst::invariant(`exists sv iv.
                          data_at n__addr Tint n__pre **
                          data_at s__addr Tint sv **
                          data_at i__addr Tint iv **
                          fact(0i <= iv) ** fact(iv <= n__pre) **
                          fact(2i * sv == iv * (iv + 1i)) **
                          fact(n__pre <= 1000i)`)]]
  {
    i = i + 1;
    s = s + i;
  }
  return s;
}

验证这个文件后，会得到两条 VC（输出已按页宽换行；行号以上面的代码清单为准）：

逐条查看这些 VC，可以看出引擎自动处理了哪些义务，又留下了哪些义务。

  • 首先注意未出现的 VC：循环入口处“建立”不变式的义务不在列表中。进入循环前，状态精确地记录了 ss、ii 两个单元的内容均为 0i0i。与不变式逐项匹配后，只剩 一类平凡的算术义务，引擎当场便将其卸除，因此不会显示出来。
  • 溢出检查同样没有出现：i = i + 1i = i + 1 与 s = s + is = s + i 的结果都必须在 intint 范围内，引擎会在这两行各检查一条安全条件。不变式足以让引擎自动卸除这两条义务：iv < n__pre <= 1000iv < n__pre <= 1000 给出了 iv + 1iiv + 1i 的界，而 2i * sv == iv * (iv + 1i)2i * sv == iv * (iv + 1i) 结合 iviv 的界给出了 sv + iv + 1isv + iv + 1i 的界。这也解释了上一节的准则：如果不将 fact(n__pre <= 1000i)fact(n__pre <= 1000i) 记录在不变式中，两条检查都会缺少依据，因而以 VC 的形式显示出来。
  • VC 1 检查不变式的保持：前件是执行完循环体后的状态（ss、ii 的内容都已更新），后件是完整的不变式（existsexists 重新出现）。证明它，需要为 iviv、svsv 选择新的实例，并验证各条 factfact。
  • VC 2 检查函数出口：|--|-- 左边是“不变式 **** 循环条件的否定”。其中所有 data_atdata_at 都已消失，空间部分只剩 empemp，因为返回时引擎会回收局部变量的存储单元，只保留纯事实；右边是 ensureensure（__return__return 已替换为 svsv）。剩下的正是“由 、、 推出 ”这一步初等数学推导。

这个例子展示了 VC 的常见形式：引擎已经对齐并消解了空间部分，留待人工证明的多是纯算术事实。

例子二：遍历数组

上一节讨论数组与链表时，还有一个问题没有展开：不变式中的资源折叠在包装谓词中，直接执行会报错。下面看实际的报错信息。移除上一节 clearclear 循环体内的内联断言，再次验证，引擎就会在 *p = 0*p = 0 处停止执行：

注意，这里报告的是错误，并非 VC：写入 *p*p 时，状态中必须有可直接使用的单元 undef_data_at (arr__pre + iv * sizeof Tchar) Tcharundef_data_at (arr__pre + iv * sizeof Tchar) Tchar，而该单元折叠在 undef_suffixundef_suffix 中。引擎不会替你决定何时按定义展开谓词，因此无法继续执行。报错随附的符号状态提供了排查问题的线索：从中可以直接看出，缺失的资源包含在哪个谓词的定义中。

补回上一节那条“展开一步”的内联断言，就能完成整个函数的符号执行，并生成四条 VC：

VC 位置 义务
1 whilewhile 行 建立：入口状态 |--|-- 不变式
2 断言行 改写：循环体状态 |--|-- 断言（展开 undef_suffixundef_suffix 一个单元）
3 循环体末尾 保持：写入后的状态 |--|-- 不变式
4 函数末尾 出口：不变式 **** 退出条件 |--|-- ensureensure

与例子一不同，这次“建立”不变式的义务也保留为 VC。要将 undef_bytes arr__pre n__preundef_bytes arr__pre n__pre 改写为“含零个单元的前缀 **** 覆盖整段的后缀”（zero_bytes arr__pre 0i ** undef_suffix arr__pre 0i n__prezero_bytes arr__pre 0i ** undef_suffix arr__pre 0i n__pre），需要按定义展开这三个谓词，超出了自动策略的能力范围。四条 VC 中，最值得细看的是断言处的 VC 2。上一节说过，assertassert 保留了原来的证明义务，使符号执行能够继续，而将这条义务留待之后证明。这里生成的正是这条 VC：

两边的各项几乎相同。右边列出的是断言自身的纯事实，因此没有 iv <= n__preiv <= n__pre，而 iv < n__preiv < n__pre 已经蕴含了它。空间部分的差异全部集中在最后一行半：需要将左边的 undef_suffix arr__pre iv n__preundef_suffix arr__pre iv n__pre 拆分为第一个单元与剩余后缀。这一步依赖 undef_suffixundef_suffix 与 undef_array_atundef_array_at 的定义，后续需要编写的正是这一步的证明。函数出口处的 VC 4 则比较短：

由边界事实可得 iv == n__preiv == n__pre，此时后缀长度为零，化简为空堆，而前缀恰好覆盖整段数组。上一节对“出口”的解释，在这里表述为一条蕴含。

例子三：反转链表

链表的情况基本相同。移除内联断言后直接验证 reversereverse，引擎会在读取 v->tailv->tail 时停止执行：

tailtail 字段对应的单元折叠在 sll vv l2sll vv l2 中。补回上一节的断言后，符号执行可以完成，同样得到四条 VC（建立、断言、保持、出口）。其中，断言处的 VC 将 sllsll 按非空分支展开：

证明这条 VC 要用到两条事实：vvvv 非空时，sll vv l2sll vv l2 只可能来自定义中的 CONSCONS 分支，因此 l2l2 必为某个 x :: xsx :: xs，展开后便得到头节点两个单元的 data_atdata_at 与剩余链表的 sll q xssll q xs；对于列表，还需要将 l == l1 ++ l2l == l1 ++ l2 改写为 l == l1 ++ x :: xsl == l1 ++ x :: xs。

VC 2 两侧的堆：左边的 sll vv l2sll vv l2 表示折叠的整条链表；右边展开出头节点两个单元的 data_atdata_at，以尾指针 qq 为起点的剩余链表仍折叠在 sll q xssll q xs 中。

检查不变式保持的 VC，其前件记录了三个指针更新后的状态：ww 的内容已是 vvvv，vv 的内容已是 qq，头节点的 FtailFtail 单元已改写为 wvwv。证明时，需要将这些资源重新折叠为不变式中的两段 sllsll。出口处的 VC 同样简短：

上一节对“出口”的三行解释，在这里归结为一条蕴含：由 vv == 0ivv == 0i 与 sll vv l2sll vv l2，按定义中的空列表分支可得 l2 == []l2 == []，进而得到 l1 == ll1 == l。这样，左边的 sll wv (REVERSE l1)sll wv (REVERSE l1) 就是要证明的结论。

在编辑器中查看验证条件

本节展示的输出都可以在 VSCode 中查看，入口与查看符号状态相同（右键单击并选择 Show Symbolic StateShow Symbolic State）：

  • 光标位于函数体内的某一行：面板显示该行的符号状态，即前向符号执行推进到此处得到的最强后置条件；
  • 光标位于文件级的某一行（比如文件末尾）：面板显示截至该处累计生成的验证条件列表，每条都标有编号与行号（VC n line lVC n line l），展开后由 |--|-- 分为两侧。

VC 列表非空，意味着验证尚未完成，还需要通过证明卸除这些义务。具体做法是在 [[cst::proof]][[cst::proof]] 中编写证明代码，构造定理、改写符号状态，直到引擎能够卸除每条 VC。后续章节将介绍这一过程。

小结

  • 验证条件（VC）是形如 p |-- qp |-- q 的分离逻辑蕴含：左边是引擎计算出的符号状态，右边是你写的断言；程序满足规约 所有 VC 得到证明。
  • 经典的 WP 演算有三点不够直观：从 ensureensure 向后代换，将整个函数归并为一条大公式，并且在分离逻辑中需要使用魔术棒。
  • C* 默认的符号执行引擎由 QCP 提供，思想源自 VST-Floyd：从 requirerequire 出发，沿程序执行方向计算最强后置条件；在循环头（建立/保持）、内联断言、函数调用与函数出口生成 VC，另有溢出、除零等安全 VC，每条都附有行号。
  • 读写内存所需的资源必须在状态中直接可见：缺少资源会导致错误，而非生成 VC；何时按定义展开谓词，需要由你通过断言（或证明）指定。
  • 引擎能自动卸除的蕴含义务不会显示出来。可见的 VC 是自动化尚未解决的部分，常见情况是空间部分已经对齐、只剩纯事实，或是还需要按定义展开一次谓词。