Add Caching Documentation

docs/user-guide/src/basic.md

@@ -157,8 +157,26 @@ fn max3(a: i32, b: i32, c: i32) -> i32 {
 }
 ```
 
-When running Prusti on this example, it highlights the failing assertion and thus enables us to quickly locate and fix the issue. 
+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](https://viperproject.github.io/prusti-dev/dev-guide/config/providing.html) for how to provide these flags and [List of Configuration Flags](https://viperproject.github.io/prusti-dev/dev-guide/config/flags.html) in the developer guide.
+
+## Caching
+
+When using the "Prusti Assistant" extension, the result of verification for each Rust function will be cached to improve future verification speeds. This cache can be cleared by clicking the trashcan button in the status bar.
+
+When running Prusti from the command line, caching is disabled by default. To enable it, set the [`CACHE_PATH`](https://viperproject.github.io/prusti-dev/dev-guide/config/flags.html#cache_path) flag to a location where the cache file should be saved.
+
+A Rust function will be re-verified if:
+
+- The function signature is changed (including name or specification)
+- The function body is changed (including changes in the signatures of any other functions it calls)
+- In some cases, if the name of the containing file is changed
+
+The cache will reuse a result even if:
+
+- Local variables and arguments are renamed
+- The location of a function within a file changes
+- Modifying comments, newlines, spaces etc. — most things that *clearly* do not change the behaviour of a function (*clearly* is the imperative albeit loose word; changing `1+1` to `2` will require re-verification)

docs/user-guide/src/tour/tour-src/01-chapter-2-1.rs

@@ -5,7 +5,7 @@
 
     > List a = Empty | Elem a (List a)
 
-    A list is a sum type (Rust: enum)  
+    A list is a sum type (Rust: enum)
 
     For now, we only support storing 32-bit integers
 */

docs/user-guide/src/tour/tour-src/02-chapter-2-1.rs

@@ -16,8 +16,8 @@ help: insert some indirection (e.g., a `Box`, `Rc`, or `&`) to make `List` repre
    |  
 
     [Module std::boxed](https://doc.rust-lang.org/std/boxed/index.html):
-        > Box<T>, casually referred to as a ‘box’, provides the simplest form of heap allocation in Rust. 
-        > Boxes provide ownership for this allocation, and drop their contents when they go out of scope. 
+        > Box<T>, casually referred to as a ‘box’, provides the simplest form of heap allocation in Rust.
+        > Boxes provide ownership for this allocation, and drop their contents when they go out of scope.
 */
 
 
@@ -32,9 +32,9 @@ pub enum List {
     Notation: [] = Stack () = Heap
 
     A list with three elements looks as follows:
-  
+
         > [Elem A, ptr] -> (Elem B, ptr) -> (Elem C, ptr) -> (Empty *junk*)
-    
+
     - The last node is just overhead, the first node is not on the heap
     - Empty consumes space for a full pointer and an element
 

docs/user-guide/src/tour/tour-src/05-chapter-2-3.rs

@@ -7,7 +7,7 @@
 
 // (1) required to enable Prusti's annotations (implemented as Rust macros/attributes)
 extern crate prusti_contracts;
-use prusti_contracts::*; 
+use prusti_contracts::*;
 
 pub struct List {
     head: Link,
@@ -26,7 +26,7 @@ struct Node {
 impl List {
 
     // (3) add a method for length without annotations
-    // Methods are a special case of function in Rust because of the self argument, 
+    // Methods are a special case of function in Rust because of the self argument,
     // which doesn't have a declared type.
     // There are 3 primary forms that self can take: self, &mut self, and &self
     // We choose &self since computing the length only requires immutable access.

docs/user-guide/src/tour/tour-src/06-chapter-2-4.rs

@@ -20,7 +20,7 @@ struct Node {
 /*
     Chapter 2.4 - Push
 
-    So let's write pushing a value onto a list. 
+    So let's write pushing a value onto a list.
     push mutates the list, so we'll want to take &mut self
 */
 
@@ -41,7 +41,7 @@ impl List {
     /*
     // (2) compile this before proceeding
     pub fn push(&mut self, elem: i32) {
-        
+
         let new_node = Node {
             elem: elem,
             next: self.head, // this should be the old list
@@ -53,15 +53,15 @@ impl List {
     }
     */
 
-    /* 
+    /*
     // (3) What if we put something back? Namely, the node that we're creating.
     // Rust does not accept this for exception safety.
     pub fn push(&mut self, elem: i32) {
         let new_node = Box::new(Node {
             elem: elem,
             next: self.head,
         });
-    
+
         self.head = Link::More(new_node);
     }
     */
@@ -74,7 +74,7 @@ impl List {
             elem: elem,
             next: mem::replace(&mut self.head, Link::Empty),
         });
-    
+
         self.head = Link::More(new_node);
     }
 

docs/user-guide/src/tour/tour-src/08-chapter-2-4.rs

@@ -51,12 +51,12 @@ impl List {
     //      a) The length of the list increases by one: check
     //      b) The first element is the pushed one
     //      c) All other elements have not been changed
-    #[ensures(self.len() == old(self.len()) + 1)] 
+    #[ensures(self.len() == old(self.len()) + 1)]
     #[ensures(self.lookup(0) == elem)] // (2) express property b)
     pub fn push(&mut self, elem: i32) {
         let new_node = Box::new(Node {
             elem: elem,
-            next: replace(&mut self.head, Link::Empty), 
+            next: replace(&mut self.head, Link::Empty),
         });
 
         self.head = Link::More(new_node);
@@ -85,7 +85,7 @@ impl Link {
 
     // (4)
     #[pure]
-    #[requires(0 <= index && index < self.len())] // (6) no fix as there's no 
+    #[requires(0 <= index && index < self.len())] // (6) no fix as there's no
                                                   // relation between being empty and length 0
     pub fn lookup(&self, index: usize) -> i32 {
         match self {

docs/user-guide/src/tour/tour-src/09-chapter-2-4.rs

@@ -22,8 +22,8 @@ struct Node {
 #[ensures(dest.is_empty())]
 #[ensures(old(dest.len()) == result.len())]
 // (5) make sure that replace leaves elements in the result untouched
-//#[ensures(forall(|i: usize| (0 <= i && i < result.len()) ==> 
-//                old(dest.lookup(i)) == result.lookup(i)))] 
+//#[ensures(forall(|i: usize| (0 <= i && i < result.len()) ==>
+//                old(dest.lookup(i)) == result.lookup(i)))]
 fn replace(dest: &mut Link, src: Link) -> Link {
     mem::replace(dest, src)
 }
@@ -53,10 +53,10 @@ impl List {
     //      a) The length of the list increases by one: check
     //      b) The first element is the pushed one: check
     //      c) All other elements have not been changed
-    #[ensures(self.len() == old(self.len()) + 1)] 
+    #[ensures(self.len() == old(self.len()) + 1)]
     #[ensures(self.lookup(0) == elem)]
     #[ensures(forall(|i: usize| (1 <= i && i < self.len()) ==>
-    old(self.lookup(i-1)) == self.lookup(i)))] // (2) specify property c) 
+    old(self.lookup(i-1)) == self.lookup(i)))] // (2) specify property c)
                                                // Why does it fail?
                                                // The spec for replace is not strong enough!
     pub fn push(&mut self, elem: i32) {
@@ -90,7 +90,7 @@ impl Link {
     }
 
     #[pure]
-    #[requires(0 <= index && index < self.len())] 
+    #[requires(0 <= index && index < self.len())]
     pub fn lookup(&self, index: usize) -> i32 {
         match self {
             Link::Empty => unreachable!(),

docs/user-guide/src/tour/tour-src/10-chapter-2-5.rs

@@ -1,8 +1,8 @@
 /*
     Chapter 2.5 Pop
 
-    Like push, pop wants to mutate the list. 
-    Unlike push, we actually want to return something. 
+    Like push, pop wants to mutate the list.
+    Unlike push, we actually want to return something.
     But pop also has to deal with a tricky corner case: what if the list is empty?
     To represent this case, we introduce an Option type.
     (Option is actually in the standard library but we write our own to assign specs to functions)
@@ -37,8 +37,8 @@ struct Node {
 #[requires(src.is_empty())]
 #[ensures(dest.is_empty())]
 #[ensures(old(dest.len()) == result.len())]
-#[ensures(forall(|i: usize| (0 <= i && i < result.len()) ==> 
-                old(dest.lookup(i)) == result.lookup(i)))] 
+#[ensures(forall(|i: usize| (0 <= i && i < result.len()) ==>
+                old(dest.lookup(i)) == result.lookup(i)))]
 fn replace(dest: &mut Link, src: Link) -> Link {
     mem::replace(dest, src)
 }
@@ -64,7 +64,7 @@ impl List {
         }
     }
 
-    #[ensures(self.len() == old(self.len()) + 1)] 
+    #[ensures(self.len() == old(self.len()) + 1)]
     #[ensures(self.lookup(0) == elem)]
     #[ensures(forall(|i: usize| (1 <= i && i < self.len()) ==>
         old(self.lookup(i-1)) == self.lookup(i)))]

docs/user-guide/src/tour/tour-src/11-chapter-2-5.rs

@@ -54,8 +54,8 @@ struct Node {
 #[requires(src.is_empty())]
 #[ensures(dest.is_empty())]
 #[ensures(old(dest.len()) == result.len())]
-#[ensures(forall(|i: usize| (0 <= i && i < result.len()) ==> 
-                old(dest.lookup(i)) == result.lookup(i)))] 
+#[ensures(forall(|i: usize| (0 <= i && i < result.len()) ==>
+                old(dest.lookup(i)) == result.lookup(i)))]
 fn replace(dest: &mut Link, src: Link) -> Link {
     mem::replace(dest, src)
 }
@@ -81,7 +81,7 @@ impl List {
         }
     }
 
-    #[ensures(self.len() == old(self.len()) + 1)] 
+    #[ensures(self.len() == old(self.len()) + 1)]
     #[ensures(self.lookup(0) == elem)]
     #[ensures(forall(|i: usize| (1 <= i && i < self.len()) ==>
         old(self.lookup(i-1)) == self.lookup(i)))]

docs/user-guide/src/tour/tour-src/12-chapter-2-6.rs

@@ -1,8 +1,8 @@
 /*
     Chapter 2.6 - Testing
-    Alright, so we've got push and pop written, now we can actually test out our stack! 
-    Rust and cargo support testing as a first-class feature, 
-    so this will be super easy. 
+    Alright, so we've got push and pop written, now we can actually test out our stack!
+    Rust and cargo support testing as a first-class feature,
+    so this will be super easy.
     All we have to do is write a function, and annotate it with #[test].
 */
 
@@ -60,8 +60,8 @@ struct Node {
 #[requires(src.is_empty())]
 #[ensures(dest.is_empty())]
 #[ensures(old(dest.len()) == result.len())]
-#[ensures(forall(|i: usize| (0 <= i && i < result.len()) ==> 
-                old(dest.lookup(i)) == result.lookup(i)))] 
+#[ensures(forall(|i: usize| (0 <= i && i < result.len()) ==>
+                old(dest.lookup(i)) == result.lookup(i)))]
 fn replace(dest: &mut Link, src: Link) -> Link {
     mem::replace(dest, src)
 }
@@ -87,7 +87,7 @@ impl List {
         }
     }
 
-    #[ensures(self.len() == old(self.len()) + 1)] 
+    #[ensures(self.len() == old(self.len()) + 1)]
     #[ensures(self.lookup(0) == elem)]
     #[ensures(forall(|i: usize| (1 <= i && i < self.len()) ==>
         old(self.lookup(i-1)) == self.lookup(i)))]