Scribble
Search…
Language
Contract Annotations
Properties that should always hold.
Contract invariants are properties that we expect to be maintained by the contract at 'all times'.
Invariant example: "The total of all balances doesn't change"
Contract invariants in Scribble are similar to class invariants in object oriented languages - internal functions to the contract are allowed to temporarily violate the invariants. However whenever we "exit" the contract (by either returning from an external call into it, or by making an external call from it), the invariants must be true. We refer to these points in the execution as places where the state is externally observable.
Observable State
The state of a contract is observable whenever some external contract can read it.
before call (observable): The state of a contract before executing a transaction is observable! At this point anyone, and any contract could read and call into a contract. Those callers / readers expect the invariant to hold.
during call (not-observable): During a contract's execution nobody looks at the state of the contract. So it's fine if an invariant doesn't hold at this point.
before making external call out (observable): If we call to another contract, then that contract can read our state or call back. This external contract expects the invariant to hold!
after (returning from) external call (observable): Once a contract is finished executing we are back to a scenario where anyone and any contract can read and call into our state. So, the invariant should hold again at this point.
Example Observability
Let's explore an example. The invariant we'll use is "the variable x is 0"
1
/// #invariant {:msg "the variable x is 0"} x == 0;
2
contract Example {
3
// Good, x holds in the beginning
4
uint public x = 0;
5
6
function example_observability() {
7
// x should be 0 here
8
x *= 10;
9
// x is still 0 if x was zero
10
return;
11
// x is still zero if x was zero, great!
12
}
13
14
function example_violation() {
15
// x should be 0 here
16
x += 1;
17
return;
18
// x is not zero anymore 😢
19
// now the invariant is violated
20
}
21
22
23
function example_nonviolation() {
24
// x should be 0 here
25
x += 1;
26
// Now x is non zero, but that doesn't matter. We're not "observable".
27
x -= 1;
28
// We immediately return x back to what it was
29
return;
30
// x is back to zero again (if it was zero before)!
31
}
32
33
function example_external(address externalContract) {
34
// x should be 0 here
35
x += 1;
36
// Now x is non zero. Which violates the invariant.
37
externalContract.call();
38
39
// externalContract might call back into us, assuming that the invariant holds
40
// For example:
41
// If externalContract calls this.example_observability(), expecting all invariants to hold.
42
// Unfortunately, x is not 0. example_observability()'s assumption is violated.
43
44
return;
45
}
46
47
}
Copied!
Syntax
Invariants have the following structure, and are placed above contract declarations:
1
invariant {:msg "<Description of your property>"} <boolean scribble expression>;
Copied!
Example 1
Example 2
This is a property could be used in a token contract to assert that the token is not inflationary or deflationary.
1
/// #invariant {:msg "The total balance doesn't change."} totalBalance == old(totalBalance);
2
contract ExampleContract {
3
4
}
Copied!
The following property is very common. It checks that if the owner of a contract changes, then msg.sender must have been the old owner.
1
/// #invariant {:msg "Only the owner changes the owner"} owner != old(owner) ==> msg.sender == old(owner);
2
contract ExampleContract {
3
address public owner;
4
}
Copied!
External Calls
Don't use external calls in invariants!
There are two kinds of external calls: Ones that call to
this and ones that call into other contracts.Scribble asserts that an invariant is valid at the end of contract construction, as this is the first point where contract state becomes observable. However, due to the mechanics of the EVM the contract account is not 100% set up. Calls into the contract don't work yet, because there is not actually any code at the contract address until the constructor returns. This is why you can't use re-entrant calls like
this.getTotalBalance() in a contract invariant.The second type of external call, those to other contracts, is possible with Scribble. But we consider this an anti-pattern.
Invariants are meant to describe properties that must always hold for a single contract. We write properties for the contract in isolation, agnostic of any external components. This makes testing more efficient and reflects the composability of (DeFi) smart contracts.
Last modified 7mo ago
Copy link