[Certora] Verification of timelocks (WIP)

.github/workflows/certora.yml

@@ -23,6 +23,7 @@ jobs:
           - ChangesMorphoMarketV1Adapter
           - ChangesMorphoVaultV1Adapter
           - ExchangeRate
+          - ExecutableAt
           - Gates
           - IdsMorphoMarketV1Adapter
           - IdsMorphoVaultV1Adapter
@@ -37,7 +38,9 @@ jobs:
           - Reentrancy
           - ReentrancyView
           - RelativeCaps
+          - RevertsTimelocked
           - SentinelLiveness
+          - Timelocks
           - TokensMorphoMarketV1Adapter
           - TokensMorphoVaultV1Adapter
           - TokensNoAdapter

certora/confs/ExecutableAt.conf

@@ -0,0 +1,16 @@
+{
+  "files": [
+    "certora/helpers/Utils.sol",
+    "certora/helpers/ExecutableAtHelpers.sol",
+    "src/VaultV2.sol"
+  ],
+  "link": [
+    "ExecutableAtHelpers:vault=VaultV2"
+  ],
+  "verify": "VaultV2:certora/specs/ExecutableAt.spec",
+  "solc": "solc-0.8.28",
+  "loop_iter": "2",
+  "optimistic_loop": true,
+  "optimistic_hashing": true,
+  "msg": "Executable conditions for timelocked functions do not revert"
+}

certora/confs/RevertsTimelocked.conf

@@ -0,0 +1,16 @@
+{
+  "files": [
+    "certora/helpers/Utils.sol",
+    "certora/helpers/RevertsTimelockedHelpers.sol",
+    "src/VaultV2.sol"
+  ],
+  "link": [
+    "RevertsTimelockedHelpers:vault=VaultV2"
+  ],
+  "solc": "solc-0.8.28",
+  "verify": "VaultV2:certora/specs/RevertsTimelocked.spec",
+  "loop_iter": "2",
+  "optimistic_loop": true,
+  "optimistic_hashing": true,
+  "msg": "Revert Conditions for Timelocked Functions"
+}

certora/confs/Timelocks.conf

@@ -0,0 +1,22 @@
+{
+  "files": [
+    "certora/helpers/Utils.sol",
+    "certora/helpers/TimelocksHelpers.sol:TimelockManagerHelpers",
+    "certora/helpers/TimelocksHelpers.sol:BeforeMinimumTimeChecker",
+    "certora/helpers/TimelocksHelpers.sol:NotSubmittedHarness",
+    "certora/helpers/TimelocksHelpers.sol:RevokeHarness",
+    "src/VaultV2.sol"
+  ],
+  "link": [
+    "TimelockManagerHelpers:vault=VaultV2",
+    "BeforeMinimumTimeChecker:vault=VaultV2",
+    "NotSubmittedHarness:vault=VaultV2",
+    "RevokeHarness:vault=VaultV2"
+  ],
+  "solc": "solc-0.8.28",
+  "verify": "VaultV2:certora/specs/Timelocks.spec",
+  "loop_iter": "2",
+  "optimistic_loop": true,
+  "optimistic_hashing": true,
+  "msg": "Timelocks"
+}

certora/helpers/ExecutableAtHelpers.sol

@@ -0,0 +1,157 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+// Copyright (c) 2025 Morpho Association
+pragma solidity 0.8.28;
+
+import "../../src/VaultV2.sol";
+import "../../src/interfaces/IVaultV2.sol";
+import "../../src/interfaces/IAdapterRegistry.sol";
+import {
+    WAD,
+    MAX_PERFORMANCE_FEE,
+    MAX_MANAGEMENT_FEE,
+    MAX_FORCE_DEALLOCATE_PENALTY
+} from "../../src/libraries/ConstantsLib.sol";
+
+/// Helper verifying timelocked functions can execute when conditions are met
+contract ExecutableAtHelpers {
+    VaultV2 public vault;
+
+    function checkTimelockConditions() internal view {
+        uint256 executableAtData = vault.executableAt(msg.data);
+        require(executableAtData != 0, "Data not submitted");
+        require(block.timestamp >= executableAtData, "Timelock not expired");
+        bytes4 selector = bytes4(msg.data);
+        require(!vault.abdicated(selector), "Function is abdicated");
+    }
+
+    // ============================================================================
+    // TIMELOCKED FUNCTIONS - Match VaultV2 signatures
+    // ============================================================================
+
+    function setIsAllocator(address, bool) external view {
+        checkTimelockConditions();
+    }
+
+    function setReceiveSharesGate(address) external view {
+        checkTimelockConditions();
+    }
+
+    function setSendSharesGate(address) external view {
+        checkTimelockConditions();
+    }
+
+    function setReceiveAssetsGate(address) external view {
+        checkTimelockConditions();
+    }
+
+    function setSendAssetsGate(address) external view {
+        checkTimelockConditions();
+    }
+
+    function setAdapterRegistry(address newAdapterRegistry) external view {
+        checkTimelockConditions();
+
+        // If setting a non-zero registry, it must include all existing adapters
+        if (newAdapterRegistry != address(0)) {
+            uint256 adaptersLength = vault.adaptersLength();
+            for (uint256 i = 0; i < adaptersLength; i++) {
+                address adapter = vault.adapters(i);
+                require(IAdapterRegistry(newAdapterRegistry).isInRegistry(adapter), "Adapter not in new registry");
+            }
+        }
+    }
+
+    function addAdapter(address account) external view {
+        checkTimelockConditions();
+
+        address registry = vault.adapterRegistry();
+        require(registry == address(0) || IAdapterRegistry(registry).isInRegistry(account), "Adapter not in registry");
+    }
+
+    function removeAdapter(address) external view {
+        checkTimelockConditions();
+    }
+
+    function increaseTimelock(bytes4 targetSelector, uint256 newDuration) external view {
+        checkTimelockConditions();
+        require(targetSelector != IVaultV2.decreaseTimelock.selector, "Cannot timelock decreaseTimelock");
+        require(newDuration >= vault.timelock(targetSelector), "Timelock not increasing");
+    }
+
+    function decreaseTimelock(bytes4 targetSelector, uint256 newDuration) external view {
+        checkTimelockConditions();
+        require(targetSelector != IVaultV2.decreaseTimelock.selector, "Cannot timelock decreaseTimelock");
+        require(newDuration <= vault.timelock(targetSelector), "Timelock not decreasing");
+    }
+
+    function abdicate(bytes4) external view {
+        checkTimelockConditions();
+    }
+
+    function setPerformanceFee(uint256 newPerformanceFee) external view {
+        checkTimelockConditions();
+        require(block.timestamp >= vault.lastUpdate(), "Last update not set");
+        require(block.timestamp <= vault.lastUpdate() + 315360000, "Time too far in future");
+        require(newPerformanceFee <= MAX_PERFORMANCE_FEE, "Fee exceeds MAX_PERFORMANCE_FEE");
+        require(
+            vault.performanceFeeRecipient() != address(0) || newPerformanceFee == 0,
+            "Fee invariant broken: recipient must be set if fee > 0"
+        );
+    }
+
+    function setManagementFee(uint256 newManagementFee) external view {
+        checkTimelockConditions();
+        require(block.timestamp >= vault.lastUpdate(), "Last update not set");
+        require(block.timestamp <= vault.lastUpdate() + 315360000, "Time too far in future");
+        require(newManagementFee <= MAX_MANAGEMENT_FEE, "Fee exceeds MAX_MANAGEMENT_FEE");
+        require(
+            vault.managementFeeRecipient() != address(0) || newManagementFee == 0,
+            "Fee invariant broken: recipient must be set if fee > 0"
+        );
+    }
+
+    function setPerformanceFeeRecipient(address newPerformanceFeeRecipient) external view {
+        checkTimelockConditions();
+        require(block.timestamp >= vault.lastUpdate(), "Last update not set");
+        require(block.timestamp <= vault.lastUpdate() + 315360000, "Time too far in future");
+        require(
+            newPerformanceFeeRecipient != address(0) || vault.performanceFee() == 0,
+            "Fee invariant broken: recipient cannot be zero if fee > 0"
+        );
+    }
+
+    function setManagementFeeRecipient(address newManagementFeeRecipient) external view {
+        checkTimelockConditions();
+        require(block.timestamp >= vault.lastUpdate(), "Last update not set");
+        require(block.timestamp <= vault.lastUpdate() + 315360000, "Time too far in future");
+        require(
+            newManagementFeeRecipient != address(0) || vault.managementFee() == 0,
+            "Fee invariant broken: recipient cannot be zero if fee > 0"
+        );
+    }
+
+    function increaseAbsoluteCap(bytes memory idData, uint256 newAbsoluteCap) external view {
+        checkTimelockConditions();
+
+        // Check that new cap is actually increasing and fits in uint128
+        bytes32 id = keccak256(idData);
+        uint256 currentAbsoluteCap = vault.absoluteCap(id);
+        require(newAbsoluteCap >= currentAbsoluteCap, "Absolute cap not increasing");
+        require(newAbsoluteCap <= type(uint128).max, "Cap exceeds uint128 max");
+    }
+
+    function increaseRelativeCap(bytes memory idData, uint256 newRelativeCap) external view {
+        checkTimelockConditions();
+        require(newRelativeCap <= WAD, "Relative cap exceeds WAD (100%)");
+
+        // Check that new cap is actually increasing
+        bytes32 id = keccak256(idData);
+        uint256 currentRelativeCap = vault.relativeCap(id);
+        require(newRelativeCap >= currentRelativeCap, "Relative cap not increasing");
+    }
+
+    function setForceDeallocatePenalty(address, uint256 newForceDeallocatePenalty) external view {
+        checkTimelockConditions();
+        require(newForceDeallocatePenalty <= MAX_FORCE_DEALLOCATE_PENALTY, "Penalty exceeds MAX");
+    }
+}

certora/helpers/RevertsTimelockedHelpers.sol

@@ -0,0 +1,94 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+// Copyright (c) 2025 Morpho Association
+pragma solidity 0.8.28;
+
+import "../../src/VaultV2.sol";
+import "../../src/interfaces/IVaultV2.sol";
+
+// Helper verifying timelocked functions revert when one of the conditions is not met
+contract RevertsTimelockedHelpers {
+    VaultV2 public vault;
+
+    function checkShouldRevert(bytes4 targetSelector) internal view {
+        bool shouldRevert =
+            (vault.abdicated(targetSelector) || vault.executableAt(msg.data) == 0
+                || vault.executableAt(msg.data) > block.timestamp);
+        require(shouldRevert, "Expected revert conditions not met");
+    }
+
+    // ============================================================================
+    // TIMELOCKED FUNCTIONS - Check revert conditions
+    // ============================================================================
+
+    function setIsAllocator(address, bool) external view {
+        checkShouldRevert(IVaultV2.setIsAllocator.selector);
+    }
+
+    function setReceiveSharesGate(address) external view {
+        checkShouldRevert(IVaultV2.setReceiveSharesGate.selector);
+    }
+
+    function setSendSharesGate(address) external view {
+        checkShouldRevert(IVaultV2.setSendSharesGate.selector);
+    }
+
+    function setReceiveAssetsGate(address) external view {
+        checkShouldRevert(IVaultV2.setReceiveAssetsGate.selector);
+    }
+
+    function setSendAssetsGate(address) external view {
+        checkShouldRevert(IVaultV2.setSendAssetsGate.selector);
+    }
+
+    function setAdapterRegistry(address) external view {
+        checkShouldRevert(IVaultV2.setAdapterRegistry.selector);
+    }
+
+    function addAdapter(address) external view {
+        checkShouldRevert(IVaultV2.addAdapter.selector);
+    }
+
+    function removeAdapter(address) external view {
+        checkShouldRevert(IVaultV2.removeAdapter.selector);
+    }
+
+    function increaseTimelock(bytes4, uint256) external view {
+        checkShouldRevert(IVaultV2.increaseTimelock.selector);
+    }
+
+    function decreaseTimelock(bytes4, uint256) external view {
+        checkShouldRevert(IVaultV2.decreaseTimelock.selector);
+    }
+
+    function abdicate(bytes4) external view {
+        checkShouldRevert(IVaultV2.abdicate.selector);
+    }
+
+    function setPerformanceFee(uint256) external view {
+        checkShouldRevert(IVaultV2.setPerformanceFee.selector);
+    }
+
+    function setManagementFee(uint256) external view {
+        checkShouldRevert(IVaultV2.setManagementFee.selector);
+    }
+
+    function setPerformanceFeeRecipient(address) external view {
+        checkShouldRevert(IVaultV2.setPerformanceFeeRecipient.selector);
+    }
+
+    function setManagementFeeRecipient(address) external view {
+        checkShouldRevert(IVaultV2.setManagementFeeRecipient.selector);
+    }
+
+    function increaseAbsoluteCap(bytes memory, uint256) external view {
+        checkShouldRevert(IVaultV2.increaseAbsoluteCap.selector);
+    }
+
+    function increaseRelativeCap(bytes memory, uint256) external view {
+        checkShouldRevert(IVaultV2.increaseRelativeCap.selector);
+    }
+
+    function setForceDeallocatePenalty(address, uint256) external view {
+        checkShouldRevert(IVaultV2.setForceDeallocatePenalty.selector);
+    }
+}