Merge pull request #620 from morpho-org/certora/suggestions-from-review

[Certora] Fix suggestions

Author: QGarchery

certora/specs/ExitLiquidity.spec

@@ -16,7 +16,7 @@ methods {
     function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;
 }
 
-// Check that it's not possible to withdraw more assets than what the user has supplied.
+// Check that it's not possible to withdraw more assets than what the user owns.
 rule withdrawLiquidity(MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) {
     env e;
     MorphoHarness.Id id = libId(marketParams);
@@ -27,27 +27,27 @@ rule withdrawLiquidity(MorphoHarness.MarketParams marketParams, uint256 assets,
     uint256 initialShares = supplyShares(id, onBehalf);
     uint256 initialTotalSupply = virtualTotalSupplyAssets(id);
     uint256 initialTotalSupplyShares = virtualTotalSupplyShares(id);
-    uint256 owedAssets = libMulDivDown(initialShares, initialTotalSupply, initialTotalSupplyShares);
+    uint256 ownedAssets = libMulDivDown(initialShares, initialTotalSupply, initialTotalSupplyShares);
 
     uint256 withdrawnAssets;
     withdrawnAssets, _ = withdraw(e, marketParams, assets, shares, onBehalf, receiver);
 
-    assert withdrawnAssets <= owedAssets;
+    assert withdrawnAssets <= ownedAssets;
 }
 
-// Check that it's not possible to withdraw more collateral than what the user has supplied.
-rule withdrawCollateralLiquidity(MorphoHarness.MarketParams marketParams, uint256 assets, address onBehalf, address receiver) {
+// Check that it's not possible to withdraw more collateral than what the user owns.
+rule withdrawCollateralLiquidity(MorphoHarness.MarketParams marketParams, uint256 withdrawnAssets, address onBehalf, address receiver) {
     env e;
     MorphoHarness.Id id = libId(marketParams);
 
-    uint256 initialCollateral = collateral(id, onBehalf);
+    uint256 ownedAssets = collateral(id, onBehalf);
 
-    withdrawCollateral(e, marketParams, assets, onBehalf, receiver);
+    withdrawCollateral(e, marketParams, withdrawnAssets, onBehalf, receiver);
 
-    assert assets <= initialCollateral;
+    assert withdrawnAssets <= ownedAssets;
 }
 
-// Check than when repaying the full outstanding debt requires more assets than what was borrowed.
+// Check than when repaying the full outstanding debt requires more assets than what the user owes.
 rule repayLiquidity(MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) {
     env e;
     MorphoHarness.Id id = libId(marketParams);
@@ -58,13 +58,13 @@ rule repayLiquidity(MorphoHarness.MarketParams marketParams, uint256 assets, uin
     uint256 initialShares = borrowShares(id, onBehalf);
     uint256 initialTotalBorrow = virtualTotalBorrowAssets(id);
     uint256 initialTotalBorrowShares = virtualTotalBorrowShares(id);
-    uint256 assetsDue = libMulDivUp(initialShares, initialTotalBorrow, initialTotalBorrowShares);
+    uint256 owedAssets = libMulDivUp(initialShares, initialTotalBorrow, initialTotalBorrowShares);
 
     uint256 repaidAssets;
     repaidAssets, _ = repay(e, marketParams, assets, shares, onBehalf, data);
 
     // Assume a full repay.
     require borrowShares(id, onBehalf) == 0;
 
-    assert repaidAssets >= assetsDue;
+    assert repaidAssets >= owedAssets;
 }

certora/specs/Health.spec

@@ -30,13 +30,13 @@ function mockPrice() returns uint256 {
 }
 
 function summaryMulDivUp(uint256 x, uint256 y, uint256 d) returns uint256 {
-    // Safe requires because the reference implementation would revert.
+    // Safe require because the reference implementation would revert.
     require d != 0;
     return require_uint256((x * y + (d - 1)) / d);
 }
 
 function summaryMulDivDown(uint256 x, uint256 y, uint256 d) returns uint256 {
-    // Safe requires because the reference implementation would revert.
+    // Safe require because the reference implementation would revert.
     require d != 0;
     return require_uint256((x * y) / d);
 }
@@ -103,6 +103,6 @@ filtered { f -> !f.isView }
 }
 
 // Check that users without collateral also have no debt.
-// This invariant ensures that bad debt is always accounted.
+// This invariant ensures that bad debt realization cannot be bypassed.
 invariant alwaysCollateralized(MorphoHarness.Id id, address borrower)
     borrowShares(id, borrower) != 0 => collateral(id, borrower) != 0;

certora/specs/Liveness.spec

@@ -53,10 +53,8 @@ function summaryAccrueInterest(env e, MorphoInternalAccess.MarketParams marketPa
     require e.block.timestamp < 2^128;
     if (e.block.timestamp != lastUpdate(id) && totalBorrowAssets(id) != 0) {
         uint128 interest;
-        uint256 borrow = totalBorrowAssets(id);
         uint256 supply = totalSupplyAssets(id);
-        // Safe requires because the reference implementation would revert.
-        require interest + borrow < 2^256;
+        // Safe require because the reference implementation would revert.
         require interest + supply < 2^256;
         increaseInterest(e, id, interest);
     }

certora/specs/RatioMath.spec

@@ -75,7 +75,7 @@ rule accrueInterestIncreasesBorrowRatio(env e, MorphoHarness.MarketParams market
 }
 
 
-// Check that excepti for liquidate, every function increases the value of supply shares.
+// Check that except when not accruing interest and except for liquidate, every function increases the value of supply shares.
 rule onlyLiquidateCanDecreaseSupplyRatio(env e, method f, calldataarg args)
 filtered {
     f -> !f.isView && f.selector != sig:liquidate(MorphoHarness.MarketParams, address, uint256, uint256, bytes).selector

certora/specs/Reentrancy.spec

@@ -5,11 +5,14 @@ methods {
     function _.borrowRate(MorphoHarness.MarketParams marketParams, MorphoHarness.Market) external => summaryBorrowRate() expect uint256;
 }
 
+ghost bool delegateCall;
+ghost bool callIsBorrowRate;
+// True when storage has been accessed with either a SSTORE or a SLOAD.
 ghost bool hasAccessedStorage;
+// True when a CALL has been done after storage has been accessed.
 ghost bool hasCallAfterAccessingStorage;
+// True when storage has been accessed, after which an external call is made, followed by accessing storage again.
 ghost bool hasReentrancyUnsafeCall;
-ghost bool delegate_call;
-ghost bool callIsBorrowRate;
 
 function summaryBorrowRate() returns uint256 {
     uint256 result;
@@ -31,14 +34,13 @@ hook CALL(uint g, address addr, uint value, uint argsOffset, uint argsLength, ui
     if (callIsBorrowRate) {
         // The calls to borrow rate are trusted and don't count.
         callIsBorrowRate = false;
-        hasCallAfterAccessingStorage = hasCallAfterAccessingStorage;
     } else {
         hasCallAfterAccessingStorage = hasAccessedStorage;
     }
 }
 
 hook DELEGATECALL(uint g, address addr, uint argsOffset, uint argsLength, uint retOffset, uint retLength) uint rc {
-    delegate_call = true;
+    delegateCall = true;
 }
 
 // Check that no function is accessing storage, then making an external CALL other than to the IRM, and accessing storage again.
@@ -53,7 +55,7 @@ rule reentrancySafe(method f, env e, calldataarg data) {
 // Check that the contract is truly immutable.
 rule noDelegateCalls(method f, env e, calldataarg data) {
     // Set up the initial state.
-    require !delegate_call;
+    require !delegateCall;
     f(e,data);
-    assert !delegate_call;
+    assert !delegateCall;
 }

certora/specs/Reverts.spec

@@ -42,7 +42,7 @@ definition exactlyOneZero(uint256 assets, uint256 shares) returns bool =
     (assets == 0 && shares != 0) || (assets != 0 && shares == 0);
 
 // This invariant catches bugs when not checking that the market is created with lastUpdate.
-invariant notInitializedEmpty(MorphoHarness.Id id)
+invariant notCreatedIsEmpty(MorphoHarness.Id id)
     !isCreated(id) => emptyMarket(id)
 {
     preserved with (env e) {
@@ -108,9 +108,9 @@ rule createMarketRevertCondition(env e, MorphoHarness.MarketParams marketParams)
     MorphoHarness.Id id = libId(marketParams);
     bool irmEnabled = isIrmEnabled(marketParams.irm);
     bool lltvEnabled = isLltvEnabled(marketParams.lltv);
-    uint256 lastUpdated = lastUpdate(id);
+    bool wasCreated = isCreated(id);
     createMarket@withrevert(e, marketParams);
-    assert lastReverted <=> e.msg.value != 0 || !irmEnabled || !lltvEnabled || lastUpdated != 0;
+    assert lastReverted <=> e.msg.value != 0 || !irmEnabled || !lltvEnabled || wasCreated;
 }
 
 // Check that supply reverts when its input are not validated.
@@ -125,7 +125,7 @@ rule withdrawInputValidation(env e, MorphoHarness.MarketParams marketParams, uin
     require e.msg.sender != 0;
     requireInvariant zeroDoesNotAuthorize(e.msg.sender);
     withdraw@withrevert(e, marketParams, assets, shares, onBehalf, receiver);
-    assert !exactlyOneZero(assets, shares) || onBehalf == 0 => lastReverted;
+    assert !exactlyOneZero(assets, shares) || onBehalf == 0 || receiver == 0 => lastReverted;
 }
 
 // Check that borrow reverts when its inputs are not validated.
@@ -134,7 +134,7 @@ rule borrowInputValidation(env e, MorphoHarness.MarketParams marketParams, uint2
     require e.msg.sender != 0;
     requireInvariant zeroDoesNotAuthorize(e.msg.sender);
     borrow@withrevert(e, marketParams, assets, shares, onBehalf, receiver);
-    assert !exactlyOneZero(assets, shares) || onBehalf == 0 => lastReverted;
+    assert !exactlyOneZero(assets, shares) || onBehalf == 0  || receiver == 0 => lastReverted;
 }
 
 // Check that repay reverts when its inputs are not validated.
@@ -155,7 +155,7 @@ rule withdrawCollateralInputValidation(env e, MorphoHarness.MarketParams marketP
     require e.msg.sender != 0;
     requireInvariant zeroDoesNotAuthorize(e.msg.sender);
     withdrawCollateral@withrevert(e, marketParams, assets, onBehalf, receiver);
-    assert assets == 0 || onBehalf == 0 => lastReverted;
+    assert assets == 0 || onBehalf == 0 || receiver == 0 => lastReverted;
 }
 
 // Check that liquidate reverts when its inputs are not validated.
@@ -173,7 +173,7 @@ rule setAuthorizationWithSigInputValidation(env e, MorphoHarness.Authorization a
 
 // Check that accrueInterest reverts when its inputs are not validated.
 rule accrueInterestInputValidation(env e, MorphoHarness.MarketParams marketParams) {
-    uint256 lastUpdate = lastUpdate(libId(marketParams));
+    bool wasCreated = isCreated(libId(marketParams));
     accrueInterest@withrevert(e, marketParams);
-    assert lastUpdate == 0 => lastReverted;
+    assert !wasCreated => lastReverted;
 }

certora/specs/Transfer.spec

@@ -63,8 +63,6 @@ rule transferRevertCondition(address token, address to, uint256 amount) {
     uint256 toInitialBalance = balanceOf(token, to);
     // Safe require because the total supply is greater than the sum of the balance of any two accounts.
     require to != currentContract => initialBalance + toInitialBalance <= to_mathint(totalSupply(token));
-    // Some tokens revert when either the sender or the receiver is the zero address.
-    require currentContract != 0 && to != 0;
 
     libSafeTransfer@withrevert(token, to, amount);
 
@@ -78,8 +76,6 @@ rule transferFromRevertCondition(address token, address from, address to, uint25
     uint256 allowance = allowance(token, from, currentContract);
     // Safe require because the total supply is greater than the sum of the balance of any two accounts.
     require to != from => initialBalance + toInitialBalance <= to_mathint(totalSupply(token));
-    // Some tokens revert when either the sender or the receiver is the zero address.
-    require from != 0 && to != 0;
 
     libSafeTransferFrom@withrevert(token, from, to, amount);