Finish ERC20FlashMint

certora/specs/ERC20FlashMint.spec

@@ -1,15 +1,15 @@
-import "helpers/helpers.spec"
-import "methods/IERC20.spec"
-import "methods/IERC3156.spec"
+import "helpers/helpers.spec";
+import "methods/IERC20.spec";
+import "methods/IERC3156.spec";
 
 methods {
     // non standard ERC3156 functions
-    flashFeeReceiver() returns (address) envfree
+    function flashFeeReceiver() external returns (address) envfree;
 
     // function summaries below
-    _mint(address account, uint256 amount)              => specMint(account, amount)
-    _burn(address account, uint256 amount)              => specBurn(account, amount)
-    _transfer(address from, address to, uint256 amount) => specTransfer(from, to, amount)
+    function _._mint(address account, uint256 amount)              internal => specMint(account, amount)        expect void ALL;
+    function _._burn(address account, uint256 amount)              internal => specBurn(account, amount)        expect void ALL;
+    function _._transfer(address from, address to, uint256 amount) internal => specTransfer(from, to, amount)   expect void ALL;
 }
 
 /*
@@ -17,13 +17,13 @@ methods {
 │ Ghost: track mint and burns in the CVL                                                                              │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
-ghost mapping(address => uint256)                     trackedMintAmount;
-ghost mapping(address => uint256)                     trackedBurnAmount;
-ghost mapping(address => mapping(address => uint256)) trackedTransferedAmount;
+ghost mapping(address => mathint)                     trackedMintAmount;
+ghost mapping(address => mathint)                     trackedBurnAmount;
+ghost mapping(address => mapping(address => mathint)) trackedTransferedAmount;
 
-function specMint(address account, uint256 amount)              returns bool { trackedMintAmount[account] = amount;        return true; }
-function specBurn(address account, uint256 amount)              returns bool { trackedBurnAmount[account] = amount;        return true; }
-function specTransfer(address from, address to, uint256 amount) returns bool { trackedTransferedAmount[from][to] = amount; return true; }
+function specMint(address account, uint256 amount)              { trackedMintAmount[account] = amount;        }
+function specBurn(address account, uint256 amount)              { trackedBurnAmount[account] = amount;        }
+function specTransfer(address from, address to, uint256 amount) { trackedTransferedAmount[from][to] = amount; }
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
@@ -37,12 +37,12 @@ rule checkMintAndBurn(env e) {
     uint256 amount;
     bytes data;
 
-    uint256 fees = flashFee(token, amount);
+    mathint fees = flashFee(token, amount);
     address recipient = flashFeeReceiver();
 
     flashLoan(e, receiver, token, amount, data);
 
-    assert trackedMintAmount[receiver] == amount;
-    assert trackedBurnAmount[receiver] == amount + (recipient == 0 ? fees : 0);
+    assert trackedMintAmount[receiver] == to_mathint(amount);
+    assert trackedBurnAmount[receiver] == amount + to_mathint(recipient == 0 ? fees : 0);
     assert (fees > 0 && recipient != 0) => trackedTransferedAmount[receiver][recipient] == fees;
 }

certora/specs/methods/IERC3156.spec

@@ -1,5 +1,8 @@
 methods {
-    maxFlashLoan(address)                    returns (uint256) envfree => DISPATCHER(true)
-    flashFee(address,uint256)                returns (uint256) envfree => DISPATCHER(true)
-    flashLoan(address,address,uint256,bytes) returns (bool)            => DISPATCHER(true)
+    function maxFlashLoan(address)                    external returns (uint256) envfree;
+    function flashFee(address,uint256)                external returns (uint256) envfree;
+    function flashLoan(address,address,uint256,bytes) external returns (bool);
+
+    // IERC3156FlashBorrower
+    function _.onFlashLoan(address,address,uint256,uint256,bytes) external => DISPATCHER(true);
 }