for PR

.github/workflows/certora.yml

@@ -5,10 +5,12 @@ on:
     branches:
       - main
       - certora
+      - ccip-gho
   pull_request:
     branches:
       - main
       - certora
+      - ccip-gho
 
   workflow_dispatch:
 

certora/confs/ccip.conf

@@ -1,6 +1,6 @@
 {
     "files": [
-        "contracts/src/v0.8/ccip/pools/UpgradeableLockReleaseTokenPool.sol",
+        "contracts/src/v0.8/ccip/pools/GHO/UpgradeableLockReleaseTokenPool.sol",
         "certora/harness/SimpleERC20.sol"
     ],
     "link": [
@@ -12,6 +12,7 @@
     "smt_timeout": "600",
     "solc": "solc8.10",
     "verify": "UpgradeableLockReleaseTokenPool:certora/specs/ccip.spec",
+    "rule_sanity": "basic",
     "msg": "CCIP"
 }
 

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;
 }
 
 
@@ -42,9 +42,7 @@ invariant currentBridge_LEQ_bridgeLimit()
 
 /* ==============================================================================
    rule: withdrawLiquidity_correctness
-   description: The rule checks that:
-         - only the rebalancer can call to withdrawLiquidity
-         - the balance of the contract is as expected.
+   description: The rule checks that the balance of the contract is as expected.
    ============================================================================*/
 rule withdrawLiquidity_correctness(env e) {
   uint256 amount;
@@ -54,16 +52,13 @@ rule withdrawLiquidity_correctness(env e) {
   withdrawLiquidity(e, amount);
   uint256 bal_after = erc20.balanceOf(e, currentContract);
 
-  assert e.msg.sender == getRebalancer();
   assert (to_mathint(bal_after) == bal_before - amount);
 }
 
 
 /* ==============================================================================
    rule: provideLiquidity_correctness
-   description: The rule checks that:
-         - only the rebalancer can call to provideLiquidity
-         - the balance of the contract is as expected.
+   description: The rule checks that the balance of the contract is as expected.
    ============================================================================*/
 rule provideLiquidity_correctness(env e) {
   uint256 amount;
@@ -73,6 +68,52 @@ rule provideLiquidity_correctness(env e) {
   provideLiquidity(e, amount);
   uint256 bal_after = erc20.balanceOf(e, currentContract);
 
-  assert e.msg.sender == getRebalancer();
   assert (to_mathint(bal_after) == bal_before + amount);
 }
+
+
+/* ==============================================================================
+   rule: only_lockOrBurn_can_increase_currentBridged
+   ============================================================================*/
+rule only_lockOrBurn_can_increase_currentBridged(env e) {
+  method f;
+  calldataarg args;
+
+  uint256 curr_bridge_before = getCurrentBridgedAmount();
+  f (e,args);
+  uint256 curr_bridge_after = getCurrentBridgedAmount();
+
+  assert 
+    curr_bridge_after > curr_bridge_before =>
+    f.selector==sig:lockOrBurn(address,bytes calldata,uint256,uint64,bytes calldata).selector;
+}
+
+
+/* ==============================================================================
+   rule: only_releaseOrMint_can_deccrease_currentBridged
+   ============================================================================*/
+rule only_releaseOrMint_can_decrease_currentBridged(env e) {
+  method f;
+  calldataarg args;
+
+  uint256 curr_bridge_before = getCurrentBridgedAmount();
+  f (e,args);
+  uint256 curr_bridge_after = getCurrentBridgedAmount();
+
+  assert 
+    curr_bridge_after < curr_bridge_before =>
+    f.selector==sig:releaseOrMint(bytes memory,address,uint256,uint64,bytes memory).selector;
+}
+
+
+/* ==============================================================================
+   rule: only_bridgeLimitAdmin_or_owner_can_call_setBridgeLimit
+   ============================================================================*/
+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();
+}
+