Certora squashed

.github/workflows/certora.yml

@@ -0,0 +1,53 @@
+name: certora
+
+on:
+  push:
+    branches:
+      - main
+      - certora
+  pull_request:
+    branches:
+      - main
+      - certora
+
+  workflow_dispatch:
+
+jobs:
+  verify:
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v2
+        with:
+          submodules: recursive
+
+      - name: Install python
+        uses: actions/setup-python@v2
+        with: { python-version: 3.9 }
+
+      - name: Install java
+        uses: actions/setup-java@v1
+        with: { java-version: '11', java-package: jre }
+
+      - name: Install certora cli
+        run: pip install certora-cli==7.6.3
+
+      - name: Install solc
+        run: |
+          wget https://github.com/ethereum/solidity/releases/download/v0.8.10/solc-static-linux
+          chmod +x solc-static-linux
+          sudo mv solc-static-linux /usr/local/bin/solc8.10
+
+      - name: Verify rule ${{ matrix.rule }}
+        run: |
+          echo "key length" ${#CERTORAKEY}
+          certoraRun certora/confs/${{ matrix.rule }}
+        env:
+          CERTORAKEY: ${{ secrets.CERTORAKEY }}
+
+    strategy:
+      fail-fast: false
+      max-parallel: 16
+      matrix:
+        rule:
+          - ccip.conf

.gitmodules

@@ -1,3 +1,6 @@
 [submodule "contracts/foundry-lib/forge-std"]
 	path = contracts/foundry-lib/forge-std
-	url = https://github.com/foundry-rs/forge-std
+	url = https://github.com/foundry-rs/forge-std
+[submodule "contracts/foundry-lib/solidity-utils"]
+	path = contracts/foundry-lib/solidity-utils
+	url = https://github.com/bgd-labs/solidity-utils

README.md

@@ -1,3 +1,5 @@
+> ❗️ Forked repository of CCIP contracts ([version 2.8.0 release](https://github.com/smartcontractkit/ccip/tree/v2.8.0-ccip1.4.0-release)) that includes modifications for developing custom TokenPool contracts tailored for the [GHO cross-chain strategy](https://governance.aave.com/t/arfc-gho-cross-chain-launch/17616). All relevant code and tests are located in the [GHO pools directory](./contracts/v0.8/ccip/pools/GHO).
+
 <br/>
 <p align="center">
 <a href="https://chain.link" target="_blank">
@@ -232,9 +234,11 @@ flowchart RL
     github.com/smartcontractkit/chainlink/core/scripts --> github.com/smartcontractkit/chainlink/v2
 
 ```
+
 The `integration-tests` and `core/scripts` modules import the root module using a relative replace in their `go.mod` files,
 so dependency changes in the root `go.mod` often require changes in those modules as well. After making a change, `go mod tidy`
 can be run on all three modules using:
+
 ```
 make gomodtidy
 ```
@@ -254,6 +258,7 @@ pnpm i
 ```bash
 pnpm test
 ```
+
 NOTE: Chainlink is currently in the process of migrating to Foundry and contains both Foundry and Hardhat tests in some versions. More information can be found here: [Chainlink Foundry Documentation](https://github.com/smartcontractkit/chainlink/blob/develop/contracts/foundry.md).
 Any 't.sol' files associated with Foundry tests, contained within the src directories will be ignored by Hardhat.
 

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,18 @@
+{
+    "files": [
+        "contracts/src/v0.8/ccip/pools/GHO/UpgradeableLockReleaseTokenPool.sol",
+        "certora/harness/SimpleERC20.sol"
+    ],
+    "link": [
+        "UpgradeableLockReleaseTokenPool:i_token=SimpleERC20"
+    ],    
+    "optimistic_loop": true,
+    "process": "emv",
+    "prover_args": ["-depth 10","-mediumTimeout 700"],
+    "smt_timeout": "600",
+    "solc": "solc8.10",
+    "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,113 @@
+/*
+    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 getRebalancer() 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:
+         - only the rebalancer can call to withdrawLiquidity
+         - 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 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.
+   ============================================================================*/
+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 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;
+}
+

contracts/remappings.txt

@@ -6,3 +6,5 @@ forge-std/=foundry-lib/forge-std/src/
 hardhat/=node_modules/hardhat/
 @eth-optimism/=node_modules/@eth-optimism/
 @scroll-tech/=node_modules/@scroll-tech/
+@aave/gho-core/=node_modules/@aave/gho/src/contracts/
+solidity-utils/=foundry-lib/solidity-utils/src/

contracts/src/v0.8/ccip/pools/GHO/UpgradeableBurnMintTokenPool.sol

@@ -0,0 +1,66 @@
+// SPDX-License-Identifier: BUSL-1.1
+pragma solidity ^0.8.0;
+
+import {ITypeAndVersion} from "../../../shared/interfaces/ITypeAndVersion.sol";
+import {IBurnMintERC20} from "../../../shared/token/ERC20/IBurnMintERC20.sol";
+
+import {UpgradeableTokenPool} from "./UpgradeableTokenPool.sol";
+import {UpgradeableBurnMintTokenPoolAbstract} from "./UpgradeableBurnMintTokenPoolAbstract.sol";
+
+import {IRouter} from "../../interfaces/IRouter.sol";
+import {VersionedInitializable} from "./VersionedInitializable.sol";
+
+/// @title UpgradeableBurnMintTokenPool
+/// @author Aave Labs
+/// @notice Upgradeable version of Chainlink's CCIP BurnMintTokenPool
+/// @dev Contract adaptations:
+/// - Implementation of VersionedInitializable to allow upgrades
+/// - Move of allowlist and router definition to initialization stage
+contract UpgradeableBurnMintTokenPool is VersionedInitializable, UpgradeableBurnMintTokenPoolAbstract, ITypeAndVersion {
+  string public constant override typeAndVersion = "BurnMintTokenPool 1.4.0";
+
+  /// @dev Constructor
+  /// @param token The bridgeable token that is managed by this pool.
+  /// @param armProxy The address of the arm proxy
+  /// @param allowlistEnabled True if pool is set to access-controlled mode, false otherwise
+  constructor(
+    address token,
+    address armProxy,
+    bool allowlistEnabled
+  ) UpgradeableTokenPool(IBurnMintERC20(token), armProxy, allowlistEnabled) {}
+
+  /// @dev Initializer
+  /// @dev The address passed as `owner` must accept ownership after initialization.
+  /// @dev The `allowlist` is only effective if pool is set to access-controlled mode
+  /// @param owner The address of the owner
+  /// @param allowlist A set of addresses allowed to trigger lockOrBurn as original senders
+  /// @param router The address of the router
+  function initialize(address owner, address[] memory allowlist, address router) public virtual initializer {
+    if (owner == address(0)) revert ZeroAddressNotAllowed();
+    if (router == address(0)) revert ZeroAddressNotAllowed();
+    _transferOwnership(owner);
+
+    s_router = IRouter(router);
+
+    // Pool can be set as permissioned or permissionless at deployment time only to save hot-path gas.
+    if (i_allowlistEnabled) {
+      _applyAllowListUpdates(new address[](0), allowlist);
+    }
+  }
+
+  /// @inheritdoc UpgradeableBurnMintTokenPoolAbstract
+  function _burn(uint256 amount) internal virtual override {
+    IBurnMintERC20(address(i_token)).burn(amount);
+  }
+
+  /// @notice Returns the revision number
+  /// @return The revision number
+  function REVISION() public pure virtual returns (uint256) {
+    return 1;
+  }
+
+  /// @inheritdoc VersionedInitializable
+  function getRevision() internal pure virtual override returns (uint256) {
+    return REVISION();
+  }
+}