From 17d221d150fd94cf83cb9df013c45068e6a3621f Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Thu, 30 Nov 2023 11:46:29 +0100
Subject: [PATCH] feat: liveness liquidate by passing shares

---
 certora/specs/Liveness.spec | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/certora/specs/Liveness.spec b/certora/specs/Liveness.spec
index 0c3fb3130..198cb8075 100644
--- a/certora/specs/Liveness.spec
+++ b/certora/specs/Liveness.spec
@@ -293,6 +293,15 @@ rule liquidateChangesTokens(env e, MorphoInternalAccess.MarketParams marketParam
     assert liquidityAfter == liquidityBefore + min(repaidAssets, borrowLoanAssetsBefore);
 }
 
+// Check that you can liquidate non-zero tokens by passing shares.
+rule canLiquidateByPassingShares(env e, MorphoInternalAccess.MarketParams marketParams, address borrower, uint256 repaidShares, bytes data) {
+    uint256 seizedAssets;
+    uint256 repaidAssets;
+    seizedAssets, repaidAssets = liquidate(e, marketParams, borrower, 0, repaidShares,  data);
+
+    satisfy seizedAssets != 0 && repaidAssets != 0;
+}
+
 // Check that nonce and authorization are properly updated with calling setAuthorizationWithSig.
 rule setAuthorizationWithSigChangesNonceAndAuthorizes(env e, MorphoInternalAccess.Authorization authorization, MorphoInternalAccess.Signature signature) {
     mathint nonceBefore = nonce(authorization.authorizer);