Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

An Iris for Expected Cost Analysis

Janine Lohse, Deepak Garg

TL;DR

ExpIris extends the Iris separation-logic framework to enable modular, correctness-grounded amortized and expected-cost analysis of probabilistic programs. It does so by integrating the expected-potential method into a probabilistic weakest precondition, parameterized by initial and postcondition potentials, and by instantiating a ProbHeapLang with real-valued costs and probabilistic primitives. The approach is demonstrated through two case studies—the probabilistic binary counter and randomized quicksort—providing explicit bounds on expected costs and illustrating the mechanics of potential distribution across probabilistic branches. The work offers a mechanized Coq formalization and an adequacy theorem connecting proofs to execution behavior, while outlining current limitations and directions for embedding probabilistic resources directly in the logic to broaden applicability and expressivity.

Abstract

We present ExpIris, a separation logic framework for the (amortized) expected cost analysis of probabilistic programs. ExpIris is based on Iris, parametric in the language and the cost model, and supports both imperative and functional languages, concurrency, higher-order functions and higher-order state. ExpIris also offers strong support for correctness reasoning, which greatly eases the analysis of programs whose expected cost depends on their high-level behavior. To enable expected cost reasoning in Iris, we build on the expected potential method. The method provides a kind of "currency" that can be used for paying for later operations, and can be distributed over the probabilistic cases whenever there is a probabilistic choice, preserving the expected value due to the linearity of expectations. We demonstrate ExpIris by verifying the expected runtime of a quicksort implementation and the amortized expected runtime of a probabilistic binary counter.

An Iris for Expected Cost Analysis

TL;DR

ExpIris extends the Iris separation-logic framework to enable modular, correctness-grounded amortized and expected-cost analysis of probabilistic programs. It does so by integrating the expected-potential method into a probabilistic weakest precondition, parameterized by initial and postcondition potentials, and by instantiating a ProbHeapLang with real-valued costs and probabilistic primitives. The approach is demonstrated through two case studies—the probabilistic binary counter and randomized quicksort—providing explicit bounds on expected costs and illustrating the mechanics of potential distribution across probabilistic branches. The work offers a mechanized Coq formalization and an adequacy theorem connecting proofs to execution behavior, while outlining current limitations and directions for embedding probabilistic resources directly in the logic to broaden applicability and expressivity.

Abstract

We present ExpIris, a separation logic framework for the (amortized) expected cost analysis of probabilistic programs. ExpIris is based on Iris, parametric in the language and the cost model, and supports both imperative and functional languages, concurrency, higher-order functions and higher-order state. ExpIris also offers strong support for correctness reasoning, which greatly eases the analysis of programs whose expected cost depends on their high-level behavior. To enable expected cost reasoning in Iris, we build on the expected potential method. The method provides a kind of "currency" that can be used for paying for later operations, and can be distributed over the probabilistic cases whenever there is a probabilistic choice, preserving the expected value due to the linearity of expectations. We demonstrate ExpIris by verifying the expected runtime of a quicksort implementation and the amortized expected runtime of a probabilistic binary counter.
Paper Structure (19 sections, 8 theorems, 35 equations)

This paper contains 19 sections, 8 theorems, 35 equations.

Table of Contents

  1. Introduction
  2. Example
  3. Preliminaries: The Iris Base Logic
  4. Probabilistic Language
  5. Definition
  6. Example Language: Probabilistic Heap Lang
  7. Probabilistic Weakest Precondition
  8. Recap of the Iris Weakest Precondition Definition
  9. Definition of the ExpIris Weakest Precondition
  10. Example
  11. Adequacy
  12. Case Studies
  13. Probabilistic Binary Counter
  14. Quicksort
  15. Limitations and Ongoing Work
  16. ...and 4 more sections

Key Result

Lemma 5.1

Theorems & Definitions (10)

  • Definition 3.1: Discrete distribution
  • Definition 3.2: Probabilistic Language
  • Lemma 5.1
  • Theorem 5.2: Adequacy
  • Theorem 6.1
  • Lemma 6.2
  • Theorem 6.3: Expected Number of Comparisons for Quicksort
  • Lemma 6.4: Good Pivot Split
  • Lemma 6.5: Bad Pivot Split
  • Theorem 1.B.1: Adequacy