Proving Hypersafety Compositionally

TL;DR

This paper introduces a new proof principle and logic for hypersafety properties, enabling more compositional and modular proofs of complex relational program properties like determinism and associativity.

Contribution

It proposes a novel proof principle that treats hyper-triples as a unifying compositional element, leading to the development of the Logic for Hyper-triple Composition (LHC).

Findings

LHC is sound and effective for complex hypersafety proofs

Enables proof compositionality not possible with previous logics

Applied successfully to challenging hypersafety examples

Abstract

Hypersafety properties of arity $n$ are program properties that relate $n$ traces of a program (or, more generally, traces of $n$ programs). Classic examples include determinism, idempotence, and associativity. A number of relational program logics have been introduced to target this class of properties. Their aim is to construct simpler proofs by capitalizing on structural similarities between the $n$ related programs. We propose an unexplored, complementary proof principle that establishes hyper-triples (i.e. hypersafety judgments) as a unifying compositional building block for proofs, and we use it to develop a Logic for Hyper-triple Composition (LHC), which supports forms of proof compositionality that were not achievable in previous logics. We prove LHC sound and apply it to a number of challenging examples.