An Iris for Expected Cost Analysis

TL;DR

ExpIris is a flexible separation logic framework that enables rigorous expected cost analysis of probabilistic programs, supporting complex language features and correctness reasoning.

Contribution

It introduces ExpIris, a novel extension of Iris for expected cost analysis using the expected potential method, applicable to various programming paradigms.

Findings

Verified expected runtime of quicksort implementation

Analyzed amortized expected runtime of probabilistic binary counter

Demonstrated applicability to imperative, functional, and concurrent programs

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.