From 1d25a222018a45181ebf93b782c7affc3c3055ad Mon Sep 17 00:00:00 2001 From: Aleksander Kryukov Date: Thu, 25 Nov 2021 13:33:36 +0200 Subject: [PATCH] runAllwithoutTypeCheckAndPolishingIt --- certora/README.md | 11 ++++----- certora/scripts/WizardFirstPriority.sh | 2 +- certora/scripts/verifyAll.sh | 30 +++++++++++++++++++++++ certora/specs/GovernorBase.spec | 22 +++++++---------- certora/specs/GovernorCountingSimple.spec | 12 ++++++--- 5 files changed, 53 insertions(+), 24 deletions(-) create mode 100644 certora/scripts/verifyAll.sh diff --git a/certora/README.md b/certora/README.md index b6cdc810e..1ad6507f2 100644 --- a/certora/README.md +++ b/certora/README.md @@ -7,29 +7,28 @@ Documentation for CVT and the specification language are available ## Running the verification -Due to current time and space limitations in the tool, many of the rules need to -be verified separately, so there are many steps required to reverify everything. - The scripts in the `certora/scripts` directory are used to submit verification jobs to the Certora verification service. These scripts should be run from the root directory; for example by running ``` -sh certora/scripts/WizardFirstPriority.sh +sh certora/scripts/WizardFirstPriority.sh ``` After the job is complete, the results will be available on [the Certora portal](https://vaas-stg.certora.com/). -The `AvengersAssemble` script runs all spec files agains all contracts in the `certora/harness` that start with `Wizard` meaning that a contract generated in [wizard](`certora/scripts`). If you want to verify new wizard's instance you also need to harness this contract. We don't recommend to do it because a list of harnesses may go beyond wizard's contract. The main goal of this script is to run all specs written by the team against all contracts properly harnessed. +The `verifyAll` script runs all spec files agains all contracts in the `certora/harness` that start with `Wizard` meaning that a contract generated in [wizard](https://wizard.openzeppelin.com/#governor). If you want to verify new wizard's instance you also need to harness this contract. We don't recommend to do it because a list of harnesses may go beyond wizard's contract. Moreover, the set of setting to run the Certora verification service may vary. The main goal of this script is to run all specs written by the team against all contracts properly harnessed. -The `WizardFirstPriority` and `WizardFirstTry` scripts run one of the scripts for the corresponding contract. In order to run another spec you should change spec file name `` in the third line of a script: +The `WizardFirstPriority` and `WizardFirstTry` scripts run one of the scripts for the corresponding contract. In order to run another spec you should change spec file name `` in the script (flag `--verify`): ``` --verify WizardFirstPriority:certora/specs/.spec \ +``` for example: +``` --verify WizardFirstPriority:certora/specs/GovernorCountingSimple.spec \ ``` diff --git a/certora/scripts/WizardFirstPriority.sh b/certora/scripts/WizardFirstPriority.sh index 980f617ea..1a491bbda 100644 --- a/certora/scripts/WizardFirstPriority.sh +++ b/certora/scripts/WizardFirstPriority.sh @@ -5,5 +5,5 @@ certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/WizardFirst --staging shelly/forSasha \ --optimistic_loop \ --settings -copyLoopUnroll=4 \ - --rule hasVotedCorrelation \ + --rule noVoteForSomeoneElse \ --msg "$1" \ No newline at end of file diff --git a/certora/scripts/verifyAll.sh b/certora/scripts/verifyAll.sh new file mode 100644 index 000000000..d2ce48350 --- /dev/null +++ b/certora/scripts/verifyAll.sh @@ -0,0 +1,30 @@ +for contract in certora/harnesses/Wizard*.sol; +do + for spec in certora/specs/*.spec; + do + contractFile=$(basename $contract) + specFile=$(basename $spec) + echo "Processing ${contractFile%.*} with $specFile" + if [ "${contractFile%.*}" = "WizardFirstPriority" ]; + then + certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/$contractFile \ + --link WizardFirstPriority:token=ERC20VotesHarness \ + --verify ${contractFile%.*}:certora/specs/$specFile "$@" \ + --solc solc8.2 \ + --staging shelly/forSasha \ + --disableLocalTypeChecking \ + --optimistic_loop \ + --settings -copyLoopUnroll=4 \ + --msg "checking $specFile on ${contractFile%.*}" + else + certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/$contractFile \ + --verify ${contractFile%.*}:certora/specs/$specFile "$@" \ + --solc solc8.2 \ + --staging shelly/forSasha \ + --disableLocalTypeChecking \ + --optimistic_loop \ + --settings -copyLoopUnroll=4 \ + --msg "checking $specFile on ${contractFile%.*}" + fi + done +done \ No newline at end of file diff --git a/certora/specs/GovernorBase.spec b/certora/specs/GovernorBase.spec index e56960347..ef2d68baf 100644 --- a/certora/specs/GovernorBase.spec +++ b/certora/specs/GovernorBase.spec @@ -61,7 +61,6 @@ function helperFunctionsWithRevert(uint256 proposalId, method f, env e) { } else if (f.selector == castVoteBySig(uint256, uint8,uint8, bytes32, bytes32).selector) { castVoteBySig@withrevert(e, proposalId, support, v, r, s); } else if (f.selector == queue(address[], uint256[], bytes[], bytes32).selector) { - require targets.length <= 1 && values.length <= 1 && calldatas.length <= 1; queue@withrevert(e, targets, values, calldatas, descriptionHash); } else { calldataarg args; @@ -96,8 +95,7 @@ function helperFunctionsWithRevert(uint256 proposalId, method f, env e) { * This is very safe assumption as usually the 0 block is genesis block which is uploaded with data * by the developers and will not be valid to raise proposals (at the current way that block chain is functioning) */ - // To use env with general preserved block first disable type checking then - // use Uri's branch - --staging uri/add_with_env_to_preserved_all + // To use env with general preserved block disable type checking [--disableLocalTypeChecking] invariant startAndEndDatesNonZero(uint256 pId) proposalSnapshot(pId) != 0 <=> proposalDeadline(pId) != 0 /*{ preserved with (env e){ @@ -108,25 +106,23 @@ invariant startAndEndDatesNonZero(uint256 pId) /* * If a proposal is canceled it must have a start and an end date */ - // To use env with general preserved block first disable type checking then - // use Uri's branch - --staging uri/add_with_env_to_preserved_all + // To use env with general preserved block disable type checking [--disableLocalTypeChecking] invariant canceledImplyStartAndEndDateNonZero(uint pId) isCanceled(pId) => proposalSnapshot(pId) != 0 - /*{preserved with (env e){ + {preserved with (env e){ require e.block.number > 0; - }}*/ + }} /* * If a proposal is executed it must have a start and an end date */ - // To use env with general preserved block first disable type checking then - // use Uri's branch - --staging uri/add_with_env_to_preserved_all + // To use env with general preserved block disable type checking [--disableLocalTypeChecking] invariant executedImplyStartAndEndDateNonZero(uint pId) isExecuted(pId) => proposalSnapshot(pId) != 0 - /*{ preserved with (env e){ + { preserved with (env e){ require e.block.number > 0; - }}*/ + }} /* @@ -138,9 +134,9 @@ invariant voteStartBeforeVoteEnd(uint256 pId) // After integration of GovernorSettings.sol the invariant expression should be changed from <= to < (proposalSnapshot(pId) > 0 => proposalSnapshot(pId) <= proposalDeadline(pId)) // (proposalSnapshot(pId) > 0 => proposalSnapshot(pId) <= proposalDeadline(pId)) - /*{ preserved { + { preserved { requireInvariant startAndEndDatesNonZero(pId); - }}*/ + }} /* diff --git a/certora/specs/GovernorCountingSimple.spec b/certora/specs/GovernorCountingSimple.spec index 8f12516f4..47f67aa90 100644 --- a/certora/specs/GovernorCountingSimple.spec +++ b/certora/specs/GovernorCountingSimple.spec @@ -158,9 +158,13 @@ rule possibleTotalVotes(uint256 pId, uint8 sup, env e, method f) { /* * Only sender's voting status can be changed by execution of any cast vote function */ -rule noVoteForSomeoneElse(uint256 pId, uint8 sup, method f) filtered {f -> f.selector == castVote(uint256, uint8).selector - || f.selector == castVoteWithReason(uint256, uint8, string).selector - || f.selector == castVoteBySig(uint256, uint8, uint8, bytes32, bytes32).selector } { +// Checked for castVote only. all 3 castVote functions call _castVote, so the completness of the verification is counted on + // the fact that the 3 functions themselves makes no chages, but rather call an internal function to execute. + // That means that we do not check those 3 functions directly, however for castVote & castVoteWithReason it is quite trivial + // to understand why this is ok. For castVoteBySig we basically assume that the signature referendum is correct without checking it. + // We could check each function seperately and pass the rule, but that would have uglyfied the code with no concrete + // benefit, as it is evident that nothing is happening in the first 2 functions (calling a view function), and we do not desire to check the signature verification. +rule noVoteForSomeoneElse(uint256 pId, uint8 sup, method f) { env e; calldataarg args; address voter = e.msg.sender; @@ -168,7 +172,7 @@ rule noVoteForSomeoneElse(uint256 pId, uint8 sup, method f) filtered {f -> f.sel bool hasVotedBefore_User = hasVoted(e, pId, user); - helperFunctionsWithRevert(pId, f, e); + castVote@withrevert(e, pId, sup); require(!lastReverted); bool hasVotedAfter_User = hasVoted(e, pId, user);