From 27fa53bba9f16543e04b8632cef8d2e8f93cfb4b Mon Sep 17 00:00:00 2001
From: Michael George <mdgeorge@cs.cornell.edu>
Date: Thu, 2 Jun 2022 14:37:40 -0400
Subject: [PATCH] added init_state axiom for sum of balances

---
 certora/specs/ERC1155Supply.spec | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/certora/specs/ERC1155Supply.spec b/certora/specs/ERC1155Supply.spec
index 48bacb3ac..01f392e88 100644
--- a/certora/specs/ERC1155Supply.spec
+++ b/certora/specs/ERC1155Supply.spec
@@ -32,7 +32,9 @@ filtered {
 
 /******************************************************************************/
 
-ghost mapping(uint256 => mathint) sumOfBalances;
+ghost mapping(uint256 => mathint) sumOfBalances {
+    init_state axiom forall uint256 token . sumOfBalances[token] == 0;
+}
 
 hook Sstore _balances[KEY uint256 token][KEY address user] uint256 newValue (uint256 oldValue) STORAGE {
     sumOfBalances[token] = sumOfBalances[token] + newValue - oldValue;