Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Alejandro Aguirre, Philipp G. Haselwarter, Markus de Medeiros, Kwing Hei Li, Simon Oddershede Gregersen, Joseph Tassarotti, Lars Birkedal

TL;DR

Eris introduces a novel resource-based approach to probabilistic reasoning for higher-order programs by treating error bounds as first-class credits within a separation-logic framework. This enables modular, value-dependent, and expectation-preserving composition of error bounds, as well as amortized analysis for data structures and almost-sure termination through a total-correctness variant Eris$_t$. The framework is demonstrated through extensive case studies (hashing, Merkle trees, rejection sampling) and is mechanized in Coq using Iris, demonstrating practical applicability and rigorous soundness. The work advances the verification of Monte Carlo and Las Vegas algorithms by delivering precise, compositional bounds and a pathway to AST results in richer languages. It also opens avenues for extending error-credit reasoning to concurrency, concentration bounds, and relational/privacy settings.

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.

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

TL;DR

Eris introduces a novel resource-based approach to probabilistic reasoning for higher-order programs by treating error bounds as first-class credits within a separation-logic framework. This enables modular, value-dependent, and expectation-preserving composition of error bounds, as well as amortized analysis for data structures and almost-sure termination through a total-correctness variant Eris. The framework is demonstrated through extensive case studies (hashing, Merkle trees, rejection sampling) and is mechanized in Coq using Iris, demonstrating practical applicability and rigorous soundness. The work advances the verification of Monte Carlo and Las Vegas algorithms by delivering precise, compositional bounds and a pathway to AST results in richer languages. It also opens avenues for extending error-credit reasoning to concurrency, concentration bounds, and relational/privacy settings.

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.
Paper Structure (54 sections, 6 theorems, 78 equations, 4 figures)

This paper contains 54 sections, 6 theorems, 78 equations, 4 figures.

Table of Contents

  1. Introduction
  2. Modular specifications of higher-order programs
  3. More precise error bounds via expectation-preserving composition
  4. Amortized error bounds
  5. Almost-sure termination using error credits
  6. Contributions
  7. Outline
  8. Preliminaries and the Language $\mathbf{\uplambda}_{\textnormal{ref}}^{\textnormal{rand}}$
  9. Probabilities and Programs
  10. Language Definition and Operational Semantics
  11. The Eris Logic
  12. Proof rules for sampling
  13. Example
  14. Case Studies
  15. Dynamic Vectors under a Faulty Allocator
  16. ...and 39 more sections

Key Result

Lemma 3

Let $\mu \in \mathcal{D}(X)$, $x \in X$, and $f : X \to \mathcal{D}(Y)$. Then gives a monadic structure to $\mathcal{D}$. We write $\mu \mathbin{ \raisebox{0.3ex}{$\gg\mkern-6mu=$} } f$ for $\mathop{\mathrm{bind}}\nolimits(f, \mu)$.

Figures (4)

  • Figure 1: Expected error analysis, partial and total.
  • Figure 2: A proof checker for Merkle trees.
  • Figure 3: Partial and total approximate correctness contrasted.
  • Figure 4: A sampler and checker implementing a simplified version of WalkSAT.

Theorems & Definitions (10)

  • Definition 1: Mass
  • Definition 2: Subdistribution
  • Lemma 3: Probability Monad
  • Definition 4: Restriction
  • Definition 5: Probability of a Predicate
  • Theorem 6: Adequacy
  • Theorem 7: Total Adequacy
  • Theorem 8: Almost-Sure Termination
  • Theorem 9: Limit WP adequacy
  • Lemma 10