Caesar

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.5
post [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.