内存模型与断言

本页介绍 C* 分离逻辑中最基础的两个层次：内存模型，以及在其上定义的断言语言。下文均按证明内核引入时的形式引用 HOL Light 定义，其中的项可以原样粘贴到反引号包裹的逻辑表达式中，也可以作为定义接口的参数。

阅读这些定义时，需要区分这两个层次：内存模型确定什么是状态，断言语言则只借助状态上的两个操作来定义，即合并关系与单位元谓词。所有连接词的定义都不直接涉及字节或权限。

地址与字节都是整数：

addr = :int
byte = :int

addr = :int
byte = :int

addraddr 与 bytebyte 是类型缩写，并非新类型：它们在解析时就会展开，因此类型为 addraddr 的项就是类型为 :int:int 的项，可以用在任何需要整数的位置。由此可以得到三点结论。

• 地址运算就是普通的整数运算。没有回绕，没有“来源（provenance）”的概念，类型层面也不区分合法地址与非法地址。field_addr p Tlist Ftailfield_addr p Tlist Ftail 与 x + i * sizeof(ty)x + i * sizeof(ty) 都是整数表达式，它们的合法性则是一条纯事实，由带类型的内存谓词中的谓词携带。
• 字节同样是无界整数。存储的字节位于 之内，这一范围由带类型的存储谓词断言，并非由字节类型保证。
• 由于这些缩写是透明的，断言中的整数字面量即使出现在地址位置也需要 ii 后缀：应写 data_at 0i Tint vdata_at 0i Tint v，不能写 data_at 0 Tint vdata_at 0 Tint v。

mem_var = Noperm | Noninit | value byte

mem_var = Noperm | Noninit | value byte

这是一个带三个构造子的归纳数据类型，也是 C* 与教科书中的堆模型唯一不同的地方：

一块内存把每个地址映射到一个单元状态：

mem = :addr->mem_var

mem = :addr->mem_var

这个映射是全映射：部分性通过陪域中的 NopermNoperm 编码。因此，无须引入有限映射或部分函数的机制，内存的相等就是普通的函数相等，可以用外延性证明。内存的“足迹”则是由此派生的概念，指状态不为 NopermNoperm 的地址集合，并非原始概念。内存也不必是有限的。

内存的拆分与组合由同一个关系表达。

mem_join (m1:mem) (m2:mem) (m:mem) : bool =
  (!p.
  (m1 p = Noperm /\ m2 p = Noperm /\ m p = Noperm) \/
  (m1 p = Noperm /\ m2 p = Noninit /\ m p = Noninit) \/
  (m1 p = Noninit /\ m2 p = Noperm /\ m p = Noninit) \/
  (?n. m1 p = Noperm /\ m2 p = value n /\ m p = value n) \/
  (?n. m1 p = value n /\ m2 p = Noperm /\ m p = value n))

mem_join (m1:mem) (m2:mem) (m:mem) : bool =
  (!p.
  (m1 p = Noperm /\ m2 p = Noperm /\ m p = Noperm) \/
  (m1 p = Noperm /\ m2 p = Noninit /\ m p = Noninit) \/
  (m1 p = Noninit /\ m2 p = Noperm /\ m p = Noninit) \/
  (?n. m1 p = Noperm /\ m2 p = value n /\ m p = value n) \/
  (?n. m1 p = value n /\ m2 p = Noperm /\ m p = value n))

这个关系是逐点的：mm 是 m1m1 与 m2m2 的合并，当且仅当每一个地址上的三个单元状态都符合所列五种组合之一。这些子句可以按以下情况理解：

• 若两个操作数都没有权限，则结果也没有；
• 若恰有一个操作数持有权限，则结果原样继承该操作数的状态，无论它处于未初始化状态还是存有一个值。

这些子句也明确排除了两种情况。首先，m1 pm1 p 与 m2 pm2 p 不能同时不等于 NopermNoperm：权限是独占的，因此拥有某个单元的内存不可能拆分为两块都拥有该单元的内存。**** 的不相交性正是由模型中的这一限制保证的。其次，合并不能把 NoninitNoninit 变为 value nvalue n：它只重新分配所有权，不会生成新的内容。用户层的断言只通过 **** 使用这个模型，规约中从不直接写出这个关系。

断言就是内存上的谓词：

model = :mem
expr  = :model->bool
hprop = :expr

model = :mem
expr  = :model->bool
hprop = :expr

hprophprop 展开为 :mem->bool:mem->bool，把断言应用于内存得到的 p mp m 就表示满足关系。这里没有单独的公式语法范畴，也没有解释函数，这就是“浅嵌入”的具体含义。在下文的定义中，joinjoin 就是关系 mem_joinmem_join，而 is_unit mis_unit m 表示 mm 处处没有权限（!p. m p = Noperm!p. m p = Noperm）；所有连接词的定义都不直接涉及 NopermNoperm 或 valuevalue。

每个连接词都通过定义引入，并非公理：定义只添加一个常量及其定义方程。用这个方程重写，就可以将常量展开为对应的 lambda 体；各条规则的语义证明正是采用这种方式。

下面先原样列出每组连接词的定义，再说明解析器与打印器所采用的表层记号。

hsep = (\x:expr y:expr m:model. ?m1 m2. join m1 m2 m /\ x m1 /\ y m2)

hsep = (\x:expr y:expr m:model. ?m1 m2. join m1 m2 m /\ x m1 /\ y m2)

mm 能够拆分为两块可合并的内存，分别满足 pp 与 qq，p ** qp ** q 就对 mm 成立。拆分方式受存在量词约束，因此断言不指定某一种拆分方式。不相交性由合并关系保证，无须另行陈述。这里使用 **** 作为记号，是因为 ** 在 HOL Light 中已用于乘法。**** 是优先级为 8 的中缀记号，右结合。

hwand = (\x:expr y:expr m:model. !m1 m2. join m m1 m2 ==> x m1 ==> y m2)

hwand = (\x:expr y:expr m:model. !m1 m2. join m m1 m2 ==> x m1 ==> y m2)

用任何满足 pp 的内存扩展 mm，都能得到满足 qq 的内存，p -* qp -* q 就对 mm 成立。注意 join m m1 m2join m m1 m2 中的参数顺序：被描述的内存 mm 是第一个操作数，m1m1 是被添加的内存，m2m2 是扩展所得的结果，因此魔术棒对添加的部分和结果都作全称量化。它是优先级为 4 的中缀记号，右结合，且 -*-* 只表示魔术棒。

hand  = (\x:expr y:expr m:model. x m /\ y m)
hor   = (\x:expr y:expr m:model. x m \/ y m)
himpl = (\x:expr y:expr m:model. x m ==> y m)

hand  = (\x:expr y:expr m:model. x m /\ y m)
hor   = (\x:expr y:expr m:model. x m \/ y m)
himpl = (\x:expr y:expr m:model. x m ==> y m)

这三个连接词把相应的布尔连接词提升到同一块内存上：p && qp && q 要求一块内存同时满足两个操作数，这正是它与 p ** qp ** q 的区别所在。&&&&（优先级 8）与 ||||（优先级 6）在 :bool:bool 与 :hprop:hprop 上重载，因此当操作数是布尔值时，同一个符号表示 /\/\ 或 \/\/；具体含义由类型推断确定。-->-->（优先级 4）只存在于 hprophprop 层；布尔蕴含仍写作 ==>==>。三者均右结合。

hexists = (\x:A->expr m:model. ?a:A. x a m)
hforall = (\x:A->expr m:model. !a:A. x a m)

hexists = (\x:A->expr m:model. ?a:A. x a m)
hforall = (\x:A->expr m:model. !a:A. x a m)

两者都接受一个函数，将被量化类型的值映射为断言；绑定子记号 exists . exists . 实质上只是 lambda 的另一种写法。类型 AA 是任意的：可以对地址、整数、列表或任何 HOL 类型量化。existsexists 与 forallforall 这两个词在 :bool:bool 与 :hprop:hprop 上重载，这正是 C* 约定用符号 ?? 与 !! 书写布尔量词、用单词书写断言层量词的原因。这样就能在项中直观地区分这两类量词。

hemp = (\m:model. is_unit m)

hemp = (\m:model. is_unit m)

empemp 恰好对处处没有权限的那块内存成立。它是 **** 的单位元（neutral_hsepneutral_hsep 证明了 neutral(**) = empneutral(**) = emp），这使得迭代分离合取是良定义的。

hpure = (\p:bool m:model. p)
hfact = (\p:bool m:model. hand (hpure p) hemp m)

hpure = (\p:bool m:model. p)
hfact = (\p:bool m:model. hand (hpure p) hemp m)

pure()pure() 完全忽略它的内存参数；fact()fact() 还额外要求那块内存为空。两个记号都采用覆盖机制，因此 purepure 与 factfact 始终表示这两个常量。下文将单独讨论二者的区别。

htrue  = (\m:model. T)
hfalse = (\m:model. F)

htrue  = (\m:model. T)
hfalse = (\m:model. F)

任何内存都满足 truetrue，它是表达“除此之外可能还有更多资源”的标准写法；没有内存满足 falsefalse。这两个词在 :bool:bool 与 :hprop:hprop 上重载。符合直觉的几个恒等式都已证明为定理：true -|- pure(T)true -|- pure(T)、false -|- pure(F)false -|- pure(F) 与 fact(T) -|- empfact(T) -|- emp。

断言之间的关系，其类型是 :bool:bool，并非 :hprop:hprop：

hentail = (\x:expr y:expr. !m. x m ==> y m)
logic_equiv = (\x:expr y:expr. hentail x y /\ hentail y x)

hentail = (\x:expr y:expr. !m. x m ==> y m)
logic_equiv = (\x:expr y:expr. hentail x y /\ hentail y x)

• hp1 |-- hp2hp1 |-- hp2（hentailhentail，优先级 2）是在所有内存上的逐点蕴含。
• hp1 -||- hp2hp1 -||- hp2（logic_equivlogic_equiv，优先级 2）是双向成立的蕴含。
• hp1 -|- hp2hp1 -|- hp2（优先级 2）是特化到 :hprop:hprop 上的 HOL 相等：记号 -|--|- 是 (=):hprop->hprop->bool(=):hprop->hprop->bool 的覆盖。因此，表示谓词的定义在断言之间使用 ==，打印时则显示为 -|--|-。

后两个记号表示不同的常量，但二者可以互换：

!hp1 hp2. (hp1 -||- hp2) <=> (hp1 -|- hp2)

!hp1 hp2. (hp1 -||- hp2) <=> (hp1 -|- hp2)

断言是取值于 :bool:bool 的函数，而 HOL 同时具备函数外延性与命题外延性，因此断言相互蕴含就等同于断言相等。这在证明中很有用：处理断言等价时，无须 setoid、合同规则或单独的重写机制。一条已证明的 -|--|- 就是普通的 HOL 等式，REWRITE_TACREWRITE_TAC 可以在断言出现的任何位置使用它，包括绑定子之下和其他连接词内部。

蕴含的自反性、传递性、反对称性（hentail_reflhentail_refl、hentail_transhentail_trans、hentail_antisymhentail_antisym）以及其余规则收录在证明规则中。

两者都把一个布尔命题嵌入为断言，区别仅在于对内存的要求：

pure(P)    对任何内存都成立，无论它拥有什么
fact(P)    仅对空内存成立
hfact_def  !p hp. fact(p) -|- (pure(p) && emp)

pure(P)    对任何内存都成立，无论它拥有什么
fact(P)    仅对空内存成立
hfact_def  !p hp. fact(p) -|- (pure(p) && emp)

这一差别会影响断言的组合。用 &&&& 组合时，两个操作数描述同一块内存，因此 pure(P) && qpure(P) && q 恰好表示“qq 成立，并且 PP 成立”。用 **** 组合时，内存会被拆分，而 pure(P)pure(P) 不限制分配给它的内存。因此，pure(P) ** qpure(P) ** q 不能保证分配给 pure(P)pure(P) 的部分为空，只要求某个子内存满足 qq，相当于用任意框架弱化了 qq。相比之下，fact(P) ** qfact(P) ** q 要求 factfact 一侧的内存为空，因而 qq 仍然描述全部内存。定理 hfact_hpurehfact_hpure 表达了这一关系： fact() ** hp -|- pure() && hpfact() ** hp -|- pure() && hp。

由于符号状态与契约都用 **** 构建，应使用 factfact。相应规则也针对这一形式给出：hsep_hfact_lefthsep_hfact_left 与 hsep_hfact_righthsep_hfact_right 让 factfact 合取项可以在分离合取中自由移动，hfact_elimhfact_elim 将它转换为一条普通假设，hfact_duphfact_dup 则可以复制它，因为纯事实不消耗任何资源。

pure(x == 1i) && data_at p Tint x
fact(x == 1i) ** data_at p Tint x

pure(x == 1i) && data_at p Tint x
fact(x == 1i) ** data_at p Tint x

纯化用于提取蕴含目标中的纯逻辑内容，将关于断言的目标转化为关于整数的目标；参见用策略纯化蕴含。

在有限索引集上作分离合取，只需一个组合子：

hitersep (s: A->bool) (f: A->hprop) = iterate (**) s f

hitersep (s: A->bool) (f: A->hprop) = iterate (**) s f

HOL Light 中的集合就是谓词 A->boolA->bool，而 iterateiterate 是标准库提供的通用函数，用于在有限集上折叠二元运算。只有对交换幺半群，不指定顺序的折叠才是良定义的。这条附加条件已统一卸除：neutral_hsepneutral_hsep 证明了 neutral(**) = empneutral(**) = emp，monoidal_hsepmonoidal_hsep 则由结合律、交换律与单位元律证明了 monoidal(**)monoidal(**)。因此，HOL Light 标准库中的每条 ITERATE_*ITERATE_* 定理都能机械地特化为一条 hitersep_*hitersep_* 定理：

hitersep_empty
  !f. hitersep {} f -|- emp
hitersep_single
  !f x. hitersep {x} f -|- f x
hitersep_insert
  !f x s. FINITE s
          ==> (hitersep (x INSERT s) f -|-
               if x IN s then hitersep s f else (f x) ** (hitersep s f))
hitersep_disjoint_union
  !f s t. FINITE s /\ FINITE t /\ DISJOINT s t
          ==> (hitersep (s UNION t) f -|- (hitersep s f) ** (hitersep t f))
hitersep_hsep
  !f g s. FINITE s
          ==> (hitersep s (\x. (f x) ** (g x)) -|-
               (hitersep s f) ** (hitersep s g))

hitersep_empty
  !f. hitersep {} f -|- emp
hitersep_single
  !f x. hitersep {x} f -|- f x
hitersep_insert
  !f x s. FINITE s
          ==> (hitersep (x INSERT s) f -|-
               if x IN s then hitersep s f else (f x) ** (hitersep s f))
hitersep_disjoint_union
  !f s t. FINITE s /\ FINITE t /\ DISJOINT s t
          ==> (hitersep (s UNION t) f -|- (hitersep s f) ** (hitersep t f))
hitersep_hsep
  !f g s. FINITE s
          ==> (hitersep s (\x. (f x) ** (g x)) -|-
               (hitersep s f) ** (hitersep s g))

采用同样的方法还可以得到 hitersep_diffhitersep_diff、hitersep_deletehitersep_delete、hitersep_eqhitersep_eq（将函数体替换为与其逐点等价的函数体）与 hitersep_caseshitersep_cases（按谓词拆分索引集）。这里的 FINITEFINITE 假设是 iterateiterate 的必要条件，不能省略。用户可以通过这个组合子在索引集上定义自己的谓词。库自带的数组谓词则不使用它：array_atarray_at 是对其值列表递归定义的，第 ii 个元素位于 x + i * sizeof(ty)x + i * sizeof(ty)，其拆分、合并与换基规则直接列于带类型的内存谓词中。

下表列出表层记号、对应的内核常量及其含义，与教程 C* 中的分离逻辑中的汇总表相对应。

中缀优先级从松到紧依次为：|--|--、-|--|-、-||--||- 为 2；-*-*、-->--> 为 4；|||| 为 6；&&&& 与 **** 为 8。它们全部右结合，而函数应用的结合力比它们都强，因此 fact(x > 0i) ** data_at x Tint v |-- truefact(x > 0i) ** data_at x Tint v |-- true 无须括号即可按预期解析。

• addraddr 与 bytebyte 是 :int:int 的透明缩写；地址运算就是整数运算，合法性由谓词断言，类型本身不作保证。
• 一个内存单元处于三种状态之一（NopermNoperm、NoninitNoninit、value value ），而一块内存是全映射 addr->mem_varaddr->mem_var，部分性由 NopermNoperm 编码。
• 拆分由三元关系 mem_joinmem_join 表达，它的五条子句使权限具有独占性；规约从不直接写出它，只通过 **** 使用它。
• 断言就是内存上的谓词，即 hprop = :mem->boolhprop = :mem->bool，每个连接词都在合并关系之上定义，并非公理。
• 蕴含 |--|-- 是逐点蕴含；-|--|- 是断言上的 HOL 相等，heqheq 证明它与相互蕴含 -||--||- 等价，因此断言的等价就是普通的重写等式。
• pure()pure() 在空间上不作任何约束，fact()fact() 则断言内存为空；factfact 是能与 **** 组合的形式，也是规约应当使用的形式。
• hitersephitersep 把 **** 在有限索引集上折叠，monoidal_hsepmonoidal_hsep 为这一折叠一次性提供了证明依据；array_atarray_at 则对其列表递归定义，不使用 hitersephitersep。