[Certora] Dispatch tokens and verify safe transfer lib

.github/workflows/certora.yml

@@ -14,6 +14,9 @@ jobs:
     steps:
       - uses: actions/checkout@v3
 
+      - name: Install submodules
+        run: git submodule update --init --recursive
+
       - name: Install python
         uses: actions/setup-python@v4
         with:
@@ -44,4 +47,5 @@ jobs:
           - verifyBlue.sh
           - verifyBlueRatioMathSummary.sh
           - verifyBlueExitLiquidity.sh
+          - verifyBlueTransferSummary.sh
           - verifyReentrancy.sh

certora/dispatch/ERC20Bad.sol

@@ -0,0 +1,12 @@
+// SPDX-License-Identifier: UNLICENSED
+pragma solidity ^0.8.0;
+
+import {ERC20} from "openzeppelin-contracts/token/ERC20/ERC20.sol";
+
+contract ERC20Bad is ERC20 {
+    constructor(string memory name, string memory symbol) ERC20(name, symbol) {}
+
+    function _beforeTokenTransfer(address from, address to, uint256 amount) internal override {
+        _mint(to, amount);
+    }
+}

certora/dispatch/ERC20Good.sol

@@ -0,0 +1,8 @@
+// SPDX-License-Identifier: UNLICENSED
+pragma solidity ^0.8.0;
+
+import {ERC20} from "openzeppelin-contracts/token/ERC20/ERC20.sol";
+
+contract ERC20Good is ERC20 {
+    constructor(string memory name, string memory symbol) ERC20(name, symbol) {}
+}

certora/dispatch/ERC20USDT.sol

@@ -0,0 +1,52 @@
+// SPDX-License-Identifier: UNLICENSED
+pragma solidity ^0.8.0;
+
+contract ERC20USDT {
+    uint256 public constant MAX_UINT = 2 ** 256 - 1;
+
+    string public name;
+    string public symbol;
+    uint256 public decimals;
+    address owner;
+    mapping(address => uint256) public balanceOf;
+    mapping(address => mapping(address => uint256)) public allowed;
+
+    constructor(string memory _name, string memory _symbol, uint256 _decimals) {
+        name = _name;
+        symbol = _symbol;
+        decimals = _decimals;
+        owner = msg.sender;
+    }
+
+    modifier onlyOwner() {
+        require(msg.sender == owner);
+        _;
+    }
+
+    function transfer(address _to, uint256 _value) public {
+        balanceOf[msg.sender] -= _value;
+        balanceOf[_to] += _value;
+    }
+
+    function transferFrom(address _from, address _to, uint256 _value) public {
+        if (allowed[_from][msg.sender] < MAX_UINT) {
+            allowed[_from][msg.sender] -= _value;
+        }
+        balanceOf[_from] -= _value;
+        balanceOf[_to] += _value;
+    }
+
+    function approve(address _spender, uint256 _value) public {
+        require(!((_value != 0) && (allowed[msg.sender][_spender] != 0)));
+
+        allowed[msg.sender][_spender] = _value;
+    }
+
+    function allowance(address _owner, address _spender) public view returns (uint256 remaining) {
+        return allowed[_owner][_spender];
+    }
+
+    function mint(address _receiver, uint256 amount) public onlyOwner {
+        balanceOf[owner] += amount;
+    }
+}

certora/harness/TransferHarness.sol

@@ -0,0 +1,24 @@
+// SPDX-License-Identifier: UNLICENSED
+pragma solidity ^0.8.0;
+
+import "../../src/libraries/SafeTransferLib.sol";
+import "../../src/interfaces/IERC20.sol";
+
+interface IERC20Extended is IERC20 {
+    function balanceOf(address) external returns (uint256);
+    function totalSupply() external returns (uint256);
+}
+
+contract TransferHarness {
+    function doTransfer(address token, address from, address to, uint256 value) public {
+        IERC20Extended(token).transferFrom(from, to, value);
+    }
+
+    function getBalance(address token, address user) public returns (uint256) {
+        return IERC20Extended(token).balanceOf(user);
+    }
+
+    function getTotalSupply(address token) public returns (uint256) {
+        return IERC20Extended(token).totalSupply();
+    }
+}

certora/scripts/verifyBlueTransferSummary.sh

@@ -0,0 +1,14 @@
+#!/bin/bash
+
+set -euxo pipefail
+
+certoraRun \
+    certora/harness/TransferHarness.sol \
+    certora/dispatch/ERC20Good.sol \
+    certora/dispatch/ERC20USDT.sol \
+    --verify TransferHarness:certora/specs/BlueTransferSummary.spec \
+    --packages openzeppelin-contracts=lib/openzeppelin-contracts/contracts \
+    --loop_iter 3 \
+    --optimistic_loop \
+    --msg "Morpho Transfer Summary" \
+    "$@"

certora/specs/BlueTransferSummary.spec

@@ -0,0 +1,39 @@
+methods {
+    function doTransfer(address, address, address, uint256) external envfree;
+    function getBalance(address, address) external returns (uint256) envfree;
+    function getTotalSupply(address) external returns (uint256) envfree;
+
+    function _.transferFrom(address, address, uint256) external => DISPATCHER(true);
+    function _.balanceOf(address) external => DISPATCHER(true);
+    function _.totalSupply() external => DISPATCHER(true);
+}
+
+ghost mapping(address => mathint) myBalances
+{
+    init_state axiom (forall address token. myBalances[token] == 0);
+}
+
+function summarySafeTransferFrom(address token, address from, address to, uint256 amount) {
+    if (from == currentContract) {
+        myBalances[token] = require_uint256(myBalances[token] - amount);
+    }
+    if (to == currentContract) {
+        myBalances[token] = require_uint256(myBalances[token] + amount);
+    }
+}
+
+rule checkTransferSummary(address token, address from, address to, uint256 amount) {
+    require from == currentContract || to == currentContract;
+
+    require from != to => getBalance(token, from) + getBalance(token, to) <= to_mathint(getTotalSupply(token));
+
+    uint256 initialBalance = getBalance(token, currentContract);
+    doTransfer(token, from, to, amount);
+    uint256 finalBalance = getBalance(token, currentContract);
+
+    mathint initialGhostBalance = myBalances[token];
+    summarySafeTransferFrom(token, from, to, amount);
+    mathint finalGhostBalance = myBalances[token];
+
+    assert finalGhostBalance - initialGhostBalance == finalBalance - initialBalance;
+}