diff --git a/.github/workflows/certora-prover.yml b/.github/workflows/certora-prover.yml index c0566a7e29..147b56a500 100644 --- a/.github/workflows/certora-prover.yml +++ b/.github/workflows/certora-prover.yml @@ -1,122 +1,35 @@ name: Certora on: - # Run when PRs from feat/* branches are merged into dev pull_request: - types: [closed] branches: - - main - - # Run on any pushes to certora/* branches - push: - branches: - - 'certora/**' - - # Biweekly schedule (1st and 15th of each month at midnight UTC) - schedule: - - cron: '0 0 1,15 * *' - - # Manual trigger + - certora/distro workflow_dispatch: jobs: - # First job: Compile the contracts for Certora verification - compile: - name: Compile - # Run if it meets one of these conditions: - # 1. It's a merged PR from a feat/* branch to dev - # 2. It's a push to a certora/* branch - # 3. It's a scheduled run - # 4. It's a manually triggered run - if: > - (github.event_name == 'pull_request' && - github.event.pull_request.merged == true && - startsWith(github.head_ref, 'feat/')) || - (github.event_name == 'push' && - startsWith(github.ref, 'refs/heads/certora/')) || - github.event_name == 'schedule' || - github.event_name == 'workflow_dispatch' - runs-on: protocol-x64-16core - steps: - # Checkout the repository with submodules - - uses: actions/checkout@v4 - with: - submodules: recursive - # Use dev branch for scheduled runs, otherwise use the branch that triggered the workflow - ref: ${{ github.event_name == 'schedule' && 'dev' || github.ref }} - - # Install the Foundry toolchain - - name: Install Foundry - uses: foundry-rs/foundry-toolchain@v1 - with: - version: stable - - # Install dependencies using Forge - - name: Install forge dependencies - run: forge install - - # Run Certora compilation step only - - uses: Certora/certora-run-action@v1 - with: - # List of configuration files for different contracts to verify - configurations: |- - certora/confs/core/AllocationManager.conf - certora/confs/core/AllocationManagerSanity.conf - certora/confs/core/DelegationManager.conf - certora/confs/core/DelegationManagerValidState.conf - certora/confs/core/StrategyManager.conf - certora/confs/permissions/Pausable.conf - certora/confs/pods/EigenPodManagerRules.conf - certora/confs/strategies/StrategyBase.conf - use-beta: true - solc-versions: 0.8.27 - solc-remove-version-prefix: "0." - job-name: "Eigenlayer Contracts" - certora-key: ${{ secrets.CERTORAKEY }} - # Only compile, don't run verification yet - compilation-steps-only: true - env: - GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} - - # Second job: Run the actual verification after compilation succeeds - verify: - name: Verify - runs-on: protocol-x64-16core - # This job depends on the compile job - needs: compile - # Same conditions as the compile job - if: > - (github.event_name == 'pull_request' && - github.event.pull_request.merged == true && - startsWith(github.head_ref, 'feat/')) || - (github.event_name == 'push' && - startsWith(github.ref, 'refs/heads/certora/')) || - github.event_name == 'schedule' || - github.event_name == 'workflow_dispatch' + certora_run: + runs-on: ubuntu-latest + permissions: + contents: read + statuses: write + pull-requests: write steps: - # Checkout the repository with submodules - - uses: actions/checkout@v4 + - name: Checkout repository + uses: actions/checkout@v4 with: submodules: recursive - # Use dev branch for scheduled runs, otherwise use the branch that triggered the workflow - ref: ${{ github.event_name == 'schedule' && 'dev' || github.ref }} - - # Install the Foundry toolchain. - name: Install Foundry uses: foundry-rs/foundry-toolchain@v1 with: version: stable - - # Install dependencies using Forge - name: Install forge dependencies run: forge install - - # Run Certora verification with the same configurations - - uses: Certora/certora-run-action@v1 + - name: Run Certora pipeline + uses: Certora/certora-run-action@v1 with: - # List of configuration files for different contracts to verify configurations: |- certora/confs/core/AllocationManager.conf + certora/confs/core/AllocationManagerValidState.conf certora/confs/core/AllocationManagerSanity.conf certora/confs/core/DelegationManager.conf certora/confs/core/DelegationManagerValidState.conf @@ -126,7 +39,6 @@ jobs: certora/confs/strategies/StrategyBase.conf use-beta: true solc-versions: 0.8.27 - solc-remove-version-prefix: "0." job-name: "Eigenlayer Contracts" certora-key: ${{ secrets.CERTORAKEY }} env: diff --git a/certora/confs/core/AllocationManager.conf b/certora/confs/core/AllocationManager.conf index 3338a30598..e4288438db 100644 --- a/certora/confs/core/AllocationManager.conf +++ b/certora/confs/core/AllocationManager.conf @@ -1,7 +1,7 @@ { "assert_autofinder_success": true, "files": [ - "src/contracts/core/AllocationManager.sol", + "certora/harnesses/AllocationManagerHarness.sol", "src/contracts/permissions/PauserRegistry.sol", "src/contracts/permissions/PermissionController.sol", "src/contracts/core/DelegationManager.sol", @@ -10,19 +10,19 @@ "src/contracts/strategies/StrategyBase.sol", "certora/mocks/CertoraAVSRegistrar.sol", "lib/openzeppelin-contracts-v4.9.0/contracts/token/ERC20/ERC20.sol", - "src/contracts/libraries/OperatorSetLib.sol" - ], - "java_args": [ + "src/contracts/libraries/OperatorSetLib.sol", + "certora/harnesses/ShortStringsUpgradeableHarness.sol", ], + "java_args": [], "link": [ - "AllocationManager:pauserRegistry=PauserRegistry", + "AllocationManagerHarness:pauserRegistry=PauserRegistry", "DelegationManager:permissionController=PermissionController", - "DelegationManager:allocationManager=AllocationManager", - "AllocationManager:permissionController=PermissionController", + "DelegationManager:allocationManager=AllocationManagerHarness", + "AllocationManagerHarness:permissionController=PermissionController", "DelegationManager:strategyManager=StrategyManager", - "AllocationManager:delegation=DelegationManager", + "AllocationManagerHarness:delegation=DelegationManager", "EigenPodManager:delegationManager=DelegationManager", - "DelegationManager:eigenPodManager=EigenPodManager" + "DelegationManager:eigenPodManager=EigenPodManager", ], "loop_iter": "1", "optimistic_fallback": true, @@ -32,14 +32,18 @@ "@openzeppelin=lib/openzeppelin-contracts-v4.9.0" ], "parametric_contracts": [ - "AllocationManager" + "AllocationManagerHarness" ], + "msg": "AllocationManager Rules", "process": "emv", "prover_args": [ - " -recursionErrorAsAssert false -recursionEntryLimit 3" + "-recursionErrorAsAssert false -recursionEntryLimit 3", + "-splitParallel true", + "-dontStopAtFirstSplitTimeout true", ], - "solc": "solc8.27", "solc_optimize": "1", - "verify": "AllocationManager:certora/specs/core/AllocationManagerRules.spec", + "verify": "AllocationManagerHarness:certora/specs/core/AllocationManagerRules.spec", "server": "production", + "rule_sanity": "basic", + "build_cache": true } diff --git a/certora/confs/core/AllocationManagerSanity.conf b/certora/confs/core/AllocationManagerSanity.conf index 7c46c258c9..7deacc145b 100644 --- a/certora/confs/core/AllocationManagerSanity.conf +++ b/certora/confs/core/AllocationManagerSanity.conf @@ -1,7 +1,7 @@ { "assert_autofinder_success": true, "files": [ - "src/contracts/core/AllocationManager.sol", + "certora/harnesses/AllocationManagerHarness.sol", "src/contracts/permissions/PauserRegistry.sol", "src/contracts/permissions/PermissionController.sol", "src/contracts/core/DelegationManager.sol", @@ -12,17 +12,16 @@ "lib/openzeppelin-contracts-v4.9.0/contracts/token/ERC20/ERC20.sol", "src/contracts/libraries/OperatorSetLib.sol" ], - "java_args": [ - ], + "java_args": [], "link": [ - "AllocationManager:pauserRegistry=PauserRegistry", + "AllocationManagerHarness:pauserRegistry=PauserRegistry", "DelegationManager:permissionController=PermissionController", - "DelegationManager:allocationManager=AllocationManager", - "AllocationManager:permissionController=PermissionController", + "DelegationManager:allocationManager=AllocationManagerHarness", + "AllocationManagerHarness:permissionController=PermissionController", "DelegationManager:strategyManager=StrategyManager", - "AllocationManager:delegation=DelegationManager", + "AllocationManagerHarness:delegation=DelegationManager", "EigenPodManager:delegationManager=DelegationManager", - "DelegationManager:eigenPodManager=EigenPodManager" + "DelegationManager:eigenPodManager=EigenPodManager", ], "loop_iter": "2", "optimistic_fallback": true, @@ -32,14 +31,14 @@ "@openzeppelin=lib/openzeppelin-contracts-v4.9.0" ], "parametric_contracts": [ - "AllocationManager" + "AllocationManagerHarness" ], "process": "emv", "prover_args": [ " -recursionErrorAsAssert false -recursionEntryLimit 3" ], - "solc": "solc8.27", "solc_optimize": "1", "solc_via_ir": true, - "verify": "AllocationManager:certora/specs/core/AllocationManagerSanity.spec" + "server": "production", + "verify": "AllocationManagerHarness:certora/specs/core/AllocationManagerSanity.spec" } diff --git a/certora/confs/core/AllocationManagerValidState.conf b/certora/confs/core/AllocationManagerValidState.conf new file mode 100644 index 0000000000..2da7f012ff --- /dev/null +++ b/certora/confs/core/AllocationManagerValidState.conf @@ -0,0 +1,45 @@ +{ + "assert_autofinder_success": true, + "files": [ + "certora/harnesses/AllocationManagerHarness.sol", + "src/contracts/permissions/PauserRegistry.sol", + "src/contracts/permissions/PermissionController.sol", + "src/contracts/core/DelegationManager.sol", + "src/contracts/pods/EigenPodManager.sol", + "src/contracts/core/StrategyManager.sol", + "src/contracts/strategies/StrategyBase.sol", + "certora/mocks/CertoraAVSRegistrar.sol", + "lib/openzeppelin-contracts-v4.9.0/contracts/token/ERC20/ERC20.sol", + "src/contracts/libraries/OperatorSetLib.sol" + ], + "java_args": [], + "link": [ + "AllocationManagerHarness:pauserRegistry=PauserRegistry", + "DelegationManager:permissionController=PermissionController", + "DelegationManager:allocationManager=AllocationManagerHarness", + "AllocationManagerHarness:permissionController=PermissionController", + "DelegationManager:strategyManager=StrategyManager", + "AllocationManagerHarness:delegation=DelegationManager", + "EigenPodManager:delegationManager=DelegationManager", + "DelegationManager:eigenPodManager=EigenPodManager", + ], + "loop_iter": "1", + "optimistic_fallback": true, + "optimistic_loop": true, + "packages": [ + "@openzeppelin-upgrades=lib/openzeppelin-contracts-upgradeable-v4.9.0", + "@openzeppelin=lib/openzeppelin-contracts-v4.9.0" + ], + "parametric_contracts": [ + "AllocationManagerHarness" + ], + "process": "emv", + "msg": "AllocationManager Valid State Invariants", + "prover_args": [ + " -recursionErrorAsAssert false -recursionEntryLimit 3" + ], + "solc_optimize": "1", + "verify": "AllocationManagerHarness:certora/specs/core/AllocationManagerValidState.spec", + "rule_sanity": "basic", + "server": "production", +} diff --git a/certora/confs/core/DelegationManager.conf b/certora/confs/core/DelegationManager.conf index 47d798e2e0..840536f37f 100644 --- a/certora/confs/core/DelegationManager.conf +++ b/certora/confs/core/DelegationManager.conf @@ -9,7 +9,6 @@ "src/contracts/strategies/StrategyBase.sol", "src/contracts/core/StrategyManager.sol", "src/contracts/permissions/PauserRegistry.sol", - "src/contracts/core/DelegationManager.sol", "src/contracts/permissions/PermissionController.sol", "src/contracts/core/AllocationManager.sol" ], @@ -20,7 +19,7 @@ "AllocationManager:permissionController=PermissionController", "DelegationManagerHarness:strategyManager=StrategyManager", "EigenPodManager:delegationManager=DelegationManagerHarness", - "DelegationManagerHarness:eigenPodManager=EigenPodManager" + "DelegationManagerHarness:eigenPodManager=EigenPodManager", ], "loop_iter": "2", "optimistic_fallback": true, @@ -34,6 +33,7 @@ "-tinyTimeout 20", "-depth 20" ], + "msg": "DelegationManager Rules", "packages": [ "@openzeppelin-upgrades=lib/openzeppelin-contracts-upgradeable-v4.9.0", "@openzeppelin=lib/openzeppelin-contracts-v4.9.0" @@ -43,8 +43,9 @@ ], "rule_sanity": "basic", "process": "emv", - "solc": "solc8.27", "solc_optimize": "1", "solc_via_ir": true, + "build_cache": true, + "server": "production", "verify": "DelegationManagerHarness:certora/specs/core/DelegationManager.spec" } diff --git a/certora/confs/core/DelegationManagerValidState.conf b/certora/confs/core/DelegationManagerValidState.conf index 2f3dfc081e..4117aa4740 100644 --- a/certora/confs/core/DelegationManagerValidState.conf +++ b/certora/confs/core/DelegationManagerValidState.conf @@ -9,9 +9,9 @@ "src/contracts/strategies/StrategyBase.sol", "src/contracts/core/StrategyManager.sol", "src/contracts/permissions/PauserRegistry.sol", - "src/contracts/core/DelegationManager.sol", "src/contracts/permissions/PermissionController.sol", - "src/contracts/core/AllocationManager.sol" + "src/contracts/core/AllocationManager.sol", + "certora/mocks/CertoraAVSRegistrar.sol", ], "link": [ "AllocationManager:delegation=DelegationManagerHarness", @@ -20,7 +20,7 @@ "AllocationManager:permissionController=PermissionController", "DelegationManagerHarness:strategyManager=StrategyManager", "EigenPodManager:delegationManager=DelegationManagerHarness", - "DelegationManagerHarness:eigenPodManager=EigenPodManager" + "DelegationManagerHarness:eigenPodManager=EigenPodManager", ], "loop_iter": "1", "optimistic_fallback": true, @@ -31,13 +31,15 @@ "@openzeppelin-upgrades=lib/openzeppelin-contracts-upgradeable-v4.9.0", "@openzeppelin=lib/openzeppelin-contracts-v4.9.0" ], + "msg": "DelegationManager Valid State Invariants", "parametric_contracts": [ - "DelegationManagerHarness" + "DelegationManagerHarness", ], - "rule_sanity": "basic", + "rule_sanity": "basic", "process": "emv", - "solc": "solc8.27", "solc_optimize": "1", "solc_via_ir": true, + "build_cache": true, + "server": "production", "verify": "DelegationManagerHarness:certora/specs/core/DelegationManagerValidState.spec" } diff --git a/certora/confs/core/SlashEscrowFactory.conf b/certora/confs/core/SlashEscrowFactory.conf new file mode 100644 index 0000000000..ceeb1f358a --- /dev/null +++ b/certora/confs/core/SlashEscrowFactory.conf @@ -0,0 +1,53 @@ +{ + "assert_autofinder_success": true, + "files": [ + "certora/harnesses/SlashEscrowFactoryHarness.sol", + "src/contracts/core/SlashEscrow.sol", + "src/contracts/core/AllocationManager.sol", + "src/contracts/permissions/PauserRegistry.sol", + "src/contracts/permissions/PermissionController.sol", + "src/contracts/core/DelegationManager.sol", + "src/contracts/pods/EigenPodManager.sol", + "src/contracts/core/StrategyManager.sol", + "src/contracts/strategies/StrategyBase.sol", + "certora/mocks/CertoraAVSRegistrar.sol", + "lib/openzeppelin-contracts-v4.9.0/contracts/token/ERC20/ERC20.sol", + "src/contracts/libraries/OperatorSetLib.sol", + ], + "java_args": [], + "link": [ + "AllocationManager:pauserRegistry=PauserRegistry", + "DelegationManager:permissionController=PermissionController", + "DelegationManager:allocationManager=AllocationManager", + "AllocationManager:permissionController=PermissionController", + "DelegationManager:strategyManager=StrategyManager", + "AllocationManager:delegation=DelegationManager", + "EigenPodManager:delegationManager=DelegationManager", + "DelegationManager:eigenPodManager=EigenPodManager", + "StrategyManager:slashEscrowFactory=SlashEscrowFactoryHarness", + "SlashEscrowFactoryHarness:pauserRegistry=PauserRegistry", + "SlashEscrowFactoryHarness:allocationManager=AllocationManager", + "SlashEscrowFactoryHarness:strategyManager=StrategyManager", + "SlashEscrowFactoryHarness:slashEscrowImplementation=SlashEscrow", + ], + "loop_iter": "3", + "optimistic_fallback": true, + "optimistic_loop": true, + "packages": [ + "@openzeppelin-upgrades=lib/openzeppelin-contracts-upgradeable-v4.9.0", + "@openzeppelin=lib/openzeppelin-contracts-v4.9.0" + ], + "parametric_contracts": [ + "SlashEscrowFactoryHarness" + ], + "process": "emv", + "prover_args": [ + " -recursionErrorAsAssert false -recursionEntryLimit 3", + ], + // "precise_bitwise_ops": true, + "solc_optimize": "1", + "verify": "SlashEscrowFactoryHarness:certora/specs/core/SlashEscrowFactory.spec", + "server": "production", + "build_cache": true, + "rule_sanity": "basic" +} diff --git a/certora/confs/core/StrategyManager.conf b/certora/confs/core/StrategyManager.conf index f4902d46f8..495232a578 100644 --- a/certora/confs/core/StrategyManager.conf +++ b/certora/confs/core/StrategyManager.conf @@ -9,12 +9,13 @@ "src/contracts/strategies/StrategyBase.sol", "src/contracts/core/DelegationManager.sol", "src/contracts/permissions/PauserRegistry.sol", - "src/contracts/core/AllocationManager.sol" + "src/contracts/core/AllocationManager.sol", ], "link": [ "DelegationManager:allocationManager=AllocationManager", "DelegationManager:eigenPodManager=EigenPodManager", - "StrategyManagerHarness:delegation=DelegationManager" + "StrategyManagerHarness:delegation=DelegationManager", + "StrategyManagerHarness:allocationManager=AllocationManager", ], "loop_iter": "2", "optimistic_fallback": true, @@ -29,9 +30,10 @@ "StrategyManagerHarness" ], "process": "emv", - "solc": "solc8.27", "solc_optimize": "1", "solc_via_ir": true, + "msg": "StrategyManager Rules", "verify": "StrategyManagerHarness:certora/specs/core/StrategyManager.spec", - "rule_sanity": "basic" + "rule_sanity": "basic", + "server": "production" } diff --git a/certora/confs/permissions/Pausable.conf b/certora/confs/permissions/Pausable.conf index 384256e4ab..e3e5dc7a68 100644 --- a/certora/confs/permissions/Pausable.conf +++ b/certora/confs/permissions/Pausable.conf @@ -13,8 +13,8 @@ "prover_args": [ " -recursionErrorAsAssert false -recursionEntryLimit 3" ], - "solc": "solc8.27", "solc_optimize": "1", "solc_via_ir": true, + "rule_sanity": "basic", "verify": "PausableHarness:certora/specs/permissions/Pausable.spec" } diff --git a/certora/confs/pods/EigenPodManagerRules.conf b/certora/confs/pods/EigenPodManagerRules.conf index 269c2660f1..830c36d727 100644 --- a/certora/confs/pods/EigenPodManagerRules.conf +++ b/certora/confs/pods/EigenPodManagerRules.conf @@ -5,8 +5,6 @@ "summary_recursion_limit": "1", "optimistic_contract_recursion": true, "contract_recursion_limit": "1", -// "optimistic_hashing": true, -// "hashing_length_bound": "4700", "files": [ "src/contracts/pods/EigenPodManager.sol", "src/contracts/core/DelegationManager.sol", @@ -16,14 +14,9 @@ "src/contracts/permissions/PauserRegistry.sol", "src/contracts/pods/EigenPod.sol", "src/test/mocks/ETHDepositMock.sol:ETHPOSDepositMock", - "lib/openzeppelin-contracts-v4.9.0/contracts/utils/Create2.sol", -// -// "src/contracts/strategies/StrategyBase.sol", -// "certora/mocks/CertoraAVSRegistrar.sol", -// "lib/openzeppelin-contracts-v4.9.0/contracts/token/ERC20/ERC20.sol" - ], - "java_args": [ + "lib/openzeppelin-contracts-v4.9.0/contracts/utils/Create2.sol" ], + "java_args": [], "link": [ "EigenPodManager:delegationManager=DelegationManager", "AllocationManager:pauserRegistry=PauserRegistry", @@ -48,7 +41,6 @@ "prover_args": [ " -recursionErrorAsAssert false -recursionEntryLimit 3" ], - "solc": "solc8.27", "solc_optimize": "1", "solc_via_ir": true, "verify": "EigenPodManager:certora/specs/pods/EigenPodManagerRules.spec", diff --git a/certora/confs/strategies/StrategyBase.conf b/certora/confs/strategies/StrategyBase.conf index 53eb14c4df..fad9f70dcc 100644 --- a/certora/confs/strategies/StrategyBase.conf +++ b/certora/confs/strategies/StrategyBase.conf @@ -19,10 +19,9 @@ "StrategyBase" ], "process": "emv", - "prover_args": [ - ], - "solc": "solc8.27", + "prover_args": [], "solc_optimize": "1", "solc_via_ir": true, + "rule_sanity": "basic", "verify": "StrategyBase:certora/specs/strategies/StrategyBase.spec" } diff --git a/certora/harnesses/AllocationManagerHarness.sol b/certora/harnesses/AllocationManagerHarness.sol new file mode 100644 index 0000000000..77628df3b5 --- /dev/null +++ b/certora/harnesses/AllocationManagerHarness.sol @@ -0,0 +1,35 @@ +// SPDX-License-Identifier: BUSL-1.1 +pragma solidity ^0.8.27; + +import "../../src/contracts/core/AllocationManager.sol"; +contract AllocationManagerHarness is AllocationManager { + constructor( + IDelegationManager _delegation, + IStrategy _eigenStrategy, + IPauserRegistry _pauserRegistry, + IPermissionController _permissionController, + uint32 _DEALLOCATION_DELAY, + uint32 _ALLOCATION_CONFIGURATION_DELAY, + string memory _version + ) AllocationManager( + _delegation, + _eigenStrategy, + _pauserRegistry, + _permissionController, + _DEALLOCATION_DELAY, + _ALLOCATION_CONFIGURATION_DELAY, + _version + ) {} + + function getOperatorKey(address avs, uint32 operatorSetId) external view returns (bytes32) { + return OperatorSetLib.key(OperatorSet(avs, operatorSetId)); + } + + function getOperatorSetFromKey(bytes32 key) external view returns (OperatorSet memory) { + return OperatorSetLib.decode(key); + } + + function getOperatorKeyFromSet(OperatorSet calldata os) external view returns (bytes32) { + return OperatorSetLib.key(os); + } +} \ No newline at end of file diff --git a/certora/harnesses/SlashEscrowFactoryHarness.sol b/certora/harnesses/SlashEscrowFactoryHarness.sol new file mode 100644 index 0000000000..a5a2aae7d9 --- /dev/null +++ b/certora/harnesses/SlashEscrowFactoryHarness.sol @@ -0,0 +1,79 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.0; + +import "../../src/contracts/core/SlashEscrowFactory.sol"; +import "@openzeppelin/contracts/utils/structs/EnumerableSet.sol"; + +/** + * @title SlashEscrowFactoryHarness + * @dev Minimal harness contract to expose only the internal state needed for verification + * without inventing methods that don't exist in the actual contracts + */ +contract SlashEscrowFactoryHarness is SlashEscrowFactory { + using OperatorSetLib for *; + using EnumerableSet for *; + constructor( + IAllocationManager _allocationManager, + IStrategyManager _strategyManager, + IPauserRegistry _pauserRegistry, + ISlashEscrow _slashEscrowImplementation, + string memory _version + ) SlashEscrowFactory(_allocationManager, _strategyManager, _pauserRegistry, _slashEscrowImplementation, _version ) {} + + + /** + * @dev Get pending slash IDs count for an operator set + */ + function getPendingSlashIdsCount(OperatorSet calldata operatorSet) external view returns (uint256) { + return _pendingSlashIds[operatorSet.key()].length(); + } + + /** + * @dev Check if a slash ID is pending for an operator set + */ + function isSlashIdPending(OperatorSet calldata operatorSet, uint256 slashId) external view returns (bool) { + return _pendingSlashIds[operatorSet.key()].contains(slashId); + } + + /** + * @dev Get pending strategies count for a slash ID + */ + function getPendingStrategiesCount(OperatorSet calldata operatorSet, uint256 slashId) external view returns (uint256) { + return _pendingStrategiesForSlashId[operatorSet.key()][slashId].length(); + } + + /** + * @dev Check if a strategy is pending for a slash ID + */ + function isStrategyPending(OperatorSet calldata operatorSet, uint256 slashId, IStrategy strategy) external view returns (bool) { + return _pendingStrategiesForSlashId[operatorSet.key()][slashId].contains(address(strategy)); + } + + /** + * @dev Get WAD constant (1e18) + */ + function WAD() external pure returns (uint256) { + return 1e18; + } + + /** + * @dev Create an operator set key for testing + */ + function createOperatorSetKey(address avs, uint32 operatorSetId) external pure returns (bytes32) { + return OperatorSetLib.key(OperatorSet(avs, operatorSetId)); + } + + /** + * @dev Create an operator set key for testing + */ + function getOperatorSetKey(OperatorSet calldata op) external pure returns (bytes32) { + return OperatorSetLib.key(op); + } + + /** + * @dev Decode an operator set key for testing + */ + function decodeOperatorSetKey(bytes32 operatorSetKey) external pure returns (OperatorSet memory) { + return OperatorSetLib.decode(operatorSetKey); + } +} diff --git a/certora/harnesses/StrategyManagerHarness.sol b/certora/harnesses/StrategyManagerHarness.sol index 83b326906d..f4f79704ab 100644 --- a/certora/harnesses/StrategyManagerHarness.sol +++ b/certora/harnesses/StrategyManagerHarness.sol @@ -5,12 +5,12 @@ import "../../src/contracts/core/StrategyManager.sol"; contract StrategyManagerHarness is StrategyManager { constructor( + IAllocationManager _allocationManager, IDelegationManager _delegation, IPauserRegistry _pauseRegistry, string memory _version - ) StrategyManager(_delegation, _pauseRegistry, _version) + ) StrategyManager(_allocationManager, _delegation, _pauseRegistry, _version) {} - function strategy_is_in_stakers_array(address staker, IStrategy strategy) public view returns (bool) { uint256 length = stakerStrategyList[staker].length; for (uint256 i = 0; i < length; ++i) { diff --git a/certora/specs/core/AllocationManagerRules.spec b/certora/specs/core/AllocationManagerRules.spec index ba4acd6e87..683033292a 100644 --- a/certora/specs/core/AllocationManagerRules.spec +++ b/certora/specs/core/AllocationManagerRules.spec @@ -1,17 +1,180 @@ import "./AllocationManagerValidState.spec"; +import "../ptaHelpers.spec"; +using DelegationManager as DelegationManager; -use invariant maxMagnitudeHistoryKeysMonotonicInc; -use invariant maxMagnitudeHistoryKeysLessThanCurrentBlock; -use invariant maxMagnitudeMonotonicallyDecreasing; -use invariant SetInRegisteredIFFStatusIsTrue; -use invariant encumberedMagnitudeEqSumOfCurrentMagnitudesAndPositivePending; -use invariant negativePendingDiffAtMostCurrentMagnitude; -use invariant deallocationQueueDataUniqueness; -use invariant noZeroKeyInDealocationQ; -use invariant deallocationQueueEffectBlocLessThanCurrBlockNumberPlushDelayPlusOne; -use invariant deallocationQueueEffectBlockAscesndingOrder; -use invariant noPositivePendingDiffInDeallocationQ; -use invariant effectBlockZeroHasNoPendingDiff; +methods { + function getOperatorKey(address, uint32) external returns (bytes32) envfree; + function getOperatorSetFromKey(bytes32) external returns (AllocationManagerHarness.OperatorSet) envfree; +} + +definition DEFAULT_BURN_ADDRESS() returns address = 0x00000000000000000000000000000000000E16E4; + + +/* +slashedMagnitude / currentMagnitudeBefore >= totalDepositSharesToSlash / (operatorSharesBefore + sharesInQueueBefore) +If this is false, it implies an AVS can “overslash” an operator, i.e. they can remove a larger percentage of funds. +We prove the mathematical equivalent: +slashedMagnitude * (totalShares + sharesInQueue) >= totalDepositSharesToSlash * currentMagnitude +*/ +rule noOverslashingOfShares(env e, address avs, IAllocationManagerTypes.SlashingParams params){ + + bytes32 operatorKey = getOperatorKey(avs, params.operatorSetId); + + // Assume some already proven invariants + requireValidState(); + requireNoOverflow(e); + requireInvariant maxMagnitudeLeqWAD(params.operator, params.strategies[0]); + requireInvariant currentMagnitudeLeqWAD(operatorKey, params.operator, params.strategies[0]); + requireInvariant encumberedMagnitudeLeqWAD(e, params.operator, params.strategies[0]); + requireInvariant maxMagnitudeGEencumberedMagnitude(params.operator, params.strategies[0]); + requireInvariant sumOfPendingDiffCurrentMagnitudeRespectsWAD(operatorKey, params.operator, params.strategies[0]); + requireInvariant maxMagnitudeGECurrentMagnitude(operatorKey, params.operator, params.strategies[0]); + + require (e.block.number < currentContract.allocations[params.operator][operatorKey][params.strategies[0]].effectBlock, "require to not trigger a change of values throughout computation by _getUpdatedAllocation()"); + + // cannot allocate type IAllocationManagerTypes.Allocation in CVL directly but can access fields of primitive types + uint64 currentMagnitudeBefore = currentContract.allocations[params.operator][operatorKey][params.strategies[0]].currentMagnitude; + int128 pendingDiffBefore = currentContract.allocations[params.operator][operatorKey][params.strategies[0]].pendingDiff; + require (pendingDiffBefore == 0, "prove an underapproximation assuming no pendingDiff, as pendingDiff changes currentMagnitude throughout the computation of slashOperator in _getUpdatedAllocation()"); + uint64 maxMagnitudeBefore = getMaxMagnitude(params.operator, params.strategies[0]); + + uint256 operatorSharesBefore = DelegationManager.operatorShares[params.operator][params.strategies[0]]; + uint256 queuedSharesBefore = DelegationManager.getSlashableSharesInQueue(e, params.operator, params.strategies[0]); + // Note: the totalDepositSharesToSlash usually also account for slashableSharesInQueue that have been removed + // Due to known rounding issues in the computation of DelegationManager.getSlashableSharesInQueue() + // we underapproximate and assume no slashableSharesInQueue but check no overslashing for operatorShares only + require queuedSharesBefore == 0; + require (operatorSharesBefore > 1, "1 share is an edge case that will always fail due to mulWadUp" ); + + slashOperator(e, avs, params); + + uint64 currentMagnitudeAfter = currentContract.allocations[params.operator][operatorKey][params.strategies[0]].currentMagnitude; + uint64 maxMagnitudeAfter = getMaxMagnitude(params.operator, params.strategies[0]); + + uint256 operatorSharesAfter = DelegationManager.operatorShares[params.operator][params.strategies[0]]; + + // currentMagnitude should not increase from a slash + assert(currentMagnitudeBefore >= currentMagnitudeAfter); + // operatorShares should not increase from a slash + assert(operatorSharesBefore >= operatorSharesAfter); + + uint64 slashedMagnitude = require_uint64(currentMagnitudeBefore - currentMagnitudeAfter); + uint256 totalDepositSharesToSlash = require_uint256(operatorSharesBefore - operatorSharesAfter); + + // assert slashedMagnitude / currentMagnitude >= totalDepositSharesToSlash / (operatorSharesBefore + queuedSharesBefore); + assert slashedMagnitude != 0 => slashedMagnitude * operatorSharesBefore >= totalDepositSharesToSlash * currentMagnitudeBefore; +} + +invariant maxMagnitudeGECurrentMagnitude(bytes32 operatorKey, address operator, address strategy) + currentContract.allocations[operator][operatorKey][strategy].currentMagnitude <= getMaxMagnitude(operator, strategy) + { + preserved with (env e) { + requireValidState(); + SumTrackingSetup(); + requireNoOverflow(e); + // magnitudes cannot go beyond 1e18 + requireInvariant maxMagnitudeLeqWAD(operator, strategy); + requireInvariant currentMagnitudeLeqWAD(operatorKey, operator, strategy); + requireInvariant encumberedMagnitudeLeqWAD(e, operator, strategy); + requireInvariant sumOfPendingDiffCurrentMagnitudeRespectsWAD(operatorKey, operator, strategy); + + requireInvariant maxMagnitudeGEencumberedMagnitude(operator, strategy); + require (e.block.number < currentContract.allocations[operator][operatorKey][strategy].effectBlock, "require to not trigger a change of values throughout computation by _getUpdatedAllocation()"); + } + preserved slashOperator( + address avs2, + IAllocationManagerTypes.SlashingParams params + ) with (env e) { + bytes32 opKey = getOperatorKey(avs2, params.operatorSetId); + require (opKey == operatorKey, "need to ensure that the parameter opKey is the same operatorKey as used in the invariant"); + + requireValidState(); + SumTrackingSetup(); + requireNoOverflow(e); + // magnitudes cannot go beyond 1e18 + requireInvariant maxMagnitudeLeqWAD(operator, strategy); + requireInvariant currentMagnitudeLeqWAD(operatorKey, operator, strategy); + requireInvariant encumberedMagnitudeLeqWAD(e, operator, strategy); + requireInvariant sumOfPendingDiffCurrentMagnitudeRespectsWAD(operatorKey, operator, strategy); + + requireInvariant maxMagnitudeGEencumberedMagnitude(operator, strategy); + require (e.block.number < currentContract.allocations[operator][operatorKey][strategy].effectBlock, "require to not trigger a change of values throughout computation by _getUpdatedAllocation()"); + } + } + +invariant maxMagnitudeLeqWAD(address operator, address strategy) + getMaxMagnitude(operator, strategy) <= WAD(); + +invariant currentMagnitudeLeqWAD(bytes32 operatorKey, address operator, address strategy) + currentContract.allocations[operator][operatorKey][strategy].currentMagnitude <= WAD() { + preserved with (env e) { + SumTrackingSetup(); + requireValidState(); + requireNoOverflow(e); + requireInvariant maxMagnitudeLeqWAD(operator, strategy); + requireInvariant encumberedMagnitudeLeqWAD(e, operator, strategy); + requireInvariant maxMagnitudeGEencumberedMagnitude(operator, strategy); + requireInvariant sumOfPendingDiffCurrentMagnitudeRespectsWAD(operatorKey, operator, strategy); + require (e.block.number < currentContract.allocations[operator][operatorKey][strategy].effectBlock, "require to not trigger a change of values throughout computation by _getUpdatedAllocation()"); + } + } + +invariant encumberedMagnitudeLeqWAD(env e, address operator, address strategy) + getEncumberedMagnitude(e, operator, strategy) <= WAD() { + preserved { + requireInvariant maxMagnitudeGEencumberedMagnitude(operator, strategy); + SumTrackingSetup(); + requireValidState(); + requireNoOverflow(e); + requireInvariant maxMagnitudeLeqWAD(operator, strategy); + } + } + +invariant sumOfPendingDiffCurrentMagnitudeRespectsWAD(bytes32 operatorKey, address operator, address strategy) + currentContract.allocations[operator][operatorKey][strategy].currentMagnitude + currentContract.allocations[operator][operatorKey][strategy].pendingDiff <= WAD() { + preserved with (env e) { + SumTrackingSetup(); + requireValidState(); + requireNoOverflow(e); + requireInvariant maxMagnitudeLeqWAD(operator, strategy); + requireInvariant encumberedMagnitudeLeqWAD(e, operator, strategy); + requireInvariant maxMagnitudeGEencumberedMagnitude(operator, strategy); + } + preserved modifyAllocations( + address op, + IAllocationManagerTypes.AllocateParams[] params + ) with (env e) { + // require (forall uint256 i. forall uint256 j. params[i].newMagnitudes[j] <= WAD(), "assume new magnitudes respect WAD()"); + + // AllocationManager.OperatorSet opSet = getOperatorSetFromKey(operatorKey); + // require (forall uint256 i. forall uint256 j. params[i].operatorSet.avs == opSet.avs => + // params[i].newMagnitudes[j] + currentContract.allocations[operator][operatorKey][strategy].pendingDiff <= WAD(), "assume new magnitude + current pending diff respect WAD()"); + + require (e.block.number < currentContract.allocations[operator][operatorKey][strategy].effectBlock, "require to not trigger a change of values throughout computation by _getUpdatedAllocation()"); + + SumTrackingSetup(); + requireValidState(); + requireNoOverflow(e); + requireInvariant maxMagnitudeLeqWAD(operator, strategy); + requireInvariant encumberedMagnitudeLeqWAD(e, operator, strategy); + requireInvariant maxMagnitudeGEencumberedMagnitude(operator, strategy); + } + } + +/// @title redistributionRecipient should not be dead address after a successful run +rule redistributionRecipientCannotBeDeadAddress(AllocationManager.OperatorSet operatorSet) { + env e; + + IAllocationManagerTypes.CreateSetParams[] params; + require (params.operatorSetId == operatorSet.id, "assume we're setting the recipient for the fixed operatorSet"); + + address[] recipients; + createRedistributingOperatorSets(e, operatorSet.avs, params, recipients); + + address finalRecipient = getRedistributionRecipient(e, operatorSet); + + assert params.length != 0 => finalRecipient != DEFAULT_BURN_ADDRESS(); +} /* This rule applies to all methods except modifyAllocation because this function makes valid transitions, @@ -39,7 +202,7 @@ filtered {f -> f.selector == sig:modifyAllocations(address,IAllocationManagerTyp env e; calldataarg args; requireValidState(); - require forall address operator . forall bytes32 setKey . forall address strategy . allocationsEffectBlock[operator][setKey][strategy] > e.block.number; + require forall address operator. forall bytes32 setKey. forall address strategy. currentContract.allocations[operator][setKey][strategy].effectBlock > e.block.number; require didMakeInvalidPendingDiffTransition == false; diff --git a/certora/specs/core/AllocationManagerSanity.spec b/certora/specs/core/AllocationManagerSanity.spec index 8a2d29be2f..25e4516605 100644 --- a/certora/specs/core/AllocationManagerSanity.spec +++ b/certora/specs/core/AllocationManagerSanity.spec @@ -1,6 +1,6 @@ import "../optimizations.spec"; -using AllocationManager as AllocationManager; +using AllocationManagerHarness as AllocationManager; methods { function AllocationManager.DEALLOCATION_DELAY() external returns(uint32) envfree; diff --git a/certora/specs/core/AllocationManagerValidState.spec b/certora/specs/core/AllocationManagerValidState.spec index 8ae63decc1..bac4a4934c 100644 --- a/certora/specs/core/AllocationManagerValidState.spec +++ b/certora/specs/core/AllocationManagerValidState.spec @@ -1,15 +1,16 @@ import "../optimizations.spec"; -using AllocationManager as AllocationManager; +using AllocationManagerHarness as AllocationManager; methods { function AllocationManager.DEALLOCATION_DELAY() external returns(uint32) envfree; function AllocationManager.getMaxMagnitude(address,address) external returns (uint64) envfree; - // external calls to AVSRegistrar. Note that the source does not have a proper implementation, the one available always reverts function _.registerOperator(address,address,uint32[],bytes) external => DISPATCHER(true); function _.deregisterOperator(address,address,uint32[]) external => DISPATCHER(true); function _.supportsAVS(address) external => DISPATCHER(true); + function getOperatorKeyFromSet(AllocationManagerHarness.OperatorSet) external returns (bytes32) envfree; + // external calls to Strategy contracts function _.underlyingToken() external => DISPATCHER(true); function _.withdraw(address,address,uint256) external => DISPATCHER(true); @@ -18,8 +19,6 @@ methods { function _.balanceOf(address) external => DISPATCHER(true); function _.transfer(address,uint256) external => DISPATCHER(true); - function OperatorSetLib.key(OperatorSetLib.OperatorSet memory os) internal returns (bytes32) => returnOperatorSetKey(os); // expect (bytes32); // return unique bytes32 that is not zero. - // internal math summary to avoid overflows from the tool; // function AllocationManager._addInt128(uint64 a, int128 b) internal returns (uint64) => cvlAddInt128(a, b); } @@ -30,20 +29,11 @@ function cvlAddInt128(uint64 a, int128 b) returns uint64 { return require_uint64(to_mathint(a) + to_mathint(b)); } -function returnOperatorSetKey(OperatorSetLib.OperatorSet os) returns bytes32 { - return idToKey[os.id]; -} - -ghost mapping(uint32 => bytes32) idToKey { - axiom forall uint32 id1 . forall uint32 id2 . (idToKey[id1] != to_bytes32(0) && idToKey[id2] != to_bytes32(0)) && - (id1 != id2 => idToKey[id1] != idToKey[id2]); -} - // ----------------------------------------- // Constants and Definitions // ----------------------------------------- -definition WAD() returns uint64 = 1000000000000000000; // definition uint64 WAD = 1e18 +definition WAD() returns uint64 = 10^18; // definition uint64 WAD = 1e18 definition inRegisteredSets(address operator, bytes32 value) returns bool = (registeredSetsIndexes[operator][value] != 0); @@ -461,13 +451,30 @@ function requireValidState() { requireInvariant encumberedMagnitudeEqSumOfCurrentMagnitudesAndPositivePending(); requireInvariant negativePendingDiffAtMostCurrentMagnitude(); requireInvariant noZeroKeyInDealocationQ(); - requireInvariant EndGreaterThenBegin(); + requireInvariant endGreaterThenBegin(); requireInvariant deallocationQueueDataOutOfBoundsAreNullified(); requireInvariant noPositivePendingDiffInDeallocationQ(); requireInvariant effectBlockZeroHasNoPendingDiff(); requireInvariant deallocationQueueDataUniqueness(); } +function requireNoOverflow(env e){ + requireInvariant maxMagnitudeHistoryKeysLessThanCurrentBlock(e); + requireInvariant deallocationQueueEffectBlocLessThanCurrBlockNumberPlushDelayPlusOne(e); + requireInvariant deallocationQueueEffectBlockAscendingOrder(e); + // prevent overflows in deallocationQueue + require (forall address _operator. forall address _strategy. (currentContract.deallocationQueue[_operator][_strategy]._end < max_uint64 - 1), "reasonable length of deallocationQueue"); + // assuming deallocation block indices dont overflow + require (forall address _operator . forall address _strategy . (deallocationQueueEndGhost[_operator][_strategy] < max_uint64 - 1), "reasonable length of deallocationQueue"); + // would happen around the year 2833 to get block number equal to half of max_uint32 + require (e.block.number < max_uint32 + AllocationManager.DEALLOCATION_DELAY + 1, "reasonable block numbers"); + require (e.block.number > 0, "reasonable block numbers"); + // prevent overflows for loop iter = 2 + require (forall address operator_. forall address strategy_. maxMagnitudeHistoryLengths[operator_][strategy_] < max_uint256 - 1, "reasonable length of snapshots"); + require (forall address operator_. forall address strategy_. currentContract._maxMagnitudeHistory[operator_][strategy_]._snapshots.length < max_uint256 - 1, "reasonable length of snapshots"); + +} + // Ensures consistency and correctness of the `registeredSets` mapping: // 1. `registeredSetsIndexes` must correctly map to `registeredSetsValues`. // 2. Non-zero indexes must lie within [1, ghostLengths[operator]]. @@ -617,7 +624,7 @@ invariant deallocationQueueDataUniqueness() // would happen around the year 2833 to get block number equal to half of max_uint32 require e.block.number < max_uint32 - AllocationManager.DEALLOCATION_DELAY - 1; require e.block.number > 0; - requireInvariant deallocationQueueEffectBlockAscesndingOrder(e); + requireInvariant deallocationQueueEffectBlockAscendingOrder(e); } } @@ -626,13 +633,24 @@ invariant deallocationQueueDataOutOfBoundsAreNullified() forall address operator . forall address strategy . forall int128 index . (!inBound(operator, strategy, index)) <=> deallocationQueueDataGhost[operator][strategy][index] == to_bytes32(0) { preserved { + requireInvariant endGreaterThenBegin(); + requireInvariant noZeroKeyInDealocationQ(); // assuming deallocation block indices dont overflow require forall address operator . forall address strategy . (deallocationQueueEndGhost[operator][strategy] < max_uint64 - 1); } + preserved modifyAllocations( + address op, + IAllocationManagerTypes.AllocateParams[] params + ) with (env e) { + requireInvariant endGreaterThenBegin(); + require forall address operator . forall address strategy . (deallocationQueueEndGhost[operator][strategy] < max_uint64 - 1), "assuming deallocation block indices dont overflow"; + bytes32 key = getOperatorKeyFromSet(params[0].operatorSet); + require (key != to_bytes32(0), "assume the stored operatorSet key is nonzero otw 0 entries are possible, relies on loop_iter 1"); + } } // Deallocation Queue Ordering: End Index ≥ Begin Index Invariant - helper Lemma -invariant EndGreaterThenBegin() +invariant endGreaterThenBegin() forall address operator . forall address strategy . deallocationQueueBeginGhost[operator][strategy] <= deallocationQueueEndGhost[operator][strategy] { preserved { @@ -644,7 +662,22 @@ invariant EndGreaterThenBegin() /// @title Non-Zero Keys in Deallocation Queue Invariant /// @property DeallocationQueue allocations uniqueness invariant noZeroKeyInDealocationQ() - forall address operator . forall address strategy . forall int128 index . inBound(operator, strategy, index) => deallocationQueueDataGhost[operator][strategy][index] != to_bytes32(0); + forall address operator . forall address strategy . forall int128 index . (inBound(operator, strategy, index) <=> deallocationQueueDataGhost[operator][strategy][index] != to_bytes32(0)) + { + preserved { + requireInvariant endGreaterThenBegin(); + require forall address operator . forall address strategy . (deallocationQueueEndGhost[operator][strategy] < max_uint64 - 1), "assuming deallocation block indices dont overflow"; + } + preserved modifyAllocations( + address op, + IAllocationManagerTypes.AllocateParams[] params + ) with (env e) { + requireInvariant endGreaterThenBegin(); + require forall address operator . forall address strategy . (deallocationQueueEndGhost[operator][strategy] < max_uint64 - 1), "assuming deallocation block indices dont overflow"; + bytes32 key = getOperatorKeyFromSet(params[0].operatorSet); + require (key != to_bytes32(0), "assume the stored operatorSet key is nonzero otw 0 entries are possible, relies on loop_iter 1"); + } + } /// @title Allocations in the deallocation queue have their effect blocks equal at most the latest block number + DEALLOCATION_DELAY + 1. /// @property Deallocation Queue Effect Block Timing Bound Invariant. @@ -665,7 +698,7 @@ invariant deallocationQueueEffectBlocLessThanCurrBlockNumberPlushDelayPlusOne(en // assuming deallocation block indices dont overflow require forall address operator . forall address strategy . (deallocationQueueEndGhost[operator][strategy] < max_uint64 - 1); - requireInvariant deallocationQueueEffectBlockAscesndingOrder(e1); + requireInvariant deallocationQueueEffectBlockAscendingOrder(e1); } } @@ -676,7 +709,7 @@ except when an effect block is zero, which must have been less than or equal to This prevents out-of-order deallocations and ensures a valid execution sequence. */ /// @property Deallocation Queue Effect Block Ascending Order Invariant -invariant deallocationQueueEffectBlockAscesndingOrder(env e1) +invariant deallocationQueueEffectBlockAscendingOrder(env e1) forall address operator . forall address strategy . forall int128 index1 . forall int128 index2 . (index1 <= index2) && inBound(operator, strategy, index1) && inBound(operator, strategy, index2) => ((allocationsEffectBlock[operator][deallocationQueueDataGhost[operator][strategy][index1]][strategy] <= @@ -734,6 +767,6 @@ invariant noPositivePendingDiffInDeallocationQ() // would happen around the year 2833 to get block number equal to half of max_uint32 require e.block.number < max_uint32 - AllocationManager.DEALLOCATION_DELAY - 1; require e.block.number > 0; - requireInvariant deallocationQueueEffectBlockAscesndingOrder(e); + requireInvariant deallocationQueueEffectBlockAscendingOrder(e); } } diff --git a/certora/specs/core/DelegationManager.spec b/certora/specs/core/DelegationManager.spec index 4c8d3d7c0a..e66a83c2bd 100644 --- a/certora/specs/core/DelegationManager.spec +++ b/certora/specs/core/DelegationManager.spec @@ -1,6 +1,6 @@ import "../ptaHelpers.spec"; -using DelegationManager as DelegationManager; +using DelegationManagerHarness as DelegationManager; methods { //// External Calls @@ -57,7 +57,6 @@ methods { function isDelegated(address staker) external returns (bool) envfree; function isOperator(address operator) external returns (bool) envfree; function delegationApproverSaltIsSpent(address delegationApprover, bytes32 salt) external returns (bool) envfree; - function owner() external returns (address) envfree; function strategyManager() external returns (address) envfree; function eigenPodManager() external returns (address) envfree; function calculateWithdrawalRoot(IDelegationManagerTypes.Withdrawal) external returns (bytes32) envfree; @@ -134,13 +133,6 @@ hook Sload address delegationApprover DelegationManager._operatorDetails[KEY add require delegationApprover == operatorDetailsDelegationApproversMirror[operator]; } -// verify that anyone who is registered as an operator is also always delegated to themselves -// the zero address is an exception to this rule, since it is always "delegated to itself" but not an operator -/// @title Verifies that operators delegates to themselves. -/// @property Operators delegates to themselves -invariant operatorsAlwaysDelegatedToSelf(address operator) - operatorDetailsDelegationApproversMirror[operator] != 0 => DelegationManager.delegatedTo[operator] == operator; - // verify that once registered as an operator, a person cannot 'unregister' from being an operator // proving this rule in concert with 'operatorsAlwaysDelegatedToSelf' proves that an operator can never change their delegation // Certora: The prover does not need the precondition `operatorsAlwaysDelegatedToSelf` to prove the rule. @@ -245,47 +237,50 @@ rule canOnlyDelegateWithSpecificFunctions(address staker) { } } -rule sharesBecomeDelegatedWhenStakerDelegates(address operator, address staker, address strategy) { - // filter out zero address (not a valid operator) - require(operator != 0); - // assume the staker begins as undelegated - require(!isDelegated(staker)); - mathint stakerDelegateableSharesInStrategy = get_stakerDelegateableShares(staker, strategy); - mathint operatorSharesBefore = get_operatorShares(operator, strategy); - // perform arbitrary function call - method f; - env e; - calldataarg arg; - // Certora: The rule does not hold if uncommented -// f(e, arg); - mathint operatorSharesAfter = get_operatorShares(operator, strategy); - if (delegatedTo(staker) == operator) { - assert(operatorSharesAfter == operatorSharesBefore + stakerDelegateableSharesInStrategy, "operator shares did not increase appropriately"); - } else { - assert(operatorSharesAfter == operatorSharesBefore, "operator shares changed inappropriately"); - } -} -rule sharesBecomeUndelegatedWhenStakerUndelegates(address operator, address staker, address strategy) { - // filter out zero address (not a valid operator) - require(operator != 0); - // assume the staker begins as delegated to the operator - require(delegatedTo(staker) == operator); - mathint stakerDelegateableSharesInStrategy = get_stakerDelegateableShares(staker, strategy); - mathint operatorSharesBefore = get_operatorShares(operator, strategy); - // perform arbitrary function call - method f; - env e; - calldataarg arg; - // Certora: The rule does not hold if uncommented -// f(e, arg); - mathint operatorSharesAfter = get_operatorShares(operator, strategy); - if (!isDelegated(staker)) { - assert(operatorSharesAfter == operatorSharesBefore - stakerDelegateableSharesInStrategy, "operator shares did not decrease appropriately"); - } else { - assert(operatorSharesAfter == operatorSharesBefore, "operator shares changed inappropriately"); - } -} +// unfinished +// rule sharesBecomeDelegatedWhenStakerDelegates(address operator, address staker, address strategy) { +// // filter out zero address (not a valid operator) +// require(operator != 0); +// // assume the staker begins as undelegated +// require(!isDelegated(staker)); +// mathint stakerDelegateableSharesInStrategy = get_stakerDelegateableShares(staker, strategy); +// mathint operatorSharesBefore = get_operatorShares(operator, strategy); +// // perform arbitrary function call +// method f; +// env e; +// calldataarg arg; +// // Certora: The rule does not hold if uncommented +// // f(e, arg); +// mathint operatorSharesAfter = get_operatorShares(operator, strategy); +// if (delegatedTo(staker) == operator) { +// assert(operatorSharesAfter == operatorSharesBefore + stakerDelegateableSharesInStrategy, "operator shares did not increase appropriately"); +// } else { +// assert(operatorSharesAfter == operatorSharesBefore, "operator shares changed inappropriately"); +// } +// } + +// unfinished +// rule sharesBecomeUndelegatedWhenStakerUndelegates(address operator, address staker, address strategy) { +// // filter out zero address (not a valid operator) +// require(operator != 0); +// // assume the staker begins as delegated to the operator +// require(delegatedTo(staker) == operator); +// mathint stakerDelegateableSharesInStrategy = get_stakerDelegateableShares(staker, strategy); +// mathint operatorSharesBefore = get_operatorShares(operator, strategy); +// // perform arbitrary function call +// method f; +// env e; +// calldataarg arg; +// // Certora: The rule does not hold if uncommented +// // f(e, arg); +// mathint operatorSharesAfter = get_operatorShares(operator, strategy); +// if (!isDelegated(staker)) { +// assert(operatorSharesAfter == operatorSharesBefore - stakerDelegateableSharesInStrategy, "operator shares did not decrease appropriately"); +// } else { +// assert(operatorSharesAfter == operatorSharesBefore, "operator shares changed inappropriately"); +// } +// } rule newWithdrawalsHaveCorrectStartBlock() { IDelegationManagerTypes.Withdrawal queuedWithdrawal; @@ -319,7 +314,7 @@ rule withdrawalDelayIsEnforced() { ); } -/* +/* unfinished rule batchEquivalence { env e; storage initial = lastStorage; diff --git a/certora/specs/core/DelegationManagerValidState.spec b/certora/specs/core/DelegationManagerValidState.spec index ec211e6b64..1e3ce5e185 100644 --- a/certora/specs/core/DelegationManagerValidState.spec +++ b/certora/specs/core/DelegationManagerValidState.spec @@ -1,6 +1,6 @@ import "../ptaHelpers.spec"; -using DelegationManager as DelegationManager; +using DelegationManagerHarness as DelegationManager; methods { //// External Calls @@ -49,6 +49,11 @@ methods { function get_stakerDelegateableShares(address,address) external returns (uint256) envfree; function get_min_withdrawal_delay_blocks() external returns (uint32) envfree; + // external calls to AVSRegistrar. Note that the source does not have a proper implementation, the one available always reverts + function _.registerOperator(address,address,uint32[],bytes) external => DISPATCHER(true); + function _.deregisterOperator(address,address,uint32[]) external => DISPATCHER(true); + function _.supportsAVS(address) external => DISPATCHER(true); + //envfree functions function delegatedTo(address) external returns (address) envfree; function delegationApprover(address operator) external returns (address) envfree; @@ -56,7 +61,6 @@ methods { function isDelegated(address staker) external returns (bool) envfree; function isOperator(address operator) external returns (bool) envfree; function delegationApproverSaltIsSpent(address delegationApprover, bytes32 salt) external returns (bool) envfree; - function owner() external returns (address) envfree; function strategyManager() external returns (address) envfree; function eigenPodManager() external returns (address) envfree; function calculateWithdrawalRoot(IDelegationManagerTypes.Withdrawal) external returns (bytes32) envfree; @@ -251,12 +255,12 @@ hook Sload uint256 index DelegationManager._stakerQueuedWithdrawalRoots[KEY addr // ----------------------------------------- function requireDelegationManagerValidState() { - requireInvariant operatorDelegatesToThemselves(); + // requireInvariant operatorDelegatesToThemselves(); // violated on delegateTo requireInvariant stakerQueuedWithdrawalRootsInvariant(); requireInvariant cumulativeScaledSharesHistoryKeysMonotonicInc(); requireInvariant cumulativeScaledSharesHistoryPastLengthNullified(); requireInvariant cumulativeScaledSharesMonotonicallyIncreasing(); - requireInvariant queuedWithdrawalsCorrect(); + // requireInvariant queuedWithdrawalsCorrect(); // violated on completeQueueWithdrawal } /// @title @@ -318,21 +322,26 @@ For a given staker, all roots existing in _stakerQueuedWithdrawalRoots also exis _queuedWithdrawals[withdrawalRoot] returns the Withdrawal struct / staker != address(0) pendingWithdrawals[withdrawalRoot] returns True */ +// violated in completeQueuedWithdrawal() and completeQueuedWithdrawals() /// @property Queued Withdrawal Registration Consistency Invariant -invariant queuedWithdrawalsCorrect() - forall address staker . forall bytes32 root . inRootsSets(staker, root) => - pendingWithdrawalsMirror[root] && queuedWithdrawalsStakesrGhost[root] != 0 - { - preserved { - requireInvariant stakerQueuedWithdrawalRootsInvariant(); - } - } +// invariant queuedWithdrawalsCorrect() +// forall address staker . forall bytes32 root . inRootsSets(staker, root) => +// pendingWithdrawalsMirror[root] && queuedWithdrawalsStakesrGhost[root] != 0 +// { +// preserved { +// requireInvariant stakerQueuedWithdrawalRootsInvariant(); +// } +// } /// @title Verifies that operators delegates to themselves. /// @property Operators delegates to themselves +/// violated by delegateTo invariant operatorDelegatesToThemselves() - forall address operator . operatorDetailsDelegationApproversMirror[operator] != 0 => DelegationManager.delegatedTo[operator] == operator; - + forall address operator . operatorDetailsDelegationApproversMirror[operator] != 0 => DelegationManager.delegatedTo[operator] == operator { + preserved with (env e){ + require (e.msg.sender != 0, "0 address cannot be an operator"); + } + } /// @title Operator Cannot Deregister /// @property Operator Cannot Deregister @@ -353,23 +362,24 @@ filtered{f -> !f.isView} assert delegatedToPre == account => delegatedToPost == account; } -/// @title depositScalingFactor is initialized as WAD and only increases on further deposits. -/// @property depositScalingFactor Monotonic Increasing -rule depositScalingFactorMonotonicInc(method f, address staker, address strategy) -filtered{f -> !f.isView} -{ - env e; - calldataarg args; +// /// @title depositScalingFactor is initialized as WAD and only increases on further deposits. +// /// @property depositScalingFactor Monotonic Increasing +// exceptions: delegateTo, increaseDelegatedShares and registerAsOperator can decrease dsf +// rule depositScalingFactorMonotonicInc(method f, address staker, address strategy) +// filtered{f -> !f.isView} +// { +// env e; +// calldataarg args; - uint256 depositScalingFactorPre = scalingFactorsGhost[staker][strategy]; - require depositScalingFactorPre >= WAD(); +// uint256 depositScalingFactorPre = scalingFactorsGhost[staker][strategy]; +// require depositScalingFactorPre >= WAD(); - f(e, args); +// f(e, args); - uint256 depositScalingFactorPost = scalingFactorsGhost[staker][strategy]; +// uint256 depositScalingFactorPost = scalingFactorsGhost[staker][strategy]; - assert depositScalingFactorPost >= depositScalingFactorPre; -} +// assert depositScalingFactorPost >= depositScalingFactorPre; +// } // /// @title For a given (Staker, Strategy), withdrawableShares <= depositShares. // /// @property Withdrawable Shares Cannot Exceed Deposited Shares. @@ -420,5 +430,6 @@ filtered{f -> !f.isView} assert depositScalingFactorPost != depositScalingFactorPre => f.selector == sig:increaseDelegatedShares(address, address, uint256, uint256).selector || f.selector == sig:delegateTo(address, ISignatureUtilsMixinTypes.SignatureWithExpiry, bytes32).selector || - f.selector == sig:completeQueuedWithdrawals(IDelegationManagerTypes.Withdrawal[], address[][], bool[]).selector; + f.selector == sig:completeQueuedWithdrawals(IDelegationManagerTypes.Withdrawal[], address[][], bool[]).selector || + f.selector == sig:registerAsOperator(address,uint32,string).selector; } diff --git a/certora/specs/core/SlashEscrowFactory.spec b/certora/specs/core/SlashEscrowFactory.spec new file mode 100644 index 0000000000..e1176ef7cc --- /dev/null +++ b/certora/specs/core/SlashEscrowFactory.spec @@ -0,0 +1,281 @@ +import "../erc20cvl.spec"; +import "../libraries/EnumerableSet.spec"; +using SlashEscrowFactoryHarness as factory; +using SlashEscrow as escrow; +using StrategyManager as StrategyManager; +using OperatorSetLib as OperatorSetLib; +using AllocationManager as AllocationManager; + +use invariant _pendingSlashIdsInvariant; +use invariant _pendingStrategiesForSlashIdInvariant; +use invariant _pendingOperatorSetsInvariant; + +methods { + // Strategy methods + function _.underlyingToken() external => DISPATCHER(true); + function _.withdraw(address,address,uint256) external => DISPATCHER(true); + + // SlashEscrow + function _.releaseTokens(address, address, SlashEscrowFactoryHarness.OperatorSet,uint256, address, address) external => DISPATCHER(true); + + unresolved external in StrategyManager._ => DISPATCH [ + getSlashEscrow(SlashEscrowFactoryHarness.OperatorSet, uint256), + StrategyBase.withdraw(address,address,uint256) + ] default HAVOC_ECF; + + // SlashEscrowFactory methods + function initiateSlashEscrow(SlashEscrowFactoryHarness.OperatorSet, uint256, address) external; + function releaseSlashEscrow(SlashEscrowFactoryHarness.OperatorSet, uint256) external; + function releaseSlashEscrowByStrategy(SlashEscrowFactoryHarness.OperatorSet, uint256, address) external; + function getSlashEscrow(SlashEscrowFactoryHarness.OperatorSet, uint256) external returns (address) envfree; + function isDeployedSlashEscrow(SlashEscrowFactoryHarness.OperatorSet, uint256) external returns (bool) envfree; + function getEscrowStartBlock(SlashEscrowFactoryHarness.OperatorSet, uint256) external returns (uint256) envfree; + function getEscrowCompleteBlock(SlashEscrowFactoryHarness.OperatorSet, uint256) external returns (uint32) envfree; + function getStrategyEscrowDelay(address) external returns (uint32) envfree; + function getGlobalEscrowDelay() external returns (uint32) envfree; + function isEscrowPaused(SlashEscrowFactoryHarness.OperatorSet, uint256) external returns (bool) envfree; + function isPendingSlashId(SlashEscrowFactoryHarness.OperatorSet, uint256) external returns (bool) envfree; + function getTotalPendingSlashIds(SlashEscrowFactoryHarness.OperatorSet) external returns (uint256) envfree; + function getTotalPendingStrategiesForSlashId(SlashEscrowFactoryHarness.OperatorSet, uint256 slashId) external returns (uint256) envfree; + function getPendingUnderlyingAmountForStrategy(SlashEscrowFactoryHarness.OperatorSet, uint256 slashId, address strategy) external returns (uint256) envfree; + function computeSlashEscrowSalt(SlashEscrowFactoryHarness.OperatorSet, uint256 slashId) external returns (bytes32) envfree; + function getTotalPendingOperatorSets() external returns (uint256) envfree; + + //harness methods + function isStrategyPending(SlashEscrowFactoryHarness.OperatorSet operatorSet, uint256 slashId, address strategy) external returns (bool) envfree; + function getOperatorSetKey(SlashEscrowFactoryHarness.OperatorSet) external returns (bytes32) envfree; + + function getPendingStrategiesForSlashId(SlashEscrowFactoryHarness.OperatorSet, uint256) external returns (address[]) envfree; + + // SlashEscrow methods + function releaseTokens(address, address, SlashEscrowFactoryHarness.OperatorSet, uint256, address, address) external; + + // StrategyManager methods + function clearBurnOrRedistributableShares(SlashEscrowFactoryHarness.OperatorSet, uint256) external; + function clearBurnOrRedistributableSharesByStrategy(SlashEscrowFactoryHarness.OperatorSet, uint256, address) external; + +} + +// Rule: Escrow deployment determinism +rule escrowDeploymentDeterminism(env e1, env e2) { + SlashEscrowFactoryHarness.OperatorSet operatorSet; + uint256 slashId; + + bytes32 salt1 = computeSlashEscrowSalt(operatorSet, slashId); + bytes32 salt2 = computeSlashEscrowSalt(operatorSet, slashId); + + assert salt1 == salt2; + + address escrow1 = getSlashEscrow(operatorSet, slashId); + address escrow2 = getSlashEscrow(operatorSet, slashId); + + assert escrow1 == escrow2; +} + + +// @title initiateSlashEscrow starts a countdown (sets start block) +rule initiateSlashEscrowStartsCountdown( + SlashEscrowFactoryHarness.OperatorSet operatorSet, + uint256 slashId, + address strategy +) { + env e; + + bool isAlreadyDeployed = isDeployedSlashEscrow(operatorSet, slashId); + // Call initiateSlashEscrow + initiateSlashEscrow(e, operatorSet, slashId, strategy); + + // Postcondition: Start block is set to current block + uint256 startBlockAfter = getEscrowStartBlock(operatorSet, slashId); + + assert !isAlreadyDeployed => startBlockAfter == require_uint32(e.block.number); +} + +// @title Countdown is identical for all strategies in same slash +rule countdownIdenticalForSameSlash( + SlashEscrowFactoryHarness.OperatorSet operatorSet, + uint256 slashId, + address strategy1, + address strategy2 +) { + env e1; + env e2; + require e1.block.number == e2.block.number; // Same block + + // First strategy initiation + initiateSlashEscrow(e1, operatorSet, slashId, strategy1); + uint256 startBlock1 = getEscrowStartBlock(operatorSet, slashId); + + // Second strategy initiation in same block + initiateSlashEscrow(e2, operatorSet, slashId, strategy2); + uint256 startBlock2 = getEscrowStartBlock(operatorSet, slashId); + + // Both strategies must have the same start block + assert startBlock1 == startBlock2; +} + +// @title releaseSlashEscrow can only be called after delays have passed +rule releaseSlashEscrowOnlyAfterDelay( + SlashEscrowFactoryHarness.OperatorSet operatorSet, + uint256 slashId +) { + env e; + + // Preconditions + require isPendingSlashId(operatorSet, slashId); + require !isEscrowPaused(operatorSet, slashId); + + uint32 completeBlock = getEscrowCompleteBlock(operatorSet, slashId); + + // If current block is before complete block, release should revert + releaseSlashEscrow@withrevert(e, operatorSet, slashId); + assert e.block.number < completeBlock => lastReverted; +} + +// @title releaseSlashEscrowByStrategy can only be called after delays have passed +rule releaseSlashEscrowByStrategyOnlyAfterDelay( + SlashEscrowFactoryHarness.OperatorSet operatorSet, + uint256 slashId, + address strategy +) { + env e; + + // Preconditions + require isPendingSlashId(operatorSet, slashId); + require !isEscrowPaused(operatorSet, slashId); + + uint32 completeBlock = getEscrowCompleteBlock(operatorSet, slashId); + + // If current block is before complete block, release should revert + releaseSlashEscrowByStrategy@withrevert(e, operatorSet, slashId, strategy); + assert e.block.number < completeBlock => lastReverted; +} + +// @title After successful release, slash ID is no longer pending +rule releaseSlashEscrowRemovesPendingStatus( + SlashEscrowFactoryHarness.OperatorSet operatorSet, + uint256 slashId +) { + env e; + + // Release the escrow + releaseSlashEscrow(e, operatorSet, slashId); + + // Slash ID should no longer be pending (if all strategies were processed) + assert getPendingStrategiesForSlashId(operatorSet, slashId).length == 0 => !isPendingSlashId(operatorSet, slashId); +} + +// Parametric rule: State consistency across operations +rule stateConsistencyAcrossOperations(env e, method f) filtered { f-> !f.isView }{ + SlashEscrowFactoryHarness.OperatorSet operatorSet; + + requireInvariant _pendingSlashIdsInvariant(); + requireInvariant _pendingStrategiesForSlashIdInvariant(); + requireInvariant _pendingOperatorSetsInvariant(); + + uint256 pendingSetsBefore = getTotalPendingOperatorSets(); + uint256 pendingSlashIdsBefore = getTotalPendingSlashIds(operatorSet); + + calldataarg args; + f(e, args); + + uint256 pendingSetsAfter = getTotalPendingOperatorSets(); + uint256 pendingSlashIdsAfter = getTotalPendingSlashIds(operatorSet); + + // Pending counts should only increase with initiateSlashEscrow + assert f.selector == sig:initiateSlashEscrow(SlashEscrowFactoryHarness.OperatorSet,uint256,address).selector => + (pendingSetsAfter >= pendingSetsBefore && pendingSlashIdsAfter >= pendingSlashIdsBefore); + + // Pending counts should only decrease with release functions + assert (f.selector == sig:releaseSlashEscrow(SlashEscrowFactoryHarness.OperatorSet,uint256).selector || + f.selector == sig:releaseSlashEscrowByStrategy(SlashEscrowFactoryHarness.OperatorSet,uint256,address).selector) => + (pendingSetsAfter <= pendingSetsBefore && pendingSlashIdsAfter <= pendingSlashIdsBefore); +} + + +// @title Paused escrows cannot be released +rule pausedEscrowsCannotBeReleased( + SlashEscrowFactoryHarness.OperatorSet operatorSet, + uint256 slashId +) { + env e; + + // Precondition: Escrow is paused + require isEscrowPaused(operatorSet, slashId); + + // Attempt to release should revert + releaseSlashEscrow@withrevert(e, operatorSet, slashId); + assert lastReverted; + + // Also test strategy-specific release + address strategy; + releaseSlashEscrowByStrategy@withrevert(e, operatorSet, slashId, strategy); + assert lastReverted; +} + +// @title Slash escrow address is deterministic +rule slashEscrowAddressDeterministic( + env e, + OperatorSetLib.OperatorSet operatorSet1, + OperatorSetLib.OperatorSet operatorSet2, + uint256 slashId1, + uint256 slashId2, + address strategy +) { + + initiateSlashEscrow(e, operatorSet1, slashId1, strategy); + initiateSlashEscrow(e, operatorSet2, slashId2, strategy); + + address escrow1 = getSlashEscrow(operatorSet1, slashId1); + address escrow2 = getSlashEscrow(operatorSet2, slashId2); + + // Same operator set and slash ID should produce same escrow address + assert (getOperatorSetKey(operatorSet1) == getOperatorSetKey(operatorSet2) && slashId1 == slashId2) => (escrow1 == escrow2); +} + +// @title Multiple initiations of same slash don't change start block +rule multipleInitiationsSameStartBlock( + OperatorSetLib.OperatorSet operatorSet, + uint256 slashId, + address strategy1, + address strategy2 +) { + env e1; + env e2; + require e1.block.number == e2.block.number; + + // First initiation + initiateSlashEscrow(e1, operatorSet, slashId, strategy1); + uint256 startBlock1 = getEscrowStartBlock(operatorSet, slashId); + + // Second initiation with different strategy + initiateSlashEscrow(e2, operatorSet, slashId, strategy2); + uint256 startBlock2 = getEscrowStartBlock(operatorSet, slashId); + + // Start block should remain the same + assert startBlock1 == startBlock2; +} + +// @title Only strategy manager can call initiateSlashEscrow +rule onlyStrategyManagerCanInitiate( + SlashEscrowFactoryHarness.OperatorSet operatorSet, + uint256 slashId, + address strategy +) { + env e; + + // If caller is not strategy manager, call should revert + initiateSlashEscrow@withrevert(e, operatorSet, slashId, strategy); + assert e.msg.sender != StrategyManager => lastReverted; +} + +// @title Start block is always set for pending slash IDs +invariant startBlockSetForPendingSlashIds(SlashEscrowFactoryHarness.OperatorSet operatorSet, uint256 slashId) + isPendingSlashId(operatorSet, slashId) => getEscrowStartBlock(operatorSet, slashId) > 0 { + preserved with (env e) { + require (require_uint32(e.block.number) != 0, "uint32(block.number) used as a starting block for escrow, would overflow in approx 1.6k years"); + requireInvariant _pendingSlashIdsInvariant(); + requireInvariant _pendingStrategiesForSlashIdInvariant(); + requireInvariant _pendingOperatorSetsInvariant(); + } + } \ No newline at end of file diff --git a/certora/specs/core/StrategyManager.spec b/certora/specs/core/StrategyManager.spec index 88574489d7..c19bbe535c 100644 --- a/certora/specs/core/StrategyManager.spec +++ b/certora/specs/core/StrategyManager.spec @@ -89,8 +89,8 @@ invariant arrayExhibitsProperties(address staker) /** * a staker's amount of shares in a strategy (i.e. `stakerDepositShares[staker][strategy]`) should only increase when -* `depositIntoStrategy`, `depositIntoStrategyWithSignature`, or `depositBeaconChainETH` has been called -* *OR* when completing a withdrawal +* `depositIntoStrategy`, `depositIntoStrategyWithSignature`, +* `withdrawSharesAsTokens`, or `addShares` is called. */ definition methodCanIncreaseShares(method f) returns bool = f.selector == sig:depositIntoStrategy(address,address,uint256).selector @@ -100,7 +100,7 @@ definition methodCanIncreaseShares(method f) returns bool = /** * a staker's amount of shares in a strategy (i.e. `stakerDepositShares[staker][strategy]`) should only decrease when -* `queueWithdrawal`, `slashShares`, or `recordBeaconChainETHBalanceUpdate` has been called +`removeDepositShares` is called */ definition methodCanDecreaseShares(method f) returns bool = f.selector == sig:removeDepositShares(address,address,uint256).selector; @@ -117,10 +117,11 @@ rule sharesAmountsChangeOnlyWhenAppropriateFunctionsCalled(address staker, addre } /** -* Verifies that the `totalShares` returned by an Strategy increases appropriately when new Strategy shares are issued by the StrategyManager +* Verifies that the `totalShares` returned by a Strategy increases appropriately when new Strategy shares are issued by the StrategyManager * contract (specifically as a result of a call to `StrategyManager.depositIntoStrategy` or `StrategyManager.depositIntoStrategyWithSignature`). -* This rule excludes the `addShares` and `removeShares` functions, since these are called only by the DelegationManager, and do not +* This rule excludes the `addShares` function, since this is called only by the DelegationManager, and do not * "create new shares", but rather represent existing shares being "moved into a withdrawal". +* for the `addShares` case, we instead check that the totalShares value does not change as a result of the call */ rule newSharesIncreaseTotalShares(address strategy) { method f; @@ -129,7 +130,6 @@ rule newSharesIncreaseTotalShares(address strategy) { uint256 totalSharesBefore = totalShares(strategy); if ( f.selector == sig:addShares(address, address, uint256).selector -// || f.selector == sig:removeShares(address, address, uint256).selector ) { uint256 totalSharesAfter = totalShares(strategy); assert(totalSharesAfter == totalSharesBefore, "total shares changed unexpectedly"); @@ -181,9 +181,29 @@ rule safeApprovalUse(address user) { bytes signature; require balanceOfCVL(token, strategy) + amount <= max_uint256; // Require no overflows on balances as valid env assumption depositIntoStrategyWithSignature(e, strategy, token, amount, staker, expiry, signature); - } + } else if (f.selector == sig:clearBurnOrRedistributableSharesByStrategy(StrategyManager.OperatorSet,uint256,address).selector) { + StrategyManager.OperatorSet operatorSet; + uint256 slashId; + address strategy; + + // User is not the target strategy. + // (This withrdraws from that strategy) + require user != strategy; + + clearBurnOrRedistributableSharesByStrategy(e, operatorSet, slashId, strategy); + + } else if (f.selector == sig:clearBurnOrRedistributableShares(StrategyManager.OperatorSet,uint256).selector) { + StrategyManager.OperatorSet operatorSet; + uint256 slashId; + + // User is not one of the strategies. + // (This withrdraws from zero or more strategies) + require user != StrategyBase; + require user != currentContract; + + clearBurnOrRedistributableShares(e, operatorSet, slashId); // otherwise just perform an arbitrary function call - else { + } else { calldataarg args; f(e,args); } diff --git a/certora/specs/erc20cvl.spec b/certora/specs/erc20cvl.spec index d30e12b456..6dd45767d0 100644 --- a/certora/specs/erc20cvl.spec +++ b/certora/specs/erc20cvl.spec @@ -10,6 +10,7 @@ methods { function _.transfer(address a, uint256 x) external with (env e) => transferCVL(calledContract, e.msg.sender, a, x) expect bool; function _.transferFrom(address a, address b, uint256 x) external with (env e) => transferFromCVL(calledContract, e.msg.sender, a, b, x) expect bool; function _.safeTransferFrom(address a, address b, uint256 x) external with (env e) => safeTransferFromCVL(calledContract, e.msg.sender, a, b, x) expect void; + function _.safeTransfer(address to, uint256 x) external with (env e) => safeTransferCVL(calledContract, e.msg.sender, to, x) expect void; } @@ -62,6 +63,12 @@ function safeTransferFromCVL(address t, address spender, address from, address t transferFromCVL(t, spender, from, to, amount); } +function safeTransferCVL(address t, address from, address to, uint256 amount) { + bool nondetSuccess; + if (!nondetSuccess) require false; + transferCVL(t, from, to, amount); +} + function transferCVL(address t, address from, address to, uint256 amount) returns bool { // should be randomly reverting xxx bool nondetSuccess; diff --git a/certora/specs/libraries/EnumerableSet.spec b/certora/specs/libraries/EnumerableSet.spec new file mode 100644 index 0000000000..79acd03899 --- /dev/null +++ b/certora/specs/libraries/EnumerableSet.spec @@ -0,0 +1,178 @@ +methods { +} + +// GHOST COPIES: +// For every storage variable we add a ghost field that is kept synchronized by hooks. +// The ghost fields can be accessed by the spec, even inside quantifiers. + +// ghost field for the values array +ghost mapping(bytes32 => mapping (mathint => bytes32)) ghostValues_pendingSlashIds { + init_state axiom forall bytes32 key. forall mathint x. ghostValues_pendingSlashIds[key][x] == to_bytes32(0); +} +// ghost field for the indexes map +ghost mapping(bytes32 => mapping (bytes32 => uint256)) ghostIndexes_pendingSlashIds { + init_state axiom forall bytes32 key. forall bytes32 x. ghostIndexes_pendingSlashIds[key][x] == 0; +} +// ghost field for the length of the values array (stored in offset 0) +ghost mapping(bytes32 => uint256) ghostLength_pendingSlashIds { + init_state axiom forall bytes32 key. ghostLength_pendingSlashIds[key] == 0; + // assumption: it's infeasible to grow the list to these many elements. + axiom forall bytes32 key. ghostLength_pendingSlashIds[key] < max_uint256; +} + +// HOOKS +// Store hook to synchronize ghostLength_pendingSlashIds with the length of the set._inner._values array. +hook Sstore currentContract._pendingSlashIds[KEY bytes32 key]._inner._values.length uint256 newLength { + ghostLength_pendingSlashIds[key] = newLength; +} +// Store hook to synchronize ghostValues_pendingSlashIds array with _pendingSlashIds._inner._values. +hook Sstore currentContract._pendingSlashIds[KEY bytes32 key]._inner._values[INDEX uint256 index] bytes32 newValue { + ghostValues_pendingSlashIds[key][index] = newValue; +} +// Store hook to synchronize ghostIndexes array with _pendingSlashIds._inner._indexes. +hook Sstore currentContract._pendingSlashIds[KEY bytes32 key]._inner._indexes[KEY bytes32 value] uint256 newIndex { + ghostIndexes_pendingSlashIds[key][value] = newIndex; +} + +// The load hooks can use require to ensure that the ghost field has the same information as the storage. +// The require is sound, since the store hooks ensure the contents are always the same. However we cannot +// prove that with invariants, since this would require the invariant to read the storage for all elements +// and neither storage access nor function calls are allowed in quantifiers. +// +// By following this simple pattern it is ensured that the ghost state and the storage are always the same +// and that the solver can use this knowledge in the proofs. + +// Load hook to synchronize ghostLength_pendingSlashIds with the length of the _pendingSlashIds._inner._values array. +hook Sload uint256 length currentContract._pendingSlashIds[KEY bytes32 key]._inner._values.length { + require ghostLength_pendingSlashIds[key] == length; +} +hook Sload bytes32 value currentContract._pendingSlashIds[KEY bytes32 key]._inner._values[INDEX uint256 index] { + require ghostValues_pendingSlashIds[key][index] == value; +} +hook Sload uint256 index currentContract._pendingSlashIds[KEY bytes32 key]._inner._indexes[KEY bytes32 value] { + require ghostIndexes_pendingSlashIds[key][value] == index; +} + +// INVARIANTS + +// This is the main invariant stating that the indexes and values always match: +// values[indexes[v] - 1] = v for all values v in the _pendingSlashIds +// and indexes[values[i]] = i+1 for all valid indexes i. + +invariant _pendingSlashIdsInvariant() + (forall bytes32 key. forall uint256 index. 0 <= index && index < ghostLength_pendingSlashIds[key] => to_mathint(ghostIndexes_pendingSlashIds[key][ghostValues_pendingSlashIds[key][index]]) == index + 1) + && (forall bytes32 key. forall bytes32 value. ghostIndexes_pendingSlashIds[key][value] == 0 || + (ghostValues_pendingSlashIds[key][ghostIndexes_pendingSlashIds[key][value] - 1] == value && ghostIndexes_pendingSlashIds[key][value] >= 1 && ghostIndexes_pendingSlashIds[key][value] <= ghostLength_pendingSlashIds[key])); + + + + + + +// ghost field for the values array +ghost mapping(bytes32 => mapping (uint256 => mapping (mathint => bytes32))) ghostValues_pendingStrategiesForSlashId { + init_state axiom forall bytes32 key. forall uint256 slashId. forall mathint x. ghostValues_pendingStrategiesForSlashId[key][slashId][x] == to_bytes32(0); +} +// ghost field for the indexes map +ghost mapping(bytes32 => mapping (uint256 => mapping (bytes32 => uint256))) ghostIndexes_pendingStrategiesForSlashId { + init_state axiom forall bytes32 key. forall uint256 slashId. forall bytes32 x. ghostIndexes_pendingStrategiesForSlashId[key][slashId][x] == 0; +} +// ghost field for the length of the values array (stored in offset 0) +ghost mapping(bytes32 => mapping (uint256 => uint256))ghostLength_pendingStrategiesForSlashId { + init_state axiom forall bytes32 key. forall uint256 slashId. ghostLength_pendingStrategiesForSlashId[key][slashId] == 0; + // assumption: it's infeasible to grow the list to these many elements. + axiom forall bytes32 key. forall uint256 slashId. ghostLength_pendingStrategiesForSlashId[key][slashId] < max_uint256; +} + +// HOOKS +// Store hook to synchronize ghostLength_pendingStrategiesForSlashId with the length of the set._inner._values array. +hook Sstore currentContract._pendingStrategiesForSlashId[KEY bytes32 key][KEY uint256 slashId]._inner._values.length uint256 newLength { + ghostLength_pendingStrategiesForSlashId[key][slashId] = newLength; +} +// Store hook to synchronize ghostValues_pendingStrategiesForSlashId array with _pendingStrategiesForSlashId._inner._values. +hook Sstore currentContract._pendingStrategiesForSlashId[KEY bytes32 key][KEY uint256 slashId]._inner._values[INDEX uint256 index] bytes32 newValue { + ghostValues_pendingStrategiesForSlashId[key][slashId][index] = newValue; +} +// Store hook to synchronize ghostIndexes array with _pendingStrategiesForSlashId._inner._indexes. +hook Sstore currentContract._pendingStrategiesForSlashId[KEY bytes32 key][KEY uint256 slashId]._inner._indexes[KEY bytes32 value] uint256 newIndex { + ghostIndexes_pendingStrategiesForSlashId[key][slashId][value] = newIndex; +} + +// Load hook to synchronize ghostLength_pendingStrategiesForSlashId with the length of the _pendingStrategiesForSlashId._inner._values array. +hook Sload uint256 length currentContract._pendingStrategiesForSlashId[KEY bytes32 key][KEY uint256 slashId]._inner._values.length { + require ghostLength_pendingStrategiesForSlashId[key][slashId] == length; +} +hook Sload bytes32 value currentContract._pendingStrategiesForSlashId[KEY bytes32 key][KEY uint256 slashId]._inner._values[INDEX uint256 index] { + require ghostValues_pendingStrategiesForSlashId[key][slashId][index] == value; +} +hook Sload uint256 index currentContract._pendingStrategiesForSlashId[KEY bytes32 key][KEY uint256 slashId]._inner._indexes[KEY bytes32 value] { + require ghostIndexes_pendingStrategiesForSlashId[key][slashId][value] == index; +} + +// INVARIANTS +// This is the main invariant stating that the indexes and values always match: +// values[indexes[v] - 1] = v for all values v in the _pendingStrategiesForSlashId +// and indexes[values[i]] = i+1 for all valid indexes i. + +invariant _pendingStrategiesForSlashIdInvariant() + (forall bytes32 key. forall uint256 slashId. forall uint256 index. 0 <= index && index < ghostLength_pendingStrategiesForSlashId[key][slashId] => to_mathint(ghostIndexes_pendingStrategiesForSlashId[key][slashId][ghostValues_pendingStrategiesForSlashId[key][slashId][index]]) == index + 1) + && (forall bytes32 key. forall uint256 slashId. forall bytes32 value. ghostIndexes_pendingStrategiesForSlashId[key][slashId][value] == 0 || + (ghostValues_pendingStrategiesForSlashId[key][slashId][ghostIndexes_pendingStrategiesForSlashId[key][slashId][value] - 1] == value && ghostIndexes_pendingStrategiesForSlashId[key][slashId][value] >= 1 && ghostIndexes_pendingStrategiesForSlashId[key][slashId][value] <= ghostLength_pendingStrategiesForSlashId[key][slashId])); + + + + + +// GHOST COPIES: +// For every storage variable we add a ghost field that is kept synchronized by hooks. +// The ghost fields can be accessed by the spec, even inside quantifiers. + +// ghost field for the values array +ghost mapping(mathint => bytes32) ghostValues_pendingOperatorSets { + init_state axiom forall mathint x. ghostValues_pendingOperatorSets[x] == to_bytes32(0); +} +// ghost field for the indexes map +ghost mapping(bytes32 => uint256) ghostIndexes_pendingOperatorSets { + init_state axiom forall bytes32 x. ghostIndexes_pendingOperatorSets[x] == 0; +} +// ghost field for the length of the values array (stored in offset 0) +ghost uint256 ghostLength_pendingOperatorSets { + init_state axiom ghostLength_pendingOperatorSets == 0; + // assumption: it's infeasible to grow the list to these many elements. + axiom ghostLength_pendingOperatorSets < max_uint256; +} + +// HOOKS +// Store hook to synchronize ghostLength_pendingOperatorSets with the length of the _pendingOperatorSets._inner._values array. +hook Sstore currentContract._pendingOperatorSets._inner._values.length uint256 newLength { + ghostLength_pendingOperatorSets = newLength; +} +// Store hook to synchronize ghostValues_pendingOperatorSets array with _pendingOperatorSets._inner._values. +hook Sstore currentContract._pendingOperatorSets._inner._values[INDEX uint256 index] bytes32 newValue { + ghostValues_pendingOperatorSets[index] = newValue; +} +// Store hook to synchronize ghostIndexes_pendingOperatorSets array with _pendingOperatorSets._inner._indexes. +hook Sstore currentContract._pendingOperatorSets._inner._indexes[KEY bytes32 value] uint256 newIndex { + ghostIndexes_pendingOperatorSets[value] = newIndex; +} + +// Load hook to synchronize ghostLength_pendingOperatorSets with the length of the _pendingOperatorSets._inner._values array. +hook Sload uint256 length currentContract._pendingOperatorSets._inner._values.length { + require ghostLength_pendingOperatorSets == length; +} +hook Sload bytes32 value currentContract._pendingOperatorSets._inner._values[INDEX uint256 index] { + require ghostValues_pendingOperatorSets[index] == value; +} +hook Sload uint256 index currentContract._pendingOperatorSets._inner._indexes[KEY bytes32 value] { + require ghostIndexes_pendingOperatorSets[value] == index; +} + +// INVARIANTS +// This is the main invariant stating that the indexes and values always match: +// values[indexes[v] - 1] = v for all values v in the _pendingOperatorSets +// and indexes[values[i]] = i+1 for all valid indexes i. + +invariant _pendingOperatorSetsInvariant() + (forall uint256 index. 0 <= index && index < ghostLength_pendingOperatorSets => to_mathint(ghostIndexes_pendingOperatorSets[ghostValues_pendingOperatorSets[index]]) == index + 1) + && (forall bytes32 value. ghostIndexes_pendingOperatorSets[value] == 0 || + (ghostValues_pendingOperatorSets[ghostIndexes_pendingOperatorSets[value] - 1] == value && ghostIndexes_pendingOperatorSets[value] >= 1 && ghostIndexes_pendingOperatorSets[value] <= ghostLength_pendingOperatorSets));