证明编译器正确性的软件中使用的CVC证明生成器的特性

29--理论计算机科学电子笔记70第2期（2002）URL：http://www.elsevier.nl/locate/entcs/volume 70. html13页s从椭圆LF作者：Aaron Stump Barrett，and David L. 莳萝计算机系统实验室，斯坦福大学，斯坦福，CA 94305，美国电子邮件：stump，barrett，cs.stanford.edu电话：+1 650 725 3646，传真：+1 650 725 6949摘要最近，能够为输出的正确性产生可独立检查的证据的软件在证明编译器和携带证据的代码中的使用中受到了关注。 CVC（“合作有效性检查器”）是一个证明生成有效性检查器，用于丰富背景理论的一阶逻辑的可判定片段。 本文介绍了如何证明有效的公式产生的线性实算术实现CVC的决策过程。 它示出了如何扩展LF支持证明规则示意图中的arity（“ 椭 圆 ” 规 则 ） 是 非 常 方 便 的 。1介绍自动推理系统产生易于验证的证明的能力已被广泛认为是有价值的（参见，例如，[14，4]）。最近，像携带证明的代码和携带证明的认证这样的应用已经产生了对证明的新需求[9，1]。爱丁堡逻辑框架（英语：EdinburghLogical Framework）[7]已经成为一种广泛使用的元语言，用于表示这些应用程序的证明系统该表示法使得证明检查被简化为LF类型检查。CVC（CVC为它声称有效的公式提供证明。每个辅助DP都为它执行的所有推理提供证明。这些证明是在LF的扩展版本中表示的，称为LFnat。 在LFnat中，列表可以直接表示。 的目标本文将展示LFnat的特性如何使其方便地进行编程，从一个相当复杂的决策过程，线性实数运算的DP的证明组织如下。第2节介绍了DP的线性实算术理论的选定部分第3节讨论了一些困难2002年由ElsevierScienceB. V.操作访问根据C CB Y-NC-N D许可证进行。斯坦，巴雷特，还有迪尔30∗V−用纯LF来表示证明。第4节描述了LFnat，第5节显示了与决策过程中的推理步骤相对应的证明规则如何在LFnat中表示。熟悉LF或者必须假设具有依赖类型的其它类型理论（参见，例如，[10]）。本文件介绍了正在进行的工作2CVC中线性实数运算的判定在线性实数运算中，项是用二进制函数符号+、和/;一元函数符号;数字0、1、2等;和一个可数无限集合中的变量。变量在实数范围内变化。线性的限制是任何项都不能包含t tJ形式的子项，其中t和tJ都包含一个变量。此外，我们将除数限制为非零数字。原子公式则是方程t=tJ和项之间的不等式t tJ通常，文字是原子公式或它们的否定。在CVC中，命题推理与理论特定推理是分开的（见[2]）。为了描述一个理论的DP，提出一个算法来测试一组文字的可满足性是足够的。在CVC中，这样一组文字被一次一个文字地呈现给DPDP负责通知系统的其余部分，无论何时它已经给出的文字集是不满意的将文字赋予DP称为将文字断言到DP。然后，它展示了线性实数算术的DP如何处理每个可能被断言的文字。DP由三个主要组件组成：算术项的规范器、断言方程的求解器和实现Fourier-Motzkin变量消除以处理断言方程的组件不等式现在我们将详细描述规范器和求解器。关于求解器的部分解释了如何处理不等式t/=tJ由于篇幅的原因，我们将2.1术语规范将项放入标准形式中以供求解器和Fourier-Motzkin组件使用是很方便的。本节描述如何执行术语的规范化。设V是变量集合V的任意固定全序。一个常数算术项是互质形式i，它的形式是N/D，其中N和D是互质数，D是正数。线性算术项的自然标准形式是多项式c +c1<$x1+. c n<$x n，其中(i) c，c1，. ，c n是互质形式的常数算术项(ii) x1，.，xn∈ V斯坦，巴雷特，还有迪尔31(iii) 对于所有1≤i j≤n，xi<$xj我们现在考虑如何在CVC系统中实现算法以将线性算术项放入这样的形式。CVC中多项式的自然和方便的内部实现是将n元加法运算符应用于单项式：例如， 3<$x +4<$y+z表示为（+（3<$x）（4<$y）z）。这是一个很好的表示，因为在CVC基础结构中，表达式的任何直接子级可以在固定时间内访问。在递归中，如果多项式被表示为二元加法运算符的嵌套应用，则访问多项式的第i个因此，将多项式表示为n元加法算子的应用更为有效使一个线性算术项成为经典的第一步是把它转换成一种特殊的形式。2.1.1简化为简化形式本节展示了如何将线性算术项转换为简化形式（+c（c1<$x1）. （c nxn）），其中c，c1，.，c n是常数算术项，并且x1，.，xn∈ V，但相似项（ci<$x i和c j<$x j，其中x i<$x j）尚未组合，也未根据变量的排序对单项式进行排序。后面的操作发生在册封的下一步有几种特殊的情况是常数项c，其中n等于0的形式是（+c）;变量的形式是（+0（1v））。它简化了衰减算法的语句，将常数和变量暂时转换成这些形式。CVC中的主要重写引擎是一个简化器，它在断言到附属DP之前自底向上重写文字。理论特定的重写可以注册为该理论的函数和谓词符号。在子项的子项被完全简化之后，这些重写将被简化器调用以尝试重写子项。把一个词在特定于理论的重写中实现，该重写针对算术函数符号（+、、/和−）进行注册。它包含在图2.1.1中给出的重写中，它假设被重写的项的直接子表达式已经是被重写的形式。加有两个规则：第一个是当有两个被加数时，第二个是当有两个以上的被加数时（在该规则中假设m>0乘法和除法的规则假设左被乘数和左除数分别是常数算术项。我们省略了乘法的类似规则，其中右被乘数是常数项。2.1.2完成封圣一旦一个项是以非线性形式出现，则可以通过对单项式进行排序来完成经典化，使得如果x≠y，则c≠x在d≠y之前。在得到的多项式中，所有相似项c1x，.，将出现具有相同变量的c nx斯坦，巴雷特，还有迪尔32∗[uminus] −（+c（c1<$x1）. （cn<$xn））−→（+（−c）（−c1<$x1）. （−cn<$xn））[mult]cJ（+c（c1x1）. （cn<$xn））−→（+（cJ<$c）（（cJ<$c1）<$x1）. （（cJ<$cn）<$xn））[除法]（+c（c1<$x1）. （cn<$xn））/cJ−→（+（c/cJ）（（c1/cJ）x1）. . . （（cn/cJ）xn））[加法]（+（+c（c1<$x1）. （c n<$x n））（+d（d1<$y1）. （dnJynJ）−→（+（c + d）（c1<$x1）. （c nx n）（d1y1）.（dnJynJ））[addition]（+t1. tm（+c（c1<$x1）. （c n<$x n））（+d（d1<$y1）.（dnJynJ）−→ （+t1. tm（+（c + d）（c1<$x1）. （c nx n）（d1y1）.（dnJ<$ynJ）[常数]c −→（+c）[变量]v−→（+ 0（1v））图1.一、重写以增加线性算术项紧挨着这些项可以通过在多项式中用（c1+. c n）x.为了完成经典化，像2/4+ 3/ 6这样的常数算术项被放入互质形式。最后，我们重写了一些（+（1v）0）−→v（+c）−→c2.2求解器现在我们考虑如何处理断言的等式t=tJ，其中t和tJ是标准形式。斯坦，巴雷特，还有迪尔33−/2.2.1经典化方程对于mtj=0，该方程被简化为一个标准形式，其中tj是项t+（−tJ）的标准形式。 如果t是（规范）常量算术项，则nift是 该等式等于T_R_U_E，并且可以丢弃p_ed;否则，它等效于T_R_E，并且DP报告断言的文字的集合是不可满足的。如果n不是常数项，则通过隔离一个变量来求解n=02.2.2隔离变量此时方程的形式为（+c（c1<$x1）. （cn<$xn））= 0从方程的左侧选择一个变量进行隔离。当前，选择具有最短通知列表（当断言具有作为其左侧的xi的等式时要执行的任务的列表）的变量xi然后将方程改写为：xi=（+d（d1<$x1）. . . （di−1<$xi−1）（di+1<$xi+1）. . .（dn<$xn）），其中对于所有j∈ {1，.，i− 1，i + 1，. n}，d j是（−c j/c i）的互质形式; d是（c/c i）的互质形式。 然后将该等式提交到由CVC的基础设施维护的等式数据库。这将导致xi在算术理论中的所有文字中被方程的右侧替换。这就从这些文字中删除了变量xi。随后断言的文字也将应用此替换2.2.3处理不平等像t=tJ这样的不等式只要将等式x=y提交到CVC中的等式数据库中，就可以通过简单地将不等式中的x替换为y来处理（如果不等式包含x任何时候不平等性以这种方式更新，并且当它第一次被断言时，方程的规范化器（上面刚刚描述的）在t=tJ上运行，以确保它不会规范为TRUE。如果它真的被规范为TRUE，那么DP报告说，到目前为止断言的文字集是不满意的。3制作样张既然已经描述了线性实数运算的DP的规范器和求解器，我们转向产生证明的问题我们遵循的CVC的基础设施已经被用于生成证明。例如，简化器将为理论特定重写的单个步骤产生的证明粘在一起。使用证明规则将证明粘在一起斯坦，巴雷特，还有迪尔34∗∗∗∗∗∗−平等的传递性和一致性。此外，等式数据库期望并存储提交给它的每个等式的证明。证明产生问题中更具挑战性的部分是如何描述LF中决策过程的推理规则。在我们的例子中，如果我们使用纯LF，多项式的表示会立即出现困难。正如上面讨论的（2.1节），DP与多项式一起工作，多项式是n元加法算子的应用. LF不提供对像这样的arity-polymorphic运算符的直接支持，因此多项式必须在LF中不那么直接地表示它可以被编码为二进制加法运算符的嵌套应用（例如， （+ 5）（+（3 （十）（4） （y）或者作为加法运算符对单项式列表的应用（例如，（+（cons5（cons（3x）（cons（4y）null））。这两种表示都是间接的，在这个意义上说，一个单一的功能应用程序（n元加法）在对象语言是由一个渐进的更大数量（n）的功能应用程序在LF表示对于多项式的间接表示，DP中的简单推断例如，对于多项式的间接表示，首先隔离多项式的第i个例如，考虑到（+ 5（3 <$x）（4 <$y））= 0 −→ −4<$y=（+ 5（3 <$x））。如果第一个方程表示为类似于（eq（+（cons5（cons（3x）（cons（4y）null）0）的东西，那么用于隔离第i个单项式的最自然的LF编码A.B写为{x：A}B）：隔离等式：{L：list} {L{t：trm real} {i：natural}{P：（removeith iLt(pf（eq（eq（+ L）0）（eq（减去t）（+L '））））这条规则说，假设其他适当的声明，隔离方程（+ L）= 0中的第i个这个规则的问题是它需要证明（remove ith i L t LJ），这只能用大小为O（i）的证明来证明。不太自然的表示可能会产生O（1）大小的证明，但提出这样的表示会给证明生产者带来额外的负担。如果使用自然方法，则需要额外的C++代码来生成（remove ith i L t LJ）的证明。虽然这种额外的代码可能不是一个非常沉重的负担，但希望尽量减少从决策过程中产生证明所需的额外代码量Frank Pfenning在LFM '02研讨会上指出，斯坦，巴雷特，还有迪尔35如果列表被表示为接受列表的其余部分的函数，则可以在不对用于APPend的证明规则进行编码的情况下进行附加因此，列表[a，b，c]可以表示为λr：list. （cons a（cons b（cons cr）类型为list→list的列表L1然后可以被附加到相同类型的列表L2 通过形成λr：list来键入。（L1（L2r））。然而，这种技术并不容易使提取列表的第i个一个方程的单项4椭圆LF我们现在考虑LF的扩展LFnat，它有助于使算术DP的证明的自然表示更方便。LFnat由CVC附带的一个名为dockea的工具支持。LFnat添加到LF自然数的基本类型nat和nat类型的数字。有也可以是子范围类型[l.. [2019 - 05 - 19][2019 - 05]这使得可以将n个元素的列表建模为domain [1.]的函数。n]。加减法的基本算术运算是方便的加法，以及算术不等式。如果我们允许算术运算符对nat的超类型实数进行运算，我们就可以添加乘法和除法。然后，我们可以要求子范围类型构造函数接受实数（并且可能表示该范围中的NAT集合），或者强制子范围类型只能从NAT构建。正如下面所提到的，LFnat正在进行中，一些类似的问题尚未完全解决。LFnat还添加了一个if-then-else构造，因此像[a，b，c]这样的实际列表可以建模为λi：nat. if（i = 1）then a else if（i = 2）then b else c end end具体的语法允许将这个λ-抽象表示为[[a，b，c]]。if-then-else的保护公式必须是一个等式或nat类型的不等式。允许多类型列表也很方便。如果a：A，b：B，c：C，我们可能希望列表[[a，b，c]]的类型对应于[A，B，C]。我们可以通过使if-then-else表达式的类型也是if-then-else表达式来实现这一点if φ then M else MJend ：if φ then A else AJend，其中，φ表示M：A，而<$φ表示MJ：AJ。[[a，b，c]]的类型是：i：nat。if（i = 1）then A else if（i = 2）then B else C end end.Cuberea的具体语法允许将这种抽象表示为{{A，B，C}}。4.1元理论LFnat的研究正在进行中。 仅仅给出系统的正式描述是相当复杂的。依赖谓词逻辑系统斯坦，巴雷特，还有迪尔36(DPL)[8]的方法，它在依赖类型理论之上添加了谓词逻辑，可以作为一个起点。困难可能会出现，因为在DPL中，序列的形式是这样的，不允许分类X：Y依赖于逻辑假设。这可能使得为if-then-else制定合适的规则变得困难。一个更基本的问题，仍然不清楚的是处理的函数的类型，被宣布为有一个类型，这是一个适当的子类型;特别是，如何使处理的类型遵循建议的二价逻辑的部分条款[3，6，5]。有一件事是众所周知的，就是仅仅将类型nat和子范围类型添加到LF中就使得类型检查通常是不可判定的。这个结果可以通过将单词问题简化为LFnat中的可键入性来证明。的关键我们的想法是，通过声明某些类型被占用，我们可以添加一个逻辑假设形式为natx：nat.t=tJ，其中t和tJ由x和nat→nat类型的函数符号构建。我们只是添加类型声明：g1：水溶性：天然[t.. tJ]。g2：水溶性：天然[tJ.. t]。唯一的方法是：nat。[t.. [J]和Na2SO4：Na2SO4。[tJ..两者都可以居住，如果nat.t=tJ.添加这种形式的逻辑假设是将文字问题简化为可键入性的关键步骤。4.2从CVC检查证明的后果由于LFnat是不可判定的，因此使用它作为检查CVC证明但不可判定性并不那么严重在这个特殊的情况下，由于下面的原因，人们可能会预料到这个问题假设在某个表达式E中，nat类型的对象（包括绑定变量）只有numerals或[n..m]，对于数字n和m。 假设所有声明的函数符号的类型都是这样的，即没有nat类型的项可以通过应用从这些函数符号中形成。然后，类型检查可以只使用常量算术表达式的求值来决定，并可能尝试像[3.]这样的有限类型的所有值。5]。当一个被声明为具有这样一个有限类型的绑定变量被添加到上下文中时，使用后者，这是通过通常的（lam）规则来分类lambda抽象。与CVC的证明规则相对应的类型声明将不会总是满足这些条件，使得LF中的类型检查是可判定的。但是证明系统被设计成使得CVC为有效公式产生的每个实际证明对象都将。这意味着，虽然可能不可能为了检查CVC的证明规则的编码类型这对CVC的目的来说已经足够了斯坦，巴雷特，还有迪尔37--5在LFnat中表示算术证明本节介绍了第2节中描述的算术DP所使用的证明规则的编码所使用的语法是BASEEA的语法，它以上一节中提到的方式扩展了BASEIF的语法重点是代表每一步的推理执行的DP在尽可能直接的方式，使用LF自然的功能。从一个更简单的不考虑公理集我们从一些标准声明开始这是用来表示算术的。sort：类型。trm：sort->type。布尔恩：算是吧。o =（trm布尔）。等式：S：sort（trm S）->（trm S）-> o. TRUE：o.：o.像往常一样，定理F的证明将被表示为类型（pf F）的对象：pf： o -> type。现在我们转向算术DP的推理表示我们首先表示语言的术语和原子公式不等式被省略，因为我们只考虑规范器和求解器的规则。PLUS被声明为接受一个自然数n和一个包含n个REAL项的列表，其中该列表被建模为[1.]中的函数。n]到（trm REAL）：REAL：sort.加：{n：nat}（[1.. n]-> trm REAL）-> trmREAL。MULT：trm REAL-> trm REAL-> trmREAL。除法：trmREAL-> trm REAL-> trm REAL。UMINUS：trm REAL-> trm REAL。我们将实数s作为REAL项嵌入，并为多项式添加一个缩写（+c（c1t1）... （cntn）），其中c，c1，. ，c，n是实数s的（嵌入），并且t1，. n是真实的。为了CVC中实际的证明-产生代码的好处，如果我们可以将这个缩写与有序对列表（ci，ti）一起使用，那会很方便。 的类型{{real，（trmREAL）}}是用于这些对的类型（对于“斯坦，巴雷特，还有迪尔38第4节（见上文）。n2I：nat->（trm REAL）.CPLUS=[n：nat][C： nat][c： [1.. n]->{{ real，（trmREAL）}}]（PLUS（n+1）[i：[1.. n+1]]如果i==1，则（n2I C）否则MULT（n2 I（c（i-1）1））（c（i-1）2）结束）。因此，（+5（5<$x）（5<$y））的表示可以写为：（C +2 5[5，x]]，[[5，y]），其归一化为：(PLUS 3 [[（n2I 5），（MULT（n2I 5）x），（MULT（n2I 5）y）]]）。图2.1.1中的重写规则用于简化一元减的应用，表示如下（[x：A]M是λx：A.M的语法）：arithcanon uminus：{n：nat}{C：nat}{c：[1.. {{real，（trmREAL）}}（pf（EQ REAL（UMINUS（CPLUS n Cc））（CPLUS n（-C）[i：[1.. n] ][[（-（ci 1）），（ci 2）]]）。请注意，使用了LFnat的内置一元减操作结果是多项式用模常数算术表示因此，具有相同值的常数算术项在LFnat中具有相等的表示。该规则的一个示例应用是：（arithcanon uminus 2 4[1，c]] [[-1，d]），它有类型（pf（EQ REAL（UMINUS（PLUS 3[[（n2I 4），（MULT（n2I 1）c），(MULT（n2I-1）d）]]）（加3[[（n2I-4），（MULT（n2I-1）c），(MULT（n2I 1）d）]]）由求解器执行的一个推断是：给定方程t= 0，其中t是规范形式的多项式，其第j个斯坦，巴雷特，还有迪尔39∗方程式 这一推论表示如下：隔离变量：{n：nat} {C：nat} {c：[1.. {{real，trm REAL}}{j：[1.. n]} {D：real} {x：trmREAL}（pf（EQ布尔(EQ REAL（CPLUS n C[i：[1.. n] ] ifi==jthen [[D，x]]else（ci） end）(n2I0））（EQREAL x（UMINUS（DIVIDE（C+（n - 1） C[i：[1..（n - 1）]]if i jthen（c i）else（c（i+1））end）<(n2I（D））。注意if-then-else是如何首先用来表示第j个非常数mono- mial是Dx，然后说在x被孤立的方程中，右边的和跳过了还要注意，当n等于0时，规则不能完全应用，因为将不存在类型为[1.的j。0]，因为该类型为空。这是假设类型上下文是一致的，在这个意义上，它没有声明空类型被占用。作为最后一个例子，我们在对多项式的项进行排序从工程的角度来看，用一个排序例程来产生一个证明是非常不可取的然而，在不对排序例程进行任何修改的情况下，我们可以使用辅助数据结构来恢复与未排序和排序列表相关的排列然后我们可以给出一个规则，它说将置换p应用于被加数的列表c会产生相等的和。除了置换p之外，该规则还接受p然后，它需要证明dp与ip组成的p是恒等式。这保证了p确实是一个置换（并且ip确实是它的逆置换）。规则说dp必须是复合类型==identity; degree允许将==用作类型。 然后检查一下，根据定义的等式，这两个表达式实际上相等LFnat。Rodeea要求提供一个占位符参数排序和数：{n：nat}{c：[1.. n] -> trmREAL}{p：[1.. n] ->[1..n]}{ip：[1.. n] ->[1..n]}{dp：（（[i：[1.. n]]（ip（p i）==（[i：[1.. （i））}（pf（EQ REAL(PLUS（c）(PLUS n [k：[1.. n] ] c（p k）。斯坦，巴雷特，还有迪尔40此规则的示例应用（假设a、b和c为（trm REAL）类型）是（sortsummands 3[[a，b，c]][[3，1，2]][[2，3，1]]**），这是一种（pf（EQ REAL(PLUS 3[[ a，b， c]]）(PLUS 3 [[ c，a，b]）。6结论描述了CVC的线性实数运算证明生成决策过程中的规范器和求解器所作的证明，在LFnat中发送，LF的扩展，包括数字，子范围类型，算术运算和if-then-else。LFnat使得在CVC中对这个和其他决策过程中的推理建模比在纯LF中更方便如果要获得LF自然的元理论的严格理解，还有很多工作要做即使LFnat是一般不可判定的，它仍然可以正确地检查CVC产生的证明Arity-Polymorphic证明规则可以CVC声称的所有有效公式的实际证明都可以检查。CVC使用的证明规则可能属于LFnat的可判定片段，但这还有待观察。这项工作得到了ARPA/空军合同F33615-00-C的支持1693和NSF合同CCR-9806889。引用[1] A. Appel和E.费尔滕携带证明的身份验证。第六届ACM计算机与通信安全，1999年。[2] C. Barrett，D. Dill，和A.树桩通过增量翻译到SAT来检查一阶公式的可满足性2002年第14届计算机辅助验证国际[3] M.比森建构数学基础：元数学研究。Springer，1985年。[4] S. Berghouth和T.尼普科单类型高阶逻辑的证明项. 在高阶逻辑中的定理证明，第13届国际会议，LNCS的第1869卷，2000年。[5] W. Farmer和J.古特曼一个支持部分函数的集合论Logica Studia，66（1）：59[6] S.费弗曼定义。Erkenntnis，43：295斯坦，巴雷特，还有迪尔41[7] R. Harper ， F. Honsell 和 G. 普 洛 特 金 定 义 逻 辑 的 框 架 。 Journal of theAssociation for Computing Machinery，40（1）：143-184，January 1993.[8] B.雅各布斯 范畴逻辑和类型理论。 Elsevier，1999年。[9] G. Necula携 带 证 明 代 码 。 第 24 届 ACM SIGPLAN-SIGACT Symposium onPrinciples of Programming Languages，第106-119页，1997年1月。[10] F.芬宁逻辑框架，第二十一章。在Robinson和Voronkov [12]，2001年。[11] F. Pfen nninganddCarstenSchürmann. 系统演绎：演绎系统的两个逻辑框架.1999年第16届国际自动演绎会议[12] A. Robinson和A.沃龙科夫，编辑。自动推理手册Elsevier and MIT Press，2001.[13] A. 施通普角Barrett和D.迪尔CVC：一种合作有效性模型。在2002年第14届计算机辅助验证国际会议[14] W.黄。通过证明检查验证HOL证明。系统设计中的形式化方法，14（2）：193