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