Forall-Exists Relational Verification by Filtering to Forall-Forall

Abstract

Relational verification encompasses reasoning about data abstraction, security and privacy, secure compilation, and functional specification of tensor programs, among others. Several relational logics and tools support compositional reasoning about $\forall \forall$ (2-safety) properties and, generally, $k$-safety properties. In contrast, few logics and tools exist for reasoning about $\forall \exists$ properties which are critical in the presence of nondeterminism. This paper's primary contribution is a technique for verifying a $\forall \exists$ judgment by way of a novel transformation. The filter-adequacy 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 bicoms, a form of product programs that facilitates expressing good alignments and caters for direct translation of $\forall \forall$ properties to unary correctness; proves that successful $\forall \forall$ verification of a transformed bicom implies the $\forall \exists$ spec for its underlying unary commands; and evaluates the technique using a prototype auto-active relational verifier. The technique enables users to work with ordinary assertions and assumptions, and a standard assertion language, so that existing $\forall \forall$ and unary verification tools can be used for $\forall \exists$.

arXiv commentv2: expanded evaluation section; expository improvements throughout; v3: add missing author in metadata