chore: introduce certora specs for CommunityTokenDeployer
This adds some basic specs for the `CommunityTokenDeployer` and its interaction with `CommunityOwnerTokenRegistry`.
This commit is contained in:
parent
aa3f26ee80
commit
847cbb9107
|
@ -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
|
||||||
|
}
|
||||||
|
|
|
@ -4,6 +4,7 @@
|
||||||
"rule_sanity": "basic",
|
"rule_sanity": "basic",
|
||||||
"verify": "CollectibleV1:certora/specs/CollectibleV1.spec",
|
"verify": "CollectibleV1:certora/specs/CollectibleV1.spec",
|
||||||
"wait_for_results": "all",
|
"wait_for_results": "all",
|
||||||
|
"optimistic_loop": true,
|
||||||
"packages": ["@openzeppelin=lib/openzeppelin-contracts"]
|
"packages": ["@openzeppelin=lib/openzeppelin-contracts"]
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
@ -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();
|
||||||
|
}
|
|
@ -23,7 +23,7 @@
|
||||||
"scripts": {
|
"scripts": {
|
||||||
"clean": "rm -rf cache out",
|
"clean": "rm -rf cache out",
|
||||||
"lint": "pnpm lint:sol && pnpm prettier:check",
|
"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",
|
"lint:sol": "forge fmt --check && pnpm solhint {script,src,test}/**/*.sol",
|
||||||
"prettier:check": "prettier --check **/*.{json,md,yml} --ignore-path=.prettierignore",
|
"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"
|
||||||
|
|
Loading…
Reference in New Issue