diff --git a/certora/specs/ccip.spec b/certora/specs/ccip.spec index 1eee1bebe1..e24d729c55 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 getRebalancer() 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_can_call_setBridgeLimit(env e) { + uint256 newBridgeLimit; + + setBridgeLimit(e, newBridgeLimit); + + assert e.msg.sender==getBridgeLimitAdmin(e); +} +