Expressions

How to write Scribble expressions

Scribble properties usually consist of three elements.

/// <specification_type> <msg> <condition>
‚Äč
Example:
/// if_succeeds {:msg "This is an example"} a == 1;

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. But, we have added some special functions and operators that make property writing that much easier.

Solidity

You write Scribble expressions in exactly the same way that you would write normal solidity expressions.

  1. Numbers, booleans and addresses

  2. State variables

  3. Function arguments and return values

  4. Member accesses (e.g. a.foo where a is a struct)

  5. Index accesses (e.g. a[5] where a is an array)

  6. Unary operations like - and !

  7. Binary opreations: +, -, *, /, %, **, <<, >>, |, &, ^, <, <=, >, >=, ==, !=, &&, ||

  8. Ternary operators (e.g. x < y ? x : y)

Changing State

Some Solidity expressions can change the state of a smart contract (e.g. i++ updates the value of i). This is something that we want to avoid doing in a specification language.

The reason? Scribble annotations are about the smart contract, they shouldn't actually change the contract. If we're altering how a smart contract works with our properties, then we're not testing / verifying the original contract anymore.

Pure and View

Scribble only allows function calls to pure and view functions.

Functions that are not pure or view can accidentally change the contract as we're checking properties. As a result, the properties calling into them could also result in changes.

Updating Expressions

Some expressions directly update a variable (e.g. i++), these are not allowed by Scribble.

Scribble Language Features

Referring to the previous state

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.

In short, you use old( expression ) to get the value of expression as it was at the beginning of a transaction.

Example 1: Constant
Example 2: Ownership
Example 3: Expression
Example 1: Constant

The balance of the sender before a transaction is equal to the balance after.

Scribble:

old(balance[mgs.sender]) == balance[msg.sender]
Example 2: Ownership

The old owner is not the new owner

Scribble:

old(owner) != owner
Example 3: Expression

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]

Binding return values

let <variable> := <expression> in <expression>

Example 1: Function return values
Example 2: Binding constants
Example 1: Function return values

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;
Example 2: Binding constants

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

Implication

<expression> ==> <expression>

In our annotations, we'll often use implications to specify some kind of conditional logic ( behaviours for example ).

An implication like A ==> Bdescribes 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 (B || !A)

Example 1: Simple implication
Example 2: Ownership
Example 1: Simple implication

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) { ... }
Example 2: Ownership

If there is a change to the owner variable, then the sender was the old owner.

owner != old(owner) ==> msg.sender == old(owner)