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 forallforall (2-safety) properties and, generally, k-safety properties of product programs. In contrast, few logics and tools exist for reasoning about forallexists properties which are critical in the context of nondeterminism. This paper's primary contribution is a methodology for verifying a forallexists judgment by way of a novel filter-adequacy transformation. This transformation adds assertions to a product program in such a way that the desired forallexists property (of a pair of underlying unary programs) is implied by a forallforall property of the transformed product. The paper develops a program logic for the basic forallexists judgement extended with assertion failures; develops bicoms, a form of product programs that represents pairs of executions and that caters for direct translation of forallforall properties to unary correctness; proves (using the logic) a soundness theorem that says successful forallforall verification of a transformed bicom implies the forallexists 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.