Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Alignment complete relational Hoare logics for some and all

Ramana Nagasamudram, Anindya Banerjee, David A. Naumann

TL;DR

The paper tackles relational verification by formalizing alignment-based proofs for both ∀∀ and ∀∃ properties. It introduces RHL+ (a Kleene algebra with tests (KAT)-based rewrite-enabled relational logic) and proves alignment completeness for a broad class of ∀∀ alignment automata, culminating in Cook completeness. It further extends the framework with ERHL+ to handle ∀∃ properties via filtered alignment automata, achieving alignment and Cook completeness in that setting as well. The approach shows that automata-based alignment and deductive proof systems can simulate each other with a minimal core of rules, highlighting the fundamental role of rewriting and alignment in relational verification. The work also discusses entailment completeness and outlines future directions toward richer languages, modular reasoning, and automated tooling.

Abstract

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 (sequential composition), atop a complete Hoare logic, comprises a RHL for $\forall\forall$ properties that is complete in the sense of Cook. The notion of alignment completeness was previously proposed as an additional 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 sound and alignment complete for a new general class of automata. The $\forall\forall$ and $\forall\exists$ automata are shown to be semantically complete. Thus both logics are complete in the sense of Cook. The paper includes discussion of why alignment is not the only important principle for relational reasoning and proposes entailment completeness as further means to evaluate RHLs.

Alignment complete relational Hoare logics for some and all

TL;DR

The paper tackles relational verification by formalizing alignment-based proofs for both ∀∀ and ∀∃ properties. It introduces RHL+ (a Kleene algebra with tests (KAT)-based rewrite-enabled relational logic) and proves alignment completeness for a broad class of ∀∀ alignment automata, culminating in Cook completeness. It further extends the framework with ERHL+ to handle ∀∃ properties via filtered alignment automata, achieving alignment and Cook completeness in that setting as well. The approach shows that automata-based alignment and deductive proof systems can simulate each other with a minimal core of rules, highlighting the fundamental role of rewriting and alignment in relational verification. The work also discusses entailment completeness and outlines future directions toward richer languages, modular reasoning, and automated tooling.

Abstract

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 (sequential composition), atop a complete Hoare logic, comprises a RHL for properties that is complete in the sense of Cook. The notion of alignment completeness was previously proposed as an additional 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 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 properties is introduced and shown to be sound and alignment complete for a new general class of automata. The and automata are shown to be semantically complete. Thus both logics are complete in the sense of Cook. The paper includes discussion of why alignment is not the only important principle for relational reasoning and proposes entailment completeness as further means to evaluate RHLs.
Paper Structure (52 sections, 41 theorems, 99 equations, 24 figures)

This paper contains 52 sections, 41 theorems, 99 equations, 24 figures.

Table of Contents

  1. Introduction
  2. Outline.
  3. Overview
  4. Rewriting facilitates expression of alignment.
  5. Nondeterminacy and $\forall\exists$ judgments.
  6. Possibilistic Noninterference.
  7. On heuristics
  8. Data dependent alignment
  9. Alignment completeness.
  10. The programming language and its ∀∀ relational Hoare logic
  11. Guarded command language
  12. Program logic.
  13. Relational specs and proof rules.
  14. Alignment automata, adequacy, and verification conditions
  15. Automata, alignment automata and adequacy
  16. ...and 37 more sections

Key Result

Lemma 4.4

If alignment automaton $\prod(A,A',L,R,J)$ is manifestly $\mathcal{P}$-adequate then it is $\mathcal{P}$-adequate (in the sense of def:adequacy).

Figures (24)

  • Figure 1: Proof rules of HL+.
  • Figure 2: The rules of RHL+.
  • Figure 3: Some derived rules of RHL+.
  • Figure 4: Transition semantics (with $n$ and $v$ ranging over $\mathbb{Z}$).
  • Figure 5: Following successor $\hbox{\upshapefsuc}(n,c,f)$, assuming $\hbox{\upshapeok}(c)$, $n\in\hbox{\upshapelabs}(c)$, and $f\notin\hbox{\upshapelabs}(c)$.
  • ...and 19 more figures

Theorems & Definitions (90)

  • Definition 3.1
  • Example 3.2
  • Definition 4.1
  • Definition 4.2
  • Definition 4.3
  • Lemma 4.4
  • Lemma 4.5: adequacy semantically sound and complete
  • Lemma 4.6: semantic soundness and completeness of IAM Floyd67
  • Corollary 4.7: soundness of alignment automata
  • Corollary 4.8: semantic completeness of alignment automata
  • ...and 80 more