C* 中的分离逻辑

上一节用形式化记号介绍了分离逻辑：程序状态是 store 加 heap，空间断言（、、）让规约精确、局部地刻画内存性质。 本节将这些数学记号映射到 C* 的具体语法：如何在 C* 中书写空间断言、C* 当前用哪些假设和约定把断言与 C 的内存语义连接起来，以及如何用 C* 提供的定义机制为链表、树这样的数据结构定义表示谓词（Representation Predicates）。 本节仅介绍“怎么写断言与谓词”，不涉及任何证明。

在 第一个 C* 程序 中我们已经见过：C* 的规约写在 `...``...` 反引号包裹的逻辑表达式里，其语法源自 C* 集成的定理证明器 HOL Light。 上一节的每个数学记号，在这套语法中都有对应的写法：

几处与数学记号的差异值得先指出：

• 分离合取写作 **** 而非 **——在 HOL Light 的语法里 ** 已被乘法占用；
• 指向谓词 data_atdata_at 比 多一个 C 类型参数，这是断言与 C 语义连接的关键，本节稍后展开；
• 整数常量带 ii 后缀（如 42i42i、0i0i），取相反数是 ----，逻辑非是 ~~，相等惯用 ====——这些在 第一个 C* 程序 的验证条件中都已出现过。

要练习书写断言，最好有一个能让 C* 立即帮我们做解析和类型检查的地方。 契约（[[cst::require]][[cst::require]] 等）当然是断言最终的归宿，但本节暂不引入契约的种种规则。 好在 C* 提供了一个更轻量的载体：全局证明声明。

[[cst::proof]][[cst::proof]] 标注表示其后的内容只服务于验证：它可以标注函数体内的一个语句块 [[cst::proof]] { ... }[[cst::proof]] { ... }（证明块，用于书写证明代码，后续章节的主角），也可以标注一个文件作用域的声明，得到一个验证时声明（Verification-Time Declaration）——它只存在于验证时，完全不进入编译产物。 验证时声明可以使用一组验证专用的 C 类型，本节用到三个：

• termterm：一个 HOL 逻辑项；
• thmthm：一条 HOL 定理；
• indtypeindtype：一个归纳数据类型（稍后在定义机制的介绍中引出）。

于是，下面这段合法的 C* 代码就是我们的“断言草稿纸”：

#include "proof/proof.h"
// 注册 term 类型的打印函数，用于在 VSCode 中查看符号状态时打印出 tm 的内容
[[cst::proof]] static inline char *cst_string_of_term(const term tm) {
  if (IS_NULL(tm)) return "<null>";
  return cstr_term(tm);
}
[[cst::proof]] term ex1 = `data_at p Tint 42i`;

#include "proof/proof.h"
// 注册 term 类型的打印函数，用于在 VSCode 中查看符号状态时打印出 tm 的内容
[[cst::proof]] static inline char *cst_string_of_term(const term tm) {
  if (IS_NULL(tm)) return "<null>";
  return cstr_term(tm);
}
[[cst::proof]] term ex1 = `data_at p Tint 42i`;

它声明了一个名为 ex1ex1 的逻辑项，内容是反引号中的断言：逻辑变量 pp 表示的地址处存储着 intint 类型的值 4242。 如果在 VSCode 中在这一行查看符号状态，HOL Light 服务器就会解析这个断言并做类型检查；若书写有误（比如漏掉 ii 后缀导致类型不一致）会立即得到诊断信息。 断言中的 pp 无须事先声明：逻辑表达式中未定义的标识符自动成为逻辑变量，其类型由类型推断确定。

反引号里的部分由 HOL Light 进行词法和语法解析。我们先花一些时间认识这个定理证明器的约定——项、类型与公式，后面读写断言、定义谓词时会更加顺利。 HOL Light 实现的是高阶逻辑（Higher-Order Logic），可以粗略理解为“带类型的 λ 演算加上经典逻辑”，语法核心非常小。

一切都是项。反引号中的表达式统称项（Term），而项只有四种构成方式：变量（未定义的标识符自动成为变量，如前文的 pp）、常量（由逻辑库或用户定义引入，如 empemp、data_atdata_at）、应用与 λ 抽象。 应用写作 f xf x；多参数函数是柯里化（Currying）的，data_at x Tint vdata_at x Tint v 其实是 ((data_at x) Tint) v((data_at x) Tint) v——参数之间只有空格，没有括号与逗号。 λ 抽象即匿名函数，写作 \. \. 。在草稿纸上试试：

[[cst::proof]] term tm1 = `\x. x + 1i`;          // λ 抽象：整数上的“加一”函数
[[cst::proof]] term tm2 = `(\x. x + 1i) 41i`;    // 应用：这个项可证等于 42i
[[cst::proof]] term tm3 = `[1i; 2i; 3i]`;        // 列表字面量，元素用分号分隔

[[cst::proof]] term tm1 = `\x. x + 1i`;          // λ 抽象：整数上的“加一”函数
[[cst::proof]] term tm2 = `(\x. x + 1i) 41i`;    // 应用：这个项可证等于 42i
[[cst::proof]] term tm3 = `[1i; 2i; 3i]`;        // 列表字面量，元素用分号分隔

每个项都有类型。常见的类型有 boolbool（命题）、numnum（自然数）、intint（整数）；A -> BA -> B 是函数类型（->-> 右结合）；类型构造子采用后缀应用，如 (int)list(int)list 是“整数列表”类型——tm3tm3 的类型正是它。 类型标注写作 ::，可以加在任何子项上，如 (x:int)(x:int)。 通常无须处处标注：HOL Light 会做类型推断，只在上下文不足以定型时才需要手动标注。 另一个与类型有关的细节：不带后缀的字面量 4242 是自然数（numnum），带后缀的 42i42i 才是整数（intint）；C* 对 C 程序的建模一律使用 intint，所以本教程中的数字总是带有 ii 后缀。

公式就是 boolbool 类型的项。高阶逻辑没有独立的“公式”语法层：命题是类型为 boolbool 的项，谓词是结果类型为 boolbool 的函数。逻辑连接词与量词的写法如下（绑定子可一次绑定多个变量，如 !x y. P!x y. P）：

[[cst::proof]] term tm4 = `!x. ?y. y > (x:int)`;  // 一个（真的）命题：任何整数都有更大的

[[cst::proof]] term tm4 = `!x. ?y. y > (x:int)`;  // 一个（真的）命题：任何整数都有更大的

注意这些是 boolbool 层的记号。断言层（hprophprop）的合取、析取与量词是它们的对应物：C* 的惯例是 boolbool 层量词用符号 !!/??，断言层量词用单词 forallforall/existsexists，两不相扰；&&&&/|||| 的双重身份则见下一节。 完整的词法与语法（算子优先级表、绑定子清单等）可查阅参考手册。

定理由计算产生。termterm 与 thmthm 的分野是 HOL Light 的灵魂：任何人都能写下一个 boolbool 项，但一个 thmthm 值只能由内核中为数不多的几条推理规则组合而成（这一设计源自 LCF 传统，内核之外的一切功能最终都归结为内核规则的组合）。 定义新常量、新类型的机制同样经过内核把关，返回相应的定义定理——本节稍后定义表示谓词时得到的 thmthm，正是这样产生的。 关于定理和证明的更多内容将在后续章节中展开。

在 C* 的逻辑层，分离逻辑的空间断言自成一个类型，名为 hprophprop（heap proposition）。 本节开头对照表中的算子按类型可以分成两组：

• 构造断言的算子，结果类型是 hprophprop：****、&&&&、||||、-*-*、empemp、fact(...)fact(...)、existsexists、forallforall 等；
• 陈述断言之间关系的算子，结果类型是 boolbool：|--|--（蕴含）与 -|--|-（等价）。

后者是“元层”的判断：p |-- qp |-- q 本身不再是断言，而是一个关于两个断言的命题——第一个 C* 程序中展示的验证条件正是这种形状。 两组算子可以混合出现在同一个逻辑项里，例如把上一节“ 把恰好放松为至少”的例子写进草稿纸：

[[cst::proof]] term ex2 = `data_at x Tint 7i ** true`;
[[cst::proof]] term ex3 = `data_at x Tint 7i |-- data_at x Tint 7i ** true`;

[[cst::proof]] term ex2 = `data_at x Tint 7i ** true`;
[[cst::proof]] term ex3 = `data_at x Tint 7i |-- data_at x Tint 7i ** true`;

ex2ex2 是一个 hprophprop；ex3ex3 是一个 boolbool——一个（恰好成立的）蕴含判断。 注意 truetrue、falsefalse、existsexists、forallforall、&&&&、|||| 都在 boolbool 与 hprophprop 两个类型上重载：fact(x > 0i && y > 0i)fact(x > 0i && y > 0i) 里的 &&&& 是布尔合取（即上一节的 /\/\），fact(x > 0i) && empfact(x > 0i) && emp 里的 &&&& 则是断言合取，类型推断会自动辨别。

算子的结合优先级从松到紧依次为：|--|--、-|--|- 最松，其次是 -*-*，然后 ||||，优先级最高的是 &&&& 与 ****（同级，均右结合）；函数应用（如 data_at x Tint vdata_at x Tint v）比所有中缀算子都紧。 所以 fact(x > 0i) ** data_at x Tint v |-- truefact(x > 0i) ** data_at x Tint v |-- true 无须任何括号，就表示“左边整个分离合取蕴含 truetrue”。

上一节我们用满足关系 定义了断言的语义。在 C* 中，这套语义是逻辑内的定义，并非纸面约定：C* 把分离逻辑浅嵌入（Shallow Embedding）到 HOL Light 中，hprophprop 就定义为“内存的谓词”类型 mem -> boolmem -> bool，其中内存 memmem 是从地址到内存单元状态的函数，而单元状态有三种可能：

在这个模型上，每个算子都是一条普通的 HOL 定义，与上一节的语义定义逐条对应：

emp      =  (\m. is_unit m)                                  已分配集合为空
pure     =  (\p m. p)                                        与 m 无关
p ** q   =  (\m. ?m1 m2. join m1 m2 m /\ p m1 /\ q m2)       堆的不相交拆分
p |-- q  =  (!m. p m ==> q m)                                所有内存上逐点蕴含

emp      =  (\m. is_unit m)                                  已分配集合为空
pure     =  (\p m. p)                                        与 m 无关
p ** q   =  (\m. ?m1 m2. join m1 m2 m /\ p m1 /\ q m2)       堆的不相交拆分
p |-- q  =  (!m. p m ==> q m)                                所有内存上逐点蕴含

其中 join m1 m2 mjoin m1 m2 m 表示 mm 可拆成不相交的 m1m1 与 m2m2——正是上一节的 。 值得强调的是：分离逻辑的代数定律（**** 的结合律与交换律、empemp 是单位元、魔术棒与 **** 的伴随关系等）在 C* 的逻辑库中都是从这些定义出发被证明的定理，而不是新增的公理。 换句话说，你在 C* 中书写的断言不是某个黑盒求解器的输入语言，它的每一步推理都可以追溯到 HOL Light 内核认可的证明。

数学记号里 只说“地址 存储着值 ”；但在 C 中，“存储着”必须回答一个问题：以什么类型存储？ intint 与 charchar 占的字节数不同，有符号与无符号的取值范围不同。 这就是 data_atdata_at 的第二个参数：一个 ctypectype 类型的值，表示 C 类型在逻辑中的化身。 常用的 ctypectype 常量与其 sizeofsizeof：

TptrTptr 统一表示指针类型（可理解为 void *void *）。逻辑层还提供 sizeof()sizeof()、min_of()min_of()、max_of()max_of() 三个函数，分别给出类型的大小与取值范围；地址本身的类型 addraddr 是 intint 的类型缩写。

有了类型参数，data_at x Tint vdata_at x Tint v 承载的信息就比数学记号的 多：它在字节粒度的内存模型上展开为从 xx 起连续 4 个字节单元的分离合取，并且内建了合法性约束——地址按 4 对齐且落在有效范围内、值 vv 落在 intint 的取值范围内。

“内建合法性”意味着断言携带着可以按需取用的纯事实，例如 C* 标准库中提供的定理：

data_at x ty v |-- data_at x ty v ** fact(min_of ty <= v && v <= max_of ty)

data_at x ty v |-- data_at x ty v ** fact(min_of ty <= v && v <= max_of ty)

即从一块 data_atdata_at 资源中随时可以“抽取”其值的范围信息。 这是 C* 断言与 C 语义连接的第一组约定：指向谓词以字节与 C 类型为粒度建模，合法地址、对齐与取值范围是谓词定义的一部分，而非额外的假设。

与 data_atdata_at 相伴的还有两组谓词：

• undef_data_at undef_data_at ：地址 处已分配了一个 类型的位置，但内容未初始化（正是浅嵌入模型中 NoninitNoninit 状态的化身）。它与数学记号 有细微的区别： 是“存着某个不关心的值”，而未初始化的内存读取即报错。定理 data_at x ty v |-- undef_data_at x tydata_at x ty v |-- undef_data_at x ty 允许把已初始化的资源“遗忘”成未初始化，因为这不会破坏安全性。
• array_at array_at ：从地址 起连续 个 类型元素，内容依次为列表 中的值。它定义为 data_atdata_at 沿下标的迭代分离合取，第 个元素位于 + * sizeof() + * sizeof()——这与 C* 对数组下标表达式的处理一致：arr[i]arr[i] 在逻辑中就展开为这个形状的地址。此外还有未初始化版本 undef_array_atundef_array_at，以及用于把某个元素从数组中拆出、拆剩的“段”与“带洞”变体（array_at_recarray_at_rec、array_at_missing_i_recarray_at_missing_i_rec 等），后续用到时再介绍。

C 程序真正有趣的堆结构总是从 structstruct 开始的。C* 把结构体纳入断言的方式同样是一组命名约定。以链表结点为例：

struct list {
  int head;
  struct list *tail;
};

struct list {
  int head;
  struct list *tail;
};

在逻辑层，结构体名与字段名各自有专门的类型：struct_namestruct_name 与 fieldfield。 约定是：结构体名对应的逻辑常量以 TT 为前缀，字段名对应的逻辑常量以 FF 为前缀——struct liststruct list 对应 TlistTlist，字段 headhead、tailtail 对应 FheadFhead、FtailFtail。 C* 按名字建立这个对应，所以我们只需（用全局证明声明）把这些常量引入逻辑：

[[cst::proof]] int _l = (new_const("Tlist", `:struct_name`), 0);
[[cst::proof]] int _h = (new_const("Fhead", `:field`), 0);
[[cst::proof]] int _t = (new_const("Ftail", `:field`), 0);

[[cst::proof]] int _l = (new_const("Tlist", `:struct_name`), 0);
[[cst::proof]] int _h = (new_const("Fhead", `:field`), 0);
[[cst::proof]] int _t = (new_const("Ftail", `:field`), 0);

new_constnew_const 声明一个新的逻辑常量（只给名字和类型，没有定义）。 它的返回类型是 voidvoid，而文件作用域要求“带初始化的声明”，于是这里用了 C 的逗号表达式凑出一个 intint 初始化值——一个值得记住的惯用法。

字段的地址由函数 field_addrfield_addr 给出：field_addr field_addr 表示 所指结构体（名为 ）中字段 的地址。 于是“ptpt 指向一个 headhead 为 xx、tailtail 为 qq 的结点”写作：

[[cst::proof]] term ex4 =
  `data_at (field_addr pt Tlist Fhead) Tint x **
   data_at (field_addr pt Tlist Ftail) Tptr q`;

[[cst::proof]] term ex4 =
  `data_at (field_addr pt Tlist Fhead) Tint x **
   data_at (field_addr pt Tlist Ftail) Tptr q`;

访问 C 代码中的 pt->headpt->head 时，C* 就会在符号状态中寻找 field_addr pt Tlist Fheadfield_addr pt Tlist Fhead 处的 data_atdata_at 资源。嵌套结构体同样奏效：&it->node.next&it->node.next 这样的地址展开为 field_addr (field_addr it Titem Fnode) Tlink Fnextfield_addr (field_addr it Titem Fnode) Tlink Fnext。

断言最终要谈论 C 程序的变量。第一个 C* 程序 中已经出现过这组约定，这里完整地汇总一遍：

• 参数或局部变量 本身占据一块内存，其地址在逻辑中是变量 __addr__addr（类型为 addraddr）；全局变量同理；
• 参数 在函数入口处的初值记作 __pre__pre；
• 后置条件中，函数返回值记作 __return__return。

所以一个 intint 参数 xx 在函数入口的符号状态中贡献的资源是 data_at x__addr Tint x__predata_at x__addr Tint x__pre；一个未初始化的局部变量 int rint r 贡献 undef_data_at r__addr Tintundef_data_at r__addr Tint——这正是上一节看到的：

undef_data_at r__addr Tint **
data_at x__addr Tint x__pre

undef_data_at r__addr Tint **
data_at x__addr Tint x__pre

指针参数没有任何特殊之处：struct list *ptstruct list *pt 的初值 pt__prept__pre 是一个地址，它指向的内存不会自动出现在符号状态里——要谈论 *pt*pt，断言必须显式刻画那块资源（用 data_atdata_at，或下一节定义的表示谓词）。 这是分离逻辑“资源须显式刻画”原则与 C 语义约定的自然衔接。

还有一处细节：intint 参数的取值范围不会作为独立的纯事实自动出现在符号状态中——它内建在 data_at x__addr Tint x__predata_at x__addr Tint x__pre 这块资源里，需要时可用上文的范围定理抽取。

这些带 __addr__addr、__pre__pre、__return__return 的逻辑变量，正是函数契约（[[cst::require]][[cst::require]]、[[cst::ensure]][[cst::ensure]]）与循环不变式（[[cst::invariant]][[cst::invariant]]）中书写断言时使用的词汇；契约与不变式的写法将在下一节再详细展开。

上一节中，“ 指向一棵合法二叉树”是用空间断言归纳定义的谓词：

要在 C* 中验证操纵链表、树的程序，就需要把这样的谓词定义到逻辑里。 这类谓词称为表示谓词：它们把一块具体的内存与一个纯数学值（HOL 中的列表、树等）关联起来——“地址 ptpt 处的那串结点表示列表 ll”。 C* 为此提供了一组定义机制，均以验证接口函数的形式出现、在全局证明声明中调用、返回定义对应的 thmthm。

new_fun_definitionnew_fun_definition 接受一个形如“左边是带参数的新常量、右边是定义体”的等式，定义一个（可以是递归的）函数或谓词，返回其定义定理。 最简单的例子是一个纯函数：

// 注册 thm 类型的打印函数，用于在 VSCode 中查看符号状态时打印出 th 的内容
[[cst::proof]] static inline char *cst_string_of_thm(const thm th) {
  if (IS_NULL(th)) return "<null>";
  return cstr_thm(th);
}
[[cst::proof]] thm doubl_def = new_fun_definition(`doubl(x:int) = x + x`);

// 注册 thm 类型的打印函数，用于在 VSCode 中查看符号状态时打印出 th 的内容
[[cst::proof]] static inline char *cst_string_of_thm(const thm th) {
  if (IS_NULL(th)) return "<null>";
  return cstr_thm(th);
}
[[cst::proof]] thm doubl_def = new_fun_definition(`doubl(x:int) = x + x`);

定义体当然也可以是断言。比如把上文 ex4ex4 的“一个链表结点”抽象成谓词：

[[cst::proof]] thm node_at_def = new_fun_definition(
  `node_at (pt:addr) (h:int) (t:addr) : hprop =
     (data_at (field_addr pt Tlist Fhead) Tint h **
      data_at (field_addr pt Tlist Ftail) Tptr t)`);

[[cst::proof]] thm node_at_def = new_fun_definition(
  `node_at (pt:addr) (h:int) (t:addr) : hprop =
     (data_at (field_addr pt Tlist Fhead) Tint h **
      data_at (field_addr pt Tlist Ftail) Tptr t)`);

此后 node_at pt x qnode_at pt x q 就是一个合法的断言。注意两个语法细节：

• 参数与结果都写了类型标注（(pt:addr)(pt:addr)、: hprop: hprop）——新常量没有任何已知信息，类型推断无从判断，定义时写全类型是良好的实践；
• 定义体整个包了一层括号。这不是可有可无的：**** 比 == 结合得更松，不加括号时 p x : hprop = A ** Bp x : hprop = A ** B 会被解析成 (p x = A) ** B(p x = A) ** B 而导致令人费解的类型错误。

表示谓词的本体通常是递归的：链表谓词沿列表递归，树谓词沿树递归。 对于 new_fun_definitionnew_fun_definition 无法完成定义的递归函数或谓词，可以使用 new_rec_definitionnew_rec_definition，它接受两个参数：所递归的数据类型的递归定理，以及用 &&&& 连接的各构造子对应的定义子句。 下面是分离逻辑中最经典的表示谓词——单链表 sllsll（singly-linked list）的完整定义：

[[cst::proof]] thm sll_def = new_rec_definition(
    get_theorem_by_name("list_RECURSION"),
    `(sll (pt:addr) ([]:(int)list) = fact(pt == 0i)) &&
     (sll (pt:addr) (CONS (x:int) (xs:(int)list)) =
        exists q. fact(~(pt == 0i)) **
                  data_at (field_addr pt Tlist Fhead) Tint x **
                  data_at (field_addr pt Tlist Ftail) Tptr q **
                  sll q xs)`);

[[cst::proof]] thm sll_def = new_rec_definition(
    get_theorem_by_name("list_RECURSION"),
    `(sll (pt:addr) ([]:(int)list) = fact(pt == 0i)) &&
     (sll (pt:addr) (CONS (x:int) (xs:(int)list)) =
        exists q. fact(~(pt == 0i)) **
                  data_at (field_addr pt Tlist Fhead) Tint x **
                  data_at (field_addr pt Tlist Ftail) Tptr q **
                  sll q xs)`);

sll pt lsll pt l 的含义是：“从地址 ptpt 出发的一串结点表示列表 ll”。两条子句沿列表的两个构造子展开：

• 空列表 [][]：ptpt 是空指针，且不占任何内存（factfact 刻画空堆）；
• 非空列表 CONS x xsCONS x xs（即 x :: xsx :: xs）：ptpt 非空，指向一个 headhead 存储着 xx 的结点，其 tailtail 存储着某个地址 qq，从 qq 出发的结点串表示余下的 xsxs。

与上一节的 对比，可以看清楚两点变化。 其一，析取转化为模式匹配：数学定义用 区分两种情形，这里则按列表构造子 [][]、CONSCONS 分条书写——这是 HOL 递归定义的标准形态，第一个参数 get_theorem_by_name("list_RECURSION")get_theorem_by_name("list_RECURSION")（按名字从定理库中取出列表类型的递归定理）保证了这样的分条定义是良定义的。 其二，谓词增加了内容参数： 只说“形状合法”，而 sll pt lsll pt l 同时钉住了链表存着什么——功能正确性（例如“反转函数确实反转了列表”）由此才获得了陈述的词汇。

链表的内容用 HOL 现成的列表类型就够了；但树形结构需要先在逻辑里定义相应的归纳数据类型。 new_datatype_definitionnew_datatype_definition 接受一个类型描述字符串，返回一个 indtypeindtype 值：

// 注册 indtype 类型的打印函数，用于在 VSCode 中查看符号状态时打印出 idt 的内容
[[cst::proof]] static inline char *cst_string_of_indtype(const indtype idt) {
  return cstr_indtype(idt);
}
[[cst::proof]] indtype ty = new_datatype_definition("tree = Leaf | Node tree int tree");

// 注册 indtype 类型的打印函数，用于在 VSCode 中查看符号状态时打印出 idt 的内容
[[cst::proof]] static inline char *cst_string_of_indtype(const indtype idt) {
  return cstr_indtype(idt);
}
[[cst::proof]] indtype ty = new_datatype_definition("tree = Leaf | Node tree int tree");

这行定义了归纳类型 treetree：要么是空树 LeafLeaf，要么是结点 Node l v rNode l v r（左子树、值、右子树）。 返回值 tyty 携带两条定理：ty.recty.rec 是递归定理——正好作为 new_rec_definitionnew_rec_definition 的第一个参数；ty.indty.ind 是归纳定理，将来做归纳证明时使用。 配合相应的 C 结构体，二叉树的表示谓词水到渠成：

struct tree {
  int val;
  struct tree *l;
  struct tree *r;
};
[[cst::proof]] int _s  = (new_const("Ttree", get_struct_name_type()), 0);
[[cst::proof]] int _fv = (new_const("Fval", get_field_type()), 0);
[[cst::proof]] int _fl = (new_const("Fl", get_field_type()), 0);
[[cst::proof]] int _fr = (new_const("Fr", get_field_type()), 0);
[[cst::proof]] thm store_tree_def = new_rec_definition(ty.rec,
    `(store_tree (pt:addr) Leaf = fact(pt == 0i)) &&
     (store_tree (pt:addr) (Node (lt:tree) (v:int) (rt:tree)) =
        exists pl pr. fact(~(pt == 0i)) **
                      data_at (field_addr pt Ttree Fval) Tint v **
                      data_at (field_addr pt Ttree Fl) Tptr pl **
                      data_at (field_addr pt Ttree Fr) Tptr pr **
                      store_tree pl lt ** store_tree pr rt)`);

struct tree {
  int val;
  struct tree *l;
  struct tree *r;
};
[[cst::proof]] int _s  = (new_const("Ttree", get_struct_name_type()), 0);
[[cst::proof]] int _fv = (new_const("Fval", get_field_type()), 0);
[[cst::proof]] int _fl = (new_const("Fl", get_field_type()), 0);
[[cst::proof]] int _fr = (new_const("Fr", get_field_type()), 0);
[[cst::proof]] thm store_tree_def = new_rec_definition(ty.rec,
    `(store_tree (pt:addr) Leaf = fact(pt == 0i)) &&
     (store_tree (pt:addr) (Node (lt:tree) (v:int) (rt:tree)) =
        exists pl pr. fact(~(pt == 0i)) **
                      data_at (field_addr pt Ttree Fval) Tint v **
                      data_at (field_addr pt Ttree Fl) Tptr pl **
                      data_at (field_addr pt Ttree Fr) Tptr pr **
                      store_tree pl lt ** store_tree pr rt)`);

上一节 free_treefree_tree 的规约 ，在 C* 中就将写成以 store_treestore_tree 为词汇的契约。

除了以上机制，验证接口还提供更底层的 new_basic_definitionnew_basic_definition（无参数常量定义）等；完整清单见参考手册。

• C* 的断言写在反引号逻辑项中，类型为 hprophprop；数学记号逐一对应： 即 ****， 即 data_atdata_at（多出 C 类型参数）， 即 |--|--；
• 反引号内是 HOL Light 的高阶逻辑：一切皆项、应用柯里化、公式即 boolbool 项、thmthm 只能出自内核的推理规则；
• 全局证明声明 [[cst::proof]] term/thm 名字 = ...;[[cst::proof]] term/thm 名字 = ...; 是验证时声明，可当作书写断言与定义的草稿纸；
• fact()fact() 刻画空堆，pure()pure() 对堆无约束；符号状态与契约惯用 factfact 搭配 ****；
• 断言浅嵌入 HOL：hprop = mem -> boolhprop = mem -> bool，代数定律皆为定理而非公理；
• 与 C 语义的连接是一组约定：data_atdata_at 内建对齐与取值范围、数组元素地址形如 + * sizeof() + * sizeof()、结构体经 TT/FF 前缀常量与 field_addrfield_addr 进入逻辑、程序变量经 __addr__addr/__pre__pre/__return__return 进入断言；
• 表示谓词把内存块与纯数学值关联：new_fun_definitionnew_fun_definition 定义非递归谓词，new_rec_definitionnew_rec_definition 沿数据类型递归定义（如 sllsll、store_treestore_tree），new_datatype_definitionnew_datatype_definition 定义新的归纳类型。