fix setMaxSupply to check total minted (#27)

.github/workflows/test.yml

@@ -135,7 +135,7 @@ jobs:
         with: { java-version: "11", java-package: jre }
 
       - name: Install Certora CLI
-        run: pip3 install certora-cli==5.0.5
+        run: pip3 install certora-cli==6.3.1
 
       - name: Install Solidity
         run: |

certora/certora.conf

@@ -0,0 +1,15 @@
+{
+  "files": [
+    "contracts/tokens/CollectibleV1.sol",
+    "certora/harness/CollectibleV1Harness.sol",
+    "contracts/tokens/OwnerToken.sol",
+    "contracts/tokens/MasterToken.sol"
+  ],
+  "msg": "Verifying CollectibleV1.sol",
+  "rule_sanity": "basic",
+  "verify": "CollectibleV1Harness:certora/specs/CollectibleV1.spec",
+  "link": ["CollectibleV1Harness:ownerToken=OwnerToken", "CollectibleV1Harness:masterToken=MasterToken"],
+  "packages": ["@openzeppelin=lib/openzeppelin-contracts"],
+  "optimistic_loop": true,
+  "loop_iter": "3"
+}

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;
+    }
+}

certora/scripts/verify-collectible-v1.sh

@@ -1,8 +1,10 @@
 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 \
 --rule_sanity "basic" \
 --wait_for_results "all" \
 --msg "Verifying CollectibleV1.sol"

certora/specs/CollectibleV1.spec

@@ -4,6 +4,128 @@ methods {
   function transferable() external returns (bool) envfree;
   function totalSupply() external returns (uint) envfree;
   function maxSupply() external returns (uint) envfree;
+  function setMaxSupply(uint256 newMaxSupply) external returns (uint);
+  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;
+}
+
+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);
+}
+
+function safeAssumptions() {
+  requireInvariant mintCountGreaterEqualTotalSupplyAndTotalSupplyEqBalances();
+}
+
+invariant mintCountGreaterEqualTotalSupplyAndTotalSupplyEqBalances()
+    to_mathint(mintedCount()) >= to_mathint(totalSupply()) &&
+      to_mathint(totalSupply()) == sumOfBalances;
+
+rule integrityOfMintTo {
+  requireInvariant mintCountGreaterEqualTotalSupplyAndTotalSupplyEqBalances();
+
+  address[] addresses;
+  env e;
+
+  mathint totalSupply_before = totalSupply();
+  mathint maxSupply = to_mathint(maxSupply());
+
+  address addr;
+
+  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 totalSupply_after = totalSupply();
+  mathint balance_addr_after = balanceOf(addr);
+
+  assert totalSupply_after == totalSupply_before + addresses.length;
+  assert balance_addr_after == balance_addr_before + count;
+}
+
+rule maxSupplyCannotBeLowerThanMintedCount() {
+  require maxSupply() >= mintedCount();
+
+  env e;
+  uint256 newMaxSupply;
+
+  setMaxSupply(e, newMaxSupply);
+
+  assert maxSupply() >= mintedCount();
+}
+
+rule maxSupplyNotLowerThanTotalSupply(env e, method f) {
+  require maxSupply() >= totalSupply();
+  requireInvariant mintCountGreaterEqualTotalSupplyAndTotalSupplyEqBalances();
+
+  calldataarg args;
+  f(e, args); // call all public/external functions of a contract
+
+  assert maxSupply() >= totalSupply();
+}
+
+rule mintToReverts() {
+  address[] addresses;
+  env e;
+
+  mathint supply_before = totalSupply();
+  mathint max_supply = maxSupply();
+  mathint minted_count = mintedCount();
+
+  require supply_before <= max_supply;
+  require minted_count >= supply_before;
+
+  mintTo@withrevert(e, addresses);
+
+  bool reverted = lastReverted;
+
+  assert (supply_before + addresses.length > max_supply) => reverted;
+
+  satisfy supply_before == max_supply && addresses.length > 0 && reverted;
+}
+
+rule mintToRelations() {
+  address[] addresses_1;
+  address[] addresses_2;
+  env e;
+
+  require addresses_1.length == 2;
+  require addresses_1.length == addresses_2.length;
+
+  require addresses_1[0] != addresses_1[1];
+  require addresses_1[0] == addresses_2[1];
+  require addresses_1[1] == addresses_2[0];
+
+  mathint supply_before = totalSupply();
+  mathint max_supply = maxSupply();
+  mathint minted_count = mintedCount();
+
+  require supply_before <= max_supply;
+  require minted_count >= supply_before;
+
+  address a;
+
+  storage s1 = lastStorage;
+  mintTo(e, addresses_1);
+  mathint balance_s1 = balanceOf(a);
+
+  mintTo(e, addresses_2) at s1;
+
+  mathint balance_s2 = balanceOf(a);
+  assert balance_s1 == balance_s2;
 }
 
 rule shouldPass {
@@ -15,90 +137,3 @@ rule shouldPass {
 /*     f(e, args); */
 /*     assert false; */
 /* } */
-
-/// rule mintTo_FromOwner {
-///   // address owner;
-///   address recipient_1;
-///   address recipient_2;
-///
-///   env e;
-///   require recipient_1 != recipient_2;
-///   // require e.msg.sender == owner;
-///   // require owner() == owner;
-///   require maxSupply() == 100000;
-///   require totalSupply() == 0;
-///   require balanceOf(recipient_1) == 0;
-///   require balanceOf(recipient_2) == 0;
-///
-///   assert balanceOf(recipient_1) == 0, "balance of recipient_1 should be 0";
-///   assert balanceOf(recipient_2) == 0, "balance of recipient_2 should be 0";
-///
-///   mintTo(e, [recipient_1, recipient_2]);
-///
-///   assert balanceOf(recipient_1) == 1, "balance of recipient_1 should be 1";
-///   assert balanceOf(recipient_2) == 1, "balance of recipient_2 should be 1";
-/// }
-///
-/// rule transferNFT_validOwner {
-///   address sender;
-///   address recipient;
-///   uint token_id;
-///
-///   env e;
-///   require e.msg.sender == sender;
-///   require sender != recipient;
-///   require ownerOf(token_id) == sender;
-///   require transferable() == true;
-///
-///   mathint balance_sender_before = balanceOf(sender);
-///   mathint balance_recipient_before = balanceOf(recipient);
-///
-///   transferFrom(e, sender, recipient, token_id);
-///
-///   assert ownerOf(token_id) == recipient;
-///   assert balanceOf(sender) == assert_uint256(balance_sender_before - 1);
-///   /* assert balanceOf(recipient) == balance_recipient_before + 1; */
-/// }
-///
-/// rule transferNFT_invalidOwner {
-///   address sender;
-///   address recipient;
-///   uint token_id;
-///
-///   env e;
-///   require e.msg.sender == sender;
-///   require sender != recipient;
-///   require ownerOf(token_id) != sender;
-///   require transferable() == true;
-///
-///   transferFrom@withrevert(e, sender, recipient, token_id);
-///   assert lastReverted, "transfer should revert when the sender is not the owner of tokenId";
-/// }
-///
-/// rule transferSoulbound {
-///   address sender;
-///   address recipient;
-///   uint token_id;
-///
-///   env e;
-///   require e.msg.sender == sender;
-///   require sender != recipient;
-///   require ownerOf(token_id) == sender;
-///   require transferable() == false;
-///
-///   mathint balance_sender_before = balanceOf(sender);
-///   mathint balance_recipient_before = balanceOf(recipient);
-///
-///   transferFrom@withrevert(e, sender, recipient, token_id);
-///
-///   assert lastReverted, "transfer should revert if it's a Soulbound token";
-/// }
-///
-/// rule maxSupplyNotLowerThanTotalSupply(env e, method f) {
-///   require maxSupply() >= totalSupply();
-///
-///   calldataarg args;
-///   f(e, args); // call all public/external functions of a contract
-///
-///   assert maxSupply() >= totalSupply();
-/// }

contracts/tokens/BaseToken.sol

@@ -69,7 +69,7 @@ abstract contract BaseToken is Context, ERC721Enumerable, CommunityOwnable {
     // External functions
 
     function setMaxSupply(uint256 newMaxSupply) external virtual onlyCommunityOwnerOrTokenMaster {
-        if (newMaxSupply < totalSupply()) {
+        if (newMaxSupply < mintedCount()) {
             revert BaseToken_MaxSupplyLowerThanTotalSupply();
         }
         maxSupply = newMaxSupply;
@@ -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);