Alignment complete relational Hoare logics for some and all

from arxiv, Vsn2 fixes a def, adds semantic completeness for filtered automata and Cook completeness for all-exists logic; Vsn3 adds section on entailment completeness and additional proof rules; Vsn4 makes minor changes in exposition; Vsn5 makes minor changes in exposition, expands discussion of Cook completeness and control determinacy, and expands a key example. arXiv admin note: text overlap with arXiv:2212.10338

In relational verification, judicious alignment of computational steps facilitates proof of relations between programs using simple relational assertions. Relational Hoare logics (RHL) provide compositional rules that embody various alignments of executions. Seemingly more flexible alignments can be expressed in terms of product automata based on program transition relations. A single degenerate alignment rule (self-composition), atop a complete Hoare logic, comprises a RHL for $\forall\forall$ properties that is complete in the ordinary logical sense (Cook'78). The notion of alignment completeness was previously proposed as a more satisfactory measure, and some rules were shown to be alignment complete with respect to a few ad hoc forms of alignment automata. This paper proves alignment completeness with respect to a general class of $\forall\forall$ alignment automata, for a RHL comprised of standard rules together with a rule of semantics-preserving rewrites based on Kleene algebra with tests. A new logic for $\forall\exists$ properties is introduced and shown to be alignment complete. The $\forall\forall$ and $\forall\exists$ automata are shown to be semantically complete. Thus the logics are both complete in the ordinary sense. Recent work by D'Osualdo et al highlights the importance of completeness relative to assumptions (which we term entailment completeness), and presents $\forall\forall$ examples seemingly beyond the scope of RHLs. Additional rules enable these examples to be proved in our RHL, shedding light on the open problem of entailment completeness.

翻译：在关系验证中，计算步骤的明智对齐有助于使用简单的关系断言证明程序间的关系。关系霍尔逻辑（RHL）提供了体现不同执行对齐方式的组合规则。表面上更灵活的对齐可以通过基于程序转移关系的乘积自动机来表达。在完备的霍尔逻辑之上，单个退化对齐规则（自组合）构成了一个在普通逻辑意义下完备的（Cook'78）用于$\forall\forall$属性的RHL。对齐完备性的概念先前被提出作为一个更令人满意的度量标准，并且一些规则被证明相对于几种特定形式的对齐自动机是对齐完备的。本文证明了一个由标准规则以及基于带测试的Kleene代数的语义保持重写规则组成的RHL，相对于一类通用的$\forall\forall$对齐自动机是对齐完备的。本文引入了一个新的用于$\forall\exists$属性的逻辑，并证明其是对齐完备的。$\forall\forall$和$\forall\exists$自动机被证明是语义完备的。因此，这些逻辑在普通意义上都是完备的。D'Osualdo等人的近期工作强调了相对于假设的完备性的重要性（我们称之为蕴涵完备性），并提出了看似超出RHLs范围的$\forall\forall$示例。额外的规则使得这些示例能够在我们的RHL中得到证明，从而为蕴涵完备性这一开放问题提供了启示。