[Certora] Remove market liveness (WIP)

.github/workflows/certora.yml

@@ -30,6 +30,7 @@ jobs:
           - Reentrancy
           - ReentrancyView
           - RelativeCaps
+          - RemoveMarketLiveness
           - SentinelLiveness
           - TokensMorphoMarketV1Adapter
           - TokensMorphoVaultV1Adapter

certora/confs/RemoveMarketLiveness.conf

@@ -0,0 +1,35 @@
+{
+  "files": [
+    "src/VaultV2.sol",
+    "src/adapters/MorphoMarketV1Adapter.sol",
+    "lib/morpho-blue/certora/helpers/MorphoHarness.sol",
+    "test/mocks/ERC20Mock.sol",
+    "certora/helpers/Utils.sol"
+  ],
+  "parametric_contracts": [
+    "VaultV2"
+  ],
+  "verify": "VaultV2:certora/specs/RemoveMarketLiveness.spec",
+  "link": [
+    "VaultV2:asset=ERC20Mock",
+    "MorphoMarketV1Adapter:morpho=MorphoHarness",
+    "MorphoMarketV1Adapter:parentVault=VaultV2",
+    "MorphoMarketV1Adapter:asset=ERC20Mock"
+  ],
+  "loop_iter": "3",
+  "optimistic_loop": true,
+  "optimistic_hashing": true,
+  "compiler_map": {
+    "VaultV2": "solc-0.8.28",
+    "MorphoMarketV1Adapter": "solc-0.8.28",
+    "MorphoHarness": "solc-0.8.19",
+    "ERC20Mock": "solc-0.8.28",
+    "Utils": "solc-0.8.28"
+  },
+  "prover_args": [
+    "-depth 5",
+    "-mediumTimeout 20",
+    "-timeout 3600"
+  ],
+  "msg": "Vault V2 Remove Market Liveness"
+}

certora/helpers/Utils.sol

@@ -3,6 +3,7 @@
 pragma solidity 0.8.28;
 
 import "../../src/libraries/ConstantsLib.sol";
+import {MarketParamsLib, MarketParams, MorphoBalancesLib, IMorpho} from "../../src/adapters/MorphoMarketV1Adapter.sol";
 
 interface IReturnFactory {
     function factory() external view returns (address);
@@ -32,4 +33,17 @@ contract Utils {
     function factory(address adapter) external view returns (address) {
         return IReturnFactory(adapter).factory();
     }
+
+    // To remove when chainsec specs are merged.
+    function decodeMarketParams(bytes memory data) external pure returns (MarketParams memory) {
+        return abi.decode(data, (MarketParams));
+    }
+
+    function expectedSupplyAssets(address morpho, MarketParams memory marketParams, address user)
+        external
+        view
+        returns (uint256)
+    {
+        return MorphoBalancesLib.expectedSupplyAssets(IMorpho(morpho), marketParams, user);
+    }
 }

certora/specs/RemoveMarketLiveness.spec

@@ -0,0 +1,69 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+// Copyright (c) 2025 Morpho Association
+
+using MorphoMarketV1Adapter as MorphoMarketV1Adapter;
+using MorphoHarness as Morpho;
+using Utils as Utils;
+
+methods {
+    function _.extSloads(bytes32[]) external => NONDET DELETE;
+    function _.multicall(bytes[] data) external => HAVOC_ALL DELETE;
+    function _.supplyShares(address, Morpho.Id id, address user) internal => summarySupplyShares(id, user) expect uint256;
+
+    function Morpho.supplyShares(Morpho.Id, address) external returns (uint256) envfree;
+    function MorphoMarketV1Adapter.marketParamsListLength() external returns (uint256) envfree;
+    function MorphoMarketV1Adapter.marketParamsList(uint256) external returns (address, address, address, address, uint256) envfree;
+    function Utils.decodeMarketParams(bytes data) external returns (Morpho.MarketParams memory) envfree;
+
+    function _.deallocate(bytes, uint256, bytes4, address) external => DISPATCHER(true);
+
+    // Todo: remove once it's linked to ERC20Mock.
+    function SafeTransferLib.safeTransfer(address, address, uint256) internal => NONDET;
+    function _.borrowRate(Morpho.MarketParams, Morpho.Market) external => ghostBorrowRate expect uint256;
+    function _.borrowRateView(Morpho.MarketParams, Morpho.Market) external => ghostBorrowRate expect uint256;
+
+    function _.market(Morpho.Id) external => DISPATCHER(true);
+}
+
+persistent ghost uint256 ghostBorrowRate;
+
+function summarySupplyShares(Morpho.Id id, address user) returns uint256 {
+    return Morpho.supplyShares(id, user);
+}
+
+rule canRemoveMarket(env e, bytes data) {
+    Morpho.MarketParams marketParams = Utils.decodeMarketParams(data);
+    require Morpho.feeRecipient != MorphoMarketV1Adapter, "sane assumption to simplify the amount of asset to remove";
+    uint256 assets = Utils.expectedSupplyAssets(e, Morpho, marketParams, MorphoMarketV1Adapter);
+
+    uint256 marketParamsListLength = MorphoMarketV1Adapter.marketParamsListLength();
+    require forall uint256 i. forall uint256 j. (i < j && j < marketParamsListLength) => (
+        MorphoMarketV1Adapter.marketParamsList[i].loanToken != MorphoMarketV1Adapter.marketParamsList[j].loanToken ||
+        MorphoMarketV1Adapter.marketParamsList[i].collateralToken != MorphoMarketV1Adapter.marketParamsList[j].collateralToken ||
+        MorphoMarketV1Adapter.marketParamsList[i].oracle != MorphoMarketV1Adapter.marketParamsList[j].oracle ||
+        MorphoMarketV1Adapter.marketParamsList[i].irm != MorphoMarketV1Adapter.marketParamsList[j].irm ||
+        MorphoMarketV1Adapter.marketParamsList[i].lltv != MorphoMarketV1Adapter.marketParamsList[j].lltv
+    ), "see distinctMarketParamsInList";
+
+    // Could also check that the deallocate call doesn't revert.
+    deallocate(e, MorphoMarketV1Adapter, data, assets);
+
+    assert Utils.expectedSupplyAssets(e, Morpho, marketParams, MorphoMarketV1Adapter) == 0;
+
+    uint256 i;
+    // Is this needed ?
+    require i < MorphoMarketV1Adapter.marketParamsListLength();
+    address loanToken;
+    address collateralToken;
+    address oracle;
+    address irm;
+    uint256 lltv;
+    (loanToken, collateralToken, oracle, irm, lltv) = MorphoMarketV1Adapter.marketParamsList(i);
+    assert (
+        loanToken != marketParams.loanToken ||
+        collateralToken != marketParams.collateralToken ||
+        oracle != marketParams.oracle ||
+        irm != marketParams.irm ||
+        lltv != marketParams.lltv
+    );
+}

test/ERC20Test.sol

@@ -18,14 +18,11 @@ contract ERC20Test is BaseTest {
         uint256 deadline;
     }
 
-    function _signPermit(
-        uint256 privateKey,
-        address owner,
-        address to,
-        uint256 shares,
-        uint256 nonce,
-        uint256 deadline
-    ) internal view returns (uint8, bytes32, bytes32) {
+    function _signPermit(uint256 privateKey, address owner, address to, uint256 shares, uint256 nonce, uint256 deadline)
+        internal
+        view
+        returns (uint8, bytes32, bytes32)
+    {
         bytes32 hashStruct = keccak256(abi.encode(PERMIT_TYPEHASH, owner, to, shares, nonce, deadline));
         bytes32 digest = keccak256(abi.encodePacked("\x19\x01", vault.DOMAIN_SEPARATOR(), hashStruct));
         return vm.sign(privateKey, digest);