[Certora] Liquidate buffer

.github/workflows/certora.yml

@@ -23,6 +23,7 @@ jobs:
           - ExchangeRate
           - Health
           - LibSummary
+          - LiquidateBuffer
           - Liveness
           - Reentrancy
           - Reverts

certora/confs/LiquidateBuffer.conf

@@ -0,0 +1,11 @@
+{
+  "files": [
+    "certora/harness/MorphoLiquidateHarness.sol",
+    "certora/harness/Util.sol"
+  ],
+  "solc": "solc-0.8.19",
+  "verify": "MorphoLiquidateHarness:certora/specs/LiquidateBuffer.spec",
+  "rule_sanity": "basic",
+  "server": "production",
+  "msg": "Morpho Blue Liquidate Buffer"
+}

certora/harness/MorphoLiquidateHarness.sol

@@ -0,0 +1,38 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+pragma solidity 0.8.19;
+
+import "./MorphoHarness.sol";
+
+contract MorphoLiquidateHarness is MorphoHarness {
+    using MarketParamsLib for MarketParams;
+    using MathLib for uint256;
+    using SharesMathLib for uint256;
+
+    constructor(address newOwner) MorphoHarness(newOwner) {}
+
+    function liquidateView(
+        MarketParams memory marketParams,
+        uint256 seizedAssets,
+        uint256 repaidShares,
+        uint256 collateralPrice
+    ) external view returns (uint256, uint256, uint256, uint256) {
+        Id id = marketParams.id();
+        uint256 liquidationIncentiveFactor = UtilsLib.min(
+            MAX_LIQUIDATION_INCENTIVE_FACTOR, WAD.wDivDown(WAD - LIQUIDATION_CURSOR.wMulDown(WAD - marketParams.lltv))
+        );
+
+        if (seizedAssets > 0) {
+            uint256 seizedAssetsQuoted = seizedAssets.mulDivUp(collateralPrice, ORACLE_PRICE_SCALE);
+
+            repaidShares = seizedAssetsQuoted.wDivUp(liquidationIncentiveFactor).toSharesUp(
+                market[id].totalBorrowAssets, market[id].totalBorrowShares
+            );
+        } else {
+            seizedAssets = repaidShares.toAssetsDown(market[id].totalBorrowAssets, market[id].totalBorrowShares)
+                .wMulDown(liquidationIncentiveFactor).mulDivDown(ORACLE_PRICE_SCALE, collateralPrice);
+        }
+        uint256 repaidAssets = repaidShares.toAssetsUp(market[id].totalBorrowAssets, market[id].totalBorrowShares);
+
+        return (seizedAssets, repaidShares, repaidAssets, liquidationIncentiveFactor);
+    }
+}

certora/harness/Util.sol

@@ -17,6 +17,10 @@ contract Util {
         return MAX_FEE;
     }
 
+    function oraclePriceScale() external pure returns (uint256) {
+        return ORACLE_PRICE_SCALE;
+    }
+
     function libId(MarketParams memory marketParams) external pure returns (Id) {
         return marketParams.id();
     }

certora/specs/LiquidateBuffer.spec

@@ -0,0 +1,71 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+
+using Util as Util;
+
+methods {
+    function extSloads(bytes32[]) external returns (bytes32[]) => NONDET DELETE;
+
+    function market_(MorphoLiquidateHarness.Id) external returns (MorphoLiquidateHarness.Market) envfree;
+    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;
+
+    function MathLib.mulDivDown(uint256 a, uint256 b, uint256 c) internal returns (uint256) => summaryMulDivDown(a,b,c);
+    function MathLib.mulDivUp(uint256 a, uint256 b, uint256 c) internal returns (uint256) => summaryMulDivUp(a,b,c);
+}
+
+function summaryMulDivUp(uint256 x, uint256 y, uint256 d) returns uint256 {
+    // Todo: why is this require ok ?
+    return require_uint256((x * y + (d - 1)) / d);
+}
+
+function summaryMulDivDown(uint256 x, uint256 y, uint256 d) returns uint256 {
+    // Todo: why is this require ok ?
+    return require_uint256((x * y) / d);
+}
+
+rule liquidateImprovePosition(MorphoLiquidateHarness.MarketParams marketParams, uint256 seizedAssetsInput, uint256 repaidSharesInput) {
+    MorphoLiquidateHarness.Id id = Util.libId(marketParams);
+
+    // TODO: use a fixed price oracle instead of passing it to liquidateView.
+    uint256 collateralPrice;
+    require collateralPrice > 0;
+
+    // TODO: take those directly from the borrower, and manage accrue interest.
+    uint256 borrowerShares;
+    uint256 borrowerCollateral;
+
+    require borrowerShares <= market_(id).totalBorrowShares;
+    uint256 borrowerAssets = summaryMulDivUp(borrowerShares, virtualTotalBorrowAssets(id), virtualTotalBorrowShares(id));
+
+    require (seizedAssetsInput > 0 && repaidSharesInput == 0) || (seizedAssetsInput == 0 && repaidSharesInput > 0);
+
+    uint256 seizedAssets;
+    uint256 repaidShares;
+    uint256 repaidAssets;
+    uint256 lif;
+    (seizedAssets, repaidShares, repaidAssets, lif) = liquidateView(marketParams, seizedAssetsInput, repaidSharesInput, collateralPrice);
+
+    uint256 borrowerCollateralQuoted = summaryMulDivDown(borrowerCollateral, collateralPrice, Util.oraclePriceScale());
+    require summaryMulDivUp(lif, borrowerAssets, Util.wad()) <= borrowerCollateralQuoted;
+    assert borrowerCollateral * collateralPrice * virtualTotalBorrowShares(id) * Util.wad() >= borrowerShares * Util.oraclePriceScale() * virtualTotalBorrowAssets(id) * lif;
+
+    assert repaidShares * Util.oraclePriceScale() * virtualTotalBorrowAssets(id) * lif >= seizedAssets * collateralPrice * virtualTotalBorrowShares(id) * Util.wad();
+
+    uint256 newBorrowerShares = require_uint256(borrowerShares - repaidShares);
+    uint256 newTotalShares = require_uint256(virtualTotalBorrowShares(id) - repaidShares);
+    uint256 newTotalAssets = require_uint256(virtualTotalBorrowAssets(id) - repaidAssets);
+
+    uint256 newBorrowerAssets = summaryMulDivUp(newBorrowerShares, newTotalAssets, newTotalShares);
+    uint256 newBorrowerCollateral = require_uint256(borrowerCollateral - seizedAssets);
+
+    assert repaidShares * borrowerCollateral >= seizedAssets * borrowerShares;
+    assert borrowerShares * newBorrowerCollateral >= newBorrowerShares * borrowerCollateral;
+    assert newTotalShares * virtualTotalBorrowAssets(id) >= newTotalAssets * virtualTotalBorrowShares(id);
+    assert borrowerShares * virtualTotalBorrowAssets(id) * newTotalShares * newBorrowerCollateral >= newBorrowerShares * virtualTotalBorrowShares(id) * newTotalAssets * borrowerCollateral;
+    assert borrowerAssets * newBorrowerCollateral >= newBorrowerAssets * borrowerCollateral;
+}