[Certora] Liquidity

.gitignore

@@ -18,6 +18,7 @@ docs/
 
 # Certora
 .certora**
+emv-*-certora*
 
 # Hardhat
 /types

certora/harness/MorphoHarness.sol

@@ -20,4 +20,12 @@ contract MorphoHarness is Morpho {
     function getMarketId(Market memory market) external pure returns (Id) {
         return market.id();
     }
+
+    function mathLibMulDivUp(uint256 x, uint256 y, uint256 d) public pure returns (uint256) {
+        return MathLib.mulDivUp(x, y, d);
+    }
+
+    function mathLibMulDivDown(uint256 x, uint256 y, uint256 d) public pure returns (uint256) {
+        return MathLib.mulDivDown(x, y, d);
+    }
 }

certora/scripts/verifyBlueRatioMath.sh

@@ -0,0 +1,9 @@
+#!/bin/sh
+
+certoraRun \
+    certora/harness/MorphoHarness.sol \
+    --verify MorphoHarness:certora/specs/BlueRatioMath.spec \
+    --solc_allow_path src \
+    --msg "Morpho Ratio Math" \
+    --send_only \
+    "$@"

certora/scripts/verifyBlueRatioMathSummary.sh

@@ -0,0 +1,7 @@
+#!/bin/sh
+
+certoraRun \
+    certora/harness/MorphoHarness.sol \
+    --verify MorphoHarness:certora/specs/BlueRatioMathSummary.spec \
+    --msg "Morpho Ratio Math Summary" \
+    "$@"

certora/specs/Blue.spec

@@ -6,17 +6,22 @@ methods {
     function totalBorrow(MorphoHarness.Id) external returns uint256 envfree;
     function totalSupplyShares(MorphoHarness.Id) external returns uint256 envfree;
     function totalBorrowShares(MorphoHarness.Id) external returns uint256 envfree;
+    function fee(MorphoHarness.Id) external returns uint256 envfree;
+    function getMarketId(MorphoHarness.Market) external returns MorphoHarness.Id envfree;
+    function idToMarket(MorphoHarness.Id) external returns (address, address, address, address, uint256) envfree;
+    function isAuthorized(address, address) external returns bool envfree;
 
     function lastUpdate(MorphoHarness.Id) external returns uint256 envfree;
     function isLltvEnabled(uint256) external returns bool envfree;
     function isIrmEnabled(address) external returns bool envfree;
 
-    function _.borrowRate(MorphoHarness.Market) external => DISPATCHER(true);
+    function _.borrowRate(MorphoHarness.Market) external => HAVOC_ECF;
 
     function getMarketId(MorphoHarness.Market) external returns MorphoHarness.Id envfree;
-    // function _.safeTransfer(address, uint256) internal => DISPATCHER(true);
-    // function _.safeTransferFrom(address, address, uint256) internal => DISPATCHER(true);
 
+    // Temporary workaround a bug that requires to have address instead of an interface in the signature
+    function SafeTransferLib.tmpSafeTransfer(address token, address to, uint256 value) internal => summarySafeTransferFrom(token, currentContract, to, value);
+    function SafeTransferLib.tmpSafeTransferFrom(address token, address from, address to, uint256 value) internal => summarySafeTransferFrom(token, from, to, value);
 }
 
 ghost mapping(MorphoHarness.Id => mathint) sumSupplyShares
@@ -31,6 +36,24 @@ ghost mapping(MorphoHarness.Id => mathint) sumCollateral
 {
     init_state axiom (forall MorphoHarness.Id id. sumCollateral[id] == 0);
 }
+ghost mapping(address => mathint) myBalances
+{
+    init_state axiom (forall address token. myBalances[token] == 0);
+}
+ghost mapping(address => mathint) expectedAmount
+{
+    init_state axiom (forall address token. expectedAmount[token] == 0);
+}
+
+ghost mapping(MorphoHarness.Id => address) idToBorrowable;
+ghost mapping(MorphoHarness.Id => address) idToCollateral;
+
+hook Sstore idToMarket[KEY MorphoHarness.Id id].borrowableToken address token STORAGE {
+    idToBorrowable[id] = token;
+}
+hook Sstore idToMarket[KEY MorphoHarness.Id id].collateralToken address token STORAGE {
+    idToCollateral[id] = token;
+}
 
 hook Sstore supplyShares[KEY MorphoHarness.Id id][KEY address owner] uint256 newShares (uint256 oldShares) STORAGE {
     sumSupplyShares[id] = sumSupplyShares[id] - oldShares + newShares;
@@ -42,10 +65,35 @@ hook Sstore borrowShares[KEY MorphoHarness.Id id][KEY address owner] uint256 new
 
 hook Sstore collateral[KEY MorphoHarness.Id id][KEY address owner] uint256 newAmount (uint256 oldAmount) STORAGE {
     sumCollateral[id] = sumCollateral[id] - oldAmount + newAmount;
+    expectedAmount[idToCollateral[id]] = expectedAmount[idToCollateral[id]] - oldAmount + newAmount;
+}
+
+hook Sstore totalSupply[KEY MorphoHarness.Id id] uint256 newAmount (uint256 oldAmount) STORAGE {
+    expectedAmount[idToBorrowable[id]] = expectedAmount[idToBorrowable[id]] - oldAmount + newAmount;
+}
+
+hook Sstore totalBorrow[KEY MorphoHarness.Id id] uint256 newAmount (uint256 oldAmount) STORAGE {
+    expectedAmount[idToBorrowable[id]] = expectedAmount[idToBorrowable[id]] + oldAmount - newAmount;
+}
+
+function summarySafeTransferFrom(address token, address from, address to, uint256 amount) {
+    if (from == currentContract) {
+        myBalances[token] = require_uint256(myBalances[token] - amount);
+    }
+    if (to == currentContract) {
+        myBalances[token] = require_uint256(myBalances[token] + amount);
+    }
 }
 
 definition VIRTUAL_ASSETS() returns mathint = 1;
-definition VIRTUAL_SHARES() returns mathint = 1000000000000000000;
+definition VIRTUAL_SHARES() returns mathint = 10^18;
+definition MAX_FEE() returns mathint = 10^18 * 25/100;
+definition isInitialized(MorphoHarness.Id id) returns bool =
+    (lastUpdate(id) != 0);
+
+
+invariant feeInRange(MorphoHarness.Id id)
+    to_mathint(fee(id)) <= MAX_FEE();
 
 invariant sumSupplySharesCorrect(MorphoHarness.Id id)
     to_mathint(totalSupplyShares(id)) == sumSupplyShares[id];
@@ -55,6 +103,44 @@ invariant sumBorrowSharesCorrect(MorphoHarness.Id id)
 invariant borrowLessSupply(MorphoHarness.Id id)
     totalBorrow(id) <= totalSupply(id);
 
+invariant marketInvariant(MorphoHarness.Market market)
+    isInitialized(getMarketId(market)) =>
+    idToBorrowable[getMarketId(market)] == market.borrowableToken
+    && idToCollateral[getMarketId(market)] == market.collateralToken;
+
+invariant isLiquid(address token)
+    expectedAmount[token] <= myBalances[token]
+{
+    preserved supply(MorphoHarness.Market market, uint256 _a, uint256 _s, address _o, bytes _d) with (env e) {
+        requireInvariant marketInvariant(market);
+        require e.msg.sender != currentContract;
+    }
+    preserved withdraw(MorphoHarness.Market market, uint256 _a, uint256 _s, address _o, address _r) with (env e) {
+        requireInvariant marketInvariant(market);
+        require e.msg.sender != currentContract;
+    }
+    preserved borrow(MorphoHarness.Market market, uint256 _a, uint256 _s, address _o, address _r) with (env e) {
+        requireInvariant marketInvariant(market);
+        require e.msg.sender != currentContract;
+    }
+    preserved repay(MorphoHarness.Market market, uint256 _a, uint256 _s, address _o, bytes _d) with (env e) {
+        requireInvariant marketInvariant(market);
+        require e.msg.sender != currentContract;
+    }
+    preserved supplyCollateral(MorphoHarness.Market market, uint256 _a, address _o, bytes _d) with (env e) {
+        requireInvariant marketInvariant(market);
+        require e.msg.sender != currentContract;
+    }
+    preserved withdrawCollateral(MorphoHarness.Market market, uint256 _a, address _o, address _r) with (env e) {
+        requireInvariant marketInvariant(market);
+        require e.msg.sender != currentContract;
+    }
+    preserved liquidate(MorphoHarness.Market market, address _b, uint256 _s, bytes _d) with (env e) {
+        requireInvariant marketInvariant(market);
+        require e.msg.sender != currentContract;
+    }
+}
+
 rule supplyRevertZero(MorphoHarness.Market market) {
     env e;
     bytes b;
@@ -65,7 +151,20 @@ rule supplyRevertZero(MorphoHarness.Market market) {
 }
 
 invariant invOnlyEnabledLltv(MorphoHarness.Market market)
-    lastUpdate(getMarketId(market)) != 0 => isLltvEnabled(market.lltv);
+    isInitialized(getMarketId(market)) => isLltvEnabled(market.lltv);
 
 invariant invOnlyEnabledIrm(MorphoHarness.Market market)
-    lastUpdate(getMarketId(market)) != 0 => isIrmEnabled(market.irm);
+    isInitialized(getMarketId(market)) => isIrmEnabled(market.irm);
+
+rule marketIdUnique() {
+    MorphoHarness.Market market1;
+    MorphoHarness.Market market2;
+
+    require getMarketId(market1) == getMarketId(market2);
+
+    assert market1.borrowableToken == market2.borrowableToken;
+    assert market1.collateralToken == market2.collateralToken;
+    assert market1.oracle == market2.oracle;
+    assert market1.irm == market2.irm;
+    assert market1.lltv == market2.lltv;
+}

certora/specs/BlueRatioMath.spec

@@ -0,0 +1,58 @@
+methods {
+    function totalSupply(MorphoHarness.Id) external returns uint256 envfree;
+    function totalSupplyShares(MorphoHarness.Id) external returns uint256 envfree;
+    function fee(MorphoHarness.Id) external returns uint256 envfree;
+
+    function MathLib.mulDivDown(uint256 a, uint256 b, uint256 c) internal returns uint256 => summaryMulDivDown(a,b,c);
+    function MathLib.mulDivUp(uint256 a, uint256 b, uint256 c) internal returns uint256 => summaryMulDivUp(a,b,c);
+    function MathLib.wTaylorCompounded(uint256, uint256) internal returns uint256 => NONDET;
+
+    function _.borrowRate(MorphoHarness.Market) external => HAVOC_ECF;
+}
+
+definition VIRTUAL_ASSETS() returns mathint = 1;
+definition VIRTUAL_SHARES() returns mathint = 10^18;
+definition MAX_FEE() returns mathint = 10^18 * 25/100;
+
+invariant feeInRange(MorphoHarness.Id id)
+    to_mathint(fee(id)) <= MAX_FEE();
+
+/* This is a simple overapproximative summary, stating that it rounds in the right direction.
+ * The summary is checked by the specification in BlueRatioMathSummary.spec.
+ */
+function summaryMulDivUp(uint256 x, uint256 y, uint256 d) returns uint256 {
+    uint256 result;
+    require result * d >= x * y;
+    return result;
+}
+
+/* This is a simple overapproximative summary, stating that it rounds in the right direction.
+ * The summary is checked by the specification in BlueRatioMathSummary.spec.
+ */
+function summaryMulDivDown(uint256 x, uint256 y, uint256 d) returns uint256 {
+    uint256 result;
+    require result * d <= x * y;
+    return result;
+}
+
+rule onlyLiquidateCanDecreasesRatio(method f) 
+filtered {
+    f -> f.selector != sig:liquidate(MorphoHarness.Market, address, uint256, bytes).selector
+}
+{
+    MorphoHarness.Id id;
+    requireInvariant feeInRange(id);
+
+    mathint assetsBefore = totalSupply(id) + VIRTUAL_ASSETS();
+    mathint sharesBefore = totalSupplyShares(id) + VIRTUAL_SHARES();
+
+    env e;
+    calldataarg args;
+    f(e,args);
+
+    mathint assetsAfter = totalSupply(id) + VIRTUAL_ASSETS();
+    mathint sharesAfter = totalSupplyShares(id) + VIRTUAL_SHARES();
+
+    // check if ratio increases: assetsBefore/sharesBefore <= assetsAfter / sharesAfter;
+    assert assetsBefore * sharesAfter <= assetsAfter * sharesBefore;
+}

certora/specs/BlueRatioMathSummary.spec

@@ -0,0 +1,15 @@
+methods {
+    function mathLibMulDivUp(uint256, uint256, uint256) external returns uint256 envfree;
+    function mathLibMulDivDown(uint256, uint256, uint256) external returns uint256 envfree;
+}
+
+/* Check the summaries required by BlueRatioMath.spec */
+rule checkSummaryMulDivUp(uint256 x, uint256 y, uint256 d) {
+    uint256 result = mathLibMulDivUp(x, y, d);
+    assert result * d >= x * y;
+}
+
+rule checkSummaryMulDivDown(uint256 x, uint256 y, uint256 d) {
+    uint256 result = mathLibMulDivDown(x, y, d);
+    assert result * d <= x * y;
+}

src/libraries/SafeTransferLib.sol

@@ -11,20 +11,29 @@ import {IERC20} from "../interfaces/IERC20.sol";
 /// @notice Library to manage tokens not fully ERC20 compliant:
 ///         not returning a boolean for `transfer` and `transferFrom` functions.
 library SafeTransferLib {
-    function safeTransfer(IERC20 token, address to, uint256 value) internal {
-        (bool success, bytes memory returndata) = address(token).call(abi.encodeCall(token.transfer, (to, value)));
+    function tmpSafeTransfer(address token, address to, uint256 value) internal {
+        (bool success, bytes memory returndata) =
+            address(token).call(abi.encodeCall(IERC20(token).transfer, (to, value)));
         require(
             success && address(token).code.length > 0 && (returndata.length == 0 || abi.decode(returndata, (bool))),
             ErrorsLib.TRANSFER_FAILED
         );
     }
 
-    function safeTransferFrom(IERC20 token, address from, address to, uint256 value) internal {
+    function tmpSafeTransferFrom(address token, address from, address to, uint256 value) internal {
         (bool success, bytes memory returndata) =
-            address(token).call(abi.encodeCall(token.transferFrom, (from, to, value)));
+            address(token).call(abi.encodeCall(IERC20(token).transferFrom, (from, to, value)));
         require(
             success && address(token).code.length > 0 && (returndata.length == 0 || abi.decode(returndata, (bool))),
             ErrorsLib.TRANSFER_FROM_FAILED
         );
     }
+
+    function safeTransfer(IERC20 token, address to, uint256 value) internal {
+        tmpSafeTransfer(address(token), to, value);
+    }
+
+    function safeTransferFrom(IERC20 token, address from, address to, uint256 value) internal {
+        tmpSafeTransferFrom(address(token), from, to, value);
+    }
 }