[Certora] Add README

certora/README.md

@@ -0,0 +1,61 @@
+This folder contains the verification of the Morpho Blue protocol using CVL, Certora's Verification Language.
+
+## High-Level Description
+
+The Morpho Blue protocol relies on several different concepts, which are described below.
+These concepts have been verified using CVL.
+See the description of the specification files below (or those files directly) for more details.
+
+The Morpho Blue protocol allows users to take out collateralized loans on ERC20 tokens.\
+**Transfers.** Token transfers are verified to behave as expected for the most common implementations, in particular the transferred amount is the amount passed as input.\
+**Markets**. Markets on Morpho Blue depend on a pair of assets, the borrowable asset that is supplied and borrowed, and the collateral asset.
+Markets are independent, which means that loans cannot be impacted by loans from other markets.
+Positions of users are also independent, so loans cannot be impacted by loans from other users.
+The accounting of the markets has been verified (such as the total amounts), as well as the fact that only market with enabled parameters are created.\
+**Supply.** When supplying on Morpho Blue, interest is earned over time, and the distribution is implemented through a shares mechanism.
+Shares increase in value as interest is accrued.\
+**Borrow.** To borrow on Morpho Blue, collateral must be deposited.
+Collateral tokens remain idle, as well as any borrowable token that has not been borrowed.\
+**Liquidation.** To ensure proper collateralization, a liquidation system is put in place.
+In the absence of accrued interest, for example when creating a new position or when interacting multiple times in the same block, a position cannot be made unhealthy.\
+**Authorization.** Morpho Blue also defines a sound authorization system where users cannot modify positions of other users without proper authorization (except when liquidating).\
+**Safety.** Other safety properties are verified, particularly regarding reentrancy attacks and about input validation and revert conditions.\
+**Liveness.** Other liveness properties are verified as well, in particular it is always possible to exit a position without concern for the oracle.
+
+## Folder and File Structure
+
+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.
+- [`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.
+- [`Liveness.spec`](./specs/Liveness.spec) checks that main functions change the owner of funds and the amount of shares as expected, and that it's always possible to exit a position.
+- [`RatioMath.spec`](./specs/RatioMath.spec) checks that the ratio between shares and assets evolves predictably over time.
+- [`Reentrancy.spec`](./specs/Reentrancy.spec) checks that the contract is immune to a particular class of reentrancy issues.
+- [`Reverts.spec`](./specs/Reverts.spec) checks the condition for reverts and that inputs are correctly validated.
+- [`Transfer.spec`](./specs/Transfer.spec) checks the summarization of the safe transfer library functions that are used in other specification files.
+
+The [`certora/scripts`](./scripts) folder contains a script for each corresponding specification file.
+
+The [`certora/harness`](./harness) folder contains contracts that enable the verification of Morpho Blue.
+Notably, this allows handling the fact that library functions should be called from a contract to be verified independently, and it allows defining needed getters.
+
+The [`certora/dispatch`](./dispatch) folder contains different contracts similar to the ones that are expected to be called from Morpho Blue.
+
+## Usage
+
+To verify specification files, run the corresponding script in the [`certora/scripts`](./scripts) folder.
+It requires having set the `CERTORAKEY` environment variable to a valid Certora key.
+You can pass arguments to the script, which allows you to verify specific properties. For example, at the root of the repository:
+
+```
+./certora/scripts/verifyConsistentState.sh --rule borrowLessSupply
+```

certora/harness/MorphoHarness.sol

@@ -70,21 +70,21 @@ contract MorphoHarness is Morpho {
         return market[id].totalBorrowShares + SharesMathLib.VIRTUAL_SHARES;
     }
 
-    function marketId(MarketParams memory marketParams) external pure returns (Id) {
+    function libId(MarketParams memory marketParams) external pure returns (Id) {
         return marketParams.id();
     }
 
-    function marketLibId(MarketParams memory marketParams) external pure returns (Id marketParamsId) {
+    function optimizedId(MarketParams memory marketParams) external pure returns (Id marketParamsId) {
         assembly ("memory-safe") {
             marketParamsId := keccak256(marketParams, mul(5, 32))
         }
     }
 
-    function mathLibMulDivUp(uint256 x, uint256 y, uint256 d) public pure returns (uint256) {
+    function libMulDivUp(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) {
+    function libMulDivDown(uint256 x, uint256 y, uint256 d) public pure returns (uint256) {
         return MathLib.mulDivDown(x, y, d);
     }
 

certora/harness/TransferHarness.sol

@@ -13,11 +13,11 @@ interface IERC20Extended is IERC20 {
 contract TransferHarness {
     using SafeTransferLib for IERC20;
 
-    function safeTransferFrom(address token, address from, address to, uint256 value) public {
+    function libSafeTransferFrom(address token, address from, address to, uint256 value) public {
         IERC20(token).safeTransferFrom(from, to, value);
     }
 
-    function safeTransfer(address token, address to, uint256 value) public {
+    function libSafeTransfer(address token, address to, uint256 value) public {
         IERC20(token).safeTransfer(to, value);
     }
 

certora/specs/ConsistentState.spec

@@ -10,7 +10,7 @@ methods {
     function collateral(MorphoHarness.Id, address) external returns uint256 envfree;
     function fee(MorphoHarness.Id) external returns uint256 envfree;
     function lastUpdate(MorphoHarness.Id) external returns uint256 envfree;
-    function marketId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;
+    function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;
 
     function isAuthorized(address, address) external returns bool envfree;
     function isLltvEnabled(uint256) external returns bool envfree;
@@ -108,9 +108,9 @@ invariant borrowLessSupply(MorphoHarness.Id id)
 
 // This invariant is useful in the following rule, to link an id back to a market.
 invariant marketInvariant(MorphoHarness.MarketParams marketParams)
-    isCreated(marketId(marketParams)) =>
-    idToBorrowable[marketId(marketParams)] == marketParams.borrowableToken &&
-    idToCollateral[marketId(marketParams)] == marketParams.collateralToken;
+    isCreated(libId(marketParams)) =>
+    idToBorrowable[libId(marketParams)] == marketParams.borrowableToken &&
+    idToCollateral[libId(marketParams)] == marketParams.collateralToken;
 
 // Check that the idle amount on the singleton is greater to the sum amount, that is the sum over all the markets of the total supply plus the total collateral minus the total borrow.
 invariant isLiquid(address token)
@@ -148,19 +148,19 @@ invariant isLiquid(address token)
 
 // Check that a market can only exist if its LLTV is enabled.
 invariant onlyEnabledLltv(MorphoHarness.MarketParams marketParams)
-    isCreated(marketId(marketParams)) => isLltvEnabled(marketParams.lltv);
+    isCreated(libId(marketParams)) => isLltvEnabled(marketParams.lltv);
 
 // Check that a market can only exist if its IRM is enabled.
 invariant onlyEnabledIrm(MorphoHarness.MarketParams marketParams)
-    isCreated(marketId(marketParams)) => isIrmEnabled(marketParams.irm);
+    isCreated(libId(marketParams)) => isIrmEnabled(marketParams.irm);
 
 // Check the pseudo-injectivity of the hashing function id().
-rule marketIdUnique() {
+rule libIdUnique() {
     MorphoHarness.MarketParams marketParams1;
     MorphoHarness.MarketParams marketParams2;
 
     // Require the same arguments.
-    require marketId(marketParams1) == marketId(marketParams2);
+    require libId(marketParams1) == libId(marketParams2);
 
     assert marketParams1.borrowableToken == marketParams2.borrowableToken;
     assert marketParams1.collateralToken == marketParams2.collateralToken;

certora/specs/ExactMath.spec

@@ -1,7 +1,7 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 methods {
     function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE(true);
-    function marketId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;
+    function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id 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;
@@ -26,8 +26,9 @@ function summaryMulDivDown(uint256 x, uint256 y, uint256 d) returns uint256 {
     return require_uint256((x * y) / d);
 }
 
+// Check that when not accruing interest, and when repaying all, the borrow ratio is at least reset to the initial ratio.
 rule repayAllResetsBorrowRatio(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onbehalf, bytes data) {
-    MorphoHarness.Id id = marketId(marketParams);
+    MorphoHarness.Id id = libId(marketParams);
     require fee(id) <= maxFee();
 
     mathint assetsBefore = virtualTotalBorrowAssets(id);
@@ -44,12 +45,13 @@ rule repayAllResetsBorrowRatio(env e, MorphoHarness.MarketParams marketParams, u
     mathint sharesAfter = virtualTotalBorrowShares(id);
 
     assert assetsAfter == 1;
+    // There are at least as many shares as virtual shares.
 }
 
 // There should be no profit from supply followed immediately by withdraw.
 rule supplyWithdraw() {
     MorphoHarness.MarketParams marketParams;
-    MorphoHarness.Id id = marketId(marketParams);
+    MorphoHarness.Id id = libId(marketParams);
     uint256 assets;
     uint256 shares;
     address onbehalf;
@@ -82,7 +84,7 @@ rule supplyWithdraw() {
 // There should be no profit from withdraw followed immediately by supply.
 rule withdrawSupply() {
     MorphoHarness.MarketParams marketParams;
-    MorphoHarness.Id id = marketId(marketParams);
+    MorphoHarness.Id id = libId(marketParams);
     uint256 assets;
     uint256 shares;
     address onbehalf;

certora/specs/ExitLiquidity.spec

@@ -11,22 +11,22 @@ methods {
 
     function lastUpdate(MorphoHarness.Id) external returns uint256 envfree;
 
-    function mathLibMulDivDown(uint256, uint256, uint256) external returns uint256 envfree;
-    function mathLibMulDivUp(uint256, uint256, uint256) external returns uint256 envfree;
-    function marketId(MorphoHarness.MarketParams) external returns MorphoHarness.Id 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;
 }
 
 // Check that it's not possible to withdraw more assets than what the user has supplied.
 rule withdrawLiquidity(MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) {
     env e;
-    MorphoHarness.Id id = marketId(marketParams);
+    MorphoHarness.Id id = libId(marketParams);
 
     require lastUpdate(id) == e.block.timestamp;
 
     uint256 initialShares = supplyShares(id, onBehalf);
     uint256 initialTotalSupply = virtualTotalSupplyAssets(id);
     uint256 initialTotalSupplyShares = virtualTotalSupplyShares(id);
-    uint256 owedAssets = mathLibMulDivDown(initialShares, initialTotalSupply, initialTotalSupplyShares);
+    uint256 owedAssets = libMulDivDown(initialShares, initialTotalSupply, initialTotalSupplyShares);
 
     uint256 withdrawnAssets;
     withdrawnAssets, _ = withdraw(e, marketParams, assets, shares, onBehalf, receiver);
@@ -37,7 +37,7 @@ rule withdrawLiquidity(MorphoHarness.MarketParams marketParams, uint256 assets,
 // 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) {
     env e;
-    MorphoHarness.Id id = marketId(marketParams);
+    MorphoHarness.Id id = libId(marketParams);
 
     uint256 initialCollateral = collateral(id, onBehalf);
 
@@ -49,14 +49,14 @@ rule withdrawCollateralLiquidity(MorphoHarness.MarketParams marketParams, uint25
 // Check than when repaying the full outstanding debt requires more assets than what was borrowed.
 rule repayLiquidity(MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) {
     env e;
-    MorphoHarness.Id id = marketId(marketParams);
+    MorphoHarness.Id id = libId(marketParams);
 
     require lastUpdate(id) == e.block.timestamp;
 
     uint256 initialShares = borrowShares(id, onBehalf);
     uint256 initialTotalBorrow = virtualTotalBorrowAssets(id);
     uint256 initialTotalBorrowShares = virtualTotalBorrowShares(id);
-    uint256 assetsDue = mathLibMulDivUp(initialShares, initialTotalBorrow, initialTotalBorrowShares);
+    uint256 assetsDue = libMulDivUp(initialShares, initialTotalBorrow, initialTotalBorrowShares);
 
     uint256 repaidAssets;
     repaidAssets, _ = repay(e, marketParams, assets, shares, onBehalf, data);

certora/specs/Health.spec

@@ -7,7 +7,7 @@ methods {
     function collateral(MorphoHarness.Id, address) external returns uint256 envfree;
     function isHealthy(MorphoHarness.MarketParams, address user) external returns bool envfree;
     function isAuthorized(address, address user) external returns bool envfree;
-    function marketId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;
+    function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;
 
     function _.price() external => mockPrice() expect uint256;
     function MathLib.mulDivDown(uint256 a, uint256 b, uint256 c) internal returns uint256 => summaryMulDivDown(a,b,c);
@@ -52,7 +52,7 @@ filtered {
 }
 {
     MorphoHarness.MarketParams marketParams;
-    MorphoHarness.Id id = marketId(marketParams);
+    MorphoHarness.Id id = libId(marketParams);
     address user;
 
     // Require that the position is healthy before the interaction.
@@ -78,7 +78,7 @@ rule healthyUserCannotLoseCollateral(env e, method f, calldataarg data)
 filtered { f -> !f.isView }
 {
     MorphoHarness.MarketParams marketParams;
-    MorphoHarness.Id id = marketId(marketParams);
+    MorphoHarness.Id id = libId(marketParams);
     address user;
 
     // Require that the e.msg.sender is not authorized.

certora/specs/LibSummary.spec

@@ -1,26 +1,26 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 methods {
     function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE(true);
-    function mathLibMulDivUp(uint256, uint256, uint256) external returns uint256 envfree;
-    function mathLibMulDivDown(uint256, uint256, uint256) external returns uint256 envfree;
-    function marketId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;
-    function marketLibId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;
+    function libMulDivUp(uint256, uint256, uint256) external returns uint256 envfree;
+    function libMulDivDown(uint256, uint256, uint256) external returns uint256 envfree;
+    function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;
+    function optimizedId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;
 }
 
 // Check the summary of mulDivUp required by RatioMath.spec
 rule checkSummaryMulDivUp(uint256 x, uint256 y, uint256 d) {
-    uint256 result = mathLibMulDivUp(x, y, d);
+    uint256 result = libMulDivUp(x, y, d);
     assert result * d >= x * y;
 }
 
 // Check the summary of mulDivDown required by RatioMath.spec
 rule checkSummaryMulDivDown(uint256 x, uint256 y, uint256 d) {
-    uint256 result = mathLibMulDivDown(x, y, d);
+    uint256 result = libMulDivDown(x, y, d);
     assert result * d <= x * y;
 }
 
 // Check the munging of the MarketParams.id function.
 // This rule cannot be checked because it is not possible disable the keccak256 summary for the moment.
 // rule checkSummaryId(MorphoHarness.MarketParams marketParams) {
-//     assert marketLibId(marketParams) == marketId(marketParams);
+//     assert optimizedId(marketParams) == libId(marketParams);
 // }