refactor: rename transfer to not only verify summary

morpho-org · Aug 17, 2023 · e0a9b50 · e0a9b50
1 parent 5b9dc63
commit e0a9b50
Show file tree

Hide file tree

Showing 4 changed files with 10 additions and 8 deletions.
diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
@@ -47,5 +47,5 @@ jobs:
           - verifyBlue.sh
           - verifyBlueRatioMathSummary.sh
           - verifyBlueExitLiquidity.sh
-          - verifyBlueTransferSummary.sh
+          - verifyBlueTransfer.sh
           - verifyReentrancy.sh
diff --git a/certora/harness/TransferHarness.sol b/certora/harness/TransferHarness.sol
@@ -5,20 +5,22 @@ 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);
+    function balanceOf(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 {
-        IERC20Extended(token).transferFrom(from, to, value);
+        IERC20(token).safeTransferFrom(from, to, value);
     }
 
-    function getBalance(address token, address user) public returns (uint256) {
+    function getBalance(address token, address user) public view returns (uint256) {
         return IERC20Extended(token).balanceOf(user);
     }
 
-    function getTotalSupply(address token) public returns (uint256) {
+    function getTotalSupply(address token) public view returns (uint256) {
         return IERC20Extended(token).totalSupply();
     }
 }
diff --git a/certora/scripts/verifyBlueTransferSummary.sh → certora/scripts/verifyBlueTransfer.sh b/certora/scripts/verifyBlueTransferSummary.sh → certora/scripts/verifyBlueTransfer.sh
@@ -7,7 +7,7 @@ certoraRun \
     certora/dispatch/ERC20Good.sol \
     certora/dispatch/ERC20USDT.sol \
     certora/dispatch/ERC20NoRevert.sol \
-    --verify TransferHarness:certora/specs/BlueTransferSummary.spec \
+    --verify TransferHarness:certora/specs/BlueTransfer.spec \
     --packages openzeppelin-contracts=lib/openzeppelin-contracts/contracts \
     --loop_iter 3 \
     --optimistic_loop \

diff --git a/certora/specs/BlueTransferSummary.spec → certora/specs/BlueTransfer.spec b/certora/specs/BlueTransferSummary.spec → certora/specs/BlueTransfer.spec
@@ -22,7 +22,7 @@ function summarySafeTransferFrom(address token, address from, address to, uint25
     }
 }
 
-rule checkTransferSummary(address token, address from, address to, uint256 amount) {
+rule checkTransfer(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));