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（appapp 右单位元），完全自底向上、不设任何目标：


[[cst::proof]] {
  // 基本情况： |- 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
}


[[cst::proof]] {
  // 基本情况： |- 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
}

逐行来看，每一步都由已有定理产出新定理：base_eqbase_eq、step_eqstep_eq 由 app_defapp_def 改写而来；ind_thmind_thm 由数据类型自带的归纳定理 nlist.indnlist.ind 经 spec_rulespec_rule（实例化）与 beta_rulebeta_rule（-归约）特化到谓词 \l. app l nil = l\l. app l nil = l；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)（doubl(x) = x + xdoubl(x) = x + x 是一个用 new_fun_definitionnew_fun_definition 定义并导出的逻辑函数）。


#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，确认状态如预期推进，并在文件末尾确认验证条件是否已被消解；
重复，直到所有验证条件都被消解。

写完 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 pt l.
//     ~(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 pt l.
//     ~(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(`l2:(int)list`, spec_rule(`vv:addr`, sll_unfold)));
  cst_set_symbolic_state(local_apply(cst_get_symbolic_state(), ent));
}


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

spec_rulespec_rule 把引理里的 ptpt、ll 实例化为当前的指针 vvvv 与列表 l2l2；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)`);
    thm folded = rewrite_rule(THM_LIST(
        get_theorem_by_name("IREPLICATE_APPEND"),
        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)`);
    thm folded = rewrite_rule(THM_LIST(
        get_theorem_by_name("IREPLICATE_APPEND"),
        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))))));
  }
}

三块证明各推进一步符号状态，形状都一样：用 list_trans_slrulelist_trans_slrule 把若干小步蕴含首尾相接，组合成一条从“当前这块堆”到“目标那块堆”的蕴含，再 local_applylocal_apply 并入状态。

基本情况 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 的追加引理，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 分别是通用与分离逻辑两类完整、可验证的例子。