Add resources, obligations, and time reasoning to user guide

docs/user-guide/src/SUMMARY.md

@@ -34,4 +34,6 @@
   - [Type models](verify/type-models.md)
   - [Counterexamples](verify/counterexample.md)
   - [Specifications in trait `impl` blocks](verify/impl_block_specs.md)
+  - [Resources and obligations](verify/resources_obligations.md)
+  - [Time reasoning](verify/time_reasoning.md)
 - [Specification Syntax](syntax.md)

docs/user-guide/src/verify/resources_obligations.md

@@ -0,0 +1,155 @@
+# Resources and Obligations
+
+One way of describing state that is otherwise not captured by a Prusti program is using resources and obligations. They are typically produced and consumed by [`#[trusted]`](trusted.md) functions that have some external effects (e.g. by calling functions in foreign non-Rust libraries or by interacting with the real world).
+
+Resources and obligations can appear in the pre- and postconditions of functions. When a function is called, Prusti must prove that all resources in its precondition are held by the caller at the call site. Calling a function then has the effect of
+- removing the resources in its precondition from and
+- adding the resources in its postcondition to
+
+the caller's state at the call site.
+
+## Resources
+
+A resource can be declared, for example, like so:
+
+```rust,noplaypen,ignore
+enum Currency {
+    CAD,
+    CHF,
+    DKK,
+}
+
+resource! {
+    fn cash(amount: usize, currency: Currency);
+}
+```
+
+The general syntax is
+
+```rust,noplaypen,ignore
+
+resource! {
+    fn resource_name(amount: usize, ...);
+}
+```
+
+where `resource_name` can be an arbitrary identifier and `...` here stands for arbitrary function parameters. The first parameter always has to be `amount: usize` (literally) and it has special semantics: it expresses how many resource instances a particular invocation of the resource represents. This means that, for example, asserting `cash(2, Currency::CHF)` is equivalent to asserting `cash(1, Currency::CHF) & cash(1, Currency::CHF)`.
+
+Example program:
+
+```rust,noplaypen
+{{#rustdoc_include ../../../../prusti-tests/tests/verify/pass/user-guide/resources_apples.rs:code}}
+// Prusti: VERIFIES
+```
+
+In the above example, Prusti is able to prove that if the trusted functions have the effects they claim they do (e.g. in the case of `buy_apple`, it removes at most CHF 2 from some hypothetical account of ours and it produces at least one apple in a hypothetical warehouse), then the non-trusted `buy_apple_in_canada` also fulfills its contract (it consumes at most CAD 4 and produces at least 1 apple). Note that the program still verifies if the `4` in `cash(4, Currency::CAD)` is increased to any number larger than `4` because in such a case, there are still enough resources for the `exchange()` calls. Compare this to obligations in a section below.
+
+In a more realistic scenario, resources can be used to establish lower and upper bounds for the number of calls of a particular function. In the following example, by making a call of `costly_function` consume one instance of `call_credits`, we have a natural way of proving upper bounds on the number of times the function is called.
+
+```rust,noplaypen,ignore
+resource! {
+    fn call_credits(amount: usize);
+}
+
+#[trusted]
+#[requires(call_credits(1))]
+fn costly_function(arg: i32) {
+    // ...
+}
+
+#[requires(call_credits(2))]
+fn costly_at_most_twice(arg: i32) {
+    costly_function(arg);
+    if arg > 0 {
+        costly_function(arg - 1);
+    }
+}
+
+#[requires(call_credits(10))]
+fn complicated_procedure() {
+    // ... costly_function(...) ... costly_at_most_twice(...) ...
+
+    // if this program verifiers, we know that this function calls
+    // `costly_function` at most ten times
+}
+```
+
+The same idea is used to prove lower and upper bounds on the running time of functions as explained in the chapter about [time reasoning](time_reasoning.md).
+
+Resources can also be asserted in universal quantifiers and loop invariants:
+
+```rust,noplaypen
+{{#rustdoc_include ../../../../prusti-tests/tests/verify/pass/user-guide/resources_clean_rooms.rs:code}}
+// Prusti: VERIFIES
+```
+
+## Usage of resources in expressions
+
+The Rust functions associated with resources may not be called or otherwise referenced outside of specification code (preconditions, postconditions, `prusti_assert!`, etc.). Inside specification code, they may only appear
+- alone,
+- as conjuncts with other expressions inside the non-short-circuiting And (`&`),
+- inside the consequent of an implication,
+- inside the body of a universal quantifier,
+- inside the then- or else-branch of a conditional.
+
+They are not allowed in other kinds expressions. In particular, not inside
+- negations,
+- non-short-circuiting disjunctions (`|`),
+- the antecedents of implications,
+- the bodies of existential quantifiers,
+- the guards of conditionals.
+
+The short-circuiting `&&` and `||` are equivalent to conditionals:
+- `A && B` is equivalent to `if A { B } else { false }`, and
+- `A || B` is equivalent to `if A { true } else { B }`.
+
+Therefore, resources are allowed to appear on the left-hand side of `&&` and `||` but not on the right-hand side.
+
+## Loops
+TODO: explain the precise semantics of resources in loop invariants
+
+## Pure functions
+[NOT IMPLEMENTED YET] Resources may appear in the preconditions of [`#[pure]`](pure.md) functions but not in their postconditions. When a pure function is called, the resources in the precondition are asserted (so verification fails if Prusti cannot prove that the caller has all the required resources), but they are not removed from the caller's state.
+
+## Obligations
+
+Obligations are declared and used almost identically to resources. The only two differences are
+
+* obligations are declared using the `obligation!` macro instead of `resource!`, but otherwise, the declarations have the same structure, and
+* for a program to verify, Prusti must prove that no instances of obligations are leaked.
+
+Obligations are leaked if at the end of a function, not all obligations that are held are asserted in the function postcondition or if from one loop iteration to another, more obligations are acquired than what the change of the obligations asserted in the loop invariant is.
+
+In the following example, `with_resources` verifies, but `with_obligations` doesn't because obligations are leaked.
+
+```rust,noplaypen
+{{#rustdoc_include ../../../../prusti-tests/tests/verify/fail/user-guide/resources_vs_obligations.rs:code}}
+// Prusti: FAILS
+```
+
+Obligations are primarily used for proving that all allocated resources are eventually deallocated. If we have only one trusted function which allocates some kind of objects and only one function which deallocates them, we can annotate the allocating function with `#[ensures(obligation_name(...))]` and the deallocating one with `#[requires(obligation_name(...))]`. Then if our program verifier, we have the guarantee that for an arbitrary function, all objects allocated by it are also deallocated by it or are asserted in its postcondition. See the example below.
+
+```rust,noplaypen
+{{#rustdoc_include ../../../../prusti-tests/tests/verify/fail/user-guide/obligation_leak.rs:code}}
+// Prusti: FAILS
+```
+
+`procedure1` verifies successfully. For `procedure2`, on the other hand, we get a verification error because if it exits through the `return;`, the allocated object does not get deallocated.
+
+## `prusti_exhale!` and `prusti_inhale!`
+
+`prusti_exhale!` and `prusti_inhale!` are close companions of [`prusti_assert!` and `prusti_assume!`](assert_refute_assume.md). They allow the full [Prusti specification syntax](../syntax.md) and for assertions that don't access any resources (here, we use _resources_ to refer to both _resources_ and _obligations_), `prusti_exhale!(...)` does the same as `prusti_assert!(..)` and `prusti_inhale!(...)` the same as `prusti_assume!(...)`. If the assertion contains resources, `prusti_exhale!` consumes them and `prusti_inhale!` produces them. Here are several examples of functions that verify:
+
+```rust,noplaypen
+{{#rustdoc_include ../../../../prusti-tests/tests/verify/pass/user-guide/inhale_exhale.rs:code}}
+// Prusti: VERIFIES
+```
+
+and here a few that don't:
+
+```rust,noplaypen
+{{#rustdoc_include ../../../../prusti-tests/tests/verify/fail/user-guide/inhale_exhale.rs:code}}
+// Prusti: FAILS
+```
+
+Similarly to `prusti_assume!`, `prusti_exhale!` and `prusti_inhale!` may introduce unsoundness. They can be a helpful tool for trying out verification approaches or debugging verification errors, which is what they are primarily meant to be used for.

docs/user-guide/src/verify/time_reasoning.md

@@ -0,0 +1,50 @@
+# Time reasoning
+
+With the setting [`TIME_REASONING=true`](https://viperproject.github.io/prusti-dev/dev-guide/config/flags.html#time_reasoning), two built-in [resources](resources_obligations.md) are available: `time_credits` and `time_receipts`. They can be used to prove lower and upper bounds on the running time of functions.
+
+For the most part, they behave as any other resource defined by the user using the [`resource!` macro](resources_obligations.md). However, they are special in that at the beginning of every function and of every loop iteration (TODO: check this: is it at the _beginning_ of loop iterations?), one instance of `time_credits` is consumed and one instance of `time_receipts` is produced. If enough `time_credits` might not be available, verification fails with an error.
+
+Since the number of `time_credits` asserted in a function's precondition is an upper bound on the number of `time_credits` consumed inside the function, it serves as an upper bound on the running time of the function. Similarly, asserting a certain number of `time_receipts` in the postcondition entails a lower bound on the function's running time.
+
+In the following example, we make these two bounds match and therefore show that the function always needs exactly `n + 1` time steps to execute.
+
+```rust,noplaypen
+{{#rustdoc_include ../../../../prusti-tests/tests/verify/pass/user-guide/time_loop.rs:code}}
+// Prusti: VERIFIES
+```
+
+The number of time steps a function needs to execute might also depend on the input in more complicated ways. See the next example.
+
+```rust,noplaygen
+{{#rustdoc_include ../../../../prusti-tests/tests/verify/pass/user-guide/time_more_complicated.rs:code}}
+// Prusti: VERIFIES
+```
+
+The following are three more equivalent ways of specifying the same precondition of `do_work` as above.
+
+```rust,noplaygen
+#[requires(time_credits(6))]
+#[requires(if more_work { time_credits(5) } else { true })]
+fn do_work(more_work: bool) {
+    // ...
+}
+```
+
+```rust,noplaypen
+#[requires(time_credits(6) & (more_work ==> time_credits(5)))]
+fn do_work(more_work: bool) {
+    // ...
+}
+```
+
+```rust,noplaypen
+#[requires(more_work ==> time_credits(11))]
+#[requires(!more_work ==> time_credits(6))]
+fn do_work(more_work: bool) {
+    // ...
+}
+```
+
+## Pure functions
+
+[NOT IMPLEMENTED YET] `time_credits` and `time_receipts` may not appear in preconditions and postconditions of [`#[pure]`](pure.md) functions. For the purposes of time reasoning, the execution of pure functions is taken to be instantaneous: they do not produce or consume any `time_credits` or `time_receipts`.

prusti-tests/tests/verify/fail/obligations/loop/leak_because_extra_iteration.rs

@@ -9,7 +9,7 @@ obligation! {
 fn alloc(loc: usize) {}
 
 #[ensures(alloced(n, loc))]
-fn multialloc(loc: usize, n: usize) { //~ ERROR the function might leak instances of obligation `alloced`
+fn multialloc(loc: usize, n: usize) { //~ ERROR function might leak instances of obligation `alloced`
     let mut i = 0;
     while i < n + 1 {
         body_invariant!(alloced(i, loc));

prusti-tests/tests/verify/fail/obligations/loop/leak_because_quantifier_argument_off.rs

@@ -21,6 +21,6 @@ fn multialloc(loc_from: usize, loc_to: usize) {
 #[ensures(alloced(1, 1))]
 #[ensures(alloced(1, 2))]
 #[ensures(alloced(1, 3))]
-fn main() { //~ ERROR the function might leak instances of obligation `alloced`
+fn main() { //~ ERROR function might leak instances of obligation `alloced`
     multialloc(1, 5); // << should be (1, 4) here
 }

prusti-tests/tests/verify/fail/obligations/simple_leak.rs

@@ -8,6 +8,6 @@ obligation! {
 #[ensures(alloced(1, loc))]
 fn alloc(loc: usize) {}
 
-fn main() { //~ ERROR the function might leak instances of obligation
+fn main() { //~ ERROR function might leak instances of obligation `alloced`
     alloc(64);
 }

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

@@ -0,0 +1,23 @@
+//// ANCHOR: nothing
+//// ANCHOR_END: nothing
+// The next line is only required for doctests, you can ignore/remove it
+extern crate prusti_contracts;
+use prusti_contracts::*;
+
+fn main() {}
+
+//// ANCHOR: code
+obligation! {
+    fn o(amount: usize);
+}
+
+fn f1() {
+    prusti_exhale!(o(1)); //~ ERROR there might be not enough resources for the exhale
+}
+
+#[requires(o(2))]
+#[ensures(o(2))]
+fn f2() { //~ ERROR function might leak instances of obligation `o`
+    prusti_inhale!(o(2));
+}
+//// ANCHOR_END: code

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

@@ -0,0 +1,61 @@
+//// ANCHOR: nothing
+//// ANCHOR_END: nothing
+// The next line is only required for doctests, you can ignore/remove it
+extern crate prusti_contracts;
+use prusti_contracts::*;
+
+fn main() {}
+
+//// ANCHOR: code
+obligation! {
+    fn alloced(amount: usize, loc: usize);
+}
+
+#[trusted]
+#[ensures(alloced(1, result))]
+fn alloc() -> usize {
+    unreachable!() // <- this would be a foreign function call to allocate an object
+}
+
+#[trusted]
+#[requires(alloced(1, loc))]
+fn dealloc(loc: usize) {
+    unreachable!() // <- this would be a foreign function call to deallocate an object
+}
+
+#[trusted]
+#[requires(alloced(1, loc))]
+#[ensures(alloced(1, loc))]
+fn read_value(loc: usize) -> i32 {
+    unreachable!() // <- this would be a foreign function call to read the value of an object
+}
+
+#[trusted]
+#[requires(alloced(1, loc))]
+#[ensures(alloced(1, loc))]
+fn write_value(loc: usize, new_value: i32) {
+    unreachable!() // <- this would be a foreign function call to write a value to an object
+}
+
+fn procedure1() {
+    let obj_loc = alloc();
+    let old_value = read_value(obj_loc);
+    let new_value = if old_value > 0 {
+        old_value - 1
+    } else {
+        0
+    };
+    write_value(obj_loc, new_value);
+    dealloc(obj_loc);
+}
+
+fn procedure2() { //~ ERROR function might leak instances of obligation `alloced`
+    let obj_loc = alloc();
+    let old_value = read_value(obj_loc);
+    if old_value <= 0 {
+        return;
+    }
+    write_value(obj_loc, old_value - 1);
+    dealloc(obj_loc);
+}
+//// ANCHOR_END: code

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

@@ -0,0 +1,29 @@
+//// ANCHOR: nothing
+//// ANCHOR_END: nothing
+// The next line is only required for doctests, you can ignore/remove it
+extern crate prusti_contracts;
+use prusti_contracts::*;
+
+fn main() {}
+
+//// ANCHOR: code
+resource! {
+    fn rsrc(amount: usize);
+}
+
+obligation! {
+    fn oblg(amount: usize);
+}
+
+#[requires(rsrc(3))]
+#[ensures(rsrc(2))]
+fn with_resources() {
+    // does nothing
+}
+
+#[requires(oblg(3))]
+#[ensures(oblg(2))]
+fn with_obligations() { //~ ERROR function might leak instances of obligation `oblg`
+    // does nothing
+}
+//// ANCHOR_END: code

prusti-tests/tests/verify/pass/user-guide/inhale_exhale.rs

@@ -0,0 +1,31 @@
+//// ANCHOR: nothing
+//// ANCHOR_END: nothing
+// The next line is only required for doctests, you can ignore/remove it
+extern crate prusti_contracts;
+use prusti_contracts::*;
+
+fn main() {}
+
+//// ANCHOR: code
+obligation! {
+    fn o(amount: usize);
+}
+
+#[requires(o(3))]
+fn f1() {
+    prusti_exhale!(o(3));
+}
+
+#[requires(o(3))]
+fn f2() {
+    prusti_exhale!(o(1) & o(1));
+    prusti_exhale!(o(1));
+}
+
+#[requires(o(1))]
+#[ensures(o(3))]
+fn f3() {
+    prusti_inhale!(o(1));
+    prusti_inhale!(o(1));
+}
+//// ANCHOR_END: code