4.3. Preserved blocks

Sometimes invariants need additional assumptions or other invariants for the Prover to successfully verify them. Preserved blocks allow us to add these assumptions to the invariants.

Worked example

Here is an example explaining the need for preserved blocks and their use. The file DebtToken.sol contains a partial implementation of a debt token. The contract keeps track of both the balances of the users and the values of their collaterals. Most importantly, the contract should ensure that a user’s balance never exceeds their collateral value.

Failed spec

To verify this property, we write a short spec FailedDebtToken.spec with a single invariant shown below

FailedDebtToken.spec
methods {
    function balanceOf(address) external returns (uint256) envfree;
    function collateralOf(address) external returns (uint256) envfree;
}


/// @title Collateral is never less than the balance
invariant collateralCoversBalance(address account)
    collateralOf(account) >= balanceOf(account);

Running this spec (using FailedDebtToken.conf ) results in a violation. Try to understand the violation for yourself.

Violation

The violation occurs in the “induction step” for the function transferDebt.

  1. At the onset (the pre-state) we have two addresses: account for which we are proving the invariant, and another address named another. These are their values at the pre-state:

    Storage at pre-state

    address

    balanceOf

    _collateralValue

    account

    1

    2

    another

    2

    0

  2. The invariant obviously holds in this pre-state:

    2 == collateralOf(account) >= balanceOf(account) == 1
    
  3. Execute transferDebt(account) where msg.sender is another.

  4. The final state after executing transferDebt(account) is:

    Storage after transferDebt

    address

    balanceOf

    _collateralValue

    account

    3

    2

    another

    0

    0

The final state clearly violates the invariant since:

2 == collateralOf(account) < balanceOf(account) == 3

Correct invariant

The problem with the Violation above is that the address another does not satisfy the invariant at start, i.e. at the pre-state. We need require that it satisfies the invariant at the start as well. Here is the syntax to do so, from DebtToken.spec:

DebtToken.spec
/// @title Collateral is never less than the balance
invariant collateralCoversBalance(address account)
    collateralOf(account) >= balanceOf(account)
    {
        preserved transferDebt(address recipient) with (env e)
        {
            requireInvariant collateralCoversBalance(e.msg.sender);
        }
    }

Run this spec using DebtToken.conf, and you will find the rule is verified.

Important notes

Why not use require?

Using a requireInvariant statement is sound, provided we prove the required invariant. On the other hand, a require statement can be a source of unsoundness, meaning it can cause us to miss violations.

Isn’t requireInvariant collateralCoversBalance... using what you’re trying to prove?

The answer is no. We’re basically using the induction assumption for another address. The section Invariants and induction expounds on that.

What is the env e doing here?

The function transferDebt is not envfree, so when the Certora Prover calls transferDebt it uses some environment. The syntax with (env e) allows us to access and use this environment inside the preserved block. For more information, see Preserved blocks.

Default preserved block

One can add a general preserved block, that will be applied by default (i.e. if no other preserved block holds). The syntax is simple:

invariant someInvariant()
    // Invariant condition
    {
        preserved {
            // Default preserved block
        }
        // Additional preserved blocks
    }

Funds managers exercise

This is an exercise for using preserved blocks and requireInvariant statements in invariants.

Background

The IManager is a rudimentary interface for keeping track of managers for funds, where:

  • A manager is simply an address

  • A fund is identified by uint256 fundId

  • Every fund must have a unique manager

  • To change managers:

    1. The current manager must set their successor as the pending manager.

    2. The pending manager must then claim management using the claimManagement method.

Exercises

In the folder manager are three implementations of the IManager interface. One is correct and the others are buggy.

  • Write an invariant verifying that no two funds have the same manager.

  • Make sure your invariant is sound. Remember requireInvariant in preserved blocks is sound (provided you also prove the required invariant). See Invariants and induction.

  • Test your invariant by running it on the implementations and finding the bugs.

Hints

Hint

You may need to prove that a fund’s manager is active.

Hint

The additional invariants you’ll need may require the invariant you’re trying to prove. This is ok when done correctly, see Invariants and induction.

Solution

A full solution is available in Manager_unique.spec.