Introduction
All scribble properties are expressed as specially formatted docstrings. For example:
1
contract Foo {
2
/// #if_succeeds {:msg "P0"} y == x + 1;
3
function foo(uint256 x) public returns (uint256 y) {
4
return x + 1;
5
}
6
}
Copied!
In the above sample `if_succeeds {:msg "P0"} y == x + 1;` is the property. Note the semicolon at the end - it is required for all properties.
There are 2 types of properties supported currently:
1. 1.
`if_succeeds` properties are specified only before functions. They specify conditions that must hold if the function returns successfully
2. 2.
`invariant` properties are specified only before contracts. They specify conditions that must hold whenever we are NOT executing code in the contract.
All properties allow adding a human-readable message using `{:msg "message"}`. This is helpful when mapping the properties to their description in other documents, or just as a reminder about the intent of a complex property.
The expressions that are allowed in custom properties are mostly a subset of Solidity expressions, with some additional syntactic sugar described below.
We will first outline some small differences between `if_succeeds` and `invariant` expressions, and then describe in-depth the allowed expressions.

# Examples

Lets look at several examples.

## Using old

In the below contract `inc` increments the variable of the state var `x` by 1. The property `x == old(x) + 1` captures exactly the same intuition.
1
contract Foo {
2
int x = 1;
3
/// #if_succeeds {:msg "P0"} x == old(x) + 1;
4
function inc() public {
5
x = x + 1;
6
}
7
}
Copied!
Note that we can also write that property as `x == old(x + 1)` since the value of the constant `1` doesn't change before and after the function.

## Incrementing contract

For the contract from the previous example we can also add a contract invariant stating that `x >= 1` as shown below:
1
/// #invariant {:msg "P1"} x >= 1;
2
contract Foo {
3
int x = 1;
4
/// #if_succeeds {:msg "P0"} x == old(x) + 1;
5
function inc() public {
6
x = x + 1;
7
}
8
}
Copied!

## Expressing pre/post conditions using implication

In verification people often think of function pre- and post- conditions (these come from Hoare logic). One can encode a precondition `P` and post-condition `Q` as: `P ==> Q`. So for example for the `sillyDiv` function below, we can express a pre-condition (`y != 0`) and post-condition (`z == x/y`) as `y!=0 ==> z == x/y`.
1
contract Div {
2
/// #if_succeeds {:msg "P0"} y != 0 ==> z == x / y;
3
function sillyDiv(uint x, uint y) public returns (uint z) {
4
return y != 0 ? x/y : 0;
5
}
6
}
Copied!
Note that this specification is incomplete - it doesn't say what happens when `y == 0`. We can make it complete by adding another property:
1
contract Div {
2
/// #if_succeeds {:msg "P0"} y != 0 ==> z == x / y;
3
/// #if_succeeds {:msg "P0"} y == 0 ==> z == 0;
4
function sillyDiv(uint x, uint y) public returns (uint z) {
5
return y != 0 ? x/y : 0;
6
}
7
}
Copied!
Multiple `if_succeeds` annotations for the same functions are conjoined together. The same holds for multiple `invariant` annotations for a contract.