[Certora] More thorough verification

certora/dispatch/ERC20NoRevert.sol

@@ -5,7 +5,8 @@ contract ERC20NoRevert {
     string public name;
     string public symbol;
     uint256 public decimals;
-    address owner;
+    address public owner;
+    uint256 public totalSupply;
     mapping(address => uint256) public balanceOf;
     mapping(address => mapping(address => uint256)) public allowed;
 
@@ -35,6 +36,9 @@ contract ERC20NoRevert {
     }
 
     function transferFrom(address _from, address _to, uint256 _amount) public returns (bool) {
+        if (allowed[_from][msg.sender] < _amount) {
+            return false;
+        }
         allowed[_from][msg.sender] -= _amount;
         return _transfer(_from, _to, _amount);
     }
@@ -51,5 +55,6 @@ contract ERC20NoRevert {
 
     function mint(address _receiver, uint256 _amount) public onlyOwner {
         balanceOf[_receiver] += _amount;
+        totalSupply += _amount;
     }
 }

certora/dispatch/ERC20USDT.sol

@@ -7,7 +7,8 @@ contract ERC20USDT {
     string public name;
     string public symbol;
     uint256 public decimals;
-    address owner;
+    uint256 public totalSupply;
+    address public owner;
     mapping(address => uint256) public balanceOf;
     mapping(address => mapping(address => uint256)) public allowed;
 
@@ -23,7 +24,7 @@ contract ERC20USDT {
         _;
     }
 
-    function _transfer(address _from, address _to, uint256 _amount) public {
+    function _transfer(address _from, address _to, uint256 _amount) internal {
         balanceOf[_from] -= _amount;
         balanceOf[_to] += _amount;
     }
@@ -51,5 +52,6 @@ contract ERC20USDT {
 
     function mint(address _receiver, uint256 _amount) public onlyOwner {
         balanceOf[_receiver] += _amount;
+        totalSupply += _amount;
     }
 }

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;
+}