feat: Add token pool for GHO based on CCIP 1.5.1 (#20)

* feat: setup deps

* feat: migrate GHO token pools to v1.5.1

* fix: ci

* feat: certora formal verification

* chore: rm whitespace, ref comment

* doc: rm unneeded remanant

* feat: upd currentBridged on liquidity transfers

* fix: certora add invariant to withdraw, provide, and transfer liq

* feat: add transferLiquidity on burnMintTokenPool

* doc: upd transferLiquidity for burnMint

* feat: rm token decimal check in constructor

* feat: setCurrentBridgedAmount, revert bridgeAmount changes on {transfer,provide,withdraw}Liquidity

* chore: fix doc

* feat: mintAndTransferLiquidity

* chore: reorder imports to minmize diff

* feat: `directMint` & `directBurn` to migrate facilitators

* chore: expand on test scenario

* chore: move revert to base test such that it can be inherited

* test: use setter over vm.store

* test: revert `InsufficientLiquidity` on `transferLiquidity`

* test: rm unneeded mockCall

* test: migrateLiquidity on remote pool

* doc: update comments

* chore: cleanup test

* new: introduce __gap on UpgradeableTokenPool

* doc: update doc & diffs for storage gap

* chore: upd directMint test

* doc: upd diff and doc for __gap

* doc: fix base diff doc

.github/workflows/certora.yml

@@ -0,0 +1,43 @@
+name: certora
+
+on: push
+
+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.20.3
+
+      - name: Install solc
+        run: |
+          wget https://github.com/ethereum/solidity/releases/download/v0.8.24/solc-static-linux
+          chmod +x solc-static-linux
+          sudo mv solc-static-linux /usr/local/bin/solc8.24
+
+      - 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

.github/workflows/tests.yml

@@ -0,0 +1,62 @@
+name: solidity
+
+on: push
+
+env:
+  FOUNDRY_PROFILE: ci
+
+jobs:
+  tests:
+    strategy:
+      fail-fast: false
+      matrix:
+        product: [ccip]
+    name: Foundry Tests ${{ matrix.product }}
+    # See https://github.com/foundry-rs/foundry/issues/3827
+    runs-on: ubuntu-22.04
+
+    # The if statements for steps after checkout repo is workaround for
+    # passing required check for PRs that don't have filtered changes.
+    steps:
+      - name: Checkout the repo
+        uses: actions/checkout@b4ffde65f46336ab88eb53be808477a3936bae11 # v4.1.1
+        with:
+          submodules: recursive
+
+      # Only needed because we use the NPM versions of packages
+      # and not native Foundry. This is to make sure the dependencies
+      # stay in sync.
+      - name: Setup NodeJS
+        uses: ./.github/actions/setup-nodejs
+
+      - name: Install Foundry
+        uses: foundry-rs/foundry-toolchain@v1
+        with:
+          # Has to match the `make foundry` version.
+          version: nightly-2cb875799419c907cc3709e586ece2559e6b340e
+
+      - name: Run Forge build
+        run: |
+          forge --version
+          forge build
+        id: build
+        working-directory: contracts
+        env:
+          FOUNDRY_PROFILE: ${{ matrix.product }}
+
+      - name: Run Forge tests
+        run: |
+          forge test -vvv
+        id: test
+        working-directory: contracts
+        env:
+          FOUNDRY_PROFILE: ${{ matrix.product }}
+
+      - name: Run Forge snapshot
+        if: ${{ !contains(fromJson('["vrf"]'), matrix.product) && !contains(fromJson('["automation"]'), matrix.product) && needs.changes.outputs.changes == 'true' }}
+        run: |
+          forge snapshot --nmt "testFuzz_\w{1,}?" --check gas-snapshots/${{ matrix.product }}.gas-snapshot
+        id: snapshot
+        working-directory: contracts
+        env:
+          FOUNDRY_PROFILE: ${{ matrix.product }}

.gitmodules

@@ -0,0 +1,6 @@
+[submodule "contracts/foundry-lib/gho-core"]
+	path = contracts/foundry-lib/gho-core
+	url = https://github.com/aave/gho-core
+[submodule "contracts/foundry-lib/solidity-utils"]
+	path = contracts/foundry-lib/solidity-utils
+	url = https://github.com/bgd-labs/solidity-utils

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,22 @@
+{
+    "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,
+    "optimistic_hashing": true,
+    "process": "emv",
+    "prover_args": ["-depth 10","-mediumTimeout 700"],
+    "smt_timeout": "600",
+    "solc": "solc8.24",
+    "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,133 @@
+/*
+    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 &&
+    f.selector != sig:setCurrentBridgedAmount(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);
+}
+
+definition filterSetter(method f) returns bool = f.selector != sig:setCurrentBridgedAmount(uint256).selector;
+
+/* ==============================================================================
+   rule: only_lockOrBurn_can_increase_currentBridged
+   ============================================================================*/
+rule only_lockOrBurn_can_increase_currentBridged(env e, method f) 
+  filtered { f -> filterSetter(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(Pool.LockOrBurnInV1).selector;
+}
+
+
+/* ==============================================================================
+   rule: only_releaseOrMint_currentBridged
+   ============================================================================*/
+rule only_releaseOrMint_currentBridged(env e, method f) 
+  filtered { f -> filterSetter(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(Pool.ReleaseOrMintInV1).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();
+}
+
+/* ==============================================================================
+   rule: only_owner_can_call_setCurrentBridgedAmount
+   ============================================================================*/
+rule only_owner_can_call_setCurrentBridgedAmount(env e) {
+  uint256 newBridgedAmount;
+
+  setCurrentBridgedAmount(e, newBridgedAmount);
+
+  assert e.msg.sender==owner();
+}

contracts/foundry.toml

@@ -6,8 +6,8 @@ optimizer_runs = 1_000_000
 src = 'src/v0.8'
 test = 'test/v0.8'
 out = 'foundry-artifacts'
-cache_path  = 'foundry-cache'
-libs = ['node_modules']
+cache_path = 'foundry-cache'
+libs = ['node_modules', 'foundry-lib']
 bytecode_hash = "none"
 ffi = false
 
@@ -33,7 +33,7 @@ evm_version = 'paris'
 solc_version = '0.8.19'
 src = 'src/v0.8/functions/dev/v1_X'
 test = 'src/v0.8/functions/tests/v1_X'
-gas_price = 3_000_000_000 # 3 gwei
+gas_price = 3_000_000_000              # 3 gwei
 
 [profile.vrf]
 optimizer_runs = 1_000

contracts/remappings.txt

@@ -6,3 +6,9 @@ hardhat/=node_modules/hardhat/
 @eth-optimism/=node_modules/@eth-optimism/
 @scroll-tech/=node_modules/@scroll-tech/
 @zksync/=node_modules/@zksync/
+
+@aave/=foundry-lib/gho-core/lib/aave-token/
+@aave-gho-core/=foundry-lib/gho-core/src/contracts/
+@aave/core-v3/=foundry-lib/gho-core/lib/aave-v3-core/
+@aave/periphery-v3/=foundry-lib/gho-core/lib/aave-v3-periphery/
+solidity-utils/=foundry-lib/solidity-utils/src/