Merge pull request #236 from Layr-Labs/more-prover-fixes

More prover fixes + added rules
Layr-Labs · Oct 12, 2023 · cfba374 · cfba374
2 parents 6b0da76 + 59c200f
commit cfba374
Show file tree

Hide file tree

Showing 4 changed files with 85 additions and 4 deletions.
diff --git a/certora/harnesses/DelegationManagerHarness.sol b/certora/harnesses/DelegationManagerHarness.sol
@@ -8,7 +8,21 @@ contract DelegationManagerHarness is DelegationManager {
     constructor(IStrategyManager _strategyManager, ISlasher _slasher, IEigenPodManager _eigenPodManager)
         DelegationManager(_strategyManager, _slasher, _eigenPodManager) {}
 
-    function get_operatorShares(address operator, IStrategy strategy) public view returns(uint256) {
+    function get_operatorShares(address operator, IStrategy strategy) public view returns (uint256) {
         return operatorShares[operator][strategy];
     }
+
+    function get_stakerDelegateableShares(address staker, IStrategy strategy) public view returns (uint256) {
+        // this is the address of the virtual 'beaconChainETH' strategy
+        if (address(strategy) == 0xbeaC0eeEeeeeEEeEeEEEEeeEEeEeeeEeeEEBEaC0) {
+            int256 beaconChainETHShares = eigenPodManager.podOwnerShares(staker);
+            if (beaconChainETHShares <= 0) {
+                return 0;
+            } else {
+                return uint256(beaconChainETHShares);
+            }
+        } else {
+            return strategyManager.stakerStrategyShares(staker, strategy);
+        }
+    }
 }
diff --git a/certora/scripts/core/verifyDelegationManager.sh b/certora/scripts/core/verifyDelegationManager.sh
@@ -14,6 +14,6 @@ certoraRun certora/harnesses/DelegationManagerHarness.sol \
     --prover_args '-optimisticFallback true' \
     --optimistic_hashing \
     $RULE \
-    --loop_iter 3 \
+    --loop_iter 2 \
     --packages @openzeppelin=lib/openzeppelin-contracts @openzeppelin-upgrades=lib/openzeppelin-contracts-upgradeable \
     --msg "DelegationManager $1 $2" \
diff --git a/certora/specs/core/DelegationManager.spec b/certora/specs/core/DelegationManager.spec
@@ -32,13 +32,23 @@ methods {
     function _.isPauser(address) external => DISPATCHER(true);
 	function _.unpauser() external => DISPATCHER(true);
 
+    // external calls to Strategy contracts
+    function _.withdraw(address,address,uint256) external => DISPATCHER(true);
+    function _.deposit(address,uint256) external => DISPATCHER(true);
+
+    // external calls to ERC20
+    function _.balanceOf(address) external => DISPATCHER(true);
+    function _.transfer(address, uint256) external => DISPATCHER(true);
+    function _.transferFrom(address, address, uint256) external => DISPATCHER(true);
+
     // external calls to ERC1271 (can import OpenZeppelin mock implementation)
     // isValidSignature(bytes32 hash, bytes memory signature) returns (bytes4 magicValue) => DISPATCHER(true)
     function _.isValidSignature(bytes32, bytes) external => DISPATCHER(true);
 
     //// Harnessed Functions
     // Harnessed getters
     function get_operatorShares(address,address) external returns (uint256) envfree;
+    function get_stakerDelegateableShares(address,address) external returns (uint256) envfree;
 
     //envfree functions
     function delegatedTo(address staker) external returns (address) envfree;
@@ -204,6 +214,47 @@ rule canOnlyDelegateWithSpecificFunctions(address staker) {
     }
 }
 
+rule sharesBecomeDelegatedWhenStakerDelegates(address operator, address staker, address strategy) {
+    requireInvariant operatorsAlwaysDelegatedToSelf(operator);
+    // 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;
+    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) {
+    requireInvariant operatorsAlwaysDelegatedToSelf(operator);
+    // 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;
+    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 batchEquivalence {
     env e;

diff --git a/certora/specs/core/StrategyManager.spec b/certora/specs/core/StrategyManager.spec
@@ -36,6 +36,10 @@ methods {
     function _.isPauser(address) external => DISPATCHER(true);
 	function _.unpauser() external => DISPATCHER(true);
 
+    // external calls to Strategy contracts
+    function _.withdraw(address,address,uint256) external => DISPATCHER(true);
+    function _.deposit(address,uint256) external => DISPATCHER(true);
+
     // external calls to ERC20
     function _.balanceOf(address) external => DISPATCHER(true);
     function _.transfer(address, uint256) external => DISPATCHER(true);
@@ -50,6 +54,7 @@ methods {
 
     //// Harnessed Functions
     // Harnessed calls
+    function _.totalShares() external => DISPATCHER(true);
     // Harnessed getters
     function strategy_is_in_stakers_array(address, address) external returns (bool) envfree;
     function num_times_strategy_is_in_stakers_array(address, address) external returns (uint256) envfree;
@@ -141,8 +146,19 @@ rule safeApprovalUse(address user) {
     uint256 tokenBalanceBefore = token.balanceOf(user);
     method f;
     env e;
-    calldataarg args;
-    f(e,args);
+    // special case logic, to handle an edge case
+    if (f.selector == sig:withdrawSharesAsTokens(address,address,uint256,address).selector) {
+        address recipient;
+        address strategy;
+        uint256 shares;
+        // filter out case where the 'user' is the strategy itself
+        require(user != strategy);
+        withdrawSharesAsTokens(e, recipient, strategy, shares, token);
+    // otherwise just perform an arbitrary function call
+    } else {
+        calldataarg args;
+        f(e,args);
+    }
     uint256 tokenBalanceAfter = token.balanceOf(user);
     if (tokenBalanceAfter < tokenBalanceBefore) {
         assert(e.msg.sender == user, "unsafeApprovalUse?");