C* 中的前向证明

EN | 中文

上一节介绍了如何用元语言中的程序表示证明。前向证明从公理与已有定理出发，逐步应用推理规则，直到得到要证明的结论。那里采用的元语言是 ML，而 C* 的证明写在 C 代码的 [[cst::proof]][[cst::proof]] 块中。那么，C 如何与 HOL Light 对接？我们又该如何在 C* 中构造前向证明？本节围绕这两个问题，介绍两类前向证明：一类是通用的，只涉及逻辑与算术；另一类则涉及分离逻辑。这里只讨论前向证明的构造，后向（目标导向）的策略和操作式写法留待后续章节介绍。

C* 如何连接 HOL Light

经典 LCF 以 ML 为元语言：证明是 ML 程序，thmthm 是抽象类型，只有内核能构造这个类型的值。 C* 则让 C 本身成为编写证明的语言，[[cst::proof]][[cst::proof]] 中的代码就是证明程序。这里有一个困难：上一节所说的定理安全性依赖宿主语言的类型抽象，而 C 并不提供这种保障。通过指针运算与强制类型转换，证明代码就可以绕过接口，直接改写 thmthm 的结论，伪造定理。

解决办法是让证明代码与内核分别运行在两个进程中，通过受控的接口通信。这就是客户端/服务器（Client/Server）模型：

客户端就是 [[cst::proof]][[cst::proof]] 中的 C 证明代码。它只持有指向逻辑对象的不透明句柄（Opaque Handle），实际的对象保存在服务器中。termterm、thmthm、typetype 在 C 侧都是不透明类型，只能通过接口函数传递，无法查看或改写其内部。
服务器是一个独立进程，包含 HOL Light 及其可信内核，并通过对象存储（Object Store）维护句柄到实际逻辑对象的映射。

这样，mp_rule(h1, h2)mp_rule(h1, h2) 实际上是一次远程过程调用：服务器先找到句柄 h1h1、h2h2 对应的定理，交给内核执行原始推理规则，再将得到的新定理存入对象存储，返回一个新句柄。这里的关键在于进程隔离（Process Isolation）：即使客户端滥用指针，也无法访问服务器进程中的逻辑对象。可信计算基（TCB）因此仍然只有这个小内核，上一节的完全可扩展性（Full Expansiveness）也在 C 中得以保留：无论 [[cst::proof]][[cst::proof]] 中写了什么，每个定理最终都由内核的原始规则生成。

C* 将 C 与 HOL Light 连接起来：[[cst::proof]][[cst::proof]] 中的 C 代码是客户端，只持有不透明句柄；真正的逻辑对象与可信内核在隔离的服务器进程里，二者通过传递句柄的 RPC 通信。

通用的前向证明

证明标准库采用了清晰的命名规则：*_rule*_rule 用于前向构造定理，*_conv*_conv（变换）将一个项映射为一条等式定理，*_TAC*_TAC 则是后向（目标导向）的策略，留待后续章节介绍。编写前向证明也就是依次调用 *_rule*_rule 与变换。先看构造定理所需的基本操作，以下代码都写在 [[cst::proof]][[cst::proof]] 声明中：


#include "proof/proof.h"
[[cst::proof]] term t1 = `x + 1`;                     // 反引号：直接写一个逻辑项
[[cst::proof]] term t2 = parse_term("x + 1");         // 或从字符串解析
[[cst::proof]] type ty = type_of(t1);
[[cst::proof]] thm r1 = refl_rule(`x + 1`);           // |- x + 1 = x + 1
[[cst::proof]] thm r2 = assume_rule(`x + 1 == y`);    // x + 1 == y |- x + 1 == y
[[cst::proof]] thm r3 = sym_rule(r2);                 // 前向：把等式翻转
[[cst::proof]] thm r4 = arith_rule(`a + b == b + a`); // 线性算术判定过程
[[cst::proof]] thm r5 = apply_conversion(             // 把变换作用到一个项上
    once_rewrite_conv(THM_LIST(r4)), `(a + b) * c`);


#include "proof/proof.h"
[[cst::proof]] term t1 = `x + 1`;                     // 反引号：直接写一个逻辑项
[[cst::proof]] term t2 = parse_term("x + 1");         // 或从字符串解析
[[cst::proof]] type ty = type_of(t1);
[[cst::proof]] thm r1 = refl_rule(`x + 1`);           // |- x + 1 = x + 1
[[cst::proof]] thm r2 = assume_rule(`x + 1 == y`);    // x + 1 == y |- x + 1 == y
[[cst::proof]] thm r3 = sym_rule(r2);                 // 前向：把等式翻转
[[cst::proof]] thm r4 = arith_rule(`a + b == b + a`); // 线性算术判定过程
[[cst::proof]] thm r5 = apply_conversion(             // 把变换作用到一个项上
    once_rewrite_conv(THM_LIST(r4)), `(a + b) * c`);

每个 *_rule*_rule 都返回一个 thmthm；apply_conversion(<变换>, <项>)apply_conversion(<变换>, <项>) 则用指定的变换计算等式，再以 thmthm 的形式返回。新的常量、函数与数据类型通过C* 中的分离逻辑介绍过的定义机制引入，它们都是保守扩展，返回相应的定义、递归或归纳定理：


[[cst::proof]] indtype nlist = new_datatype_definition(
    "nlist = nil | cons num nlist");
[[cst::proof]] thm app_def = new_rec_definition(nlist.rec,
    `app nil l = l &&
     app (cons h t) l = cons h (app t l)`);


[[cst::proof]] indtype nlist = new_datatype_definition(
    "nlist = nil | cons num nlist");
[[cst::proof]] thm app_def = new_rec_definition(nlist.rec,
    `app nil l = l &&
     app (cons h t) l = cons h (app t l)`);

有了这些操作，我们就能前向地证明定理。下面证明 forall l. app l nil = lforall l. app l nil = l，即 nilnil 是 appapp 的右单位元。整个证明自底向上构造，无须设立目标：


[[cst::proof]] thm app_nil_r(void) {
  // 基本情况： |- app nil nil = nil，用 app 的定义改写
  thm base_eq = apply_conversion(rewrite_conv(THM_LIST(app_def)), `app nil nil`);
  // 归纳步骤：在归纳假设 ih 下改写，再全称化、卸除假设
  thm ih = assume_rule(`app t nil = t`);
  thm step_eq = apply_conversion(
      rewrite_conv(THM_LIST(app_def, ih)), `app (cons h t) nil`);
  step_eq = gen_all_rule(disch_all_rule(step_eq));
  // 把归纳定理实例化到我们的谓词上，再把基本情况、归纳步骤传入
  thm ind_thm = beta_rule(spec_rule(`\l. app l nil = l`, nlist.ind));
  thm result  = mp_rule(ind_thm, conj_rule(base_eq, step_eq));
  //  |- forall l. app l nil = l
  return result;
}
[[cst::proof]] thm app_nil_r_thm = app_nil_r();


[[cst::proof]] thm app_nil_r(void) {
  // 基本情况： |- app nil nil = nil，用 app 的定义改写
  thm base_eq = apply_conversion(rewrite_conv(THM_LIST(app_def)), `app nil nil`);
  // 归纳步骤：在归纳假设 ih 下改写，再全称化、卸除假设
  thm ih = assume_rule(`app t nil = t`);
  thm step_eq = apply_conversion(
      rewrite_conv(THM_LIST(app_def, ih)), `app (cons h t) nil`);
  step_eq = gen_all_rule(disch_all_rule(step_eq));
  // 把归纳定理实例化到我们的谓词上，再把基本情况、归纳步骤传入
  thm ind_thm = beta_rule(spec_rule(`\l. app l nil = l`, nlist.ind));
  thm result  = mp_rule(ind_thm, conj_rule(base_eq, step_eq));
  //  |- forall l. app l nil = l
  return result;
}
[[cst::proof]] thm app_nil_r_thm = app_nil_r();

（文件作用域不允许独立的语句块，所以我们将证明写在一个返回定理的幽灵函数中，再通过后面的声明调用这个函数。）逐行来看，每一步都由已有定理生成新定理。首先，用 app_defapp_def 改写得到 base_eqbase_eq 和 step_eqstep_eq。然后，对数据类型自带的归纳定理 nlist.indnlist.ind 应用 spec_rulespec_rule（实例化）与 beta_rulebeta_rule（-归约），将它特化到谓词 \l. app l nil = l\l. app l nil = l，得到 ind_thmind_thm。最后，conj_ruleconj_rule 将基本情况与归纳步骤组合为一条合取定理，mp_rulemp_rule（假言推理）再将它应用于归纳定理，得到 resultresult。这就是“前向”的含义：从叶节点（已知定理）出发，逐步向上构造，直到得到要证明的结论。

forall l. app l nil = lforall l. app l nil = l 的前向推导：箭头自下而上，已知定理经 specspec/betabeta、conj_ruleconj_rule、mp_rulemp_rule 汇聚成 resultresult。方向恰与上一节后向证明的目标分解树相反。

用前向证明卸除验证条件

上面的 appapp 例子是纯粹的逻辑演算，还没有涉及 C 程序。回忆验证条件生成：符号执行引擎执行到 [[cst::proof]][[cst::proof]] 处时，持有一个符号状态，并可能留下待证的验证条件（VC）。前向证明在这里的用法是：读出当前符号状态，前向构造一条定理，再将其写回以推进状态。这里需要三个接口：cst_get_symbolic_state()cst_get_symbolic_state() 读出当前状态（一个断言），cst_set_symbolic_state(...)cst_set_symbolic_state(...) 写入一条“从当前状态到新状态”的蕴含，eq2ent(...)eq2ent(...) 将一条等式定理转换为这样的蕴含。

下面验证 twicetwice：它计算 (n+1) + (n-1)(n+1) + (n-1)，规约要求结果等于 doubl(n)doubl(n)。这里的 doubldoubl 是通过 new_fun_definitionnew_fun_definition 定义并导出的逻辑函数，定义为 doubl(x) = x + xdoubl(x) = x + x。


#include "proof/proof.h"
[[cst::proof]] thm doubl_def = new_fun_definition(`doubl(x:int) = x + x`);
[[cst::proof]] int _e = cst_add_const_to_header(`doubl`);
int twice(int n)
    [[cst::require(`fact(0i <= n && n <= 100i)`)]]
    [[cst::ensure(`fact(__return == doubl(n))`)]]
{
  int a = n + 1;
  int b = n - 1;
  int r = a + b;
  [[cst::proof]] {
    term st = cst_get_symbolic_state();
    thm eq = int_arith_rule(`(a + 1i) + (b - 1i) == (a + b)`);    // 前向构造等式
    thm st_eq = apply_conversion(rewrite_conv(THM_LIST(eq)), st); // 改写状态
    cst_set_symbolic_state(eq2ent(st_eq));                        // 推进
  }
  [[cst::proof]] {
    term st = cst_get_symbolic_state();
    thm st_eq = apply_conversion(
        rewrite_conv(THM_LIST(sym_rule(doubl_def))), st);         // 用 doubl 定义反向改写
    cst_set_symbolic_state(eq2ent(st_eq));
  }
  return r;
}


#include "proof/proof.h"
[[cst::proof]] thm doubl_def = new_fun_definition(`doubl(x:int) = x + x`);
[[cst::proof]] int _e = cst_add_const_to_header(`doubl`);
int twice(int n)
    [[cst::require(`fact(0i <= n && n <= 100i)`)]]
    [[cst::ensure(`fact(__return == doubl(n))`)]]
{
  int a = n + 1;
  int b = n - 1;
  int r = a + b;
  [[cst::proof]] {
    term st = cst_get_symbolic_state();
    thm eq = int_arith_rule(`(a + 1i) + (b - 1i) == (a + b)`);    // 前向构造等式
    thm st_eq = apply_conversion(rewrite_conv(THM_LIST(eq)), st); // 改写状态
    cst_set_symbolic_state(eq2ent(st_eq));                        // 推进
  }
  [[cst::proof]] {
    term st = cst_get_symbolic_state();
    thm st_eq = apply_conversion(
        rewrite_conv(THM_LIST(sym_rule(doubl_def))), st);         // 用 doubl 定义反向改写
    cst_set_symbolic_state(eq2ent(st_eq));
  }
  return r;
}

两块证明都采用相同的步骤：读状态 → 前向构造一条等式定理 → 用它改写状态 → 写回。第一块把 (a+1) + (b-1)(a+1) + (b-1) 化简为 a + ba + b；第二块用 doubldoubl 的定义（经 sym_rulesym_rule 翻转为 x + x == doubl(x)x + x == doubl(x) 的方向）把 a + ba + b 归并为 doubl(n)doubl(n)。两步过后，符号状态里的返回值恰好是 doubl(n)doubl(n)，末尾的 VC 也就得以卸除。

在 VSCode 中开发证明

编写前一节的两块证明时，我们需要不断查看符号状态，根据状态的变化调整证明。C* 的 VSCode 扩展提供了相应的反馈。

在任意一行上右键单击，选择 Show Symbolic StateShow Symbolic State（快捷键 alt+rightalt+right，macOS 上 ctrl+alt+rightctrl+alt+right；我们在第一个 C* 程序用过它），右侧面板就显示该行执行之后的符号状态；在函数出口或文件末尾查看，面板显示的则是待证的验证条件（形如 … |-- …… |-- …）。也可以在证明块内查看每个步骤之后的状态；顶层证明函数的函数体没有符号状态，不支持在其中查看。

以 twicetwice 为例，在 int r = a + b;int r = a + b; 一行查看，面板显示：

符号状态 @ int r = a + b;int r = a + b; 后


fact (0i <= n__pre) ** fact (n__pre <= 100i) **
data_at r__addr Tint ((n__pre + 1i) + n__pre - 1i) **
data_at b__addr Tint (n__pre - 1i) **
data_at a__addr Tint (n__pre + 1i) **
data_at n__addr Tint n__pre


fact (0i <= n__pre) ** fact (n__pre <= 100i) **
data_at r__addr Tint ((n__pre + 1i) + n__pre - 1i) **
data_at b__addr Tint (n__pre - 1i) **
data_at a__addr Tint (n__pre + 1i) **
data_at n__addr Tint n__pre

从中可以看出还需要证明什么：rr 所在的单元存储着尚未化简的和 (n+1) + (n-1)(n+1) + (n-1)，而后置条件要求它等于 doubl(n)doubl(n)。我们可以按以下步骤反复调整证明：

查看状态：在证明块前后的语句行选择 Show Symbolic StateShow Symbolic State，查看当前状态，确定还需要证明什么；
查找工具：找到完成这一步证明所需的引理或变换。C* 的工具链可以按名称或命题陈述搜索数千条命名定理与变换，例如 doubldoubl 的定义定理、整数算术的判定过程；
编写前向证明块：在 [[cst::proof]][[cst::proof]] 里用 *_rule*_rule/*_slrule*_slrule/变换构造定理，再用 local_applylocal_apply 或 cst_set_symbolic_statecst_set_symbolic_state 推进状态；
再次查看状态：重新选择 Show Symbolic StateShow Symbolic State，确认状态按预期推进，并在文件末尾检查验证条件是否已被清除；
重复以上步骤，直到所有验证条件都被卸除。

如果某条规则应用失败，错误信息会给出规则名和参数，并说明不匹配之处。例如，传给 spec_rulespec_rule 的项与最外层绑定变量的类型不符时，错误信息会同时显示这个项、绑定变量及各自的类型。我们通常可以据此确定如何修改。

写完 twicetwice 的两块证明后，在第二块的最后一行查看：

符号状态 @ 第二块证明之后


fact (0i <= n__pre) ** fact (n__pre <= 100i) **
data_at r__addr Tint (doubl n__pre) **
data_at b__addr Tint (n__pre - 1i) **
data_at a__addr Tint (n__pre + 1i) **
data_at n__addr Tint n__pre


fact (0i <= n__pre) ** fact (n__pre <= 100i) **
data_at r__addr Tint (doubl n__pre) **
data_at b__addr Tint (n__pre - 1i) **
data_at a__addr Tint (n__pre + 1i) **
data_at n__addr Tint n__pre

rr 所在单元存储的值已变为 doubl n__predoubl n__pre，末尾的验证条件随之清除。前向证明的开发因此是状态驱动的：你始终关注当前状态，逐步推进，直到满足后置条件。

一个完整的例子：McCarthy 91

现在将前面的方法用于一个完整的递归程序。McCarthy 91 是一个经典函数：当 n > 100n > 100 时返回 n - 10n - 10，否则返回 9191。


#include "proof/proof.h"
int mc91(int n)
    [[cst::require(`fact(0i <= n)`)]]
    [[cst::ensure(`fact(n > 100i ==> __return == n - 10i) **
                   fact(n <= 100i ==> __return == 91i)`)]]
{
  if (n > 100) {
    [[cst::proof]] {
      // 取出 n 的 data_at 单元蕴含的取值范围，并入符号状态
      thm rng = rewrite_rule(THM_LIST(get_theorem_by_name("min_of_def"),
                                      get_theorem_by_name("max_of_def")),
          spec_rule(`n__pre:int`, spec_rule(`Tint`,
              spec_rule(`n__addr:int`, get_data_at_range()))));
      cst_set_symbolic_state(local_apply(cst_get_symbolic_state(), rng));
    }
    return n - 10;
  }
  return mc91(mc91(n + 11));
}


#include "proof/proof.h"
int mc91(int n)
    [[cst::require(`fact(0i <= n)`)]]
    [[cst::ensure(`fact(n > 100i ==> __return == n - 10i) **
                   fact(n <= 100i ==> __return == 91i)`)]]
{
  if (n > 100) {
    [[cst::proof]] {
      // 取出 n 的 data_at 单元蕴含的取值范围，并入符号状态
      thm rng = rewrite_rule(THM_LIST(get_theorem_by_name("min_of_def"),
                                      get_theorem_by_name("max_of_def")),
          spec_rule(`n__pre:int`, spec_rule(`Tint`,
              spec_rule(`n__addr:int`, get_data_at_range()))));
      cst_set_symbolic_state(local_apply(cst_get_symbolic_state(), rng));
    }
    return n - 10;
  }
  return mc91(mc91(n + 11));
}

后置条件采用条件式写法：分别规定 n > 100n > 100 与 n <= 100n <= 100 时的返回值，再用 **** 将两条事实合取。

唯一的证明块位于 n > 100n > 100 分支中，它完成了一项常见操作：把参数的取值范围显式地提取出来。函数入口给出的事实只有 fact(0i <= n)fact(0i <= n)。不过，符号状态中还有 nn 对应的单元 data_at n__addr Tint n__predata_at n__addr Tint n__pre，这个 intint 类型的单元本身就蕴含了 n__pren__pre 在 intint 取值范围内。get_data_at_range()get_data_at_range() 就是这条通用引理，三层嵌套的 spec_rulespec_rule 将它实例化为关于 nn 的地址、类型 TintTint 与取值 n__pren__pre 的引理；外层的 rewrite_rulerewrite_rule 用 min_ofmin_of/max_ofmax_of 的定义把边界化为具体数值，local_applylocal_apply 再把得到的范围事实并入状态。

要理解为什么需要这个证明块，可以将其删除，再在函数出口查看验证条件。面板会显示：

验证条件 @ 删去证明块后


fact (n__pre > 100i) ** fact (0i <= n__pre) ** data_at n__addr Tint n__pre
|--
fact (n__pre - 10i <= 2147483647i) **
fact (-- 2147483648i <= n__pre - 10i) **
data_at n__addr Tint n__pre


fact (n__pre > 100i) ** fact (0i <= n__pre) ** data_at n__addr Tint n__pre
|--
fact (n__pre - 10i <= 2147483647i) **
fact (-- 2147483648i <= n__pre - 10i) **
data_at n__addr Tint n__pre

这正是 n - 10n - 10 的 intint 溢出安全检查：前件中的两条事实没有给出 n__pren__pre 的上界，因此无法证明右侧的 n__pre - 10i <= 2147483647in__pre - 10i <= 2147483647i。证明块用 get_data_at_rangeget_data_at_range 补充上界 n__pre <= 2147483647n__pre <= 2147483647。有了它，引擎就能证明 n - 10n - 10 不溢出，并推进两个分支的后置条件。

递归调用无须任何特殊处理：引擎在每个调用点直接应用被调用函数的契约。mc91(mc91(n + 11))mc91(mc91(n + 11)) 的内外两次调用各自以 mc91mc91 的规约为准。C* 只验证部分正确性，不产生终止性证明义务，因此递归本身不需要单独的证明。

分离逻辑的前向证明

一旦证明涉及堆，等式就不够了，需要分离逻辑蕴含 |--|--（见C* 中的分离逻辑）。与 *_rule*_rule 相对应，证明标准库还提供一族 *_slrule*_slrule，用于前向构造以 |--|-- 为结论的定理。以下是几条常用规则，其中表示 |--|--，表示分离合取 ****：

trans_slruletrans_slrule 把两条蕴含首尾相接；frame_right_slruleframe_right_slrule 是分离逻辑的框架规则，在两侧同时添加一块与原有堆互不重叠的堆 FF；intro_fact_slruleintro_fact_slrule 把一条已证的纯事实 pp 注入空间蕴含的右侧。 local_applylocal_apply 用这些蕴含推进符号状态：它以当前状态为前件，通过框架规则，将一条小足迹蕴含（只涉及操作所需的几块堆）推广到整个堆，导出下一状态。这样，只涉及局部的蕴含也能作用于完整状态。

以单链表谓词 sllsll为例。要读写链表节点，需要先将 sll pt lsll pt l 展开成头、尾两块 data_atdata_at 资源。展开操作由一条预先证明的蕴含引理给出。它的证明用到后向策略，将在后续章节介绍；这里先将它作为已有定理，用于前向证明：


// sll_unfold（已在别处证明）：
//   forall l pt.
//     ~(pt == 0i) ==>
//     ( sll pt l |-- exists x xs q. fact(l == x :: xs)
//                      ** data_at (field_addr pt Tlist Fhead) Tint x
//                      ** data_at (field_addr pt Tlist Ftail) Tptr q
//                      ** sll q xs )


// sll_unfold（已在别处证明）：
//   forall l pt.
//     ~(pt == 0i) ==>
//     ( sll pt l |-- exists x xs q. fact(l == x :: xs)
//                      ** data_at (field_addr pt Tlist Fhead) Tint x
//                      ** data_at (field_addr pt Tlist Ftail) Tptr q
//                      ** sll q xs )

在循环体中，已知 v != 0v != 0，也就知道链表非空。此时可以前向应用这条引理：


[[cst::proof]] {
  thm ent = undisch_rule(
      spec_rule(`vv:addr`, spec_rule(`l2:(int)list`, sll_unfold)));
  cst_set_symbolic_state(local_apply(cst_get_symbolic_state(), ent));
}


[[cst::proof]] {
  thm ent = undisch_rule(
      spec_rule(`vv:addr`, spec_rule(`l2:(int)list`, sll_unfold)));
  cst_set_symbolic_state(local_apply(cst_get_symbolic_state(), ent));
}

spec_rulespec_rule 每次应用都实例化引理最外层的变量，因此内层调用将 ll 实例化为当前列表 l2l2，外层调用将 ptpt 实例化为指针 vvvv；undisch_ruleundisch_rule 将前提 ~(vv == 0i)~(vv == 0i) 移入定理的假设；local_applylocal_apply 根据符号状态中已有的这条事实卸除假设，再把展开蕴含作用到当前状态上，将 sll vv l2sll vv l2 替换为展开后的头、尾节点。这段证明无须为 VC 设立目标，而是以当前状态为前件，自左向右导出下一状态。这正是前向证明的过程。

两类前向证明常常配合使用：先用通用的前向证明得到一条纯事实，再将它注入空间状态。下面的片段把一条已证的等式事实 wantwant（例如某个列表恒等式）经 intro_fact_slruleintro_fact_slrule 注入状态：


[[cst::proof]] {
  // want : |- ...（一条前向证得的纯事实）
  cst_set_symbolic_state(local_apply(cst_get_symbolic_state(),
      intro_fact_slrule(want, refl_slrule(`emp`))));
}


[[cst::proof]] {
  // want : |- ...（一条前向证得的纯事实）
  cst_set_symbolic_state(local_apply(cst_get_symbolic_state(),
      intro_fact_slrule(want, refl_slrule(`emp`))));
}

refl_slrule(emp)refl_slrule(emp) 提供一条平凡的空堆蕴含 emp |-- empemp |-- emp 作为载体，intro_fact_slruleintro_fact_slrule 把纯事实 wantwant 附加于其上，local_applylocal_apply 再将得到的蕴含应用于状态，只添加这条事实，堆保持不变。

一个完整的例子：清零数组

前面通过 sllsll 展示了一步前向证明。下面给出一个完整通过验证，且证明完全前向的程序：clear(char *arr, int n)clear(char *arr, int n) 递归地将 arrarr 的前 nn 个字节清零，整个过程不使用后向证明。

讨论单个内存单元时我们用 data_atdata_at；讨论一段连续内存则用它的数组版：array_at array_at 表示从地址起有个类型单元，依次存储列表中的元素；undef_array_at x T nundef_array_at x T n 则是个未初始化的单元。由于契约不能直接接受带 C 类型参数的谓词，我们先用 new_fun_definitionnew_fun_definition 将它们分别封装为单态谓词并导出。其中，undef_char_array arr nundef_char_array arr n 表示 nn 个未初始化字节，zeroed arr nzeroed arr n 表示 nn 个值为 00 的字节。后者定义为 array_at arr Tchar n (ireplicate n 0i)array_at arr Tchar n (ireplicate n 0i)，其中 ireplicate n 0iireplicate n 0i 是由 nn 个 00 组成的列表。相应的规约为：入口 fact(0i <= n) ** undef_char_array arr nfact(0i <= n) ** undef_char_array arr n，出口 zeroed arr nzeroed arr n。


#include "proof/proof.h"
// 契约不能直接接受带 ctype 的谓词，故把 char 数组的两个谓词各包一层单态版本。
[[cst::proof]] thm undef_char_array_def = new_fun_definition(
    `undef_char_array (x:addr) (n:int) : hprop = undef_array_at x Tchar n`);
[[cst::proof]] int _e1 = cst_add_const_to_header(`undef_char_array`);
[[cst::proof]] thm zeroed_def = new_fun_definition(
    `zeroed (x:addr) (n:int) : hprop = array_at x Tchar n (ireplicate n 0i)`);
[[cst::proof]] int _e2 = cst_add_const_to_header(`zeroed`);
void clear(char *arr, int n)
    [[cst::require(`fact(0i <= n) ** undef_char_array arr n`)]]
    [[cst::ensure(`zeroed arr n`)]]
{
  if (n == 0) {
    // 基本情况：undef_char_array arr 0 -|- emp -|- zeroed arr 0。
    [[cst::proof]] {
      thm repl_nil = apply_conversion(
          pure_rewrite_conv(THM_LIST(
              assume_rule(`n__pre == 0i`),
              get_theorem_by_name("IREPLICATE_DEF"),
              get_theorem_by_name("NUM_OF_INT_OF_NUM"),
              get_theorem_by_name("REPLICATE"))),
          `ireplicate n__pre 0i`);
      thm e_uz = undisch_rule(spec_rule(`n__pre:int`, spec_rule(`Tchar`,
          spec_rule(`arr__pre:int`,
              get_theorem_by_name("undef_array_at_zero")))));
      thm e_az = mp_rule(mp_rule(
          spec_rule(`ireplicate n__pre 0i`, spec_rule(`n__pre:int`,
              spec_rule(`Tchar`, spec_rule(`arr__pre:int`,
                  get_theorem_by_name("array_at_zero"))))),
          assume_rule(`n__pre == 0i`)), repl_nil);
      thm d_all = apply_conversion(
          once_rewrite_conv(THM_LIST(undef_char_array_def)),
          `undef_char_array (arr__pre:int) (n__pre:int)`);
      thm d_z = apply_conversion(once_rewrite_conv(THM_LIST(zeroed_def)),
          `zeroed (arr__pre:int) (n__pre:int)`);
      cst_set_symbolic_state(local_apply(cst_get_symbolic_state(),
          eq2ent(list_trans_rule(THM_LIST(
              d_all, e_uz, sym_rule(e_az), sym_rule(d_z))))));
    }
    return;
  };
  // n >= 1，从末尾切下最后一字节：
  //   undef_char_array arr n |--
  //     undef_char_array arr (n-1) ** undef_data_at (arr + (n-1)*sizeof Tchar) Tchar
  [[cst::proof]] {
    // 从 n 的 data_at 单元取出取值范围，供 n - 1 的下标与减法安全性检查。
    thm rng = rewrite_rule(THM_LIST(get_theorem_by_name("min_of_def"),
                                    get_theorem_by_name("max_of_def")),
        spec_rule(`n__pre:int`, spec_rule(`Tint`,
            spec_rule(`n__addr:int`, get_data_at_range()))));
    cst_set_symbolic_state(local_apply(cst_get_symbolic_state(), rng));
    // 一条 int_arith_rule 一次性生成这一步需要的全部纯事实
    thm facts = undisch_all_rule(int_arith_rule(
        `~(n__pre == 0i) ==> 0i <= n__pre ==> n__pre <= 2147483647i
         ==> n__pre >= 1i && 0i <= n__pre - 1i
             && n__pre - 1i <= 2147483647i && -- 2147483648i <= n__pre - 1i`));
    cst_set_symbolic_state(local_apply(cst_get_symbolic_state(),
        intro_fact_slrule(facts, refl_slrule(`emp`))));
    thm d_all = apply_conversion(
        once_rewrite_conv(THM_LIST(undef_char_array_def)),
        `undef_char_array (arr__pre:int) (n__pre:int)`);
    thm split = undisch_rule(spec_rule(`n__pre:int`, spec_rule(`Tchar`,
        spec_rule(`arr__pre:int`,
            get_theorem_by_name("undef_array_at_split_last")))));
    thm d_sub = apply_conversion(
        once_rewrite_conv(THM_LIST(undef_char_array_def)),
        `undef_char_array (arr__pre:int) (n__pre - 1i)`);
    cst_set_symbolic_state(local_apply(cst_get_symbolic_state(),
        list_trans_slrule(THM_LIST(
            eq2ent(d_all),
            split,
            frame_right_slrule(eq2ent(sym_rule(d_sub)),
                `undef_data_at (arr__pre + (n__pre - 1i) * sizeof Tchar) Tchar`)))));
  }
  clear(arr, n - 1);
  char *p = arr + (n - 1);
  *p = 0;
  // 把最后一字节合回去：zeroed arr (n-1) ** data_at (arr+(n-1)*sizeof Tchar) Tchar 0i
  //                       |-- zeroed arr n
  [[cst::proof]] {
    thm d_sub = apply_conversion(once_rewrite_conv(THM_LIST(zeroed_def)),
        `zeroed (arr__pre:int) (n__pre - 1i)`);
    // IREPLICATE_APPEND 带有前提 `0i <= n`，用作用域内的事实卸除它
    thm app = mp_rule(
        ispec_rule(`0i`, spec_rule(`n__pre - 1i`,
            get_theorem_by_name("IREPLICATE_APPEND"))),
        assume_rule(`0i <= n__pre - 1i`));
    thm folded = rewrite_rule(THM_LIST(
        app,
        int_arith_rule(`(n__pre - 1i) + 1i == n__pre`)),
        spec_rule(`ireplicate (n__pre - 1i) 0i`, spec_rule(`0i`,
            spec_rule(`n__pre - 1i`, spec_rule(`Tchar`, spec_rule(`arr__pre:int`,
                get_theorem_by_name("array_at_merge_last")))))));
    thm d_all = apply_conversion(once_rewrite_conv(THM_LIST(zeroed_def)),
        `zeroed (arr__pre:int) (n__pre:int)`);
    cst_set_symbolic_state(local_apply(cst_get_symbolic_state(),
        list_trans_slrule(THM_LIST(
            frame_right_slrule(eq2ent(d_sub),
                `data_at (arr__pre + (n__pre - 1i) * sizeof Tchar) Tchar 0i`),
            folded,
            eq2ent(sym_rule(d_all))))));
  }
}


#include "proof/proof.h"
// 契约不能直接接受带 ctype 的谓词，故把 char 数组的两个谓词各包一层单态版本。
[[cst::proof]] thm undef_char_array_def = new_fun_definition(
    `undef_char_array (x:addr) (n:int) : hprop = undef_array_at x Tchar n`);
[[cst::proof]] int _e1 = cst_add_const_to_header(`undef_char_array`);
[[cst::proof]] thm zeroed_def = new_fun_definition(
    `zeroed (x:addr) (n:int) : hprop = array_at x Tchar n (ireplicate n 0i)`);
[[cst::proof]] int _e2 = cst_add_const_to_header(`zeroed`);
void clear(char *arr, int n)
    [[cst::require(`fact(0i <= n) ** undef_char_array arr n`)]]
    [[cst::ensure(`zeroed arr n`)]]
{
  if (n == 0) {
    // 基本情况：undef_char_array arr 0 -|- emp -|- zeroed arr 0。
    [[cst::proof]] {
      thm repl_nil = apply_conversion(
          pure_rewrite_conv(THM_LIST(
              assume_rule(`n__pre == 0i`),
              get_theorem_by_name("IREPLICATE_DEF"),
              get_theorem_by_name("NUM_OF_INT_OF_NUM"),
              get_theorem_by_name("REPLICATE"))),
          `ireplicate n__pre 0i`);
      thm e_uz = undisch_rule(spec_rule(`n__pre:int`, spec_rule(`Tchar`,
          spec_rule(`arr__pre:int`,
              get_theorem_by_name("undef_array_at_zero")))));
      thm e_az = mp_rule(mp_rule(
          spec_rule(`ireplicate n__pre 0i`, spec_rule(`n__pre:int`,
              spec_rule(`Tchar`, spec_rule(`arr__pre:int`,
                  get_theorem_by_name("array_at_zero"))))),
          assume_rule(`n__pre == 0i`)), repl_nil);
      thm d_all = apply_conversion(
          once_rewrite_conv(THM_LIST(undef_char_array_def)),
          `undef_char_array (arr__pre:int) (n__pre:int)`);
      thm d_z = apply_conversion(once_rewrite_conv(THM_LIST(zeroed_def)),
          `zeroed (arr__pre:int) (n__pre:int)`);
      cst_set_symbolic_state(local_apply(cst_get_symbolic_state(),
          eq2ent(list_trans_rule(THM_LIST(
              d_all, e_uz, sym_rule(e_az), sym_rule(d_z))))));
    }
    return;
  };
  // n >= 1，从末尾切下最后一字节：
  //   undef_char_array arr n |--
  //     undef_char_array arr (n-1) ** undef_data_at (arr + (n-1)*sizeof Tchar) Tchar
  [[cst::proof]] {
    // 从 n 的 data_at 单元取出取值范围，供 n - 1 的下标与减法安全性检查。
    thm rng = rewrite_rule(THM_LIST(get_theorem_by_name("min_of_def"),
                                    get_theorem_by_name("max_of_def")),
        spec_rule(`n__pre:int`, spec_rule(`Tint`,
            spec_rule(`n__addr:int`, get_data_at_range()))));
    cst_set_symbolic_state(local_apply(cst_get_symbolic_state(), rng));
    // 一条 int_arith_rule 一次性生成这一步需要的全部纯事实
    thm facts = undisch_all_rule(int_arith_rule(
        `~(n__pre == 0i) ==> 0i <= n__pre ==> n__pre <= 2147483647i
         ==> n__pre >= 1i && 0i <= n__pre - 1i
             && n__pre - 1i <= 2147483647i && -- 2147483648i <= n__pre - 1i`));
    cst_set_symbolic_state(local_apply(cst_get_symbolic_state(),
        intro_fact_slrule(facts, refl_slrule(`emp`))));
    thm d_all = apply_conversion(
        once_rewrite_conv(THM_LIST(undef_char_array_def)),
        `undef_char_array (arr__pre:int) (n__pre:int)`);
    thm split = undisch_rule(spec_rule(`n__pre:int`, spec_rule(`Tchar`,
        spec_rule(`arr__pre:int`,
            get_theorem_by_name("undef_array_at_split_last")))));
    thm d_sub = apply_conversion(
        once_rewrite_conv(THM_LIST(undef_char_array_def)),
        `undef_char_array (arr__pre:int) (n__pre - 1i)`);
    cst_set_symbolic_state(local_apply(cst_get_symbolic_state(),
        list_trans_slrule(THM_LIST(
            eq2ent(d_all),
            split,
            frame_right_slrule(eq2ent(sym_rule(d_sub)),
                `undef_data_at (arr__pre + (n__pre - 1i) * sizeof Tchar) Tchar`)))));
  }
  clear(arr, n - 1);
  char *p = arr + (n - 1);
  *p = 0;
  // 把最后一字节合回去：zeroed arr (n-1) ** data_at (arr+(n-1)*sizeof Tchar) Tchar 0i
  //                       |-- zeroed arr n
  [[cst::proof]] {
    thm d_sub = apply_conversion(once_rewrite_conv(THM_LIST(zeroed_def)),
        `zeroed (arr__pre:int) (n__pre - 1i)`);
    // IREPLICATE_APPEND 带有前提 `0i <= n`，用作用域内的事实卸除它
    thm app = mp_rule(
        ispec_rule(`0i`, spec_rule(`n__pre - 1i`,
            get_theorem_by_name("IREPLICATE_APPEND"))),
        assume_rule(`0i <= n__pre - 1i`));
    thm folded = rewrite_rule(THM_LIST(
        app,
        int_arith_rule(`(n__pre - 1i) + 1i == n__pre`)),
        spec_rule(`ireplicate (n__pre - 1i) 0i`, spec_rule(`0i`,
            spec_rule(`n__pre - 1i`, spec_rule(`Tchar`, spec_rule(`arr__pre:int`,
                get_theorem_by_name("array_at_merge_last")))))));
    thm d_all = apply_conversion(once_rewrite_conv(THM_LIST(zeroed_def)),
        `zeroed (arr__pre:int) (n__pre:int)`);
    cst_set_symbolic_state(local_apply(cst_get_symbolic_state(),
        list_trans_slrule(THM_LIST(
            frame_right_slrule(eq2ent(d_sub),
                `data_at (arr__pre + (n__pre - 1i) * sizeof Tchar) Tchar 0i`),
            folded,
            eq2ent(sym_rule(d_all))))));
  }
}

三块证明各推进一步符号状态，思路相同：先将若干小步蕴含首尾连接，得到从当前堆到目标堆的蕴含，再通过 local_applylocal_apply 应用于状态。其中，蕴含的组合用 list_trans_slrulelist_trans_slrule 完成；基本情况先用 list_trans_rulelist_trans_rule 组合等式，再转换为蕴含。

基本情况 n == 0n == 0：空数组既等价于 empemp 也等价于 zeroed arr 0zeroed arr 0；证明把 undef_char_array arr 0undef_char_array arr 0 经 undef_array_at_zeroundef_array_at_zero、array_at_zeroarray_at_zero 等库引理逐步等价改写为 zeroed arr 0zeroed arr 0。这些 -|--|- 等价关系通过 list_trans_rulelist_trans_rule 连接为一条，再由 eq2enteq2ent 转换为蕴含，应用于状态。
递归前：从数组末尾切出一个单元。undef_array_at_split_lastundef_array_at_split_last 经 spec_rulespec_rule/undisch_ruleundisch_rule 实例化，frame_right_slruleframe_right_slrule 用框架规则保留切出的最后一个单元，list_trans_slrulelist_trans_slrule 将 undef_char_array arr nundef_char_array arr n 分解为 undef_char_array arr (n-1) ** undef_data_at …undef_char_array arr (n-1) ** undef_data_at …；下标与减法的安全性还需要 n >= 1n >= 1、n-1n-1 落在 intint 界内等纯事实。一次 int_arith_ruleint_arith_rule 调用即可生成这些事实，再经 intro_fact_slruleintro_fact_slrule 注入状态。
递归后 *p = 0*p = 0：将最后一个单元重新合并到数组中。结合 array_at_merge_lastarray_at_merge_last 与 ireplicateireplicate 的追加引理（其前提 0i <= n0i <= n 用作用域内已有的事实卸除），用 frame_right_slruleframe_right_slrule/list_trans_slrulelist_trans_slrule 将 zeroed arr (n-1) ** data_at … 0izeroed arr (n-1) ** data_at … 0i 合并为 zeroed arr nzeroed arr n，正好是出口断言。

最后这一步可以在 Show Symbolic StateShow Symbolic State 里看得很清楚。在 *p = 0;*p = 0; 一行查看，符号状态里除了若干 factfact 与局部变量的单元之外，正好有这两块堆：

符号状态 @ *p = 0;*p = 0; 后


… **
zeroed arr__pre (n__pre - 1i) **
data_at (arr__pre + (n__pre - 1i) * sizeof Tchar) Tchar 0i


… **
zeroed arr__pre (n__pre - 1i) **
data_at (arr__pre + (n__pre - 1i) * sizeof Tchar) Tchar 0i

它们分别是已清零的前 n-1n-1 个字节 zeroed arr (n-1)zeroed arr (n-1)，以及刚刚写入 00 的最后一个单元。末尾的证明块将这两部分合并为 zeroed arr nzeroed arr n。

自始至终没有为任何验证条件建立目标：每一步都以当前状态为前件、向右推出下一状态。这是一段完全前向的完整证明。

小结

C* 通过客户端/服务器模型连接 C 与 HOL Light：[[cst::proof]][[cst::proof]] 里的 C 代码是客户端、只持有不透明句柄，真正的逻辑对象与可信内核在隔离的服务器进程里，进程隔离使 TCB 与完全可扩展性得以保持；
前向证明就是调用 *_rule*_rule/*_slrule*_slrule/*_conv*_conv，从已知定理自底向上构造出新定理；
通用前向证明用 refl_rulerefl_rule/sym_rulesym_rule/arith_rulearith_rule/spec_rulespec_rule/conj_ruleconj_rule/mp_rulemp_rule 与变换，典型用法是通过归纳，自底向上证明一条定理；
分离逻辑前向证明用 *_slrule*_slrule 构造以 |--|-- 为结论的定理，intro_fact_slruleintro_fact_slrule 注入纯事实、local_applylocal_apply 借框架规则推进符号状态；
经 eq2enteq2ent/local_applylocal_apply 把前向证得的定理写回符号状态，即可卸除符号执行引擎留下的验证条件；
开发时可在 VSCode 里用 Show Symbolic StateShow Symbolic State 查看状态并逐步推进证明；mc91mc91 与 clearclear 分别是通用与分离逻辑两类完整、可验证的例子。