CertiK Prover user guide

Multiple cases and modifiers

Some functions behave differently depending on their input, and some share setup code in modifiers. This chapter shows how to write one specification case per behavior, and how to specify what a modifier does around the function it wraps.

You will learn: also, let, and the modifier clauses establishes and expects.
Builds on: Your first specification

One case per behavior: `also`

also splits a function's specification into cases. Each case has its own requires, ensures, assignable, and revert clauses. Here, withdrawing zero changes nothing, while a positive withdrawal reduces the balance:

//@ let (uint256 entryBalance) = balance;
//@ requires amount == 0;
//@ ensures balance == entryBalance;
//@ assignable \nothing;
//@ also
//@ requires amount > 0 && amount <= balance;
//@ ensures balance == entryBalance - amount;
//@ assignable balance;
function withdraw(uint256 amount) external {
    if (amount > 0) {
        balance -= amount;
    }
}

At a call, at least one case's requires must hold.
Every case whose requires holds must be satisfied; CertiK Prover does not stop at the first match.
Prefer clear, separate cases over one weak case that blurs them together.

let (uint256 entryBalance) = balance; captures a value once, before any case starts, and every case can use it. A let value can never be reassigned.

5//@ requires amount < 100;
6//@ ensures \result == 0;
7//@ also
8//@ requires amount >= 100;
9//@ ensures \result == amount / 100;
10function fee(uint256 amount) external pure returns (uint256) {
11    if (amount <= 100) {
12        return 0;
13    }
14    return amount / 100;
15}

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

Modifiers

A modifier wraps a function: its code runs before and after the _ placeholder. A modifier specification describes both halves, using two extra clauses:

Clause	Checked
`requires P;`	When the modifier starts.
`establishes P;`	Just before `_`: the code before it must make `P` true for the wrapped function.
`expects P;`	Just after `_`: the wrapped function must leave `P` true.
`ensures P;`	When the modifier finishes.
`assignable x;`	Limits what the modifier itself may change.

In this gate, the modifier closes the gate before the function runs and reopens it afterward. The wrapped function use may change only used, so the gate is still closed when _ returns:

//@ requires open;
//@ establishes !open;
//@ expects !open;
//@ ensures open;
//@ assignable open;
modifier onlyOpen() {
    require(open, "gate closed");
    open = false;
    _;
    open = true;
}

//@ requires open;
//@ assignable used;
function use() external onlyOpen {
    used = true;
}

expects is not an entry condition. It is checked after the wrapped function has run; use requires for what must hold at the start.

8//@ requires open;
9//@ establishes !open;
10//@ expects !open;
11//@ ensures open;
12//@ assignable open;
13modifier onlyOpen() {
14    require(open, "gate closed");
15    open = false;
16    _;
17}

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.

Multiple cases and modifiers

One case per behavior: `also`

A boundary in the wrong case

Modifiers

A gate that never reopens

Run the full examples