Merge remote-tracking branch 'origin/certora/dev' into certora/via-ir

Author: QGarchery

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/dispatch/ERC20NoRevert.sol

@@ -2,18 +2,12 @@
 pragma solidity ^0.8.0;
 
 contract ERC20NoRevert {
-    string public name;
-    string public symbol;
-    uint256 public decimals;
     address public owner;
     uint256 public totalSupply;
     mapping(address => uint256) public balanceOf;
-    mapping(address => mapping(address => uint256)) public allowed;
+    mapping(address => mapping(address => uint256)) public allowance;
 
-    constructor(string memory _name, string memory _symbol, uint256 _decimals) {
-        name = _name;
-        symbol = _symbol;
-        decimals = _decimals;
+    constructor() {
         owner = msg.sender;
     }
 
@@ -36,19 +30,15 @@ contract ERC20NoRevert {
     }
 
     function transferFrom(address _from, address _to, uint256 _amount) public returns (bool) {
-        if (allowed[_from][msg.sender] < _amount) {
+        if (allowance[_from][msg.sender] < _amount) {
             return false;
         }
-        allowed[_from][msg.sender] -= _amount;
+        allowance[_from][msg.sender] -= _amount;
         return _transfer(_from, _to, _amount);
     }
 
     function approve(address _spender, uint256 _amount) public {
-        allowed[msg.sender][_spender] = _amount;
-    }
-
-    function allowance(address _owner, address _spender) public view returns (uint256 remaining) {
-        return allowed[_owner][_spender];
+        allowance[msg.sender][_spender] = _amount;
     }
 
     function mint(address _receiver, uint256 _amount) public onlyOwner {

certora/dispatch/ERC20USDT.sol

@@ -4,18 +4,12 @@ pragma solidity ^0.8.0;
 contract ERC20USDT {
     uint256 public constant MAX_UINT = 2 ** 256 - 1;
 
-    string public name;
-    string public symbol;
-    uint256 public decimals;
     uint256 public totalSupply;
     address public owner;
     mapping(address => uint256) public balanceOf;
-    mapping(address => mapping(address => uint256)) public allowed;
+    mapping(address => mapping(address => uint256)) public allowance;
 
-    constructor(string memory _name, string memory _symbol, uint256 _decimals) {
-        name = _name;
-        symbol = _symbol;
-        decimals = _decimals;
+    constructor() {
         owner = msg.sender;
     }
 
@@ -34,20 +28,16 @@ contract ERC20USDT {
     }
 
     function transferFrom(address _from, address _to, uint256 _amount) public {
-        if (allowed[_from][msg.sender] < MAX_UINT) {
-            allowed[_from][msg.sender] -= _amount;
+        if (allowance[_from][msg.sender] < MAX_UINT) {
+            allowance[_from][msg.sender] -= _amount;
         }
         _transfer(_from, _to, _amount);
     }
 
     function approve(address _spender, uint256 _amount) public {
-        require(!((_amount != 0) && (allowed[msg.sender][_spender] != 0)));
+        require(!((_amount != 0) && (allowance[msg.sender][_spender] != 0)));
 
-        allowed[msg.sender][_spender] = _amount;
-    }
-
-    function allowance(address _owner, address _spender) public view returns (uint256 remaining) {
-        return allowed[_owner][_spender];
+        allowance[msg.sender][_spender] = _amount;
     }
 
     function mint(address _receiver, uint256 _amount) public onlyOwner {

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/scripts/verifyAccrueInterest.sh

@@ -7,7 +7,6 @@ make -C certora munged
 certoraRun \
     certora/harness/MorphoHarness.sol \
     --verify MorphoHarness:certora/specs/AccrueInterest.spec \
-    --solc_allow_path src \
     --solc_via_ir \
     --solc_optimize 4294967295 \
     --msg "Morpho Blue Accrue Interest" \

certora/scripts/verifyConsistentState.sh

@@ -7,7 +7,6 @@ make -C certora munged
 certoraRun \
     certora/harness/MorphoHarness.sol \
     --verify MorphoHarness:certora/specs/ConsistentState.spec \
-    --solc_allow_path src \
     --solc_via_ir \
     --solc_optimize 4294967295 \
     --msg "Morpho Blue Consistent State" \

certora/scripts/verifyExactMath.sh

@@ -6,10 +6,9 @@ make -C certora munged
 
 certoraRun \
     certora/harness/MorphoHarness.sol \
-    src/mocks/OracleMock.sol \
     --verify MorphoHarness:certora/specs/ExactMath.spec \
     --solc_via_ir \
     --solc_optimize 4294967295 \
-    --prover_args '-smt_hashingScheme plaininjectivity' \
+    --prover_args '-smt_hashingScheme plaininjectivity -mediumTimeout 12' \
     --msg "Morpho Blue Exact Math" \
     "$@"

certora/scripts/verifyExitLiquidity.sh

@@ -7,7 +7,6 @@ make -C certora munged
 certoraRun \
     certora/harness/MorphoHarness.sol \
     --verify MorphoHarness:certora/specs/ExitLiquidity.spec \
-    --solc_allow_path src \
     --solc_via_ir \
     --solc_optimize 4294967295 \
     --msg "Morpho Blue Exit Liquidity" \

certora/scripts/verifyLiveness.sh

@@ -7,7 +7,6 @@ make -C certora munged
 certoraRun \
     certora/harness/MorphoInternalAccess.sol \
     --verify MorphoInternalAccess:certora/specs/Liveness.spec \
-    --solc_allow_path src \
     --solc_via_ir \
     --solc_optimize 4294967295 \
     --msg "Morpho Blue Liveness" \

certora/scripts/verifyRatioMath.sh

@@ -7,7 +7,6 @@ make -C certora munged
 certoraRun \
     certora/harness/MorphoHarness.sol \
     --verify MorphoHarness:certora/specs/RatioMath.spec \
-    --solc_allow_path src \
     --solc_via_ir \
     --solc_optimize 4294967295 \
     --prover_args '-smt_hashingScheme plaininjectivity' \

certora/specs/AccrueInterest.spec

@@ -32,6 +32,7 @@ ghost ghostTransferFrom(address, address, uint256) returns bool;
 // Check that calling accrueInterest first has no effect.
 // This is because supply should call accrueInterest itself.
 rule supplyAccruesInterest(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) {
+    // Safe require because timestamps cannot realistically be that large.
     require e.block.timestamp < 2^128;
 
     storage init = lastStorage;
@@ -49,6 +50,7 @@ rule supplyAccruesInterest(env e, MorphoHarness.MarketParams marketParams, uint2
 // Check that calling accrueInterest first has no effect.
 // This is because withdraw should call accrueInterest itself.
 rule withdrawAccruesInterest(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) {
+    // Safe require because timestamps cannot realistically be that large.
     require e.block.timestamp < 2^128;
 
     storage init = lastStorage;
@@ -66,6 +68,7 @@ rule withdrawAccruesInterest(env e, MorphoHarness.MarketParams marketParams, uin
 // Check that calling accrueInterest first has no effect.
 // This is because borrow should call accrueInterest itself.
 rule borrowAccruesInterest(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) {
+    // Safe require because timestamps cannot realistically be that large.
     require e.block.timestamp < 2^128;
 
     storage init = lastStorage;
@@ -83,6 +86,7 @@ rule borrowAccruesInterest(env e, MorphoHarness.MarketParams marketParams, uint2
 // Check that calling accrueInterest first has no effect.
 // This is because repay should call accrueInterest itself.
 rule repayAccruesInterest(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) {
+    // Safe require because timestamps cannot realistically be that large.
     require e.block.timestamp < 2^128;
 
     storage init = lastStorage;
@@ -111,9 +115,9 @@ filtered {
     env e2;
     MorphoHarness.MarketParams marketParams;
 
-    // Require interactions to happen at the same block.
+    // Assume interactions to happen at the same block.
     require e1.block.timestamp == e2.block.timestamp;
-    // Assumption required to cast a timestamp to uint128.
+    // Safe require because timestamps cannot realistically be that large.
     require e1.block.timestamp < 2^128;
 
     storage init = lastStorage;