From 36efa32a9c60d2ea1d62a3f63dba9e060db78731 Mon Sep 17 00:00:00 2001
From: 0xb337r007 <0xe4e5@proton.me>
Date: Sun, 11 Feb 2024 14:22:32 +0100
Subject: [PATCH] fix integrityOfMintTo

---
 certora/certora.conf                     |  4 +-
 certora/harness/CollectibleV1Harness.sol | 44 ++++++++++++++++++++
 certora/scripts/verify-collectible-v1.sh |  3 +-
 certora/specs/CollectibleV1.spec         | 51 +++++++++++++++---------
 contracts/tokens/BaseToken.sol           |  2 +-
 5 files changed, 82 insertions(+), 22 deletions(-)
 create mode 100644 certora/harness/CollectibleV1Harness.sol

diff --git a/certora/certora.conf b/certora/certora.conf
index 85eee90..788d145 100644
--- a/certora/certora.conf
+++ b/certora/certora.conf
@@ -1,8 +1,8 @@
 {
-  "files": ["contracts/tokens/CollectibleV1.sol"],
+  "files": ["contracts/tokens/CollectibleV1.sol", "certora/harness/CollectibleV1Harness.sol"],
   "msg": "Verifying CollectibleV1.sol",
   "rule_sanity": "basic",
-  "verify": "CollectibleV1:certora/specs/CollectibleV1.spec",
+  "verify": "CollectibleV1Harness:certora/specs/CollectibleV1.spec",
   "wait_for_results": "all",
   "packages": ["@openzeppelin=lib/openzeppelin-contracts"]
 }
diff --git a/certora/harness/CollectibleV1Harness.sol b/certora/harness/CollectibleV1Harness.sol
new file mode 100644
index 0000000..6ee0023
--- /dev/null
+++ b/certora/harness/CollectibleV1Harness.sol
@@ -0,0 +1,44 @@
+// SPDX-License-Identifier: Mozilla Public License 2.0
+pragma solidity ^0.8.17;
+
+import {CollectibleV1} from "../../contracts/tokens/CollectibleV1.sol";
+
+contract CollectibleV1Harness is CollectibleV1 {
+    constructor(
+        string memory name,
+        string memory symbol,
+        uint256 maxSupply,
+        bool remoteBurnable,
+        bool transferable,
+        string memory baseURI,
+        address ownerToken,
+        address masterToken
+    )
+        CollectibleV1(
+            name,
+            symbol,
+            maxSupply,
+            remoteBurnable,
+            transferable,
+            baseURI,
+            ownerToken,
+            masterToken
+        )
+    {}
+
+    /**
+     * @notice A helper function to count the number of occurrences of an address in a list.
+     */
+    function countAddressOccurrences(
+        address[] memory list,
+        address addr
+    ) external pure returns (uint) {
+        uint256 count = 0;
+        for (uint256 i = 0; i < list.length; i++) {
+            if (list[i] == addr) {
+                count++;
+            }
+        }
+        return count;
+    }
+}
diff --git a/certora/scripts/verify-collectible-v1.sh b/certora/scripts/verify-collectible-v1.sh
index 9af2007..3de5760 100755
--- a/certora/scripts/verify-collectible-v1.sh
+++ b/certora/scripts/verify-collectible-v1.sh
@@ -1,6 +1,7 @@
 certoraRun \
   contracts/tokens/CollectibleV1.sol \
---verify CollectibleV1:certora/specs/CollectibleV1.spec \
+  certora/harness/CollectibleV1Harness.sol \
+--verify CollectibleV1Harness:certora/specs/CollectibleV1.spec \
 --packages @openzeppelin=lib/openzeppelin-contracts \
 --optimistic_loop \
 --loop_iter 3 \
diff --git a/certora/specs/CollectibleV1.spec b/certora/specs/CollectibleV1.spec
index 0c1c800..6dcf789 100644
--- a/certora/specs/CollectibleV1.spec
+++ b/certora/specs/CollectibleV1.spec
@@ -4,36 +4,51 @@ methods {
   function transferable() external returns (bool) envfree;
   function totalSupply() external returns (uint) envfree;
   function maxSupply() external returns (uint) envfree;
+  function mintTo(address[]) external;
   function mintedCount() external returns (uint) envfree;
+  function countAddressOccurrences(address[], address) external returns (uint) envfree;
+  function _.onERC721Received(address, address, uint256, bytes) external => NONDET;
 }
 
-rule integrityOfMintTo() {
+ghost mathint sumOfBalances {
+    init_state axiom sumOfBalances == 0;
+}
+
+hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) STORAGE {
+    sumOfBalances = sumOfBalances - oldValue + newValue;
+}
+
+hook Sload uint256 balance _balances[KEY address addr] STORAGE {
+    require sumOfBalances >= to_mathint(balance);
+}
+
+invariant mintCountGreaterEqualTotalSupplyAndTotalSupplyEqBalances()
+    to_mathint(mintedCount()) >= to_mathint(totalSupply()) &&
+      to_mathint(totalSupply()) == sumOfBalances;
+
+rule integrityOfMintTo {
+  requireInvariant mintCountGreaterEqualTotalSupplyAndTotalSupplyEqBalances();
+
   address[] addresses;
-  uint index;
   env e;
 
-  require addresses.length > 0;
-  require index >= 0 && index < addresses.length;
+  mathint totalSupply_before = totalSupply();
+  mathint maxSupply = to_mathint(maxSupply());
 
+  address addr;
 
-  mathint supply_before = totalSupply();
-  mathint max_supply = maxSupply();
-  mathint minted_count = mintedCount();
-
-  address a = addresses[index];
-  mathint balance_before = balanceOf(a);
-
-  require supply_before <= max_supply;
-  require minted_count >= supply_before;
+  require totalSupply_before < maxSupply;
+  require totalSupply_before + addresses.length <= maxSupply;
 
+  mathint balance_addr_before = balanceOf(addr);
+  mathint count = countAddressOccurrences(addresses, addr);
   mintTo(e, addresses);
 
-  mathint supply_after = totalSupply();
+  mathint totalSupply_after = totalSupply();
+  mathint balance_addr_after = balanceOf(addr);
 
-  assert supply_after <= max_supply;
-  assert supply_after == supply_before + to_mathint(addresses.length);
-
-  assert to_mathint(balanceOf(a)) > balance_before;
+  assert totalSupply_after == totalSupply_before + addresses.length;
+  assert balance_addr_after == balance_addr_before + count;
 }
 
 
diff --git a/contracts/tokens/BaseToken.sol b/contracts/tokens/BaseToken.sol
index 7d37a4a..af46621 100644
--- a/contracts/tokens/BaseToken.sol
+++ b/contracts/tokens/BaseToken.sol
@@ -82,7 +82,7 @@ abstract contract BaseToken is Context, ERC721Enumerable, CommunityOwnable {
      *
      */
     function mintTo(address[] memory addresses) public onlyCommunityOwnerOrTokenMaster {
-        if (_tokenIdTracker.current() + addresses.length > maxSupply) {
+        if (mintedCount() + addresses.length > maxSupply) {
             revert BaseToken_MaxSupplyReached();
         }
         _mintTo(addresses);