fix max supply check

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(), "");

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
 

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(