CertiK Prover
Login

CertiK Prover user guide

Loops

A loop can repeat any number of times, so CertiK Prover cannot simply try every repetition. Instead, you describe the loop with clauses that hold on every repetition, and CertiK Prover proves the rest of the function from them.

You will learn
Loop invariants with maintaining, loop frames with assigning, and termination with decreasing.

Three loop clauses

Write loop clauses directly above a for, while, or do while loop:

FormMeaning
maintaining P;A loop invariant: true before the first repetition and after every repetition.
assigning x, y;The loop frame: the only variables the loop may change. Every loop needs one.
decreasing e;A measure that stays non-negative and shrinks on every repetition, which proves that the loop ends.

Prove a sum

triangle(n) adds 1 + 2 + … + n. The invariant states what is true once the first i - 1 numbers have been added. When the loop ends with i == n + 1, it gives exactly the postcondition:

//@ ensures \result == n * (n + 1) / 2;
function triangle(uint256 n) external pure returns (uint256) {
    uint256 total = 0;
    //@ maintaining 1 <= i && i <= n + 1;
    //@ maintaining total == (i - 1) * i / 2;
    //@ decreasing n + 1 - i;
    //@ assigning i, total;
    for (uint256 i = 1; i <= n; i++) {
        total += i;
    }
    return total;
}

  1. Before the loop

    i == 1 and total == 0, so total == (i - 1) * i / 2 holds.

  2. Each repetition

    Adding i to total and then incrementing i keeps the invariant true.

  3. After the loop

    i == n + 1, so the invariant becomes total == n * (n + 1) / 2.

After a loop, CertiK Prover knows only that the loop condition is false and that the invariants hold. Anything an invariant does not state is forgotten.

Try it

An off-by-one loop bound

triangle(n) should add every number from 1 to n. Does the loop stop at the right place?

Read-only
//@ ensures \result == n * (n + 1) / 2;
function triangle(uint256 n) external pure returns (uint256) {
    uint256 total = 0;
    //@ maintaining 1 <= i && i <= n + 1;
    //@ maintaining total == (i - 1) * i / 2;
    //@ decreasing n + 1 - i;
    //@ assigning i, total;
    for (uint256 i = 1; i < n; i++) {
        total += i;
    }
    return total;
}

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

When the invariant is too weak

If an invariant leaves something out, CertiK Prover cannot recover it after the loop, even when the code is correct. In the next playground the code never changes; only the invariant does.

Try it

An invariant that says too little

The code is correct. Can CertiK Prover prove the result without an invariant about total?

Read-only
//@ ensures \result == n * (n + 1) / 2;
function triangle(uint256 n) external pure returns (uint256) {
    uint256 total = 0;
    //@ maintaining 1 <= i && i <= n + 1;
    //@ decreasing n + 1 - i;
    //@ assigning i, total;
    for (uint256 i = 1; i <= n; i++) {
        total += i;
    }
    return total;
}

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

More loop patterns

A while loop that counts up, and a loop that sums part of an array, where \sum_of(values[0:i]) is the sum of the first i entries:

//@ ensures \result == 2 * n;
//@ assignable \nothing;
function doubleN(uint256 n) public pure returns (uint256) {
    uint256 result = 0;
    uint256 i = 0;
    //@ maintaining result == 2 * i;
    //@ maintaining i <= n;
    //@ decreasing n - i;
    //@ assigning i, result;
    while (i < n) {
        result += 2;
        i++;
    }
    return result;
}
//@ requires end <= values.length;
//@ ensures \result == \sum_of(values[0:end]);
//@ assignable \nothing;
function prefixSum(uint256[] calldata values, uint256 end) external pure returns (uint256 total) {
    //@ maintaining i <= end;
    //@ maintaining total == \sum_of(values[0:i]);
    //@ decreasing end - i;
    //@ assigning total, i;
    for (uint256 i = 0; i < end; i++) {
        total += values[i];
    }
}

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.