# Proving Hypersafety Compositionally

# 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.