refactor: remove withdrawnAssets from ERC20Helper

morpho-org · Oct 29, 2024 · fb02d69 · fb02d69
1 parent c3b2c3a
commit fb02d69
Show file tree

Hide file tree

Showing 4 changed files with 12 additions and 17 deletions.
diff --git a/certora/helpers/ERC20Helper.sol b/certora/helpers/ERC20Helper.sol
@@ -1,11 +1,10 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 pragma solidity 0.8.21;
 
-import {IERC20, SafeERC20, IMorphoHarness, SharesMathLib, Id, Market} from "../munged/MetaMorpho.sol";
+import {IERC20, SafeERC20} from "../munged/MetaMorpho.sol";
 
 contract ERC20Helper {
     using SafeERC20 for IERC20;
-    using SharesMathLib for uint256;
 
     function balanceOf(address token, address user) external view returns (uint256) {
         return IERC20(token).balanceOf(user);
@@ -18,17 +17,4 @@ contract ERC20Helper {
     function safeTransferFrom(address token, address from, address to, uint256 amount) external {
         IERC20(token).safeTransferFrom(from, to, amount);
     }
-
-    function withdrawnAssets(IMorphoHarness morpho, Id id, uint256 assets, uint256 shares)
-        external
-        view
-        returns (uint256)
-    {
-        if (shares == 0) {
-            return assets;
-        } else {
-            Market memory market = morpho.market(id);
-            return shares.toAssetsDown(market.totalSupplyAssets, market.totalSupplyShares);
-        }
-    }
 }
diff --git a/certora/specs/ConsistentState.spec b/certora/specs/ConsistentState.spec
@@ -5,6 +5,7 @@ using Util as Util;
 
 methods {
     function Util.libId(MetaMorphoHarness.MarketParams) external returns(MetaMorphoHarness.Id) envfree;
+    function Util.libMulDivDown(uint256, uint256, uint256) external returns(uint256) envfree;
 }
 
 // Check that the fee cannot accrue to an unset fee recipient.

diff --git a/certora/specs/LastUpdated.spec b/certora/specs/LastUpdated.spec
@@ -8,9 +8,10 @@ methods {
     function ERC20.balanceOf(address, address) external returns(uint256) envfree;
     function ERC20.totalSupply(address) external returns(uint256) envfree;
     function ERC20.safeTransferFrom(address, address, address, uint256) external envfree;
-    function ERC20.withdrawnAssets(address, MetaMorphoHarness.Id, uint256, uint256) external returns (uint256) envfree;
 
     function Morpho.lastUpdate(MorphoHarness.Id) external returns(uint256) envfree;
+    function Morpho.virtualTotalSupplyAssets(MorphoHarness.Id) external returns(uint256) envfree;
+    function Morpho.virtualTotalSupplyShares(MorphoHarness.Id) external returns(uint256) envfree;
 }
 
 function hasCuratorRole(address user) returns bool {

diff --git a/certora/specs/Tokens.spec b/certora/specs/Tokens.spec
@@ -51,7 +51,14 @@ function summaryWithdraw(MetaMorphoHarness.MarketParams marketParams, uint256 as
     requireInvariant enabledHasConsistentAsset(marketParams);
 
     // Use effective withdrawn assets if shares are given as input.
-    uint256 withdrawn = ERC20.withdrawnAssets(MORPHO(), id, assets, shares);
+    uint256 withdrawn;
+    if (shares == 0) {
+        require withdrawn == assets;
+    } else {
+        uint256 totalAssets = Morpho.virtualTotalSupplyAssets(id);
+        uint256 totalShares = Morpho.virtualTotalSupplyShares(id);
+        require withdrawn == Util.libMulDivDown(shares, totalAssets, totalShares);
+    }
     // Summarize withdraw as just a transfer for the purpose of this specification file, which is sound because only the properties about tokens are verified in this file.
     ERC20.safeTransferFrom(marketParams.loanToken, MORPHO(), currentContract, withdrawn);