From 0f88e1a7f3c01a5aa8bc6843da99feef50932ae5 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Fri, 1 Dec 2023 15:40:19 +0100
Subject: [PATCH] feat: check supply ratio in liquidate without bad debt
 realization

---
 certora/specs/RatioMath.spec | 27 +++++++++++++++++++++++++++
 1 file changed, 27 insertions(+)

diff --git a/certora/specs/RatioMath.spec b/certora/specs/RatioMath.spec
index 2ae82a8bc..1fabb7742 100644
--- a/certora/specs/RatioMath.spec
+++ b/certora/specs/RatioMath.spec
@@ -1,6 +1,8 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 methods {
     function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE;
+
+    function collateral(MorphoHarness.Id, address) external returns uint256 envfree;
     function virtualTotalSupplyAssets(MorphoHarness.Id) external returns uint256 envfree;
     function virtualTotalSupplyShares(MorphoHarness.Id) external returns uint256 envfree;
     function virtualTotalBorrowAssets(MorphoHarness.Id) external returns uint256 envfree;
@@ -100,6 +102,31 @@ filtered {
     assert assetsBefore * sharesAfter <= assetsAfter * sharesBefore;
 }
 
+// Check that when not realizing bad debt in liquidate, the value of supply shares increases.
+rule liquidateWithoutBadDebtRealizationIncreasesSupplyRatio(env e, MorphoHarness.MarketParams marketParams, address borrower, uint256 seizedAssets, uint256 repaidShares, bytes data)
+{
+    MorphoHarness.Id id;
+    requireInvariant feeInRange(id);
+
+    mathint assetsBefore = virtualTotalSupplyAssets(id);
+    mathint sharesBefore = virtualTotalSupplyShares(id);
+
+    // Interest is checked separately by the rules above.
+    // Here we assume interest has already been accumulated for this block.
+    require lastUpdate(id) == e.block.timestamp;
+
+    liquidate(e, marketParams, borrower, seizedAssets, repaidShares, data);
+
+    mathint assetsAfter = virtualTotalSupplyAssets(id);
+    mathint sharesAfter = virtualTotalSupplyShares(id);
+
+    // Trick to ensure that no bad debt realization happened.
+    require collateral(id, borrower) != 0;
+
+    // Check that the ratio increases: assetsBefore/sharesBefore <= assetsAfter / sharesAfter
+    assert assetsBefore * sharesAfter <= assetsAfter * sharesBefore;
+}
+
 // Check that except when not accruing interest, every function is decreasing the value of borrow shares.
 // The repay function is checked separately, see below.
 // The liquidate function is not checked.