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

Added rule singleTokenBurnBurnBatchEquivalence (passing)

Browse Source
This commit is contained in:
Thomas Adams
2022-05-31 16:02:23 -07:00
parent f74e316422
commit 38495a5026
1 changed files with 26 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

26
certora/specs/ERC1155Burnable.spec
View File

@ -77,6 +77,32 @@ rule sequentialBatchBurnsEquivalentToSingleBurnBatchOfSum { // TODO implement ru
"just a placeholder that should never show up";
}
/// The result of burning a single token must be equivalent whether done via
/// burn or burnBatch.
rule singleTokenBurnBurnBatchEquivalence {
storage beforeBurn = lastStorage;
env e;
address holder;
uint256 token; uint256 burnAmount;
uint256[] tokens; uint256[] burnAmounts;
mathint startingBalance = balanceOf(holder, token);
require tokens.length == 1; require burnAmounts.length == 1;
require tokens[0] == token; require burnAmounts[0] == burnAmount;
// burning via burn
burn(e, holder, token, burnAmount) at beforeBurn;
mathint burnBalanceChange = startingBalance - balanceOf(holder, token);
// burning via burnBatch
burnBatch(e, holder, tokens, burnAmounts) at beforeBurn;
mathint burnBatchBalanceChange = startingBalance - balanceOf(holder, token);
assert burnBalanceChange == burnBatchBalanceChange,
"Burning a single token via burn or burnBatch must be equivalent";
}
/// This rule should always fail.
rule sanity {
method f; env e; calldataarg args;