# Caesar

A Deductive Verifierย for Probabilistic Programs

### Expectation-Based Reasoning

Our approach is based on weakest precondition-style reasoning, generalized to probabilistic programs. We can reason about lower and upper bounds of expected values.

### A Quantitative Intermediate Verification Language

Caesar is built on our novel quantitative intermediate verification language HeyVL.
See our OOPSLA '23 paper!

## Features of HeyVL โ Lossy List Traversal Example

Let's look at a program that traverses a list but has a chance of crashing during the traversal. We'll verify that the crash probability is at least 50% if the list has length 1.

We explain more of the details as part of our getting started guide.

### ๐ฅ `lossy_list` Procedure

This procedure is the entry point. It has one output, the resulting list `l`. In the body of `lossy_list`, we traverse the list by repeatedly removing the first element using `pop`. We model a 50% chance of crashing by a coin flip (`flip(0.5)`) leading to `assert [false]`.

``proc lossy_list(init_l: List) -> (l: List)    pre [len(init_l) == 1] * 0.5  // quantitative specification!    post [true]{    l = init_l    @invariant(exp(0.5, len(l)))    while len(l) > 0 {        var prob_choice: Bool = flip(0.5) // coin flip        if prob_choice {            l = pop(l)     // next list element        } else {            assert [false] // crash        }    }}``

### ๐ Reading The Spec

Let's focus on the quantitative specification of `lossy_list`:

``pre [len(init_l) == 1] * 0.5post [true]``

The `post` says that we are looking at the expected value of `[true]` (i.e. 1) in the final states of the program. In other words, we are interested in the probability of running without an error.

The `pre` specifies a lower bound to the probability of a run without crashing (expected value of the post `[true]`). It says that if the length of the list is 1, then the lower bound is `0.5` and otherwise `0`.

To verify the spec, the `while` loop has an `@invariant` annotation with a probabilistic invariant.

### ๐ Axiomatizing Exponentials and Lists

Here is a strength of deductive verification: users can axomatize additional functions and data types that can be used for verification! We simply declare the uninterpreted sort and functions with just the necessary axioms in HeyVL.

``domain Exponentials {    func exp(base: UReal, exponent: UInt): EUReal    axiom exp_base forall base: UReal.      exp(base, 0) == 1    axiom exp_step forall base: UReal, exponent: UInt.      exp(base, exponent + 1) == base * exp(base, exponent)}domain List {    func len(l: List): UInt    func pop(l: List): List    axiom list_len forall l: List.      len(pop(l)) == len(l) - 1}``

### ๐ Running Caesar

Download and extract the latest `caesar` binary (or visit Getting Started for alternative installation options).

The example from above is included in the Git repository. After downloading and storing it in `examples/lossy_list.heyvl` you can try Caesar on it:

``caesar examples/lossy_list.heyvl``

Caesar will print: `examples/lossy_list.heyvl: Verified.`