Forall-Exists Relational Verification by Filtering to Forall-Forall

Relational verification encompasses research directions such as reasoning about data abstraction, reasoning about security and privacy, secure compilation, and functional specificaton of tensor programs, among others. Several relational Hoare logics exist, with accompanying tool support for compositional reasoning of $\forall\forall$ (2-safety) properties and, generally, k-safety properties of product programs. In contrast, few logics and tools exist for reasoning about $\forall\exists$ properties which are critical in the context of nondeterminism. This paper's primary contribution is a methodology for verifying a $\forall\exists$ judgment by way of a novel filter-adequacy transformation. This transformation adds assertions to a product program in such a way that the desired $\forall\exists$ property (of a pair of underlying unary programs) is implied by a $\forall\forall$ property of the transformed product. The paper develops a program logic for the basic $\forall\exists$ judgement extended with assertion failures; develops bicoms, a form of product programs that represents pairs of executions and that caters for direct translation of $\forall\forall$ properties to unary correctness; proves (using the logic) a soundness theorem that says successful $\forall\forall$ verification of a transformed bicom implies the $\forall\exists$ spec for its underlying unary commands; and implements a proof of principle prototype for auto-active relational verification which has been used to verify all examples in the paper. The methodology thereby enables a user to work with ordinary assertions and assumptions, and a standard assertion language, so that existing tools including auto-active verifiers can be used.