held tokens should exist passing

certora/harnesses/ERC1155/ERC1155SupplyHarness.sol

@@ -4,5 +4,11 @@ contract ERC1155SupplyHarness is ERC1155Supply {
     constructor(string memory uri_)
         ERC1155(uri_)
     {}
+
+    // workaround for problem caused by `exists` being a CVL keyword
+    function exists_wrapper(uint256 id) public view virtual returns (bool) {
+        return exists(id);
+    }
+
 }
 

certora/specs/ERC1155Supply.spec

@@ -2,6 +2,7 @@
 methods {
     totalSupply(uint256) returns uint256 envfree
     balanceOf(address, uint256) returns uint256 envfree
+    exists_wrapper(uint256) returns bool envfree
 }
 
 /// given two different token ids, if totalSupply for one changes, then
@@ -29,15 +30,56 @@ filtered {
         "methods must not change the total supply of more than one token";
 }
 
-invariant sum_user_token_balances_vs_totalSupply(uint256 id, address user1, address user2)
-    balanceOf(user1, id) + balanceOf(user2, id) <= totalSupply(id) 
-{ preserved {
-    require user1 != user2;
-    //for every address not user1 or user2, balance is < user1 and < user2
-    require forall address user3. (user3 != user1 && user3 != user2) => balanceOf(user3, id) < balanceOf(user1, id) && balanceOf(user3, id) < balanceOf(user2, id);
+/******************************************************************************/
+
+ghost mapping(uint256 => mathint) sumOfBalances;
+
+hook Sstore _balances[KEY uint256 token][KEY address user] uint256 newValue (uint256 oldValue) STORAGE {
+    sumOfBalances[token] = sumOfBalances[token] + newValue - oldValue;
 }
+
+// status: not passing, because mint and burn are the same as transferring to/from
+//         the 0 address.
+invariant total_supply_is_sum_of_balances(uint256 token)
+    sumOfBalances[token] == totalSupply(token) + balanceOf(0, token)
+
+rule total_supply_is_sum_of_balances_as_rule {
+    uint256 token;
+
+    require sumOfBalances[token] == totalSupply(token) + balanceOf(0, token);
+
+    mathint sum_before = sumOfBalances[token];
+
+    method f; calldataarg arg; env e;
+    f(e, arg);
+
+    mathint sum_after = sumOfBalances[token];
+
+    assert sumOfBalances[token] == totalSupply(token) + balanceOf(0, token);
 }
 
+/******************************************************************************/
+
+// if a user has a token, then the token should exist
+
+/*
+hook Sload _balances[...] {
+    require balance <= totalSupply
+}
+*/
+
+rule held_tokens_should_exist {
+    address user; uint256 token;
+
+    // This assumption is safe because of total_supply_is_sum_of_balances
+    require balanceOf(user, token) <= totalSupply(token);
+
+    assert balanceOf(user, token) > 0 => exists_wrapper(token),
+        "if a user's balance for a token is positive, the token must exist";
+}
+
+/******************************************************************************/
+
 rule sanity {
     method f; env e; calldataarg args;
 
@@ -45,4 +87,3 @@ rule sanity {
 
     assert false;
 }
-