Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic ProgramsDistinguished Paper
Probabilistic programs often trade accuracy for efficiency, and thus
may, with a small probability, return an incorrect result.
It is important to obtain precise bounds for
the probability of these errors, but existing verification approaches have limitations that
lead to error probability bounds that are excessively coarse, or only apply to first-order programs.
In this paper we present Eris, a higher-order separation logic for proving
error probability bounds for probabilistic programs written in an expressive higher-order language.
Our key novelty is the introduction of error credits, a separation logic resource
that tracks an upper bound on the probability that a program returns an erroneous result.
By representing error bounds as a resource,
we recover the benefits of separation logic, including compositionality,
modularity, and dependency between errors and program terms, allowing
for more precise specifications. Moreover, we enable novel reasoning principles
such as expectation-preserving error composition, amortized error reasoning,
and error induction.
We illustrate the advantages of our approach by proving amortized error
bounds on a range of examples, including collision probabilities
in hash functions, which allow 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
in the Coq proof assistant using the Iris separation logic framework and
the Coquelicot real analysis library.
