Add OETHVault fuzzing suite

contracts/contracts/fuzz/oethvault/Dummy.sol

@@ -0,0 +1,9 @@
+// SPDX-License-Identifier: MIT
+
+/**
+ * @title Dummy contract to simulate smart contract actors.
+ * @author Rappie <rappie@perimetersec.io>
+ * @dev This contract gets deployed by Echidna. See `echidna-config.yaml`
+ * for more details.
+ */
+contract Dummy {}

contracts/contracts/fuzz/oethvault/Fuzz.sol

@@ -0,0 +1,19 @@
+// SPDX-License-Identifier: MIT
+import {FuzzSetup} from "./FuzzSetup.sol";
+import {FuzzOETH} from "./FuzzOETH.sol";
+import {FuzzVault} from "./FuzzVault.sol";
+import {FuzzGlobal} from "./FuzzGlobal.sol";
+import {FuzzSelfTest} from "./FuzzSelfTest.sol";
+
+/**
+ * @title Top-level Fuzz contract to be deployed by Echidna.
+ * @author Rappie <rappie@perimetersec.io>
+ */
+contract Fuzz is
+    FuzzOETH, // Fuzz tests for OETH
+    FuzzVault, // Fuzz tests for Vault
+    FuzzGlobal, // Global invariants
+    FuzzSelfTest // Self-tests (for debugging)
+{
+    constructor() payable FuzzSetup() {}
+}

contracts/contracts/fuzz/oethvault/FuzzActor.sol

@@ -0,0 +1,46 @@
+// SPDX-License-Identifier: MIT
+import {FuzzConfig} from "./FuzzConfig.sol";
+
+/**
+ * @title Contract containing the actor setup.
+ * @author Rappie <rappie@perimetersec.io>
+ */
+contract FuzzActor is FuzzConfig {
+    // Actors are the addresses to be used as senders.
+    address internal constant ADDRESS_ACTOR1 = address(0x10000);
+    address internal constant ADDRESS_ACTOR2 = address(0x20000);
+    address internal constant ADDRESS_ACTOR3 = address(0x30000);
+    address internal constant ADDRESS_ACTOR4 = address(0x40000);
+
+    // Outsiders are addresses meant to contain funds but not take actions.
+    address internal constant ADDRESS_OUTSIDER_REBASING = address(0x50000);
+    address internal constant ADDRESS_OUTSIDER_NONREBASING = address(0x60000);
+
+    // List of all actors
+    address[] internal ACTORS = [
+        ADDRESS_ACTOR1,
+        ADDRESS_ACTOR2,
+        ADDRESS_ACTOR3,
+        ADDRESS_ACTOR4
+    ];
+
+    // Variable containing current actor.
+    address internal currentActor;
+
+    // Debug toggle to disable setting the current actor.
+    bool internal constant DEBUG_TOGGLE_SET_ACTOR = true;
+
+    /// @notice Modifier storing `msg.sender` for the duration of the function call.
+    modifier setCurrentActor() {
+        address previousActor = currentActor;
+        if (DEBUG_TOGGLE_SET_ACTOR) {
+            currentActor = msg.sender;
+        }
+
+        _;
+
+        if (DEBUG_TOGGLE_SET_ACTOR) {
+            currentActor = previousActor;
+        }
+    }
+}

contracts/contracts/fuzz/oethvault/FuzzConfig.sol

@@ -0,0 +1,64 @@
+// SPDX-License-Identifier: MIT
+
+/**
+ * @title Contract containing configuration variables for the fuzzing suite.
+ * @author Rappie <rappie@perimetersec.io>
+ */
+contract FuzzConfig {
+    // Starting balance for actors that will interact with the system.
+    uint256 internal constant STARTING_BALANCE = 1_000_000_000_000e18;
+
+    // Starting balance for outsides that will not interact with the system.
+    //
+    // We need these to have initial balances to prevent problems caused by
+    // rounding errors.
+    // We want this amount to be considerably lower than the starting balance
+    // of the actors, to be able to reach lower Credits Per Token (CPT) values.
+    //
+    uint256 internal constant STARTING_BALANCE_OUTSIDER = 1_000_000_000e18;
+
+    // Tolerance for rounding errors when mining or redeeming OETH.
+    uint256 internal constant MINT_TOLERANCE = 1;
+    uint256 internal constant REDEEM_TOLERANCE = 1;
+
+    // Tolerance for rounding errors in balance changes after rebasing.
+    uint256 internal constant BALANCE_AFTER_REBASE_TOLERANCE = 1;
+
+    // Tolerance for rounding errors in amount of yield generated by donating
+    // and rebasing.
+    uint256 internal constant YIELD_TOLERANCE = 10_000;
+
+    // Tolerance for the amount of WETH that should be available in the vault
+    // as a buffer for all actors (including outsiders) to be able to redeem
+    // all their OETH.
+    uint256 internal constant REDEEM_ALL_TOLERANCE = 1 ether / 100;
+
+    // Tolerance for the difference between the total generated yield and the
+    // total donated amount.
+    //
+    // Max difference found with quick optimization: 11_359_396
+    //
+    uint256 internal constant DONATE_VS_YIELD_TOLERANCE = 2e7;
+
+    // Tolerance for the difference between the vault balance and the total
+    // OETH in the system.
+    //
+    // This is strongly related to the donate vs yield tolerance, so it makes
+    // sense to have the same value.
+    //
+    // Max difference found with quick optimization: 11_923_059
+    //
+    uint256 internal constant VAULT_BALANCE_VS_TOTAL_OETH_TOLERANCE = 2e7;
+
+    // Tolerance used to the major "accounting" global invariant.
+    //
+    // See `globalAccounting` for more info.
+    //
+    uint256 internal constant ACCOUNTING_TOLERANCE = 10;
+
+    // Total amount of WETH donated to the vault.
+    uint256 totalDonated;
+
+    // Total amount of OETH yield generated from donations to the vault.
+    uint256 totalYield;
+}

contracts/contracts/fuzz/oethvault/FuzzGlobal.sol

@@ -0,0 +1,121 @@
+// SPDX-License-Identifier: MIT
+import {FuzzHelper} from "./FuzzHelper.sol";
+
+/**
+ * @title Contract containing fuzz tests for global invariants
+ * @author Rappie <rappie@perimetersec.io>
+ */
+contract FuzzGlobal is FuzzHelper {
+    /**
+     * @notice Run all global invariants fuzz tests
+     * @dev We use one single function to run all global invariants fuzz tests.
+     * This is done to minize the search space for the fuzzer
+     */
+    function globalInvariants() public {
+        totalWethVsStartingBalance();
+        totalOethVsStartingBalance();
+        totalYieldVsDonated();
+        globalAccounting();
+        globalOethVsWethTotalSupply();
+        globalVaultBalanceVsOethTotalBalance();
+    }
+
+    /**
+     * @notice Test total WETH vs starting balance
+     */
+    function totalWethVsStartingBalance() internal {
+        uint256 totalStarting = getTotalWethStartingBalance();
+        uint256 totalWeth = getTotalWethBalance();
+
+        if (totalWeth > totalStarting) {
+            uint diff = diff(totalStarting, totalWeth);
+
+            lte(
+                diff,
+                YIELD_TOLERANCE,
+                "GLOBAL-01: The sum of WETH held by all actors never exceeds the sum of their WETH starting balances"
+            );
+        }
+    }
+
+    /**
+     * @notice Test total OETH vs starting balance
+     */
+    function totalOethVsStartingBalance() internal {
+        uint256 totalStarting = getTotalWethStartingBalance();
+        uint256 totalOeth = getTotalOethBalance();
+
+        lte(
+            totalOeth,
+            totalStarting,
+            "GLOBAL-02: The sum of OETH held by all actors never exceeds the sum of their WETH starting balances"
+        );
+    }
+
+    /**
+     * @notice Test total yield vs donated
+     */
+    function totalYieldVsDonated() internal {
+        uint256 diff = diff(totalYield, totalDonated);
+
+        lte(
+            diff,
+            DONATE_VS_YIELD_TOLERANCE,
+            "GLOBAL-03: The total amount of generated yield equals the total amount of WETH donated to the Vault"
+        );
+    }
+
+    /**
+     * @notice Test global accounting
+     */
+    function globalAccounting() internal {
+        uint256 totalStarting = getTotalWethStartingBalanceInclOutsiders();
+        uint256 totalWeth = getTotalWethBalanceInclOutsiders();
+        uint256 totalOeth = getTotalOethBalanceInclOutsiders();
+
+        // Invariant:
+        //    totalStarting - totalDonated = totalWeth + totalOeth - totalYield
+        int256 left = int256(totalStarting) - int256(totalDonated);
+        int256 right = int256(totalWeth) +
+            int256(totalOeth) -
+            int256(totalYield);
+
+        uint256 diff = diff(left, right);
+
+        lte(
+            diff,
+            ACCOUNTING_TOLERANCE,
+            "GLOBAL-04: The sum of all starting balances minus the total amount of WETH donated equals the sum of all WETH and OETH balances minus the total amount of yield generated"
+        );
+    }
+
+    /**
+     * @notice Test OETH total supply vs WETH total supply
+     */
+    function globalOethVsWethTotalSupply() internal {
+        uint256 wethTotalSupply = weth.totalSupply();
+        uint256 oethTotalSupply = oeth.totalSupply();
+
+        lte(
+            oethTotalSupply,
+            wethTotalSupply,
+            "GLOBAL-05: The total supply of OETH never exceeds the total supply of WETH"
+        );
+    }
+
+    /**
+     * @notice Test vault balance vs total OETH balance
+     */
+    function globalVaultBalanceVsOethTotalBalance() internal {
+        uint256 vaultBalance = weth.balanceOf(address(vault));
+        uint256 oethTotalBalance = getTotalOethBalanceInclOutsiders();
+
+        uint256 diff = diff(vaultBalance, oethTotalBalance);
+
+        lte(
+            diff,
+            VAULT_BALANCE_VS_TOTAL_OETH_TOLERANCE,
+            "GLOBAL-06: The Vault WETH balance never exceeds the total amount of OETH held by all actors and outsiders"
+        );
+    }
+}

contracts/contracts/fuzz/oethvault/FuzzHelper.sol

@@ -0,0 +1,75 @@
+// SPDX-License-Identifier: MIT
+import {FuzzSetup} from "./FuzzSetup.sol";
+
+/**
+ * @title Contract containing internal helper functions.
+ * @author Rappie <rappie@perimetersec.io>
+ */
+contract FuzzHelper is FuzzSetup {
+    /**
+     * @notice Get the total starting balance of OETH for all actors
+     * @return total Total starting balance of OETH
+     */
+    function getTotalWethStartingBalance() internal returns (uint256 total) {
+        total += STARTING_BALANCE * ACTORS.length;
+    }
+
+    /**
+     * @notice Get the total starting balance of OETH for all actors including outsiders
+     * @return total Total starting balance of OETH including outsiders
+     */
+    function getTotalWethStartingBalanceInclOutsiders()
+        internal
+        returns (uint256 total)
+    {
+        total += getTotalWethStartingBalance();
+        total += STARTING_BALANCE_OUTSIDER; // rebasing outsider
+        total += STARTING_BALANCE_OUTSIDER; // non-rebasing outsider
+    }
+
+    /**
+     * @notice Get the total OETH balance of all actors
+     * @return total Total OETH balance of all actors
+     */
+    function getTotalOethBalance() internal returns (uint256 total) {
+        for (uint256 i = 0; i < ACTORS.length; i++) {
+            total += oeth.balanceOf(ACTORS[i]);
+        }
+    }
+
+    /**
+     * @notice Get the total OETH balance of all actors including outsiders
+     * @return total Total OETH balance of all actors including outsiders
+     */
+    function getTotalOethBalanceInclOutsiders()
+        internal
+        returns (uint256 total)
+    {
+        total += getTotalOethBalance();
+        total += oeth.balanceOf(ADDRESS_OUTSIDER_NONREBASING);
+        total += oeth.balanceOf(ADDRESS_OUTSIDER_REBASING);
+    }
+
+    /**
+     * @notice Get the total WETH balance of all actors
+     * @return total Total WETH balance of all actors
+     */
+    function getTotalWethBalance() internal returns (uint256 total) {
+        for (uint256 i = 0; i < ACTORS.length; i++) {
+            total += weth.balanceOf(ACTORS[i]);
+        }
+    }
+
+    /**
+     * @notice Get the total WETH balance of all actors including outsiders
+     * @return total Total WETH balance of all actors including outsiders
+     */
+    function getTotalWethBalanceInclOutsiders()
+        internal
+        returns (uint256 total)
+    {
+        total += getTotalWethBalance();
+        total += weth.balanceOf(ADDRESS_OUTSIDER_NONREBASING);
+        total += weth.balanceOf(ADDRESS_OUTSIDER_REBASING);
+    }
+}