Introduction

This is the user guide for Prusti - a Rust verifier built upon the the Viper verification infrastructure.

Installation

Prusti Assistant

The easiest way to try out Prusti is by using the "Prusti Assistant" extension for Visual Studio Code. Please confer the extension's webpage for:

• Detailed installation and first usage instructions.
• The description of the available commands, among which are commands to run and update the verifier.
• The description of the configuration flags.
• Troubleshooting instructions.

Warning: Some of the Prusti-specific syntax described in this guide is currently only available in the "LatestDev" build channel, which corresponds to the latest development version of Prusti. The settings for switching to this version in Prusti Assistant are found in File → Preferences → Settings → Prusti Assistant → Build Channel.

In case you experience difficulties or encounter bugs while using Prusti Assistant, please open an issue in Prusti Assistant's repository or contact us in the Zulip chat. Bugs with Prusti itself can be reported on the prusti-dev repository.

Command-line setup

Alternatively, Prusti can be set up by downloading the precompiled binaries available from the project page. We currently provide binaries for Windows, macOS (Intel), and Ubuntu. Releases marked as "Pre-release" may contain unstable or experimental features.

For a command-line setup with Prusti built from source, please confer the developer guide.

Basic Usage

Prusti Assistant

When the Prusti Assistant extension is active, Rust files can be verified in one of the following ways:

• By clicking the "Verify with Prusti" button in the status bar.
• By opening the Command Palette and running the command "Prusti: save and verify this file".
• By saving a Rust document, if "Verify on save" is enabled.
• By opening a Rust document, if "Verify on open" is enabled.

See the Verification Features chapter for a list of verification features available in Prusti.

Command line

To run Prusti on a file using the command-line setup:

prusti-rustc --edition=2018 path/to/file.rs

Run this command from a crate or workspace root directory to verify it:

cargo-prusti

If Prusti is in $PATH, it can also be run as a Cargo subcommand:

cargo prusti

Introductory example

Let us verify that the function max below, which takes two integers and returns the greater one, is implemented correctly.

fn max(a: i32, b: i32) -> i32 {
    if a > b {
        a
    } else {
        b
    }
}

When pasting the above code into a Rust file and then verifying it with Prusti (as outlined at the top of the page), Prusti should report that verification succeeded. This tells us that

1. the file consists of valid Rust code that can be compiled successfuly, and
2. no execution reaches a Rust panic (explicit call of the panic!() macro, a failed assertion, etc).

To also verify that max indeed always returns the maximum of its two inputs, we have to add a corresponding specification, which states that the return value of max is at least as large as both a and b and, additionally, coincides with a or b:

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

#[ensures(result >= a && result >= b)]
#[ensures(result == a || result == b)]
fn max(a: i32, b: i32) -> i32 {
    if a > b {
        a
    } else {
        b
    }
}

In the above program, the first line (use prusti_contracts::*;) simplifies writing Prusti-specific syntax for specifications; allowing us to write #[ensures(...)] instead of #[prusti_contracts::ensures(...)].

Warning: Due to limitations in Rust procedural macros, use prusti_contracts::*; should always be used, and the Prusti specification attributes should not be imported with an alias.

After that, we used #[ensures(...)] to attach two postconditions to the function max. The syntax of specifications is a superset of Rust expressions, where result is a keyword referring to the function's return value.

Again, verifying the above code with Prusti should succeed. Notice that Prusti assumes by default that integer types are bounded; it thus performs overflow and underflow checks unless corresponding options are provided.

Next, we add a second function max3 which returns the maximum of three instead of two integers; we reuse the already verified function max in the new function's specification to show that this function is implemented correctly.

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

#[pure]
#[ensures(result >= a && result >= b)]
#[ensures(result == a || result == b)]
fn max(a: i32, b: i32) -> i32 {
    if a > b {
        a
    } else {
        b
    }
}

#[ensures(result == max(a, max(b, c)))]
fn max3(a: i32, b: i32, c: i32) -> i32 {
    if a > b && a > c {
        a
    } else {
        if b > c {
            b
        } else {
            c
        }
    }
}

Again, Prusti should successfully verify the above program. Notice that we additionally declared the function max as pure such that it can be used within specifications. If we omit this annotation, Prusti will complain that the postcondition of function max3 is invalid because it uses an impure function, which may potentially have side-effects.

So far, we only considered programs that meet their specification and that, consequently, Prusti successfully verified. To conclude this example, assume we accidentally return c instead of b if b > c holds:

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

#[ensures(result == max(a, max(b, c)))]
fn max3(a: i32, b: i32, c: i32) -> i32 {
    if a > b && a > c {
        a
    } else {
        if b > c {
            c // ERROR
        } else {
            c
        }
    }
}

In this case, Prusti will highlight the line with the error and report that the postcondition might not hold.

For debugging purposes, it is often useful to add assert!(...) macros to our code to locate the issue. For example, in the code below, we added an assertion that fails because b > c and thus the maximum of b and c is b instead of c.

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

#[pure]
#[ensures(result >= a && result >= b)]
#[ensures(result == a || result == b)]
fn max(a: i32, b: i32) -> i32 {
    if a > b {
        a
    } else {
        b
    }
}

#[ensures(result == max(a, max(b, c)))]
fn max3(a: i32, b: i32, c: i32) -> i32 {
    if a > b && a > c {
        a
    } else {
        if b > c {
            assert!(max(b, c) == c); // FAILS
            c
        } else {
            c
        }
    }
}

When running Prusti on this example, it highlights the failing assertion and thus enables us to quickly locate and fix the issue.

Configuration

Prusti offers a many flags to configure its behavior. See Providing Flags for how to provide these flags and List of Configuration Flags in the developer guide.

Guided Tour

Disclaimer: All code shown in this tutorial has been tested with Prusti version 0.2.1, 2023-01-26

Unless stated otherwise, all code listings should be put in their own file and can be verified with Prusti assistant.

In this chapter, we demonstrate Prusti's capabilities. As a running example, we roughly follow the first chapters of the Rust tutorial Learn Rust with Entirely Too Many Linked Lists. Linked lists turn out to be sufficiently complex that their implementation and verification covers most of Rust's and Prusti's essential concepts. While the above tutorial explains in detail how linked lists are implemented in Rust, we additionally aim to verify that the implemented list operations are functionally correct.

While we assume basic familiarity with Rust, it is possible to learn both Rust and Prusti at the same time by reading this tour and the Rust tutorial that inspired it in an interleaved fashion. We will provide pointers to the Rust tutorial for beginners to catch up where appropriate.

Throughout this tour, we will cover the following Prusti concepts:

• How Prusti reports errors and integrates into the development process
• Runtime errors detected by Prusti
• Writing function-modular specifications
• Using pure functions and predicates in specifications
• Writing loop invariants
• Using extern_spec to deal with library code
• Writing pledges for functions that return mutable references
• Basic troubleshooting

The individual chapters are found in the sidebar, which may be collapsed on mobile devices. As a quick reference, the main steps of this tour and the involved Prusti features are as follows:

1. Setup: Adding Prusti to a Rust project
2. Getting Started: Simple runtime errors caught by Prusti
3. New: Postconditions, pure functions
4. Push: Preconditions, external specifications, trusted functions, old expressions, quantifiers, snapshots, structural/snapshot equality
5. Pop: Similar concepts as in Push, predicates
6. Testing: Showing guarantees of verification vs running tests, and how to test specifications
7. Option: Changing Link to use Option type
8. Generics: Prusti and generics
9. Peek: Verifying a peek function
10. Pledges (mutable peek): Demonstrating Prusti's pledges for functions returning mutable references
11. Final Code: Final code for the verified linked list
12. Loop Invariants: Verifying code containing loops by writing loop invariants
13. Counterexamples: Getting counterexamples for failing assertions

Setup

To get started, you can use an existing Rust project or create a new one with Cargo:

cargo new prusti_tutorial

Then you can change the current working directory to the project's directory:

cd ./prusti_tutorial/

To use the additional syntax used for verification with Prusti, you need to add the prusti-contracts crate to your project. If you have at least Cargo version 1.62.0, you can use this command to add the dependency:

cargo add prusti-contracts

For older versions of Rust, you can manually add the dependency in your Cargo.toml file:

[dependencies]
prusti-contracts = "0.1.6"

To use prusti-contracts in a Rust code file, just add the following line:

use prusti_contracts::*;

To simplify the tutorial, overflow checks by Prusti will be disabled. To do that, create a file called Prusti.toml in your project's root directory (where Cargo.toml is located). In this file, you can set configuration flags used by Prusti. To disable overflow checking, add the following line:

check_overflows = false

Note: Creating a new project will create a main.rs file containing a Hello World program. Since Prusti does not yet support Strings, verification will fail on main.rs. To still verify the code, remove the line println!("Hello, world!");.

Standard library annotations

Annotations for functions and types in the Rust standard library will be available in the prusti-std crate after this PR is merged.

Adding this crate works the same as for the prusti-contracts crate:

cargo add prusti-std

or:

[dependencies]
prusti-std = "0.1.6"

You do not need to import anything to use the annotations in this crate in a file.

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!()
   |         ^^^^^^^^

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));
}

Push

Recommended reading: 2.4: Push

Informal specifications

Our next goal is to implement and verify a method that pushes an integer onto a list. In contrast to methods like len, push modifies the list; it thus takes &mut self as its first argument:

impl List {
    pub fn push(&mut self, elem: i32) {
        // TODO
    }
}

Since push modifies self, it cannot be marked as a #[pure] function (it has a side effect on self). This means we will not be able to use push inside specifications for other functions later.

Before we implement push, let us briefly think of possible specifications. Ideally, our implementation satisfies at least the following properties:

1. Executing push increases the length of the underlying list by one. (Chapter link)
2. After push(elem) the first element of the list stores the value elem. (Chapter link)
3. After executing push(elem), the elements of the original list remain unchanged, but are moved back by 1 position. (Chapter link)

Initial code

We start out with an implementation of push. If you want to learn more about how this code works, you can read 2.4: Push, where it is explained in detail.

Here is our initial code:

// 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 push(&mut self, elem: i32) {
        let new_node = Box::new(Node {
            elem, // we can use `elem` instead of `elem: elem,` here, since the variable has the same name as the field
            next: std::mem::replace(&mut self.head, Link::Empty),
        });

        self.head = Link::More(new_node);
    }

    #[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)
    }
}

First property

The first property can easily be expressed as a postcondition that uses the pure method len introduced in the previous 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,
}

#[extern_spec(std::mem)]
#[ensures(snap(dest) === src)]
#[ensures(result === old(snap(dest)))]
fn replace<T>(dest: &mut T, src: T) -> T;

impl List {
    #[ensures(self.len() == old(self.len()) + 1)] // 1. Property
    pub fn push(&mut self, elem: i32) {
        let new_node = Box::new(Node {
            elem,
            next: std::mem::replace(&mut self.head, Link::Empty),
        });

        self.head = Link::More(new_node);
    }

    #[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)
    }
}

Even though the above implementation of push is correct, attempting to verify it with Prusti still yields a verification error:

[Prusti: verification error] postcondition might not hold.

This error may look surprising at first: We create a new list node that stores the the original list in its next field. Why is Prusti unable to realize that the length of the resulting list is one plus the length of the original list?

The explanation is that Prusti performs function modular verification, that is, it only uses a function's specification (instead of also consulting the function's implementation) whenever it encounters a function call. The only exception are pure functions, such as len, where Prusti also takes the function body into account.

Adding external specifications to library code

In our case, the function std::mem::replace is neither marked as pure nor does it come with a specification. Hence, Prusti assumes that it is memory safe and nothing else. That is, Prusti uses true as both pre- and postcondition of replace, which is too weak to prove the specification of push. According to its specification, replace could arbitrarily change the original list and thus also its length. Hence, we cannot conclude that the length the list returned by replace(&mut self.head, Link::Empty) coincides with the length of the original list.

We can remedy this issue by strengthening the specification of replace. In this tutorial, we will assume that the standard library is correct, that is, we do not attempt to verify specifications for functions in external crates, like replace. To this end, we have to add the specification to the function. This can be done with another piece of Prusti syntax, the extern_spec:

// 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,
}

#[extern_spec(std::mem)]
#[ensures(snap(dest) === src)]
#[ensures(result === old(snap(dest)))]
fn replace<T>(dest: &mut T, src: T) -> T;

impl List {
    #[ensures(self.len() == old(self.len()) + 1)] // 1. Property
    pub fn push(&mut self, elem: i32) {
        let new_node = Box::new(Node {
            elem,
            next: std::mem::replace(&mut self.head, Link::Empty),
        });

        self.head = Link::More(new_node);
    }

    #[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)
    }
}

Let's break this snippet down step by step:

• First, we write the Prusti annotation #[extern_spec] to denote that we are writing an external specification. This requires prusti_contracts::* to be imported first.
• Next, we need to declare where the original function is located. In this case it is the module std::mem, so we put its path in the parameter: #[extern_spec(std::mem)]
• After a quick search for "rust std mem replace" we can find the documentation for std::mem::replace. Here we can get the function signature: pub fn replace<T>(dest: &mut T, src: T) -> T. We then write down the signature in the inner module, followed by a ;.
• Since there are no preconditions to replace, we can use the (implicit) default #[requires(true)].
• For writing the postcondition, we use four pieces of Prusti syntax:
  • === is called snapshot equality or logical equality. Is means that the left and right operands are structurally equal. === does not require the type of the compared elements to implement PartialEq, which would be required if we used the standard equality operator ==.
  • The snap() function takes a snapshot of a reference. It has a similar functionality to the clone() method, but does not require the type of the reference it is called on to implement the Clone trait. snap should only be used in specifications, since it ignores the borrow checker.
  • Lastly, we have the old() function, which denotes that we want to refer to the state of snap(dest) from before the function was called.
  • The identifier result is used to refer to the return parameter of the function.
• The postcondition consists of two parts, which can either be written in one condition with &&, or in multiple #[ensures(...)] annotations like in the example above.
  • The first condition snap(dest) === src means: After the function returns, the location referenced by dest is structurally equal to the parameter src
  • The second part of the postcondition is result === old(snap(dest)). This means: The result returned by the function is structurally equal to the the element that was referenced by dest before the function was called.

Since result is structurally equal to dest from before the function call, Prusti knows that the pure function len() called on result returns the same value as it would have for dest.

An important thing to note here is that Prusti does not check if replace actually does what the external specification says it does. #[extern_spec] implicitly implies the #[trusted] annotation, which means that any postconditions are just accepted and used by Prusti.

Future

There is currently new functionality planned for Prusti-assistant, which should enable the user to automatically generate parts of the extern_spec syntax.

There is also work being done for providing external specifications for the Rust standard library. Depending on when you are reading this, the std::mem::replace function might be annotated already, in that case this extern_spec may not be needed anymore. You can track the progress and find some already completed specifications in this Pull Request.

Specifications for the standard library should eventually be available in the prusti-std crate. Any specifications in this crate will be available by adding it to your project's dependencies.

Trusted functions

As mentioned above, extern_specs are implicitly #[trusted] by Prusti. Trusted functions can be used for verifying projects containing external code that does not have Prusti annotations, or projects using Rust features that are not yet supported by Prusti. An example is printing a string slice (not supported yet):

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

#[trusted]
fn print(s: &str) {
    println!("{s}");
}

Prusti will not check trusted functions for correctness, so it is the programmers responsibility to check their the specification manually. A single incorrect specification of a trusted function can invalidate the correctness of Prusti as a whole! Hence, trusted functions, like unsafe Rust code, need to be treated carefully and require external justification.

For example, the following function will not cause the verification to fail:

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

#[trusted]
fn incorrect_function() -> i32 {
    panic!()
}

This one is even worse, it will enable anything to be verified:

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

#[trusted]
#[ensures(false)]
fn wrong() {}

Checking the extern_spec

Let's get back to our code. After adding the external specification for std::mem::replace, we can finally verify the first property of our push 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,
}

#[extern_spec(std::mem)]
#[ensures(snap(dest) === src)]
#[ensures(result === old(snap(dest)))]
fn replace<T>(dest: &mut T, src: T) -> T;

impl List {
    #[ensures(self.len() == old(self.len()) + 1)] // 1. Property
    pub fn push(&mut self, elem: i32) {
        let new_node = Box::new(Node {
            elem,
            next: std::mem::replace(&mut self.head, Link::Empty),
        });

        self.head = Link::More(new_node);
    }

    #[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)
    }
}
// Prusti: Verifies

With this, the first of the three properties of push is verified, but we still have two more to prove.

Second property

Recall the second property of our specification:

2. After push(elem), the first element of the list stores the value elem.

To formally specify the above property, we first introduce another pure function, called lookup, that recursively traverses the list and returns its i-th element. Our second desired property then corresponds to the postcondition self.lookup(0) == elem.

// 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,
}

#[extern_spec(std::mem)]
#[ensures(snap(dest) === src)]
#[ensures(result === old(snap(dest)))]
fn replace<T>(dest: &mut T, src: T) -> T;

impl List {
    #[pure]
    pub fn lookup(&self, index: usize) -> i32 {
        self.head.lookup(index)
    }

    #[ensures(self.len() == old(self.len()) + 1)]
    #[ensures(self.lookup(0) == elem)] // 2. Property //~ ERROR postcondition might not hold
    pub fn push(&mut self, elem: i32) {
        // ...
        let new_node = Box::new(Node {
            elem,
            next: std::mem::replace(&mut self.head, Link::Empty),
        });

        self.head = Link::More(new_node);
    }

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

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

impl Link {
    #[pure]
    pub fn lookup(&self, index: usize) -> i32 {
        match self {
            Link::More(node) => {
                if index == 0 {
                    node.elem
                } else {
                    node.next.lookup(index - 1)
                }
            }
            Link::Empty => unreachable!(), //~ ERROR: unreachable!(..) statement might be reachable
        }
    }

    #[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)
    }
}

Consider the match statement in the last function. The Rust compiler will complain if we attempt to omit the case Link::Empty. We have no sensible implementation of lookup if the underlying list is empty, so we used the macro unreachable!(), which will crash the program with a panic. Since nothing prevents us from calling lookup on an empty list, Prusti complains:

unreachable!(..) statement might be reachable

We can specify that lookup should only be called with an index between 0 and self.len() (which implies that we cannot call lookup on an empty list: 0 <= index < self.len() implies 0 < self.len()). We do this by adding the precondition index < self.len() to both lookup functions. This is sufficient to verify our second property for push:

// 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,
}

#[extern_spec(std::mem)]
#[ensures(snap(dest) === src)]
#[ensures(result === old(snap(dest)))]
fn replace<T>(dest: &mut T, src: T) -> T;

impl List {
    #[pure]
    #[requires(index < self.len())]
    pub fn lookup(&self, index: usize) -> i32 {
        // ...
        self.head.lookup(index)
    }

    #[ensures(self.len() == old(self.len()) + 1)] // 1. Property
    #[ensures(self.lookup(0) == elem)] // 2. Property
    pub fn push(&mut self, elem: i32) {
        let new_node = Box::new(Node {
            elem,
            next: std::mem::replace(&mut self.head, Link::Empty),
        });

        self.head = Link::More(new_node);
    }

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

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

impl Link {
    #[pure]
    #[requires(index < self.len())]
    pub fn lookup(&self, index: usize) -> i32 {
        // ...
        match self {
            Link::More(node) => {
                if index == 0 {
                    node.elem
                } else {
                    node.next.lookup(index - 1)
                }
            }
            Link::Empty => unreachable!(),
        }
    }

    #[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)
    }
}

We don't need to add the condition 0 <= index, since index has the type usize, and unsigned integers are always non-negative. (If you don't want Prusti to add this condition automatically, you can add the line encode_unsigned_num_constraint = false to your Prusti.toml file).

After these changes, Prusti can successfully verify the code, so the first two properties of push are correct.

Third property

The third and final property we will verify for push is that the original list content is not modified:

3. After executing push(elem), the elements of the original list remain unchanged (just shifted back by one).

To formalize the above property, we can reuse our pure function lookup, quantifiers, and old expressions, that is, we add the postcondition:

// 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,
}

#[extern_spec(std::mem)]
#[ensures(snap(dest) === src)]
#[ensures(result === old(snap(dest)))]
fn replace<T>(dest: &mut T, src: T) -> T;

impl List {
    #[pure]
    #[requires(index < self.len())]
    pub fn lookup(&self, index: usize) -> i32 {
        self.head.lookup(index)
    }

    #[ensures(self.len() == old(self.len()) + 1)] // 1. Property
    #[ensures(self.lookup(0) == elem)] // 2. Property
    #[ensures(forall(|i: usize| (i < old(self.len())) ==>
                 old(self.lookup(i)) == self.lookup(i + 1)))] // 3. Property
    pub fn push(&mut self, elem: i32) {
        // ...
        let new_node = Box::new(Node {
            elem,
            next: std::mem::replace(&mut self.head, Link::Empty),
        });

        self.head = Link::More(new_node);
    }

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

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

impl Link {
    #[pure]
    #[requires(index < self.len())]
    pub fn lookup(&self, index: usize) -> i32 {
        match self {
            Link::More(node) => {
                if index == 0 {
                    node.elem
                } else {
                    node.next.lookup(index - 1)
                }
            }
            Link::Empty => unreachable!(),
        }
    }

    #[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)
    }
}

Let's break this expression down like before:

• We start with the ensures annotation, to denote a postcondition.
• forall(..) denotes a quantifier. The variables and body of a quantifier use a syntax similar to Rust closures.
• The two vertical bars: || contain the variables that the quantifier quantifies over. Here we only have one parameter i: usize. The type of the quantifier body is bool. You can think of the forall expression as follows: Any values chosen for the quantified variables should result in the expression evaluating to true.
• In this case, the quantifier uses the implication operator ==>. It takes a left and right argument of type bool and is true if the left-hand side is false, or both sides are true.
  • The left-hand side of the implication is (1 <= i && i < self.len()), which is the range where the right side must hold. If the index i is outside of this range, we don't care about it, so the condition will be false, making the entire implication true.
  • The right-hand side is the condition for everything being shifted back by one element: old(self.lookup(i - 1)) == self.lookup(i))). Note that the right side is only evaluated if the left side is true, otherwise there would be an overflow in i - 1 for i == 0, or a panic if i is out of bounds.

This code is verified successfully by Prusti, so we know that the lookup function satisfies the three postconditions!

Full code listing

// 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,
}

#[extern_spec(std::mem)]
#[ensures(snap(dest) === src)]
#[ensures(result === old(snap(dest)))]
fn replace<T>(dest: &mut T, src: T) -> T;

impl List {
    #[pure]
    #[requires(index < self.len())]
    pub fn lookup(&self, index: usize) -> i32 {
        self.head.lookup(index)
    }

    #[ensures(self.len() == old(self.len()) + 1)] // 1. Property
    #[ensures(self.lookup(0) == elem)] // 2. Property
    #[ensures(forall(|i: usize| (i < old(self.len())) ==>
                 old(self.lookup(i)) == self.lookup(i + 1)))] // 3. Property
    pub fn push(&mut self, elem: i32) {
        // ...
        let new_node = Box::new(Node {
            elem,
            next: std::mem::replace(&mut self.head, Link::Empty),
        });

        self.head = Link::More(new_node);
    }

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

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

impl Link {
    #[pure]
    #[requires(index < self.len())]
    pub fn lookup(&self, index: usize) -> i32 {
        match self {
            Link::More(node) => {
                if index == 0 {
                    node.elem
                } else {
                    node.next.lookup(index - 1)
                }
            }
            Link::Empty => unreachable!(),
        }
    }

    #[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)
    }
}

Pop

Recommended reading: 2.5: Pop,

Let's continue with a function to remove and return the element at the head of a list. The way to write such a function is described in 2.5: Pop, we will focus on the verification in this chapter.

There is one change to the code from the original tutorial: We will rename the pop function to try_pop. The return type is still Option<i32> and try_pop will return Some(item) if the list has elements, and None otherwise. We will then add a new pop function, which has the return type i32, and will panic if it is called with an empty list. However, by using the correct precondition, we can prevent the pop function from ever panicking! Here is the code:

// 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()
    }
    
    #[pure]
    fn is_empty(&self) -> bool {
        self.head.is_empty()
    }

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

    #[pure]
    #[requires(index < self.len())]
    pub fn lookup(&self, index: usize) -> i32 {
        self.head.lookup(index)
    }

    #[ensures(self.len() == old(self.len()) + 1)] //~ ERROR postcondition might not hold
    #[ensures(self.lookup(0) == elem)]
    #[ensures(forall(|i: usize| (i < old(self.len())) ==>
                 old(self.lookup(i)) == self.lookup(i + 1)))]
    pub fn push(&mut self, elem: i32) {
        let new_node = Box::new(Node {
            elem,
            next: std::mem::replace(&mut self.head, Link::Empty),
        });

        self.head = Link::More(new_node);
    }

    pub fn try_pop(&mut self) -> Option<i32> {
        match std::mem::replace(&mut self.head, Link::Empty) {
            Link::Empty => None,
            Link::More(node) => {
                self.head = node.next;
                Some(node.elem)
            },
        }
    }
    
    #[requires(!self.is_empty())]
    pub fn pop(&mut self) -> i32 {
        self.try_pop().unwrap()
    }
}

impl Link {
    #[pure]
    #[requires(index < self.len())]
    pub fn lookup(&self, index: usize) -> i32 {
        match self {
            Link::More(node) => {
                if index == 0 {
                    node.elem
                } else {
                    node.next.lookup(index - 1)
                }
            },
            Link::Empty => unreachable!(),  
        }
    }
    
    #[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)
    }
}

For the implementation of our pop method, we can reuse the implementation of try_pop. We call try_pop on the list, then call unwrap on the result. unwrap will return the inner value of the Option if it is Some, and will panic otherwise. Normally, it is bad form to use unwrap in production code, where you should handle potential errors, instead of just panicking. But, since we are verifying that there will never be None passed to unwrap, we should be able to get away with it here.

Properties of try_pop

Let's start by (informally) listing the properties we want our try_pop method to have. We do not need a precondition for try_pop, since it can be called on any list. This just leaves all the postconditions, which can be put into two categories:

• If the input list is empty before the call:
  1. The result will be None.
  2. The list will still be empty afterwards.
• If the input list is not empty before the call:
  1. The result will be Some(value) and value is the element that was the first element of the list.
  2. The length will get reduced by one.
  3. All elements will be shifted forwards by one.

Properties of pop

For pop, we will add a precondition that the list is not empty. The postconditions are similar to those of try_pop, but we can skip all those that only apply to empty lists.

Preparations

Adding List::is_empty

Since we will need to check if a list is empty, we can implement a #[pure] function is_empty for List. It can just call the is_empty function on self.head:

// 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()
    }
    
    #[pure]
    fn is_empty(&self) -> bool {
        self.head.is_empty()
    }

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

    #[pure]
    #[requires(index < self.len())]
    pub fn lookup(&self, index: usize) -> i32 {
        self.head.lookup(index)
    }

    #[ensures(self.len() == old(self.len()) + 1)] //~ ERROR postcondition might not hold
    #[ensures(self.lookup(0) == elem)]
    #[ensures(forall(|i: usize| (i < old(self.len())) ==>
                 old(self.lookup(i)) == self.lookup(i + 1)))]
    pub fn push(&mut self, elem: i32) {
        let new_node = Box::new(Node {
            elem,
            next: std::mem::replace(&mut self.head, Link::Empty),
        });

        self.head = Link::More(new_node);
    }

    pub fn try_pop(&mut self) -> Option<i32> {
        match std::mem::replace(&mut self.head, Link::Empty) {
            Link::Empty => None,
            Link::More(node) => {
                self.head = node.next;
                Some(node.elem)
            },
        }
    }
    
    #[requires(!self.is_empty())]
    pub fn pop(&mut self) -> i32 {
        self.try_pop().unwrap()
    }
}

impl Link {
    #[pure]
    #[requires(index < self.len())]
    pub fn lookup(&self, index: usize) -> i32 {
        match self {
            Link::More(node) => {
                if index == 0 {
                    node.elem
                } else {
                    node.next.lookup(index - 1)
                }
            },
            Link::Empty => unreachable!(),  
        }
    }
    
    #[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)
    }
}

Writing the external specifications for Option

Since we use Option::unwrap, we will need an external specification for it. While we're at it, let's also write the #[extern_spec] for Option::is_some and Option::is_none:

// 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,
}

#[extern_spec(std::mem)]
#[ensures(snap(dest) === src)]
#[ensures(result === old(snap(dest)))]
fn replace<T>(dest: &mut T, src: T) -> T;

// Specs for std::option::Option<T>::unwrap(self) (and others) can be found here (work in progress):
// https://github.com/viperproject/prusti-dev/pull/1249/files#diff-bccda07f8a48357687e26408251041072c7470c188092fb58439de39974bdab5R47-R49

#[extern_spec]
impl<T> std::option::Option<T> {
    #[requires(self.is_some())]
    #[ensures(old(self) === Some(result))]
    pub fn unwrap(self) -> T;

    #[pure]
    #[ensures(result == matches!(self, None))]
    pub const fn is_none(&self) -> bool;

    #[pure]
    #[ensures(result == matches!(self, Some(_)))]
    pub const fn is_some(&self) -> bool;
}

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

    #[pure]
    fn is_empty(&self) -> bool {
        self.head.is_empty()
    }

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

    #[pure]
    #[requires(index < self.len())]
    pub fn lookup(&self, index: usize) -> i32 {
        self.head.lookup(index)
    }

    #[ensures(self.len() == old(self.len()) + 1)]
    #[ensures(self.lookup(0) == elem)]
    #[ensures(forall(|i: usize| (i < old(self.len())) ==>
                 old(self.lookup(i)) == self.lookup(i + 1)))]
    pub fn push(&mut self, elem: i32) {
        let new_node = Box::new(Node {
            elem,
            next: std::mem::replace(&mut self.head, Link::Empty),
        });

        self.head = Link::More(new_node);
    }

    predicate! {
        // two-state predicate to check if the head of a list was correctly removed
        fn head_removed(&self, prev: &Self) -> bool {
            self.len() == prev.len() - 1 // The length will decrease by 1
            && forall(|i: usize| // Every element will be shifted forwards by one
                (1 <= i && i < prev.len())
                    ==> prev.lookup(i) == self.lookup(i - 1))
        }
    }

    #[ensures(old(self.is_empty()) ==>
        result.is_none() &&
        self.is_empty()
    )]
    #[ensures(!old(self.is_empty()) ==>
        self.head_removed(&old(snap(self)))
        &&
        result === Some(old(snap(self)).lookup(0))
    )]
    pub fn try_pop(&mut self) -> Option<i32> {
        // ...
        match std::mem::replace(&mut self.head, Link::Empty) {
            Link::Empty => None,
            Link::More(node) => {
                self.head = node.next;
                Some(node.elem)
            }
        }
    }

    #[requires(!self.is_empty())]
    #[ensures(self.head_removed(&old(snap(self))))]
    #[ensures(result === old(snap(self)).lookup(0))]
    pub fn pop(&mut self) -> i32 {
        // ...
        self.try_pop().unwrap()
    }
}

impl Link {
    #[pure]
    #[requires(index < self.len())]
    pub fn lookup(&self, index: usize) -> i32 {
        match self {
            Link::More(node) => {
                if index == 0 {
                    node.elem
                } else {
                    node.next.lookup(index - 1)
                }
            }
            Link::Empty => unreachable!(),
        }
    }

    #[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)
    }
}

The syntax for writing external specifications for functions associated with Option is slightly different to that of std::mem::replace, which was a standalone function.

Note: In the future, you should just be able to import these external specifications using the prusti-std crate. It should be available after this PR is merged. Until then, you can find the work in progress specifications in the PR (e.g., for Option::unwrap).

Implementing the specification

Writing the precondition

Let's start our specification with the precondition of pop. Since the unwrap will panic if it is passed None, and try_pop returns None if the list is empty, we have to ensure that pop is only called on non-empty lists. Therefore we add it as a precondition:

// 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()
    }
    
    #[pure]
    fn is_empty(&self) -> bool {
        self.head.is_empty()
    }

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

    #[pure]
    #[requires(index < self.len())]
    pub fn lookup(&self, index: usize) -> i32 {
        self.head.lookup(index)
    }

    #[ensures(self.len() == old(self.len()) + 1)] //~ ERROR postcondition might not hold
    #[ensures(self.lookup(0) == elem)]
    #[ensures(forall(|i: usize| (i < old(self.len())) ==>
                 old(self.lookup(i)) == self.lookup(i + 1)))]
    pub fn push(&mut self, elem: i32) {
        let new_node = Box::new(Node {
            elem,
            next: std::mem::replace(&mut self.head, Link::Empty),
        });

        self.head = Link::More(new_node);
    }

    pub fn try_pop(&mut self) -> Option<i32> {
        match std::mem::replace(&mut self.head, Link::Empty) {
            Link::Empty => None,
            Link::More(node) => {
                self.head = node.next;
                Some(node.elem)
            },
        }
    }
    
    #[requires(!self.is_empty())]
    pub fn pop(&mut self) -> i32 {
        self.try_pop().unwrap()
    }
}

impl Link {
    #[pure]
    #[requires(index < self.len())]
    pub fn lookup(&self, index: usize) -> i32 {
        match self {
            Link::More(node) => {
                if index == 0 {
                    node.elem
                } else {
                    node.next.lookup(index - 1)
                }
            },
            Link::Empty => unreachable!(),  
        }
    }
    
    #[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)
    }
}

try_pop does not require a precondition, since it will never panic.

try_pop postcondition for empty lists

Now we will implement the two conditions that hold for try_pop if you pass an empty list to it. To ensures that these are only checked for empty lists, we use the implication operator ==>:

// 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,
}

#[extern_spec(std::mem)]
#[ensures(snap(dest) === src)]
#[ensures(result === old(snap(dest)))]
fn replace<T>(dest: &mut T, src: T) -> T;

// Specs for std::option::Option<T>::unwrap(self) (and others) can be found here (work in progress):
// https://github.com/viperproject/prusti-dev/pull/1249/files#diff-bccda07f8a48357687e26408251041072c7470c188092fb58439de39974bdab5R47-R49

#[extern_spec]
impl<T> std::option::Option<T> {
    #[requires(self.is_some())]
    #[ensures(old(self) === Some(result))]
    pub fn unwrap(self) -> T;

    #[pure]
    #[ensures(result == matches!(self, None))]
    pub const fn is_none(&self) -> bool;

    #[pure]
    #[ensures(result == matches!(self, Some(_)))]
    pub const fn is_some(&self) -> bool;
}

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

    #[pure]
    fn is_empty(&self) -> bool {
        self.head.is_empty()
    }

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

    #[pure]
    #[requires(index < self.len())]
    pub fn lookup(&self, index: usize) -> i32 {
        self.head.lookup(index)
    }

    #[ensures(self.len() == old(self.len()) + 1)]
    #[ensures(self.lookup(0) == elem)]
    #[ensures(forall(|i: usize| (i < old(self.len())) ==>
                 old(self.lookup(i)) == self.lookup(i + 1)))]
    pub fn push(&mut self, elem: i32) {
        let new_node = Box::new(Node {
            elem,
            next: std::mem::replace(&mut self.head, Link::Empty),
        });

        self.head = Link::More(new_node);
    }

    predicate! {
        // two-state predicate to check if the head of a list was correctly removed
        fn head_removed(&self, prev: &Self) -> bool {
            self.len() == prev.len() - 1 // The length will decrease by 1
            && forall(|i: usize| // Every element will be shifted forwards by one
                (1 <= i && i < prev.len())
                    ==> prev.lookup(i) == self.lookup(i - 1))
        }
    }

    #[ensures(old(self.is_empty()) ==>
        result.is_none() &&
        self.is_empty()
    )]
    #[ensures(!old(self.is_empty()) ==>
        self.head_removed(&old(snap(self)))
        &&
        result === Some(old(snap(self)).lookup(0))
    )]
    pub fn try_pop(&mut self) -> Option<i32> {
        // ...
        match std::mem::replace(&mut self.head, Link::Empty) {
            Link::Empty => None,
            Link::More(node) => {
                self.head = node.next;
                Some(node.elem)
            }
        }
    }

    #[requires(!self.is_empty())]
    #[ensures(self.head_removed(&old(snap(self))))]
    #[ensures(result === old(snap(self)).lookup(0))]
    pub fn pop(&mut self) -> i32 {
        // ...
        self.try_pop().unwrap()
    }
}

impl Link {
    #[pure]
    #[requires(index < self.len())]
    pub fn lookup(&self, index: usize) -> i32 {
        match self {
            Link::More(node) => {
                if index == 0 {
                    node.elem
                } else {
                    node.next.lookup(index - 1)
                }
            }
            Link::Empty => unreachable!(),
        }
    }

    #[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)
    }
}

This specification ensures that for empty lists, the list will still be empty afterwards, and try_pop will return None.

Checking if the correct result is returned

Now we can add the specification for checking if the correct result is returned. Like with push, we will use the lookup function to check that result was the first element of the list. For this we call lookup(0) on a snapshot of self before the function call: old(snap(self)).lookup(0).

We can check this condition for snapshot equality (===) with result. This will always hold for pop, since the list is never empty:

// 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,
}

#[extern_spec(std::mem)]
#[ensures(snap(dest) === src)]
#[ensures(result === old(snap(dest)))]
fn replace<T>(dest: &mut T, src: T) -> T;

// Specs for std::option::Option<T>::unwrap(self) (and others) can be found here (work in progress):
// https://github.com/viperproject/prusti-dev/pull/1249/files#diff-bccda07f8a48357687e26408251041072c7470c188092fb58439de39974bdab5R47-R49

#[extern_spec]
impl<T> std::option::Option<T> {
    #[requires(self.is_some())]
    #[ensures(old(self) === Some(result))]
    pub fn unwrap(self) -> T;

    #[pure]
    #[ensures(result == matches!(self, None))]
    pub const fn is_none(&self) -> bool;

    #[pure]
    #[ensures(result == matches!(self, Some(_)))]
    pub const fn is_some(&self) -> bool;
}

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

    #[pure]
    fn is_empty(&self) -> bool {
        self.head.is_empty()
    }

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

    #[pure]
    #[requires(index < self.len())]
    pub fn lookup(&self, index: usize) -> i32 {
        self.head.lookup(index)
    }

    #[ensures(self.len() == old(self.len()) + 1)]
    #[ensures(self.lookup(0) == elem)]
    #[ensures(forall(|i: usize| (i < old(self.len())) ==>
                 old(self.lookup(i)) == self.lookup(i + 1)))]
    pub fn push(&mut self, elem: i32) {
        let new_node = Box::new(Node {
            elem,
            next: std::mem::replace(&mut self.head, Link::Empty),
        });

        self.head = Link::More(new_node);
    }

    predicate! {
        // two-state predicate to check if the head of a list was correctly removed
        fn head_removed(&self, prev: &Self) -> bool {
            self.len() == prev.len() - 1 // The length will decrease by 1
            && forall(|i: usize| // Every element will be shifted forwards by one
                (1 <= i && i < prev.len())
                    ==> prev.lookup(i) == self.lookup(i - 1))
        }
    }

    #[ensures(old(self.is_empty()) ==>
        result.is_none() &&
        self.is_empty()
    )]
    #[ensures(!old(self.is_empty()) ==>
        self.head_removed(&old(snap(self)))
        &&
        result === Some(old(snap(self)).lookup(0))
    )]
    pub fn try_pop(&mut self) -> Option<i32> {
        // ...
        match std::mem::replace(&mut self.head, Link::Empty) {
            Link::Empty => None,
            Link::More(node) => {
                self.head = node.next;
                Some(node.elem)
            }
        }
    }

    #[requires(!self.is_empty())]
    #[ensures(self.head_removed(&old(snap(self))))]
    #[ensures(result === old(snap(self)).lookup(0))]
    pub fn pop(&mut self) -> i32 {
        // ...
        self.try_pop().unwrap()
    }
}

impl Link {
    #[pure]
    #[requires(index < self.len())]
    pub fn lookup(&self, index: usize) -> i32 {
        match self {
            Link::More(node) => {
                if index == 0 {
                    node.elem
                } else {
                    node.next.lookup(index - 1)
                }
            }
            Link::Empty => unreachable!(),
        }
    }

    #[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)
    }
}

For try_pop, the condition only holds if the list was not empty before the call. In addition, the result is an Option::Some, so we will have to include this in our postcondition:

// 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,
}

#[extern_spec(std::mem)]
#[ensures(snap(dest) === src)]
#[ensures(result === old(snap(dest)))]
fn replace<T>(dest: &mut T, src: T) -> T;

// Specs for std::option::Option<T>::unwrap(self) (and others) can be found here (work in progress):
// https://github.com/viperproject/prusti-dev/pull/1249/files#diff-bccda07f8a48357687e26408251041072c7470c188092fb58439de39974bdab5R47-R49

#[extern_spec]
impl<T> std::option::Option<T> {
    #[requires(self.is_some())]
    #[ensures(old(self) === Some(result))]
    pub fn unwrap(self) -> T;

    #[pure]
    #[ensures(result == matches!(self, None))]
    pub const fn is_none(&self) -> bool;

    #[pure]
    #[ensures(result == matches!(self, Some(_)))]
    pub const fn is_some(&self) -> bool;
}

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

    #[pure]
    fn is_empty(&self) -> bool {
        self.head.is_empty()
    }

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

    #[pure]
    #[requires(index < self.len())]
    pub fn lookup(&self, index: usize) -> i32 {
        self.head.lookup(index)
    }

    #[ensures(self.len() == old(self.len()) + 1)]
    #[ensures(self.lookup(0) == elem)]
    #[ensures(forall(|i: usize| (i < old(self.len())) ==>
                 old(self.lookup(i)) == self.lookup(i + 1)))]
    pub fn push(&mut self, elem: i32) {
        let new_node = Box::new(Node {
            elem,
            next: std::mem::replace(&mut self.head, Link::Empty),
        });

        self.head = Link::More(new_node);
    }

    predicate! {
        // two-state predicate to check if the head of a list was correctly removed
        fn head_removed(&self, prev: &Self) -> bool {
            self.len() == prev.len() - 1 // The length will decrease by 1
            && forall(|i: usize| // Every element will be shifted forwards by one
                (1 <= i && i < prev.len())
                    ==> prev.lookup(i) == self.lookup(i - 1))
        }
    }

    #[ensures(old(self.is_empty()) ==>
        result.is_none() &&
        self.is_empty()
    )]
    #[ensures(!old(self.is_empty()) ==>
        self.head_removed(&old(snap(self)))
        &&
        result === Some(old(snap(self)).lookup(0))
    )]
    pub fn try_pop(&mut self) -> Option<i32> {
        // ...
        match std::mem::replace(&mut self.head, Link::Empty) {
            Link::Empty => None,
            Link::More(node) => {
                self.head = node.next;
                Some(node.elem)
            }
        }
    }

    #[requires(!self.is_empty())]
    #[ensures(self.head_removed(&old(snap(self))))]
    #[ensures(result === old(snap(self)).lookup(0))]
    pub fn pop(&mut self) -> i32 {
        // ...
        self.try_pop().unwrap()
    }
}

impl Link {
    #[pure]
    #[requires(index < self.len())]
    pub fn lookup(&self, index: usize) -> i32 {
        match self {
            Link::More(node) => {
                if index == 0 {
                    node.elem
                } else {
                    node.next.lookup(index - 1)
                }
            }
            Link::Empty => unreachable!(),
        }
    }

    #[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)
    }
}

Using predicate! to reduce code duplication

You may have noticed that the last two conditions for pop are the same as the last two of try_pop. We could just write the same conditions twice, but we can also place them in a Prusti predicate, and then use that predicate in both specifications.

A predicate is basically just a pure function that returns a bool, but it can use all the additional syntax available in Prusti specifications. Let's look at an example:

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

predicate! {
    fn larger_than_five(x: i32) -> bool {
        x > 5
    }
}

#[ensures(larger_than_five(result))]
fn ten() -> i32 {
    10
}

In our specific case, we want to have a predicate to compare the state of the list before the call to the state afterwards. The old function cannot be used inside a predicate, so we have to pass the two states as separate arguments. For this we write a predicate with two parameters, which represent the state before and after the function. Such a predicate is also called a "two-state predicate". Note that we take both arguments by (immutable) reference, since we don't need the predicate to take ownership over the arguments:

use prusti_contracts::*;

impl List {
    predicate! {
        // two-state predicate to check if the head of a list was correctly removed
        fn head_removed(&self, prev: &Self) -> bool {
            // ...
        }
    }
}

The two parameters are called self and prev, both with the type &Self.

The goal of this predicate is to check if the head of a list was correctly removed. For this we need check two properties:

1. The new length is the old length minus one.
2. Each element is shifted forwards by one.

We combine these two properties into a single expression using &&:

// 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,
}

#[extern_spec(std::mem)]
#[ensures(snap(dest) === src)]
#[ensures(result === old(snap(dest)))]
fn replace<T>(dest: &mut T, src: T) -> T;

// Specs for std::option::Option<T>::unwrap(self) (and others) can be found here (work in progress):
// https://github.com/viperproject/prusti-dev/pull/1249/files#diff-bccda07f8a48357687e26408251041072c7470c188092fb58439de39974bdab5R47-R49

#[extern_spec]
impl<T> std::option::Option<T> {
    #[requires(self.is_some())]
    #[ensures(old(self) === Some(result))]
    pub fn unwrap(self) -> T;

    #[pure]
    #[ensures(result == matches!(self, None))]
    pub const fn is_none(&self) -> bool;

    #[pure]
    #[ensures(result == matches!(self, Some(_)))]
    pub const fn is_some(&self) -> bool;
}

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

    #[pure]
    fn is_empty(&self) -> bool {
        self.head.is_empty()
    }

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

    #[pure]
    #[requires(index < self.len())]
    pub fn lookup(&self, index: usize) -> i32 {
        self.head.lookup(index)
    }

    #[ensures(self.len() == old(self.len()) + 1)]
    #[ensures(self.lookup(0) == elem)]
    #[ensures(forall(|i: usize| (i < old(self.len())) ==>
                 old(self.lookup(i)) == self.lookup(i + 1)))]
    pub fn push(&mut self, elem: i32) {
        let new_node = Box::new(Node {
            elem,
            next: std::mem::replace(&mut self.head, Link::Empty),
        });

        self.head = Link::More(new_node);
    }

    predicate! {
        // two-state predicate to check if the head of a list was correctly removed
        fn head_removed(&self, prev: &Self) -> bool {
            self.len() == prev.len() - 1 // The length will decrease by 1
            && forall(|i: usize| // Every element will be shifted forwards by one
                (1 <= i && i < prev.len())
                    ==> prev.lookup(i) == self.lookup(i - 1))
        }
    }

    #[ensures(old(self.is_empty()) ==>
        result.is_none() &&
        self.is_empty()
    )]
    #[ensures(!old(self.is_empty()) ==>
        self.head_removed(&old(snap(self)))
        &&
        result === Some(old(snap(self)).lookup(0))
    )]
    pub fn try_pop(&mut self) -> Option<i32> {
        // ...
        match std::mem::replace(&mut self.head, Link::Empty) {
            Link::Empty => None,
            Link::More(node) => {
                self.head = node.next;
                Some(node.elem)
            }
        }
    }

    #[requires(!self.is_empty())]
    #[ensures(self.head_removed(&old(snap(self))))]
    #[ensures(result === old(snap(self)).lookup(0))]
    pub fn pop(&mut self) -> i32 {
        // ...
        self.try_pop().unwrap()
    }
}

impl Link {
    #[pure]
    #[requires(index < self.len())]
    pub fn lookup(&self, index: usize) -> i32 {
        match self {
            Link::More(node) => {
                if index == 0 {
                    node.elem
                } else {
                    node.next.lookup(index - 1)
                }
            }
            Link::Empty => unreachable!(),
        }
    }

    #[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)
    }
}

Here we are able to call .len() and .lookup() on both references, because they are pure functions.

To use this predicate, we call it on the list self, and then pass in a snapshot of the self from before the function call. Like with the condition for correctness of the result, we can just add this predicate to pop, but we need to restrict it to non-empty lists for try_pop:

// 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,
}

#[extern_spec(std::mem)]
#[ensures(snap(dest) === src)]
#[ensures(result === old(snap(dest)))]
fn replace<T>(dest: &mut T, src: T) -> T;

// Specs for std::option::Option<T>::unwrap(self) (and others) can be found here (work in progress):
// https://github.com/viperproject/prusti-dev/pull/1249/files#diff-bccda07f8a48357687e26408251041072c7470c188092fb58439de39974bdab5R47-R49

#[extern_spec]
impl<T> std::option::Option<T> {
    #[requires(self.is_some())]
    #[ensures(old(self) === Some(result))]
    pub fn unwrap(self) -> T;

    #[pure]
    #[ensures(result == matches!(self, None))]
    pub const fn is_none(&self) -> bool;

    #[pure]
    #[ensures(result == matches!(self, Some(_)))]
    pub const fn is_some(&self) -> bool;
}

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

    #[pure]
    fn is_empty(&self) -> bool {
        self.head.is_empty()
    }

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

    #[pure]
    #[requires(index < self.len())]
    pub fn lookup(&self, index: usize) -> i32 {
        self.head.lookup(index)
    }

    #[ensures(self.len() == old(self.len()) + 1)]
    #[ensures(self.lookup(0) == elem)]
    #[ensures(forall(|i: usize| (i < old(self.len())) ==>
                 old(self.lookup(i)) == self.lookup(i + 1)))]
    pub fn push(&mut self, elem: i32) {
        let new_node = Box::new(Node {
            elem,
            next: std::mem::replace(&mut self.head, Link::Empty),
        });

        self.head = Link::More(new_node);
    }

    predicate! {
        // two-state predicate to check if the head of a list was correctly removed
        fn head_removed(&self, prev: &Self) -> bool {
            self.len() == prev.len() - 1 // The length will decrease by 1
            && forall(|i: usize| // Every element will be shifted forwards by one
                (1 <= i && i < prev.len())
                    ==> prev.lookup(i) == self.lookup(i - 1))
        }
    }

    #[ensures(old(self.is_empty()) ==>
        result.is_none() &&
        self.is_empty()
    )]
    #[ensures(!old(self.is_empty()) ==>
        self.head_removed(&old(snap(self)))
        &&
        result === Some(old(snap(self)).lookup(0))
    )]
    pub fn try_pop(&mut self) -> Option<i32> {
        // ...
        match std::mem::replace(&mut self.head, Link::Empty) {
            Link::Empty => None,
            Link::More(node) => {
                self.head = node.next;
                Some(node.elem)
            }
        }
    }

    #[requires(!self.is_empty())]
    #[ensures(self.head_removed(&old(snap(self))))]
    #[ensures(result === old(snap(self)).lookup(0))]
    pub fn pop(&mut self) -> i32 {
        // ...
        self.try_pop().unwrap()
    }
}

impl Link {
    #[pure]
    #[requires(index < self.len())]
    pub fn lookup(&self, index: usize) -> i32 {
        match self {
            Link::More(node) => {
                if index == 0 {
                    node.elem
                } else {
                    node.next.lookup(index - 1)
                }
            }
            Link::Empty => unreachable!(),
        }
    }

    #[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)
    }
}

Prusti can now successfully verify the postconditions of both try_pop and pop, and ensure that they will not panic! But there might still be a chance that our specifications don't fully match what we expect the code to do, so we will look at how to test specifications in the next chapter.

Full Code Listing

// 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,
}

#[extern_spec(std::mem)]
#[ensures(snap(dest) === src)]
#[ensures(result === old(snap(dest)))]
fn replace<T>(dest: &mut T, src: T) -> T;

// Specs for std::option::Option<T>::unwrap(self) (and others) can be found here (work in progress):
// https://github.com/viperproject/prusti-dev/pull/1249/files#diff-bccda07f8a48357687e26408251041072c7470c188092fb58439de39974bdab5R47-R49

#[extern_spec]
impl<T> std::option::Option<T> {
    #[requires(self.is_some())]
    #[ensures(old(self) === Some(result))]
    pub fn unwrap(self) -> T;

    #[pure]
    #[ensures(result == matches!(self, None))]
    pub const fn is_none(&self) -> bool;

    #[pure]
    #[ensures(result == matches!(self, Some(_)))]
    pub const fn is_some(&self) -> bool;
}

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

    #[pure]
    fn is_empty(&self) -> bool {
        self.head.is_empty()
    }

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

    #[pure]
    #[requires(index < self.len())]
    pub fn lookup(&self, index: usize) -> i32 {
        self.head.lookup(index)
    }

    #[ensures(self.len() == old(self.len()) + 1)]
    #[ensures(self.lookup(0) == elem)]
    #[ensures(forall(|i: usize| (i < old(self.len())) ==>
                 old(self.lookup(i)) == self.lookup(i + 1)))]
    pub fn push(&mut self, elem: i32) {
        let new_node = Box::new(Node {
            elem,
            next: std::mem::replace(&mut self.head, Link::Empty),
        });

        self.head = Link::More(new_node);
    }

    predicate! {
        // two-state predicate to check if the head of a list was correctly removed
        fn head_removed(&self, prev: &Self) -> bool {
            self.len() == prev.len() - 1 // The length will decrease by 1
            && forall(|i: usize| // Every element will be shifted forwards by one
                (1 <= i && i < prev.len())
                    ==> prev.lookup(i) == self.lookup(i - 1))
        }
    }

    #[ensures(old(self.is_empty()) ==>
        result.is_none() &&
        self.is_empty()
    )]
    #[ensures(!old(self.is_empty()) ==>
        self.head_removed(&old(snap(self)))
        &&
        result === Some(old(snap(self)).lookup(0))
    )]
    pub fn try_pop(&mut self) -> Option<i32> {
        // ...
        match std::mem::replace(&mut self.head, Link::Empty) {
            Link::Empty => None,
            Link::More(node) => {
                self.head = node.next;
                Some(node.elem)
            }
        }
    }

    #[requires(!self.is_empty())]
    #[ensures(self.head_removed(&old(snap(self))))]
    #[ensures(result === old(snap(self)).lookup(0))]
    pub fn pop(&mut self) -> i32 {
        // ...
        self.try_pop().unwrap()
    }
}

impl Link {
    #[pure]
    #[requires(index < self.len())]
    pub fn lookup(&self, index: usize) -> i32 {
        match self {
            Link::More(node) => {
                if index == 0 {
                    node.elem
                } else {
                    node.next.lookup(index - 1)
                }
            }
            Link::Empty => unreachable!(),
        }
    }

    #[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)
    }
}

Testing

Recommended reading: 2.6: Testing,

The linked chapter in the "Learning Rust With Entirely Too Many Linked Lists" tutorial explains how testing normal Rust code works. In this chapter we will show some differences between testing and verification and of the guarantees that each provides.

Note: Normal tests (marked with #[cfg(test)] or #[test]) are currently not checked by Prusti, but this may be added in the future. If you remove the test markers, Prusti will check any test like it would a normal function.

Differing guarantees of verification and testing

Static verification has stronger guarantees than testing. Running tests is only be possible for a small subset of all possible input values. Take as an example a function taking a single value of type u64. The range of potential inputs is 0 to 2^64 - 1, or 2^64 total values. Assuming each value takes 1 nano-second to test, it would take approximately 584.5 years to exhaustively test just this single function.

In contrast, a static verifier like Prusti is able to check the entire input space of a function with the help of the specifications of each function.

When verification succeeds, you are guaranteed to not have a bug like a crash, overflow, or return value not fitting the specification. This assumes that you have manually verified any #[trusted] functions and have checked for correct termination of all functions. If the verification fails, you may have a bug, or your specifications are not strong enough.

The guarantees of testing are different. If a test fails, you know that you have a bug (either in the code or the test), but if all your tests pass, you might still have some bugs, just not with the specific inputs used in the tests.

In other words: Testing can show the presence of bugs, verification can show the absence of bugs.

It might still be worth writing (and running) some unit tests even for verified code, as they can serve as documentation on using a function. If you made some mistake in both the code and the specification, you may notice it if you write a test for it or use that function in another verified function.

The next section shows some potential issues with specifications.

Examples of bugs in specifications

The specification for a function could have a precondition that is too restrictive. If you never use the function in another verified function, you may not notice this:

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

fn main() {}

#[requires(x == 10)] // Restrictive precondition
#[ensures(result == x * x)]
pub fn restrictive_square(x: i32) -> i32 {
    x * x
}

fn test() {
    assert!(restrictive_square(10) == 100); // Works
    assert!(restrictive_square(5) == 25); //~ ERROR precondition might not hold.
}

This function is correct (ignoring potential overflows), but it is not useful, since the input must be 10.

Another potential problem could be an incomplete postcondition. The abs function below should return the absolute value of x, but it only works for positive values. The verification will still succeed, because the postcondition does not specify the result for x < 0:

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

fn main() {}

#[pure]
// Note that a postcondition is not actually needed here, since `abs` is #[pure]
#[ensures(x >= 0 ==> result == x)]
pub fn abs(x: i32) -> i32 {
    x
}

fn test_abs() {
    prusti_assert!(abs(8) == 8); // Works
    prusti_assert!(abs(-10) == 10); //~ ERROR the asserted expression might not hold
}

This bug will be noticed as soon as you try using abs with a negative input. For functions internal to a project, you will likely notice mistakes in the specification when you try to use the function in other code. However, when you have public functions, like for example in a library, you might want to write some test functions for your specification. Specification errors sometimes only show up when they are actually used.

Testing our linked list specifications

To check our specifications and code, we could write a function that relies on the expected behavior. We can create a new namespace for the test, here we call it prusti_tests:

// 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,
}

#[extern_spec(std::mem)]
#[ensures(snap(dest) === src)]
#[ensures(result === old(snap(dest)))]
fn replace<T>(dest: &mut T, src: T) -> T;

// Specs for std::option::Option<T>::unwrap(self) (and others) can be found here (work in progress):
// https://github.com/viperproject/prusti-dev/pull/1249/files#diff-bccda07f8a48357687e26408251041072c7470c188092fb58439de39974bdab5R47-R49

#[extern_spec]
impl<T> std::option::Option<T> {
    #[requires(self.is_some())]
    #[ensures(old(self) === Some(result))]
    pub fn unwrap(self) -> T;
    
    #[pure]
    #[ensures(result == matches!(self, None))]
    pub const fn is_none(&self) -> bool;

    #[pure]
    #[ensures(result == matches!(self, Some(_)))]
    pub const fn is_some(&self) -> bool;
}

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

    #[pure]
    fn is_empty(&self) -> bool {
        self.head.is_empty()
    }

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

    #[pure]
    #[requires(index < self.len())]
    pub fn lookup(&self, index: usize) -> i32 {
        self.head.lookup(index)
    }

    #[ensures(self.len() == old(self.len()) + 1)]
    #[ensures(self.lookup(0) == elem)]
    #[ensures(forall(|i: usize| (i < old(self.len())) ==>
                 old(self.lookup(i)) == self.lookup(i + 1)))]
    pub fn push(&mut self, elem: i32) {
        let new_node = Box::new(Node {
            elem,
            next: std::mem::replace(&mut self.head, Link::Empty),
        });

        self.head = Link::More(new_node);
    }

    predicate! {
        // two-state predicate to check if the head of a list was correctly removed
        fn head_removed(&self, prev: &Self) -> bool {
            self.len() == prev.len() - 1 // The length will decrease by 1
            && forall(|i: usize| // Every element will be shifted forwards by one
                (1 <= i && i < prev.len())
                    ==> prev.lookup(i) == self.lookup(i - 1))
        }
    }

    #[ensures(old(self.is_empty()) ==>
        result.is_none() &&
        self.is_empty()
    )]
    #[ensures(!old(self.is_empty()) ==>
        self.head_removed(&old(snap(self)))
        &&
        result === Some(old(snap(self)).lookup(0))
    )]
    pub fn try_pop(&mut self) -> Option<i32> {
        match std::mem::replace(&mut self.head, Link::Empty) {
            Link::Empty => None,
            Link::More(node) => {
                self.head = node.next;
                Some(node.elem)
            }
        }
    }

    #[requires(!self.is_empty())]
    #[ensures(self.head_removed(&old(snap(self))))]
    #[ensures(result === old(snap(self)).lookup(0))]
    pub fn pop(&mut self) -> i32 {
        self.try_pop().unwrap()
    }
}

impl Link {
    #[pure]
    #[requires(index < self.len())]
    pub fn lookup(&self, index: usize) -> i32 {
        match self {
            Link::More(node) => {
                if index == 0 {
                    node.elem
                } else {
                    node.next.lookup(index - 1)
                }
            }
            Link::Empty => unreachable!(),
        }
    }

    #[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)
    }
}

#[cfg(prusti)]
mod prusti_tests {
    use super::*;

    fn _test_list(){
        let mut list = List::new(); // create an new, empty list
        prusti_assert!(list.is_empty() && list.len() == 0); // list should be empty

        list.push(5);
        list.push(10);
        prusti_assert!(!list.is_empty() && list.len() == 2); // length correct
        prusti_assert!(list.lookup(0) == 10); // head is 10
        prusti_assert!(list.lookup(1) == 5); // 5 got pushed back correctly

        let x = list.pop();
        prusti_assert!(x == 10); // pop returns the value that was added last

        match list.try_pop() {
            Some(y) => assert!(y == 5),
            None => unreachable!()
        }

        let z = list.try_pop();
        prusti_assert!(list.is_empty() && list.len() == 0); // length correct
        prusti_assert!(z.is_none()); // `try_pop` on an empty list should return `None`
    }

    // This shows a test that takes 2 lists as input parameters:
    #[requires(list_0.len() >= 4)]
    #[requires(!list_1.is_empty())]
    #[requires(list_0.lookup(1) == 42)]
    #[requires(list_0.lookup(3) == list_1.lookup(0))]
    fn _test_lists(list_0: &mut List, list_1: &mut List) {
        let x0 = list_0.pop();

        list_0.push(10);
        prusti_assert!(list_0.len() >= 4);
        prusti_assert!(list_0.lookup(1) == 42);
        assert!(list_0.pop() == 10); // Cannot be `prusti_assert`, `pop` changes the list

        let x1 = list_0.pop();
        let x2 = list_0.pop();
        let x3 = list_0.pop();
        prusti_assert!(x0 == old(snap(list_0)).lookup(0));
        prusti_assert!(x1 == old(snap(list_0)).lookup(1) && x1 == 42);
        prusti_assert!(x2 == old(snap(list_0)).lookup(2));
        prusti_assert!(x3 == old(snap(list_0)).lookup(3));
        
        let y0 = list_1.pop();
        prusti_assert!(y0 == old(snap(list_1)).lookup(0));
        prusti_assert!(y0 == x3);
    }
}
// Prusti: verifies

Note the #[cfg(prusti)] on the module prusti_tests. This makes the module only available during verification, with no effect during normal compilation, similar to #[cfg(test)] for unit tests.

Our test code can be verified, so it appears that our specification is not too restrictive or incomplete.

Options

Recommended reading: 3: An Ok Single-Linked Stack, 3.1. Option

Just like in the "Learning Rust With Entirely Too Many Linked Lists" tutorial, we can change our enum Link to use the Option type via a type alias instead of manually implementing Empty and More:

type Link = Option<Box<Node>>;

In order to use the Option::take function, we also have to implement the extern_spec for it. As you can see, it is quite similar to the extern_spec for mem::replace, since take does the same as replace(&mut self, None):

// 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,
}

type Link = Option<Box<Node>>;

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

#[extern_spec(std::mem)]
#[ensures(snap(dest) === src)]
#[ensures(result === old(snap(dest)))]
fn replace<T>(dest: &mut T, src: T) -> T;

// Specs for std::option::Option<T>::unwrap(self) (and others) can be found here (work in progress):
// https://github.com/viperproject/prusti-dev/pull/1249/files#diff-bccda07f8a48357687e26408251041072c7470c188092fb58439de39974bdab5R47-R49

#[extern_spec]
impl<T> std::option::Option<T> {
    #[requires(self.is_some())]
    #[ensures(old(self) === Some(result))]
    pub fn unwrap(self) -> T;
    
    #[pure]
    #[ensures(result == matches!(self, None))]
    pub const fn is_none(&self) -> bool;

    #[pure]
    #[ensures(result == matches!(self, Some(_)))]
    pub const fn is_some(&self) -> bool;

    #[ensures(result === old(snap(self)))]
    #[ensures(self.is_none())]
    pub fn take(&mut self) -> Option<T>;
}

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

    #[pure]
    fn is_empty(&self) -> bool {
        matches!(self.head, None)
    }

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

    #[pure]
    #[requires(index < self.len())]
    pub fn lookup(&self, index: usize) -> i32 {
        link_lookup(&self.head, index)
    }

    #[ensures(self.len() == old(self.len()) + 1)]
    #[ensures(self.lookup(0) == elem)]
    #[ensures(forall(|i: usize| (i < old(self.len())) ==>
                 old(self.lookup(i)) == self.lookup(i + 1)))]
    pub fn push(&mut self, elem: i32) {
        let new_node = Box::new(Node {
            elem,
            next: self.head.take(),
        });

        self.head = Some(new_node);
    }

    predicate! {
        // two-state predicate to check if the head of a list was correctly removed
        fn head_removed(&self, prev: &Self) -> bool {
            self.len() == prev.len() - 1 // The length will decrease by 1
            && forall(|i: usize| // Every element will be shifted forwards by one
                (1 <= i && i < prev.len())
                    ==> prev.lookup(i) == self.lookup(i - 1))
        }
    }

    #[ensures(old(self.is_empty()) ==>
        result.is_none() &&
        self.is_empty()
    )]
    #[ensures(!old(self.is_empty()) ==>
        self.head_removed(&old(snap(self)))
        &&
        result === Some(old(snap(self)).lookup(0))
    )]
    pub fn try_pop(&mut self) -> Option<i32> {
        match self.head.take() { // Replace mem::swap with the buildin Option::take
            None => None,
            Some(node) => {
                self.head = node.next;
                Some(node.elem)
            }
        }
    }
    
    // // This will likely work in the future, but doesn't currently (even if you provide an `extern_spec` for `Option::map`):
    // // Currently you get this error:
    // //     [Prusti: unsupported feature] unsupported creation of unique borrows (implicitly created in closure bindings)
    // pub fn try_pop(&mut self) -> Option<i32> {
    //     let tmp = self.head.take();
    //     tmp.map(move |node| {
    //         self.head = node.next;
    //         node.elem
    //     })
    // }

    #[requires(!self.is_empty())]
    #[ensures(self.head_removed(&old(snap(self))))]
    #[ensures(result === old(snap(self)).lookup(0))]
    pub fn pop(&mut self) -> i32 {
        self.try_pop().unwrap()
    }
}

#[pure]
#[requires(index < link_len(link))]
fn link_lookup(link: &Link, index: usize) -> i32 {
    match link {
        Some(node) => {
            if index == 0 {
                node.elem
            } else {
                link_lookup(&node.next, index - 1)
            }
        }
        None => unreachable!(),
    }
}

#[pure]
fn link_len(link: &Link) -> usize {
    match link {
        None => 0,
        Some(node) => 1 + link_len(&node.next),
    }
}

#[cfg(prusti)]
mod prusti_tests {
    use super::*;

    fn _test_list(){
        let mut list = List::new(); // create an new, empty list
        prusti_assert!(list.is_empty() && list.len() == 0); // list should be empty

        list.push(5);
        list.push(10);
        prusti_assert!(!list.is_empty() && list.len() == 2); // length correct
        prusti_assert!(list.lookup(0) == 10); // head is 10
        prusti_assert!(list.lookup(1) == 5); // 5 got pushed back correctly

        let x = list.pop();
        prusti_assert!(x == 10); // pop returns the value that was added last

        match list.try_pop() {
            Some(y) => assert!(y == 5),
            None => unreachable!()
        }

        let z = list.try_pop();
        prusti_assert!(list.is_empty() && list.len() == 0); // length correct
        prusti_assert!(z.is_none()); // `try_pop` on an empty list should return `None`
    }
}

Changing the Link type requires some adjustments of the code and specifications. With the new type alias for Link, we cannot have an impl Link block anymore, so our lookup and len functions on Link are now normal, free-standing functions:

// 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,
}

type Link = Option<Box<Node>>;

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

#[extern_spec(std::mem)]
#[ensures(snap(dest) === src)]
#[ensures(result === old(snap(dest)))]
fn replace<T>(dest: &mut T, src: T) -> T;

// Specs for std::option::Option<T>::unwrap(self) (and others) can be found here (work in progress):
// https://github.com/viperproject/prusti-dev/pull/1249/files#diff-bccda07f8a48357687e26408251041072c7470c188092fb58439de39974bdab5R47-R49

#[extern_spec]
impl<T> std::option::Option<T> {
    #[requires(self.is_some())]
    #[ensures(old(self) === Some(result))]
    pub fn unwrap(self) -> T;
    
    #[pure]
    #[ensures(result == matches!(self, None))]
    pub const fn is_none(&self) -> bool;

    #[pure]
    #[ensures(result == matches!(self, Some(_)))]
    pub const fn is_some(&self) -> bool;

    #[ensures(result === old(snap(self)))]
    #[ensures(self.is_none())]
    pub fn take(&mut self) -> Option<T>;
}

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

    #[pure]
    fn is_empty(&self) -> bool {
        matches!(self.head, None)
    }

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

    #[pure]
    #[requires(index < self.len())]
    pub fn lookup(&self, index: usize) -> i32 {
        link_lookup(&self.head, index)
    }

    #[ensures(self.len() == old(self.len()) + 1)]
    #[ensures(self.lookup(0) == elem)]
    #[ensures(forall(|i: usize| (i < old(self.len())) ==>
                 old(self.lookup(i)) == self.lookup(i + 1)))]
    pub fn push(&mut self, elem: i32) {
        let new_node = Box::new(Node {
            elem,
            next: self.head.take(),
        });

        self.head = Some(new_node);
    }

    predicate! {
        // two-state predicate to check if the head of a list was correctly removed
        fn head_removed(&self, prev: &Self) -> bool {
            self.len() == prev.len() - 1 // The length will decrease by 1
            && forall(|i: usize| // Every element will be shifted forwards by one
                (1 <= i && i < prev.len())
                    ==> prev.lookup(i) == self.lookup(i - 1))
        }
    }

    #[ensures(old(self.is_empty()) ==>
        result.is_none() &&
        self.is_empty()
    )]
    #[ensures(!old(self.is_empty()) ==>
        self.head_removed(&old(snap(self)))
        &&
        result === Some(old(snap(self)).lookup(0))
    )]
    pub fn try_pop(&mut self) -> Option<i32> {
        match self.head.take() { // Replace mem::swap with the buildin Option::take
            None => None,
            Some(node) => {
                self.head = node.next;
                Some(node.elem)
            }
        }
    }
    
    // // This will likely work in the future, but doesn't currently (even if you provide an `extern_spec` for `Option::map`):
    // // Currently you get this error:
    // //     [Prusti: unsupported feature] unsupported creation of unique borrows (implicitly created in closure bindings)
    // pub fn try_pop(&mut self) -> Option<i32> {
    //     let tmp = self.head.take();
    //     tmp.map(move |node| {
    //         self.head = node.next;
    //         node.elem
    //     })
    // }

    #[requires(!self.is_empty())]
    #[ensures(self.head_removed(&old(snap(self))))]
    #[ensures(result === old(snap(self)).lookup(0))]
    pub fn pop(&mut self) -> i32 {
        self.try_pop().unwrap()
    }
}

#[pure]
#[requires(index < link_len(link))]
fn link_lookup(link: &Link, index: usize) -> i32 {
    match link {
        Some(node) => {
            if index == 0 {
                node.elem
            } else {
                link_lookup(&node.next, index - 1)
            }
        }
        None => unreachable!(),
    }
}

#[pure]
fn link_len(link: &Link) -> usize {
    match link {
        None => 0,
        Some(node) => 1 + link_len(&node.next),
    }
}

#[cfg(prusti)]
mod prusti_tests {
    use super::*;

    fn _test_list(){
        let mut list = List::new(); // create an new, empty list
        prusti_assert!(list.is_empty() && list.len() == 0); // list should be empty

        list.push(5);
        list.push(10);
        prusti_assert!(!list.is_empty() && list.len() == 2); // length correct
        prusti_assert!(list.lookup(0) == 10); // head is 10
        prusti_assert!(list.lookup(1) == 5); // 5 got pushed back correctly

        let x = list.pop();
        prusti_assert!(x == 10); // pop returns the value that was added last

        match list.try_pop() {
            Some(y) => assert!(y == 5),
            None => unreachable!()
        }

        let z = list.try_pop();
        prusti_assert!(list.is_empty() && list.len() == 0); // length correct
        prusti_assert!(z.is_none()); // `try_pop` on an empty list should return `None`
    }
}

Due to current limitations of Prusti, we cannot replace our link_len and link_lookup functions with loops:

// ignore-test: This code causes Prusti to panic
// The next and previous line are only required for (doc)tests, you can ignore/remove it
extern crate prusti_contracts;
use prusti_contracts::*;

fn main() {}

pub struct List {
    head: Link,
}

type Link = Option<Box<Node>>;

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

impl List {
    // Prusti cannot verify these functions at the moment,
    // since loops in pure functions are not yet supported:
    #[pure]
    pub fn len(&self) -> usize {
        let mut curr = &self.head;
        let mut i = 0;
        while let Some(node) = curr {
            body_invariant!(true);
            i += 1;
            curr = &node.next;
        }
        i
    }

    #[pure]
    #[requires(index < self.len())]
    pub fn lookup(&self, index: usize) -> i32 {
        let mut curr = &self.head;
        let mut i = index;
        while let Some(node) = curr {
            body_invariant!(true);
            if i == 0 {
                return node.elem;
            }
            i -= 1;
            curr = &node.next;
        }
        unreachable!()
    }
}

Since Prusti doesn't fully support closures yet, we also cannot do the rewrite to use the Option::map 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,
}

type Link = Option<Box<Node>>;

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

#[extern_spec(std::mem)]
#[ensures(snap(dest) === src)]
#[ensures(result === old(snap(dest)))]
fn replace<T>(dest: &mut T, src: T) -> T;

// Specs for std::option::Option<T>::unwrap(self) (and others) can be found here (work in progress):
// https://github.com/viperproject/prusti-dev/pull/1249/files#diff-bccda07f8a48357687e26408251041072c7470c188092fb58439de39974bdab5R47-R49

#[extern_spec]
impl<T> std::option::Option<T> {
    #[requires(self.is_some())]
    #[ensures(old(self) === Some(result))]
    pub fn unwrap(self) -> T;
    
    #[pure]
    #[ensures(result == matches!(self, None))]
    pub const fn is_none(&self) -> bool;

    #[pure]
    #[ensures(result == matches!(self, Some(_)))]
    pub const fn is_some(&self) -> bool;

    #[ensures(result === old(snap(self)))]
    #[ensures(self.is_none())]
    pub fn take(&mut self) -> Option<T>;
}

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

    #[pure]
    fn is_empty(&self) -> bool {
        matches!(self.head, None)
    }

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

    #[pure]
    #[requires(index < self.len())]
    pub fn lookup(&self, index: usize) -> i32 {
        link_lookup(&self.head, index)
    }

    #[ensures(self.len() == old(self.len()) + 1)]
    #[ensures(self.lookup(0) == elem)]
    #[ensures(forall(|i: usize| (i < old(self.len())) ==>
                 old(self.lookup(i)) == self.lookup(i + 1)))]
    pub fn push(&mut self, elem: i32) {
        let new_node = Box::new(Node {
            elem,
            next: self.head.take(),
        });

        self.head = Some(new_node);
    }

    predicate! {
        // two-state predicate to check if the head of a list was correctly removed
        fn head_removed(&self, prev: &Self) -> bool {
            self.len() == prev.len() - 1 // The length will decrease by 1
            && forall(|i: usize| // Every element will be shifted forwards by one
                (1 <= i && i < prev.len())
                    ==> prev.lookup(i) == self.lookup(i - 1))
        }
    }

    #[ensures(old(self.is_empty()) ==>
        result.is_none() &&
        self.is_empty()
    )]
    #[ensures(!old(self.is_empty()) ==>
        self.head_removed(&old(snap(self)))
        &&
        result === Some(old(snap(self)).lookup(0))
    )]
    pub fn try_pop(&mut self) -> Option<i32> {
        match self.head.take() { // Replace mem::swap with the buildin Option::take
            None => None,
            Some(node) => {
                self.head = node.next;
                Some(node.elem)
            }
        }
    }
    
    // // This will likely work in the future, but doesn't currently (even if you provide an `extern_spec` for `Option::map`):
    // // Currently you get this error:
    // //     [Prusti: unsupported feature] unsupported creation of unique borrows (implicitly created in closure bindings)
    // pub fn try_pop(&mut self) -> Option<i32> {
    //     let tmp = self.head.take();
    //     tmp.map(move |node| {
    //         self.head = node.next;
    //         node.elem
    //     })
    // }

    #[requires(!self.is_empty())]
    #[ensures(self.head_removed(&old(snap(self))))]
    #[ensures(result === old(snap(self)).lookup(0))]
    pub fn pop(&mut self) -> i32 {
        self.try_pop().unwrap()
    }
}

#[pure]
#[requires(index < link_len(link))]
fn link_lookup(link: &Link, index: usize) -> i32 {
    match link {
        Some(node) => {
            if index == 0 {
                node.elem
            } else {
                link_lookup(&node.next, index - 1)
            }
        }
        None => unreachable!(),
    }
}

#[pure]
fn link_len(link: &Link) -> usize {
    match link {
        None => 0,
        Some(node) => 1 + link_len(&node.next),
    }
}

#[cfg(prusti)]
mod prusti_tests {
    use super::*;

    fn _test_list(){
        let mut list = List::new(); // create an new, empty list
        prusti_assert!(list.is_empty() && list.len() == 0); // list should be empty

        list.push(5);
        list.push(10);
        prusti_assert!(!list.is_empty() && list.len() == 2); // length correct
        prusti_assert!(list.lookup(0) == 10); // head is 10
        prusti_assert!(list.lookup(1) == 5); // 5 got pushed back correctly

        let x = list.pop();
        prusti_assert!(x == 10); // pop returns the value that was added last

        match list.try_pop() {
            Some(y) => assert!(y == 5),
            None => unreachable!()
        }

        let z = list.try_pop();
        prusti_assert!(list.is_empty() && list.len() == 0); // length correct
        prusti_assert!(z.is_none()); // `try_pop` on an empty list should return `None`
    }
}

After all the changes done in this chapter, Prusti is still be able to verify the code, so we didn't break anything. If you want to see the full code after all the changes, expand the following code block.

// 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,
}

type Link = Option<Box<Node>>;

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

#[extern_spec(std::mem)]
#[ensures(snap(dest) === src)]
#[ensures(result === old(snap(dest)))]
fn replace<T>(dest: &mut T, src: T) -> T;

// Specs for std::option::Option<T>::unwrap(self) (and others) can be found here (work in progress):
// https://github.com/viperproject/prusti-dev/pull/1249/files#diff-bccda07f8a48357687e26408251041072c7470c188092fb58439de39974bdab5R47-R49

#[extern_spec]
impl<T> std::option::Option<T> {
    #[requires(self.is_some())]
    #[ensures(old(self) === Some(result))]
    pub fn unwrap(self) -> T;
    
    #[pure]
    #[ensures(result == matches!(self, None))]
    pub const fn is_none(&self) -> bool;

    #[pure]
    #[ensures(result == matches!(self, Some(_)))]
    pub const fn is_some(&self) -> bool;

    #[ensures(result === old(snap(self)))]
    #[ensures(self.is_none())]
    pub fn take(&mut self) -> Option<T>;
}

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

    #[pure]
    fn is_empty(&self) -> bool {
        matches!(self.head, None)
    }

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

    #[pure]
    #[requires(index < self.len())]
    pub fn lookup(&self, index: usize) -> i32 {
        link_lookup(&self.head, index)
    }

    #[ensures(self.len() == old(self.len()) + 1)]
    #[ensures(self.lookup(0) == elem)]
    #[ensures(forall(|i: usize| (i < old(self.len())) ==>
                 old(self.lookup(i)) == self.lookup(i + 1)))]
    pub fn push(&mut self, elem: i32) {
        let new_node = Box::new(Node {
            elem,
            next: self.head.take(),
        });

        self.head = Some(new_node);
    }

    predicate! {
        // two-state predicate to check if the head of a list was correctly removed
        fn head_removed(&self, prev: &Self) -> bool {
            self.len() == prev.len() - 1 // The length will decrease by 1
            && forall(|i: usize| // Every element will be shifted forwards by one
                (1 <= i && i < prev.len())
                    ==> prev.lookup(i) == self.lookup(i - 1))
        }
    }

    #[ensures(old(self.is_empty()) ==>
        result.is_none() &&
        self.is_empty()
    )]
    #[ensures(!old(self.is_empty()) ==>
        self.head_removed(&old(snap(self)))
        &&
        result === Some(old(snap(self)).lookup(0))
    )]
    pub fn try_pop(&mut self) -> Option<i32> {
        match self.head.take() { // Replace mem::swap with the buildin Option::take
            None => None,
            Some(node) => {
                self.head = node.next;
                Some(node.elem)
            }
        }
    }
    
    // // This will likely work in the future, but doesn't currently (even if you provide an `extern_spec` for `Option::map`):
    // // Currently you get this error:
    // //     [Prusti: unsupported feature] unsupported creation of unique borrows (implicitly created in closure bindings)
    // pub fn try_pop(&mut self) -> Option<i32> {
    //     let tmp = self.head.take();
    //     tmp.map(move |node| {
    //         self.head = node.next;
    //         node.elem
    //     })
    // }

    #[requires(!self.is_empty())]
    #[ensures(self.head_removed(&old(snap(self))))]
    #[ensures(result === old(snap(self)).lookup(0))]
    pub fn pop(&mut self) -> i32 {
        self.try_pop().unwrap()
    }
}

#[pure]
#[requires(index < link_len(link))]
fn link_lookup(link: &Link, index: usize) -> i32 {
    match link {
        Some(node) => {
            if index == 0 {
                node.elem
            } else {
                link_lookup(&node.next, index - 1)
            }
        }
        None => unreachable!(),
    }
}

#[pure]
fn link_len(link: &Link) -> usize {
    match link {
        None => 0,
        Some(node) => 1 + link_len(&node.next),
    }
}

#[cfg(prusti)]
mod prusti_tests {
    use super::*;

    fn _test_list(){
        let mut list = List::new(); // create an new, empty list
        prusti_assert!(list.is_empty() && list.len() == 0); // list should be empty

        list.push(5);
        list.push(10);
        prusti_assert!(!list.is_empty() && list.len() == 2); // length correct
        prusti_assert!(list.lookup(0) == 10); // head is 10
        prusti_assert!(list.lookup(1) == 5); // 5 got pushed back correctly

        let x = list.pop();
        prusti_assert!(x == 10); // pop returns the value that was added last

        match list.try_pop() {
            Some(y) => assert!(y == 5),
            None => unreachable!()
        }

        let z = list.try_pop();
        prusti_assert!(list.is_empty() && list.len() == 0); // length correct
        prusti_assert!(z.is_none()); // `try_pop` on an empty list should return `None`
    }
}

Making it all Generic

Recommended reading: 3.2: Generic

Just like the corresponding chapter in the "Learning Rust With Entirely Too Many Linked Lists" book, we will change our list to have a generic element type T, not just i32. For this, we go through our code an add the generic parameter T where required. The compiler really helps for this, since it will mark where a generic parameter is needed. If you do this process with Prusti, at some point you will encounter the following error:

[E0369] binary operation `==` cannot be applied to type `T`.

This is because the generic type T might not implement PartialEq and thus not have an equality function == that could be called on it like i32 does. Since we only used == inside of specifications, we can fix this problems by using snapshot equality === instead.

Here you can see where some of the changes were done (expand to see the full changes):

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

fn main() {}

// Make the types generic:
pub struct List<T> {
    head: Link<T>,
}

type Link<T> = Option<Box<Node<T>>>;

struct Node<T> {
    elem: T,
    next: Link<T>,
}

#[extern_spec(std::mem)]
#[ensures(snap(dest) === src)]
#[ensures(result === old(snap(dest)))]
fn replace<T>(dest: &mut T, src: T) -> T;

// Specs for std::option::Option<T>::unwrap(self) (and others) can be found here (work in progress):
// https://github.com/viperproject/prusti-dev/pull/1249/files#diff-bccda07f8a48357687e26408251041072c7470c188092fb58439de39974bdab5R47-R49

#[extern_spec]
impl<T> std::option::Option<T> {
    #[requires(self.is_some())]
    #[ensures(old(self) === Some(result))]
    pub fn unwrap(self) -> T;
    
    #[pure]
    #[ensures(result == matches!(self, None))]
    pub const fn is_none(&self) -> bool;

    #[pure]
    #[ensures(result == matches!(self, Some(_)))]
    pub const fn is_some(&self) -> bool;

    #[ensures(result === old(snap(self)))]
    #[ensures(self.is_none())]
    pub fn take(&mut self) -> Option<T>;
}

impl<T> List<T> {
    // ...

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

    #[pure]
    fn is_empty(&self) -> bool {
        matches!(self.head, None)
    }

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

    #[pure]
    #[requires(index < self.len())]
    // Return type is changed from `T` to `&T`
    pub fn lookup(&self, index: usize) -> &T {
        link_lookup(&self.head, index)
    }

    #[ensures(self.len() == old(self.len()) + 1)]
    #[ensures(snap(self.lookup(0)) === elem)] // Here we add a `snap`
    #[ensures(forall(|i: usize| (i < old(self.len())) ==>
        old(self.lookup(i)) === self.lookup(i + 1)))]
    pub fn push(&mut self, elem: T) {
        // ...
        let new_node = Box::new(Node {
            elem,
            next: self.head.take(),
        });

        self.head = Some(new_node);
    }

    predicate! {
        // two-state predicate to check if the head of a list was correctly removed
        fn head_removed(&self, prev: &Self) -> bool {
            self.len() == prev.len() - 1 // The length will decrease by 1
            && forall(|i: usize| // Every element will be shifted forwards by one
                (1 <= i && i < prev.len())
                    ==> prev.lookup(i) === self.lookup(i - 1))
        }
    }

    #[ensures(old(self.is_empty()) ==>
        result.is_none() &&
        self.is_empty()
    )]
    #[ensures(!old(self.is_empty()) ==>
        self.head_removed(&old(snap(self)))
        &&
        result === Some(snap(old(snap(self)).lookup(0)))
    )]
    // Return type changed from `Option<i32>`
    pub fn try_pop(&mut self) -> Option<T> {
        // ...
        match self.head.take() { // Replace mem::swap with the buildin Option::take
            None => None,
            Some(node) => {
                self.head = node.next;
                Some(node.elem)
            }
        }
    }

    #[requires(!self.is_empty())]
    #[ensures(self.head_removed(&old(snap(self))))]
    #[ensures(result === old(snap(self)).lookup(0))]
    // Return type changed from `i32`
    pub fn pop(&mut self) -> T {
        self.try_pop().unwrap()
    }
}

#[pure]
#[requires(index < link_len(link))]
// Return type is changed from `T` to `&T`
fn link_lookup<T>(link: &Link<T>, index: usize) -> &T {
    match link {
        Some(node) => {
            if index == 0 {
                // Here we return a reference to `elem` instead of the `elem` itself
                &node.elem
            } else {
                link_lookup(&node.next, index - 1)
            }
        }
        None => unreachable!(),
    }
}

#[pure]
fn link_len<T>(link: &Link<T>) -> usize {
    match link {
        None => 0,
        Some(node) => 1 + link_len(&node.next),
    }
}

#[cfg(prusti)]
mod prusti_tests {
    use super::*;

    fn _test_list(){
        // ...
        let mut list = List::new(); // create an new, empty list
        prusti_assert!(list.is_empty() && list.len() == 0); // list should be empty

        list.push(5);
        list.push(10);
        prusti_assert!(!list.is_empty() && list.len() == 2); // length correct

        // Here we can just dereference the lookup with `*`, since `i32` is `Copy`:
        prusti_assert!(*list.lookup(0) == 10); // head is 10
        prusti_assert!(*list.lookup(1) == 5); // 5 got pushed back correctly

        let x = list.pop();
        prusti_assert!(x == 10); // pop returns the value that was added last

        match list.try_pop() {
            Some(y) => assert!(y == 5),
            None => unreachable!()
        }

        let z = list.try_pop();
        prusti_assert!(list.is_empty() && list.len() == 0); // length correct
        prusti_assert!(z.is_none()); // `try_pop` on an empty list should return `None`
    }
}

This code still fails to compile, this time with an error from the function link_lookup:

[E0507] cannot move out of `node.elem` which is behind a shared reference.
[Note] move occurs because `node.elem` has type `T`, which does not implement the `Copy` trait

To fix this, we will change List::lookup and link_lookup to return a reference to the element at index i, instead of the element itself. This was not needed for i32, since it implements the Copy trait. For a general type T, returning it by value would move it out of the list, which we don't want. By returning a reference instead, the lookups will work for any type T, because the element stays in the list.

In addition to returning a reference, we will have to adjust some of the places where lookup is used, mostly by dereferencing or using snap on the returned reference:

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

fn main() {}

// Make the types generic:
pub struct List<T> {
    head: Link<T>,
}

type Link<T> = Option<Box<Node<T>>>;

struct Node<T> {
    elem: T,
    next: Link<T>,
}

#[extern_spec(std::mem)]
#[ensures(snap(dest) === src)]
#[ensures(result === old(snap(dest)))]
fn replace<T>(dest: &mut T, src: T) -> T;

// Specs for std::option::Option<T>::unwrap(self) (and others) can be found here (work in progress):
// https://github.com/viperproject/prusti-dev/pull/1249/files#diff-bccda07f8a48357687e26408251041072c7470c188092fb58439de39974bdab5R47-R49

#[extern_spec]
impl<T> std::option::Option<T> {
    #[requires(self.is_some())]
    #[ensures(old(self) === Some(result))]
    pub fn unwrap(self) -> T;
    
    #[pure]
    #[ensures(result == matches!(self, None))]
    pub const fn is_none(&self) -> bool;

    #[pure]
    #[ensures(result == matches!(self, Some(_)))]
    pub const fn is_some(&self) -> bool;

    #[ensures(result === old(snap(self)))]
    #[ensures(self.is_none())]
    pub fn take(&mut self) -> Option<T>;
}

impl<T> List<T> {
    // ...

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

    #[pure]
    fn is_empty(&self) -> bool {
        matches!(self.head, None)
    }

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

    #[pure]
    #[requires(index < self.len())]
    // Return type is changed from `T` to `&T`
    pub fn lookup(&self, index: usize) -> &T {
        link_lookup(&self.head, index)
    }

    #[ensures(self.len() == old(self.len()) + 1)]
    #[ensures(snap(self.lookup(0)) === elem)] // Here we add a `snap`
    #[ensures(forall(|i: usize| (i < old(self.len())) ==>
        old(self.lookup(i)) === self.lookup(i + 1)))]
    pub fn push(&mut self, elem: T) {
        // ...
        let new_node = Box::new(Node {
            elem,
            next: self.head.take(),
        });

        self.head = Some(new_node);
    }

    predicate! {
        // two-state predicate to check if the head of a list was correctly removed
        fn head_removed(&self, prev: &Self) -> bool {
            self.len() == prev.len() - 1 // The length will decrease by 1
            && forall(|i: usize| // Every element will be shifted forwards by one
                (1 <= i && i < prev.len())
                    ==> prev.lookup(i) === self.lookup(i - 1))
        }
    }

    #[ensures(old(self.is_empty()) ==>
        result.is_none() &&
        self.is_empty()
    )]
    #[ensures(!old(self.is_empty()) ==>
        self.head_removed(&old(snap(self)))
        &&
        result === Some(snap(old(snap(self)).lookup(0)))
    )]
    // Return type changed from `Option<i32>`
    pub fn try_pop(&mut self) -> Option<T> {
        // ...
        match self.head.take() { // Replace mem::swap with the buildin Option::take
            None => None,
            Some(node) => {
                self.head = node.next;
                Some(node.elem)
            }
        }
    }

    #[requires(!self.is_empty())]
    #[ensures(self.head_removed(&old(snap(self))))]
    #[ensures(result === old(snap(self)).lookup(0))]
    // Return type changed from `i32`
    pub fn pop(&mut self) -> T {
        self.try_pop().unwrap()
    }
}

#[pure]
#[requires(index < link_len(link))]
// Return type is changed from `T` to `&T`
fn link_lookup<T>(link: &Link<T>, index: usize) -> &T {
    match link {
        Some(node) => {
            if index == 0 {
                // Here we return a reference to `elem` instead of the `elem` itself
                &node.elem
            } else {
                link_lookup(&node.next, index - 1)
            }
        }
        None => unreachable!(),
    }
}

#[pure]
fn link_len<T>(link: &Link<T>) -> usize {
    match link {
        None => 0,
        Some(node) => 1 + link_len(&node.next),
    }
}

#[cfg(prusti)]
mod prusti_tests {
    use super::*;

    fn _test_list(){
        // ...
        let mut list = List::new(); // create an new, empty list
        prusti_assert!(list.is_empty() && list.len() == 0); // list should be empty

        list.push(5);
        list.push(10);
        prusti_assert!(!list.is_empty() && list.len() == 2); // length correct

        // Here we can just dereference the lookup with `*`, since `i32` is `Copy`:
        prusti_assert!(*list.lookup(0) == 10); // head is 10
        prusti_assert!(*list.lookup(1) == 5); // 5 got pushed back correctly

        let x = list.pop();
        prusti_assert!(x == 10); // pop returns the value that was added last

        match list.try_pop() {
            Some(y) => assert!(y == 5),
            None => unreachable!()
        }

        let z = list.try_pop();
        prusti_assert!(list.is_empty() && list.len() == 0); // length correct
        prusti_assert!(z.is_none()); // `try_pop` on an empty list should return `None`
    }
}

After all these changes, Prusti is able to verify the code again, so now our linked list can be used to store elements of any type, not just i32! If you want to see the full code after all the changes, expand the following code block.

// 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() {}

// Make the types generic:
pub struct List<T> {
    head: Link<T>,
}

type Link<T> = Option<Box<Node<T>>>;

struct Node<T> {
    elem: T,
    next: Link<T>,
}

#[extern_spec(std::mem)]
#[ensures(snap(dest) === src)]
#[ensures(result === old(snap(dest)))]
fn replace<T>(dest: &mut T, src: T) -> T;

// Specs for std::option::Option<T>::unwrap(self) (and others) can be found here (work in progress):
// https://github.com/viperproject/prusti-dev/pull/1249/files#diff-bccda07f8a48357687e26408251041072c7470c188092fb58439de39974bdab5R47-R49

#[extern_spec]
impl<T> std::option::Option<T> {
    #[requires(self.is_some())]
    #[ensures(old(self) === Some(result))]
    pub fn unwrap(self) -> T;
    
    #[pure]
    #[ensures(result == matches!(self, None))]
    pub const fn is_none(&self) -> bool;

    #[pure]
    #[ensures(result == matches!(self, Some(_)))]
    pub const fn is_some(&self) -> bool;

    #[ensures(result === old(snap(self)))]
    #[ensures(self.is_none())]
    pub fn take(&mut self) -> Option<T>;
}

impl<T> List<T> {
    // ...

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

    #[pure]
    fn is_empty(&self) -> bool {
        matches!(self.head, None)
    }

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

    #[pure]
    #[requires(index < self.len())]
    // Return type is changed from `T` to `&T`
    pub fn lookup(&self, index: usize) -> &T {
        link_lookup(&self.head, index)
    }

    #[ensures(self.len() == old(self.len()) + 1)]
    #[ensures(snap(self.lookup(0)) === elem)] // Here we add a `snap`
    #[ensures(forall(|i: usize| (i < old(self.len())) ==>
        old(self.lookup(i)) === self.lookup(i + 1)))]
    pub fn push(&mut self, elem: T) {
        // ...
        let new_node = Box::new(Node {
            elem,
            next: self.head.take(),
        });

        self.head = Some(new_node);
    }

    predicate! {
        // two-state predicate to check if the head of a list was correctly removed
        fn head_removed(&self, prev: &Self) -> bool {
            self.len() == prev.len() - 1 // The length will decrease by 1
            && forall(|i: usize| // Every element will be shifted forwards by one
                (1 <= i && i < prev.len())
                    ==> prev.lookup(i) === self.lookup(i - 1))
        }
    }

    #[ensures(old(self.is_empty()) ==>
        result.is_none() &&
        self.is_empty()
    )]
    #[ensures(!old(self.is_empty()) ==>
        self.head_removed(&old(snap(self)))
        &&
        result === Some(snap(old(snap(self)).lookup(0)))
    )]
    // Return type changed from `Option<i32>`
    pub fn try_pop(&mut self) -> Option<T> {
        // ...
        match self.head.take() { // Replace mem::swap with the buildin Option::take
            None => None,
            Some(node) => {
                self.head = node.next;
                Some(node.elem)
            }
        }
    }

    #[requires(!self.is_empty())]
    #[ensures(self.head_removed(&old(snap(self))))]
    #[ensures(result === old(snap(self)).lookup(0))]
    // Return type changed from `i32`
    pub fn pop(&mut self) -> T {
        self.try_pop().unwrap()
    }
}

#[pure]
#[requires(index < link_len(link))]
// Return type is changed from `T` to `&T`
fn link_lookup<T>(link: &Link<T>, index: usize) -> &T {
    match link {
        Some(node) => {
            if index == 0 {
                // Here we return a reference to `elem` instead of the `elem` itself
                &node.elem
            } else {
                link_lookup(&node.next, index - 1)
            }
        }
        None => unreachable!(),
    }
}

#[pure]
fn link_len<T>(link: &Link<T>) -> usize {
    match link {
        None => 0,
        Some(node) => 1 + link_len(&node.next),
    }
}

#[cfg(prusti)]
mod prusti_tests {
    use super::*;

    fn _test_list(){
        // ...
        let mut list = List::new(); // create an new, empty list
        prusti_assert!(list.is_empty() && list.len() == 0); // list should be empty

        list.push(5);
        list.push(10);
        prusti_assert!(!list.is_empty() && list.len() == 2); // length correct

        // Here we can just dereference the lookup with `*`, since `i32` is `Copy`:
        prusti_assert!(*list.lookup(0) == 10); // head is 10
        prusti_assert!(*list.lookup(1) == 5); // 5 got pushed back correctly

        let x = list.pop();
        prusti_assert!(x == 10); // pop returns the value that was added last

        match list.try_pop() {
            Some(y) => assert!(y == 5),
            None => unreachable!()
        }

        let z = list.try_pop();
        prusti_assert!(list.is_empty() && list.len() == 0); // length correct
        prusti_assert!(z.is_none()); // `try_pop` on an empty list should return `None`
    }
}

Peek

Recommended reading: 3.3: Peek

Ideally, we could implement peek and try_peek like we implemented pop and try_pop before. Like pop, peek can only be called if the list is non-empty, and it then always returns a reference to the element at the head of the list (type &T). Similarly, try_peek can be called on any list, but returns an Option<&T>. The latter is currently not possible in Prusti, since structures containing references are not supported at the moment.

We can still implement peek, but we just cannot do it by using try_peek like before in pop. Instead, we can reuse the already implemented and verified lookup function! Since lookup can return a reference to any element of the list, we can just call self.lookup(0) inside of peek:

// 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<T> {
    head: Link<T>,
}

type Link<T> = Option<Box<Node<T>>>;

struct Node<T> {
    elem: T,
    next: Link<T>,
}

#[extern_spec(std::mem)]
#[ensures(snap(dest) === src)]
#[ensures(result === old(snap(dest)))]
fn replace<T>(dest: &mut T, src: T) -> T;

// Specs for std::option::Option<T>::unwrap(self) (and others) can be found here (work in progress):
// https://github.com/viperproject/prusti-dev/pull/1249/files#diff-bccda07f8a48357687e26408251041072c7470c188092fb58439de39974bdab5R47-R49

#[extern_spec]
impl<T> std::option::Option<T> {
    #[requires(self.is_some())]
    #[ensures(old(self) === Some(result))]
    pub fn unwrap(self) -> T;
    
    #[pure]
    #[ensures(result == matches!(self, None))]
    pub const fn is_none(&self) -> bool;

    #[pure]
    #[ensures(result == matches!(self, Some(_)))]
    pub const fn is_some(&self) -> bool;

    #[ensures(result === old(snap(self)))]
    #[ensures(self.is_none())]
    pub fn take(&mut self) -> Option<T>;
}

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

    #[pure]
    fn is_empty(&self) -> bool {
        matches!(self.head, None)
    }

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

    #[pure]
    #[requires(index < self.len())]
    pub fn lookup(&self, index: usize) -> &T {
        link_lookup(&self.head, index)
    }

    #[ensures(self.len() == old(self.len()) + 1)]
    #[ensures(snap(self.lookup(0)) === elem)]
    #[ensures(forall(|i: usize| (i < old(self.len())) ==>
                 old(self.lookup(i)) === self.lookup(i + 1)))]
    pub fn push(&mut self, elem: T) {
        let new_node = Box::new(Node {
            elem,
            next: self.head.take(),
        });

        self.head = Some(new_node);
    }

    predicate! {
        // two-state predicate to check if the head of a list was correctly removed
        fn head_removed(&self, prev: &Self) -> bool {
            self.len() == prev.len() - 1 // The length will decrease by 1
            && forall(|i: usize| // Every element will be shifted forwards by one
                (1 <= i && i < prev.len())
                    ==> prev.lookup(i) === self.lookup(i - 1))
        }
    }

    #[ensures(old(self.is_empty()) ==>
        result.is_none() &&
        self.is_empty()
    )]
    #[ensures(!old(self.is_empty()) ==>
        self.head_removed(&old(snap(self)))
        &&
        result === Some(snap(old(snap(self)).lookup(0)))
    )]
    pub fn try_pop(&mut self) -> Option<T> {
        match self.head.take() { // Replace mem::swap with the buildin Option::take
            None => None,
            Some(node) => {
                self.head = node.next;
                Some(node.elem)
            }
        }
    }

    #[requires(!self.is_empty())]
    #[ensures(self.head_removed(&old(snap(self))))]
    #[ensures(result === old(snap(self)).lookup(0))]
    pub fn pop(&mut self) -> T {
        self.try_pop().unwrap()
    }

    // // Not currently possible in Prusti
    // pub fn try_peek(&self) -> Option<&T> {
    //     todo!()
    // }

    #[pure]
    #[requires(!self.is_empty())]
    pub fn peek(&self) -> &T {
        self.lookup(0)
    }
}

#[pure]
#[requires(index < link_len(link))]
fn link_lookup<T>(link: &Link<T>, index: usize) -> &T {
    match link {
        Some(node) => {
            if index == 0 {
                &node.elem
            } else {
                link_lookup(&node.next, index - 1)
            }
        }
        None => unreachable!(),
    }
}

#[pure]
fn link_len<T>(link: &Link<T>) -> usize {
    match link {
        None => 0,
        Some(node) => 1 + link_len(&node.next),
    }
}

#[cfg(prusti)]
mod prusti_tests {
    use super::*;

    fn _test_list(){
        let mut list = List::new(); // create an new, empty list
        prusti_assert!(list.is_empty() && list.len() == 0); // list should be empty

        list.push(5);
        list.push(10);
        prusti_assert!(!list.is_empty() && list.len() == 2); // length correct

        prusti_assert!(*list.lookup(0) == 10); // head is 10
        prusti_assert!(*list.lookup(1) == 5); // 5 got pushed back correctly

        let x = list.pop();
        prusti_assert!(x == 10); // pop returns the value that was added last

        match list.try_pop() {
            Some(y) => assert!(y == 5),
            None => unreachable!()
        }

        let z = list.try_pop();
        prusti_assert!(list.is_empty() && list.len() == 0); // length correct
        prusti_assert!(z.is_none()); // `try_pop` on an empty list should return `None`
    }

    fn _test_peek() {
        let mut list = List::new();
        list.push(16);
        prusti_assert!(list.peek() === list.lookup(0));
        prusti_assert!(*list.peek() == 16);
        
        list.push(5);
        prusti_assert!(*list.peek() == 5);

        list.pop();
        prusti_assert!(*list.peek() == 16);
    }
}

We can also write a test again, to see if our specification holds up in actual code:

// 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<T> {
    head: Link<T>,
}

type Link<T> = Option<Box<Node<T>>>;

struct Node<T> {
    elem: T,
    next: Link<T>,
}

#[extern_spec(std::mem)]
#[ensures(snap(dest) === src)]
#[ensures(result === old(snap(dest)))]
fn replace<T>(dest: &mut T, src: T) -> T;

// Specs for std::option::Option<T>::unwrap(self) (and others) can be found here (work in progress):
// https://github.com/viperproject/prusti-dev/pull/1249/files#diff-bccda07f8a48357687e26408251041072c7470c188092fb58439de39974bdab5R47-R49

#[extern_spec]
impl<T> std::option::Option<T> {
    #[requires(self.is_some())]
    #[ensures(old(self) === Some(result))]
    pub fn unwrap(self) -> T;
    
    #[pure]
    #[ensures(result == matches!(self, None))]
    pub const fn is_none(&self) -> bool;

    #[pure]
    #[ensures(result == matches!(self, Some(_)))]
    pub const fn is_some(&self) -> bool;

    #[ensures(result === old(snap(self)))]
    #[ensures(self.is_none())]
    pub fn take(&mut self) -> Option<T>;
}

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

    #[pure]
    fn is_empty(&self) -> bool {
        matches!(self.head, None)
    }

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

    #[pure]
    #[requires(index < self.len())]
    pub fn lookup(&self, index: usize) -> &T {
        link_lookup(&self.head, index)
    }

    #[ensures(self.len() == old(self.len()) + 1)]
    #[ensures(snap(self.lookup(0)) === elem)]
    #[ensures(forall(|i: usize| (i < old(self.len())) ==>
                 old(self.lookup(i)) === self.lookup(i + 1)))]
    pub fn push(&mut self, elem: T) {
        let new_node = Box::new(Node {
            elem,
            next: self.head.take(),
        });

        self.head = Some(new_node);
    }

    predicate! {
        // two-state predicate to check if the head of a list was correctly removed
        fn head_removed(&self, prev: &Self) -> bool {
            self.len() == prev.len() - 1 // The length will decrease by 1
            && forall(|i: usize| // Every element will be shifted forwards by one
                (1 <= i && i < prev.len())
                    ==> prev.lookup(i) === self.lookup(i - 1))
        }
    }

    #[ensures(old(self.is_empty()) ==>
        result.is_none() &&
        self.is_empty()
    )]
    #[ensures(!old(self.is_empty()) ==>
        self.head_removed(&old(snap(self)))
        &&
        result === Some(snap(old(snap(self)).lookup(0)))
    )]
    pub fn try_pop(&mut self) -> Option<T> {
        match self.head.take() { // Replace mem::swap with the buildin Option::take
            None => None,
            Some(node) => {
                self.head = node.next;
                Some(node.elem)
            }
        }
    }

    #[requires(!self.is_empty())]
    #[ensures(self.head_removed(&old(snap(self))))]
    #[ensures(result === old(snap(self)).lookup(0))]
    pub fn pop(&mut self) -> T {
        self.try_pop().unwrap()
    }

    // // Not currently possible in Prusti
    // pub fn try_peek(&self) -> Option<&T> {
    //     todo!()
    // }

    #[pure]
    #[requires(!self.is_empty())]
    pub fn peek(&self) -> &T {
        self.lookup(0)
    }
}

#[pure]
#[requires(index < link_len(link))]
fn link_lookup<T>(link: &Link<T>, index: usize) -> &T {
    match link {
        Some(node) => {
            if index == 0 {
                &node.elem
            } else {
                link_lookup(&node.next, index - 1)
            }
        }
        None => unreachable!(),
    }
}

#[pure]
fn link_len<T>(link: &Link<T>) -> usize {
    match link {
        None => 0,
        Some(node) => 1 + link_len(&node.next),
    }
}

#[cfg(prusti)]
mod prusti_tests {
    use super::*;

    fn _test_list(){
        let mut list = List::new(); // create an new, empty list
        prusti_assert!(list.is_empty() && list.len() == 0); // list should be empty

        list.push(5);
        list.push(10);
        prusti_assert!(!list.is_empty() && list.len() == 2); // length correct

        prusti_assert!(*list.lookup(0) == 10); // head is 10
        prusti_assert!(*list.lookup(1) == 5); // 5 got pushed back correctly

        let x = list.pop();
        prusti_assert!(x == 10); // pop returns the value that was added last

        match list.try_pop() {
            Some(y) => assert!(y == 5),
            None => unreachable!()
        }

        let z = list.try_pop();
        prusti_assert!(list.is_empty() && list.len() == 0); // length correct
        prusti_assert!(z.is_none()); // `try_pop` on an empty list should return `None`
    }

    fn _test_peek() {
        let mut list = List::new();
        list.push(16);
        prusti_assert!(list.peek() === list.lookup(0));
        prusti_assert!(*list.peek() == 16);
        
        list.push(5);
        prusti_assert!(*list.peek() == 5);

        list.pop();
        prusti_assert!(*list.peek() == 16);
    }
}

This verifies too, so it appears our implementation of peek is correct.

The peek method only returns an immutable reference, but what if you want to get a mutable reference? We will see how in the next chapter.

Here you can see the full code we have now:

// 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<T> {
    head: Link<T>,
}

type Link<T> = Option<Box<Node<T>>>;

struct Node<T> {
    elem: T,
    next: Link<T>,
}

#[extern_spec(std::mem)]
#[ensures(snap(dest) === src)]
#[ensures(result === old(snap(dest)))]
fn replace<T>(dest: &mut T, src: T) -> T;

// Specs for std::option::Option<T>::unwrap(self) (and others) can be found here (work in progress):
// https://github.com/viperproject/prusti-dev/pull/1249/files#diff-bccda07f8a48357687e26408251041072c7470c188092fb58439de39974bdab5R47-R49

#[extern_spec]
impl<T> std::option::Option<T> {
    #[requires(self.is_some())]
    #[ensures(old(self) === Some(result))]
    pub fn unwrap(self) -> T;
    
    #[pure]
    #[ensures(result == matches!(self, None))]
    pub const fn is_none(&self) -> bool;

    #[pure]
    #[ensures(result == matches!(self, Some(_)))]
    pub const fn is_some(&self) -> bool;

    #[ensures(result === old(snap(self)))]
    #[ensures(self.is_none())]
    pub fn take(&mut self) -> Option<T>;
}

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

    #[pure]
    fn is_empty(&self) -> bool {
        matches!(self.head, None)
    }

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

    #[pure]
    #[requires(index < self.len())]
    pub fn lookup(&self, index: usize) -> &T {
        link_lookup(&self.head, index)
    }

    #[ensures(self.len() == old(self.len()) + 1)]
    #[ensures(snap(self.lookup(0)) === elem)]
    #[ensures(forall(|i: usize| (i < old(self.len())) ==>
                 old(self.lookup(i)) === self.lookup(i + 1)))]
    pub fn push(&mut self, elem: T) {
        let new_node = Box::new(Node {
            elem,
            next: self.head.take(),
        });

        self.head = Some(new_node);
    }

    predicate! {
        // two-state predicate to check if the head of a list was correctly removed
        fn head_removed(&self, prev: &Self) -> bool {
            self.len() == prev.len() - 1 // The length will decrease by 1
            && forall(|i: usize| // Every element will be shifted forwards by one
                (1 <= i && i < prev.len())
                    ==> prev.lookup(i) === self.lookup(i - 1))
        }
    }

    #[ensures(old(self.is_empty()) ==>
        result.is_none() &&
        self.is_empty()
    )]
    #[ensures(!old(self.is_empty()) ==>
        self.head_removed(&old(snap(self)))
        &&
        result === Some(snap(old(snap(self)).lookup(0)))
    )]
    pub fn try_pop(&mut self) -> Option<T> {
        match self.head.take() { // Replace mem::swap with the buildin Option::take
            None => None,
            Some(node) => {
                self.head = node.next;
                Some(node.elem)
            }
        }
    }

    #[requires(!self.is_empty())]
    #[ensures(self.head_removed(&old(snap(self))))]
    #[ensures(result === old(snap(self)).lookup(0))]
    pub fn pop(&mut self) -> T {
        self.try_pop().unwrap()
    }

    // // Not currently possible in Prusti
    // pub fn try_peek(&self) -> Option<&T> {
    //     todo!()
    // }

    #[pure]
    #[requires(!self.is_empty())]
    pub fn peek(&self) -> &T {
        self.lookup(0)
    }
}

#[pure]
#[requires(index < link_len(link))]
fn link_lookup<T>(link: &Link<T>, index: usize) -> &T {
    match link {
        Some(node) => {
            if index == 0 {
                &node.elem
            } else {
                link_lookup(&node.next, index - 1)
            }
        }
        None => unreachable!(),
    }
}

#[pure]
fn link_len<T>(link: &Link<T>) -> usize {
    match link {
        None => 0,
        Some(node) => 1 + link_len(&node.next),
    }
}

#[cfg(prusti)]
mod prusti_tests {
    use super::*;

    fn _test_list(){
        let mut list = List::new(); // create an new, empty list
        prusti_assert!(list.is_empty() && list.len() == 0); // list should be empty

        list.push(5);
        list.push(10);
        prusti_assert!(!list.is_empty() && list.len() == 2); // length correct

        prusti_assert!(*list.lookup(0) == 10); // head is 10
        prusti_assert!(*list.lookup(1) == 5); // 5 got pushed back correctly

        let x = list.pop();
        prusti_assert!(x == 10); // pop returns the value that was added last

        match list.try_pop() {
            Some(y) => assert!(y == 5),
            None => unreachable!()
        }

        let z = list.try_pop();
        prusti_assert!(list.is_empty() && list.len() == 0); // length correct
        prusti_assert!(z.is_none()); // `try_pop` on an empty list should return `None`
    }

    fn _test_peek() {
        let mut list = List::new();
        list.push(16);
        prusti_assert!(list.peek() === list.lookup(0));
        prusti_assert!(*list.peek() == 16);
        
        list.push(5);
        prusti_assert!(*list.peek() == 5);

        list.pop();
        prusti_assert!(*list.peek() == 16);
    }
}

Pledges

Now we will look at pledges. Pledges are used for functions that return mutable references into some datastructure. With a pledge you can explain to Prusti how the original object gets affected by changes to the returned reference. We will demonstrate by implementing a function that gives you a mutable reference to the first element in the list.

Implementing peek_mut

The peek_mut will return a mutable reference of type T, so the precondition of the list requires it to be non-empty. As a first postcondition, we want to ensure that the result of peek_mut points to the first element of the list.

In the code, we need to get a mutable reference to the type inside the Link = Option<Box<Node<T>>>. This requires the use of the type Option<&mut T>, which is a structure containing a reference, so it is not yet supported by Prusti. To still be able to verify peek_mut, we mark it as trusted for now:

// 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<T> {
    head: Link<T>,
}

type Link<T> = Option<Box<Node<T>>>;

struct Node<T> {
    elem: T,
    next: Link<T>,
}

#[extern_spec(std::mem)]
#[ensures(snap(dest) === src)]
#[ensures(result === old(snap(dest)))]
fn replace<T>(dest: &mut T, src: T) -> T;

// Specs for std::option::Option<T>::unwrap(self) (and others) can be found here (work in progress):
// https://github.com/viperproject/prusti-dev/pull/1249/files#diff-bccda07f8a48357687e26408251041072c7470c188092fb58439de39974bdab5R47-R49

#[extern_spec]
impl<T> std::option::Option<T> {
    #[requires(self.is_some())]
    #[ensures(old(self) === Some(result))]
    pub fn unwrap(self) -> T;
    
    #[pure]
    #[ensures(result == matches!(self, None))]
    pub const fn is_none(&self) -> bool;

    #[pure]
    #[ensures(result == matches!(self, Some(_)))]
    pub const fn is_some(&self) -> bool;

    #[ensures(result === old(snap(self)))]
    #[ensures(self.is_none())]
    pub fn take(&mut self) -> Option<T>;
}
impl<T> List<T> {
    #[pure]
    pub fn len(&self) -> usize {
        link_len(&self.head)
    }

    #[pure]
    fn is_empty(&self) -> bool {
        matches!(self.head, None)
    }

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

    #[pure]
    #[requires(index < self.len())]
    pub fn lookup(&self, index: usize) -> &T {
        link_lookup(&self.head, index)
    }

    #[ensures(self.len() == old(self.len()) + 1)]
    #[ensures(snap(self.lookup(0)) === elem)]
    #[ensures(forall(|i: usize| (i < old(self.len())) ==>
                 old(self.lookup(i)) === self.lookup(i + 1)))]
    pub fn push(&mut self, elem: T) {
        let new_node = Box::new(Node {
            elem,
            next: self.head.take(),
        });

        self.head = Some(new_node);
    }

    predicate! {
        // two-state predicate to check if the head of a list was correctly removed
        fn head_removed(&self, prev: &Self) -> bool {
            self.len() == prev.len() - 1 // The length will decrease by 1
            && forall(|i: usize| // Every element will be shifted forwards by one
                (1 <= i && i < prev.len())
                    ==> prev.lookup(i) === self.lookup(i - 1))
        }
    }

    #[ensures(old(self.is_empty()) ==>
        result.is_none() &&
        self.is_empty()
    )]
    #[ensures(!old(self.is_empty()) ==>
        self.head_removed(&old(snap(self))) &&
        result === Some(snap(old(snap(self)).lookup(0)))
    )]
    pub fn try_pop(&mut self) -> Option<T> {
        match self.head.take() {
            None => None,
            Some(node) => {
                self.head = node.next;
                Some(node.elem)
            }
        }
    }

    #[requires(!self.is_empty())]
    #[ensures(self.head_removed(&old(snap(self))))]
    #[ensures(result === old(snap(self)).lookup(0))]
    pub fn pop(&mut self) -> T {
        self.try_pop().unwrap()
    }

    // // Not currently possible in Prusti
    // pub fn try_peek(&self) -> Option<&T> {
    //     todo!()
    // }

    #[pure]
    #[requires(!self.is_empty())]
    pub fn peek(&self) -> &T {
        self.lookup(0)
    }
    
    // #[requires(index < self.len())]
    // pub fn lookup_mut(&mut self, index: usize) -> &mut T {
    //     let mut curr_node = &mut self.head;
    //     let mut index = index; // Workaround for Prusti not supporting mutable fn arguments
    //     while index != 0 {
    //         body_invariant!(true);
    //         if let Some(next_node) = curr_node { // reference in enum
    //             curr_node = &mut next_node.next;
    //         } else {
    //             unreachable!();
    //         }
    //         index -= 1;
    //     }
    //     if let Some(node) = curr_node { // ERROR: [Prusti: unsupported feature] the creation of loans in this loop is not supported (ReborrowingDagHasNoMagicWands)
    //         &mut node.elem
    //     } else {
    //         unreachable!()
    //     }
    // }

    #[trusted] // required due to unsupported reference in enum
    #[requires(!self.is_empty())]
    #[ensures(snap(result) === old(snap(self.peek())))]
    pub fn peek_mut(&mut self) -> &mut T {
        // This does not work in Prusti at the moment:
        // "&mut self.head" has type "&mut Option<T>"
        // this gets auto-dereferenced by Rust into type: "Option<&mut T>"
        // this then gets matched to "Some(node: &mut T)"
        // References in enums are not yet supported, so this cannot be verified by Prusti
        if let Some(node) = &mut self.head {
            &mut node.elem
        } else {
            unreachable!()
        }
    }
}

#[pure]
#[requires(index < link_len(link))]
fn link_lookup<T>(link: &Link<T>, index: usize) -> &T {
    match link {
        Some(node) => {
            if index == 0 {
                &node.elem
            } else {
                link_lookup(&node.next, index - 1)
            }
        }
        None => unreachable!(),
    }
}

#[pure]
fn link_len<T>(link: &Link<T>) -> usize {
    match link {
        None => 0,
        Some(node) => 1 + link_len(&node.next),
    }
}

#[cfg(prusti)]
mod prusti_tests {
    use super::*;

    fn _test_list(){
        let mut list = List::new(); // create an new, empty list
        prusti_assert!(list.is_empty() && list.len() == 0); // list should be empty

        list.push(5);
        list.push(10);
        prusti_assert!(!list.is_empty() && list.len() == 2); // length correct

        prusti_assert!(*list.lookup(0) == 10); // head is 10
        prusti_assert!(*list.lookup(1) == 5); // 5 got pushed back correctly

        let x = list.pop();
        prusti_assert!(x == 10); // pop returns the value that was added last

        match list.try_pop() {
            Some(y) => assert!(y == 5),
            None => unreachable!()
        }

        let z = list.try_pop();
        prusti_assert!(list.is_empty() && list.len() == 0); // length correct
        prusti_assert!(z.is_none()); // `try_pop` on an empty list should return `None`
    }

    fn _test_peek() {
        let mut list = List::new();
        list.push(16);
        prusti_assert!(list.peek() === list.lookup(0));
        prusti_assert!(*list.peek() == 16);
        
        list.push(5);
        prusti_assert!(*list.peek() == 5);

        list.pop();
        prusti_assert!(*list.peek() == 16);
    }

    fn _test_peek_mut() {
        let mut list = List::new();
        list.push(8);
        list.push(16);

        // Open a new scope using an opening bracket `{`
        // `first` will get dropped at the closing bracket `}`
        {
            let first = list.peek_mut();
            // `first` is a mutable reference to the first element of the list
            // for as long as `first` is exists, `list` cannot be accessed
            prusti_assert!(*first == 16);
            *first = 5; // Write 5 to the first slot of the list
            prusti_assert!(*first == 5);
            // `first` gets dropped here, `list` can be accessed again
        }
        prusti_assert!(list.len() == 2); //~ ERROR the asserted expression might not hold
        prusti_assert!(*list.lookup(0) == 5); // this fails too
        prusti_assert!(*list.lookup(1) == 8); // this fails too
    }
}

Note that peek_mut cannot be #[pure], since it returns a mutable reference.

Writing a test for our specification

Let's write a test to see if our specification works:

• Create a list with two elements: [16, 8]
• Get a mutable reference to the first element (16)
• Change the first element to 5
• Check if the list still has the expected properties after first gets dropped
  • Is the length 2?
  • Is the first element 5?
  • Is the second element 8?

// 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<T> {
    head: Link<T>,
}

type Link<T> = Option<Box<Node<T>>>;

struct Node<T> {
    elem: T,
    next: Link<T>,
}

#[extern_spec(std::mem)]
#[ensures(snap(dest) === src)]
#[ensures(result === old(snap(dest)))]
fn replace<T>(dest: &mut T, src: T) -> T;

// Specs for std::option::Option<T>::unwrap(self) (and others) can be found here (work in progress):
// https://github.com/viperproject/prusti-dev/pull/1249/files#diff-bccda07f8a48357687e26408251041072c7470c188092fb58439de39974bdab5R47-R49

#[extern_spec]
impl<T> std::option::Option<T> {
    #[requires(self.is_some())]
    #[ensures(old(self) === Some(result))]
    pub fn unwrap(self) -> T;
    
    #[pure]
    #[ensures(result == matches!(self, None))]
    pub const fn is_none(&self) -> bool;

    #[pure]
    #[ensures(result == matches!(self, Some(_)))]
    pub const fn is_some(&self) -> bool;

    #[ensures(result === old(snap(self)))]
    #[ensures(self.is_none())]
    pub fn take(&mut self) -> Option<T>;
}
impl<T> List<T> {
    #[pure]
    pub fn len(&self) -> usize {
        link_len(&self.head)
    }

    #[pure]
    fn is_empty(&self) -> bool {
        matches!(self.head, None)
    }

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

    #[pure]
    #[requires(index < self.len())]
    pub fn lookup(&self, index: usize) -> &T {
        link_lookup(&self.head, index)
    }

    #[ensures(self.len() == old(self.len()) + 1)]
    #[ensures(snap(self.lookup(0)) === elem)]
    #[ensures(forall(|i: usize| (i < old(self.len())) ==>
                 old(self.lookup(i)) === self.lookup(i + 1)))]
    pub fn push(&mut self, elem: T) {
        let new_node = Box::new(Node {
            elem,
            next: self.head.take(),
        });

        self.head = Some(new_node);
    }

    predicate! {
        // two-state predicate to check if the head of a list was correctly removed
        fn head_removed(&self, prev: &Self) -> bool {
            self.len() == prev.len() - 1 // The length will decrease by 1
            && forall(|i: usize| // Every element will be shifted forwards by one
                (1 <= i && i < prev.len())
                    ==> prev.lookup(i) === self.lookup(i - 1))
        }
    }

    #[ensures(old(self.is_empty()) ==>
        result.is_none() &&
        self.is_empty()
    )]
    #[ensures(!old(self.is_empty()) ==>
        self.head_removed(&old(snap(self))) &&
        result === Some(snap(old(snap(self)).lookup(0)))
    )]
    pub fn try_pop(&mut self) -> Option<T> {
        match self.head.take() {
            None => None,
            Some(node) => {
                self.head = node.next;
                Some(node.elem)
            }
        }
    }

    #[requires(!self.is_empty())]
    #[ensures(self.head_removed(&old(snap(self))))]
    #[ensures(result === old(snap(self)).lookup(0))]
    pub fn pop(&mut self) -> T {
        self.try_pop().unwrap()
    }

    // // Not currently possible in Prusti
    // pub fn try_peek(&self) -> Option<&T> {
    //     todo!()
    // }

    #[pure]
    #[requires(!self.is_empty())]
    pub fn peek(&self) -> &T {
        self.lookup(0)
    }
    
    // #[requires(index < self.len())]
    // pub fn lookup_mut(&mut self, index: usize) -> &mut T {
    //     let mut curr_node = &mut self.head;
    //     let mut index = index; // Workaround for Prusti not supporting mutable fn arguments
    //     while index != 0 {
    //         body_invariant!(true);
    //         if let Some(next_node) = curr_node { // reference in enum
    //             curr_node = &mut next_node.next;
    //         } else {
    //             unreachable!();
    //         }
    //         index -= 1;
    //     }
    //     if let Some(node) = curr_node { // ERROR: [Prusti: unsupported feature] the creation of loans in this loop is not supported (ReborrowingDagHasNoMagicWands)
    //         &mut node.elem
    //     } else {
    //         unreachable!()
    //     }
    // }

    #[trusted] // required due to unsupported reference in enum
    #[requires(!self.is_empty())]
    #[ensures(snap(result) === old(snap(self.peek())))]
    pub fn peek_mut(&mut self) -> &mut T {
        // This does not work in Prusti at the moment:
        // "&mut self.head" has type "&mut Option<T>"
        // this gets auto-dereferenced by Rust into type: "Option<&mut T>"
        // this then gets matched to "Some(node: &mut T)"
        // References in enums are not yet supported, so this cannot be verified by Prusti
        if let Some(node) = &mut self.head {
            &mut node.elem
        } else {
            unreachable!()
        }
    }
}

#[pure]
#[requires(index < link_len(link))]
fn link_lookup<T>(link: &Link<T>, index: usize) -> &T {
    match link {
        Some(node) => {
            if index == 0 {
                &node.elem
            } else {
                link_lookup(&node.next, index - 1)
            }
        }
        None => unreachable!(),
    }
}

#[pure]
fn link_len<T>(link: &Link<T>) -> usize {
    match link {
        None => 0,
        Some(node) => 1 + link_len(&node.next),
    }
}

#[cfg(prusti)]
mod prusti_tests {
    use super::*;

    fn _test_list(){
        let mut list = List::new(); // create an new, empty list
        prusti_assert!(list.is_empty() && list.len() == 0); // list should be empty

        list.push(5);
        list.push(10);
        prusti_assert!(!list.is_empty() && list.len() == 2); // length correct

        prusti_assert!(*list.lookup(0) == 10); // head is 10
        prusti_assert!(*list.lookup(1) == 5); // 5 got pushed back correctly

        let x = list.pop();
        prusti_assert!(x == 10); // pop returns the value that was added last

        match list.try_pop() {
            Some(y) => assert!(y == 5),
            None => unreachable!()
        }

        let z = list.try_pop();
        prusti_assert!(list.is_empty() && list.len() == 0); // length correct
        prusti_assert!(z.is_none()); // `try_pop` on an empty list should return `None`
    }

    fn _test_peek() {
        let mut list = List::new();
        list.push(16);
        prusti_assert!(list.peek() === list.lookup(0));
        prusti_assert!(*list.peek() == 16);
        
        list.push(5);
        prusti_assert!(*list.peek() == 5);

        list.pop();
        prusti_assert!(*list.peek() == 16);
    }

    fn _test_peek_mut() {
        let mut list = List::new();
        list.push(8);
        list.push(16);

        // Open a new scope using an opening bracket `{`
        // `first` will get dropped at the closing bracket `}`
        {
            let first = list.peek_mut();
            // `first` is a mutable reference to the first element of the list
            // for as long as `first` is exists, `list` cannot be accessed
            prusti_assert!(*first == 16);
            *first = 5; // Write 5 to the first slot of the list
            prusti_assert!(*first == 5);
            // `first` gets dropped here, `list` can be accessed again
        }
        prusti_assert!(list.len() == 2); //~ ERROR the asserted expression might not hold
        prusti_assert!(*list.lookup(0) == 5); // this fails too
        prusti_assert!(*list.lookup(1) == 8); // this fails too
    }
}

But this fails, Prusti cannot verify any of our last three prusti_assert statements. This is where pledges come in. We have to tell Prusti how the result affects the original list. Without this, Prusti assumes that changes to the reference can change every property of the original list, so nothing can be known about it after the reference gets dropped.

Writing the pledge

The pledge is written using an annotation, like ensures and requires, but with the keyword after_expiry. Inside we have all the conditions that hold after the returned reference gets dropped:

// 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<T> {
    head: Link<T>,
}

type Link<T> = Option<Box<Node<T>>>;

struct Node<T> {
    elem: T,
    next: Link<T>,
}

#[extern_spec(std::mem)]
#[ensures(snap(dest) === src)]
#[ensures(result === old(snap(dest)))]
fn replace<T>(dest: &mut T, src: T) -> T;

// Specs for std::option::Option<T>::unwrap(self) (and others) can be found here (work in progress):
// https://github.com/viperproject/prusti-dev/pull/1249/files#diff-bccda07f8a48357687e26408251041072c7470c188092fb58439de39974bdab5R47-R49

#[extern_spec]
impl<T> std::option::Option<T> {
    #[requires(self.is_some())]
    #[ensures(old(self) === Some(result))]
    pub fn unwrap(self) -> T;
    
    #[pure]
    #[ensures(result == matches!(self, None))]
    pub const fn is_none(&self) -> bool;

    #[pure]
    #[ensures(result == matches!(self, Some(_)))]
    pub const fn is_some(&self) -> bool;

    #[ensures(result === old(snap(self)))]
    #[ensures(self.is_none())]
    pub fn take(&mut self) -> Option<T>;
}
impl<T> List<T> {
    #[pure]
    pub fn len(&self) -> usize {
        link_len(&self.head)
    }

    #[pure]
    fn is_empty(&self) -> bool {
        matches!(self.head, None)
    }

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

    #[pure]
    #[requires(index < self.len())]
    pub fn lookup(&self, index: usize) -> &T {
        link_lookup(&self.head, index)
    }

    #[ensures(self.len() == old(self.len()) + 1)]
    #[ensures(snap(self.lookup(0)) === elem)]
    #[ensures(forall(|i: usize| (i < old(self.len())) ==>
                 old(self.lookup(i)) === self.lookup(i + 1)))]
    pub fn push(&mut self, elem: T) {
        let new_node = Box::new(Node {
            elem,
            next: self.head.take(),
        });

        self.head = Some(new_node);
    }

    predicate! {
        // two-state predicate to check if the head of a list was correctly removed
        fn head_removed(&self, prev: &Self) -> bool {
            self.len() == prev.len() - 1 // The length will decrease by 1
            && forall(|i: usize| // Every element will be shifted forwards by one
                (1 <= i && i < prev.len())
                    ==> prev.lookup(i) === self.lookup(i - 1))
        }
    }

    #[ensures(old(self.is_empty()) ==>
        result.is_none() &&
        self.is_empty()
    )]
    #[ensures(!old(self.is_empty()) ==>
        self.head_removed(&old(snap(self))) &&
        result === Some(snap(old(snap(self)).lookup(0)))
    )]
    pub fn try_pop(&mut self) -> Option<T> {
        match self.head.take() {
            None => None,
            Some(node) => {
                self.head = node.next;
                Some(node.elem)
            }
        }
    }

    #[requires(!self.is_empty())]
    #[ensures(self.head_removed(&old(snap(self))))]
    #[ensures(result === old(snap(self)).lookup(0))]
    pub fn pop(&mut self) -> T {
        self.try_pop().unwrap()
    }

    // // Not currently possible in Prusti
    // pub fn try_peek(&self) -> Option<&T> {
    //     todo!()
    // }

    #[pure]
    #[requires(!self.is_empty())]
    pub fn peek(&self) -> &T {
        self.lookup(0)
    }

    #[trusted] // required due to unsupported reference in enum
    #[requires(!self.is_empty())]
    #[ensures(snap(result) === old(snap(self.peek())))]
    #[after_expiry(
        old(self.len()) === self.len() // (1. condition)
        && forall(|i: usize| 1 <= i && i < self.len() // (2. condition)
            ==> old(snap(self.lookup(i))) === snap(self.lookup(i)))
        && snap(self.peek()) === before_expiry(snap(result)) // (3. condition)
    )]
    pub fn peek_mut(&mut self) -> &mut T {
        // This does not work in Prusti at the moment:
        // "&mut self.head" has type "&mut Option<T>"
        // this gets auto-dereferenced by Rust into type: "Option<&mut T>"
        // this then gets matched to "Some(node: &mut T)"
        // References in enums are not yet supported, so this cannot be verified by Prusti
        if let Some(node) = &mut self.head {
            &mut node.elem
        } else {
            unreachable!()
        }
        // ...
    }
}

#[pure]
#[requires(index < link_len(link))]
fn link_lookup<T>(link: &Link<T>, index: usize) -> &T {
    match link {
        Some(node) => {
            if index == 0 {
                &node.elem
            } else {
                link_lookup(&node.next, index - 1)
            }
        }
        None => unreachable!(),
    }
}

#[pure]
fn link_len<T>(link: &Link<T>) -> usize {
    match link {
        None => 0,
        Some(node) => 1 + link_len(&node.next),
    }
}

#[cfg(prusti)]
mod prusti_tests {
    use super::*;

    fn _test_list(){
        let mut list = List::new(); // create an new, empty list
        prusti_assert!(list.is_empty() && list.len() == 0); // list should be empty

        list.push(5);
        list.push(10);
        prusti_assert!(!list.is_empty() && list.len() == 2); // length correct

        prusti_assert!(*list.lookup(0) == 10); // head is 10
        prusti_assert!(*list.lookup(1) == 5); // 5 got pushed back correctly

        let x = list.pop();
        prusti_assert!(x == 10); // pop returns the value that was added last

        match list.try_pop() {
            Some(y) => assert!(y == 5),
            None => unreachable!()
        }

        let z = list.try_pop();
        prusti_assert!(list.is_empty() && list.len() == 0); // length correct
        prusti_assert!(z.is_none()); // `try_pop` on an empty list should return `None`
    }

    fn _test_peek() {
        let mut list = List::new();
        list.push(16);
        prusti_assert!(list.peek() === list.lookup(0));
        prusti_assert!(*list.peek() == 16);
        
        list.push(5);
        prusti_assert!(*list.peek() == 5);

        list.pop();
        prusti_assert!(*list.peek() == 16);
    }

    fn _test_peek_mut() {
        let mut list = List::new();
        list.push(8);
        list.push(16);

        // Open a new scope using an opening bracket `{`
        // `first` will get dropped at the closing bracket `}`
        {
            let first = list.peek_mut();
            // `first` is a mutable reference to the first element of the list
            // for as long as `first` is exists, `list` cannot be accessed
            prusti_assert!(*first == 16);
            *first = 5; // Write 5 to the first slot of the list
            prusti_assert!(*first == 5);
            // `first` gets dropped here, `list` can be accessed again
        }
        prusti_assert!(list.len() == 2);
        prusti_assert!(*list.lookup(0) == 5); // slot 0 is now `5`
        prusti_assert!(*list.lookup(1) == 8); // slot 1 is unchanged
    }
}

We have three properties here:

1. The list will have the same length afterwards.
2. Any element of the list with index 1..list.len() will not be changed.
3. The element at the head of the list is the value that was assigned to the returned reference. This is denoted with the before_expiry function.

With these three properties specified, our test verifies successfully!

Assert on expiry

Like after_expiry, there is also assert_on_expiry. It is used to check for conditions that have to be true when the returned reference expires, usually in order to uphold some type invariant.

As an example, we could use this to make sure that our list of i32 can only contain elements between 0 and 16. Given that this invariant held before the reference was given out, it will hold again only if the element, potentially changed by the caller, is still in the correct range:

// 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<T> {
    head: Link<T>,
}

type Link<T> = Option<Box<Node<T>>>;

struct Node<T> {
    elem: T,
    next: Link<T>,
}

#[extern_spec(std::mem)]
#[ensures(snap(dest) === src)]
#[ensures(result === old(snap(dest)))]
fn replace<T>(dest: &mut T, src: T) -> T;

// Specs for std::option::Option<T>::unwrap(self) (and others) can be found here (work in progress):
// https://github.com/viperproject/prusti-dev/pull/1249/files#diff-bccda07f8a48357687e26408251041072c7470c188092fb58439de39974bdab5R47-R49

#[extern_spec]
impl<T> std::option::Option<T> {
    #[requires(self.is_some())]
    #[ensures(old(self) === Some(result))]
    pub fn unwrap(self) -> T;
    
    #[pure]
    #[ensures(result == matches!(self, None))]
    pub const fn is_none(&self) -> bool;

    #[pure]
    #[ensures(result == matches!(self, Some(_)))]
    pub const fn is_some(&self) -> bool;

    #[ensures(result === old(snap(self)))]
    #[ensures(self.is_none())]
    pub fn take(&mut self) -> Option<T>;
}
impl<T> List<T> {
    #[pure]
    pub fn len(&self) -> usize {
        link_len(&self.head)
    }

    #[pure]
    fn is_empty(&self) -> bool {
        matches!(self.head, None)
    }

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

    #[pure]
    #[requires(index < self.len())]
    pub fn lookup(&self, index: usize) -> &T {
        link_lookup(&self.head, index)
    }

    #[ensures(self.len() == old(self.len()) + 1)]
    #[ensures(snap(self.lookup(0)) === elem)]
    #[ensures(forall(|i: usize| (i < old(self.len())) ==>
                 old(self.lookup(i)) === self.lookup(i + 1)))]
    pub fn push(&mut self, elem: T) {
        let new_node = Box::new(Node {
            elem,
            next: self.head.take(),
        });

        self.head = Some(new_node);
    }

    predicate! {
        // two-state predicate to check if the head of a list was correctly removed
        fn head_removed(&self, prev: &Self) -> bool {
            self.len() == prev.len() - 1 // The length will decrease by 1
            && forall(|i: usize| // Every element will be shifted forwards by one
                (1 <= i && i < prev.len())
                    ==> prev.lookup(i) === self.lookup(i - 1))
        }
    }

    #[ensures(old(self.is_empty()) ==>
        result.is_none() &&
        self.is_empty()
    )]
    #[ensures(!old(self.is_empty()) ==>
        self.head_removed(&old(snap(self)))
        &&
        result === Some(snap(old(snap(self)).lookup(0)))
    )]
    pub fn try_pop(&mut self) -> Option<T> {
        match self.head.take() { // Replace mem::swap with the buildin Option::take
            None => None,
            Some(node) => {
                self.head = node.next;
                Some(node.elem)
            }
        }
    }

    #[requires(!self.is_empty())]
    #[ensures(self.head_removed(&old(snap(self))))]
    #[ensures(result === old(snap(self)).lookup(0))]
    pub fn pop(&mut self) -> T {
        self.try_pop().unwrap()
    }

    // // Not currently possible in Prusti
    // pub fn try_peek(&self) -> Option<&T> {
    //     todo!()
    // }

    #[pure]
    #[requires(!self.is_empty())]
    pub fn peek(&self) -> &T {
        self.lookup(0)
    }

    #[trusted] // required due to unsupported reference in enum
    #[requires(!self.is_empty())]
    #[ensures(snap(result) === old(snap(self.peek())))]
    #[after_expiry(
        old(self.len()) === self.len() // (1.)
        && forall(|i: usize| 1 <= i && i < self.len() // (2.)
            ==> old(snap(self.lookup(i))) === snap(self.lookup(i)))
        && snap(self.peek()) === before_expiry(snap(result)) // (3.)
    )]
    pub fn peek_mut(&mut self) -> &mut T {
        // This does not work in Prusti at the moment:
        // "&mut self.head" has type "&mut Option<T>"
        // this gets auto-dereferenced by Rust into type: "Option<&mut T>"
        // this then gets matched to "Some(node: &mut T)"
        // References in enums are not yet supported, so this cannot be verified by Prusti
        if let Some(node) = &mut self.head {
            &mut node.elem
        } else {
            unreachable!()
        }
        // ...
    }
}

impl List<i32> {
    predicate!{
        fn is_valid(&self) -> bool {
            forall(|i: usize| i < self.len()
                ==> *self.lookup(i) >= 0 && *self.lookup(i) < 16)
        }
    }
    // ==> { let value = *self.lookup(i);
    //     0 <= value && value < 16 })

    #[trusted] // required due to unsupported reference in enum
    #[requires(!self.is_empty())]
    #[requires(self.is_valid())]
    #[ensures(snap(result) === old(snap(self.peek())))]
    #[assert_on_expiry(
        0 <= *result && *result < 16,
        self.is_valid()
        && old(self.len()) === self.len() // (1.)
        && forall(|i: usize| 1 <= i && i < self.len() // (2.)
            ==> old(snap(self.lookup(i))) === snap(self.lookup(i)))
        && snap(self.peek()) === before_expiry(snap(result)) // (3.)
    )]
    pub fn peek_mut_16(&mut self) -> &mut i32 {
        if let Some(node) = &mut self.head {
            &mut node.elem
        } else {
            unreachable!()
        }
    }
}

fn _test_assert_on_expiry() {
    let mut list = List::new();
    list.push(2);
    list.push(1);
    list.push(0);
    {
        let first = list.peek_mut_16();
        // *first = 16; // This gives an error: [Prusti: verification error] obligation might not hold on borrow expiry
        *first = 15;
    }
}

#[pure]
#[requires(index < link_len(link))]
fn link_lookup<T>(link: &Link<T>, index: usize) -> &T {
    match link {
        Some(node) => {
            if index == 0 {
                &node.elem
            } else {
                link_lookup(&node.next, index - 1)
            }
        }
        None => unreachable!(),
    }
}

#[pure]
fn link_len<T>(link: &Link<T>) -> usize {
    match link {
        None => 0,
        Some(node) => 1 + link_len(&node.next),
    }
}

#[cfg(prusti)]
mod prusti_tests {
    use super::*;

    fn _test_list(){
        let mut list = List::new(); // create an new, empty list
        prusti_assert!(list.is_empty() && list.len() == 0); // list should be empty

        list.push(5);
        list.push(10);
        prusti_assert!(!list.is_empty() && list.len() == 2); // length correct

        prusti_assert!(*list.lookup(0) == 10); // head is 10
        prusti_assert!(*list.lookup(1) == 5); // 5 got pushed back correctly

        let x = list.pop();
        prusti_assert!(x == 10); // pop returns the value that was added last

        match list.try_pop() {
            Some(y) => assert!(y == 5),
            None => unreachable!()
        }

        let z = list.try_pop();
        prusti_assert!(list.is_empty() && list.len() == 0); // length correct
        prusti_assert!(z.is_none()); // `try_pop` on an empty list should return `None`
    }

    fn _test_peek() {
        let mut list = List::new();
        list.push(16);
        prusti_assert!(list.peek() === list.lookup(0));
        prusti_assert!(*list.peek() == 16);
        
        list.push(5);
        prusti_assert!(*list.peek() == 5);

        list.pop();
        prusti_assert!(*list.peek() == 16);
    }

    fn _test_peek_mut() {
        let mut list = List::new();
        list.push(8);
        list.push(16);

        // Open a new scope using an opening bracket `{`
        // `first` will get dropped at the closing bracket `}`
        {
            let first = list.peek_mut();
            // `first` is a mutable reference to the first element of the list
            // for as long as `first` is exists, `list` cannot be accessed
            prusti_assert!(*first == 16);
            *first = 5; // Write 5 to the first slot of the list
            prusti_assert!(*first == 5);
            // `first` gets dropped here, `list` can be accessed again
        }
        prusti_assert!(list.len() == 2);
        prusti_assert!(*list.lookup(0) == 5); // slot 0 is now `5`
        prusti_assert!(*list.lookup(1) == 8); // slot 1 is unchanged
    }
}

The syntax here is #[assert_on_expiry(condition, pledge)]. This means that condition is checked at the caller side before (or "when") the reference expires, and pledge must hold after the reference expires.

Note that for any assertion A, after_expiry(A) is equivalent to assert_on_expiry(true, A).

Full Code

// 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<T> {
    head: Link<T>,
}

type Link<T> = Option<Box<Node<T>>>;

struct Node<T> {
    elem: T,
    next: Link<T>,
}

#[extern_spec(std::mem)]
#[ensures(snap(dest) === src)]
#[ensures(result === old(snap(dest)))]
fn replace<T>(dest: &mut T, src: T) -> T;

// Specs for std::option::Option<T>::unwrap(self) (and others) can be found here (work in progress):
// https://github.com/viperproject/prusti-dev/pull/1249/files#diff-bccda07f8a48357687e26408251041072c7470c188092fb58439de39974bdab5R47-R49

#[extern_spec]
impl<T> std::option::Option<T> {
    #[requires(self.is_some())]
    #[ensures(old(self) === Some(result))]
    pub fn unwrap(self) -> T;
    
    #[pure]
    #[ensures(result == matches!(self, None))]
    pub const fn is_none(&self) -> bool;

    #[pure]
    #[ensures(result == matches!(self, Some(_)))]
    pub const fn is_some(&self) -> bool;

    #[ensures(result === old(snap(self)))]
    #[ensures(self.is_none())]
    pub fn take(&mut self) -> Option<T>;
}
impl<T> List<T> {
    #[pure]
    pub fn len(&self) -> usize {
        link_len(&self.head)
    }

    #[pure]
    fn is_empty(&self) -> bool {
        matches!(self.head, None)
    }

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

    #[pure]
    #[requires(index < self.len())]
    pub fn lookup(&self, index: usize) -> &T {
        link_lookup(&self.head, index)
    }

    #[ensures(self.len() == old(self.len()) + 1)]
    #[ensures(snap(self.lookup(0)) === elem)]
    #[ensures(forall(|i: usize| (i < old(self.len())) ==>
                 old(self.lookup(i)) === self.lookup(i + 1)))]
    pub fn push(&mut self, elem: T) {
        let new_node = Box::new(Node {
            elem,
            next: self.head.take(),
        });

        self.head = Some(new_node);
    }

    predicate! {
        // two-state predicate to check if the head of a list was correctly removed
        fn head_removed(&self, prev: &Self) -> bool {
            self.len() == prev.len() - 1 // The length will decrease by 1
            && forall(|i: usize| // Every element will be shifted forwards by one
                (1 <= i && i < prev.len())
                    ==> prev.lookup(i) === self.lookup(i - 1))
        }
    }

    #[ensures(old(self.is_empty()) ==>
        result.is_none() &&
        self.is_empty()
    )]
    #[ensures(!old(self.is_empty()) ==>
        self.head_removed(&old(snap(self))) &&
        result === Some(snap(old(snap(self)).lookup(0)))
    )]
    pub fn try_pop(&mut self) -> Option<T> {
        match self.head.take() {
            None => None,
            Some(node) => {
                self.head = node.next;
                Some(node.elem)
            }
        }
    }

    #[requires(!self.is_empty())]
    #[ensures(self.head_removed(&old(snap(self))))]
    #[ensures(result === old(snap(self)).lookup(0))]
    pub fn pop(&mut self) -> T {
        self.try_pop().unwrap()
    }

    // // Not currently possible in Prusti
    // pub fn try_peek(&self) -> Option<&T> {
    //     todo!()
    // }

    #[pure]
    #[requires(!self.is_empty())]
    pub fn peek(&self) -> &T {
        self.lookup(0)
    }

    #[trusted] // required due to unsupported reference in enum
    #[requires(!self.is_empty())]
    #[ensures(snap(result) === old(snap(self.peek())))]
    #[after_expiry(
        old(self.len()) === self.len() // (1. condition)
        && forall(|i: usize| 1 <= i && i < self.len() // (2. condition)
            ==> old(snap(self.lookup(i))) === snap(self.lookup(i)))
        && snap(self.peek()) === before_expiry(snap(result)) // (3. condition)
    )]
    pub fn peek_mut(&mut self) -> &mut T {
        // This does not work in Prusti at the moment:
        // "&mut self.head" has type "&mut Option<T>"
        // this gets auto-dereferenced by Rust into type: "Option<&mut T>"
        // this then gets matched to "Some(node: &mut T)"
        // References in enums are not yet supported, so this cannot be verified by Prusti
        if let Some(node) = &mut self.head {
            &mut node.elem
        } else {
            unreachable!()
        }
        // ...
    }
}

#[pure]
#[requires(index < link_len(link))]
fn link_lookup<T>(link: &Link<T>, index: usize) -> &T {
    match link {
        Some(node) => {
            if index == 0 {
                &node.elem
            } else {
                link_lookup(&node.next, index - 1)
            }
        }
        None => unreachable!(),
    }
}

#[pure]
fn link_len<T>(link: &Link<T>) -> usize {
    match link {
        None => 0,
        Some(node) => 1 + link_len(&node.next),
    }
}

#[cfg(prusti)]
mod prusti_tests {
    use super::*;

    fn _test_list(){
        let mut list = List::new(); // create an new, empty list
        prusti_assert!(list.is_empty() && list.len() == 0); // list should be empty

        list.push(5);
        list.push(10);
        prusti_assert!(!list.is_empty() && list.len() == 2); // length correct

        prusti_assert!(*list.lookup(0) == 10); // head is 10
        prusti_assert!(*list.lookup(1) == 5); // 5 got pushed back correctly

        let x = list.pop();
        prusti_assert!(x == 10); // pop returns the value that was added last

        match list.try_pop() {
            Some(y) => assert!(y == 5),
            None => unreachable!()
        }

        let z = list.try_pop();
        prusti_assert!(list.is_empty() && list.len() == 0); // length correct
        prusti_assert!(z.is_none()); // `try_pop` on an empty list should return `None`
    }

    fn _test_peek() {
        let mut list = List::new();
        list.push(16);
        prusti_assert!(list.peek() === list.lookup(0));
        prusti_assert!(*list.peek() == 16);
        
        list.push(5);
        prusti_assert!(*list.peek() == 5);

        list.pop();
        prusti_assert!(*list.peek() == 16);
    }

    fn _test_peek_mut() {
        let mut list = List::new();
        list.push(8);
        list.push(16);

        // Open a new scope using an opening bracket `{`
        // `first` will get dropped at the closing bracket `}`
        {
            let first = list.peek_mut();
            // `first` is a mutable reference to the first element of the list
            // for as long as `first` is exists, `list` cannot be accessed
            prusti_assert!(*first == 16);
            *first = 5; // Write 5 to the first slot of the list
            prusti_assert!(*first == 5);
            // `first` gets dropped here, `list` can be accessed again
        }
        prusti_assert!(list.len() == 2);
        prusti_assert!(*list.lookup(0) == 5); // slot 0 is now `5`
        prusti_assert!(*list.lookup(1) == 8); // slot 1 is unchanged
    }
}

Final Code

Here you can see the full implementation we have thus far.

// Expand to see the full code
// 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<T> {
    head: Link<T>,
}

type Link<T> = Option<Box<Node<T>>>;

struct Node<T> {
    elem: T,
    next: Link<T>,
}

#[extern_spec(std::mem)]
#[ensures(snap(dest) === src)]
#[ensures(result === old(snap(dest)))]
fn replace<T>(dest: &mut T, src: T) -> T;

// Specs for std::option::Option<T>::unwrap(self) (and others) can be found here (work in progress):
// https://github.com/viperproject/prusti-dev/pull/1249/files#diff-bccda07f8a48357687e26408251041072c7470c188092fb58439de39974bdab5R47-R49

#[extern_spec]
impl<T> std::option::Option<T> {
    #[requires(self.is_some())]
    #[ensures(old(self) === Some(result))]
    pub fn unwrap(self) -> T;
    
    #[pure]
    #[ensures(result == matches!(self, None))]
    pub const fn is_none(&self) -> bool;

    #[pure]
    #[ensures(result == matches!(self, Some(_)))]
    pub const fn is_some(&self) -> bool;

    #[ensures(result === old(snap(self)))]
    #[ensures(self.is_none())]
    pub fn take(&mut self) -> Option<T>;
}
impl<T> List<T> {
    #[pure]
    pub fn len(&self) -> usize {
        link_len(&self.head)
    }

    #[pure]
    fn is_empty(&self) -> bool {
        matches!(self.head, None)
    }

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

    #[pure]
    #[requires(index < self.len())]
    pub fn lookup(&self, index: usize) -> &T {
        link_lookup(&self.head, index)
    }

    #[ensures(self.len() == old(self.len()) + 1)]
    #[ensures(snap(self.lookup(0)) === elem)]
    #[ensures(forall(|i: usize| (i < old(self.len())) ==>
                 old(self.lookup(i)) === self.lookup(i + 1)))]
    pub fn push(&mut self, elem: T) {
        let new_node = Box::new(Node {
            elem,
            next: self.head.take(),
        });

        self.head = Some(new_node);
    }

    predicate! {
        // two-state predicate to check if the head of a list was correctly removed
        fn head_removed(&self, prev: &Self) -> bool {
            self.len() == prev.len() - 1 // The length will decrease by 1
            && forall(|i: usize| // Every element will be shifted forwards by one
                (1 <= i && i < prev.len())
                    ==> prev.lookup(i) === self.lookup(i - 1))
        }
    }

    #[ensures(old(self.is_empty()) ==>
        result.is_none() &&
        self.is_empty()
    )]
    #[ensures(!old(self.is_empty()) ==>
        self.head_removed(&old(snap(self))) &&
        result === Some(snap(old(snap(self)).lookup(0)))
    )]
    pub fn try_pop(&mut self) -> Option<T> {
        match self.head.take() {
            None => None,
            Some(node) => {
                self.head = node.next;
                Some(node.elem)
            }
        }
    }

    #[requires(!self.is_empty())]
    #[ensures(self.head_removed(&old(snap(self))))]
    #[ensures(result === old(snap(self)).lookup(0))]
    pub fn pop(&mut self) -> T {
        self.try_pop().unwrap()
    }

    // // Not currently possible in Prusti
    // pub fn try_peek(&self) -> Option<&T> {
    //     todo!()
    // }

    #[pure]
    #[requires(!self.is_empty())]
    pub fn peek(&self) -> &T {
        self.lookup(0)
    }

    #[trusted] // required due to unsupported reference in enum
    #[requires(!self.is_empty())]
    #[ensures(snap(result) === old(snap(self.peek())))]
    #[after_expiry(
        old(self.len()) === self.len() // (1. condition)
        && forall(|i: usize| 1 <= i && i < self.len() // (2. condition)
            ==> old(snap(self.lookup(i))) === snap(self.lookup(i)))
        && snap(self.peek()) === before_expiry(snap(result)) // (3. condition)
    )]
    pub fn peek_mut(&mut self) -> &mut T {
        // This does not work in Prusti at the moment:
        // "&mut self.head" has type "&mut Option<T>"
        // this gets auto-dereferenced by Rust into type: "Option<&mut T>"
        // this then gets matched to "Some(node: &mut T)"
        // References in enums are not yet supported, so this cannot be verified by Prusti
        if let Some(node) = &mut self.head {
            &mut node.elem
        } else {
            unreachable!()
        }
        // ...
    }
}

#[pure]
#[requires(index < link_len(link))]
fn link_lookup<T>(link: &Link<T>, index: usize) -> &T {
    match link {
        Some(node) => {
            if index == 0 {
                &node.elem
            } else {
                link_lookup(&node.next, index - 1)
            }
        }
        None => unreachable!(),
    }
}

#[pure]
fn link_len<T>(link: &Link<T>) -> usize {
    match link {
        None => 0,
        Some(node) => 1 + link_len(&node.next),
    }
}

#[cfg(prusti)]
mod prusti_tests {
    use super::*;

    fn _test_list(){
        let mut list = List::new(); // create an new, empty list
        prusti_assert!(list.is_empty() && list.len() == 0); // list should be empty

        list.push(5);
        list.push(10);
        prusti_assert!(!list.is_empty() && list.len() == 2); // length correct

        prusti_assert!(*list.lookup(0) == 10); // head is 10
        prusti_assert!(*list.lookup(1) == 5); // 5 got pushed back correctly

        let x = list.pop();
        prusti_assert!(x == 10); // pop returns the value that was added last

        match list.try_pop() {
            Some(y) => assert!(y == 5),
            None => unreachable!()
        }

        let z = list.try_pop();
        prusti_assert!(list.is_empty() && list.len() == 0); // length correct
        prusti_assert!(z.is_none()); // `try_pop` on an empty list should return `None`
    }

    fn _test_peek() {
        let mut list = List::new();
        list.push(16);
        prusti_assert!(list.peek() === list.lookup(0));
        prusti_assert!(*list.peek() == 16);
        
        list.push(5);
        prusti_assert!(*list.peek() == 5);

        list.pop();
        prusti_assert!(*list.peek() == 16);
    }

    fn _test_peek_mut() {
        let mut list = List::new();
        list.push(8);
        list.push(16);

        // Open a new scope using an opening bracket `{`
        // `first` will get dropped at the closing bracket `}`
        {
            let first = list.peek_mut();
            // `first` is a mutable reference to the first element of the list
            // for as long as `first` is exists, `list` cannot be accessed
            prusti_assert!(*first == 16);
            *first = 5; // Write 5 to the first slot of the list
            prusti_assert!(*first == 5);
            // `first` gets dropped here, `list` can be accessed again
        }
        prusti_assert!(list.len() == 2);
        prusti_assert!(*list.lookup(0) == 5); // slot 0 is now `5`
        prusti_assert!(*list.lookup(1) == 8); // slot 1 is unchanged
    }
}

Loop Invariants

To show how to verify loops, we will use a different example than our linked list for simplicity. We will write and verify a function that can add some value to every element of an array slice.

Let's write a function that takes an integer x and sums up all values from 0 to that value in a loop. For non-negative inputs, the result will be equal to x * (x + 1) / 2:

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

fn main() {}

#[requires(x >= 0)]
#[ensures(result == x * (x + 1) / 2)] //~ ERROR postcondition might not hold
fn summation(x: i32) -> i32 {
    let mut i = 1;
    let mut sum = 0;
    while i <= x {
        sum += i;
        i += 1;
    }
    sum
}
// Prusti: fails

We cannot verify this code yet, because Prusti does not know what the while loop does to sum and i. For that, we need to add a body_invariant. Body invariants are expressions that always hold at the beginning and end of the loop body. In our case, the invariant is that sum contains the sum of all values between 1 and i. Since i starts at 1 and not at 0, we have to slightly adjust the formula by using i - 1 instead of i, so we get: sum == (i - 1) * i / 2.

After adding the body_invariant, we get this code:

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

fn main() {}

#[requires(x >= 0)]
#[ensures(result == x * (x + 1) / 2)]
fn summation(x: i32) -> i32 {
    let mut i = 1;
    let mut sum = 0;
    while i <= x {
        body_invariant!(sum == (i - 1) * i / 2);
        sum += i;
        i += 1;
    }
    sum
}
// Prusti: verifies

This body invariant is enough to verify the postcondition. After the loop, i == x + 1 will hold. Plugging this into our body_invariant!(sum == (i - 1) * i / 2), we get sum == x * (x + 1) / 2, which is our postcondition.

Note that we did not have to add body_invariant!(1 <= i && i <= x). In some cases, such as when the loop condition is side-effect free, Prusti adds the loop condition to the body invariant, as long as at least one body_invariant is syntactically present in the loop.

Counterexamples

Let's take the summation function from the Loop invariants chapter, which adds up all the numbers from 1 to x. Let's suppose we forgot to add the non-negativity postcondition for x:

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

fn main() {}

// Note: counterexample = true

// #[requires(x >= 0)] // Forgot to add this condition
#[ensures(result == x * (x + 1) / 2)] //~ ERROR postcondition might not hold
fn summation(x: i32) -> i32 {
    let mut i = 1;
    let mut sum = 0;
    while i <= x {
        body_invariant!(sum == (i - 1) * i / 2);
        sum += i;
        i += 1;
    }
    sum
}

Attempting to verify this file will result in an error:

[Prusti: verification error] postcondition might not hold.

One way to help with debugging such a verification failure, is to have Prusti print a counterexample. This can be enabled by adding the counterexample = true flag in the Prusti.toml file.

A counterexample is any combination of values, which will cause some postcondition or assertion to fail (there are no guarantees on which values get chosen).

After running Prusti again with the new setting, we will get an error message like this one:

[Prusti: verification error] postcondition might not hold.
    final_code.rs(12, 1): the error originates here
    final_code.rs(12, 14): counterexample for "x"
        initial value: ?
        final value: -2
    final_code.rs(13, 9): counterexample for "i"
        final value: 1
    final_code.rs(14, 9): counterexample for "sum"
        final value: 0
    final_code.rs(12, 25): counterexample for result
        final value: 0

Here we can see that the postcondition does not hold for x == -2, which will result in final values of i == 1, sum == 0 and result == 0. This should help with finding wrong specifications or bugs in the code, which in this case is allowing negative numbers as an input.

Note that verification with counterexample = true is slower than normal verification.

Verification Features

Even if no specifications are provided, Prusti is capable of verifying a few basic properties about the supplied Rust code. These properties include:

• Absence of panics
• Overflow checks

More intricate properties require users to write suitable specifications. The following features are either currently supported or planned to be supported in Prusti:

• Pre- and postconditions
• Assertions, refutations and assumptions
• Trusted functions
• Pure functions
• Predicates
• External specifications
• Loop body invariants
• Pledges
• Type-conditional spec refinements
• Closures
• Specification entailments
• Type models
• Conditional compilation

By default, Prusti only checks absence of panics. Moreover, Prusti verifies partial correctness. That is, it only verifies that terminating program executions meet the supplied specification.

Absence of panics

With the default settings, Prusti checks absence of panics. For example, consider the following program which always panics when executed:

pub fn main() {
    unreachable!();
}

When run on the previous program, Prusti reports a verification error:

error[P0004]: unreachable!(..) statement might be reachable
 --> src/lib.rs:2:5
  |
2 |     unreachable!();
  |     ^^^^^^^^^^^^^^^
  |

This message correctly points out that the unreachable!() statement might actually be reachable.

The message says "might" because Prusti is conservative, i.e., it reports a verification error unless it can prove that the statement is unreachable. Hence, Prusti successfully verified the example below as it can rule out that the condition in the conditional statement, a <= 0, holds.

pub fn main() {
    let a = 5;
    if a <= 0 {
        unreachable!();
    }
}

Since Prusti is conservative, if it reports no verification errors then the program is provably correct with regard to the checked properties. The last part is important because checks such as overflow checks may be disabled. Furthermore, Prusti may verify a program although some (or even all) of its executions do not terminate because it verifies partial correctness properties.

Overflow checks

Overflow checks are enabled by default.

When overflow checks are enabled, Prusti models integers as bounded values with a range that depends on the type of the integer. Values of u32 types, for example, would be modeled to be between 0 and 2^32 - 1.

When overflow checks are disabled, Prusti models signed integers as unbounded integers.

Overflow checks can be disabled by setting the check_overflows flag to false. See Providing Flags in the developer guide for details.

By default, unsigned integers are modeled as being non-negative (0 <= i), even with overflow checks disabled. They can also be modeled as unbounded integers by setting the encode_unsigned_num_constraint flag to false.

Pre- and postconditions

In Prusti, the externally observable behaviour of a function can be specified with preconditions and postconditions. They can be provided using Rust attributes:

use prusti_contracts::*;

#[requires(...)]
#[ensures(...)]
fn example() { ... }

#[requires(...)] is a precondition, #[ensures(...)] is a postcondition. There can be any number (including none) of preconditions and postconditions attached to a function. When no precondition is specified, #[requires(true)] is assumed, and likewise for postconditions. The expression inside the parentheses of requires or ensures should be a Prusti specification.

Preconditions are checked whenever the given function is called. Postconditions are checked at any exit point of the function, i.e. explicit return statements, as well as the end of the function body.

Assertions, Refutations and Assumptions

You can use Prusti to verify that a certain property holds at a certain point within the body of a function (via an assertion). It is also possible to instruct Prusti to assume that a property holds at a certain point within a function (via an assumption).

Assertions

The macros prusti_assert!, prusti_assert_eq! and prusti_assert_ne! instruct Prusti to verify that a certain property holds at a specific point within the body of a function. In contrast to the assert!, assert_eq! and assert_ne! macros, which only accept Rust expressions, the Prusti variants accept specification expressions as arguments. Therefore, quantifiers, old expressions and other Prusti specification syntax is allowed within a call to prusti_assert!, as in the following example:

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

#[requires(*x != 2)]
fn go(x: &mut u32) {
   *x = 2;
   prusti_assert!(*x != old(*x));
}

The two macros prusti_assert_eq! and prusti_assert_ne! are also slightly different than their standard counterparts, in that they use snapshot equality === instead of Partial Equality ==.

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

#[requires(a === b)]
fn equal(a: u64, b: u64) {
    // these 2 lines do the same:
    prusti_assert!(a === b);
    prusti_assert_eq!(a, b);
}

#[requires(a !== b)]
fn different(a: u64, b: u64) {
    // these 2 lines do the same:
    prusti_assert!(a !== b);
    prusti_assert_ne!(a, b);
}

Note that the expression given to prusti_assert! must be side-effect free, since they will not result in any runtime code. Therefore, using code containing impure functions will work in an assert!, but not within a prusti_assert!. For example:

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

fn test(map: std::collections::HashMap) {
assert!(map.insert(5));
prusti_assert!(map.insert(5)); // error
}

Using Prusti assertions instead of normal assertions can speed up verification, because every assert! results in a branch in the code, while prusti_assert! does not.

Refutations

Refutation should not be relied upon for soundness as they may succeed even when expected to fail; Prusti may not be able to prove the property being refuted and thus won't complain even though the property actually holds (e.g. if the property is difficult to prove).

The prusti_refute! macro is similar to prusti_assert! in its format, conditions of use and what expressions it accepts. It instructs Prusti to verify that a certain property at a specific point within the body of a function might hold in some, but not all cases. For example the following code will verify:

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

#[ensures(val < 0 ==> result == -1)]
#[ensures(val == 0 ==> result == 0)]
#[ensures(val > 0 ==> result == 1)]
fn sign(val: i32) -> i32 {
  prusti_refute!(val <= 0);
  prusti_refute!(val >= 0);
  if val < 0 {
    -1
  } else if val > 0 {
    1
  } else {
    prusti_refute!(false);
    0
  }
}

But the following function would not:

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

#[requires(val < 0 && val > 0)]
#[ensures(result == val/2)]
fn half(val: i32) -> i32 {
  prusti_refute!(false);
  val/2
}

Assumptions

The prusti_assume! macro instructs Prusti to assume that a certain property holds at a point within the body of a function. Of course, if used improperly, this can be used to introduce unsoundness. For example, Prusti would verify the following function:

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

#[ensures(p == np)]
fn proof(p: u32, np: u32) {
    prusti_assume!(false);
}

Trusted functions

Sometimes specifications express a fact which is true about a function, but the verifier cannot prove it automatically, or it uses features not yet supported by Prusti. In such cases, it is possible to mark a function as #[trusted]:

use prusti_contracts::*;

#[trusted]
#[ensures(*a == old(*b) && *b == old(*a))]
fn xor_swap(a: &mut i32, b: &mut i32) {
    *a ^= *b;
    *b ^= *a;
    *a ^= *b;
}

In the above example, the contract for xor_swap is correct, but Prusti would not be able to verify it because it uses currently unsupported XOR operations.

While a common application of #[trusted] is to wrap functions from the standard library or external libraries, note that external specifications provide a more robust solution for this use case.

Why trusted functions are dangerous

When declaring a function as #[trusted], Prusti ignores the function's body and assumes the provided pre- and postconditions have already been successfully verified. As the example below demonstrates, a single wrong, yet trusted, specification may lead to wrong and unexpected verification results. Hence, some care is needed to ensure that the specifications of trusted functions are indeed correct.

use prusti_contracts::*;

#[trusted]
#[ensures(42 == 23)] // assumed correct since we trust foo()
fn foo() { unreachable!() }

fn test() {
    foo();
    assert!(1 == 2); // verifies successfully
}

Pure functions

Pure functions are functions which are deterministic and side-effect free. In Prusti, such functions can be marked with the #[pure] attribute. They can take shared references as arguments, but they cannot take mutable references, because modifying the heap is considered a side effect.

At the moment, it is up to the user to ensure that functions annotated with #[pure] always terminate. Non-terminating pure functions would allow to infer false.

use prusti_contracts::*;

#[pure]
#[ensures(result == *a + *b)]
fn pure_example(a: &i32, b: &i32) -> i32 {
  *a + *b
}

#[ensures(*c == a + b)]
fn impure_example(a: &i32, b: &i32, c: &mut i32) {
  *c = *a + *b
}

Predicates

Predicates are similar to pure functions in that they are deterministic and side-effect free and used in specifications.

They are more powerful than pure functions: inside predicate bodies the full Prusti specification syntax is allowed. However, they are not usable in regular Rust code, as there are no direct Rust equivalents for specification constructs like quantifiers or implications. Instead, predicates can only be called from within specifications and other predicates.

Predicates are declared using the predicate! macro on a function:

predicate! {
    fn all_zeroes(a: &MyArray) -> bool {
        forall(|i: usize|
            (0 <= i && i < a.len() ==> a.lookup(i) == 0))
    }
}

Within specifications, predicates can be called just like pure functions:

#[ensures(all_zeros(a))]
fn zero(a: &mut MyArray) { ... }

The predicate! macro is incompatible with other Prusti specifications, i.e. a predicate function cannot have pre- or postconditions. The body of a predicate must be provided, so it cannot be #[trusted]. Predicates are always considered pure.

External specifications

Since the Rust standard library and external libraries do not specify contracts for their functions, Prusti allows specifying the contract for functions separately from where they are implemented. Such a specification looks like a regular impl, with the exception that there are no bodies in the implementation functions, and that the impl has an #[extern_spec] attribute.

The standard library type std::option::Option could be specified as follows:

use prusti_contracts::*;

#[extern_spec]
impl<T> std::option::Option<T> {
    #[pure]
    #[ensures(matches!(*self, Some(_)) == result)]
    pub fn is_some(&self) -> bool;

    #[pure]
    #[ensures(self.is_some() == !result)]
    pub fn is_none(&self) -> bool;

    #[requires(self.is_some())]
    pub fn unwrap(self) -> T;

    // ...
}

Any function in an external specification is implicitly trusted (as if marked with #[trusted]). It is possible to specify multiple #[extern_spec] implementations for the same type, but it is an error to externally specify the same function multiple times.

The extern_spec attribute accepts an optional argument to provide the module path to the function being specified. For example, to specify std::mem::swap, the argument is std::mem:

use prusti_contracts::*;

#[extern_spec(std::mem)]
#[ensures(*a === old(snap(b)) && *b === old(snap(a)))]
fn swap<T>(a: &mut T, b: &mut T);

Loop body invariants

To verify loops, including loops in which the loop condition has side effects, Prusti allows specifying the invariant of the loop body using the body_invariant!(...); statement. The expression inside the parentheses should be a Prusti specification. There may be any number of body invariants in any given loop, but they must all be written next to each other.

In general, given the loop:

while {
  G; // possibly side-effectful
  g // loop condition
} {
  body_invariant!(I); // loop body invariant
  B // loop body
}

Prusti checks the following:

1. The first time that G has been executed, if g evaluates to true then the property I must hold.
2. Assuming that the property I holds, after executing B; G, if g evaluates to true then I must hold (again).

After the loop, Prusti knows that the program is in a state in which the loop condition evaluated to false. This can happen for two reasons:

1. The loop body has never been executed, because the first evaluation of the loop condition resulted in false. In this case, the invariant in the loop body is never reached.
2. The loop executed at least one iteration, then after executing B the evaluation of { G; g } resulted in false.

Finally, the loop body invariant is not enforced when exiting from a loop with a break or return statement.

As an example, consider the following program. The loop condition calls test_and_increment, and the call has side effects:

use prusti_contracts::*;

#[ensures(result == (old(*i) >= 0))]
#[ensures(*i == 1 + old(*i))]
fn test_and_increment(i: &mut usize) -> bool {
    let old_i = *i;
    *i += 1;
    old_i >= 0
}

#[requires(*i > 0)]
fn work(i: &mut usize) {
    // ...
}

fn main() {
    let mut i = 0;

    while test_and_increment(&mut i) {
        body_invariant!(i > 0);
        work(i);
    }

    assert!(i <= 0);
}

We can assert i <= 0 after the loop, because in the last evaluation of the loop condition i >= 0 was false, and i was then incremented by one.

Note that it would be wrong to assert i < 0 after the loop, because it is possible to have i == 0. Note also that the loop body invariant i >= 0 is not strong enough to verify the program, since work requires i > 0. In fact, after test_and_increment returns true, i cannot be 0 because of the += 1.

Pledges

Pledges are a construct that can be used to specify the behaviour of functions that reborrow. For example, pledges should be used for modelling an assignment to a vector element because, in Rust, v[i] = 4 is not a method call v.store(i, 4) but rather let tmp = v.get_mut(i); *tmp = 4, where get_mut is a method that reborrows the v receiver to return a reference to a particular element.

As a full example, a wrapper around Rust Vec<i32> could be implemented as follows:

use prusti_contracts::*;

pub struct VecWrapperI32 {
    v: Vec<i32>
}

impl VecWrapperI32 {
    #[trusted]
    #[pure]
    #[ensures(result >= 0)]
    pub fn len(&self) -> usize {
        self.v.len()
    }

    /// A ghost function for specifying values stored in the vector.
    #[trusted]
    #[pure]
    #[requires(0 <= index && index < self.len())]
    pub fn lookup(&self, index: usize) -> i32 {
        self.v[index]
    }

    #[trusted]
    #[requires(0 <= index && index < self.len())]
    #[ensures(*result == old(self.lookup(index)))]
    #[after_expiry(
        self.len() == old(self.len()) &&
        self.lookup(index) == before_expiry(*result) &&
        forall(
            |i: usize| (0 <= i && i < self.len() && i != index) ==>
            self.lookup(i) == old(self.lookup(i))
        )
    )]
    pub fn index_mut(&mut self, index: usize) -> &mut i32 {
        self.v.get_mut(index).unwrap()
    }
}

The syntax for a pledge is #[after_expiry(reference => condition)] where reference is the reborrowing reference (defaults to result, which is currently the only thing one can write until we have support for reference fields) and condition is a Prusti specification that specifies how the borrowed data structure will look once the borrow expires. To refer in the condition to the state that a memory location pointed at by the reference has just before expiring, use before_expiry(*reference).

Run assertions when reference expires

In some cases, a condition must be checked at the point of expiry, like for example a type invariant. The syntax for this is #[assert_on_expiry(condition, invariant)]. This means that the invariant holds, given that condition is true when the reference expires.

Note that for any assertion A, after_expiry(A) is equivalent to assert_on_expiry(true, A).

Type-Conditional Spec Refinement

When specifying trait methods or generic functions, there is often a special case that allows for more complete specification. In these cases, you can attach a type-conditional spec refinement attribute to the function in question, spelled e.g. #[refine_spec(where T: A + B, U: C, [requires(true), pure])]

For example, one could use this to specify a function like core::mem::size_of by defining a trait for types whose size we'd like to specify:

#[pure]
#[refine_spec(where T: KnownSize, [
    ensures(result == T::size()),
])]
fn size_of<T>() -> usize;

pub trait KnownSize {
    #[pure]
    fn size() -> usize;
}

Note that the involved functions are marked as pure, allowing them to be used within specifications. This is another common use case, because functions can only be pure if their parameters and result are Copy, so it is often useful to specify something like #[refine_spec(where T: Copy, [pure])].

There are some marker traits which simply modify the behavior of methods in their super-traits. For instance, consider the PartialEq<T> and Eq traits. In order to consider this additional behavior for verification, we can refine the contract of PartialEq::eq when the type is known to be marked Eq:

pub trait PartialEq<Rhs: ?Sized = Self> {
    #[refine_spec(where Self: Eq, [
        ensures(self == self), // reflexive
        // we could write more specs here
    ])]
    #[ensures(/* partial equivalence formulas */)]
    fn eq(&self, other: &Rhs) -> bool;
}

Thus, any client implementing Eq on a custom type can take advantage of the additional semantics of the total equivalence.

Closures

NOT YET SUPPORTED: This feature is not yet supported in Prusti. See PR #138 for the status of this feature as well as a prototype. The syntax described here is subject to change.

NOTE: The syntax for attaching specifications to closures is currently not working

Rust closures can be given a specification using the closure!(...) syntax:

use prusti_contracts::*;

fn main() {
    let cl = closure!(
        requires(a > b),
        ensures(result > b),
        |a: i32, b: i32| -> i32 { a }
    );
}

closure! can have any number of pre- and postconditions. The arguments and return type for the closure must be given explicitly. See specification entailments for specifying the contract of a higher-order function (e.g. when taking a closure as an argument).

Specification entailments

NOT YET SUPPORTED: This feature is not yet supported in Prusti. See PR #138 for the status of this feature as well as a prototype. The syntax described here is subject to change.

The contract for a closure or function pointer variable can be given using the specification entailment syntax:

use prusti_contracts::*;

#[requires(
  f |= |a: i32, b: i32| [
    requires(a == 5),
    requires(b == 4),
    ensures(result > 4)
  ]
)]
fn example<F: Fn (i32, i32) -> i32> (f: F) { ... }

In the above example, f, the argument to example, must be a function that takes two i32 arguments. A call to f inside the body of example is only valid if the preconditions are satisfied, and the result of that call must satisfy the postcondition given.

TODO:

• arrow syntax (~~>)
• ghost arguments
• history invariants
• multiple-call specification entailment

Type Models

Some structs, mostly non-local structs from other crates, contain non-public code which are essential for verification. To provide a specification for such structs, you can add model fields to be used in specifications. To introduce a type model for a struct, simply annotate it with the #[model] macro and declare the to-be-modelled fields inside the struct:

#[model]
struct SomeStruct {
    some_i32: i32,
    // ... more fields
}

You then can use the model of SomeStruct inside specifications via the .model() function:

#[requires(some_struct.model().some_i32 == 42)]
fn some_method(some_struct: &SomeStruct) {
    // ...
}

A model cannot be used outside of specification code, that is the following code will emit an error in Prusti and panic when executed:

fn some_client(some_struct: &mut SomeStruct) {
    some_struct.model().some_i32 = 42;
}

This means that a model cannot be instantiated or directly manipulated with runtime code. Instead, the source of a model is always a trusted function or an external specification.

Further remarks

• A model needs to be copyable, i.e. all fields need to be Copy. That also applies to type parameters where you need to add the Copy trait as a bound.
• When the modelled type has no fields, a warning will be emmitted. Using .model() on such types can lead to unsound verification results. See below for an example.

Modelled types should have fields

Using models on types without fields can have unexpected verification behavior as shown in the code snippet below:

struct A;

// no fields
#[model]
struct A {
    val: i32
}

#[trusted]
#[ensures(result.model().val == with_model_val)]
fn create_a(with_model_val: i32) -> A { A {} }

fn main() {
    let a1 = create_a(42);
    let a2 = create_a(43);
    // Can prove: a1.model().val == x for any x
    // Can prove: a2.model().val == x for any x
}

The reason for this is due to the encoding of A in Viper. When encoding the main function, Prusti creates two snapshots for a1 and a2. Since A has no fields, any two snapshots of A will be considered equal and thereafter, their models too. When inhaling the two postconditions for the call to create_a in main Viper thus assumes that the field val for the same model is 42 and 43, a contradiction.

Example: std::iter::Iter

Caution

As of yet, iterators are not fully supported in Prusti. This example is a draft and is meant as a possible real-world usage of #[model] in the near future.

An example where a type model comes in handy is the std::slice::Iter struct from the standard library. We would like to provide a specification for the Iterator:

impl<T> Iterator<'a, T> for std::slice::Iter<'a, T> {
    // ??? spec involving Iter ??? 
    fn next(&mut self) -> Option<&'a T>;
}

There is not really a way to provide a specification for this implementation, because Iter's fields do not allow a straightforward specification.

We can instead provide a model for Iter in the following way, using the #[model] macro:

use std::slice::Iter;

#[model]
struct Iter<'a, #[generic] T: Copy> {
    position: usize,
    len: usize,
    data: GhostSeq<T> // Note: Assuming this is defined somewhere
}

This allows an instance of Iter<'_, T> to be modelled by the fields position, len and data.

The model can then be used in specifications:

#[ensures(result.model().position == 0)]
#[ensures(result.model().len == slice.len())]
#[trusted]
fn create_iter<T>(slice: &[T]) -> std::slice::Iter<'_, T> {
    slice.iter()
}

#[extern_spec]
impl<T> Iterator for std::slice::Iter<'a, T> {
    type Item = T;

    [ensures( self .model().data.len == old( self .model().data.len)) )]
    #[ensures(old(self.model().pos) < self.model().data.len == >
    ( result.is_some() &&
    result.unwrap() == self.model().data.lookup(old(self.model().pos))))
    ]
    // ... more ...
    fn next(&mut self) -> Option<&'a T>;
}

Printing Counterexamples

Prusti can print counterexamples for verification failures, i.e., values for variables that violate some assertion or pre-/postcondition. This can be enabled by setting counterexample = true in the Prusti.toml file, or with the PRUSTI_COUNTEREXAMPLES=true environment variable.

For example:

fn test_assert(x: i32) {
    assert!(x >= 10);
}

This will result in an error like this one:

[Prusti: verification error] the asserted expression might not hold
assert_counterexample.rs(3, 4): counterexample for "x"
initial value: 9
final value: 9

Note 1: There are no guarantees on which value gets returned for the counterexample. The result will be an arbitrary value that fails the assertion (in this case any value in the range i32::MIN..=9). Note 2: Verification will be slower with counterexamples = true.

Customizable counterexamples

A counterexample for structs and enums can be formatted by annotating the type with #[print_counterexample(..)]. This is only available if the unsafe_core_proof flag is set to true.

Syntax structs

If a struct is annotated, the macro must have at least one argument and the first argument must be of type String and can contain an arbitrary number of curly brackets. The number of curly brackets must match the number of the remaining arguments. The remaining arguments must either be a field name, if the fields are named, or an index, if the fields are unnamed. A field can be used multiple times.

use prusti_contracts::*;

#[print_counterexample("Custom message: {}, {}", field_1, field_2) ]
struct X {
    field_1: i32,
    field_2: i32,
}

Syntax enums

If an enum is annotated, the macro must not contain any arguments. Each variant can be annotated in the exact same way as previously described. Only annotating a variant without the enum itself will result in a compile time error.

use prusti_contracts::*;

#[print_counterexample()]
enum X {
    #[print_counterexample("Custom message: {}, {}", 0, 1)]
    Variant1(i32, i32),
    #[print_counterexample("Custom message")]
    Variant2,
}

Specifications in trait impl blocks

Adding specifications to trait functions requires the impl block to be annotated with #[refine_trait_spec]:

use prusti_contracts::*;

trait TestTrait {
    fn trait_fn(self) -> i64;
}

#[refine_trait_spec] // <== Add this annotation
impl TestTrait for i64 {

    // Cannot add these 2 specifications without `refine_trait_spec`:
    #[requires(true)]
    #[ensures(result >= 0)]
    fn trait_fn(self) -> i64 {
        5
    }
}

Note: The current error message returned when #[refine_trait_spec] is missing does not hint at how to fix the issue. A message like this will be shown on either requires or ensures:

[E0407]
method `prusti_pre_item_trait_fn_d5ce99cd719545e8adb9de778a953ec2`
is not a member of trait `TestTrait`.

See issue #625 for more details.

Specification syntax

Prusti specifications are a superset of Rust Boolean expressions. They must be deterministic and side-effect free. Therefore, they can call only pure functions and predicates. The extensions to Rust expressions are summarized below:

result Variable

When using Prusti, result is used to refer to what a function returns. result can only be used inside a postcondition, meaning that function arguments called result need to be renamed.

Here is an example for returning an integer:

use prusti_contracts::*;

#[ensures(result == 5)]
fn five() -> i32 {
    5
}

And an example for returning a tuple and accessing individual fields:

use prusti_contracts::*;

#[ensures(result.0 / 2 == result.1 && result.2 == 'a')]
fn tuple() -> (i32, i32, char) {
    (10, 5, 'a')
}

Old Expressions

Old expressions are used to refer to the value that a memory location pointed at by a mutable reference had at the beginning of the function:

use prusti_contracts::*;

#[ensures(*x == old(*x) + 1)]
pub fn inc(x: &mut u32) {
    *x += 1;
}

Implications

Implications express a relationship between two Boolean expressions:

use prusti_contracts::*;

#[pure]
#[ensures(result ==> self.len() == 0)]
#[ensures(!result ==> self.len() > 0)]
pub fn is_empty(&self) -> bool {
    // ...
}

a ==> b is equivalent to !a || b and !(a && !b). Here you can see a truth table for the implication operator:

Note: The expression b is only evaluated if a is true (Short-circuit evaluation).

There is also syntax for a right-to-left implication:

use prusti_contracts::*;

#[pure]
#[ensures(self.len() == 0 <== result)]
#[ensures(self.len() > 0 <== !result)]
pub fn is_empty(&self) -> bool;

There is also syntax for biconditionals ("if and only if"):

use prusti_contracts::*;

#[pure]
#[ensures(self.len() == 0 <==> result)]
pub fn is_empty(&self) -> bool {
    // ...
}

Semantically, a biconditional is equivalent to a Boolean ==. However, it has lower precedence than the == operator.

Snapshot Equality

Snapshot equality (===) compares the snapshots of two values; essentially checking if the two values are structurally equal. In contrast, the standard equality (==) between values is determined by the implementation of PartialEq. These two equalities do not necessarily coincide. For example, some types do not implement PartialEq, or their implementation cannot be encoded as a pure function. Nonetheless, snapshot equality could be used to compare values of such types, as in the following code:

use prusti_contracts::*;

#[requires(a === b)]
fn foo<T>(a: T, b: T) {}

struct X { a: i32 }

fn main() {
    foo(X { a: 1 }, X { a: 1 });
}

There is also the counterpart for != for checking structural inequality: !==.

snap Function

The function snap can be used to take a snapshot of a reference in specifications. Its functionality is similar to the clone function, but snap is only intended for use in specifications. It also does not require the type behind the reference to implement the Clone trait:

fn snap<T>(input: &T) -> T {
    // ...
}

The snap function enables writing specifications that would otherwise break Rusts ownership rules:

use prusti_contracts::*;

struct NonCopyInt {
    value: i32
}

#[ensures(x === old(x))] // Error: Cannot borrow "*x" mutably
fn do_nothing_1(x: &mut NonCopyInt) {}

#[ensures(snap(x) === old(snap(x)))]
fn do_nothing_2(x: &mut NonCopyInt) {}

In the first function, x will be borrowed by the old function, and can therefore not be used in the snapshot equality === at the same time. Using snap(x) will create a snapshot of x, almost like using x.clone(), but only for specifications and even for x that cannot be cloned normally.

Quantifiers

Quantifiers are typically used for describing how a method call changes a container such as a vector:

use prusti_contracts::*;

#[requires(0 <= index && index < self.len())]
#[ensures(self.len() == old(self.len()))]
#[ensures(self.lookup(index) == value)]
#[ensures(
    forall(|i: usize|
        (0 <= i && i < self.len() && i != index)
        ==> (self.lookup(i) == old(self.lookup(i)))
    )
)]
pub fn store(&mut self, index: usize, value: i32) {
    // ...
}

There may be multiple bound variables:

forall(|x: isize, y: isize| ...)

The syntax of universal quantifiers is:

forall(|<bound variable>: <bound variable type>, ...| <filter> ==> <expression>)

and the syntax of existential ones:

exists(|<bound variable>: <bound variable type>, ...| <expression>)

Triggers

To specify triggers for a quantifier, the syntax is triggers=[..]:

forall(|<bound variable>: <bound variable type>, ...| <filter> ==> <expression>, triggers=[<trigger sets>])

There may be multiple trigger sets. Each trigger set is a tuple of expressions. For example:

forall(|x: usize| foo(x) ==> bar(x), triggers=[(foo(x),), (bar(x),)])

Specification entailments

Specification entailments provide the contract for a given closure or function variable. See the specification entailments chapter for more details.