Merge pull request #72 from morpho-org/colin@verif/pre-liquidate-with…

…-shares

[Certora] Verify pre-liquidate with shares

certora/README.md

@@ -40,6 +40,7 @@ The [`certora/specs`](specs) folder contains the following files:
 - [`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/confs`](confs) folder contains a configuration file for each corresponding specification file.
 

certora/specs/Liveness.spec

@@ -1,11 +1,5 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 
-using PreLiquidation as preLiq;
-
-methods {
-    function preLiq.MORPHO() external returns address envfree;
-}
-
 // True when `preLiquidate` has been called.
 persistent ghost bool preLiquidateCalled;
 
@@ -28,7 +22,8 @@ rule preLiquidateRepays(method f, env e, calldataarg data) {
     require !onMorphoRepayCalled;
 
     // Safe require because Morpho cannot send transactions.
-    require e.msg.sender != preLiq.MORPHO();
+    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) {
@@ -42,3 +37,20 @@ rule preLiquidateRepays(method f, env e, calldataarg 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;
+}