Fix unsound require assumptions in Liveness spec (#781)

.github/workflows/certora.yml

@@ -23,6 +23,7 @@ jobs:
           - LibSummary
           - LiquidateBuffer
           - Liveness
+          - Reachability
           - Reentrancy
           - Reverts
           - StayHealthy

certora/confs/Reachability.conf

@@ -0,0 +1,11 @@
+{
+  "files": [
+    "certora/helpers/MorphoInternalAccess.sol",
+    "certora/helpers/Util.sol"
+  ],
+  "solc": "solc-0.8.19",
+  "verify": "MorphoInternalAccess:certora/specs/Reachability.spec",
+  "rule_sanity": "basic",
+  "server": "production",
+  "msg": "Morpho Blue Reachability"
+}

certora/specs/Liveness.spec

@@ -1,5 +1,7 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 
+// Liveness properties: a user can always exit the market by repaying, withdrawing, or withdrawing collateral.
+
 using Util as Util;
 
 methods {
@@ -13,6 +15,8 @@ methods {
     function virtualTotalSupplyShares(MorphoInternalAccess.Id) external returns uint256 envfree;
     function totalBorrowAssets(MorphoInternalAccess.Id) external returns uint256 envfree;
     function totalBorrowShares(MorphoInternalAccess.Id) external returns uint256 envfree;
+    function virtualTotalBorrowAssets(MorphoInternalAccess.Id) external returns uint256 envfree;
+    function virtualTotalBorrowShares(MorphoInternalAccess.Id) external returns uint256 envfree;
     function fee(MorphoInternalAccess.Id) external returns uint256 envfree;
     function lastUpdate(MorphoInternalAccess.Id) external returns uint256 envfree;
     function nonce(address) external returns uint256 envfree;
@@ -29,7 +33,7 @@ methods {
     function SafeTransferLib.safeTransferFrom(address token, address from, address to, uint256 value) internal => summarySafeTransferFrom(token, from, to, value);
 }
 
-persistent ghost mapping(address => mathint) balance {
+persistent ghost mapping(address => uint256) balance {
     init_state axiom (forall address token. balance[token] == 0);
 }
 
@@ -39,11 +43,11 @@ function summaryId(MorphoInternalAccess.MarketParams marketParams) returns Morph
 
 function summarySafeTransferFrom(address token, address from, address to, uint256 amount) {
     if (from == currentContract) {
-        // Safe require because the reference implementation would revert.
-        balance[token] = require_uint256(balance[token] - amount);
+        // Assert instead of require because this is a liveness property: the absence of underflow must be proven, not assumed.
+        balance[token] = assert_uint256(balance[token] - amount);
     }
     if (to == currentContract) {
-        // Safe require because the reference implementation would revert.
+        // Safe require as the sum of balances is equal to totalSupply <= type(uint256).max.
         balance[token] = require_uint256(balance[token] + amount);
     }
 }
@@ -74,249 +78,6 @@ function summaryAccrueInterest(env e, MorphoInternalAccess.MarketParams marketPa
 definition isCreated(MorphoInternalAccess.Id id) returns bool =
     lastUpdate(id) != 0;
 
-// Check that tokens and shares are properly accounted following a supply.
-rule supplyChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) {
-    MorphoInternalAccess.Id id = Util.libId(marketParams);
-
-    // Safe require because Morpho cannot call such functions by itself.
-    require currentContract != e.msg.sender;
-    // Assumption to ensure that no interest is accumulated.
-    require lastUpdate(id) == e.block.timestamp;
-
-    mathint sharesBefore = supplyShares(id, onBehalf);
-    mathint balanceBefore = balance[marketParams.loanToken];
-    mathint liquidityBefore = totalSupplyAssets(id) - totalBorrowAssets(id);
-
-    uint256 suppliedAssets;
-    uint256 suppliedShares;
-    suppliedAssets, suppliedShares = supply(e, marketParams, assets, shares, onBehalf, data);
-
-    mathint sharesAfter = supplyShares(id, onBehalf);
-    mathint balanceAfter = balance[marketParams.loanToken];
-    mathint liquidityAfter = totalSupplyAssets(id) - totalBorrowAssets(id);
-
-    assert assets != 0 => suppliedAssets == assets;
-    assert shares != 0 => suppliedShares == shares;
-    assert sharesAfter == sharesBefore + suppliedShares;
-    assert balanceAfter == balanceBefore + suppliedAssets;
-    assert liquidityAfter == liquidityBefore + suppliedAssets;
-}
-
-// Check that you can supply non-zero tokens by passing shares.
-rule canSupplyByPassingShares(env e, MorphoInternalAccess.MarketParams marketParams, uint256 shares, address onBehalf, bytes data) {
-    uint256 suppliedAssets;
-    suppliedAssets, _ = supply(e, marketParams, 0, shares, onBehalf, data);
-
-    satisfy suppliedAssets != 0;
-}
-
-// Check that tokens and shares are properly accounted following a withdraw.
-rule withdrawChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) {
-    MorphoInternalAccess.Id id = Util.libId(marketParams);
-
-    // Assume that Morpho is not the receiver.
-    require currentContract != receiver;
-    // Assumption to ensure that no interest is accumulated.
-    require lastUpdate(id) == e.block.timestamp;
-
-    mathint sharesBefore = supplyShares(id, onBehalf);
-    mathint balanceBefore = balance[marketParams.loanToken];
-    mathint liquidityBefore = totalSupplyAssets(id) - totalBorrowAssets(id);
-
-    uint256 withdrawnAssets;
-    uint256 withdrawnShares;
-    withdrawnAssets, withdrawnShares = withdraw(e, marketParams, assets, shares, onBehalf, receiver);
-
-    mathint sharesAfter = supplyShares(id, onBehalf);
-    mathint balanceAfter = balance[marketParams.loanToken];
-    mathint liquidityAfter = totalSupplyAssets(id) - totalBorrowAssets(id);
-
-    assert assets != 0 => withdrawnAssets == assets;
-    assert shares != 0 => withdrawnShares == shares;
-    assert sharesAfter == sharesBefore - withdrawnShares;
-    assert balanceAfter == balanceBefore - withdrawnAssets;
-    assert liquidityAfter == liquidityBefore - withdrawnAssets;
-}
-
-// Check that you can withdraw non-zero tokens by passing shares.
-rule canWithdrawByPassingShares(env e, MorphoInternalAccess.MarketParams marketParams, uint256 shares, address onBehalf, address receiver) {
-    uint256 withdrawnAssets;
-    withdrawnAssets, _ = withdraw(e, marketParams, 0, shares, onBehalf, receiver);
-
-    satisfy withdrawnAssets != 0;
-}
-
-// Check that tokens and shares are properly accounted following a borrow.
-rule borrowChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) {
-    MorphoInternalAccess.Id id = Util.libId(marketParams);
-
-    // Assume that Morpho is not the receiver.
-    require currentContract != receiver;
-    // Assumption to ensure that no interest is accumulated.
-    require lastUpdate(id) == e.block.timestamp;
-
-    mathint sharesBefore = borrowShares(id, onBehalf);
-    mathint balanceBefore = balance[marketParams.loanToken];
-    mathint liquidityBefore = totalSupplyAssets(id) - totalBorrowAssets(id);
-
-    uint256 borrowedAssets;
-    uint256 borrowedShares;
-    borrowedAssets, borrowedShares = borrow(e, marketParams, assets, shares, onBehalf, receiver);
-
-    mathint sharesAfter = borrowShares(id, onBehalf);
-    mathint balanceAfter = balance[marketParams.loanToken];
-    mathint liquidityAfter = totalSupplyAssets(id) - totalBorrowAssets(id);
-
-    assert assets != 0 => borrowedAssets == assets;
-    assert shares != 0 => borrowedShares == shares;
-    assert sharesAfter == sharesBefore + borrowedShares;
-    assert balanceAfter == balanceBefore - borrowedAssets;
-    assert liquidityAfter == liquidityBefore - borrowedAssets;
-}
-
-// Check that you can borrow non-zero tokens by passing shares.
-rule canBorrowByPassingShares(env e, MorphoInternalAccess.MarketParams marketParams, uint256 shares, address onBehalf, address receiver) {
-    uint256 borrowedAssets;
-    borrowedAssets, _ = borrow(e, marketParams, 0, shares, onBehalf, receiver);
-
-    satisfy borrowedAssets != 0;
-}
-
-// Check that tokens and shares are properly accounted following a repay.
-rule repayChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) {
-    MorphoInternalAccess.Id id = Util.libId(marketParams);
-
-    // Safe require because Morpho cannot call such functions by itself.
-    require currentContract != e.msg.sender;
-    // Assumption to ensure that no interest is accumulated.
-    require lastUpdate(id) == e.block.timestamp;
-
-    mathint sharesBefore = borrowShares(id, onBehalf);
-    mathint balanceBefore = balance[marketParams.loanToken];
-    mathint liquidityBefore = totalSupplyAssets(id) - totalBorrowAssets(id);
-
-    mathint borrowAssetsBefore = totalBorrowAssets(id);
-
-    uint256 repaidAssets;
-    uint256 repaidShares;
-    repaidAssets, repaidShares = repay(e, marketParams, assets, shares, onBehalf, data);
-
-    mathint sharesAfter = borrowShares(id, onBehalf);
-    mathint balanceAfter = balance[marketParams.loanToken];
-    mathint liquidityAfter = totalSupplyAssets(id) - totalBorrowAssets(id);
-
-    assert assets != 0 => repaidAssets == assets;
-    assert shares != 0 => repaidShares == shares;
-    assert sharesAfter == sharesBefore - repaidShares;
-    assert balanceAfter == balanceBefore + repaidAssets;
-    // Taking the min to handle the zeroFloorSub in the code.
-    assert liquidityAfter == liquidityBefore + min(repaidAssets, borrowAssetsBefore);
-}
-
-// Check that you can repay non-zero tokens by passing shares.
-rule canRepayByPassingShares(env e, MorphoInternalAccess.MarketParams marketParams, uint256 shares, address onBehalf, bytes data) {
-    uint256 repaidAssets;
-    repaidAssets, _ = repay(e, marketParams, 0, shares, onBehalf, data);
-
-    satisfy repaidAssets != 0;
-}
-
-// Check that tokens and balances are properly accounted following a supplyCollateral.
-rule supplyCollateralChangesTokensAndBalance(env e, MorphoInternalAccess.MarketParams marketParams, uint256 assets, address onBehalf, bytes data) {
-    MorphoInternalAccess.Id id = Util.libId(marketParams);
-
-    // Safe require because Morpho cannot call such functions by itself.
-    require currentContract != e.msg.sender;
-
-    mathint collateralBefore = collateral(id, onBehalf);
-    mathint balanceBefore = balance[marketParams.collateralToken];
-
-    supplyCollateral(e, marketParams, assets, onBehalf, data);
-
-    mathint collateralAfter = collateral(id, onBehalf);
-    mathint balanceAfter = balance[marketParams.collateralToken];
-
-    assert collateralAfter == collateralBefore + assets;
-    assert balanceAfter == balanceBefore + assets;
-}
-
-// Check that tokens and balances are properly accounted following a withdrawCollateral.
-rule withdrawCollateralChangesTokensAndBalance(env e, MorphoInternalAccess.MarketParams marketParams, uint256 assets, address onBehalf, address receiver) {
-    MorphoInternalAccess.Id id = Util.libId(marketParams);
-
-    // Assume that Morpho is not the receiver.
-    require currentContract != receiver;
-    // Assumption to ensure that no interest is accumulated.
-    require lastUpdate(id) == e.block.timestamp;
-
-    mathint collateralBefore = collateral(id, onBehalf);
-    mathint balanceBefore = balance[marketParams.collateralToken];
-
-    withdrawCollateral(e, marketParams, assets, onBehalf, receiver);
-
-    mathint collateralAfter = collateral(id, onBehalf);
-    mathint balanceAfter = balance[marketParams.collateralToken];
-
-    assert collateralAfter == collateralBefore - assets;
-    assert balanceAfter == balanceBefore - assets;
-}
-
-// Check that tokens are properly accounted following a liquidate.
-rule liquidateChangesTokens(env e, MorphoInternalAccess.MarketParams marketParams, address borrower, uint256 seized, uint256 repaidShares, bytes data) {
-    MorphoInternalAccess.Id id = Util.libId(marketParams);
-
-    // Safe require because Morpho cannot call such functions by itself.
-    require currentContract != e.msg.sender;
-    // Assumption to simplify the balance specification in the rest of this rule.
-    require marketParams.loanToken != marketParams.collateralToken;
-    // Assumption to ensure that no interest is accumulated.
-    require lastUpdate(id) == e.block.timestamp;
-
-    mathint collateralBefore = collateral(id, borrower);
-    mathint balanceLoanBefore = balance[marketParams.loanToken];
-    mathint balanceCollateralBefore = balance[marketParams.collateralToken];
-    mathint liquidityBefore = totalSupplyAssets(id) - totalBorrowAssets(id);
-
-    mathint borrowLoanAssetsBefore = totalBorrowAssets(id);
-
-    uint256 seizedAssets;
-    uint256 repaidAssets;
-    seizedAssets, repaidAssets = liquidate(e, marketParams, borrower, seized, repaidShares, data);
-
-    mathint collateralAfter = collateral(id, borrower);
-    mathint balanceLoanAfter = balance[marketParams.loanToken];
-    mathint balanceCollateralAfter = balance[marketParams.collateralToken];
-    mathint liquidityAfter = totalSupplyAssets(id) - totalBorrowAssets(id);
-
-    assert seized != 0 => seizedAssets == seized;
-    assert collateralBefore > to_mathint(seizedAssets) => collateralAfter == collateralBefore - seizedAssets;
-    assert balanceLoanAfter == balanceLoanBefore + repaidAssets;
-    assert balanceCollateralAfter == balanceCollateralBefore - seizedAssets;
-    // Taking the min to handle the zeroFloorSub in the code.
-    assert liquidityAfter == liquidityBefore + min(repaidAssets, borrowLoanAssetsBefore);
-}
-
-// Check that you can liquidate non-zero tokens by passing shares.
-rule canLiquidateByPassingShares(env e, MorphoInternalAccess.MarketParams marketParams, address borrower, uint256 repaidShares, bytes data) {
-    uint256 seizedAssets;
-    uint256 repaidAssets;
-    seizedAssets, repaidAssets = liquidate(e, marketParams, borrower, 0, repaidShares,  data);
-
-    satisfy seizedAssets != 0 && repaidAssets != 0;
-}
-
-// Check that nonce and authorization are properly updated with calling setAuthorizationWithSig.
-rule setAuthorizationWithSigChangesNonceAndAuthorizes(env e, MorphoInternalAccess.Authorization authorization, MorphoInternalAccess.Signature signature) {
-    mathint nonceBefore = nonce(authorization.authorizer);
-
-    setAuthorizationWithSig(e, authorization, signature);
-
-    mathint nonceAfter = nonce(authorization.authorizer);
-
-    assert nonceAfter == nonceBefore + 1;
-    assert isAuthorized(authorization.authorizer, authorization.authorized) == authorization.isAuthorized;
-}
-
 // Check that one can always repay the debt in full.
 rule canRepayAll(env e, MorphoInternalAccess.MarketParams marketParams, uint256 shares, bytes data) {
     MorphoInternalAccess.Id id = Util.libId(marketParams);
@@ -329,6 +90,8 @@ rule canRepayAll(env e, MorphoInternalAccess.MarketParams marketParams, uint256
     // Omit sanity checks.
     require isCreated(id);
     require e.msg.sender != 0;
+    // Safe require because Morpho cannot call such functions by itself.
+    require currentContract != e.msg.sender;
     require e.msg.value == 0;
     require shares > 0;
     // Safe require because of the noTimeTravel rule.
@@ -364,6 +127,8 @@ rule canWithdrawAll(env e, MorphoInternalAccess.MarketParams marketParams, uint2
     require lastUpdate(id) <= e.block.timestamp;
     // Safe require because of the sumSupplySharesCorrect invariant.
     require shares <= totalSupplyShares(id);
+    // Assume that the singleton holds enough tokens to cover the withdrawal, which is at most totalSupplyAssets. Justified by the idleAmountLessThanBalance invariant (ConsistentState.spec).
+    require balance[marketParams.loanToken] >= to_mathint(totalSupplyAssets(id));
 
     // Accrue interest first, for the shares -> assets conversion below.
     // Safe because of the AccrueInterest.withdrawAccruesInterest rule, and because `_accrueInterest` is already summarized like so in this file.
@@ -394,6 +159,8 @@ rule canWithdrawCollateralAll(env e, MorphoInternalAccess.MarketParams marketPar
     require lastUpdate(id) <= e.block.timestamp;
     // Assume that the user does not have an outstanding debt.
     require borrowShares(id, e.msg.sender) == 0;
+    // Assume that the singleton holds enough collateral tokens to cover the withdrawal. Justified by the idleAmountLessThanBalance invariant (ConsistentState.spec).
+    require balance[marketParams.collateralToken] >= to_mathint(assets);
 
     withdrawCollateral@withrevert(e, marketParams, assets, e.msg.sender, receiver);