# 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        }    }}``

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

After installing Rust, install the `caesar` binary (c.f. Getting Started):

``git clone git@github.com:moves-rwth/caesar.gitcd caesarcargo install --path . caesarcaesar tests/domains/lossy_list.heyvl``

This will run Caesar on the example above (it is included in the Git repository). Caesar will print: `tests/domains/lossy_list.heyvl: Verified.`