Logics and Examples

The Clutch project family of logics use a lifting-based approach, which re-uses the existing model of separation logic assertions from Iris, and augments these with additional resources or ghost state that is used to track aspects of the probabilistic behavior of the program. These resources are connected to the program's behavior through a custom definition of the weakest precondition or Hoare triple assertions. The lifting-based approach was pioneered in logics such as pRHL and aHL by Barthe et al. The Clutch project shows how to adapt lifting to the setting of a modern higher-order separation logic.

The benefit of this approach is that it retains the expressive features of Iris's modern separation logic framework, such as impredicative invariants and custom resource algebras. These features are useful for reasoning about complex program behaviors and language effects. The logics in the Clutch project target a range of different program specifications and properties as described in the following sections.:

Contextual Equivalence

Proving that two randomized programs are equivalent has important applications in security and cryptography, where it is common to argue that an attacker cannot distinguish between a real implementation of a program and an ideal version that is perfectly secure by construction.

The original Clutch logic provided support for proving such equivalences in the setting of a higher-order language with mutable state. Clutch is a relational logic, where specifications relate the behaviors of two programs. The logic works by constructing probabilistic couplings between the two programs. It introduces new constructs called presampling and asynchronous couplings that make it possible to apply couplings in a rich language with higher-order features and general references.

Clutch supports proving exact equivalences, in which the two programs must have precisely the same probability distribution. However, for many applications, it is important to weaken this to approximate equivalences, where one bounds the distance or difference between the distributions. The Approxis logic generalizes Clutch to support these approximate equivalences. It uses a separationg logic resource to track an "error budget" that bounds the distance between the two programs' distributions.

Both Clutch and Approxis target a sequential language. The Foxtrot logic extends this line of work to concurrent probabilistic programs.

Examples:

Differential Privacy

Differential privacy (DP) is a standard framework for privacy-preserving data analysis: a randomized program is differentially private when small changes to its input (e.g. replacing one user's record) produce only small changes to its output distribution, controlled by a numeric privacy budget

The Clutch-DP logic supports verifying differential privacy of higher-order programs in this style. It treats the privacy budget as a separation logic resource, so reasoning about the composition of DP programs reduces to standard separation logic accounting in which each part of a program consumes some of the budget. Because the underlying language has higher-order functions and local state, Clutch-DP can verify the kind of modular, dynamic, library-style DP code — including privacy filters and caching used in practice in libraries such as OpenDP.

Examples:

Error Probability Bounds

Many randomized algorithms and probabilistic data structures (hash tables, Bloom filters, Miller–Rabin primality testing, rejection samplers, …) only return the right answer with high probability, and using them safely depends on having a tight bound on the probability that they fail.

The Eris logic introduces error credits: a separation logic resource that tracks an upper bound on the probability that a program returns an erroneous result. Treating an error bound as a resource again brings the usual benefits of separation logic such as compositionality and modularity. It also allows for a form of amortized error reasoning, analogous to the use of amortized analysis of algorithmic complexity. The Coneris logic extends the error-credit approach to concurrent programs. Coneris internalizes a notion of randomized logical atomicity using presampling tapes and a new probabilistic update modality, allowing concurrent probabilistic modules (e.g. shared hash tables, concurrent Bloom filters) to be specified and verified modularly.

Examples:

Sampler Correctness

Although Eris was initially designed for reasoning about upper bounds of error probabilities, subsequent work showed that in fact it is possible to prove specifications in Eris that describe the complete distribution of behaviors of a program. Using this approach it is possible to prove the correctness of implementations of sampling routines A common pattern in randomized programming is to build samplers for complex distributions (e.g. binomial, geometric, beta-binomial, etc.) on top of a primitive uniform sampler. Verifying such a library has two goals: ensuring each sampler really implements its target distribution, and giving clients of the library specifications expressive enough to reason about them.

Examples:

Expected Cost Analysis

In probabilistic programs, the resources consumed by the program (time, space, entropy usage) are random variables. The expected value of these random variables gives the average cost of the program.

The Tachis logic introduces probabilistic cost credits: a separation logic resource that can be spent to pay for the cost of operations. These are a probabilistic variant of time credit resources, which had been used in prior separation logics to give worst-case bounds on resource use in deterministic programs. Tachis is parametric in the cost model, so the same logic supports reasoning about expected running time, expected entropy usage, and other resources.

Examples:

Almost-Sure Termination

A randomized program almost-surely terminates if it terminates with probability 1. Establishing this is subtle for higher-order programs with general references, where recursion and looping can be encoded in many different ways and there is no syntactic loop construct to induct on. The Clutch project provides two complementary approaches.

The total-correctness variant of Eris, called Eris_t, reinterprets Eris's Hoare triples by defining their semantics as a least fixed point rather than a guarded one. With this interpretation, an error budget ε in the precondition bounds the probability that the program never reaches a value satisfying the postcondition (which includes both finishing in a bad state and not finishing at all). If a total Hoare triple holds for arbitrarily small ε, the program terminates with probability 1. This gives a uniform way to combine error reasoning with almost-sure termination, and is used to verify algorithms such as rejection samplers in Eris.

The Caliper logic takes a different route: rather than directly proving termination of a program, it establishes a termination-preserving refinement to a simpler probabilistic model (e.g. a Markov chain whose termination behavior is easier to analyze). Refinements are established by probabilistic couplings, much as in Clutch, and general higher-order recursion is handled with guarded recursion (Löb induction).

Examples: