From ca61dc03bcbf1f1310f32183e2a12b150b17b90c Mon Sep 17 00:00:00 2001
From: ChaoticWalrus <93558947+ChaoticWalrus@users.noreply.github.com>
Date: Mon, 16 Oct 2023 09:48:11 -0700
Subject: [PATCH] update specs to include "nondet" summary of the calls to
 `ServiceManager.updateStakes`

This basically means treating the function as 'view' -- see documentation here https://docs.certora.com/en/latest/docs/cvl/methods.html#summaries
Seems like a reasonable assumption to add.
---
 certora/specs/core/DelegationManager.spec | 3 +++
 certora/specs/core/StrategyManager.spec   | 3 +++
 certora/specs/pods/EigenPodManager.spec   | 3 +++
 3 files changed, 9 insertions(+)

diff --git a/certora/specs/core/DelegationManager.spec b/certora/specs/core/DelegationManager.spec
index e0d545887..a24fc29b7 100644
--- 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
index 9af8f8562..ec7f7b9cd 100644
--- 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
index 4d5e1afbe..b7a2802fa 100644
--- 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);