Quantitative Weakest Hyper Pre: Unifying Correctness and Incorrectness Hyperproperties via Predicate Transformers
Linpeng Zhang, Noam Zilberstein, Benjamin Lucien Kaminski, Alexandra Silva
TL;DR
This work introduces a quantitative weakest hyper pre (whp) calculus that unifies correctness and incorrectness reasoning for hyperproperties of nondeterministic and probabilistic programs. By lifting classical weakest preconditions to hyperproperties and further to hyperquantities, the framework supports reasoning about initial sets or distributions and about quantities such as mean and variance. The authors define a weighted imperative language with semiring-based semantics, develop a quantitative strongest post and a quantitative weakest hyper pre, and establish Kozen-style dualities between forward and backward transformers. They show that whp subsumes several existing Hoare-like logics (e.g., Hyper Hoare Logic and Outcome Logic), provide healthiness properties, and demonstrate practical case studies on proving/disproving hyperproperties and performing quantitative information flow and variance analysis. The approach enables mechanized, compositional reasoning about a broad class of hyperproperties, with potential impact on security, reliability, and probabilistic programming analysis.
Abstract
We present a novel \emph{weakest pre calculus} for \emph{reasoning about quantitative hyperproperties} over \emph{nondeterministic and probabilistic} programs. Whereas existing calculi allow reasoning about the expected value that a quantity assumes after program termination from a \emph{single initial state}, we do so for \emph{initial sets of states} or \emph{initial probability distributions}. We thus (i)~obtain a weakest pre calculus for hyper Hoare logic and (ii)~enable reasoning about so-called \emph{hyperquantities} which include expected values but also quantities (e.g. variance) out of scope of previous work. As a byproduct, we obtain a novel strongest post for weighted programs that extends both existing strongest and strongest liberal post calculi. Our framework reveals novel dualities between forward and backward transformers, correctness and incorrectness, as well as nontermination and unreachability.