From 15e847c835a0b2735056581fed97b50ef5b6b216 Mon Sep 17 00:00:00 2001 From: Thomas Adams Date: Tue, 31 May 2022 18:34:22 -0700 Subject: [PATCH] Added invariant balanceOfZeroAddressIsZero (partially passing) --- certora/specs/ERC1155Supply.spec | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) 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 /*