[Certora] Equivalent input of liquidate

certora/confs/AccrueInterest.conf

@@ -1,12 +1,12 @@
 {
     "files": [
-        "certora/harness/MorphoHarness.sol"
+        "certora/harness/MorphoHarness.sol",
     ],
     "verify": "MorphoHarness:certora/specs/AccrueInterest.spec",
     "prover_args": [
         "-depth 3",
         "-smt_hashingScheme plaininjectivity",
-        "-mediumTimeout 30"
+        "-mediumTimeout 30",
     ],
     "rule_sanity": "basic",
     "server": "production",

certora/confs/AssetsAccounting.conf

@@ -1,6 +1,6 @@
 {
     "files": [
-        "certora/harness/MorphoHarness.sol"
+        "certora/harness/MorphoHarness.sol",
     ],
     "verify": "MorphoHarness:certora/specs/AssetsAccounting.spec",
     "rule_sanity": "basic",

certora/confs/ConsistentState.conf

@@ -1,6 +1,6 @@
 {
     "files": [
-        "certora/harness/MorphoHarness.sol"
+        "certora/harness/MorphoHarness.sol",
     ],
     "verify": "MorphoHarness:certora/specs/ConsistentState.spec",
     "rule_sanity": "basic",

certora/confs/ExactMath.conf

@@ -1,12 +1,13 @@
 {
     "files": [
-        "certora/harness/MorphoHarness.sol"
+        "certora/harness/MorphoHarness.sol",
     ],
     "verify": "MorphoHarness:certora/specs/ExactMath.spec",
     "rule_sanity": "basic",
     "prover_args": [
+        "-depth 3",
         "-smt_hashingScheme plaininjectivity",
-        "-mediumTimeout 30"
+        "-mediumTimeout 30",
     ],
     "server": "production",
     "msg": "Morpho Blue Exact Math"

certora/confs/Health.conf

@@ -6,7 +6,7 @@
     "verify": "MorphoHarness:certora/specs/Health.spec",
     "rule_sanity": "basic",
     "prover_args": [
-        "-smt_hashingScheme plaininjectivity"
+        "-smt_hashingScheme plaininjectivity",
     ],
     "server": "production",
     "msg": "Morpho Blue Health"

certora/confs/LibSummary.conf

@@ -1,6 +1,6 @@
 {
     "files": [
-        "certora/harness/MorphoHarness.sol"
+        "certora/harness/MorphoHarness.sol",
     ],
     "verify": "MorphoHarness:certora/specs/LibSummary.spec",
     "rule_sanity": "basic",

certora/confs/Liveness.conf

@@ -1,6 +1,6 @@
 {
     "files": [
-        "certora/harness/MorphoInternalAccess.sol"
+        "certora/harness/MorphoInternalAccess.sol",
     ],
     "verify": "MorphoInternalAccess:certora/specs/Liveness.spec",
     "rule_sanity": "basic",

certora/confs/RatioMath.conf

@@ -1,13 +1,13 @@
 {
     "files": [
-        "certora/harness/MorphoHarness.sol"
+        "certora/harness/MorphoHarness.sol",
     ],
     "verify": "MorphoHarness:certora/specs/RatioMath.spec",
     "rule_sanity": "basic",
     "prover_args": [
         "-smt_hashingScheme plaininjectivity",
         "-mediumTimeout 30",
-        "-timeout 3600"
+        "-timeout 3600",
     ],
     "server": "production",
     "msg": "Morpho Blue Ratio Math"

certora/confs/Reentrancy.conf

@@ -1,11 +1,11 @@
 {
     "files": [
-        "certora/harness/MorphoHarness.sol"
+        "certora/harness/MorphoHarness.sol",
     ],
     "verify": "MorphoHarness:certora/specs/Reentrancy.spec",
     "rule_sanity": "basic",
     "prover_args": [
-        "-enableStorageSplitting false"
+        "-enableStorageSplitting false",
     ],
     "server": "production",
     "msg": "Morpho Blue Reentrancy"

certora/confs/Reverts.conf

@@ -1,6 +1,6 @@
 {
     "files": [
-        "certora/harness/MorphoHarness.sol"
+        "certora/harness/MorphoHarness.sol",
     ],
     "verify": "MorphoHarness:certora/specs/Reverts.spec",
     "rule_sanity": "basic",

certora/confs/Transfer.conf

@@ -3,7 +3,7 @@
         "certora/harness/TransferHarness.sol",
         "certora/dispatch/ERC20Standard.sol",
         "certora/dispatch/ERC20USDT.sol",
-        "certora/dispatch/ERC20NoRevert.sol"
+        "certora/dispatch/ERC20NoRevert.sol",
     ],
     "verify": "TransferHarness:certora/specs/Transfer.spec",
     "rule_sanity": "basic",

certora/specs/Health.spec

@@ -7,6 +7,7 @@ methods {
     function borrowShares(MorphoHarness.Id, address) external returns uint256 envfree;
     function collateral(MorphoHarness.Id, address) external returns uint256 envfree;
     function isAuthorized(address, address user) external returns bool envfree;
+    function lastUpdate(MorphoHarness.Id) external returns uint256 envfree;
 
     function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;
     function isHealthy(MorphoHarness.MarketParams, address user) external returns bool envfree;
@@ -21,12 +22,12 @@ persistent ghost uint256 lastPrice;
 persistent ghost bool priceChanged;
 
 function mockPrice() returns uint256 {
-    uint256 somePrice;
-    if (somePrice != lastPrice) {
+    uint256 updatedPrice;
+    if (updatedPrice != lastPrice) {
         priceChanged = true;
-        lastPrice = somePrice;
+        lastPrice = updatedPrice;
     }
-    return somePrice;
+    return updatedPrice;
 }
 
 function summaryMulDivUp(uint256 x, uint256 y, uint256 d) returns uint256 {
@@ -106,3 +107,28 @@ filtered { f -> !f.isView }
 // This invariant ensures that bad debt realization cannot be bypassed.
 invariant alwaysCollateralized(MorphoHarness.Id id, address borrower)
     borrowShares(id, borrower) != 0 => collateral(id, borrower) != 0;
+
+// Checks that passing a seized amount input to liquidate leads to repaid shares S and repaid amount A such that liquidating instead with shares S also repays the amount A.
+rule liquidateEquivalentInputDebtAndInputCollateral(env e, MorphoHarness.MarketParams marketParams, address borrower, uint256 seizedAssets, bytes data) {
+    MorphoHarness.Id id = libId(marketParams);
+
+    // Assume no interest accrual to ease the verification.
+    require lastUpdate(id) == e.block.timestamp;
+
+    storage init = lastStorage;
+    uint256 sharesBefore = borrowShares(id, borrower);
+
+    uint256 repaidAssets1;
+    _, repaidAssets1 = liquidate(e, marketParams, borrower, seizedAssets, 0, data);
+    require !priceChanged;
+    // Omit the bad debt realization case.
+    require collateral(id, borrower) != 0;
+    uint256 sharesAfter = borrowShares(id, borrower);
+    uint256 repaidShares1 = assert_uint256(sharesBefore - sharesAfter);
+
+    uint256 repaidAssets2;
+    _, repaidAssets2 = liquidate(e, marketParams, borrower, 0, repaidShares1, data) at init;
+    require !priceChanged;
+
+    assert repaidAssets1 == repaidAssets2;
+}