From 8250553b748d440a7c56eb16e343956257802a59 Mon Sep 17 00:00:00 2001
From: nisnislevi <nissan@certora.com>
Date: Tue, 28 May 2024 12:22:04 +0300
Subject: [PATCH] update spec: remove rebalancer and add bridgeLimitAdmin rule

---
 certora/specs/ccip.spec | 18 +++++++++++++++---
 1 file changed, 15 insertions(+), 3 deletions(-)

diff --git a/certora/specs/ccip.spec b/certora/specs/ccip.spec
index 1eee1bebe1..69fd216f3b 100644
--- a/certora/specs/ccip.spec
+++ b/certora/specs/ccip.spec
@@ -8,7 +8,7 @@ using SimpleERC20 as erc20;
 methods {
   function getCurrentBridgedAmount() external returns (uint256) envfree;
   function getBridgeLimit() external returns (uint256) envfree;
-  function getRebalancer() external returns (address) envfree;
+  function owner() external returns (address) envfree;
 }
 
 
@@ -54,7 +54,7 @@ rule withdrawLiquidity_correctness(env e) {
   withdrawLiquidity(e, amount);
   uint256 bal_after = erc20.balanceOf(e, currentContract);
 
-  assert e.msg.sender == getRebalancer();
+  //  assert e.msg.sender == getRebalancer();
   assert (to_mathint(bal_after) == bal_before - amount);
 }
 
@@ -73,7 +73,7 @@ rule provideLiquidity_correctness(env e) {
   provideLiquidity(e, amount);
   uint256 bal_after = erc20.balanceOf(e, currentContract);
 
-  assert e.msg.sender == getRebalancer();
+  //  assert e.msg.sender == getRebalancer();
   assert (to_mathint(bal_after) == bal_before + amount);
 }
 
@@ -111,3 +111,15 @@ rule only_releaseOrMint_can_decrease_currentBridged(env e) {
     f.selector==sig:releaseOrMint(bytes memory,address,uint256,uint64,bytes memory).selector;
 }
 
+
+/* ==============================================================================
+   rule: only_releaseOrMint_can_deccrease_currentBridged
+   ============================================================================*/
+rule only_bridgeLimitAdmin_or_owner_can_call_setBridgeLimit(env e) {
+  uint256 newBridgeLimit;
+
+  setBridgeLimit(e, newBridgeLimit);
+  
+  assert e.msg.sender==getBridgeLimitAdmin(e) || e.msg.sender==owner();
+}
+