Merge remote-tracking branch 'origin/style/constructor-readability' i…

…nto feat/lif-restriction

.github/workflows/certora.yml

@@ -17,6 +17,7 @@ jobs:
       matrix:
         conf:
           - Immutability
+          - Liveness
           - Reentrancy
 
     steps:

certora/README.md

@@ -1,34 +1,22 @@
 # Pre-liquidation Contract Formal Verification
 
-This folder contains the
-[CVL](https://docs.certora.com/en/latest/docs/cvl/index.html)
-specification and verification setup for the
-[pre-liquidation](../src/PreLiquidation.sol) contract using the
-[Certora Prover](https://www.certora.com/).
+This folder contains the [CVL](https://docs.certora.com/en/latest/docs/cvl/index.html) specification and verification setup for the [PreLiquidation](../src/PreLiquidation.sol) contract.
 
 ## Getting Started
 
-This project depends on two different versions of
-[Solidity](https://soliditylang.org/) which are required for running
-the verification. The compiler binaries should be available under the
-following path names:
+This project depends on two different versions of [Solidity](https://soliditylang.org/) which are required for running the verification.
+The compiler binaries should be available under the following path names:
 
-  - `solc-0.8.19` for the solidity compiler version `0.8.19`, which is
-    used for `Morpho`;
-  - `solc-0.8.27` for the solidity compiler version `0.8.27`, which is
-    used for `PreLiquidation`.
+- `solc-0.8.19` for the solidity compiler version `0.8.19`, which is used for `Morpho`;
+- `solc-0.8.27` for the solidity compiler version `0.8.27`, which is used for `PreLiquidation`.
 
-To verifying a specification, run the command `certoraRun Spec.conf`
-where `Spec.conf` is the configuration file of the matching CVL
-specification. Configuration files are available in
-[`certora/conf`](./confs). Please ensure that `CERTORAKEY` is set up
-in your environment.
+To verify a specification, run the command `certoraRun Spec.conf`where `Spec.conf` is the configuration file of the matching CVL specification.
+Configuration files are available in [`certora/confs`](confs).
+Please ensure that `CERTORAKEY` is set up in your environment.
 
 ## Overview
 
-The PreLiquidation contract enables Morpho Blue borrowers to set up a
-safer liquidation plan on a given position, thus preventing undesired
-liquidations.
+The PreLiquidation contract enables Morpho borrowers to set up a safer liquidation plan on a given position, thus preventing undesired liquidations.
 
 ### Reentrancy
 
@@ -38,28 +26,23 @@ This is checked in [`Reentrancy.spec`](specs/Reentrancy.spec).
 
 This is checked in [`Immutability.spec`](specs/Immutability.spec).
 
+### Liveness properties
+
+This is checked in [`Liveness.spec`](specs/Liveness.spec).
+
 ## Verification architecture
 
 ### Folders and file structure
 
 The [`certora/specs`](specs) folder contains the following files:
 
-- [`Reentrancy.spec`](specs/Reentrancy.spec) checks that
-  PreLiquidation is reentrancy safe by checking that the storage is never
-  used.
-
-- [`Immutability.spec`](specs/Immutability.spec) checks that
-  PreLiquidation contract is immutable because it doesn't perform any
-  delegate call.
-
-The [`certora/confs`](confs) folder contains a configuration file for
-each corresponding specification file.
+- [`Reentrancy.spec`](specs/Reentrancy.spec) checks that PreLiquidation is reentrancy safe by checking that the storage is never used;
+- [`Immutability.spec`](specs/Immutability.spec) checks that PreLiquidation contract is immutable because it doesn't perform any delegate call;
+- [`Liveness.spec`](specs/Liveness.spec) ensure that expected computations will always be performed.
+  For instance, pre-liquidations will always trigger a repay operation.
+  We also check that pre-liquidation can successfully be performed by passing shares to be repaid instead of the collateral ammount to be seized.
 
-The [`certora/helpers`](helpers) folder contains helper contracts that
-enable the verification of PreLiquidation. 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/confs`](confs) folder contains a configuration file for each corresponding specification file.
 
 ## TODO
 

certora/confs/Immutability.conf

@@ -1,16 +1,16 @@
 {
-    "files": [
-        "src/PreLiquidation.sol",
-    ],
-    "solc": "solc-0.8.27",
-    "solc_via_ir" : true,
-    "verify": "PreLiquidation:certora/specs/Immutability.spec",
-    "prover_args": [
-        "-depth 3",
-        "-mediumTimeout 20",
-        "-timeout 120",
-    ],
-    "rule_sanity": "basic",
-    "server": "production",
-    "msg": "PreLiquidation Immutability",
+  "files": [
+    "src/PreLiquidation.sol"
+  ],
+  "solc": "solc-0.8.27",
+  "solc_via_ir": true,
+  "verify": "PreLiquidation:certora/specs/Immutability.spec",
+  "prover_args": [
+    "-depth 3",
+    "-mediumTimeout 20",
+    "-timeout 120"
+  ],
+  "rule_sanity": "basic",
+  "server": "production",
+  "msg": "PreLiquidation Immutability"
 }

certora/confs/Liveness.conf

@@ -0,0 +1,31 @@
+{
+  "files": [
+    "src/PreLiquidation.sol",
+    "lib/morpho-blue/src/Morpho.sol"
+  ],
+  "link": [
+    "PreLiquidation:MORPHO=Morpho"
+  ],
+  "parametric_contracts": [
+    "PreLiquidation"
+  ],
+  "solc_via_ir": true,
+  "verify": "PreLiquidation:certora/specs/Liveness.spec",
+  "solc_optimize_map": {
+    "Morpho": "99999",
+    "PreLiquidation": "99999"
+  },
+  "solc_map": {
+    "Morpho": "solc-0.8.19",
+    "PreLiquidation": "solc-0.8.27"
+  },
+  "prover_args": [
+    "-depth 3",
+    "-mediumTimeout 20",
+    "-timeout 120",
+    "-smt_nonLinearArithmetic true"
+  ],
+  "rule_sanity": "basic",
+  "server": "production",
+  "msg": "PreLiquidation Liveness"
+}

certora/confs/Reentrancy.conf

@@ -1,17 +1,17 @@
 {
-    "files": [
-        "src/PreLiquidation.sol",
-    ],
-    "solc": "solc-0.8.27",
-    "solc_via_ir" : true,
-    "verify": "PreLiquidation:certora/specs/Reentrancy.spec",
-    "prover_args": [
-        "-enableStorageSplitting false",
-        "-depth 3",
-        "-mediumTimeout 20",
-        "-timeout 120",
-    ],
-    "rule_sanity": "basic",
-    "server": "production",
-    "msg": "PreLiquidation Reentrancy",
+  "files": [
+    "src/PreLiquidation.sol"
+  ],
+  "solc": "solc-0.8.27",
+  "solc_via_ir": true,
+  "verify": "PreLiquidation:certora/specs/Reentrancy.spec",
+  "prover_args": [
+    "-enableStorageSplitting false",
+    "-depth 3",
+    "-mediumTimeout 20",
+    "-timeout 120"
+  ],
+  "rule_sanity": "basic",
+  "server": "production",
+  "msg": "PreLiquidation Reentrancy"
 }

certora/specs/Liveness.spec

@@ -0,0 +1,56 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+
+// True when `preLiquidate` has been called.
+persistent ghost bool preLiquidateCalled;
+
+// True when `onMorphoRepay` has been called.
+persistent ghost bool onMorphoRepayCalled;
+
+hook CALL(uint g, address addr, uint value, uint argsOffset, uint argsLength, uint retOffset, uint retLength) uint rc {
+    if (selector == sig:preLiquidate(address, uint256, uint256, bytes).selector) {
+       preLiquidateCalled = true;
+    } else if (selector == sig:onMorphoRepay(uint256, bytes).selector) {
+       onMorphoRepayCalled = true;
+    }
+}
+
+// Check that pre-liquidations happen if and only if `onMorphoRepay` is called.
+rule preLiquidateRepays(method f, env e, calldataarg data) {
+
+    // Set up the initial state.
+    require !preLiquidateCalled;
+    require !onMorphoRepayCalled;
+
+    // Safe require because Morpho cannot send transactions.
+    require e.msg.sender != currentContract.MORPHO;
+
+
+    // Capture the first method call which is not performed with a CALL opcode.
+    if (f.selector == sig:preLiquidate(address, uint256, uint256, bytes).selector) {
+       preLiquidateCalled = true;
+    } else if (f.selector == sig:onMorphoRepay(uint256, bytes).selector) {
+       onMorphoRepayCalled = true;
+    }
+
+    f@withrevert(e,data);
+
+    // Avoid failing vacuity checks, either the proposition is true or the execution reverts.
+    assert !lastReverted => (preLiquidateCalled <=> onMorphoRepayCalled);
+}
+
+// Check that you can pre-liquidate non-zero tokens by passing shares.
+rule canPreLiquidateByPassingShares(env e, address borrower, uint256 repaidShares, bytes data) {
+    uint256 seizedAssets;
+    uint256 repaidAssets;
+    seizedAssets, repaidAssets = preLiquidate(e, borrower, 0, repaidShares,  data);
+
+    satisfy seizedAssets != 0 && repaidAssets != 0;
+}
+
+// Check that you can pre-liquidate non-zero tokens by passing seized assets.
+rule canPreLiquidateByPassingSeizedAssets(env e, address borrower, uint256 seizedAssets, bytes data) {
+    uint256 repaidAssets;
+    _, repaidAssets = preLiquidate(e, borrower, seizedAssets, 0,  data);
+
+    satisfy repaidAssets != 0;
+}

certora/specs/Reentrancy.spec

@@ -1,7 +1,5 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 
-
-
 // True when storage has been accessed with either a SSTORE or a SLOAD.
 persistent ghost bool hasAccessedStorage;
 

foundry.toml

@@ -8,4 +8,6 @@ optimizer_runs = 999999 # Etherscan does not support verifying contracts with mo
 [profile.default.fmt]
 wrap_comments = true
 
+[fuzz]
+runs = 10_000
 # See more config options https://github.com/foundry-rs/foundry/blob/master/crates/config/README.md#all-options

src/PreLiquidation.sol

@@ -106,7 +106,7 @@ contract PreLiquidation is IPreLiquidation, IMorphoRepayCallback {
         PRE_LIF_2 = _preLiquidationParams.preLIF2;
         PRE_LIQUIDATION_ORACLE = _preLiquidationParams.preLiquidationOracle;
 
-        ERC20(LOAN_TOKEN).safeApprove(morpho, type(uint256).max);
+        ERC20(_marketParams.loanToken).safeApprove(morpho, type(uint256).max);
     }
 
     /* PRE-LIQUIDATION */

test/BaseTest.sol

@@ -9,15 +9,18 @@ import {IrmMock} from "../src/mocks/IrmMock.sol";
 import {OracleMock} from "../src/mocks/OracleMock.sol";
 
 import {MarketParams, IMorpho, Id} from "../lib/morpho-blue/src/interfaces/IMorpho.sol";
+import {IOracle} from "../lib/morpho-blue/src/interfaces/IOracle.sol";
 import {MarketParamsLib} from "../lib/morpho-blue/src/libraries/MarketParamsLib.sol";
 import {ORACLE_PRICE_SCALE} from "../lib/morpho-blue/src/libraries/ConstantsLib.sol";
 import {WAD, MathLib} from "../lib/morpho-blue/src/libraries/MathLib.sol";
 import {UtilsLib} from "../lib/morpho-blue/src/libraries/UtilsLib.sol";
 
-import {PreLiquidationParams} from "../src/interfaces/IPreLiquidation.sol";
+import {PreLiquidationParams, IPreLiquidation} from "../src/interfaces/IPreLiquidation.sol";
+import {PreLiquidationFactory} from "../src/PreLiquidationFactory.sol";
 
 contract BaseTest is Test {
     using MarketParamsLib for MarketParams;
+    using MathLib for uint256;
 
     address internal SUPPLIER = makeAddr("Supplier");
     address internal BORROWER = makeAddr("Borrower");
@@ -35,6 +38,12 @@ contract BaseTest is Test {
     MarketParams internal marketParams;
     Id internal id;
 
+    uint256 internal minCollateral = 10 ** 18;
+    uint256 internal maxCollateral = 10 ** 24;
+
+    PreLiquidationFactory internal factory;
+    IPreLiquidation internal preLiquidation;
+
     function setUp() public virtual {
         vm.label(address(MORPHO), "Morpho");
         vm.label(address(loanToken), "Loan");
@@ -91,4 +100,69 @@ contract BaseTest is Test {
 
         return preLiquidationParams;
     }
+
+    function _preparePreLiquidation(
+        PreLiquidationParams memory preLiquidationParams,
+        uint256 collateralAmount,
+        uint256 borrowAmount,
+        address liquidator
+    ) internal {
+        preLiquidation = factory.createPreLiquidation(id, preLiquidationParams);
+
+        loanToken.mint(SUPPLIER, borrowAmount);
+        vm.prank(SUPPLIER);
+        if (borrowAmount > 0) {
+            MORPHO.supply(marketParams, borrowAmount, 0, SUPPLIER, hex"");
+        }
+
+        collateralToken.mint(BORROWER, collateralAmount);
+        vm.startPrank(BORROWER);
+
+        MORPHO.supplyCollateral(marketParams, collateralAmount, BORROWER, hex"");
+
+        if (borrowAmount > 0) {
+            MORPHO.borrow(marketParams, borrowAmount, 0, BORROWER, BORROWER);
+        }
+        MORPHO.setAuthorization(address(preLiquidation), true);
+        vm.stopPrank();
+
+        loanToken.mint(liquidator, type(uint128).max);
+        vm.prank(liquidator);
+        loanToken.approve(address(preLiquidation), type(uint256).max);
+    }
+
+    function _closeFactor(PreLiquidationParams memory preLiquidationParams, uint256 ltv)
+        internal
+        view
+        returns (uint256)
+    {
+        return UtilsLib.min(
+            (ltv - preLiquidationParams.preLltv).wDivDown(marketParams.lltv - preLiquidationParams.preLltv).wMulDown(
+                preLiquidationParams.preLCF2 - preLiquidationParams.preLCF1
+            ) + preLiquidationParams.preLCF1,
+            preLiquidationParams.preLCF2
+        );
+    }
+
+    function _preLIF(PreLiquidationParams memory preLiquidationParams, uint256 ltv) internal view returns (uint256) {
+        return UtilsLib.min(
+            (ltv - preLiquidationParams.preLltv).wDivDown(marketParams.lltv - preLiquidationParams.preLltv).wMulDown(
+                preLiquidationParams.preLIF2 - preLiquidationParams.preLIF1
+            ) + preLiquidationParams.preLIF1,
+            preLiquidationParams.preLIF2
+        );
+    }
+
+    function _getBorrowBounds(
+        PreLiquidationParams memory preLiquidationParams,
+        MarketParams memory _marketParams,
+        uint256 collateralAmount
+    ) internal view returns (uint256, uint256, uint256) {
+        uint256 collateralPrice = IOracle(preLiquidationParams.preLiquidationOracle).price();
+        uint256 collateralQuoted = collateralAmount.mulDivDown(collateralPrice, ORACLE_PRICE_SCALE);
+        uint256 borrowPreLiquidationThreshold = collateralQuoted.wMulDown(preLiquidationParams.preLltv);
+        uint256 borrowLiquidationThreshold = collateralQuoted.wMulDown(_marketParams.lltv);
+
+        return (collateralQuoted, borrowPreLiquidationThreshold, borrowLiquidationThreshold);
+    }
 }