Approximate Relational Reasoning for Higher-Order Probabilistic Programs

TL;DR

This paper introduces Approxis, a higher-order relational logic for probabilistic programs, enabling reasoning about approximate equivalences with modularity, compositionality, and formal verification in Coq.

Contribution

The paper develops a novel higher-order relational separation logic, Approxis, for probabilistic programs, extending existing logics to handle higher-order functions, state, and approximation.

Findings

Successfully applied to cryptographic security proofs.

Mechanized proofs in Coq and Iris.

Handles complex probabilistic reasoning with modular rules.

Abstract

Properties such as provable security and correctness for randomized programs are naturally expressed relationally as approximate equivalences. As a result, a number of relational program logics have been developed to reason about such approximate equivalences of probabilistic programs. However, existing approximate relational logics are mostly restricted to first-order programs without general state. In this paper we develop Approxis, a higher-order approximate relational separation logic for reasoning about approximate equivalence of programs written in an expressive ML-like language with discrete probabilistic sampling, higher-order functions, and higher-order state. The Approxis logic recasts the concept of error credits in the relational setting to reason about relational approximation, which allows for expressive notions of modularity and composition, a range of new approximate relational rules, and an internalization of a standard limiting argument for showing exact probabilistic equivalences by approximation. We also use Approxis to develop a logical relation model that quantifies over error credits, which can be used to prove exact contextual equivalence. We demonstrate the flexibility of our approach on a range of examples, including the PRP/PRF switching lemma, IND\$-CPA security of an encryption scheme, and a collection of rejection samplers. All of the results have been mechanized in the Coq proof assistant and the Iris separation logic framework.