We introduce eRHL, a program logic for reasoning about relational expectation properties of pairs of probabilistic programs. eRHL is quantitative, i.e., its pre- and post-conditions take values in the extended non-negative reals. Thanks to its quantitative assertions, eRHL overcomes randomness alignment restrictions from prior logics, including PRHL, a popular relational program logic used to reason about security of cryptographic constructions, and apRHL, a variant of PRHL for differential privacy. As a result, eRHL is the first relational probabilistic program logic to be supported by non-trivial soundness and completeness results for all almost surely terminating programs. We show that eRHL is sound and complete with respect to program equivalence, statistical distance, and differential privacy. We also show that every PRHL judgment is valid iff it is provable in eRHL. We showcase the practical benefits of eRHL with examples that are beyond reach of PRHL and apRHL.

翻译：我们介绍了eRHL，一种用于推理概率程序对之间关系期望性质的程序逻辑。eRHL是定量的，即其前置条件和后置条件取值于扩展的非负实数。得益于其定量断言，eRHL克服了先前逻辑中的随机性对齐限制，这些逻辑包括PRHL（一种常用于推理密码构造安全性的流行关系程序逻辑）以及apRHL（PRHL的一个用于差分隐私的变体）。因此，eRHL是首个对所有几乎必然终止程序具有非平凡可靠性和完备性结果支持的关系概率程序逻辑。我们证明eRHL在程序等价性、统计距离和差分隐私方面是可靠且完备的。我们还证明了每个PRHL判断是有效的，当且仅当它可以在eRHL中被证明。我们通过一些超出PRHL和apRHL能力范围的示例，展示了eRHL的实际优势。