New

Recommended reading: 2.2: New, 2.3: Ownership 101

How to associate code with a type through impl blocks; writing simple static functions; Rust's ownership system.

Implementing new

We first provide a static function to create empty lists:

fn main() {}

pub struct List {
    head: Link,
}

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

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

impl List {
    pub fn new() -> Self {
        List { head: Link::Empty }
    }
}
// Prusti: VERIFIES

A first specification

What would be a sensible first specification for new()? We could attempt to verify the list returned by new() is always empty. In other words, the length of the returned list is always zero. To express this property, we first implement a length method for lists which itself calls an auxiliary length method implemented for Link. For simplicity, we will not actually compute the length of a Link yet. Rather, we will just always return 0. The return type for the len functions is usize, which is a pointer-sized unsigned integer (e.g., 64 bits on a 64-bit computer). usize is also used in the Vec::len function in the standard library.

// The next line is only required for doctests, you can ignore/remove it
extern crate prusti_contracts;
use prusti_contracts::*;

fn main() {}

pub struct List {
    head: Link,
}

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

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

impl List {
    pub fn len(&self) -> usize {
        self.head.len()
    }

    #[ensures(result.len() == 0)] //~ ERROR use of impure function "List::len" in pure code is not allowed
    pub fn new() -> Self {
        List { head: Link::Empty }
    }
}

impl Link {
    fn len(&self) -> usize {
        0
    }
}
// Prusti: VERIFIES

Now that we have implemented a method for computing the length of a list, we can write our first specification for new(): the returned list should always have length zero. That is, we attach the postcondition result.len() == 0 to the function new(). The special variable result is used in Prusti specifications to refer to the value that is returned by a function:

// The next line is only required for doctests, you can ignore/remove it
extern crate prusti_contracts;
use prusti_contracts::*;

fn main() {}

pub struct List {
    head: Link,
}

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

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

impl List {
    pub fn len(&self) -> usize {
        self.head.len()
    }

    #[ensures(result.len() == 0)] //~ ERROR use of impure function "List::len" in pure code is not allowed
    pub fn new() -> Self {
        List { head: Link::Empty }
    }
}

impl Link {
    fn len(&self) -> usize {
        0
    }
}

Unfortunately, Prusti—or rather, the Rust compiler—will complain about the postcondition:

error: cannot find attribute `ensures` in this scope
  --> list.rs:39:7
   |
39 |     #[ensures(result.len() == 0)]    
   |       ^^^^^^^

Prusti's specifications consist of Rust macros and attributes that are defined in a separate crate called prusti-contracts. To see how to add this crate to your project, see the Setup chapter. Before we can use these specifications, we need to make the path to these macros and attributes visible:

// The next line is only required for doctests, you can ignore/remove it
extern crate prusti_contracts;
use prusti_contracts::*;

fn main() {}

pub struct List {
    head: Link,
}

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

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

impl List {
    pub fn len(&self) -> usize {
        self.head.len()
    }

    #[ensures(result.len() == 0)] //~ ERROR use of impure function "List::len" in pure code is not allowed
    pub fn new() -> Self {
        List { head: Link::Empty }
    }
}

impl Link {
    fn len(&self) -> usize {
        0
    }
}

Declaring that we use the prusti_contracts module removes the compiler error but leads to a new error. This time it is an error raised by Prusti:

error: [Prusti: invalid specification] use of impure function "List::len" in pure code is not allowed
  --> list.rs:34:15
   |
34 |     #[ensures(result.len() == 0)]    
   | 

Prusti complains about our use of the method len() in a postcondition because the specification syntax only admits calling so-called pure functions, that is, functions that are deterministic, have no side effects, and always terminate.

While our implementation of len() clearly satisfies all of the above properties, Prusti requires us to explicitly mark a function with the #[pure] attribute before it considers a function pure. After adding the #[pure] attribute to our List::len() method, it is allowed to appear in Prusti specifications:

// The next line is only required for doctests, you can ignore/remove it
extern crate prusti_contracts;
use prusti_contracts::*;

fn main() {}

pub struct List {
    head: Link,
}

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

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

impl List {
    #[pure]
    pub fn len(&self) -> usize {
        self.head.len() //~ ERROR use of impure function "Link::len" in pure code is not allowed
    }

    #[ensures(result.len() == 0)] //~ ERROR precondition of pure function call might not hold.
    pub fn new() -> Self {
        List { head: Link::Empty }
    }
}

impl Link {
    fn len(&self) -> usize {
        0
    }
}

However, Prusti still won't verify! It produces the same error but now it refers to the body of len():

error: [Prusti: invalid specification] use of impure function "Link::len" in pure code is not allowed
  --> list.rs:30:9
   |
30 |         self.head.len() // (5)
   |         ^^^^

Whenever we add the attribute #[pure] to a function, Prusti will check whether that function is indeed deterministic and side-effect free (notice that termination is not checked); otherwise, it complains. In this case, Prusti complains because we call an impure function, namely Link::len(), within the body of the pure function List::len().

To fix this issue, it suffices to mark Link::len() as pure as well.

// The next line is only required for doctests, you can ignore/remove it
extern crate prusti_contracts;
use prusti_contracts::*;

fn main() {}

pub struct List {
    head: Link,
}

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

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

impl List {
    #[pure]
    pub fn len(&self) -> usize {
        self.head.len()
    }

    #[ensures(result.len() == 0)]
    pub fn new() -> Self {
        List { head: Link::Empty }
    }
}

impl Link {
    #[pure]
    fn len(&self) -> usize {
        0
    }
}
// Prusti: VERIFIES

$ cargo prusti
// ...
Successful verification of 4 items

Prusti now manages to verify that new() always returns a list for which the method len() returns 0. (notice this is hardly surprising since len() ultimately always returns 0.)

Proper implementation of len

We will now properly implement len(), and while we're at it, is_empty() for Link. Both of them are pure functions, so we will add the #[pure] annotation. Both functions can be called without any restrictions, so they have the default postcondition #[requires(true)], which we don't have to add manually. We also don't need to add any additional postconditions, since the body of pure functions is considered to be part of their contract.

// The next line is only required for doctests, you can ignore/remove it
extern crate prusti_contracts;
use prusti_contracts::*;

fn main() {}

pub struct List {
    head: Link,
}

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

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

impl List {
    #[pure]
    pub fn len(&self) -> usize {
        self.head.len()
    }

    #[ensures(result.len() == 0)]
    pub fn new() -> Self {
        List {
            head: Link::Empty,
        }
    }
}

impl Link {
    #[pure]
    fn len(&self) -> usize {
        match self {
            Link::Empty => 0,
            Link::More(node) => 1 + node.next.len(),
        }
    }

    #[pure]
    fn is_empty(&self) -> bool {
        matches!(self, Link::Empty)
    }
}

fn test_len(link: &Link) {
    let link_is_empty = link.is_empty();
    let link_len = link.len();
    assert!(link_is_empty == (link_len == 0));
}

Here we use the matches! macro in is_empty, which is true if and only if the first argument matches the pattern in the second argument.

We can now check if the specification is working, by writing a function that panics if the specification is wrong:

// The next line is only required for doctests, you can ignore/remove it
extern crate prusti_contracts;
use prusti_contracts::*;

fn main() {}

pub struct List {
    head: Link,
}

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

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

impl List {
    #[pure]
    pub fn len(&self) -> usize {
        self.head.len()
    }

    #[ensures(result.len() == 0)]
    pub fn new() -> Self {
        List {
            head: Link::Empty,
        }
    }
}

impl Link {
    #[pure]
    fn len(&self) -> usize {
        match self {
            Link::Empty => 0,
            Link::More(node) => 1 + node.next.len(),
        }
    }

    #[pure]
    fn is_empty(&self) -> bool {
        matches!(self, Link::Empty)
    }
}

fn test_len(link: &Link) {
    let link_is_empty = link.is_empty();
    let link_len = link.len();
    assert!(link_is_empty == (link_len == 0));
}

The last line asserts that the is_empty function only returns true if the len function returns 0. And Prusti can verify it! Now we know that this assert statement holds for any link that is passed to the test_len function. Note that we wrote this function only for demonstration purposes—the contract is checked even without the test_len function. We will consider the relationship between testing and static verification further in the Testing chapter.

Overflow checks

Here you can also see why we disabled overflow checking for this tutorial. If you remove the check_overflows = false flag in the Prusti.toml file, and then try to verify the crate again, you will get an error:

[Prusti: verification error] assertion might fail with "attempt to add with overflow"
    Link::More(node) => 1 + node.next.len(),
                        ^^^^^^^^^^^^^^^^^^^

This overflow could happen, if you call len on a list with more than usize::MAX elements. To prevent this verification error, we would have to constrain the maximum size of a List, which is beyond this tutorial.

Full code listing

Before we continue, we provide the full code implemented in this chapter. It should successfully verify with Prusti and we will further extend it throughout the next chapters.

// Expand to see full code up to this chapter
// The next line is only required for doctests, you can ignore/remove it
extern crate prusti_contracts;
use prusti_contracts::*;

fn main() {}

pub struct List {
    head: Link,
}

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

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

impl List {
    #[pure]
    pub fn len(&self) -> usize {
        self.head.len()
    }

    #[ensures(result.len() == 0)]
    pub fn new() -> Self {
        List {
            head: Link::Empty,
        }
    }
}

impl Link {
    #[pure]
    fn len(&self) -> usize {
        match self {
            Link::Empty => 0,
            Link::More(node) => 1 + node.next.len(),
        }
    }

    #[pure]
    fn is_empty(&self) -> bool {
        matches!(self, Link::Empty)
    }
}

fn test_len(link: &Link) {
    let link_is_empty = link.is_empty();
    let link_len = link.len();
    assert!(link_is_empty == (link_len == 0));
}