[Certora] Liquidity

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/specs/Blue.spec

@@ -6,17 +6,24 @@ 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);
 
+    function mathLibMulDivUp(uint256, uint256, uint256) external returns uint256 envfree;
+    function mathLibMulDivDown(uint256, uint256, uint256) external returns uint256 envfree;
+
+    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 +38,17 @@ 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 idToBorrowable(MorphoHarness.Id) returns address;
+ghost idToCollateral(MorphoHarness.Id) returns address;
 
 hook Sstore supplyShares[KEY MorphoHarness.Id id][KEY address owner] uint256 newShares (uint256 oldShares) STORAGE {
     sumSupplyShares[id] = sumSupplyShares[id] - oldShares + newShares;
@@ -42,10 +60,36 @@ 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 goodMarket(MorphoHarness.Market market, MorphoHarness.Id id) returns bool =
+    (idToBorrowable(id) == market.borrowableToken &&
+     idToCollateral(id) == market.collateralToken);
+
 definition VIRTUAL_ASSETS() returns mathint = 1;
 definition VIRTUAL_SHARES() returns mathint = 1000000000000000000;
+definition MAX_FEE() returns mathint = 250000000000000000;
+
+invariant feeInRange(MorphoHarness.Id id)
+    to_mathint(fee(id)) <= MAX_FEE();
 
 invariant sumSupplySharesCorrect(MorphoHarness.Id id)
     to_mathint(totalSupplyShares(id)) == sumSupplyShares[id];
@@ -55,6 +99,41 @@ invariant sumBorrowSharesCorrect(MorphoHarness.Id id)
 invariant borrowLessSupply(MorphoHarness.Id id)
     totalBorrow(id) <= totalSupply(id);
 
+invariant isLiquid(address token)
+    expectedAmount[token] <= myBalances[token]
+{
+    preserved supply(MorphoHarness.Market market, uint256 _a, uint256 _s, address _o, bytes _d) with (env _e) {
+        require goodMarket(market, getMarketId(market));
+        require _e.msg.sender != currentContract;
+    }
+    preserved withdraw(MorphoHarness.Market market, uint256 _a, uint256 _s, address _o, address _r) with (env _e) {
+        require goodMarket(market, getMarketId(market));
+        require _e.msg.sender != currentContract;
+    }
+    preserved borrow(MorphoHarness.Market market, uint256 _a, uint256 _s, address _o, address _r) with (env _e) {
+        require goodMarket(market, getMarketId(market));
+        require _e.msg.sender != currentContract;
+    }
+    preserved repay(MorphoHarness.Market market, uint256 _a, uint256 _s, address _o, bytes _d) with (env _e) {
+        require goodMarket(market, getMarketId(market));
+        require _e.msg.sender != currentContract;
+    }
+    preserved supplyCollateral(MorphoHarness.Market market, uint256 _a, address _o, bytes _d) with (env _e) {
+        require goodMarket(market, getMarketId(market));
+        require _e.msg.sender != currentContract;
+    }
+    preserved withdrawCollateral(MorphoHarness.Market market, uint256 _a, address _o, address _r) with (env _e) {
+        require goodMarket(market, getMarketId(market));
+        require _e.msg.sender != currentContract;
+    }
+    preserved liquidate(MorphoHarness.Market market, address _b, uint256 _s, bytes _d) with (env _e) {
+        require goodMarket(market, getMarketId(market));
+        require _e.msg.sender != currentContract;
+    }
+}
+//invariant liquidOnCollateralToken(MorphoHarness.Market market)
+//    myBalances[market.collateralToken] <= collateral(getMarketId(market));
+
 rule supplyRevertZero(MorphoHarness.Market market) {
     env e;
     bytes b;
@@ -69,3 +148,14 @@ invariant invOnlyEnabledLltv(MorphoHarness.Market market)
 
 invariant invOnlyEnabledIrm(MorphoHarness.Market market)
     lastUpdate(getMarketId(market)) != 0 => isIrmEnabled(market.irm);
+
+/* Check the summaries required by BlueRatioMath.spec */
+rule checkSummaryToAssetsUp(uint256 x, uint256 y, uint256 d) {
+    uint256 result = mathLibMulDivUp(x, y, d);
+    assert result * d >= x * y;
+}
+
+rule checkSummaryToAssetsDown(uint256 x, uint256 y, uint256 d) {
+    uint256 result = mathLibMulDivDown(x, y, d);
+    assert result * d <= x * y;
+}

certora/specs/BlueRatioMath.spec

@@ -0,0 +1,62 @@
+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 MathLib.wMulDown(uint256, uint256) internal returns uint256 => NONDET;
+
+    //function SharesMathLib.toAssetsUp(uint256 shares, uint256 totalAssets, uint256 totalShares) internal returns uint256 => summaryToAssetsUp(shares, totalAssets, totalShares);
+    //function SharesMathLib.toAssetsDown(uint256 shares, uint256 totalAssets, uint256 totalShares) internal returns uint256 => summaryToAssetsDown(shares, totalAssets, totalShares);
+
+    function _.borrowRate(MorphoHarness.Market) external => HAVOC_ECF;
+}
+
+definition VIRTUAL_ASSETS() returns mathint = 1;
+definition VIRTUAL_SHARES() returns mathint = 1000000000000000000;
+definition MAX_FEE() returns mathint = 250000000000000000;
+
+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 Blue.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 Blue.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;
+}

src/libraries/SafeTransferLib.sol

@@ -11,20 +11,28 @@ 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);
+    }
 }