From 87d022dfd0de8a6f1a2f528a8a9345032b70a510 Mon Sep 17 00:00:00 2001
From: nisnislevi <nissan@certora.com>
Date: Wed, 1 Jan 2025 17:18:16 +0200
Subject: [PATCH] some small additions to spec

---
 .github/workflows/certora.yml |  2 +-
 certora/confs/ccip.conf       |  2 +-
 certora/specs/ccip.spec       | 27 +++++++++++++++++++++++++--
 3 files changed, 27 insertions(+), 4 deletions(-)

diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
index 64e2f32053..bc44c7b9d4 100644
--- a/.github/workflows/certora.yml
+++ b/.github/workflows/certora.yml
@@ -20,7 +20,7 @@ jobs:
         with: { java-version: '11', java-package: jre }
 
       - name: Install certora cli
-        run: pip install certora-cli==7.20.3
+        run: pip install certora-cli==7.21.1
 
       - name: Install solc
         run: |
diff --git a/certora/confs/ccip.conf b/certora/confs/ccip.conf
index c3d10c3c5e..df46c2843f 100644
--- a/certora/confs/ccip.conf
+++ b/certora/confs/ccip.conf
@@ -4,7 +4,7 @@
         "certora/harness/SimpleERC20.sol"
     ],
     "packages": [
-        "solidity-utils/=contracts/foundry-lib/solidity-utils/src/"
+        "solidity-utils/=contracts/foundry-lib/solidity-utils/src"
     ],
     "link": [
         "UpgradeableLockReleaseTokenPool:i_token=SimpleERC20"
diff --git a/certora/specs/ccip.spec b/certora/specs/ccip.spec
index 0172ac0091..6e9d6d5593 100644
--- a/certora/specs/ccip.spec
+++ b/certora/specs/ccip.spec
@@ -9,6 +9,7 @@ methods {
   function getCurrentBridgedAmount() external returns (uint256) envfree;
   function getBridgeLimit() external returns (uint256) envfree;
   function owner() external returns (address) envfree;
+  function getRebalancer() external returns (address) envfree;
 }
 
 
@@ -93,9 +94,9 @@ rule only_lockOrBurn_can_increase_currentBridged(env e, method f)
 
 
 /* ==============================================================================
-   rule: only_releaseOrMint_currentBridged
+   rule: only_releaseOrMint_can_decrease_currentBridged
    ============================================================================*/
-rule only_releaseOrMint_currentBridged(env e, method f) 
+rule only_releaseOrMint_can_decrease_currentBridged(env e, method f) 
   filtered { f -> filterSetter(f) }
 {
   calldataarg args;
@@ -121,6 +122,7 @@ rule only_bridgeLimitAdmin_or_owner_can_call_setBridgeLimit(env e) {
   assert e.msg.sender==getBridgeLimitAdmin(e) || e.msg.sender==owner();
 }
 
+
 /* ==============================================================================
    rule: only_owner_can_call_setCurrentBridgedAmount
    ============================================================================*/
@@ -131,3 +133,24 @@ rule only_owner_can_call_setCurrentBridgedAmount(env e) {
   
   assert e.msg.sender==owner();
 }
+
+/* ==============================================================================
+   rule: only_rebalancer_can_call_provideLiquidity
+   ============================================================================*/
+rule only_rebalancer_can_call_provideLiquidity(env e) {
+  uint256 amount;
+  provideLiquidity(e, amount);
+  
+  assert e.msg.sender==getRebalancer();
+}
+
+
+/* ==============================================================================
+   rule: only_rebalancer_can_call_withdrawLiquidity
+   ============================================================================*/
+rule only_rebalancer_can_call_withdrawLiquidity(env e) {
+  uint256 amount;
+  withdrawLiquidity(e, amount);
+  
+  assert e.msg.sender==getRebalancer();
+}