Cyclic Proofs in Hoare Logic and its Reverse

1. Problem Statement

The paper addresses the challenge of automating the verification of computer programs, specifically focusing on the difficulties associated with loop invariants and termination measures.

• Standard Hoare Logic: Traditional axiomatic proof systems for Hoare logic (both partial and total correctness) require the user to manually supply a loop invariant (for partial correctness) and a well-founded termination measure (for total correctness). This requirement is a significant bottleneck for automated proof search.
• Reverse Hoare Logic: Similarly, the dual notion of Reverse Hoare Logic (RHL), used for specifying the presence of behaviors (reachability) or proving the existence of bugs (incorrectness logic), faces analogous challenges in its axiomatic formulation.
• The Gap: While cyclic proof systems (which replace explicit invariants with global soundness conditions on infinite derivation trees) have been applied to various logics, a unified treatment of cyclic proofs for both Partial/Total Hoare Logic and their Reverse/Incorrectness counterparts was lacking. The paper aims to establish these systems, demonstrate their soundness and relative completeness, and clarify the semantic and proof-theoretic symmetries between them.

2. Methodology

The authors employ a formal proof-theoretic approach, defining syntax, semantics, and proof systems for a simple while-language.

A. Semantic Framework

• Language: A standard imperative language with skip, assignment, sequencing, conditionals, and while loops.
• Semantics: Defined via small-step operational semantics.
• Logics Defined:
  1. PHL (Partial Hoare Logic): $\{P\} C \{Q\}$ holds if all terminating executions starting in $P$ end in $Q$.
  2. THL (Total Hoare Logic): $\{P\} C \{Q\}$ holds if all executions starting in $P$ terminate and end in $Q$.
  3. PRHL (Partial Reverse Hoare Logic): $[P] C [Q]$ holds if for every state in $Q$, there exists a starting state in $P$ that reaches it (allowing divergence).
  4. TRHL (Total Reverse Hoare Logic): $[P] C [Q]$ holds if for every state in $Q$, there exists a terminating execution from a state in $P$ reaching it.

B. Axiomatic Systems

The paper first reviews standard axiomatic systems where loop rules require explicit invariants ($Inv$) and termination measures ($Inv\text{-}Total$).

C. Cyclic Proof Systems

The core methodology involves replacing the explicit invariant rules with cyclic proof rules:

• Continuation Style: Rules are formulated in a continuation style (e.g., $\{P\} C; C' \{Q\}$) to facilitate the handling of backlinks.
• Loop Unfolding: The while loop rule ($CInv$) simply unrolls the loop once, creating a "bud" (open leaf) that links back to a "companion" node.
• Global Soundness Conditions: To ensure the cyclic proofs are valid, the paper defines global conditions on infinite paths in the derivation tree:
  • For Partial Logic (PHL/PRHL): Every infinite path must contain infinitely many symbolic execution steps. This ensures that any counterexample would require an infinite execution, which contradicts the definition of a finite counterexample.
  • For Total Logic (THL/TRHL): Every infinite path must contain an infinitely progressing trace of well-founded measures (e.g., natural numbers) that strictly decrease infinitely often. This ensures that any counterexample would require an infinite descending chain of natural numbers, which is impossible.

3. Key Contributions

1. Unified Cyclic Systems: The authors present the first cyclic proof systems for both Partial/Total Reverse Hoare Logic and their standard Hoare counterparts.
2. Symmetry and Duality: The paper explicitly maps the dual relationships:
   • PHL and TRHL are semantic duals.
   • THL and PRHL are semantic duals.
   • The cyclic soundness conditions for partial logics are coinductive (requiring infinite progress of execution), while those for total logics are inductive (requiring infinite descent of measures).
3. Soundness Proofs: Direct arguments are provided showing that if a cyclic proof exists, the triple is valid. The proofs rely on constructing counter-examples (infinite paths) and showing they lead to contradictions (infinite execution or infinite descent).
4. Relative Completeness: The paper proves that any valid triple provable in the standard axiomatic system is also provable in the cyclic system. This is achieved via an explicit translation algorithm that transforms standard derivation trees (with invariants) into cyclic pre-proofs (with backlinks).
5. Novelty in Reverse Logic: The paper introduces and formalizes Partial Reverse Hoare Logic (PRHL), a variant that admits program divergence, which appears to be a new or under-explored variant in the literature.

4. Results

• Soundness Theorems: Theorem 4.7 (for Hoare Logic) and Theorem 5.5 (for Reverse Hoare Logic) establish that cyclic provability implies semantic validity for both partial and total variants.
• Completeness Theorems: Theorem 4.9 and Theorem 5.7 establish relative completeness. Specifically, if a triple is valid (and thus provable in the axiomatic system assuming an oracle for logical entailment), a cyclic proof can be constructed.
• Translation Mechanism: The paper provides a constructive method (Lemma 4.8 and Lemma 5.6) to convert standard proofs into cyclic proofs. For example, the standard loop invariant rule is transformed into a cyclic rule where the invariant is implicitly maintained by the backlink structure and the global soundness condition.

5. Significance

• Automation Potential: By removing the need for users to manually supply loop invariants and termination measures, cyclic proof systems pave the way for more automated program verification tools. The "global soundness" check can potentially be automated (e.g., using tools like the Cyclist theorem prover).
• Theoretical Unification: The paper clarifies the deep structural similarities between Hoare logic and Reverse Hoare logic. It demonstrates that the distinction between partial and total correctness is primarily a matter of the global soundness condition applied to the same underlying cyclic proof rules, rather than a fundamental difference in the proof rules themselves.
• Foundation for Incorrectness Logic: Since Reverse Hoare Logic is the basis for Incorrectness Logic (used for bug finding), this work provides a rigorous cyclic proof foundation for automated bug detection, potentially allowing tools to prove the existence of bugs without manual annotation.
• Clarification of Duality: The work highlights that the "dual" nature of these logics is not just semantic but extends to their proof-theoretic structures, offering a cohesive view of program verification (proving absence of errors) and program analysis (proving presence of behaviors).

In summary, the paper successfully bridges the gap between axiomatic and cyclic proof systems for a comprehensive set of program logics, demonstrating that cyclic proofs offer a sound, relatively complete, and structurally elegant alternative to traditional invariant-based verification.