feat: migrate certora formal verification conf

certora/Makefile

@@ -0,0 +1,24 @@
+default: help
+
+PATCH         = applyHarness.patch
+CONTRACTS_DIR = ../contracts
+MUNGED_DIR    = munged
+
+help:
+	@echo "usage:"
+	@echo "  make clean:  remove all generated files (those ignored by git)"
+	@echo "  make $(MUNGED_DIR): create $(MUNGED_DIR) directory by applying the patch file to $(CONTRACTS_DIR)"
+	@echo "  make record: record a new patch file capturing the differences between $(CONTRACTS_DIR) and $(MUNGED_DIR)"
+
+munged:  $(wildcard $(CONTRACTS_DIR)/*.sol) $(PATCH)
+	rm -rf $@
+	cp -r $(CONTRACTS_DIR) $@
+	patch -p0 -d $@ < $(PATCH)
+
+record:
+	diff -ruN $(CONTRACTS_DIR) $(MUNGED_DIR) | sed 's+\.\./contracts/++g' | sed 's+munged/++g' > $(PATCH)
+
+clean:
+	git clean -fdX
+	touch $(PATCH)
+

certora/confs/ccip.conf

@@ -0,0 +1,21 @@
+{
+    "files": [
+        "contracts/src/v0.8/ccip/pools/GHO/UpgradeableLockReleaseTokenPool.sol",
+        "certora/harness/SimpleERC20.sol"
+    ],
+    "packages": [
+        "solidity-utils/=contracts/foundry-lib/solidity-utils/src/"
+    ],
+    "link": [
+        "UpgradeableLockReleaseTokenPool:i_token=SimpleERC20"
+    ],
+    "optimistic_loop": true,
+    "process": "emv",
+    "prover_args": ["-depth 10","-mediumTimeout 700"],
+    "smt_timeout": "600",
+    "solc": "solc8.19",
+    "verify": "UpgradeableLockReleaseTokenPool:certora/specs/ccip.spec",
+    "rule_sanity": "basic",
+    "msg": "CCIP"
+}
+

certora/harness/SimpleERC20.sol

@@ -0,0 +1,58 @@
+// SPDX-License-Identifier: agpl-3.0
+pragma solidity ^0.8.0;
+
+import {IERC20} from "../../contracts/src/v0.8/vendor/openzeppelin-solidity/v4.8.3/contracts/token/ERC20/IERC20.sol";
+
+/**
+A simple ERC implementation used as the underlying_asset for the verification process.
+ */
+contract SimpleERC20 is IERC20 {
+  uint256 t;
+  mapping(address => uint256) b;
+  mapping(address => mapping(address => uint256)) a;
+
+  function add(uint a, uint b) internal pure returns (uint256) {
+    uint c = a + b;
+    require(c >= a);
+    return c;
+  }
+
+  function sub(uint a, uint b) internal pure returns (uint256) {
+    require(a >= b);
+    return a - b;
+  }
+
+  function totalSupply() external view override returns (uint256) {
+    return t;
+  }
+
+  function balanceOf(address account) external view override returns (uint256) {
+    return b[account];
+  }
+
+  function transfer(address recipient, uint256 amount) external override returns (bool) {
+    b[msg.sender] = sub(b[msg.sender], amount);
+    b[recipient] = add(b[recipient], amount);
+    return true;
+  }
+
+  function allowance(address owner, address spender) external view override returns (uint256) {
+    return a[owner][spender];
+  }
+
+  function approve(address spender, uint256 amount) external override returns (bool) {
+    a[msg.sender][spender] = amount;
+    return true;
+  }
+
+  function transferFrom(
+    address sender,
+    address recipient,
+    uint256 amount
+  ) external override returns (bool) {
+    b[sender] = sub(b[sender], amount);
+    b[recipient] = add(b[recipient], amount);
+    a[sender][msg.sender] = sub(a[sender][msg.sender], amount);
+    return true;
+  }
+}

certora/munged/.gitignore

@@ -0,0 +1,2 @@
+*
+!.gitignore

certora/specs/ccip.spec

@@ -0,0 +1,119 @@
+/*
+    This is a Specification File for Smart Contract Verification with the Certora Prover.
+    Contract name: UpgradeableLockReleaseTokenPool
+*/
+
+using SimpleERC20 as erc20;
+
+methods {
+  function getCurrentBridgedAmount() external returns (uint256) envfree;
+  function getBridgeLimit() external returns (uint256) envfree;
+  function owner() external returns (address) envfree;
+}
+
+
+rule sanity {
+  env e;
+  calldataarg arg;
+  method f;
+  f(e, arg);
+  satisfy true;
+}
+
+
+
+/* ==============================================================================
+   invariant: currentBridge_LEQ_bridgeLimit.
+   Description: The value of s_currentBridged is LEQ than the value of s_bridgeLimit.
+   Note: this may be violated if one calls to setBridgeLimit(newBridgeLimit) with 
+         newBridgeLimit < s_currentBridged.
+   ============================================================================*/
+invariant currentBridge_LEQ_bridgeLimit()
+  getCurrentBridgedAmount() <= getBridgeLimit()
+  filtered { f ->
+    !f.isView &&
+    f.selector != sig:setBridgeLimit(uint256).selector}
+  {
+    preserved initialize(address owner, address[] allowlist, address router, uint256 bridgeLimit) with (env e2) {
+      require getCurrentBridgedAmount()==0;
+    }
+  }
+
+
+/* ==============================================================================
+   rule: withdrawLiquidity_correctness
+   description: The rule checks that the balance of the contract is as expected.
+   ============================================================================*/
+rule withdrawLiquidity_correctness(env e) {
+  uint256 amount;
+
+  require e.msg.sender != currentContract;
+  uint256 bal_before = erc20.balanceOf(e, currentContract);
+  withdrawLiquidity(e, amount);
+  uint256 bal_after = erc20.balanceOf(e, currentContract);
+
+  assert (to_mathint(bal_after) == bal_before - amount);
+}
+
+
+/* ==============================================================================
+   rule: provideLiquidity_correctness
+   description: The rule checks that the balance of the contract is as expected.
+   ============================================================================*/
+rule provideLiquidity_correctness(env e) {
+  uint256 amount;
+
+  require e.msg.sender != currentContract;
+  uint256 bal_before = erc20.balanceOf(e, currentContract);
+  provideLiquidity(e, amount);
+  uint256 bal_after = erc20.balanceOf(e, currentContract);
+
+  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();
+}
+