From 77b799111d164e9849b8c4d8d3618dbcbaeac5a5 Mon Sep 17 00:00:00 2001
From: 0xb337r007 <0xe4e5@proton.me>
Date: Sun, 18 Feb 2024 15:24:57 +0100
Subject: [PATCH] update certora config and add a rule for setMaxSupply

---
 certora/certora.conf             |  13 +++-
 certora/specs/CollectibleV1.spec | 111 ++++++-------------------------
 2 files changed, 32 insertions(+), 92 deletions(-)

diff --git a/certora/certora.conf b/certora/certora.conf
index 788d145..dea973e 100644
--- a/certora/certora.conf
+++ b/certora/certora.conf
@@ -1,8 +1,15 @@
 {
-  "files": ["contracts/tokens/CollectibleV1.sol", "certora/harness/CollectibleV1Harness.sol"],
+  "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",
-  "wait_for_results": "all",
-  "packages": ["@openzeppelin=lib/openzeppelin-contracts"]
+  "link": ["CollectibleV1Harness:ownerToken=OwnerToken", "CollectibleV1Harness:masterToken=MasterToken"],
+  "packages": ["@openzeppelin=lib/openzeppelin-contracts"],
+  "optimistic_loop": true,
+  "loop_iter": "3"
 }
diff --git a/certora/specs/CollectibleV1.spec b/certora/specs/CollectibleV1.spec
index 6dcf789..57e4c7f 100644
--- a/certora/specs/CollectibleV1.spec
+++ b/certora/specs/CollectibleV1.spec
@@ -4,6 +4,7 @@ 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;
@@ -22,6 +23,10 @@ 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;
@@ -51,10 +56,25 @@ rule integrityOfMintTo {
   assert balance_addr_after == balance_addr_before + count;
 }
 
+rule maxSupplyCannotBeLowerThanMintedCount() {
+  require maxSupply() >= mintedCount();
 
-//rule integrityOfMintToWithEmptyArray{
-//}
+  env e;
+  uint256 newMaxSupply;
 
+  setMaxSupply(e, newMaxSupply);
+
+  assert maxSupply() >= mintedCount();
+}
+
+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();
+}
 
 rule mintToReverts() {
   address[] addresses;
@@ -116,90 +136,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();
-/// }