feat: add equivalent input liquidate rule

certora/specs/AccrueInterest.spec

@@ -3,6 +3,7 @@ methods {
     function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE;
 
     function maxFee() external returns uint256 envfree;
+    function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;
 
     function MathLib.mulDivDown(uint256 a, uint256 b, uint256 c) internal returns uint256 => ghostMulDivDown(a,b,c);
     function MathLib.mulDivUp(uint256 a, uint256 b, uint256 c) internal returns uint256 => ghostMulDivUp(a,b,c);
@@ -136,3 +137,21 @@ filtered {
     assert revert1 <=> revert2;
     assert store1 == store2;
 }
+
+// Checks that the debt input or the colleteral input of the liquidate function lead to the same repaid assets amount.
+rule liquidateEquivalentInputDebtAndInputCollateral(env e, MorphoHarness.MarketParams marketParams, address borrower, uint256 seized, uint256 repaidShares, bytes data) {
+    MorphoHarness.Id id = libId(marketParams);
+
+    storage init = lastStorage;
+
+    uint256 seizedAssets1;
+    uint256 repaidAssets1;
+    seizedAssets1, repaidAssets1 = liquidate(e, marketParams, borrower, 0, repaidShares, data);
+
+    uint256 seizedAssets2;
+    uint256 repaidAssets2;
+    seizedAssets2, repaidAssets2 = liquidate(e, marketParams, borrower, seizedAssets1, 0, data) at init;
+
+    assert seizedAssets1 == seizedAssets2;
+    assert repaidAssets1 == repaidAssets2;
+}

certora/specs/Health.spec

@@ -106,3 +106,24 @@ 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 the debt input or the colleteral input of the liquidate function lead to the same repaid assets amount.
+rule liquidateEquivalentInputDebtAndInputCollateral(env e, MorphoHarness.MarketParams marketParams, address borrower, uint256 seized, uint256 repaidShares, bytes data) {
+    MorphoHarness.Id id = libId(marketParams);
+
+    storage init = lastStorage;
+
+    uint256 seizedAssets1;
+    uint256 repaidAssets1;
+    seizedAssets1, repaidAssets1 = liquidate(e, marketParams, borrower, 0, repaidShares, data);
+
+    uint256 seizedAssets2;
+    uint256 repaidAssets2;
+    seizedAssets2, repaidAssets2 = liquidate(e, marketParams, borrower, seizedAssets1, 0, data) at init;
+
+    // Assume same context, including the oracle answer.
+    require !priceChanged;
+
+    assert seizedAssets1 == seizedAssets2;
+    assert repaidAssets1 == repaidAssets2;
+}