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 后缀导致类型不一致），服务器会立即给出诊断信息，并提示错误的原因：不带后缀的 4242 是自然数（numnum），整数字面量要写成 42i42i。断言中的 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 *）。复合 C 类型（结构体、枚举、联合、typedef、数组、函数类型）也有各自的 ctypectype 构造子，但断言里很少直接写出它们：结构体的内存是通过下文介绍的 field_addrfield_addr 逐字段访问的，TfunTfun 只出现在函数指针契约的 fnspecfnspec 里。逻辑层还提供 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 从而产生关于 == 的类型错误；诊断信息会提示其中一侧很可能是 hprophprop，这就是排查的线索。

表示谓词通常采用递归定义：链表谓词沿列表递归，树谓词沿树递归。对于 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 是归纳定理，将来做归纳证明时使用。文件作用域中的声明顺序也有要求：[[cst::proof]][[cst::proof]] 全局声明必须先定义再使用。如果某条定义在 tyty 的定义之前就使用了 ty.recty.rec，编译器会拒绝该定义，并给出同时指向这两行的提示。有了这个类型，再配合相应的 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 定义新的归纳类型。