feat: more thourough verification of the transfer lib

Author: QGarchery

certora/harness/TransferHarness.sol

@@ -6,20 +6,29 @@ import "../../src/interfaces/IERC20.sol";
 
 interface IERC20Extended is IERC20 {
     function balanceOf(address) external view returns (uint256);
+    function allowance(address, address) external view returns (uint256);
     function totalSupply() external view returns (uint256);
 }
 
 contract TransferHarness {
     using SafeTransferLib for IERC20;
 
-    function doTransfer(address token, address from, address to, uint256 value) public {
+    function doTransferFrom(address token, address from, address to, uint256 value) public {
         IERC20(token).safeTransferFrom(from, to, value);
     }
 
+    function doTransfer(address token, address to, uint256 value) public {
+        IERC20(token).safeTransfer(to, value);
+    }
+
     function getBalance(address token, address user) public view returns (uint256) {
         return IERC20Extended(token).balanceOf(user);
     }
 
+    function getAllowance(address token, address owner, address spender) public view returns (uint256) {
+        return IERC20Extended(token).allowance(owner, spender);
+    }
+
     function getTotalSupply(address token) public view returns (uint256) {
         return IERC20Extended(token).totalSupply();
     }

certora/specs/BlueTransfer.spec

@@ -1,10 +1,14 @@
 methods {
-    function doTransfer(address, address, address, uint256) external envfree;
+    function doTransfer(address, address, uint256) external envfree;
+    function doTransferFrom(address, address, address, uint256) external envfree;
     function getBalance(address, address) external returns (uint256) envfree;
+    function getAllowance(address, address, address) external returns (uint256) envfree;
     function getTotalSupply(address) external returns (uint256) envfree;
 
+    function _.transfer(address, uint256) external => DISPATCHER(true);
     function _.transferFrom(address, address, uint256) external => DISPATCHER(true);
     function _.balanceOf(address) external => DISPATCHER(true);
+    function _.allowance(address, address) external => DISPATCHER(true);
     function _.totalSupply() external => DISPATCHER(true);
 }
 
@@ -22,16 +26,49 @@ function summarySafeTransferFrom(address token, address from, address to, uint25
     }
 }
 
-rule checkTransfer(address token, address from, address to, uint256 amount) {
-    require from == currentContract || to == currentContract;
+rule checkTransferFromSummary(address token, address from, uint256 amount) {
+    mathint initialBalance = getBalance(token, currentContract);
+    require from != currentContract => initialBalance + getBalance(token, from) <= to_mathint(getTotalSupply(token));
+
+    doTransferFrom(token, from, currentContract, amount);
+    mathint finalBalance = getBalance(token, currentContract);
 
-    require from != to => getBalance(token, from) + getBalance(token, to) <= to_mathint(getTotalSupply(token));
+    require myBalances[token] == initialBalance;
+    summarySafeTransferFrom(token, from, currentContract, amount);
+    assert myBalances[token] == finalBalance;
+}
 
+rule checkTransferSummary(address token, address to, uint256 amount) {
     mathint initialBalance = getBalance(token, currentContract);
-    doTransfer(token, from, to, amount);
+    require to != currentContract => initialBalance + getBalance(token, to) <= to_mathint(getTotalSupply(token));
+
+    doTransfer(token, to, amount);
     mathint finalBalance = getBalance(token, currentContract);
 
     require myBalances[token] == initialBalance;
-    summarySafeTransferFrom(token, from, to, amount);
+    summarySafeTransferFrom(token, currentContract, to, amount);
     assert myBalances[token] == finalBalance;
 }
+
+rule transferRevertCondition(address token, address to, uint256 amount) {
+    uint256 initialBalance = getBalance(token, currentContract);
+    uint256 toInitialBalance = getBalance(token, to);
+    require to != currentContract => initialBalance + toInitialBalance <= to_mathint(getTotalSupply(token));
+    require currentContract != 0 && to != 0;
+
+    doTransfer@withrevert(token, to, amount);
+
+    assert lastReverted == (initialBalance < amount);
+}
+
+rule transferFromRevertCondition(address token, address from, address to, uint256 amount) {
+    uint256 initialBalance = getBalance(token, from);
+    uint256 toInitialBalance = getBalance(token, to);
+    uint256 allowance = getAllowance(token, from, currentContract);
+    require to != from => initialBalance + toInitialBalance <= to_mathint(getTotalSupply(token));
+    require from != 0 && to != 0;
+
+    doTransferFrom@withrevert(token, from, to, amount);
+
+    assert lastReverted == (initialBalance < amount) || allowance < amount;
+}