docs: add erc20 invariant testing examples (#548)

Author: daejunpark

.github/workflows/test-long.yml

@@ -22,6 +22,7 @@ jobs:
         testname:
           - "tests/solver"
           - "examples/simple"
+          - "examples/invariants"
           - "examples/tokens/ERC20"
           - "examples/tokens/ERC721"
 

examples/README.md

@@ -3,6 +3,7 @@
 #### Usage Examples
 
 - [Simple examples](simple/test/)
+- [Invariant testing](invariants/test/)
 - [ERC20](tokens/ERC20/test/): verifies OpenZeppelin, Solady, Solmate ERC20 tokens, and CurveTokenV3.
   - Includes identifying the DEI token bug exploited in the [Deus DAO hack](https://rekt.news/deus-dao-r3kt/).
 - [ERC721](tokens/ERC721/test/): verifies OpenZeppelin, Solady, and Solmate ERC721 tokens.

examples/invariants/foundry.toml

@@ -0,0 +1,6 @@
+[profile.default]
+src = "src"
+out = "out"
+libs = ["../../tests/lib", "lib"]
+
+evm_version = 'cancun'

examples/invariants/remappings.txt

@@ -0,0 +1 @@
+openzeppelin/=../../tests/lib/openzeppelin-contracts/contracts/

examples/invariants/src/ERC20.sol

@@ -0,0 +1,19 @@
+// SPDX-License-Identifier: AGPL-3.0
+pragma solidity >=0.8.0 <0.9.0;
+
+// from https://github.com/aviggiano/halmos-stateful-erc20/blob/main/src/ERC20.sol
+
+import {ERC20 as OpenZeppelinERC20} from "openzeppelin/token/ERC20/ERC20.sol";
+import {Ownable} from "openzeppelin/access/Ownable.sol";
+
+contract ERC20 is OpenZeppelinERC20, Ownable {
+    constructor(string memory name, string memory symbol) OpenZeppelinERC20(name, symbol) Ownable(msg.sender) { }
+
+    function mint(address to, uint256 amount) public virtual onlyOwner {
+        _mint(to, amount);
+    }
+
+    function burn(address from, uint256 amount) public virtual onlyOwner {
+        _burn(from, amount);
+    }
+}

examples/invariants/src/ERC721.sol

@@ -0,0 +1,13 @@
+// SPDX-License-Identifier: AGPL-3.0
+pragma solidity >=0.8.0 <0.9.0;
+
+import {ERC721 as OpenZeppelinERC721} from "openzeppelin/token/ERC721/ERC721.sol";
+import {Ownable} from "openzeppelin/access/Ownable.sol";
+
+contract ERC721 is OpenZeppelinERC721, Ownable {
+    constructor(string memory name, string memory symbol) OpenZeppelinERC721(name, symbol) Ownable(msg.sender) { }
+
+    function mint(address to, uint256 tokenId) public virtual onlyOwner {
+        _mint(to, tokenId);
+    }
+}

examples/simple/src/MiniVat.sol examples/invariants/src/MiniVat.solexamples/simple/src/MiniVat.sol renamed to examples/invariants/src/MiniVat.sol

@@ -0,0 +1,97 @@
+// SPDX-License-Identifier: AGPL-3.0
+pragma solidity >=0.8.0 <0.9.0;
+
+// inspired by https://github.com/aviggiano/halmos-stateful-erc20
+
+import {ERC20} from "../src/ERC20.sol";
+import {Test} from "forge-std/Test.sol";
+
+/// @custom:halmos --solver bitwuzla-abs --loop 3 --solver-timeout-assertion 0
+contract ERC20Test is Test {
+    // token address
+    ERC20 internal token;
+
+    // token holders
+    address[] internal holders;
+
+    function setUp() public virtual {
+        // deploy token
+        token = new ERC20("ERC20", "ERC20");
+
+        // declare token holders
+        holders = new address[](3);
+        holders[0] = address(0x1001);
+        holders[1] = address(0x1002);
+        holders[2] = address(0x1003);
+
+        // setup initial balances
+        for (uint i = 0; i < holders.length; i++) {
+            token.mint(holders[i], 1_000_000e18);
+        }
+
+        // register this contract as the target to call the handler functions
+        targetContract(address(this));
+    }
+
+    /*
+     * handlers
+     *
+     * handlers are used to track token holders, allowing us to iterate over
+     * them when calculating the sum of balances for specifying invariants.
+     * for simplicity, in this example, only the initial token holders are
+     * allowed as recipients of tokens.
+     */
+
+    function transfer(address to, uint256 amount) public asCaller assumeHolder(to) returns (bool) {
+        return token.transfer(to, amount);
+    }
+
+    function transferFrom(address from, address to, uint256 amount) public asCaller assumeHolder(to) returns (bool) {
+        return token.transferFrom(from, to, amount);
+    }
+
+    function mint(address to, uint256 amount) public asCaller assumeHolder(to) {
+        token.mint(to, amount);
+    }
+
+    function burn(address from, uint256 amount) public asCaller {
+        token.burn(from, amount);
+    }
+
+    function approve(address spender, uint256 amount) public asCaller returns (bool) {
+        return token.approve(spender, amount);
+    }
+
+    /*
+     * helpers
+     */
+
+    modifier asCaller() {
+        vm.startPrank(msg.sender);
+        _;
+        vm.stopPrank();
+    }
+
+    modifier assumeHolder(address account) {
+        vm.assume(_contains(holders, account));
+        _;
+    }
+
+    function _contains(address[] storage array, address value) internal view returns (bool) {
+        for (uint256 i = 0; i < array.length; i++) {
+            if (array[i] == value) {
+                return true;
+            }
+        }
+        return false;
+    }
+
+    // invariant: the sum of balances must equal the total supply
+    function invariant_sumOfBalancesEqualsTotalSupply() public view {
+        uint256 sumOfBalances = 0;
+        for (uint256 i = 0; i < holders.length; i++) {
+            sumOfBalances += token.balanceOf(holders[i]);
+        }
+        assertEq(sumOfBalances, token.totalSupply());
+    }
+}

examples/simple/src/Vat.sol examples/invariants/src/Vat.solexamples/simple/src/Vat.sol renamed to examples/invariants/src/Vat.sol

@@ -0,0 +1,35 @@
+// SPDX-License-Identifier: AGPL-3.0
+pragma solidity >=0.8.0 <0.9.0;
+
+import {ERC721} from "../src/ERC721.sol";
+import {Test} from "forge-std/Test.sol";
+
+/// @custom:halmos --solver bitwuzla-abs --solver-timeout-assertion 0
+contract ERC721Test is Test {
+    // ERC721 token address
+    ERC721 internal token;
+
+    function setUp() public virtual {
+        // deploy ERC721 token
+        token = new ERC721("ERC721", "ERC721");
+
+        // mint initial tokens
+        token.mint(address(0x1001), 1);
+        token.mint(address(0x1001), 2);
+        token.mint(address(0x1002), 3);
+        token.mint(address(0x1003), 4);
+
+        // register the token contract as the target for invariant testing
+        targetContract(address(token));
+    }
+
+    // invariant: the owner of any token ID must have at least one token
+    function invariant_ownerHasAtLeastOneToken() public {
+        uint256 tokenId = vm.randomUint();
+        try token.ownerOf(tokenId) returns (address owner) {
+            assertGe(token.balanceOf(owner), 1);
+        } catch {
+            // nothing to do if the token does not exist
+        }
+    }
+}