NoBey/openzeppelin-contracts
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

flashMint finished

Browse Source
This commit is contained in:
Aleksander Kryukov
2022-04-04 21:16:15 +01:00
parent fe7d42dedd
commit a0b58c3071
1 changed files with 3 additions and 4 deletions
Download Patch File Download Diff File Expand all files Collapse all files

7
certora/specs/ERC20FlashMint.spec
View File

@ -1,9 +1,8 @@
import "erc20.spec" import "erc20.spec"
methods { methods {
onFlashLoan(address, address, uint256, uint256, bytes) => HAVOC_ALL maxFlashLoan(address) returns(uint256) envfree
_burn(address account, uint256 amount) returns(bool) => specBurn(account, amount)
_burn(address account, uint256 amount) returns(bool) => specBurn(account, amount);
} }
ghost mapping(address => uint256) trackedBurnAmount; ghost mapping(address => uint256) trackedBurnAmount;
@ -26,4 +25,4 @@ rule letsWatchItBurns(env e){
uint256 burned = trackedBurnAmount[receiver]; uint256 burned = trackedBurnAmount[receiver];
assert to_mathint(amount + feeBefore) == burned, "cheater"; assert to_mathint(amount + feeBefore) == burned, "cheater";
} }