[Certora] Exit liquidity

.github/workflows/certora.yml

@@ -43,3 +43,4 @@ jobs:
         script:
           - verifyBlue.sh
           - verifyBlueRatioMathSummary.sh
+          - verifyBlueExitLiquidity.sh

certora/harness/MorphoHarness.sol

@@ -17,6 +17,14 @@ contract MorphoHarness is Morpho {
         return totalSupplyShares[id] + SharesMathLib.VIRTUAL_SHARES;
     }
 
+    function getVirtualTotalBorrow(Id id) external view returns (uint256) {
+        return totalBorrow[id] + SharesMathLib.VIRTUAL_ASSETS;
+    }
+
+    function getVirtualTotalBorrowShares(Id id) external view returns (uint256) {
+        return totalBorrowShares[id] + SharesMathLib.VIRTUAL_SHARES;
+    }
+
     function getMarketId(Market memory market) external pure returns (Id) {
         return market.id();
     }

certora/scripts/verifyBlueExitLiquidity.sh

@@ -0,0 +1,12 @@
+#!/bin/bash
+
+set -euxo pipefail
+
+certoraRun \
+    certora/harness/MorphoHarness.sol \
+    --verify MorphoHarness:certora/specs/BlueExitLiquidity.spec \
+    --solc_allow_path src \
+    --loop_iter 3 \
+    --optimistic_loop \
+    --msg "Morpho Blue Exit Liquidity" \
+    "$@"

certora/specs/BlueExitLiquidity.spec

@@ -0,0 +1,62 @@
+methods {
+    function supplyShares(MorphoHarness.Id, address) external returns uint256 envfree;
+    function getVirtualTotalSupply(MorphoHarness.Id) external returns uint256 envfree;
+    function getVirtualTotalSupplyShares(MorphoHarness.Id) external returns uint256 envfree;
+    function borrowShares(MorphoHarness.Id, address) external returns uint256 envfree;
+    function getVirtualTotalBorrow(MorphoHarness.Id) external returns uint256 envfree;
+    function getVirtualTotalBorrowShares(MorphoHarness.Id) external returns uint256 envfree;
+    function collateral(MorphoHarness.Id, address) external returns uint256 envfree;
+
+    function lastUpdate(MorphoHarness.Id) external returns uint256 envfree;
+
+    function mathLibMulDivDown(uint256, uint256, uint256) external returns uint256 envfree;
+    function mathLibMulDivUp(uint256, uint256, uint256) external returns uint256 envfree;
+    function getMarketId(MorphoHarness.Market) external returns MorphoHarness.Id envfree;
+}
+
+rule withdrawLiquidity(MorphoHarness.Market market, uint256 assets, uint256 shares, address onBehalf, address receiver) {
+    env e;
+    MorphoHarness.Id id = getMarketId(market);
+
+    require lastUpdate(id) == e.block.timestamp;
+
+    uint256 initialShares = supplyShares(id, onBehalf);
+    uint256 initialTotalSupply = getVirtualTotalSupply(id);
+    uint256 initialTotalSupplyShares = getVirtualTotalSupplyShares(id);
+    uint256 owedAssets = mathLibMulDivDown(initialShares, initialTotalSupply, initialTotalSupplyShares);
+
+    uint256 withdrawnAssets;
+    withdrawnAssets, _ = withdraw(e, market, assets, shares, onBehalf, receiver);
+
+    assert withdrawnAssets <= owedAssets;
+}
+
+rule withdrawCollateralLiquidity(MorphoHarness.Market market, uint256 assets, address onBehalf, address receiver) {
+    env e;
+    MorphoHarness.Id id = getMarketId(market);
+
+    uint256 initialCollateral = collateral(id, onBehalf);
+
+    withdrawCollateral(e, market, assets, onBehalf, receiver);
+
+    assert assets <= initialCollateral;
+}
+
+rule repayLiquidity(MorphoHarness.Market market, uint256 assets, uint256 shares, address onBehalf, bytes data) {
+    env e;
+    MorphoHarness.Id id = getMarketId(market);
+
+    require lastUpdate(id) == e.block.timestamp;
+
+    uint256 initialShares = borrowShares(id, onBehalf);
+    uint256 initialTotalBorrow = getVirtualTotalBorrow(id);
+    uint256 initialTotalBorrowShares = getVirtualTotalBorrowShares(id);
+    uint256 assetsDue = mathLibMulDivUp(initialShares, initialTotalBorrow, initialTotalBorrowShares);
+
+    uint256 repaidAssets;
+    repaidAssets, _ = repay(e, market, assets, shares, onBehalf, data);
+
+    require borrowShares(id, onBehalf) == 0;
+
+    assert repaidAssets >= assetsDue;
+}