runAllwithoutTypeCheckAndPolishingIt

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 <arguments>
+sh certora/scripts/WizardFirstPriority.sh <meaningful comment>
 ```
 
 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 `<specName>` 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 `<specName>` in the script (flag `--verify`):
 
 ```
 --verify WizardFirstPriority:certora/specs/<specName>.spec \
+```
 
 for example:
 
+```
 --verify WizardFirstPriority:certora/specs/GovernorCountingSimple.spec \
 ```
 

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"

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

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);
-        }}*/
+        }}
 
 
 /*

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);