分离逻辑

C* 的断言就是分离逻辑断言。在 C* 中，分离逻辑通过浅嵌入（shallow embedding）在 HOL Light 内部实现，并非一套由黑盒求解器支持的固定记号。这一实现分为三层，本部分按证明内核中的实际实现逐层说明。

最底层是具体内存模型。内存是从地址到内存单元的全函数 mem = addr -> mem_varmem = addr -> mem_var，每个单元处于三种状态之一：无权限、已分配但未初始化、已初始化并存有一个字节。地址与字节都是整数，因此该模型以字节为粒度，地址运算就是整数运算。内存拆分用三元关系 mem_join m1 m2 mmem_join m1 m2 m 表示，不使用偏运算。

中间层是断言语言。一条断言就是一个关于内存的谓词：hprophprop 是 :mem->bool:mem->bool 的缩写。每个连接词——****、-*-*、&&&&、||||、-->-->、existsexists、forallforall、empemp、purepure、factfact、truetrue、falsefalse——都由一条 HOL 定义给出，定义体是基于该内存模型的 lambda 子句。蕴含 |--|-- 展开后，就是在所有内存上逐点成立的蕴涵。这一层的内容都不以公理的形式引入，因此无论写出怎样的断言，都不会扩大可信基础。

最上层是规则集，包括 **** 的结合性与交换性、empemp 作为单位元、魔术棒的伴随关系、框架规则、纯事实规则与量词规则。每条规则都从内存模型与各连接词的定义中证明得到，这一层的内容也不以公理的形式引入。在裸字节之上定义的带类型内存谓词同样经过证明；介绍这些谓词的页面还说明了理论对复合 C 类型有哪些尚未规定的内容。

• 内存模型与断言——地址、字节与三状态单元；内存及其合并关系；hprophprop 与各连接词的定义；蕴含与等价；purepure 与 factfact 的区别；迭代分离合取；记号汇总。

• 证明规则——列出各条规则，每条都是已证明的定理：蕴含、**** 的代数性质、框架消除、各条伴随关系、命题规则与量词规则，以及如何在 C* 证明中获取一条规则对应的 thmthm。

• 带类型的内存谓词——如何在字节单元之上定义 data_atdata_at、undef_data_atundef_data_at、array_atarray_at 及其同族谓词，这些谓词内建的有效性与范围约束，以及拆分、合并与换基的规则。