some small additions to spec

Certora · Jan 1, 2025 · 87d022d · 87d022d
1 parent 59c3763
commit 87d022d
Show file tree

Hide file tree

Showing 3 changed files with 27 additions and 4 deletions.
diff --git 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
@@ -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
@@ -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();
+}