Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs

TL;DR

Eris introduces a higher-order separation logic with error credits to precisely bound error probabilities in probabilistic programs, enabling modular, compositional reasoning for complex error bounds.

Contribution

The paper presents Eris, a novel higher-order separation logic that uses error credits to improve error bound precision and reasoning capabilities in probabilistic program verification.

Findings

Proved amortized error bounds for hash collision probabilities

Verified correctness and almost-sure termination of rejection sampling algorithms

Mechanized proofs in Coq using Iris and Coquelicot libraries

Abstract

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.