Linked list

Important

Get the starting code for this tutorial in the creusot-rs/tutorial repository.

Open the file src/ex2_linked_list.rs.

This tutorial demonstrates how we can use Creusot to verify a data structure manipulating raw pointers. This data structure uses unsafe blocks to dereference raw pointers, and we can prove that these operations are in fact safe.

A linked list provides an efficient implementation for a queue: the operations push_back and pop_front can be performed in constant time. Moreover, the push_front operation is also available in constant time.

To support constant-time push_back and pop_front, we must be able to access and modify the linked list from both ends. For that reason, this data structure is inherently challenging to express in safe Rust. Hence, we implement this linked list using raw pointers.

A linked list is made of multiple links. Each Link contains a value and a raw pointer to the next Link. This pointer may be null, which indicates the end of the list.

struct Link<T> {
    value: T,
    next: *const Link<T>,
}

We keep track of a linked list with two pointers: they point to the first and last links. If we start from the first link and repeatedly follow next pointers, we will eventually reach the last link, and its next pointer must be null.

pub struct List<T> {
    first: *const Link<T>,
    last: *const Link<T>,
}

This type implements the following methods:

• push_back(&mut self, value: T): allocate a new link: Link<T>, make the next field of the current last link point to the new link, and change last to link.

• pop_front(&mut self) -> T: take out the first link, and change first to the next link.

• push_front(&mut self, value: T).

Step 1: Ghost permissions

To verify pointer operations, Creusot provides the notion of ghost permissions. A permission is a token which keeps track of the data associated with a pointer. This token cannot be duplicated: we leverage Rust’s ownership system to reason about pointer aliasing. Permissions are a ghost resource, which means that they have no run-time impact; their only use is to enable formal verification. Pointer permissions play a similar role to points-to assertions in separation logic.

The first step is to make permissions explicit in the data structure.

Extend the List type with a Ghost field containing the permissions for the pointers contained in the linked list.

Tip

• The type of permissions for pointers *const T is Perm<*const T>.
• Perm is an unsized type; we can put it in a Box when a sized type is expected.
• As a linked list is essentially a sequence of Link<T>, we can store permissions in a sequence (Seq).
• To make it compile, we will also need to update List::new() to call Seq::new() to conjure an empty ghost sequence.

pub struct List<T> {
    first: *const Link<T>,
    last: *const Link<T>,
    /// Pointer permissions of all list links
    seq: Ghost<Seq<Box<Perm<*const Link<T>>>>>,
}

impl<T> List<T> {
    pub fn new() -> List<T> {
        // Initialize the `seq` field with an empty `Seq`.
        List { first: std::ptr::null(), last: std::ptr::null(), seq: Seq::new() }
    }
}

Step 2: Type invariant

The permissions in a List<T> should correspond to the pointers that it contains.

Write a type invariant, by implementing the Invariant trait, to encode this well-formedness condition.

It contains one method invariant(self) which defines the property that all values of that type should satisfy.

Creusot will automatically assume type invariants of function parameters as additional preconditions, and type invariants of results as additional postconditions. For functions that take mutable borrows as arguments, type invariants are assumed for the initial value as preconditions, and asserted as postconditions for the final value.

Tip

• A permission Perm<*const T> contains two pieces of data: the .ward(), which is the pointer protected by the permission, and the value (.val()) that the pointer points to.
• self.first must point to the first element: it must be the ward of the first element of self.seq. Similarly, self.last must be the ward of the last element of self.seq.
• The links must be chained properly: each link’s next pointer must be the ward of the next link in self.seq, except for the last link, whose next must be null. (Hint: use is_null_logic.)
• Don’t forget the base case!

impl<T> Invariant for List<T> {
    #[logic(inline)]
    fn invariant(self) -> bool {
        pearlite! {
            (*self.seq == Seq::empty() &&
             self.first.is_null_logic() &&
             self.last.is_null_logic())
            ||
            (self.seq.len() > 0 &&
             self.first == *self.seq[0].ward() &&
             self.last  == *self.seq[self.seq.len() - 1].ward() &&
             // the links in `seq` are chained properly
             (forall<i> 0 <= i && i < self.seq.len() - 1 ==>
                 self.seq[i].val().next == *self.seq[i+1].ward()) &&
             self.seq[self.seq.len() - 1].val().next.is_null_logic())
        }
    }
}

Step 3: View

To formalize the functional correctness of List methods, it is convenient to have a functional model for it, also known as a view in Creusot.

Implement the View trait to define a view.

A linked list naturally represents a sequence of elements: we define the view of linked lists as a mapping from List<T> to sequences Seq<T>. Thus, a view provides a high-level representation of a data structure, hiding the details of memory layout.

Tip

• Use the Seq::map method.
• The body of #[logic] functions should be wrapped in the pearlite! macro.

impl<T> View for List<T> {
    type ViewTy = Seq<T>;

    #[logic]
    fn view(self) -> Self::ViewTy {
        pearlite! {
            (*self.seq).map(|ptr_perm: Box<Perm<*const Link<T>>>| ptr_perm.val().value)
        }
    }
}

We are now ready to verify the methods of List.

Step 4: new

Write the contract of new(): the view of the result is the empty sequence Seq::empty().

#[ensures(result@ == Seq::empty())]

Step 5: push_back

Specify push_back

Write the contract of List::push_back.

Tip

Use Seq::push_back.

#[ensures((^self)@ == (*self)@.push_back(value))]

Verify push_back

We must rewrite the body of the function slightly to make use of the permissions that we’ve made explicit. There are three things to do:

1. Replace Box::into_raw, which casts the newly allocated Box into a pointer, with Perm::from_box, which also returns the associated permission with it.
2. Replace the raw pointer dereference *(self.last as *mut Link<T>) with Perm::as_mut, which requires the pointer’s permission.
3. Push the permission (from Perm::from_box) into self.seq. (Hint: Seq implements the push_back method.)

Tip

For steps 2 and 3, use ghost! blocks: they enable calling ghost functions (Seq::len_ghost, Seq::get_mut_ghost, Seq::push_back_ghost, Ghost::into_inner) and they are erased at run time.

pub fn push_back(&mut self, value: T) {
    let link = Box::new(Link { value, next: std::ptr::null() });
    let (link_ptr, link_own) = Perm::from_box(link);              // 1
    if self.last.is_null() {
        self.first = link_ptr;
        self.last = link_ptr;
    } else {
        let link_last = unsafe {
            Perm::as_mut(
                self.last as *mut Link<T>,
                ghost! {                                          // 2
                    let off = self.seq.len_ghost() - 1int;
                    self.seq.get_mut_ghost(off).unwrap()
                },
            )
        };
        link_last.next = link_ptr;
        self.last = link_ptr;
    }
    ghost! { self.seq.push_back_ghost(link_own.into_inner()) };   // 3
}

Step 6: pop_front

Specify pop_front

Write the contract of pop_front.

Tip

• Use Seq::pop_front.
• We can use match in Pearlite.

#[ensures(match result {
    None => (*self)@ == Seq::empty() && (^self)@ == Seq::empty(),
    Some(x) => (*self)@.len() > 0 && x == (*self)@[0] && (^self)@ == (*self)@.pop_front()
})]

Verify pop_front.

As before, we must modify the function to manipulate pointer permissions.

1. Pop the first permission from self.seq. (Hint: use Seq::pop_front_ghost.)
2. Replace Box::from_raw, which casts a pointer to a Box, with Perm::to_box, which also requires the permission protecting the pointer.

pub fn pop_front(&mut self) -> Option<T> {
    if self.first.is_null() {
        return None;
    }
    let own = ghost! { self.seq.pop_front_ghost().unwrap() };              // 1
    let link = unsafe { *Perm::to_box(self.first as *mut Link<T>, own) };  // 2
    self.first = link.next;
    if self.first.is_null() {
        self.last = std::ptr::null_mut();
    }
    Some(link.value)
}

Step 7: push_front

Follow the same recipe as push_back and pop_front.

Conclusion

We now have a verified implementation of linked lists. This data structure makes use of unsafe primitives, and Creusot formally verifies that their safety conditions are satisfied.