[Certora] Revamp sentinel liveness

.github/workflows/certora.yml

@@ -34,6 +34,8 @@ jobs:
           - PreviewFunctions
           - Reentrancy
           - SentinelLiveness
+          - SentinelLivenessDeallocateMarketV1
+          - SentinelLivenessDeallocateVaultV1
           - TokensMorphoMarketV1Adapter
           - TokensMorphoVaultV1Adapter
           - TokensNoAdapter
@@ -47,7 +49,7 @@ jobs:
       - uses: actions/setup-java@v4
         with:
           distribution: temurin
-          java-version: '21'
+          java-version: "21"
 
       - name: Install Jq
         uses: sergeysova/jq-action@v2

certora/confs/SentinelLiveness.conf

@@ -1,20 +1,12 @@
 {
   "files": [
     "certora/helpers/Utils.sol",
-    "certora/helpers/VaultV2Harness.sol",
-    "test/mocks/ERC20Mock.sol"
+    "certora/helpers/VaultV2Harness.sol"
   ],
-  "link": [
-    "VaultV2Harness:asset=ERC20Mock"
-  ],
-  "solc": "solc-0.8.28",
   "verify": "VaultV2Harness:certora/specs/SentinelLiveness.spec",
   "optimistic_loop": true,
   "loop_iter": "3",
   "optimistic_hashing": true,
-  "prover_args": [
-    "-superOptimisticReturnsize true"
-  ],
-  "server": "production",
+  "solc": "solc-0.8.28",
   "msg": "VaultV2 Sentinel Liveness"
 }

certora/confs/SentinelLivenessDeallocateMarketV1.conf

@@ -0,0 +1,22 @@
+{
+  "files": [
+    "src/VaultV2.sol",
+    "src/adapters/MorphoMarketV1Adapter.sol",
+    "certora/helpers/Utils.sol",
+    "test/mocks/ERC20Mock.sol"
+  ],
+  "link": [
+    "MorphoMarketV1Adapter:parentVault=VaultV2",
+    "MorphoMarketV1Adapter:asset=ERC20Mock",
+    "VaultV2:asset=ERC20Mock"
+  ],
+  "verify": "VaultV2:certora/specs/SentinelLivenessDeallocateMarketV1.spec",
+  "prover_args": [
+    "-superOptimisticReturnsize true"
+  ],
+  "optimistic_loop": true,
+  "loop_iter": "3",
+  "optimistic_hashing": true,
+  "solc": "solc-0.8.28",
+  "msg": "VaultV2 Sentinel Liveness Deallocate Market V1"
+}

certora/confs/SentinelLivenessDeallocateVaultV1.conf

@@ -0,0 +1,20 @@
+{
+  "files": [
+    "src/VaultV2.sol",
+    "src/adapters/MorphoVaultV1Adapter.sol",
+    "test/mocks/ERC20Mock.sol"
+  ],
+  "link": [
+    "MorphoVaultV1Adapter:parentVault=VaultV2",
+    "VaultV2:asset=ERC20Mock"
+  ],
+  "verify": "VaultV2:certora/specs/SentinelLivenessDeallocateVaultV1.spec",
+  "prover_args": [
+    "-superOptimisticReturnsize true"
+  ],
+  "optimistic_loop": true,
+  "loop_iter": "3",
+  "optimistic_hashing": true,
+  "solc": "solc-0.8.28",
+  "msg": "VaultV2 Sentinel Liveness Deallocate Vault V1"
+}

certora/helpers/Utils.sol

@@ -54,6 +54,10 @@ contract Utils {
         return supplyShares.toAssetsDown(totalSupplyAssets, totalSupplyShares);
     }
 
+    function encodeMarketParams(MarketParams memory marketParams) external pure returns (bytes memory) {
+        return abi.encode(marketParams);
+    }
+
     function decodeMarketParams(bytes memory data) external pure returns (MarketParams memory) {
         return abi.decode(data, (MarketParams));
     }

certora/specs/AllocationMorphoMarketV1Adapter.spec

@@ -46,7 +46,7 @@ function morphoMarketV1AdapterWrapperSummary(env e, bool isAllocateCall, bytes d
     } else {
         ids, change = MorphoMarketV1Adapter.deallocate(e, data, assets, bs, a);
     }
-    require forall uint256 i. forall uint256 j. i < j && j < ids.length => ids[j] != ids[i], "proven in the distinctMarketV1AdapterIds rule";
+    require forall uint256 i. forall uint256 j. i < j && j < ids.length => ids[j] != ids[i], "proven in the distinctAdapterIds rule";
     ghostChange = change;
 
     return (ids, change);

certora/specs/IdsMorphoMarketV1Adapter.spec

@@ -60,7 +60,8 @@ rule matchingIdsOnDeallocate(env e, bytes data, uint256 assets, bytes4 selector,
 invariant valueOfAdapterId()
   adapterId() == Utils.adapterId(currentContract);
 
-rule distinctMarketV1AdapterIds(MorphoMarketV1Adapter.MarketParams marketParams) {
+// Show that the ids returned are distinct.
+rule distinctAdapterIds(MorphoMarketV1Adapter.MarketParams marketParams) {
   bytes32[] ids = ids(marketParams);
 
   requireInvariant valueOfAdapterId();

certora/specs/IdsMorphoVaultV1Adapter.spec

@@ -45,3 +45,10 @@ rule matchingIdsOnDeallocate(env e, bytes data, uint256 amount, bytes4 selector,
   assert idsDeallocate.length == 1;
   assert idsDeallocate[0] == ids[0];
 }
+
+// Show that the ids returned are distinct (trivial since there is only one id).
+rule distinctAdapterIds() {
+  bytes32[] ids = ids();
+
+  assert forall uint256 i. forall uint256 j. i < j && j < ids.length => ids[j] != ids[i];
+}

certora/specs/SentinelLiveness.spec

@@ -1,90 +1,49 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 // Copyright (c) 2025 Morpho Association
 
-using ERC20Mock as ERC20;
 using Utils as Utils;
 
-definition max_int256() returns int256 = (2 ^ 255) - 1;
-
 methods {
-    function isAdapter(address) external returns bool envfree;
-    function isSentinel(address) external returns bool envfree;
-    function executableAt(bytes) external returns uint256 envfree;
-    function getAbsoluteCap(bytes) external returns uint256 envfree;
-    function getRelativeCap(bytes) external returns uint256 envfree;
-
-    function _.deallocate(bytes, uint256 assets, bytes4, address) external =>
-        nondetDeallocateSummary(assets) expect (bytes32[], int256);
-    function ERC20.transferFrom(address, address, uint256) external returns bool => NONDET;
-}
-
-// Ghost copy of caps[*].allocation to be able to use quantifiers.
-ghost mapping(bytes32 => uint256) ghostAllocation {
-    init_state axiom forall bytes32 id. ghostAllocation[id] == 0;
-}
-
-hook Sload uint256 alloc caps[KEY bytes32 id].allocation {
-    require (ghostAllocation[id] == alloc, "set ghost value to be equal to the concrete value");
-}
-
-hook Sstore caps[KEY bytes32 id].allocation uint256 newAllocation (uint256 oldAllocation) {
-    ghostAllocation[id] = newAllocation;
-}
-
-function nondetDeallocateSummary(uint256 assets) returns (bytes32[], int256) {
-    bytes32[] ids;
-    int256 change;
-
-    require (forall uint256 i. forall uint256 j. i < j && j < ids.length => ids[j] != ids[i], "assume that all returned ids are unique");
-    require (forall uint256 i. i < ids.length => ghostAllocation[ids[i]] <= max_int256(), "no overflow before");
-    require (forall uint256 i. i < ids.length => ghostAllocation[ids[i]] > 0, "positive");
-    require (forall uint256 i. i < ids.length => change < 0 || ghostAllocation[ids[i]] + change <= max_int256(), "no overflow after");
-    require (forall uint256 i. i < ids.length => change >= 0 || ghostAllocation[ids[i]] >= -change, "no underflow after");
-
-    return (ids, change);
+    function isSentinel(address) external returns (bool) envfree;
+    function executableAt(bytes) external returns (uint256) envfree;
+    function getAbsoluteCap(bytes) external returns (uint256) envfree;
+    function getRelativeCap(bytes) external returns (uint256) envfree;
 }
 
-rule sentinelCanRevoke(env e, bytes data){
-    require (isSentinel(e.msg.sender), "ack");
-    require (e.msg.value == 0, "ack");
-
-    require (executableAt(data) != 0, "assume `data` is pending");
+// Check that a sentinel can always revoke.
+rule sentinelCanRevoke(env e, bytes data) {
+    require executableAt(data) != 0, "assume that data is pending";
 
+    require isSentinel(e.msg.sender), "setup call to be performed by a sentinel";
+    require e.msg.value == 0, "setup call to have no ETH value";
     revoke@withrevert(e, data);
     assert !lastReverted;
+
     assert executableAt(data) == 0;
 }
 
+// Check that a sentinel can always decrease the absolute cap.
 rule sentinelCanDecreaseAbsoluteCap(env e, bytes idData, uint256 newAbsoluteCap) {
-    require (isSentinel(e.msg.sender), "ack");
-    require (e.msg.value == 0, "ack");
-
-    require (newAbsoluteCap <= getAbsoluteCap(idData), "assume that newAbsoluteCap <= absoluteCap");
+    require executableAt(idData) != 0, "assume that idData is pending";
 
+    require newAbsoluteCap <= getAbsoluteCap(idData), "setup call to have a newAbsoluteCap <= absoluteCap";
+    require isSentinel(e.msg.sender), "setup call to be performed by a sentinel";
+    require e.msg.value == 0, "setup call to have no ETH value";
     decreaseAbsoluteCap@withrevert(e, idData, newAbsoluteCap);
     assert !lastReverted;
+
     assert getAbsoluteCap(idData) == newAbsoluteCap;
 }
 
+// Check that a sentinel can always decrease the relative cap.
 rule sentinelCanDecreaseRelativeCap(env e, bytes idData, uint256 newRelativeCap) {
-    require (isSentinel(e.msg.sender), "ack");
-    require (e.msg.value == 0, "ack");
-
-    require (newRelativeCap <= getRelativeCap(idData), "assume that newRelativeCap <= relativeCap");
+    require executableAt(idData) != 0, "assume that idData is pending";
 
+    require newRelativeCap <= getRelativeCap(idData), "setup call to have a newRelativeCap <= relativeCap";
+    require isSentinel(e.msg.sender), "setup call to be performed by a sentinel";
+    require e.msg.value == 0, "setup call to have no ETH value";
     decreaseRelativeCap@withrevert(e, idData, newRelativeCap);
     assert !lastReverted;
-    assert getRelativeCap(idData) == newRelativeCap;
-}
-
-rule sentinelCanDeallocate(env e, address adapter, bytes data, uint256 assets){
-    require (isSentinel(e.msg.sender), "ack");
-    require (e.msg.value == 0, "ack");
-    require (e.block.timestamp < 2^63, "safe because it corresponds to a time very far in the future");
-    require (e.block.timestamp >= currentContract.lastUpdate, "safe because lastUpdate is growing and monotonic");
-
-    require (isAdapter(adapter), "assume the adapter is valid");
 
-    deallocate@withrevert(e, adapter, data, assets);
-    assert !lastReverted;
+    assert getRelativeCap(idData) == newRelativeCap;
 }

certora/specs/SentinelLivenessDeallocateMarketV1.spec

@@ -0,0 +1,71 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+// Copyright (c) 2025 Morpho Association
+
+using ERC20Mock as ERC20;
+using Utils as Utils;
+using MorphoMarketV1Adapter as MorphoMarketV1Adapter;
+
+definition max_int256() returns int256 = (2 ^ 255) - 1;
+
+methods {
+    function isAdapter(address) external returns (bool) envfree;
+    function isSentinel(address) external returns (bool) envfree;
+    function Utils.decodeMarketParams(bytes) external returns (MorphoMarketV1Adapter.MarketParams) envfree;
+    function Utils.encodeMarketParams(MorphoMarketV1Adapter.MarketParams) external returns (bytes) envfree;
+    function MorphoMarketV1Adapter.allocation(MorphoMarketV1Adapter.MarketParams) external returns (uint256) envfree;
+
+    function _.deallocate(bytes data, uint256 assets, bytes4 selector, address sender) external with(env e) => morphoMarketV1AdapterDeallocateWrapper(calledContract, e, data, assets, selector, sender) expect(bytes32[], int256);
+
+    // Assume that the adapter's withdraw call succeeds.
+    function _.withdraw(MorphoMarketV1Adapter.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) external => NONDET;
+
+    // Transfers should not revert because market v1 sends back tokens to the adapter on withdraw.
+    function ERC20.transferFrom(address, address, uint256) external returns (bool) => NONDET;
+
+    // Assume that expectedSupplyAssets doesn't revert on market v1.
+    function _.expectedSupplyAssets(address morpho, MorphoMarketV1Adapter.MarketParams memory marketParams, address user) internal => summaryExpectedSupplyAssets(morpho, marketParams, user) expect uint256;
+}
+
+function summaryExpectedSupplyAssets(address morpho, MorphoMarketV1Adapter.MarketParams marketParams, address user) returns (uint256) {
+    uint256 assets;
+    require assets <= max_int256(), "assume that expectedSupplyAssets returns a value bounded by max_int256";
+    return assets;
+}
+
+
+function morphoMarketV1AdapterDeallocateWrapper(address adapter, env e, bytes data, uint256 assets, bytes4 selector, address sender) returns (bytes32[], int256) {
+    MorphoMarketV1Adapter.MarketParams marketParams = Utils.decodeMarketParams(data);
+    require MorphoMarketV1Adapter.allocation(marketParams) <= max_int256(), "see allocationIsInt256";
+
+    bytes32[] ids;
+    int256 change;
+    ids, change = adapter.deallocate(e, data, assets, selector, sender);
+
+    require forall uint256 i. forall uint256 j. i < j && j < ids.length => ids[j] != ids[i], "see distinctAdapterIds";
+    require forall uint256 i. i < ids.length => currentContract.caps[ids[i]].allocation <= max_int256(), "see allocationIsInt256";
+    require forall uint256 i. i < ids.length => currentContract.caps[ids[i]].allocation + change >= 0, "see changeForDeallocateIsBoundedByAllocation";
+
+    require forall uint256 i. i < ids.length => currentContract.caps[ids[i]].allocation > 0, "assume that all ids have a positive allocation";
+    require forall uint256 i. i < ids.length => currentContract.caps[ids[i]].allocation + change <= max_int256(), "assume that the change doesn't overflow int256 on any id";
+
+    return (ids, change);
+}
+
+// Check that a sentinel can deallocate, assuming that:
+// - the adapter has positive allocations on all ids,
+// - the adapter's withdraw call succeeds,
+// - expectedSupplyAssets doesn't revert and returns a value bounded by max_int256.
+// - the change doesn't overflow int256 on any id.
+rule sentinelCanDeallocate(env e, address adapter, bytes data, uint256 assets) {
+    require e.block.timestamp < 2 ^ 63, "safe because it corresponds to a time very far in the future";
+    require e.block.timestamp >= currentContract.lastUpdate, "safe because lastUpdate is growing and monotonic";
+
+    MorphoMarketV1Adapter.MarketParams marketParams;
+    require marketParams.loanToken == currentContract.asset, "setup call to have the correct loan token";
+    require data == Utils.encodeMarketParams(marketParams), "setup call to have the correct data";
+    require isAdapter(adapter), "setup call to be performed on a valid adapter";
+    require isSentinel(e.msg.sender), "setup call to be performed by a sentinel";
+    require e.msg.value == 0, "setup call to have no ETH value";
+    deallocate@withrevert(e, adapter, data, assets);
+    assert !lastReverted;
+}

certora/specs/SentinelLivenessDeallocateVaultV1.spec

@@ -0,0 +1,64 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+// Copyright (c) 2025 Morpho Association
+
+using ERC20Mock as ERC20;
+using MorphoVaultV1Adapter as MorphoVaultV1Adapter;
+
+definition max_int256() returns int256 = (2 ^ 255) - 1;
+
+methods {
+    function isAdapter(address) external returns (bool) envfree;
+    function isSentinel(address) external returns (bool) envfree;
+    function MorphoVaultV1Adapter.allocation() external returns (uint256) envfree;
+
+    function _.deallocate(bytes data, uint256 assets, bytes4 selector, address sender) external with(env e) => morphoVaultV1AdapterDeallocateWrapper(calledContract, e, data, assets, selector, sender) expect(bytes32[], int256);
+
+    // Assume that the adapter's withdraw call succeeds.
+    function _.withdraw(uint256 assets, address onBehalf, address receiver) external => NONDET;
+
+    // Transfers should not revert because vault v1 sends back tokens to the adapter on withdraw.
+    function ERC20.transferFrom(address, address, uint256) external returns (bool) => NONDET;
+
+    // The function balanceOf doesn't revert on vault v1.
+    function _.balanceOf(address) external => NONDET;
+
+    // Assume that previewRedeem doesn't revert on vault v1, this implies that underlying expectedSupplyAssets calls don't revert.
+    function _.previewRedeem(uint256 shares) external => summaryPreviewRedeem(shares) expect uint256;
+}
+
+function summaryPreviewRedeem(uint256 shares) returns (uint256) {
+    uint256 assets;
+    require assets <= max_int256(), "assume that previewRedeem returns a value bounded by max_int256";
+    return assets;
+}
+
+function morphoVaultV1AdapterDeallocateWrapper(address adapter, env e, bytes data, uint256 assets, bytes4 selector, address sender) returns (bytes32[], int256) {
+    uint256 allocation = MorphoVaultV1Adapter.allocation();
+    require allocation <= max_int256(), "see allocationIsInt256";
+
+    bytes32[] ids;
+    int256 change;
+    ids, change = adapter.deallocate(e, data, assets, selector, sender);
+
+    require allocation + change >= 0, "see changeForDeallocateIsBoundedByAllocation";
+
+    require allocation > 0, "assume that the adapter has a positive allocation";
+
+    return (ids, change);
+}
+
+// Check that a sentinel can deallocate, assuming that:
+// - the adapter has a positive allocation,
+// - the adapter's withdraw call succeeds,
+// - previewRedeem doesn't revert and returns a value bounded by max_int256.
+rule sentinelCanDeallocate(env e, address adapter, bytes data, uint256 assets) {
+    require e.block.timestamp < 2 ^ 63, "safe because it corresponds to a time very far in the future";
+    require e.block.timestamp >= currentContract.lastUpdate, "safe because lastUpdate is growing and monotonic";
+
+    require data.length == 0, "setup call to have the correct data";
+    require isAdapter(adapter), "setup call to be performed on a valid adapter";
+    require isSentinel(e.msg.sender), "setup call to be performed by a sentinel";
+    require e.msg.value == 0, "setup call to have no ETH value";
+    deallocate@withrevert(e, adapter, data, assets);
+    assert !lastReverted;
+}