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.

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

Storage at *pre-state*¶
`address`	`balanceOf`	`_collateralValue`
`account`	`1`	`2`
`another`	`2`	`0`

The invariant obviously holds in this pre-state:

2 == collateralOf(account) >= balanceOf(account) == 1

Execute transferDebt(account) where msg.sender is another.
The final state after executing transferDebt(account) is:

Storage after transferDebt¶

address

balanceOf

_collateralValue

account

3

2

another

0

0

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 it has a debt of 2 but 0 collateral. We need to require another to satisfy the invariant at the start so there is no bad debt to transfer. 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 there is no other preserved block that applies to a function). 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. Modify the conf (or command line) to find the bugs in ManagerBug1.sol and ManagerBug2.sol.