Getting Started

Our first goal is to implement and verify a simple singly-linked stack that stores 32-bit integers without relying on existing data structures provided by Rust's standard library.

For readers that are unfamiliar with Rust, this is a good time to additionally read the introduction of the accompanying Rust tutorial Learn Rust With Entirely Too Many Linked Lists, which explains the Rust features covered by the tutorial and how to set up a new project with Cargo.

From now on, we will simply provide links to the relevant parts of the Rust tutorial together with a brief summary. For example, reading up on possible data layouts for lists might be useful for beginners:

Recommended reading: 2.1: Basic Data Layout

Discusses potential pitfalls and errors when setting up a singly-linked data structure in Rust.

Stack layout

Our naïve singly-linked stack is composed of a public structure List storing the head of the list, an enum Link representing either an empty list or a heap-allocated Node storing the payload—an integer—and the link to the next node:

pub struct List {
    head: Link,
}

enum Link {
    Empty,
    More(Box<Node>),
}

struct Node {
    elem: i32,
    next: Link,
}

fn main() {
    let test = Node {
        elem: 17,
        next: Link::Empty,
    };

    if test.elem > 23 {
        panic!() // unreachable
    }
}
// Prusti: VERIFIES

As explained in the chapter 2.1: Basic Data Layout, this design avoids making both Link and Node public. Moreover, it benefits from the Rust compiler's null-pointer optimization and makes sure that all list elements are uniformly allocated on the heap.

Absence of runtime errors

Prusti automatically checks that no statement or macro that causes an explicit runtime error, such as panic!, unreachable!, unimplemented!, todo!, or possibly a failing assertion, is reachable. Prusti assertions are also checked. These are like the normal assert! statements, but they can use the full Prusti specification syntax and will not result in any runtime checks or code when compiled normally.

For example, the following test function creates a node with no successor and panics if the node's payload is greater than 23:

pub struct List {
    head: Link,
}

enum Link {
    Empty,
    More(Box<Node>),
}

struct Node {
    elem: i32,
    next: Link,
}

fn main() {
    let test = Node {
        elem: 17,
        next: Link::Empty,
    };

    if test.elem > 23 {
        panic!() // unreachable
    }
}
// Prusti: VERIFIES

Prusti successfully verifies the above function because it can statically guarantee that test.elem <= 23 holds whenever execution reaches the if statement.

This is not the case for the following function in which the test node is initialized with an arbitrary integer:

pub struct List {
    head: Link,
}

enum Link {
    Empty,
    More(Box<Node>),
}

struct Node {
    elem: i32,
    next: Link,
}

fn main() {
    let test = Node {
        elem: 17,
        next: Link::Empty,
    };

    if test.elem > 23 {
        panic!() // unreachable
    }
}

fn test(x: i32) {
    let test = Node {
        elem: x, // unknown value
        next: Link::Empty,
    };

    if test.elem > 23 {
        panic!() //~ ERROR panic!(..) statement might be reachable
    }
}
// Prusti: FAILS

Prusti reports errors in the same fashion as the Rust compiler (with the prefix Prusti: verification error). For example, the error produced for the above function is:

error: [Prusti: verification error] statement might panic
  --> getting_started_failing.rs:33:9
   |
33 |         panic!()
   |         ^^^^^^^^