From 847cbb91072f535023d551b751aadc376d10e9fe Mon Sep 17 00:00:00 2001
From: r4bbit <445106+0x-r4bbit@users.noreply.github.com>
Date: Wed, 10 Jan 2024 15:36:48 +0100
Subject: [PATCH] chore: introduce certora specs for CommunityTokenDeployer

This adds some basic specs for the `CommunityTokenDeployer` and its
interaction with `CommunityOwnerTokenRegistry`.
---
 certora/CommunityTokenDeployer.conf       | 20 ++++++
 certora/certora.conf                      |  1 +
 certora/specs/CommunityTokenDeployer.spec | 76 +++++++++++++++++++++++
 package.json                              |  2 +-
 4 files changed, 98 insertions(+), 1 deletion(-)
 create mode 100644 certora/CommunityTokenDeployer.conf
 create mode 100644 certora/specs/CommunityTokenDeployer.spec

diff --git a/certora/CommunityTokenDeployer.conf b/certora/CommunityTokenDeployer.conf
new file mode 100644
index 0000000..95ef5a4
--- /dev/null
+++ b/certora/CommunityTokenDeployer.conf
@@ -0,0 +1,20 @@
+{
+  "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
index 22a3ae4..a28bac7 100644
--- a/certora/certora.conf
+++ b/certora/certora.conf
@@ -4,6 +4,7 @@
   "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/specs/CommunityTokenDeployer.spec b/certora/specs/CommunityTokenDeployer.spec
new file mode 100644
index 0000000..8cdf0cd
--- /dev/null
+++ b/certora/specs/CommunityTokenDeployer.spec
@@ -0,0 +1,76 @@
+using CommunityOwnerTokenRegistry as CommunityOwnerTokenRegistry;
+
+methods {
+  function owner() external returns (address) envfree;
+  function deploymentRegistry() external returns (address) envfree;
+  function ownerTokenFactory() external returns (address) envfree;
+  function masterTokenFactory() external returns (address) envfree;
+  function deploy(CommunityTokenDeployer.TokenConfig, CommunityTokenDeployer.TokenConfig, CommunityTokenDeployer.DeploymentSignature, bytes) external returns (address, address);
+
+  function CommunityOwnerTokenRegistry.getEntry(address) external returns (address) envfree;
+  function CommunityOwnerTokenRegistry.tokenDeployer() external returns (address) envfree;
+
+
+  function _.balanceOf(address _owner) external => DISPATCHER(true);
+}
+
+rule integrityOfDeploy {
+
+  env e;
+  CommunityTokenDeployer.TokenConfig ownerToken;
+  CommunityTokenDeployer.TokenConfig masterToken;
+  CommunityTokenDeployer.DeploymentSignature signature;
+  bytes signerPublicKey;
+
+  deploy(e, ownerToken, masterToken, signature, signerPublicKey);
+
+  address tokenAddress = CommunityOwnerTokenRegistry.getEntry(signature.signer);
+  assert tokenAddress != 0;
+}
+
+rule registryMutability(method f) {
+  env e;
+  CommunityTokenDeployer.DeploymentSignature signature;
+  calldataarg args;
+
+  address tokenAddressBefore = CommunityOwnerTokenRegistry.getEntry(signature.signer);
+  require tokenAddressBefore != 0;
+
+  f(e, args);
+
+  address tokenAddressAfter = CommunityOwnerTokenRegistry.getEntry(signature.signer);
+  assert tokenAddressBefore == tokenAddressAfter;
+}
+
+rule registryChange(method f) {
+  env e;
+  calldataarg args;
+
+  address registryBefore = deploymentRegistry();
+  f(e, args);
+  address registryAfter = deploymentRegistry();
+
+  assert registryBefore != registryAfter => e.msg.sender == owner();
+}
+
+rule ownerTokenFactoryChange(method f) {
+  env e;
+  calldataarg args;
+
+  address factoryBefore = ownerTokenFactory();
+  f(e, args);
+  address factoryAfter = ownerTokenFactory();
+
+  assert factoryBefore != factoryAfter => e.msg.sender == owner();
+}
+
+rule masterTokenFactoryChange(method f) {
+  env e;
+  calldataarg args;
+
+  address factoryBefore = masterTokenFactory();
+  f(e, args);
+  address factoryAfter = masterTokenFactory();
+
+  assert factoryBefore != factoryAfter => e.msg.sender == owner();
+}
diff --git a/package.json b/package.json
index 0154cb9..01c3eb2 100644
--- a/package.json
+++ b/package.json
@@ -23,7 +23,7 @@
   "scripts": {
     "clean": "rm -rf cache out",
     "lint": "pnpm lint:sol && pnpm prettier:check",
-    "verify": "certoraRun certora/certora.conf",
+    "verify": "certoraRun certora/CommunityTokenDeployer.conf",
     "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"