Comment on page
Expressions
How to write Scribble expressions
Scribble property annotations usually consist of three elements:
/// <property_type> <msg> <condition>
Example:
/// #if_succeeds {:msg "This is an example"} a == 1;
The property type is one of several expected keywords (
if_succeeds, invariant, if_updated, assert ). The <msg> part defines a human readable label for the property. It is either in the format {:msg "The label"} or just the short-hand "The label".The condition is an expression that evaluates to a boolean (True / False). For the most part, you use the same syntax here as in regular Solidity expressions. To ease development we have added some special functions and operators that are described in this section.
You can use the following standard Solidity expressions in Scribble expressions:
- 1.Numbers, boolean litearls and addresse literals
- 2.Identifiers naming state variables and function arguments and return values
- 3.Member accesses (e.g.
a.foowhereais a struct) - 4.Index accesses (e.g.
a[5]whereais an array or a map) - 5.Unary operators -
-and! - 6.Binary operators -
+,-,*,/,%,**,<<,>>,|,&,^,<,<=,>,>=,==,!=,&&,|| - 7.Ternary operators (e.g.
x < y ? x : y) - 8.Function calls (e.g.
foo(1,true, x))
As of Solidity 0.8.0 all arithmetic is checked by default - that is an exception is thrown (i.e. your code reverts) whenever an overflow or underflow happens. Scribble arithmetic on the other hand is unchecked - that is overflows/underflows would happen silently, without a revert. This is on purpose, as we want to minimize the conditions under which an exception would originate from the instrumentation. However this requires users to be mindful of whether overflow may happen in arithmetic inside their properties.
Some Solidity expressions can change the state of a smart contract (e.g.
i++ and (somewhat surprisingly) i=1 are both expressions modifying state in Solidity) . In Scribble we forbid such expressions, as we don't want annotations to change state in any way.For the same reason, while Scribble expressions allow function calls, they only allow calls to pure and view functions.
We add several extensions to Scribble on top of the core Solidity language. These are described in this section.
syntax: old( <expression> )
You can't use old() in invariants!
When writing properties, you'll often want to describe how state is expected to change. For example, you might expect some persons balance to increase.To write these properties, you'll be able to use the old() construct.
You can talk about state changing only in
if_succeds and if_updated invariants. In the case of if_succeeds invariants old(expression) refers to the value of the expression before the function began executing. In the case of if_updated old(expression) refers to the value of the expression before the annotated variable was updated.Example 1: Constant
Example 2: Ownership
Example 3: Expression
The balance of the sender before a transaction is equal to the balance after.
Scribble:
old(balance[mgs.sender]) == balance[msg.sender]
The old owner is not the new owner
Scribble:
old(owner) != owner
The sum of balances between the sender and receiver is the same before and after a transaction.
You can put any expression in old(...), not just single variables.
old(balance[sender] + balance[receiver]) == balance[sender] + balance[receiver]
Note that the type of the expression inside
old(expression) can be any primitive value type - e.g. number, fixed bytes, address, boolean, etc. However we disallow reference types such as arrays, maps, structs, strings and bytes. This is done to limit the overhead of our instrumentation, since making a copy of such (usually dynamically sized) types may require loops. In the future we amy reconsider this decision, given enough interest.let <variable> := <expression> in <expression>For convenience you can defined immutable variables that can be used inside of an annotation. This can be useful in several cases:
1. Reducing duplication. If the same expression
E appears multiple times inside of the annotation A, you can re-write A as let x := E in A' where A' is the same as A with E replaced with x.2. Unpacking multiple returns values of a function and giving them names (see below example)
3. Giving human-readable names to certain expressions/constats for more readability.
Function return values
Binding constants
Multiple lets
In this example we assume there is a function
unpack() that returns three values: amount, sender and receiver.In this example, we'll write a property that only uses one of the variables (the amount) and checks that it is bigger than zero.
If you don't use a variable replace it with `_` to make your property easy to read.
let amount, sender, _ := unpack(packedTransaction) in amout >= 0;
You are not limited to binding function return values.
Take the following expression for example, this evaluates to 25.
let x := 5 in x * x
Sometimes you might need multiple let bindings.
In the following example we first bind the
balance variable, and then we use it to compute and bind halfBalance. Which we end up using to check halfBalance >= amount.Both balance and halfBalance can be used in the final expression!
/// if_succeeds {:msg "You can only extract half of the current balance in one time"}
/// let balance = token.balanceOf(this) in
/// let halfBalance = balance / 2 in
/// halfBalance >= amount;
function extractFunds(uint amount) public returns (bool) {
...
}
Sometimes you may want to use a
let- binding variable inside of an old() expression in the body of the let, as in the contrived example below:contract Foo {
uint x;
/// #if_succeeds let t:= x in old(t+1) > 10;
function foo() public {
...
}
}
However running the above code through scribble would result in the following error:
tmp.sol:5:5 TypeError: Variable t is defined in the new context in (let t := x in (old((t + 1)) > 10)) but used in an old() expression
In:
if_succeeds let t:= x in old(t+1) > 10;
The issue we are running into is, that the expression that
t is bound to is implicitly computed after the original function was called, but we are attempting to use it in a computation that is executed before the original function was called. Since doing this requires time travel, we obviously cannot make it happen. The fix in such a scenario is to wrap the expression that t is bound to in an old() expression like so: /// #if_succeeds let t:= old(x) in old(t+1) > 10;
function foo() public {
...
}
If that doesn't fix our problem, then we should re-think the property we are trying to express.
<expression> ==> <expression>In our annotations, we'll often use implications to specify some kind of conditional logic ( behaviours for example ).
An implication like
A ==> B describes that B must be true if A is true. If A isn't true, then it doesn't matter whether B is true or false.
In natural language, you can usually describe an implication as: If A, then also B.Fun Fact:
A ==> B is equivalent to (!A || B)Example 1: Simple implication
Example 2: Ownership
If the input to a function is negative, then the output is as well.
/// #if_succeeds {:msg "negativity"} input < 0 ==> output < 0;
function convert(uint input) public returns (uint output) { ... }
If there is a change to the owner variable, then the sender was the old owner.
owner != old(owner) ==> msg.sender == old(owner)
unchecked_sum(<expression>)Sometimes a property wants to talk about the sum of numeric values in an array or a map. For such cases we have introduced the
unchecked_sum() builtin function. You can apply it to both numeric maps and arrays.Example 1: Token balances
Example 2: Constant Supply
This example uses
unchecked_sum() to ensure that the sum of balances is equal to the mintedTokens variable./// #invariant unchecked_sum(balances) == mintedTokens;
contract Token {
uint mintedTokens;
mapping(address=>uint) balances;
...
}
Here you can see how we use sum to make sure no new tokens get minted.
/// #if_succeeds old(unchecked_sum(balances)) == unchecked_sum(balances);
contract Token {
mapping(address=>uint) balances;
...
}
The return type for
unchecked_sum() is always either uint256 or int256 (depending on whether the underlying map/array is signed). While it may seem confusing that unchecked_sum(arr) is int256 even if arr itself is int8, this was done on purpose, to minimize the chance of overflow when working with small integer types.Speaking of overflow, as the name
unchecked_sum suggests, the computation of the sum is UNCHECKED and thus may overflow silently. It is up to the user to add additional annotations to ensure that the sum of entries in an array doesn't overflow. In the future we may add a checked version of the sum, that fails loudly when the summation overflows.
Last modified 1yr ago