diff --git a/certora/confs/ccip.conf b/certora/confs/ccip.conf index d6667401d3..003f089502 100644 --- a/certora/confs/ccip.conf +++ b/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" } diff --git a/certora/specs/ccip.spec b/certora/specs/ccip.spec index ca8a4c02d4..1eee1bebe1 100644 --- a/certora/specs/ccip.spec +++ b/certora/specs/ccip.spec @@ -76,3 +76,38 @@ rule provideLiquidity_correctness(env e) { 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; +} +