From a61981e403d53403c0d69da0a7ba34863e9d074d Mon Sep 17 00:00:00 2001
From: 0xb337r007 <0xe4e5@proton.me>
Date: Fri, 26 May 2023 11:27:58 +0200
Subject: [PATCH] fix max supply check

---
 contracts/mvp/CollectibleV1.sol |  2 +-
 specs/mvp/CollectibleV1.spec    |  2 ++
 test/mvp/CollectibleV1.ts       | 36 ++++++++++++++++++++++++++++-----
 3 files changed, 34 insertions(+), 6 deletions(-)

diff --git a/contracts/mvp/CollectibleV1.sol b/contracts/mvp/CollectibleV1.sol
index e07876c..7166997 100644
--- a/contracts/mvp/CollectibleV1.sol
+++ b/contracts/mvp/CollectibleV1.sol
@@ -67,7 +67,7 @@ contract CollectibleV1 is
     function mintTo(address[] memory addresses) external onlyOwner {
         // We cannot just use totalSupply() to create the new tokenId because tokens
         // can be burned so we use a separate counter.
-        require(_tokenIdTracker.current() + addresses.length < maxSupply, "MAX_SUPPLY_REACHED");
+        require(_tokenIdTracker.current() + addresses.length <= maxSupply, "MAX_SUPPLY_REACHED");
 
         for (uint256 i = 0; i < addresses.length; i++) {
             _safeMint(addresses[i], _tokenIdTracker.current(), "");
diff --git a/specs/mvp/CollectibleV1.spec b/specs/mvp/CollectibleV1.spec
index 108bc4d..1e2cc78 100644
--- a/specs/mvp/CollectibleV1.spec
+++ b/specs/mvp/CollectibleV1.spec
@@ -92,6 +92,8 @@ rule transferSoulbound {
 }
 
 rule maxSupplyNotLowerThanTotalSupply(env e, method f) {
+  require maxSupply() >= totalSupply();
+
   calldataarg args;
   f(e, args); // call all public/external functions of a contract
 
diff --git a/test/mvp/CollectibleV1.ts b/test/mvp/CollectibleV1.ts
index 367bacd..b2941fb 100644
--- a/test/mvp/CollectibleV1.ts
+++ b/test/mvp/CollectibleV1.ts
@@ -49,24 +49,50 @@ describe("CollectibleV1", function () {
 
     it("normal user cannot mint", async () => {
       const a = accounts[0];
-      await expect(
-        token.connect(a).mintTo([a.address])
-      ).to.be.revertedWith("Ownable: caller is not the owner");
+      await expect(token.connect(a).mintTo([a.address])).to.be.revertedWith(
+        "Ownable: caller is not the owner"
+      );
     });
 
     it("owner can mint", async () => {
-      const addresses = accounts.map(a => a.address);
+      const addresses = accounts.map((a) => a.address);
       for (let i = 0; i < addresses.length; i++) {
         expect(await token.balanceOf(addresses[i])).to.equal("0");
       }
 
-      await token.connect(owner).mintTo(addresses)
+      await token.connect(owner).mintTo(addresses);
 
       for (let i = 0; i < addresses.length; i++) {
         expect(await token.balanceOf(addresses[i])).to.equal("1");
       }
     });
 
+    it("owner can mint until max supply is reached", async () => {
+      const CollectibleV1 = await ethers.getContractFactory("CollectibleV1");
+      const maxSupply = BN(4);
+      const token = await CollectibleV1.deploy(
+        "Test Token",
+        "TEST",
+        maxSupply.toString(),
+        true,
+        true,
+        "http://test.local"
+      );
+
+      await token.connect(owner).mintTo([accounts[0].address]);
+      await token.connect(owner).mintTo([accounts[1].address]);
+      await token
+        .connect(owner)
+        .mintTo([accounts[2].address, accounts[3].address]);
+
+      await expect(
+        token.connect(owner).mintTo([accounts[4].address])
+      ).to.be.revertedWith("MAX_SUPPLY_REACHED");
+
+      expect(await token.maxSupply()).to.equal(4);
+      expect(await token.totalSupply()).to.equal(4);
+    });
+
     it("normal user cannot burn", async () => {
       const a = accounts[0];
       await expect(token.connect(a).remoteBurn([0])).to.be.revertedWith(