WETH invariant examples

foundry.toml

@@ -3,4 +3,11 @@ src = 'src'
 out = 'out'
 libs = ['lib']
 
-# See more config options https://github.com/foundry-rs/foundry/tree/master/config
+[invariant]
+runs = 10000
+depth = 15
+fail_on_revert = false 
+call_override = false
+dictionary_weight = 80
+include_storage = true
+include_push_bytes = true

src/WETH9.sol

@@ -0,0 +1,76 @@
+// Copyright (C) 2015, 2016, 2017 Dapphub
+
+// This program is free software: you can redistribute it and/or modify
+// it under the terms of the GNU General Public License as published by
+// the Free Software Foundation, either version 3 of the License, or
+// (at your option) any later version.
+
+// This program is distributed in the hope that it will be useful,
+// but WITHOUT ANY WARRANTY; without even the implied warranty of
+// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+// GNU General Public License for more details.
+
+// You should have received a copy of the GNU General Public License
+// along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+pragma solidity ^0.8.13;
+
+contract WETH9 {
+    string public name = "Wrapped Ether";
+    string public symbol = "WETH";
+    uint8 public decimals = 18;
+
+    event Approval(address indexed src, address indexed guy, uint256 wad);
+    event Transfer(address indexed src, address indexed dst, uint256 wad);
+    event Deposit(address indexed dst, uint256 wad);
+    event Withdrawal(address indexed src, uint256 wad);
+
+    mapping(address => uint256) public balanceOf;
+    mapping(address => mapping(address => uint256)) public allowance;
+
+    fallback() external payable {
+        deposit();
+    }
+
+    function deposit() public payable {
+        balanceOf[msg.sender] += msg.value;
+        emit Deposit(msg.sender, msg.value);
+    }
+
+    function withdraw(uint256 wad) public {
+        require(balanceOf[msg.sender] >= wad);
+        balanceOf[msg.sender] -= wad;
+        payable(msg.sender).transfer(wad);
+        emit Withdrawal(msg.sender, wad);
+    }
+
+    function totalSupply() public view returns (uint256) {
+        return address(this).balance;
+    }
+
+    function approve(address guy, uint256 wad) public returns (bool) {
+        allowance[msg.sender][guy] = wad;
+        emit Approval(msg.sender, guy, wad);
+        return true;
+    }
+
+    function transfer(address dst, uint256 wad) public returns (bool) {
+        return transferFrom(msg.sender, dst, wad);
+    }
+
+    function transferFrom(address src, address dst, uint256 wad) public returns (bool) {
+        require(balanceOf[src] >= wad);
+
+        if (src != msg.sender && allowance[src][msg.sender] != type(uint256).max) {
+            require(allowance[src][msg.sender] >= wad);
+            allowance[src][msg.sender] -= wad;
+        }
+
+        balanceOf[src] -= wad;
+        balanceOf[dst] += wad;
+
+        emit Transfer(src, dst, wad);
+
+        return true;
+    }
+}

test/WETH9.invariants.t.sol

@@ -0,0 +1,52 @@
+// SPDX-License-Identifier: UNLICENSED
+pragma solidity ^0.8.13;
+
+import {Test} from "forge-std/Test.sol";
+import {InvariantTest} from "forge-std/InvariantTest.sol";
+import "forge-std/console.sol";
+
+import {Depositor} from "./actors/Depositor.sol";
+import {WETH9} from "../src/WETH9.sol";
+
+contract WETH9Invariants is Test, InvariantTest {
+    WETH9 public weth;
+
+    Depositor public depositor;
+
+    function setUp() public {
+        weth = new WETH9();
+        depositor = new Depositor(weth);
+
+        bytes4[] memory selectors = new bytes4[](4);
+        selectors[0] = Depositor.deposit.selector;
+        selectors[1] = Depositor.withdraw.selector;
+        selectors[2] = Depositor.sendETH.selector;
+        selectors[3] = Depositor.forceSend.selector;
+
+        targetSelector(FuzzSelector({addr: address(depositor), selectors: selectors}));
+        excludeContract(address(weth));
+    }
+
+    // ETH can only be wrapped into WETH, WETH can only be
+    // unwrapped back into ETH. The sum of Depositor's
+    // ETH balance plus their WETH balance should always
+    // equal the total ETH_SUPPLY.
+    function invariant_preservationOfETH() public {
+        assertEq(depositor.ETH_SUPPLY(), address(depositor).balance + weth.totalSupply());
+    }
+
+    // WETH balance should always be at least as much as
+    // the sum of individual deposits.
+    function invariant_WETHSolvency() public {
+        assertEq(weth.totalSupply(), depositor.ghost_depositSum() + depositor.ghost_forceSendSum() - depositor.ghost_withdrawSum());
+    }
+
+    // No individual depositor balance can exceed the
+    // wETH totalSupply()
+    function invariant_depositorBalances() public {
+        address[] memory depositors = depositor.depositors();
+        for (uint256 i; i < depositors.length; ++i) {
+            assertLe(weth.balanceOf(depositors[i]), weth.totalSupply());
+        }
+    }
+}

test/actors/Depositor.sol

@@ -0,0 +1,62 @@
+// SPDX-License-Identifier: UNLICENSED
+pragma solidity ^0.8.13;
+
+import {Test} from "forge-std/Test.sol";
+import {WETH9} from "../../src/WETH9.sol";
+
+contract ForceSend {
+    function forceSend(address payable dst) external payable {
+        selfdestruct(dst);
+    }
+}
+
+contract Depositor is Test {
+    WETH9 public weth;
+
+    uint256 public ETH_SUPPLY = 120_000_000 ether;
+
+    uint256 public ghost_depositSum;
+    uint256 public ghost_withdrawSum;
+    uint256 public ghost_forceSendSum;
+
+    address[] internal _depositors;
+
+    constructor(WETH9 _weth) {
+        weth = _weth;
+        deal(address(this), ETH_SUPPLY);
+    }
+
+    function deposit(uint256 amount) public {
+        try weth.deposit{value: amount}() {
+            ghost_depositSum += amount;
+            _depositors.push(msg.sender);
+        } catch {}
+    }
+
+    function sendETH(uint256 amount) public {
+        (bool success,) = payable(address(weth)).call{value: amount}("");
+        if (success) {
+            ghost_depositSum += amount;
+            _depositors.push(msg.sender);
+        }
+    }
+
+    function withdraw(uint256 amount) public {
+        try weth.withdraw(amount) {
+            ghost_withdrawSum += amount;
+        } catch {}
+    }
+
+    function forceSend(uint256 amount) public {
+        ForceSend sender = new ForceSend();
+        try sender.forceSend{value: amount}(payable(address(weth))) {
+            ghost_forceSendSum += amount;
+        } catch {}
+    }
+
+    function depositors() public view returns (address[] memory) {
+        return _depositors;
+    }
+
+    receive() external payable {}
+}