diff --git a/certora/specs/ERC1155Supply.spec b/certora/specs/ERC1155Supply.spec index b5c84cc3f..a810a06a0 100644 --- a/certora/specs/ERC1155Supply.spec +++ b/certora/specs/ERC1155Supply.spec @@ -4,7 +4,7 @@ methods { balanceOf(address, uint256) returns uint256 envfree exists_wrapper(uint256) returns bool envfree } - + /// given two different token ids, if totalSupply for one changes, then /// totalSupply for other should not rule token_totalSupply_independence(method f) @@ -60,6 +60,10 @@ rule total_supply_is_sum_of_balances_as_rule { /******************************************************************************/ +/// The balance of a token for the zero address must be zero. +invariant balanceOfZeroAddressIsZero(uint256 token) + balanceOf(0, token) == 0 + // if a user has a token, then the token should exist /*