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`.
This commit is contained in:
r4bbit 2024-01-11 11:30:14 +01:00
parent 847cbb9107
commit e3142f1e52
5 changed files with 28 additions and 33 deletions

View File

@ -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
}

View File

@ -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"]
}

View File

@ -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"

View File

@ -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"

View File

@ -23,10 +23,12 @@
"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/CommunityTokenDeployer.conf", "verify": "pnpm verify:collectible_v1 && pnpm verify:community_token_deployer",
"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",
"verify:collectible_v1": "./certora/scripts/verify-collectible-v1.sh",
"verify:community_token_deployer": "./certora/scripts/verify-community-token-deployer.sh"
} }
} }