[Certora] Assets accounting when entering a position

.github/workflows/certora.yml

@@ -17,9 +17,9 @@ jobs:
       matrix:
         conf:
           - AccrueInterest
+          - AssetsAccounting
           - ConsistentState
           - ExactMath
-          - ExitLiquidity
           - Health
           - LibSummary
           - Liveness

certora/README.md

@@ -243,11 +243,12 @@ The [`certora/specs`](specs) folder contains the following files:
 - [`AccrueInterest.spec`](specs/AccrueInterest.spec) checks that the main functions accrue interest at the start of the interaction.
   This is done by ensuring that accruing interest before calling the function does not change the outcome compared to just calling the function.
   View functions do not necessarily respect this property (for example, `totalSupplyShares`), and are filtered out.
+- [`AssetsAccounting.spec`](specs/AssetsAccounting.spec) checks that when exiting a position the user cannot get more than what was owed.
+  Similarly, when entering a position, the assets owned as a result are no greater than what was given.
 - [`ConsistentState.spec`](specs/ConsistentState.spec) checks that the state (storage) of the Morpho contract is consistent.
   This includes checking that the accounting of the total amount and shares is correct, that markets are independent from each other, that only enabled IRMs and LLTVs can be used, and that users cannot have their position made worse by an unauthorized account.
 - [`ExactMath.spec`](specs/ExactMath.spec) checks precise properties when taking into account exact multiplication and division.
   Notably, this file specifies that using supply and withdraw in the same block cannot yield more funds than at the start.
-- [`ExitLiquidity.spec`](specs/ExitLiquidity.spec) checks that when exiting a position with withdraw, withdrawCollateral, or repay, the user cannot get more than what was owed.
 - [`Health.spec`](specs/Health.spec) checks properties about the health of the positions.
   Notably, functions cannot render an account unhealthy, and debt positions always have some collateral (thanks to the bad debt realization mechanism).
 - [`LibSummary.spec`](specs/LibSummary.spec) checks the summarization of the library functions that are used in other specification files.

certora/confs/AssetsAccounting.conf

@@ -0,0 +1,8 @@
+{
+    "files": [
+        "certora/harness/MorphoHarness.sol"
+    ],
+    "verify": "MorphoHarness:certora/specs/AssetsAccounting.spec",
+    "rule_sanity": "basic",
+    "msg": "Morpho Blue Assets Accounting"
+}

certora/specs/AssetsAccounting.spec

@@ -0,0 +1,126 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+methods {
+    function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE;
+
+    function supplyShares(MorphoHarness.Id, address) external returns uint256 envfree;
+    function borrowShares(MorphoHarness.Id, address) external returns uint256 envfree;
+    function collateral(MorphoHarness.Id, address) external returns uint256 envfree;
+    function virtualTotalSupplyAssets(MorphoHarness.Id) external returns uint256 envfree;
+    function virtualTotalSupplyShares(MorphoHarness.Id) external returns uint256 envfree;
+    function virtualTotalBorrowAssets(MorphoHarness.Id) external returns uint256 envfree;
+    function virtualTotalBorrowShares(MorphoHarness.Id) external returns uint256 envfree;
+    function lastUpdate(MorphoHarness.Id) external returns uint256 envfree;
+
+    function libMulDivDown(uint256, uint256, uint256) external returns uint256 envfree;
+    function libMulDivUp(uint256, uint256, uint256) external returns uint256 envfree;
+    function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;
+}
+
+function expectedSupplyAssets(MorphoHarness.Id id, address user) returns uint256 {
+    uint256 userShares = supplyShares(id, user);
+    uint256 totalSupplyAssets = virtualTotalSupplyAssets(id);
+    uint256 totalSupplyShares = virtualTotalSupplyShares(id);
+
+    return libMulDivDown(userShares, totalSupplyAssets, totalSupplyShares);
+}
+
+function expectedBorrowAssets(MorphoHarness.Id id, address user) returns uint256 {
+    uint256 userShares = borrowShares(id, user);
+    uint256 totalBorrowAssets = virtualTotalBorrowAssets(id);
+    uint256 totalBorrowShares = virtualTotalBorrowShares(id);
+
+    return libMulDivUp(userShares, totalBorrowAssets, totalBorrowShares);
+}
+
+// Check that the assets supplied are greater than the assets owned in the end.
+rule supplyAssetsAccounting(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) {
+    MorphoHarness.Id id = libId(marketParams);
+
+    // Assume no interest as it would increase the total supply assets.
+    require lastUpdate(id) == e.block.timestamp;
+    // Assume no supply position to begin with.
+    require supplyShares(id, onBehalf) == 0;
+
+    uint256 suppliedAssets;
+    suppliedAssets, _ = supply(e, marketParams, assets, shares, onBehalf, data);
+
+    uint256 ownedAssets = expectedSupplyAssets(id, onBehalf);
+
+    assert suppliedAssets >= ownedAssets;
+}
+
+// Check that the assets withdrawn are less than the assets owned initially.
+rule withdrawAssetsAccounting(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) {
+    MorphoHarness.Id id = libId(marketParams);
+
+    // Assume no interest as it would increase the total supply assets.
+    require lastUpdate(id) == e.block.timestamp;
+
+    uint256 ownedAssets = expectedSupplyAssets(id, onBehalf);
+
+    uint256 withdrawnAssets;
+    withdrawnAssets, _ = withdraw(e, marketParams, assets, shares, onBehalf, receiver);
+
+    assert withdrawnAssets <= ownedAssets;
+}
+
+// Check that the assets borrowed are less than the assets owed in the end.
+rule borrowAssetsAccounting(env e, MorphoHarness.MarketParams marketParams, uint256 shares, address onBehalf, address receiver) {
+    MorphoHarness.Id id = libId(marketParams);
+
+    // Assume no interest as it would increase the total borrowed assets.
+    require lastUpdate(id) == e.block.timestamp;
+    // Assume no outstanding debt to begin with.
+    require borrowShares(id, onBehalf) == 0;
+
+    // The borrow call is restricted to shares as input to make it easier on the prover.
+    uint256 borrowedAssets;
+    borrowedAssets, _ = borrow(e, marketParams, 0, shares, onBehalf, receiver);
+
+    uint256 owedAssets = expectedBorrowAssets(id, onBehalf);
+
+    assert borrowedAssets <= owedAssets;
+}
+
+// Check that the assets repaid are greater than the assets owed initially.
+rule repayAssetsAccounting(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) {
+    MorphoHarness.Id id = libId(marketParams);
+
+    // Assume no interest as it would increase the total borrowed assets.
+    require lastUpdate(id) == e.block.timestamp;
+
+    uint256 owedAssets = expectedBorrowAssets(id, onBehalf);
+
+    uint256 repaidAssets;
+    repaidAssets, _ = repay(e, marketParams, assets, shares, onBehalf, data);
+
+    // Assume a full repay.
+    require borrowShares(id, onBehalf) == 0;
+
+    assert repaidAssets >= owedAssets;
+}
+
+// Check that the collateral assets supplied are greater than the assets owned in the end.
+rule supplyCollateralAssetsAccounting(env e, MorphoHarness.MarketParams marketParams, uint256 suppliedAssets, address onBehalf, bytes data) {
+    MorphoHarness.Id id = libId(marketParams);
+
+    // Assume no collateral to begin with.
+    require collateral(id, onBehalf) == 0;
+
+    supplyCollateral(e, marketParams, suppliedAssets, onBehalf, data);
+
+    uint256 ownedAssets = collateral(id, onBehalf);
+
+    assert suppliedAssets == ownedAssets;
+}
+
+// Check that the collateral assets withdrawn are less than the assets owned initially.
+rule withdrawCollateralAssetsAccounting(env e, MorphoHarness.MarketParams marketParams, uint256 withdrawnAssets, address onBehalf, address receiver) {
+    MorphoHarness.Id id = libId(marketParams);
+
+    uint256 ownedAssets = collateral(id, onBehalf);
+
+    withdrawCollateral(e, marketParams, withdrawnAssets, onBehalf, receiver);
+
+    assert withdrawnAssets <= ownedAssets;
+}

certora/specs/Liveness.spec

@@ -23,8 +23,8 @@ methods {
     function SafeTransferLib.safeTransferFrom(address token, address from, address to, uint256 value) internal => summarySafeTransferFrom(token, from, to, value);
 }
 
-ghost mapping(address => mathint) myBalances {
-    init_state axiom (forall address token. myBalances[token] == 0);
+ghost mapping(address => mathint) balance {
+    init_state axiom (forall address token. balance[token] == 0);
 }
 
 function summaryId(MorphoInternalAccess.MarketParams marketParams) returns MorphoInternalAccess.Id {
@@ -34,11 +34,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.
-        myBalances[token] = require_uint256(myBalances[token] - amount);
+        balance[token] = require_uint256(balance[token] - amount);
     }
     if (to == currentContract) {
         // Safe require because the reference implementation would revert.
-        myBalances[token] = require_uint256(myBalances[token] + amount);
+        balance[token] = require_uint256(balance[token] + amount);
     }
 }
 
@@ -75,15 +75,15 @@ rule supplyChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams marke
     require lastUpdate(id) == e.block.timestamp;
 
     mathint sharesBefore = supplyShares(id, onBehalf);
-    mathint balanceBefore = myBalances[marketParams.loanToken];
+    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 = myBalances[marketParams.loanToken];
+    mathint balanceAfter = balance[marketParams.loanToken];
     mathint liquidityAfter = totalSupplyAssets(id) - totalBorrowAssets(id);
 
     assert assets != 0 => suppliedAssets == assets;
@@ -111,15 +111,15 @@ rule withdrawChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams mar
     require lastUpdate(id) == e.block.timestamp;
 
     mathint sharesBefore = supplyShares(id, onBehalf);
-    mathint balanceBefore = myBalances[marketParams.loanToken];
+    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 = myBalances[marketParams.loanToken];
+    mathint balanceAfter = balance[marketParams.loanToken];
     mathint liquidityAfter = totalSupplyAssets(id) - totalBorrowAssets(id);
 
     assert assets != 0 => withdrawnAssets == assets;
@@ -147,15 +147,15 @@ rule borrowChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams marke
     require lastUpdate(id) == e.block.timestamp;
 
     mathint sharesBefore = borrowShares(id, onBehalf);
-    mathint balanceBefore = myBalances[marketParams.loanToken];
+    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 = myBalances[marketParams.loanToken];
+    mathint balanceAfter = balance[marketParams.loanToken];
     mathint liquidityAfter = totalSupplyAssets(id) - totalBorrowAssets(id);
 
     assert assets != 0 => borrowedAssets == assets;
@@ -183,7 +183,7 @@ rule repayChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams market
     require lastUpdate(id) == e.block.timestamp;
 
     mathint sharesBefore = borrowShares(id, onBehalf);
-    mathint balanceBefore = myBalances[marketParams.loanToken];
+    mathint balanceBefore = balance[marketParams.loanToken];
     mathint liquidityBefore = totalSupplyAssets(id) - totalBorrowAssets(id);
 
     mathint borrowAssetsBefore = totalBorrowAssets(id);
@@ -193,7 +193,7 @@ rule repayChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams market
     repaidAssets, repaidShares = repay(e, marketParams, assets, shares, onBehalf, data);
 
     mathint sharesAfter = borrowShares(id, onBehalf);
-    mathint balanceAfter = myBalances[marketParams.loanToken];
+    mathint balanceAfter = balance[marketParams.loanToken];
     mathint liquidityAfter = totalSupplyAssets(id) - totalBorrowAssets(id);
 
     assert assets != 0 => repaidAssets == assets;
@@ -220,12 +220,12 @@ rule supplyCollateralChangesTokensAndBalance(env e, MorphoInternalAccess.MarketP
     require currentContract != e.msg.sender;
 
     mathint collateralBefore = collateral(id, onBehalf);
-    mathint balanceBefore = myBalances[marketParams.collateralToken];
+    mathint balanceBefore = balance[marketParams.collateralToken];
 
     supplyCollateral(e, marketParams, assets, onBehalf, data);
 
     mathint collateralAfter = collateral(id, onBehalf);
-    mathint balanceAfter = myBalances[marketParams.collateralToken];
+    mathint balanceAfter = balance[marketParams.collateralToken];
 
     assert collateralAfter == collateralBefore + assets;
     assert balanceAfter == balanceBefore + assets;
@@ -241,12 +241,12 @@ rule withdrawCollateralChangesTokensAndBalance(env e, MorphoInternalAccess.Marke
     require lastUpdate(id) == e.block.timestamp;
 
     mathint collateralBefore = collateral(id, onBehalf);
-    mathint balanceBefore = myBalances[marketParams.collateralToken];
+    mathint balanceBefore = balance[marketParams.collateralToken];
 
     withdrawCollateral(e, marketParams, assets, onBehalf, receiver);
 
     mathint collateralAfter = collateral(id, onBehalf);
-    mathint balanceAfter = myBalances[marketParams.collateralToken];
+    mathint balanceAfter = balance[marketParams.collateralToken];
 
     assert collateralAfter == collateralBefore - assets;
     assert balanceAfter == balanceBefore - assets;
@@ -264,8 +264,8 @@ rule liquidateChangesTokens(env e, MorphoInternalAccess.MarketParams marketParam
     require lastUpdate(id) == e.block.timestamp;
 
     mathint collateralBefore = collateral(id, borrower);
-    mathint balanceLoanBefore = myBalances[marketParams.loanToken];
-    mathint balanceCollateralBefore = myBalances[marketParams.collateralToken];
+    mathint balanceLoanBefore = balance[marketParams.loanToken];
+    mathint balanceCollateralBefore = balance[marketParams.collateralToken];
     mathint liquidityBefore = totalSupplyAssets(id) - totalBorrowAssets(id);
 
     mathint borrowLoanAssetsBefore = totalBorrowAssets(id);
@@ -275,8 +275,8 @@ rule liquidateChangesTokens(env e, MorphoInternalAccess.MarketParams marketParam
     seizedAssets, repaidAssets = liquidate(e, marketParams, borrower, seized, repaidShares, data);
 
     mathint collateralAfter = collateral(id, borrower);
-    mathint balanceLoanAfter = myBalances[marketParams.loanToken];
-    mathint balanceCollateralAfter = myBalances[marketParams.collateralToken];
+    mathint balanceLoanAfter = balance[marketParams.loanToken];
+    mathint balanceCollateralAfter = balance[marketParams.collateralToken];
     mathint liquidityAfter = totalSupplyAssets(id) - totalBorrowAssets(id);
 
     assert seized != 0 => seizedAssets == seized;