CertiK Prover user guide

Logic and quantifiers

Conditions can do more than compare two values. This chapter adds implication and equivalence, statements about every value or some value, and the exact arithmetic that specifications use.

You will learn: ==>, <==>, \forall, \exists, and how specification arithmetic differs from Solidity arithmetic.
Builds on: Your first specification and Security properties

Connect conditions

Specifications add two operators to Solidity's &&, ||, and !:

Form	Read it as
`P ==> Q`	If `P` is true, `Q` must be true. When `P` is false, the clause claims nothing.
`P <==> Q`	`P` and `Q` are both true or both false.

Implication makes a claim conditional. Crediting a positive amount must increase the balance:

//@ ensures amount > 0 ==> balances[to] > \old(balances[to]);

Equivalence pins down a Boolean result exactly: canPay returns true exactly when the balance covers the amount.

//@ ensures \result <==> balances[account] >= amount;
function canPay(address account, uint256 amount) external view returns (bool) {
    return balances[account] >= amount;
}

Use parentheses whenever ==> or <==> appears next to && or ||, so every reader sees the same grouping.

Every value: `\forall`

\forall (T x) P says that P holds for every value x of type T. The variable exists only inside the condition. This clause says that crediting to leaves every other account unchanged:

//@ ensures \forall (address a) a != to ==> balances[a] == \old(balances[a]);

A \forall over address covers every possible address, not only those a test happens to use. That is how a specification protects accounts nobody has thought of yet.

8//@ ensures balances[to] == \old(balances[to]) + amount;
9//@ ensures \forall (address a) a != to ==> balances[a] == \old(balances[a]);
10function credit(address to, uint256 amount) external {
11    require(to != treasury, "treasury");
12    balances[to] += amount;
13    balances[treasury] += amount / 100;
14}

Select Run CertiK Prover to check this code against its specification.

Some value: `\exists`

\exists (T x) P says that at least one value x of type T makes P true. Here, isEven returns true exactly when some k doubles to n:

//@ ensures \result <==> \exists (uint256 k) n == 2 * k;
function isEven(uint256 n) external pure returns (bool) {
    return n % 2 == 0;
}

Quantifiers make checks harder. A complicated quantified clause can end as Inconclusive, so keep each one as simple as the property allows.

Arithmetic without overflow

Arithmetic in a specification uses exact mathematical integers, called mathint: a + b never overflows or wraps, even when a and b are uint256. That makes overflow easy to state: add reverts exactly when the true sum exceeds the largest uint256.

//@ ensures \result == a + b;
//@ reverts_when_and_only_when a + b > type(uint256).max;
function add(uint256 a, uint256 b) external pure returns (uint256) {
    return a + b;
}

Code is different: Solidity arithmetic still checks for overflow, and an unchecked block wraps around. When code wraps on purpose, state the wrap explicitly with % 2**256:

//@ ensures \result == (x + 1) % 2**256;
function next(uint256 x) external pure returns (uint256) {
    unchecked {
        return x + 1;
    }
}

5//@ ensures \result == x + 1;
6function next(uint256 x) external pure returns (uint256) {
7    unchecked {
8        return x + 1;
9    }
10}

Select Run CertiK Prover to check this code against its specification.

Run the full examples

Every code sample and playground on this page is a complete contract in the CertiK Prover Server Tutorial project, where CertiK Prover runs it on the server. Sign in and open an entry's results to see the real run behind each simulated one.