[Certora] Add README

certora/README.md

@@ -0,0 +1,44 @@
+This folder defines the verification of the Morpho Blue protocol using CVL, Certora's verification language.
+
+## High level description
+
+The Morpho Blue protocol relies on a few different concepts that are described below. Those concepts have been verified using CVL, see the description of the specification files (or those files directly) for more details.
+
+The Morpho Blue protocol allows to take collateralized loans on ERC20 tokens. Transfers of tokens are verified to behave as expected, notably for the most common implementations.\
+Supplying on Morpho Blue entails to some interest, and this is implemented using the share mechanism. Notably, shares can increase in value when accruing interest. What is not borrowed stays on the contract.\
+Borrowing on Morpho Blue requires to deposit collateral. This collateral stays idle, and participates to the liquidity of the contract.\
+Markets on Morpho Blue depend on a pair of assets: the borrowable asset that is supplied and borrowed, and the collateral asset that is needed to be able to take a borrow position. Markets are sound, independent, and positions of users are also independent. In particular, loans cannot be impacted by loans from other markets.\
+To ensure proper collateralization, a liquidation system is put in place. It is verified that no unhealthy position can be created in a given block.\
+Morpho Blue also defines an authorization system that is sound: a user cannot modify the position of another user without the proper authorization (except when liquidating).\
+Other safety properties are verified, notably about reentrancy attacks and about input validation and revert conditions.\
+Other liveness properties are verified, notably it is always possible to exit a position, without concern for the external contracts such as the oracle.
+
+## Folder and files structure
+
+The [`certora/specs`](./specs) folder contains the following files:
+
+- [`AccrueInterest.spec`](./specs/AccrueInterest.spec), checking that the main functions accrue interest at the start of the interaction. This is done by making sure that accruing interest before calling the function does not change the outcome. View functions do not necessarily respect this property (for example `totalSupplyShares`), and are filtered out.
+- [`ConsistentState.spec`](./specs/ConsistentState.spec), checking 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), checking precise properties when taking into account the exact multiplication and division. Notably, this file specifies that doing using supply and withdraw in the same block cannot yield more funds than at the start.
+- [`ExitLiquidity.spec`](./specs/ExitLiquidity.spec), checking that when exiting a position with witdraw, withdrawCollateral or repay, the user cannot get more than what was owed.
+- [`Health.spec`](./specs/Health.spec), checking properties about the health of the positions. Notably, functions cannot render an account unhealthy, and debt positions at least have some collateral.
+- [`LibSummary.spec`](./specs/LibSummary.spec), checking the summarization of the library functions that are used in other specification files.
+- [`Liveness.spec`](./specs/Liveness.spec), checking 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), checking that the ratio between shares and assets evolves predictably over time.
+- [`Reentrancy.spec`](./specs/Reentrancy.spec), checking that the contract is immune to a particular class of reentrancy issues.
+- [`Reverts.spec`](./specs/Reverts.spec), checking the condition for reverts and that inputs are correctly validated.
+- [`Transfer.spec`](./specs/Transfer.spec), checking 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 to handle the fact that library functions should be called from a contract to be verified independently, and it allows to define needed getters.
+
+The [`certora/dispatch`](./dispatch/) folder contains different contracts similar to contracts that are expected to be called from Morpho Blue.
+
+## Usage
+
+Verify specification files by running the corresponding script in the [`certora/scripts`](./scripts/) folder. You can pass arguments to the script, which notable 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);
 // }