account for prusti-std in user guide

docs/user-guide/src/SUMMARY.md

@@ -17,6 +17,7 @@
   - [Final Code](tour/final.md)
   - [Loop Invariants](tour/loop_invariants.md)
   - [Counterexamples](tour/counterexamples.md)
+  - [`prusti-std` and External Specifications](tour/extern_specs.md)
 - [Verification Features](verify/summary.md)
   - [Absence of panics](verify/panic.md)
   - [Overflow checks](verify/overflow.md)

docs/user-guide/src/tour/extern_specs.md

@@ -0,0 +1,42 @@
+# `prusti-std` and External Specifications
+
+In the previous chapters, the code we verified included calls to functions provided by the standard library, such as `std::mem::replace`. Prusti verifies code in a *function modular* fashion, so it only considers the specification of a function in order to verify a call to it. By default, external functions are assumed to have the contract `#[requires(true)]`, `#[ensures(true)]`, i.e. it is always possible to call the function, but it does not guarantee anything.
+
+`prusti-std` is a crate that is part of the Prusti project. It provides specifications for some standard library methods. It does not provide specifications for *all* standard library methods, but the aim is to provide a high coverage of calls, based on data found in real Rust code, evaluated on the top crates of `crates.io`.
+
+The documentation of `prusti-std` provides an overview of the specified methods, as well as informal descriptions of the contracts.
+
+## Creating new external specifications
+
+When the specification for an external method is not provided (for example, because it is not in `prusti-std`), it is likely that verification of code using that method will fail. To provide the contract for an external method, an [*external specification*](../verify/external.md) should be declared.
+
+For the sake of example, assume the `std::mem::replace` method was *not* specified in `prusti-std`. We could provide an external specification for it like so:
+
+```rust,ignore
+#[extern_spec(std::mem)]
+#[ensures(snap(dest) === src)]
+#[ensures(result === old(snap(dest)))]
+fn replace<T>(dest: &mut T, src: T) -> T;
+```
+
+Let's break this snippet down step by step:
+- First, we write the Prusti annotation `#[extern_spec]` to denote that we are writing an external specification. This requires `prusti_contracts::*` to be imported first.
+- Next, we need to declare where the original function is located. In this case it is the module `std::mem`, so we put its path in the parameter: `#[extern_spec(std::mem)]`
+- After a quick search for *\"rust std mem replace\"* we can find the [documentation for std::mem::replace](https://doc.rust-lang.org/std/mem/fn.replace.html). Here we can get the function signature: `pub fn replace<T>(dest: &mut T, src: T) -> T`. We then write down the signature in the inner module, followed by a `;`. The visibility modifier is omitted for external specifications.
+- Since there are no preconditions to `replace`, we can use the (implicit) default `#[requires(true)]`.
+- For writing the postcondition, we use four pieces of Prusti syntax:
+  - [`===`](../syntax.md#snapshot-equality) is called **snapshot equality** or **logical equality**. Is means that the left and right operands are structurally equal. `===` does not require the type of the compared elements to implement [PartialEq](https://doc.rust-lang.org/std/cmp/trait.PartialEq.html), which would be required if we used the standard equality operator `==`.
+  - The [`snap()`](../syntax.md#snap-function) function takes a snapshot of a reference. It has a similar functionality to the [`clone()`](https://doc.rust-lang.org/std/clone/trait.Clone.html) method, but does not require the type of the reference it is called on to implement the `Clone` trait. `snap` should only be used in specifications, since it ignores the borrow checker.
+  - Lastly, we have the [`old()` function](../syntax.md#old-expressions), which denotes that we want to refer to the state of `snap(dest)` from before the function was called.
+  - The identifier [`result`](../syntax.md#result-variable) is used to refer to the return parameter of the function.
+- The postcondition consists of two parts, which can either be written in one condition with `&&`, or in multiple `#[ensures(...)]` annotations like in the example above.
+  - The first condition `snap(dest) === src` means: *After the function returns, the location referenced by `dest` is structurally equal to the parameter `src`.*
+  - The second part of the postcondition is `result === old(snap(dest))`. This means: *The `result` returned by the function is structurally equal to the the element that was referenced by `dest` **before** the function was called.*
+
+Since `result` is structurally equal to `dest` from before the function call, Prusti knows that the pure function `len()` called on `result` returns the same value as it would have for `dest`.
+
+An important thing to note here is that Prusti does ***not*** check if `replace` actually does what the external specification says it does. `#[extern_spec]` implicitly implies the `#[trusted]` annotation, which means that any postconditions are just accepted and used by Prusti.
+
+### Future
+
+There is currently new functionality planned for Prusti-assistant, which should enable the user to automatically generate the `extern_spec` declaration for a given call.

docs/user-guide/src/tour/option.md

@@ -10,12 +10,6 @@ Just like in the "Learning Rust With Entirely Too Many Linked Lists" tutorial, w
 type Link = Option<Box<Node>>;
 ```
 
-In order to use the `Option::take` function, we also have to implement the `extern_spec` for it. As you can see, it is quite similar to the `extern_spec` for `mem::replace`, since `take` does the same as `replace(&mut self, None)`:
-
-```rust,noplaypen
-{{#rustdoc_include ../../../../prusti-tests/tests/verify/pass/user-guide/option.rs:option_take_extern_spec}}
-```
-
 Changing the `Link` type requires some adjustments of the code and specifications. With the new type alias for `Link`, we cannot have an `impl Link` block anymore, so our `lookup` and `len` functions on `Link` are now normal, free-standing functions:
 
 ```rust,noplaypen
@@ -31,6 +25,9 @@ Due to current limitations of Prusti, we cannot replace our `link_len` and `link
 ```
 
 Since Prusti doesn't fully support closures yet, we also cannot do the rewrite to use the `Option::map` function:
+
+<!-- TODO: link capabilities/limitations chapter (closures) -->
+
 ```rust,noplaypen
 {{#rustdoc_include ../../../../prusti-tests/tests/verify/pass/user-guide/option.rs:try_pop_rewrite}}
 ```
@@ -41,4 +38,4 @@ If you want to see the full code after all the changes, expand the following cod
 ```rust,noplaypen
 // Expand to see full code up to this chapter
 {{#rustdoc_include ../../../../prusti-tests/tests/verify/pass/user-guide/option.rs:nothing}}
-```
+```

docs/user-guide/src/tour/pop.md

@@ -45,18 +45,6 @@ Since we will need to check if a list is empty, we can implement a `#[pure]` fun
 {{#rustdoc_include ../../../../prusti-tests/tests/verify/fail/user-guide/pop.rs:is_empty}}
 ```
 
-### Writing the external specifications for `Option`
-
-Since we use `Option::unwrap`, we will need an external specification for it. While we're at it, let's also write the `#[extern_spec]` for `Option::is_some` and `Option::is_none`:
-
-```rust,noplaypen
-{{#rustdoc_include ../../../../prusti-tests/tests/verify/pass/user-guide/pop.rs:extern_spec}}
-```
-
-The syntax for writing external specifications for functions associated with `Option` is slightly different to that of `std::mem::replace`, which was a standalone function.
-
-Note: In the future, you should just be able to import these external specifications using the [`prusti-std` crate](https://crates.io/crates/prusti-std). It should be available after [this PR](https://github.com/viperproject/prusti-dev/pull/1249) is merged. Until then, you can find the work in progress specifications in the PR (e.g., for [`Option::unwrap`](https://github.com/viperproject/prusti-dev/pull/1249/files#diff-bccda07f8a48357687e26408251041072c7470c188092fb58439de39974bdab5R47-R49)).
-
 ## Implementing the specification
 
 ### Writing the precondition

docs/user-guide/src/tour/push.md

@@ -44,79 +44,20 @@ pure method `len` introduced in the [previous chapter](new.md):
 
 ```rust,noplaypen
 {{#rustdoc_include ../../../../prusti-tests/tests/verify/pass/user-guide/push_property_1.rs:property_1}}
+// Prusti: Verifies
 ```
 
-Even though the above implementation of `push` is correct, attempting to verify it with Prusti still yields a verification error:
-
-```plain
-[Prusti: verification error] postcondition might not hold.
-```
-
-This error may look surprising at first: 
-We create a new list node that stores the the original list in its next field.
-Why is Prusti unable to realize that the length of the resulting list
-is one plus the length of the original list?
-
-The explanation is that Prusti performs *function modular* verification, 
-that is, it only uses a function's specification (instead of also consulting the 
-function's implementation) whenever it encounters a function call.
-The only exception are *pure* functions, such as `len`, where Prusti also takes the
-function body into account.
-
-
-
-### Adding external specifications to library code
-
-In our case, the function `std::mem::replace` is neither marked as `pure` nor does it
-come with a specification. Hence, Prusti assumes that it is memory safe and nothing else.
-That is, Prusti uses `true` as both pre- and postcondition of `replace`,
-which is too weak to prove the specification of `push`. According to its specification,
-`replace` could arbitrarily change the original list and thus also its length.
-Hence, we cannot conclude that the length the list returned by
-`replace(&mut self.head, Link::Empty)` coincides with the length of the original 
-list.
-
-We can remedy this issue by strengthening the specification of `replace`.
-In this tutorial, we will assume that the standard library is correct, that is, we 
-do not attempt to verify specifications for functions in external crates, 
-like `replace`. To this end, we have to add the specification to the function.
-This can be done with another piece of Prusti syntax, the [extern_spec](../verify/external.md):
-
-```rust,noplaypen
-{{#rustdoc_include ../../../../prusti-tests/tests/verify/pass/user-guide/push_property_1.rs:extern_spec}}
-```
-
-Let's break this snippet down step by step:
-- First, we write the Prusti annotation `#[extern_spec]` to denote that we are writing an external specification. This requires `prusti_contracts::*` to be imported first.
-- Next, we need to declare where the original function is located. In this case it is the module `std::mem`, so we put its path in  the parameter: `#[extern_spec(std::mem)]`
-- After a quick search for *\"rust std mem replace\"* we can find the [documentation for std::mem::replace](https://doc.rust-lang.org/std/mem/fn.replace.html). Here we can get the function signature: `pub fn replace<T>(dest: &mut T, src: T) -> T`. We then write down the signature in the inner module, followed by a `;`.
-- Since there are no preconditions to `replace`, we can use the (implicit) default `#[requires(true)]`.
-- For writing the postcondition, we use four pieces of Prusti syntax:
-  - [`===`](../syntax.md#snapshot-equality) is called **snapshot equality** or **logical equality**. Is means that the left and right operands are structurally equal. `===` does not require the type of the compared elements to implement [PartialEq](https://doc.rust-lang.org/std/cmp/trait.PartialEq.html), which would be required if we used the standard equality operator `==`.
-  - The [`snap()`](../syntax.md#snap-function) function takes a snapshot of a reference. It has a similar functionality to the [`clone()`](https://doc.rust-lang.org/std/clone/trait.Clone.html) method, but does not require the type of the reference it is called on to implement the `Clone` trait. `snap` should only be used in specifications, since it ignores the borrow checker.
-  - Lastly, we have the [`old()` function](../syntax.md#old-expressions), which denotes that we want to refer to the state of `snap(dest)` from before the function was called.
-  - The identifier [`result`](../syntax.md#result-variable) is used to refer to the return parameter of the function.
-- The postcondition consists of two parts, which can either be written in one condition with `&&`, or in multiple `#[ensures(...)]` annotations like in the example above.
-  - The first condition `snap(dest) === src` means: *After the function returns, the location referenced by `dest` is structurally equal to the parameter `src`*
-  - The second part of the postcondition is `result === old(snap(dest))`. This means: *The `result` returned by the function is structurally equal to the the element that was referenced by `dest` **before** the function was called.*
-
-Since `result` is structurally equal to `dest` from before the function call, Prusti knows that the pure function `len()` called on `result` returns the same value as it would have for `dest`.
-
-
-An important thing to note here is that Prusti does ***not*** check if `replace` actually does what the external specification says it does. `#[extern_spec]` implicitly implies the `#[trusted]` annotation, which means that any postconditions are just accepted and used by Prusti.
-
-### Future
+With this, the first of the three properties of `push` is verified, but we still have two more to prove.
 
-There is currently new functionality planned for Prusti-assistant, which should enable the user to automatically generate parts of the `extern_spec` syntax.
+## Note about external specifications
 
-There is also work being done for providing external specifications for the Rust standard library. Depending on when you are reading this, the `std::mem::replace` function might be annotated already, in that case this `extern_spec` may not be needed anymore.
-You can track the progress and find some already completed specifications [in this Pull Request](https://github.com/viperproject/prusti-dev/pull/1249).
+Prusti verifies the above implementation of `push`, but this might come as a surprise: the implementation calls the standard library method `std::mem::replace`. How does Prusti know what this method does? Prusti performs *function modular* verification, so calls to other methods only use that method's specifications, and never its implementation (which may not even be available, or may use unsupported features).
 
-Specifications for the standard library should eventually be available in the [prusti-std crate](https://crates.io/crates/prusti-std). Any specifications in this crate will be available by adding it to your project's dependencies.
+The answer is that the `prusti-std` crate provides specifications for *some* of the most common standard library methods, including `std::mem::replace`. In situations where `prusti-std` does not (yet) provide a suitable specification for a method used in the code, an *external specification* must be declared. Creating external specifications is discussed in the [`prusti-std` and External Specifications](extern_specs.md) chapter of this guide.
 
 ## Trusted functions
 
-As mentioned above, `extern_specs` are implicitly `#[trusted]` by Prusti.
+External specifications, like the one for `std::mem::replace` provided by `prusti-std`, are implicitly `#[trusted]` by Prusti.
 Trusted functions can be used for verifying projects containing external code that does not have Prusti annotations, or projects using Rust features that are not yet supported by Prusti.
 An example is printing a string slice (not supported yet):
 ```rust,noplaypen
@@ -156,17 +97,6 @@ This one is even worse, it will enable anything to be verified:
 fn wrong() {}
 ```
 
-### Checking the `extern_spec`
-
-Let's get back to our code. After adding the external specification for `std::mem::replace`, we can finally verify the first property of our `push` function:
-
-```rust,noplaypen
-{{#rustdoc_include ../../../../prusti-tests/tests/verify/pass/user-guide/push_property_1.rs:property_1}}
-// Prusti: Verifies
-```
-
-With this, the first of the three properties of `push` is verified, but we still have two more to prove.
-
 ## Second property
 
 Recall the second property of our specification:
@@ -203,9 +133,6 @@ We don't need to add the condition `0 <= index`, since `index` has the type `usi
 
 After these changes, Prusti can successfully verify the code, so the first two properties of `push` are correct.
 
-
-
-
 ## Third property
 
 The third and final property we will verify for `push` is that the original list

docs/user-guide/src/tour/setup.md

@@ -18,10 +18,10 @@ cargo add prusti-contracts
 For older versions of Rust, you can manually add the dependency in your Cargo.toml file:
 ```toml
 [dependencies]
-prusti-contracts = "0.1.6"
+prusti-contracts = "0.1"
 ```
 
-To use prusti-contracts in a Rust code file, just add the following line:
+To use `prusti-contracts` in a Rust code file, just add the following line:
 ```rust,ignore
 use prusti_contracts::*;
 ```
@@ -37,9 +37,9 @@ check_overflows = false
 
 <!-- TODO: link capabilities/limitations chapter (strings) -->
 
-## Standard library annotations
+## Standard library specifications
 
-Annotations for functions and types in the Rust standard library will be available in the [`prusti-std` crate](https://crates.io/crates/prusti-std) after [this PR](https://github.com/viperproject/prusti-dev/pull/1249) is merged.
+Specifications for functions and types in the Rust standard library are provided in the [`prusti-std` crate](https://crates.io/crates/prusti-std).
 
 Adding this crate works the same as for the `prusti-contracts` crate:
 ```sh
@@ -48,6 +48,11 @@ cargo add prusti-std
 or:
 ```toml
 [dependencies]
-prusti-std = "0.1.6"
+prusti-std = "0.1"
+```
+
+To make the specifications available when using `cargo prusti`, the following line also needs to be added to the crate:
+
+```rust,ignore
+use prusti_std;
 ```
-You do not need to import anything to use the annotations in this crate in a file.

docs/user-guide/src/tour/summary.md

@@ -49,3 +49,4 @@ are as follows:
 11. [Final Code](final.md): Final code for the verified linked list
 12. [Loop Invariants](loop_invariants.md): Verifying code containing loops by writing loop invariants
 13. [Counterexamples](counterexamples.md): Getting counterexamples for failing assertions
+14. [`prusti-std` and External Specifications](extern_specs.md): Specifications for the Rust standard library, specifying external methods

prusti-contracts/prusti-contracts/src/core_spec/mem.rs

@@ -12,6 +12,10 @@ mod mem {
 
     #[ensures(*x === old(snap(y)) && *y === old(snap(x)))]
     fn swap<T>(x: &mut T, y: &mut T);
+
+    #[ensures(snap(dest) === src)]
+    #[ensures(result === old(snap(dest)))]
+    fn replace<T>(dest: &mut T, src: T) -> T;
 }
 
 pub trait KnownSize {

prusti-tests/tests/verify/fail/user-guide/peek_mut_pledges.rs

@@ -17,32 +17,6 @@ struct Node<T> {
     next: Link<T>,
 }
 
-#[extern_spec(std::mem)]
-#[ensures(snap(dest) === src)]
-#[ensures(result === old(snap(dest)))]
-fn replace<T>(dest: &mut T, src: T) -> T;
-
-// Specs for std::option::Option<T>::unwrap(self) (and others) can be found here (work in progress):
-// https://github.com/viperproject/prusti-dev/pull/1249/files#diff-bccda07f8a48357687e26408251041072c7470c188092fb58439de39974bdab5R47-R49
-
-#[extern_spec]
-impl<T> std::option::Option<T> {
-    #[requires(self.is_some())]
-    #[ensures(old(self) === Some(result))]
-    pub fn unwrap(self) -> T;
-
-    #[pure]
-    #[ensures(result == matches!(self, None))]
-    pub const fn is_none(&self) -> bool;
-
-    #[pure]
-    #[ensures(result == matches!(self, Some(_)))]
-    pub const fn is_some(&self) -> bool;
-
-    #[ensures(result === old(snap(self)))]
-    #[ensures(self.is_none())]
-    pub fn take(&mut self) -> Option<T>;
-}
 //// ANCHOR: peek_mut_code
 impl<T> List<T> {
     //// ANCHOR_END: peek_mut_code