Merge pull request #250 from Layr-Labs/fix-prover-havocs

update specs to include "nondet" summary of the calls to `ServiceMana…
Layr-Labs · Oct 16, 2023 · dad75a4 · dad75a4
2 parents 5d2d534 + ca61dc0
commit dad75a4
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 0 deletions.
diff --git a/certora/specs/core/DelegationManager.spec b/certora/specs/core/DelegationManager.spec
@@ -6,6 +6,9 @@ methods {
     function decreaseDelegatedShares(address,address,uint256) external;
 	function increaseDelegatedShares(address,address,uint256) external;
 
+    // external calls from DelegationManager to ServiceManager
+    function _.updateStakes(address[]) external => NONDET;
+
 	// external calls to Slasher
     function _.isFrozen(address) external => DISPATCHER(true);
 	function _.canWithdraw(address,uint32,uint256) external => DISPATCHER(true);

diff --git a/certora/specs/core/StrategyManager.spec b/certora/specs/core/StrategyManager.spec
@@ -10,6 +10,9 @@ methods {
 	function _.decreaseDelegatedShares(address,address,uint256) external => DISPATCHER(true);
 	function _.increaseDelegatedShares(address,address,uint256) external => DISPATCHER(true);
 
+    // external calls from DelegationManager to ServiceManager
+    function _.updateStakes(address[]) external => NONDET;
+
 	// external calls to Slasher
     function _.isFrozen(address) external => DISPATCHER(true);
 	function _.canWithdraw(address,uint32,uint256) external => DISPATCHER(true);

diff --git a/certora/specs/pods/EigenPodManager.spec b/certora/specs/pods/EigenPodManager.spec
@@ -6,6 +6,9 @@ methods {
     function _.decreaseDelegatedShares(address,address,uint256) external;
 	function _.increaseDelegatedShares(address,address,uint256) external;
 
+    // external calls from DelegationManager to ServiceManager
+    function _.updateStakes(address[]) external => NONDET;
+
 	// external calls to Slasher
     function _.isFrozen(address) external => DISPATCHER(true);
 	function _.canWithdraw(address,uint32,uint256) external => DISPATCHER(true);