From 701d11d14f93bbff1616d12ef3bbabc4e665aaf9 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Fri, 22 Nov 2024 14:35:17 +0100
Subject: [PATCH] feat: start borrower proof

---
 certora/specs/LiquidateBuffer.spec | 26 ++++++++++++++++++--------
 1 file changed, 18 insertions(+), 8 deletions(-)

diff --git a/certora/specs/LiquidateBuffer.spec b/certora/specs/LiquidateBuffer.spec
index fe1f4fa1..2dd46874 100644
--- a/certora/specs/LiquidateBuffer.spec
+++ b/certora/specs/LiquidateBuffer.spec
@@ -3,10 +3,12 @@
 using Util as Util;
 
 methods {
-    function liquidateView(MorphoLiquidateHarness.MarketParams, uint256, uint256, uint256) external returns (uint256, uint256, uint256, uint256) envfree;
-
     function extSloads(bytes32[]) external returns (bytes32[]) => NONDET DELETE;
 
+    function virtualTotalBorrowAssets(MorphoLiquidateHarness.Id) external returns uint256 envfree;
+    function virtualTotalBorrowShares(MorphoLiquidateHarness.Id) external returns uint256 envfree;
+    function liquidateView(MorphoLiquidateHarness.MarketParams, uint256, uint256, uint256) external returns (uint256, uint256, uint256, uint256) envfree;
+
     function Util.wad() external returns (uint256) envfree;
     function Util.libId(MorphoLiquidateHarness.MarketParams) external returns (MorphoLiquidateHarness.Id) envfree;
     function Util.oraclePriceScale() external returns (uint256) envfree;
@@ -26,25 +28,33 @@ function summaryMulDivDown(uint256 x, uint256 y, uint256 d) returns uint256 {
 }
 
 rule liquidateImprovePosition(MorphoLiquidateHarness.MarketParams marketParams, uint256 seizedAssetsInput, uint256 repaidSharesInput) {
-    uint256 collateralPrice;
+    MorphoLiquidateHarness.Id id = Util.libId(marketParams);
 
-    // uint256 borrowerShares;
-    // uint256 borrowerCollateral;
+    // TODO: use a fixed price oracle instead of passing it to liquidateView.
+    uint256 collateralPrice;
 
-    // require borrowerShares < totalShares
-    // require borrowerAssets < totalAssets
+    // TODO: take those directly from the borrower, and manage accrue interest.
+    uint256 borrowerShares;
+    uint256 borrowerCollateral;
 
-    // require LTV < 1 / LIF;
+    require borrowerShares <= market_(id).totalBorrowShares;
+    uint256 borrowerAssets = summaryMulDivUp(borrowerShares, virtualTotalBorrowAssets(id), virtualTotalBorrowShares(id));
+    require borrowerAssets > 0;
 
     require seizedAssetsInput > 0 && repaidSharesInput == 0;
 
     uint256 seizedAssets;
     uint256 repaidShares;
     uint256 repaidAssets;
+    require repaidAssets > 0;
     uint256 lif;
     (seizedAssets, repaidShares, repaidAssets, lif) = liquidateView(marketParams, seizedAssetsInput, repaidSharesInput, collateralPrice);
 
+    require summaryMulDivUp(borrowerCollateral, collateralPrice, Util.oraclePriceScale()) >= summaryMulDivUp(lif, borrowerAssets, Util.wad());
+    assert summaryMulDivDown(summaryMulDivUp(borrowerCollateral, collateralPrice, Util.oraclePriceScale()), Util.wad(), borrowerAssets) >= lif;
+
     assert summaryMulDivDown(lif, repaidAssets, Util.wad()) >= summaryMulDivUp(seizedAssets, collateralPrice, Util.oraclePriceScale());
+    assert lif >= summaryMulDivDown(summaryMulDivUp(seizedAssets, collateralPrice, Util.oraclePriceScale()), Util.wad(), repaidAssets);
 
     // assert repaidShares * borrowerCollateral > seizedAssets * borrowerShares;
 }