内存模型与断言

本页给出 C* 分离逻辑最底下的两层：内存模型，以及在其上定义的断言语言。下文的每一条都是 HOL Light 定义，按证明内核引入它们时的形式抄录，因此这些项可以原样粘贴进反引号包裹的逻辑表达式，或用作某个定义接口的参数。

阅读这些定义时，分层很重要：内存模型确定什么是状态，断言语言随后只借助状态上的两个操作来定义——一个合并关系与一个单位元谓词。没有任何连接词直接提到字节或权限。

地址与字节都是整数：

addr = :int
byte = :int
addr_eqb:addr->addr->bool = (=)
byte_eqb:byte->byte->bool = (=)

addr = :int
byte = :int
addr_eqb:addr->addr->bool = (=)
byte_eqb:byte->byte->bool = (=)

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。

addr_eqbaddr_eqb 与 byte_eqbbyte_eqb 的定义就是 HOL 的相等本身。它们的存在只是为了让模型能用一个显式的比较函数来表述；下文的 single_byte_memsingle_byte_mem 是它们唯一的用武之地。

mem_var = Noperm | Noninit | value byte

mem_var = Noperm | Noninit | value byte

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

用 define_typedefine_type 引入 mem_varmem_var 时还会得到三个构造子的相异性定理与情况穷举定理；证明规则中那些基本的分离代数证明所重写用到的，正是这些事实。

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

mem = :addr->mem_var

mem = :addr->mem_var

这个映射是全映射：部分性通过 NopermNoperm 编码在陪域之内。这一选择免去了任何有限映射或部分函数机制——内存的相等就是普通的函数相等，可由外延性证明，而内存的“足迹”是一个派生概念（状态不为 NopermNoperm 的地址集合），并非原始概念。另外注意，内存并不要求是有限的。

四个常量补全了这个模型：

empty_mem:mem = (\p. Noperm)
single_byte_mem (p:addr) (n:byte) = (\p'. if (addr_eqb p' p) then value n else Noperm)
single_noninit_mem (p:addr) = (\p'. if (addr_eqb p' p) then Noninit else Noperm)
mem_empty (m:mem) : bool = (!p. m p = Noperm)

empty_mem:mem = (\p. Noperm)
single_byte_mem (p:addr) (n:byte) = (\p'. if (addr_eqb p' p) then value n else Noperm)
single_noninit_mem (p:addr) = (\p'. if (addr_eqb p' p) then Noninit else Noperm)
mem_empty (m:mem) : bool = (!p. m p = Noperm)

empty_memempty_mem 与 mem_emptymem_empty 很容易混淆：前者是一块内存，后者是内存上的一个谓词。由外延性可知，empty_memempty_mem 是满足 mem_emptymem_empty 的唯一内存，这也是单位元律可以通过给出 empty_memempty_mem 作为例证来证明的原因。两块单点内存——一个字节，以及一个已拥有但未初始化的单元——是构造每一条带类型的内存谓词所用的原子。

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

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：合并只重新分配所有权，绝不凭空生成内容。

关系之外还有两个辅助常量：

mem_disjoint (m1:mem) (m2:mem) : bool = (!x. (m1 x = Noperm) \/ (m2 x = Noperm))
mem_merge (m1:mem) (m2:mem) : mem = (\x.
  match (m1 x) with
  | Noperm -> m2 x
  | Noninit -> (match (m2 x) with value v2 -> value v2 | _ -> Noninit)
  | value v1 -> value v1
)

mem_disjoint (m1:mem) (m2:mem) : bool = (!x. (m1 x = Noperm) \/ (m2 x = Noperm))
mem_merge (m1:mem) (m2:mem) : mem = (\x.
  match (m1 x) with
  | Noperm -> m2 x
  | Noninit -> (match (m2 x) with value v2 -> value v2 | _ -> Noninit)
  | value v1 -> value v1
)

mem_disjointmem_disjoint 单独给出相容性条件：在每个地址上至少有一侧没有权限。mem_mergemem_merge 则是一个全的组合函数，按固定的优先级消解重叠。两者都不属于断言语言，书写规约时都不应使用：mem_mergemem_merge 只作为证明中的例证存在——它提供 join_assocjoin_assoc 中存在量词所需的中间内存——并且在不相交的参数上它与合并关系一致。用户层的断言只通过 **** 看到这个模型。

断言层是针对一个抽象接口定义的，随后再用内存模型实例化该接口：

model = :mem
expr  = :model->bool
hprop = :expr
join:model->model->model->bool = mem_join
is_unit:model->bool = mem_empty

model = :mem
expr  = :model->bool
hprop = :expr
join:model->model->model->bool = mem_join
is_unit:model->bool = mem_empty

于是断言就是内存上的谓词：hprophprop 展开为 :mem->bool:mem->bool，而把断言作用于内存所得的 p mp m 便是满足关系。这里没有单独的公式语法范畴，也没有解释函数——这就是“浅嵌入”落到实处的含义。

经由 modelmodel、exprexpr、joinjoin 与 is_unitis_unit 的这层间接是有意为之。下文每个连接词都只用 joinjoin 与 is_unitis_unit 定义，从不直接使用 NopermNoperm、valuevalue 或 mem_joinmem_join，因此断言层对底层的分离代数是参数化的，修订内存模型时无须改动任何一条连接词定义。这也意味着把断言一路展开到字节需要两步重写，而不是一步。

关于整个这一层，有两条事实成立：

• 每个连接词都由 new_basic_definitionnew_basic_definition 引入，即作为定义式扩展——它只添加一个常量及其定义方程，不可能让逻辑变得不一致；
• 因此每个连接词都可以通过用其定义定理重写而展开为对应的 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 并不能把那一份限定为空：它只是说某个子内存满足 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 就是 data_atdata_at 在一段索引区间上的迭代分离合取，带类型的内存谓词中的拆分、合并与换基规则皆由此而来。

下表列出表层记号、它所缩写的内核常量，以及它的含义。这张表是 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 表达，它的五条子句使权限具有独占性；mem_disjointmem_disjoint 是相容性条件，mem_mergemem_merge 则是仅供证明使用的例证。
• 断言就是内存上的谓词，即 hprop = :mem->boolhprop = :mem->bool，而每个连接词都是针对抽象的 joinjoin 与 is_unitis_unit 写出的定义，并非公理。
• 蕴含 |--|-- 是逐点蕴含；-|--|- 是断言上的 HOL 相等，并由 heqheq 与相互蕴含 -||--||- 重合，因此断言的等价就是普通的重写等式。
• pure()pure() 在空间上不作任何约束，fact()fact() 则断言内存为空；factfact 是能与 **** 组合的形式，也是规约应当使用的形式。
• hitersephitersep 把 **** 在有限索引集上折叠，其正当性由 monoidal_hsepmonoidal_hsep 一次性给出，并且是数组谓词的基础。