# Rust Contracts

Prusti Zulip: https://prusti.zulipchat.com/

## Contracts Supported by Prusti

### Attributes and Function-Like Contracts

Here `A` is an assertion (described below):

* `#[requires(A)]` – (function/method) precondition.
* `#[ensures(A)]` – (function/method) postcondition.
* `#[after_expiry(R => A)]` – pledge in a postcondition on reference `R`.
* `#[after_expiry_if(R => A, A)]` – guarded pledge in a postcondition on reference `R`.
* `body_invariant!(A)` – loop body invariant.
* `#[pure]` – marks the annotated function/method as pure.
* `#[trusted]` – marks the annotated function/method as trusted.

### Assertions

An assertion can be:

* A conjuction of assertions.
* An implication `A1 ==> A2` where `A1` and `A2` are assertions. (Note: due to [a bug](https://github.com/viperproject/prusti-dev/issues/127) in the Rust compiler, the implication with a space `== >` is also accepted by the parser).
* A quantifier `forall(|args| A, triggers)` where `args` are variables bound by the quantifier, `A` is an assertion, and `triggers` are the Rust expressions used to trigger the quantifier.

The parser treats `old` and `before_expiry` as regular function calls. The special semantics are given to them in the later stages of Prusti.

## Contracts Supported by `contracts`

Contracts generally have the shape `#[name(expr, expr, ... expr, "description")]`. The description has to be the last argument of the attribute and needs to be a string literal.
Only one expression is required but more can be used with `,` to create a conjunction.

All contracts have `debug_` and `test_` versions of the attributes (for example `debug_ensures` and `test_requires`) which are only checked in debug builds or when the `test` cfg is set.

### On functions (and methods)

Expressions are regular Rust expressions, "anything goes" (no side-effect checks since that's very tricky in a proc-macro crate).

Additionally expressions can contain `->` as a binary operator for implication. The `->` was chosen over `==>` due to `rustc` erasing spacing information when using `==>`.

- Preconditions
- `#[requires(x + 2 < self.len())]`
- Checked before the body of the function runs

- Postconditions
- `#[ensures(ret % 2 == 0)]`
- Checked after the body of the function ran
- The name `ret` is bound to the return value of the funtcion
- supports `old(expr)` in the contract expressions
- Generates a `let` binding with a generated name before the function body executes, the `old(..)` call gets replaced with the generated name

- Invariants
- `#[invariant(self.value <= 100)]`
- The same as a pre-condition *and* a post-condition with the same expression
- Because it needs to be a valid `#[pre]` condition the `old(expr)` function is not supported

### On `impl Type` blocks

- Invariants
- `#[invariant(self.value <= 100)]`
- Injects the `#[invariant]` attribute on all methods that take `&self` or `&mut self`
- Does not apply to `fn new() -> Self` or methods that move `self`

### On `trait`s and Trait `impl`s

To check contracts on traits at runtime a trait must be marked with the `#[contract_trait]`

To implement a trait with contracts also the `impl` block needs the `#[contract_trait]` attribute.

### Planned features

- `unchanged` attribute, `#[unchanged(expr)]` => `#[ensures(old(expr) == expr)]`
- ACSL like `behaviour` attributes to group together contracts for different behaviours of a function
- Loop invariants as function-like procedural macros
- "Ghost code" support for existential quantifiers
- universal quantifier `forall` inside contract expressions

## Syntax Differences between Prusti and `contracts`

* Different operators for implication (`==>` vs `->`).
* `contracts` attributes can have a string literal description as the last attribute argument
* `contracts` has different versions of attributes for debug and test environments

## Communalities between Prusti and `contracts`

* Both implemented completely by using Rust procedural macros.
* Assertions are structurally very similar: contain conjuctions and implications that connect Rust expressions.
* `old()` functions to use values from before the function body in post-conditions