Probabilistic programs often trade accuracy for efficiency, and are thus only approximately correct. It is important to obtain precise error bounds for these approximations, but existing approaches rely on simplifications that make the error bounds excesively coarse, or only apply to first-order programs. In this paper we present Eris, a higher-order separation logic for probabilistic programs written in an expressive higher-order language.

Our key novely is the introduction of error credits, a separation logic resource that tracks the error bound of our program. By representing error bounds as a resource, we recover all of the benefits of separation logic, including composability, modularity and interdependency between errors and program terms, which allows for more precise specifications. Moreover, we enable novel reasoning principles such as expectation-preserving error composition, amortized error reasoning, and reasoning about almost-sure termination by induction on the error credits.

We illustrate the advantages of our approach by proving amortized error bounds on a range of examples, including collision probabilities in hash functions, which allows us to write more modular specifications for data structures that use them as clients. We also use our logic to prove correctness and almost-sure termination of rejection sampling algorithms. All of our results have been mechanized using Coq, Iris and the Coquelicot real analysis library.