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