From e3142f1e52ab404dd296abd891c943e0b4dc7eb1 Mon Sep 17 00:00:00 2001
From: r4bbit <445106+0x-r4bbit@users.noreply.github.com>
Date: Thu, 11 Jan 2024 11:30:14 +0100
Subject: [PATCH] refactor: move certora configs into individual scripts

This is done to allow execution of multiple verifications per command,
such that we can still use `pnpm verify` as usual to run all specs, but
also target individual specs using `pnpm verify:sub_command`.
---
 certora/CommunityTokenDeployer.conf           | 20 -------------------
 certora/certora.conf                          | 11 ----------
 certora/scripts/verify-collectible-v1.sh      |  9 +++++++++
 .../verify-community-token-deployer.sh        | 15 ++++++++++++++
 package.json                                  |  6 ++++--
 5 files changed, 28 insertions(+), 33 deletions(-)
 delete mode 100644 certora/CommunityTokenDeployer.conf
 delete mode 100644 certora/certora.conf
 create mode 100755 certora/scripts/verify-collectible-v1.sh
 create mode 100755 certora/scripts/verify-community-token-deployer.sh

diff --git a/certora/CommunityTokenDeployer.conf b/certora/CommunityTokenDeployer.conf
deleted file mode 100644
index 95ef5a4..0000000
--- a/certora/CommunityTokenDeployer.conf
+++ /dev/null
@@ -1,20 +0,0 @@
-{
-  "files": [
-    "contracts/CommunityTokenDeployer.sol",
-    "contracts/CommunityOwnerTokenRegistry.sol",
-    "contracts/factories/CommunityOwnerTokenFactory.sol",
-    "contracts/factories/CommunityMasterTokenFactory.sol"
-  ],
-  "link": [
-    "CommunityTokenDeployer:deploymentRegistry=CommunityOwnerTokenRegistry",
-    "CommunityTokenDeployer:ownerTokenFactory=CommunityOwnerTokenFactory",
-    "CommunityTokenDeployer:masterTokenFactory=CommunityMasterTokenFactory"
-  ],
-  "msg": "Verifying CommunityTokenDeployer.sol",
-  "rule_sanity": "basic",
-  "verify": "CommunityTokenDeployer:certora/specs/CommunityTokenDeployer.spec",
-  "wait_for_results": "all",
-  "packages": ["@openzeppelin=lib/openzeppelin-contracts"],
-  "optimistic_loop": true
-}
-
diff --git a/certora/certora.conf b/certora/certora.conf
deleted file mode 100644
index a28bac7..0000000
--- a/certora/certora.conf
+++ /dev/null
@@ -1,11 +0,0 @@
-{
-  "files": ["contracts/tokens/CollectibleV1.sol"],
-  "msg": "Verifying CollectibleV1.sol",
-  "rule_sanity": "basic",
-  "verify": "CollectibleV1:certora/specs/CollectibleV1.spec",
-  "wait_for_results": "all",
-  "optimistic_loop": true,
-  "packages": ["@openzeppelin=lib/openzeppelin-contracts"]
-}
-
-
diff --git a/certora/scripts/verify-collectible-v1.sh b/certora/scripts/verify-collectible-v1.sh
new file mode 100755
index 0000000..6266aa3
--- /dev/null
+++ b/certora/scripts/verify-collectible-v1.sh
@@ -0,0 +1,9 @@
+certoraRun \
+  contracts/tokens/CollectibleV1.sol \
+--verify CollectibleV1:certora/specs/CollectibleV1.spec \
+--packages @openzeppelin=lib/openzeppelin-contracts \
+--optimistic_loop \
+--rule_sanity "basic" \
+--wait_for_results "all" \
+--msg "Verifying CollectibleV1.sol"
+
diff --git a/certora/scripts/verify-community-token-deployer.sh b/certora/scripts/verify-community-token-deployer.sh
new file mode 100755
index 0000000..e318e45
--- /dev/null
+++ b/certora/scripts/verify-community-token-deployer.sh
@@ -0,0 +1,15 @@
+certoraRun \
+  contracts/CommunityTokenDeployer.sol \
+  contracts/CommunityOwnerTokenRegistry.sol \
+  contracts/factories/CommunityOwnerTokenFactory.sol \
+  contracts/factories/CommunityMasterTokenFactory.sol \
+--verify CommunityTokenDeployer:certora/specs/CommunityTokenDeployer.spec \
+--link CommunityTokenDeployer:deploymentRegistry=CommunityOwnerTokenRegistry \
+--link CommunityTokenDeployer:ownerTokenFactory=CommunityOwnerTokenFactory \
+--link CommunityTokenDeployer:masterTokenFactory=CommunityMasterTokenFactory \
+--packages @openzeppelin=lib/openzeppelin-contracts \
+--optimistic_loop \
+--rule_sanity "basic" \
+--wait_for_results "all" \
+--msg "Verifying CommunityTokenDeployer.sol"
+
diff --git a/package.json b/package.json
index 01c3eb2..155a32b 100644
--- a/package.json
+++ b/package.json
@@ -23,10 +23,12 @@
   "scripts": {
     "clean": "rm -rf cache out",
     "lint": "pnpm lint:sol && pnpm prettier:check",
-    "verify": "certoraRun certora/CommunityTokenDeployer.conf",
+    "verify": "pnpm verify:collectible_v1 && pnpm verify:community_token_deployer",
     "lint:sol": "forge fmt --check && pnpm solhint {script,src,test}/**/*.sol",
     "prettier:check": "prettier --check **/*.{json,md,yml} --ignore-path=.prettierignore",
-    "prettier:write": "prettier --write **/*.{json,md,yml} --ignore-path=.prettierignore"
+    "prettier:write": "prettier --write **/*.{json,md,yml} --ignore-path=.prettierignore",
+    "verify:collectible_v1": "./certora/scripts/verify-collectible-v1.sh",
+    "verify:community_token_deployer": "./certora/scripts/verify-community-token-deployer.sh"
   }
 }