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.