refactor accrueInterest

certora/specs/AccrueInterest.spec

@@ -108,7 +108,9 @@ rule repayAccruesInterest(env e, MorphoHarness.MarketParams marketParams, uint25
 // We also exclude setFeeRecipient, as it is known to be not commutative.
 rule accrueInterestCommutesExceptForSetFeeRecipient(method f, calldataarg args)
 filtered {
-    f -> !f.isView && f.selector != sig:setFeeRecipient(address).selector
+    f -> !f.isView 
+    && f.selector != sig:setFeeRecipient(address).selector 
+    && f.selector != sig:liquidate(MorphoHarness.MarketParams, address, uint256, uint256, bytes).selector
 }
 {
     env e1;

src/Morpho.sol

@@ -159,8 +159,7 @@ contract Morpho is IMorphoStaticTyping {
 
         emit EventsLib.CreateMarket(id, marketParams);
 
-        // Call to initialize the IRM in case it is stateful.
-        if (marketParams.irm != address(0)) IIrm(marketParams.irm).borrowRate(marketParams, market[id]);
+        _accrueInterest(marketParams, id);
     }
 
     /* SUPPLY MANAGEMENT */
@@ -482,16 +481,19 @@ contract Morpho is IMorphoStaticTyping {
     /// @dev Accrues interest for the given market `marketParams`.
     /// @dev Assumes that the inputs `marketParams` and `id` match.
     function _accrueInterest(MarketParams memory marketParams, Id id) internal {
+        // The IRM is called even when elapsed=0. It can be useful for stateful IRMs.
+        uint256 borrowRate;
+        if (marketParams.irm != address(0)) borrowRate = IIrm(marketParams.irm).borrowRate(marketParams, market[id]);
+
         uint256 elapsed = block.timestamp - market[id].lastUpdate;
-        if (elapsed == 0) return;
 
-        if (marketParams.irm != address(0)) {
-            uint256 borrowRate = IIrm(marketParams.irm).borrowRate(marketParams, market[id]);
-            uint256 interest = market[id].totalBorrowAssets.wMulDown(borrowRate.wTaylorCompounded(elapsed));
+        uint256 interest;
+        uint256 feeShares;
+        if (elapsed != 0) {
+            interest = market[id].totalBorrowAssets.wMulDown(borrowRate.wTaylorCompounded(elapsed));
             market[id].totalBorrowAssets += interest.toUint128();
             market[id].totalSupplyAssets += interest.toUint128();
 
-            uint256 feeShares;
             if (market[id].fee != 0) {
                 uint256 feeAmount = interest.wMulDown(market[id].fee);
                 // The fee amount is subtracted from the total supply in this calculation to compensate for the fact
@@ -501,12 +503,12 @@ contract Morpho is IMorphoStaticTyping {
                 position[id][feeRecipient].supplyShares += feeShares;
                 market[id].totalSupplyShares += feeShares.toUint128();
             }
-
-            emit EventsLib.AccrueInterest(id, borrowRate, interest, feeShares);
         }
 
         // Safe "unchecked" cast.
         market[id].lastUpdate = uint128(block.timestamp);
+
+        emit EventsLib.AccrueInterest(id, borrowRate, interest, feeShares);
     }
 
     /* HEALTH CHECK */