feat: Update Certora Formal Verification Tests

Author: nisnislevi

.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: |

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"

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;
@@ -131,3 +132,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();
+}