分离逻辑断言的Coq证明策略

Tactics for Proving Separation Logic Assertions in Coq

摘要: 大型程序的验证是一项十分复杂但又极其重要的工作。本文以使用Hoare风格的分离逻辑验证C程序为目的，在基于Coq的现有的验证系统中，添加分离蕴含以扩展其分离逻辑断言语法，使得分离逻辑断言可以更灵活的描述程序状态。此外，我们开发了一些相关的自动证明策略，尽可能的通过减少人工证明来提高验证效率。

Abstract: The verification of the correctness of large programs is an unmanageable but important endeavor. We are interested in verifying C programs with formal methods; the logic is separation logic, a Hoare-style program logic. In this paper, we present a simple extension of the syntax of separation logic assertion on existing verification system in Coq proof assistant to make assertions more ver-satile and flexible to describe the state of programs. Moreover, we develop several tactics for prov-ing some related assertions to reduce manual proof as much as possible and improve the efficiency of verification.

1. 引言

随着科技的发展，软件系统的应用日益广泛，其正确性也越来越重要，尤其是安全攸关 [1]，商业攸关以及任务攸关等系统。由于C语言具有编译效率高、可移植性好等特点，大多数软件系统较底层的开发是由它实现的。验证C程序的正确性可采用形式化方法，该方法是通过使用数学方法，对软件或硬件系统进行描述、开发和验证的一种技术。然而，大型C程序的验证是一个十分巨大且困难的工作，并且该问题已被证明是一个不可判定性问题，即不可以完全自动化验证。因此，交互式的证明C程序的正确性是一个很好的选择。

自20世纪60年代以来，Hoare提出的Hoare逻辑是一直被广泛应用的程序验证逻辑系统 [2]，用于对命令式程序进行推理验证，是程序逻辑研究领域的一个重大进展。但是Hoare逻辑对于带有指针的程序的验证仍然十分繁琐。

2002年，Reynolds和O’Hearn将Hoare逻辑拓展为可推理验证操作动态分配内存程序的分离逻辑 [3] [4]，进一步发展了程序逻辑理论。近二十年以来，分离逻辑已被拓展至多种版本，其使用范围更加广泛，在程序验证中占据着越来越重要的地位。分离逻辑具有更强的表达力和验证能力，例如并发程序的验证等。然而表达力越强的程序逻辑，其验证过程越复杂。分离逻辑已被证明是一个不可判定的程序逻辑，因此使用分离逻辑验证C程序的过程无法达到完全自动化。然而大型的C程序证明十分复杂，手动证明不但需要大量的人力物力，可信度也不是很高，因此人机交互式的证明C程序是不可避免的。

在过去的几十年中，有关交互式定理证明器实现与应用分离逻辑的进展有很多，例如 [5] [6] [7] [8] [9]。Coq [10] 是一个被广泛应用的人机交互式的定理证明器，其基本理论是归纳结构的演算。一些由 [11] 提供的Coq实用策略也是用于基于分离逻辑的C程序验证，这些高度自动化的策略可以仅使用单行证明脚本完成对特定C程序的验证，例如，该系统只需使用1行仅有4个单词的证明脚本来证明经典的就地反转链表算法，而McCreight的Coq策略 [12] 需要68行400个单词，Charge的策略 [13] 需要25行105个单词。本文将分离逻辑中的分离蕴含运算符添加到该系统的分离逻辑断言语法中，并提供一些相关的自动证明策略。

2. 程序逻辑和证明助手

2.1. Hoare逻辑

Hoare逻辑是使用严格的数理逻辑推理来验证命令式程序正确性的逻辑系统，它使用逻辑断言来描述程序的状态。

Hoare使用霍尔三元组来描述程序的行为，是Hoare逻辑的中心特征，其形式如下：

$\left\{P\right\}c\left\{Q\right\},$

其中断言P是前置条件，断言Q是后置条件，c是程序。前置条件和后置条件是分别描述执行程序c前后的程序状态的断言。一个有效的霍尔三元组表示：如果程序c执行前，内存状态满足断言P，那么程序执行后，内存状态满足断言Q。考虑以下霍尔三元组：

$\left\{x=3\right\}x:=x\ast 2\left\{x>4\right\},$

它显然是有效的，由于程序 $x:=x\ast 2$ 执行前x的值为3，执行后可得出x的值为6，因此 $x>3$ 为真。然而上述霍尔三元组并不够精准，如果更换其后置条件为 $x>5\wedge x<10$，则霍尔三元组为 $\left\{x=3\right\}x:=x\ast 2\left\{x>5\wedge x<10\right\}$，因为 $x=6$ 蕴含 $x>5\wedge x<10$，所以该霍尔三元组也是有效的。显然 $x>5\wedge x<10$ 相比于 $x>3$ 更加精准，但是相对于 $x=6$ 还是要弱一些，像 $x=6$ 这样的后置条件通常被称之为最强后置条件。一般的，对于给定的霍尔三元组{P} c {Q}，对于所有的Q'，如果有{P} c {Q'}，且Q ⇒ Q'，则称Q为对应的P和c的最强后置条件。与最强后置条件类似，如果对于所有的P'，有t {P'} c {Q}，且P' ⇒ P，那么称P为最弱前置条件。在霍尔逻辑中，下面的规则可以根据对应的语句与后置条件生成最弱前置条件：

$\begin{array}{l}\frac{}{\left\{\text{Q}\left[\text{a/x}\right]\right\}\text{x}\text{:}=\text{a}\left\{\text{Q}\right\}}\left(赋值规则\right)\\ \frac{\left\{\text{P}\right\}{\text{c}}_{\text{1}}\left\{\text{Q}\right\}\left\{\text{Q}\right\}{\text{c}}_{\text{2}}\left\{\text{R}\right\}}{\left\{\text{P}\right\}{\text{c}}_{\text{1}}\text{;}{\text{c}}_{\text{2}}\left\{\text{R}\right\}}\left(顺序规则\right)\\ \frac{\left\{\text{P}\right\}{\text{c}}_{\text{1}}\left\{\text{Q}\right\}\left\{\text{P}\right\}{\text{c}}_{\text{2}}\left\{\text{Q}\right\}}{\left\{\text{P}\right\}IF\text{b}THEN{\text{c}}_{\text{1}}ELSE{\text{c}}_{\text{2}}\left\{\text{Q}\right\}}\left(条件规则\right)\\ \frac{\left\{\text{P}\wedge \text{b}\right\}\text{c}\left\{\text{P}\right\}}{\left\{\text{P}\right\}WHILE\text{b}DO\text{c}END\left\{\text{P}\wedge \neg \text{b}\right\}}\left(循环规则\right)\end{array}$

其中Q[a/x]表示使用a替换Q中x的每次自由出现。此外，推论规则(如下)可以加强前置条件或者减弱后置条件：

$\frac{{\mathrm{P}}^{\prime }\Rightarrow \text{P}\left\{\text{P}\right\}\text{c}\left\{\text{Q}\right\}\text{Q}\Rightarrow \text{<msup> <mn> Q </mn> <mo> ′ </mo> </msup>}}{\left\{\text{<msup> <mn> P </mn> <mo> ′ </mo> </msup>}\right\}\text{c}\left\{\text{<msup> <mn> Q </mn> <mo> ′ </mo> </msup>}\right\}}$

自1960年起，Hoare逻辑被广泛的应用于命令式程序语言的验证中，然而，在验证带有指针的程序时，其证明过程仍然十分复杂，极具挑战性。2002年，分离逻辑作为霍尔逻辑的拓展，简化了此类证明过程。

2.2. 分离逻辑

分离逻辑是Hoare霍尔逻辑的拓展，它引入了两个重要的运算符分别是分离合取(∗)和分离蕴涵(−∗)，它们的形式语义如下：

$\begin{array}{l}s,h|\text{}=p_0\ast p_1\text{iff}\exists h_0,h_1\\ h_0\perp h_1\text{and}{h}_0\cdot h_1=h\text{and}s,h_0|\text{}=p_0\text{and}s,h_1|\text{}=p_1\end{array}$

其中s表示栈，h表示堆， $h_0\perp h_1$ 表示堆 $h_0$ 和 $h_1$ 不相交， $h_0\cdot h_1$ 表示堆 $h_0$ 和 $h_1$ 的并集。[P * Q] s h断言整个堆h分为两个不相交的部分 $h_0$ 和 $h_1$，对于子堆 $h_0$，断言P为真，对于子堆 $h_1$，断言Q为真。

$\begin{array}{l}s,h|\text{}=p_0-\text{}\text{}\text{}\ast p_1\text{iff}\forall h^{\prime }\\ \left(h^{\prime }\perp h\text{and}s,h^{\prime }\text{|}\text{}=p_0\right)\text{implies}s,h\cdot h^{\prime }\text{|}\text{}=p_1\end{array}$

也就是说，如果堆的扩展h'满足断言 $p_0$，并且断言 $p_0$ 对h'是正确的，则对于扩展后的堆 $h\cdot h^{\prime }$ 满足断言 $p_1$。

分离逻辑通过表达显示分离的逻辑连接词以及相应的规则消除了共享的可能，具有较强的表达能力。分离逻辑用于程序验证，简化了程序的验证工作，例如带有数组和指针的程序，并支持局部推理，其分离思想和对应的框架规则使得局部推理可以很好地应用到程序验证中。较比Hoare逻辑，分离逻辑具有更强的表达能力与验证能力，因此继Hoare逻辑之后，分离逻辑成为程序验证的一种重要方法。

2.3. Coq证明助手

交互式定理证明工具Coq，为交互式形式化验证提供了一个丰富的环境。Coq的规范语言是Galina，它支持开发数学定理以及证明程序规范，其命令语言为vernacular。

通常，Coq是一个开发数学证明的环境，其应用包括法伊特–汤普森(Feit-Thompson)定理的证明，实现了CompCert编译器 [14] 以及VST [11] [15] 等。它虽然是交互式的定理证明器，不能达到完全自动化，但是它拥有着强大的判定过程以及自动化证明策略库，还有一种编写自动证明策略的语言，称为Ltac [16]。本文旨在使用Coq证明助手验证C程序的正确性，其中的证明策略使用Ltac语言实现。

3. 分离逻辑断言

分离逻辑引入分离合取和分离蕴涵等运算符扩展断言语法，从而可以对堆进行更简洁而灵活的描述。本节将添加分离蕴含到原有系统中，扩展系统的断言语法 [17]。

下面阐述如何逐步将分离蕴含添加到原有系统中，首先，扩充原有断言语法如下：

$\begin{array}{l}扩充前\text{:}(Asrt)p::=\\ emp\left|true\right|false|a\mapsto v|e=v|x@a\\ |p*p|Exx.p|p\wedge p|p\vee q|\langle p\rangle \\ \Downarrow \\ 扩充后\text{:}(Asrt)p::=\\ emp\left|true\right|false|a\mapsto v|e=v|x@a\\ |p*p|p-\text{}-\text{}*p|Exx.p|p\wedge p|p\vee q|\langle p\rangle \end{array}$

在Coq中，添加构造子Awand，这意味着将分离蕴含加入到Asrt的归纳定义中：

$|Awand(P:asrt)(Q:asrt)$

随后定义

$Infix\text{'}\text{'}-\text{}-\text{}*\text{'}\text{'}:=Awand.$

意味着P −∗ Q代表 (Awand P Q)。下一步，在Coq中描述s |= P −∗ Q的含义如下：

$\begin{array}{l}existsM1M2M,\\ M=get\_mems\wedge MemMod.joinM1M2M\wedge \\ (sat(substmemsM1)p\to sat(substmemsM)q)\end{array}$

其中 (sat s P) 表示s| = P，即内存s满足断言P。显然，M，M1和M2代表堆，并且参照章节2.2中[P −∗ Q] s h的定义，(MemMod.join M1 M2 M)表示 $\text{M}1\perp \text{M}2$ 并且 $\text{M}1\cdot \text{M}2=\text{M}$。

当然，仍有一些关于添加分离蕴含到系统中的细节，我们在这里不关注。

4. 策略

从本节开始，我们将在Coq中证明工作中使用的部分推理规则的可靠性并介绍证明带有分离蕴含的分离逻辑断言的策略。

4.1. 推理规则

以下是两个重要的推理规则，分别称为柯灵规则和柯灵逆反：

$\frac{\text{P}\ast \text{Q}\Rightarrow \text{R}}{\text{P}\Rightarrow \left(\text{Q}-\text{}-\text{}\ast \text{R}\right)}\left(柯灵规则\right)\frac{\text{P}\Rightarrow \left(\text{Q}-\text{}-\text{}\ast \text{R}\right)}{\text{P}\ast \text{Q}\Rightarrow \text{R}}\left(柯灵逆反规则\right)$

柯灵规则及其逆反规则表述了分离合取和分离蕴涵之间的关系，并且由此可以推导出一系列推理规则。我们从几个基本示例开始阐述如何在Coq中证明它们是正确的。考虑下面的推断规则，它可由柯灵规则推出：

$\frac{}{\text{emp}\Rightarrow \left(\text{P}-\text{}\ast \text{P}\right)}$

证明过程如下：

$Theoremawand\_emp:forallP,emp\Rightarrow P-\text{}-\text{}*P.$

Theorem是一个命令，它表示正确性证明的开始，其证明过程从以下状态开始：

$\begin{array}{l}1subgoal\\ \\ \text{=================}\\ forallP:asrt,emp\Rightarrow P-\text{}-\text{}*P\end{array}$

$\begin{array}{l}Proof.introP.\\ \\ P:asrt\\ \text{=================}\\ emp\Rightarrow P-\text{}-\text{}*P\end{array}$

proof是指启动证明脚本，而intro P将P转变为自由变量。这里，我们可以应用柯灵规则如下：

$\begin{array}{l}applyCURRYINGwith(Q:=P)(R:=P).\\ P:asrt\\ \text{=================}\\ emp*P\Rightarrow P\\ applyastar\_elim.\end{array}$

astar_elim是一个证明定理，其内容是：对所有P，emp ∗ P⇒P成立。应用astar_elim后，则不再有子目标，这意味着证明已完成。

$Qed.$

最后，Qed检查证明是否完成。

注意到上面证明的规则可以被用来消去一些分离蕴含，那么以这样一个简单的设想为例，实现一个简单的策略，以展示如何使用交互式的机器证明代替手动证明。该策略称为sclearwand：

$\begin{array}{l}Ltacsclearwand:=\\ 1matchgoalwith\\ 2||-?s\text{|=}?\text{}A\Rightarrow matchfind\_awandAwith\\ 3\text{|}some?n\Rightarrow sep\_liftn;\\ 4matchgoalwith\\ 5|H:\_\text{|=}\_|-\_\text{|=}(?B-\text{}-\text{}*?B)*?C\Rightarrow \\ \text{6}\text{}\text{}applyastar\_l\_aemp\_introinH;\\ \text{7}eapplyastar\_mono;[eapplyawand\_emp|\\ \text{8}intross\text{'}H\text{'};exactH\text{'}|auto];sclearwand\\ \text{9}|\_\Rightarrow idtac\\ 10end\\ 1\text{1}|\_\Rightarrow idtac\\ 12end\\ 13\text{}\text{|}\_\Rightarrow fail\\ 14end.\end{array}$

首先匹配目标的模式，如果目标是类似于第2行的模式，则在第3行中，调用find_awand以查找A中分离蕴涵的位置。在第3行中，sep_lift将其移至A的左侧，随后证明目标将在第5~11行中解决，其中astar_l_aemp_intro和astar_mono分别是如下规则：

$\frac{}{\text{P}\Rightarrow \text{emp}\ast \text{P}}\frac{\text{P}\Rightarrow \text{<msup> <mn> P </mn> <mo> ′ </mo> </msup>}\text{Q}\Rightarrow \text{<msup> <mn> Q </mn> <mo> ′ </mo> </msup>}}{\text{P}\ast \text{Q}\Rightarrow \text{<msup> <mn> P </mn> <mo> ′ </mo> </msup>}\ast \text{<msup> <mn> Q </mn> <mo> ′ </mo> </msup>}}$

sclearwand可以消除(P −∗ P)，之后“emp”将在证明目标中取代它，例如：

$\begin{array}{l}Goal\text{}forall(AB:asrt),A\Rightarrow A*(B-\text{}*B).\\ Proof.intros.sclearwand.Qed.\end{array}$

现在，考虑下面的推理规则并在Coq中证明其整确定性

$\frac{\text{<msup> <mn> P </mn> <mo> ′ </mo> </msup>}\Rightarrow \text{P}\text{Q}\Rightarrow \text{<msup> <mn> Q </mn> <mo> ′ </mo> </msup>}}{\text{P}-\text{}-\text{}\ast \text{Q}\Rightarrow \text{<msup> <mn> P </mn> <mo> ′ </mo> </msup>}-\text{}-\text{}\ast \text{<msup> <mn> Q </mn> <mo> ′ </mo> </msup>}}$

$\begin{array}{l}Theoremawand\_pro:forallPP\text{'}QQ\text{'},P\text{'}\Rightarrow P\to Q\Rightarrow Q\text{'}\to P-\text{}-\text{}*Q\Rightarrow P\text{'}-\text{}-\text{}*Q\text{'}.\\ Proof.\\ intros.simplin*;mytac.\\ do3eexists;mytac;eauto.\\ Qed.\end{array}$

mytac是原有系统中用于断言的自动证明策略，而上面的规则可以使用mytac证明，说明分离蕴含已被很好的添加到系统中。

仍然有很多关于分离蕴含的推理规则如下，在这里省略对他们的可靠性证明：

$\begin{array}{l}\frac{}{\text{Q}\ast \left(\text{Q}-\text{}-\text{}\ast \text{P}\right)\Rightarrow \text{P}}\frac{}{\text{P}\Rightarrow \text{Q}\ast \left(\text{Q}-\text{}-\text{}\ast \text{P}\right)}\\ \frac{}{\left(\text{P}\ast \text{R}\right)\Rightarrow \left(\text{P}\ast \left(\text{Q}-\text{}-\text{}\ast \left(\text{Q}\ast \text{R}\right)\right)\right)}\\ \\ \frac{{\text{P}}_0\Rightarrow \left(\text{Q}-\text{}-\text{}\ast \text{R}\right){\text{P}}_1\Rightarrow \left(\text{R}-\text{}-\text{}\ast \text{S}\right)}{{\text{P}}_0\ast {\text{P}}_1\Rightarrow \left(\text{Q}-\text{}-\text{}\ast \text{S}\right)}\\ \\ \frac{\text{P}\Rightarrow \text{<msup> <mn> P </mn> <mo> ′ </mo> </msup>}}{\text{P}\ast \left(\text{<msup> <mn> P </mn> <mo> ′ </mo> </msup>}-\text{}-\text{}\ast \text{Q}\right)\Rightarrow \text{Q}}\end{array}$

4.2. 资源检测

在 [5] 提供的实用策略可以仅使用一行证明脚本证明整个程序，即“repeat hoare forward; sep pure”，其中repeat表示重复执行某项策略，这里指重复执行“hoare forward; sep pure”，sep pure是证明关于纯断言的策略，而hoare forward可以证明霍尔三元组⊢{P} c {Q}，是验证程序的的关键。

hoare forward的第一步是资源检测(check_resource)，它检测前置条件是否具有语句执行所需的信息。例如：

$\text{{}y>\text{}\text{}\text{}\to \text{\_\_}}y:=x\text{{}x>\text{}\text{}\text{}\to \text{\_\_}\ast y>\text{}\text{}\text{}\to \text{\_\_}}$

其中 $\text{x}\rightarrowtail \text{v}$ 表示变量x的值为v。显然，如果将x的值赋给y我们首先需要x的值。这里，resource_check在前置条件中没有找到有关x的信息，它将返回一条用户友好的消息，用户可以根据将相应的信息添加前置条件中，如下：

$\text{{}x>\text{}\text{}\text{}\to \text{\_\_}\ast y>\text{}\text{}\text{}\to \text{\_\_}}y:=x\text{{}x>\text{}\text{}\text{}\to \text{\_\_}\ast y>\text{}\text{}\text{}\to \text{\_}}$

这就像开始验证前的预处理一样。然而，尽管如上一节所述分离蕴含已经被添加到系统中，并且前置条件中具有足够的信息，resource_check也无法检测到有关分离蕴含的信息，例如：

$\text{{}x>\text{}\text{}\text{}\to \text{\_\_}\ast \left(x>\text{}\text{}\text{}\to v_1-\text{}-\text{}\ast y>\text{}\text{}\text{}\to \text{\_}\right)\text{}}x:=v_1;y:=v_2\text{{}y>\text{}\text{}\text{}\to v_2\text{}}$

前置条件中虽然存在 $\text{y}\rightarrowtail \_$，但无法被识别。因此，我们需要调整resource_check的组件使得分离蕴含可以被识别并可以从中检测到需要的信息。

考虑resource_check的组件find_match_retV，它可以识别“∗”，但无法识别“−∗”，如下：

$\begin{array}{l}Ltacfind\_match\_retVHpx:=\\ \text{1}matchHpwith\\ \text{2}|?A*?B\Rightarrow matchfind\_match\_retVAxwith\\ \text{3}|some?v\Rightarrow constr:(somev)\\ \text{4}|\_\Rightarrow matchfind\_match\_retVBxwith\\ \text{5}|some?v\Rightarrow constr:(somev)\\ \text{6}|\_\Rightarrow constr:(@None)\\ \text{7}end\\ \text{8}end\\ \text{9}|?A\Rightarrow (*hoare\_tactics.v*)\\ \text{10}end.\end{array}$

将其更改如下：

$\begin{array}{l}Ltacfind\_match\_retV\text{'}Hpx:=\\ \text{1}matchHpwith\\ \text{2}|?A*?B\Rightarrow matchfind\_match\_retVAxwith\\ \text{3}|some?v\Rightarrow constr:(somev)\\ \text{4}|\_\Rightarrow matchfind\_match\_retVBxwith\\ \text{5}|some?v\Rightarrow constr:(somev)\\ \text{6}|\_\Rightarrow constr:(@None)\\ \text{7}end\\ \text{8}end\\ \text{9}|?C-\text{}-\text{}*?D\Rightarrow matchfind\_match\_retVCxwith\\ \text{10}|some?v\Rightarrow constr:(somev)\\ \text{11}|\_\Rightarrow (*hoare\_tactics.v*)\\ \text{12}matchfind\_match\_retVDxwith\\ \text{13}|some?v\Rightarrow constr:(somev)\\ \text{14}|\_\Rightarrow constr:(@None)\\ \text{15}end\\ \text{16}end\\ \text{17}|?A\Rightarrow (*hoare\_tactics.v*)\\ \text{18}end.\end{array}$

将resource_check中的find_match_retV替换为find_match_retV'之后，上述 ，因此hoare forward可以正常开始运行。

5. 一个简单的例子

本节将给出一个简单的示例来表明，我们可以证明程序状态由含有分离蕴含的断言描述的程序规范。

sclearwand in是可以证明含有分离蕴含的断言的策略，例如，sclearwand in策略可以证明下面的证明目标：

$\begin{array}{l}Goal\text{}forall(ABDE:asrt),\\ (A*D*B)*((D*A*B)-\text{}-\text{}*E)\Rightarrow E.\\ Proof.intros.sclearwand\_inH.Qed.\end{array}$

我们以一个简单的例子来说明它在程序验证中的作用，如下：

$\begin{array}{c}\text{{}x>\text{}\text{}\text{}\to v_1\ast (x>\text{}\text{}\text{}\to null-\text{}-\text{}\ast y>\text{}\text{}\text{}\to v_2)\text{}}\\ x:=null;\\ \{y>\text{}\text{}\text{}\to v_2\}\end{array}$

这里，运行“repeat hoare forward; sep pure”后得到一个子目标：

$\left(x>\text{}\text{}\text{}\to null\ast \left(x>\text{}\text{}\text{}\to null-\text{}-\text{}\ast y>\text{}\text{}\text{}\to v_2\right)\right)\Rightarrow \left(y>\text{}\text{}\text{}\to v_2\right)$

运行“sclearwand in H”，该子目标被解决，证明完成。

6. 总结

我们通过添加分离蕴含操作符到已有系统的分离逻辑断言语法中，拓展了该验证系统，并提供了一些相关的自动证明策略。但是由于分离逻辑断言的复杂多样性，我们现有的策略不足以解决包含分离蕴涵的断言的所有证明。将来，我们将扩展自动证明策略以提高程序验证的效率。

NOTES

^*通讯作者。