🎓 A1Learner
🔍
0 of 45 lessons completed

Solidity Invariant Testing in Depth

Solidity invariant testing in depth is the practice of checking one rule after every action in a long sequence of calls. The rule in this lesson is that the sum of recorded balances always equals the ether the vault holds.

A handler checks the rule after every step

The handler deposits for two actors and withdraws for one. The proof checks the rule after each handler call.

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.30;

contract Vault {
    mapping(address => uint256) public balances;

    function deposit() public payable {
        balances[msg.sender] += msg.value;
    }

    function withdraw(uint256 amount) public {
        require(balances[msg.sender] >= amount, "too much");
        balances[msg.sender] -= amount;
        (bool success, ) = payable(msg.sender).call{value: amount}("");
        require(success, "send failed");
    }
}

The buggy vault breaks the rule on purpose

BuggyVault sends ether without reducing the recorded balance. After one withdrawal the recorded balance is larger than the ether held.

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.30;

contract BuggyVault {
    mapping(address => uint256) public balances;

    function deposit() public payable {
        balances[msg.sender] += msg.value;
    }

    function withdraw(uint256 amount) public {
        require(balances[msg.sender] >= amount, "too much");
        (bool success, ) = payable(msg.sender).call{value: amount}("");
        require(success, "send failed");
    }
}

The fixed vault holds the rule through the same steps

FixedVault reduces the recorded balance before it sends ether. The same sequence now keeps the rule true after every step.

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.30;

contract FixedVault {
    mapping(address => uint256) public balances;

    function deposit() public payable {
        balances[msg.sender] += msg.value;
    }

    function withdraw(uint256 amount) public {
        require(balances[msg.sender] >= amount, "too much");
        balances[msg.sender] -= amount;
        (bool success, ) = payable(msg.sender).call{value: amount}("");
        require(success, "send failed");
    }
}

Example

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.30;

contract InvariantVault {
    mapping(address => uint256) public balances;

    function deposit() public payable {
        balances[msg.sender] += msg.value;
    }

    function withdraw(uint256 amount) public {
        require(balances[msg.sender] >= amount, "too much");
        balances[msg.sender] -= amount;
        (bool success, ) = payable(msg.sender).call{value: amount}("");
        require(success, "send failed");
    }

    function transfer(address to, uint256 amount) public {
        require(balances[msg.sender] >= amount, "too much");
        balances[msg.sender] -= amount;
        balances[to] += amount;
    }
}

Key points

  • Invariant: An invariant is a rule that must stay true after every action in the sequence.
  • Handler: A handler is a helper contract that performs calls from several actors in a fixed order.
  • Fixed sequence: A fixed sequence is a set order of deposits, transfers, and withdrawals.
  • Break: A break is a step after which the rule no longer holds.
  • Restatement: Checking the rule after every step catches a break that a final check alone would miss.

In this example, InvariantVault holds a balance mapping with deposit, withdraw, and transfer. deposit adds ether and records it together. transfer moves a recorded balance between two holders without changing the vault total. withdraw reduces the recorded balance before sending, and the proof checks the sum rule after each step of the sequence.

Note

The invariant here covers only the two known holders, since a mapping cannot be listed in full.

Try it Yourself

Edit the code, then press Run.

Running is simulated · Remix IDE

Exercise

A handler runs deposits, a transfer, and a withdrawal, checking the sum rule after each step. The transfer step breaks the rule. What does the handler approach catch that a final check alone might miss?