feat: dispatch tokens

morpho-org · May 21, 2024 · 79371b5 · 79371b5
1 parent 37b91d4
commit 79371b5
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 1 deletion.
diff --git a/certora/confs/SupplyCap.conf b/certora/confs/SupplyCap.conf
@@ -3,6 +3,7 @@
         "lib/morpho-blue/certora/harness/MorphoHarness.sol",
         "certora/helpers/MetaMorphoHarness.sol",
         "certora/helpers/Util.sol",
+        "certora/dispatch/ERC20Standard.sol",
     ],
     "parametric_contracts": [
         "MetaMorphoHarness",
@@ -14,6 +15,7 @@
         "MorphoHarness": "solc-0.8.19",
         "MetaMorphoHarness": "solc-0.8.21",
         "Util": "solc-0.8.21",
+        "ERC20Standard": "solc-0.8.21",
     },
     "verify": "MetaMorphoHarness:certora/specs/SupplyCap.spec",
     "loop_iter": "2",

diff --git a/certora/specs/SupplyCap.spec b/certora/specs/SupplyCap.spec
@@ -15,7 +15,8 @@ methods {
     function Util.libId(MetaMorphoHarness.MarketParams) external returns(MetaMorphoHarness.Id) envfree;
     function Util.toAssetsDown(uint256, uint256, uint256) external returns(uint256) envfree;
 
-    function _.balanceOf(address) external => NONDET;
+    function _.balanceOf(address) external => DISPATCHER(true);
+    function _.transfer(address, uint256) external => DISPATCHER(true);
 }
 
 function supplyAssets(MetaMorphoHarness.Id id, address user) returns uint256 {