FixedERC20VotesIssue

certora/harnesses/ERC20VotesHarness.sol

@@ -1,5 +1,5 @@
 import "../../contracts/token/ERC20/extensions/ERC20Votes.sol";
 
 contract ERC20VotesHarness is ERC20Votes {
-    constructor(string memory name) ERC20Permit(name) {}
+    constructor(string memory name, string memory symbol) ERC20Permit(name) ERC20(name, symbol) {}
 }

certora/harnesses/GovernorBasicHarness.sol

@@ -71,9 +71,10 @@ contract GovernorBasicHarness is Governor, GovernorCountingSimple, GovernorVotes
     // Harness of castVoteWithReason to be able to impose requirement on the proposal ID.
     uint256 public _pId_Harness;
     function castVoteWithReason(uint256 proposalId, uint8 support, string calldata reason) 
-    public 
-    override(IGovernor, Governor) 
-    returns (uint256) {
+        public 
+        override(IGovernor, Governor) 
+        returns (uint256) 
+    {
         require(proposalId == _pId_Harness);
         return super.castVoteWithReason(proposalId, support, reason);
     }

certora/harnesses/WizardHarness1.sol

@@ -64,7 +64,17 @@ contract WizardHarness1 is Governor, GovernorProposalThreshold, GovernorCounting
         return _proposals[proposalId].voteStart._deadline;
     }
 
-    
+
+    // Harness of castVoteWithReason to be able to impose requirement on the proposal ID.
+    uint256 public _pId_Harness;
+    function castVoteWithReason(uint256 proposalId, uint8 support, string calldata reason) 
+        public 
+        override(IGovernor, Governor) 
+        returns (uint256) 
+    {
+        require(proposalId == _pId_Harness);
+        return super.castVoteWithReason(proposalId, support, reason);
+    }
 
     // original code
 

certora/scripts/Governor.sh

@@ -1,7 +1,7 @@
-certoraRun certora/harnesses/GovernorHarness.sol \
+certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorHarness.sol \
     --verify GovernorHarness:certora/specs/GovernorBase.spec \
     --solc solc8.0 \
-    --staging \
+    --staging shelly/forSasha \
     --optimistic_loop \
     --settings -copyLoopUnroll=4 \
     --rule voteStartBeforeVoteEnd \

certora/scripts/GovernorBasic.sh

@@ -1,4 +1,4 @@
-certoraRun certora/harnesses/GovernorBasicHarness.sol \
+certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorBasicHarness.sol \
     --verify GovernorBasicHarness:certora/specs/GovernorBase.spec \
     --solc solc8.2 \
     --staging shelly/forSasha \

certora/scripts/GovernorCountingSimple-counting.sh

@@ -1,4 +1,4 @@
-certoraRun certora/harnesses/GovernorBasicHarness.sol \
+certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorBasicHarness.sol \
     --verify GovernorBasicHarness:certora/specs/GovernorCountingSimple.spec \
     --solc solc8.2 \
     --staging shelly/forSasha \

certora/scripts/WizardHarness1.sh

@@ -1,8 +1,8 @@
-certoraRun certora/harnesses/WizardHarness1.sol \
-    --verify WizardHarness1:certora/specs/GovernorBase.spec \
+certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/WizardHarness1.sol \
+    --verify WizardHarness1:certora/specs/GovernorCountingSimple.spec \
     --solc solc8.2 \
     --staging shelly/forSasha \
     --optimistic_loop \
     --settings -copyLoopUnroll=4 \
-    --rule allFunctionsRevertIfCanceled \
+    --rule SumOfVotesCastEqualSumOfPowerOfVoted \
     --msg "$1"

certora/specs/GovernorBase.spec

@@ -22,6 +22,14 @@ methods {
     // function summarization
     hashProposal(address[], uint256[], bytes[], bytes32) => CONSTANT
     proposalThreshold() returns uint256 envfree
+
+    getVotes(address, uint256) returns uint256 envfree => DISPATCHER(true)
+    //getVotes(address, uint256) => DISPATCHER(true)
+
+    getPastTotalSupply(uint256) returns uint256 envfree => DISPATCHER(true)
+    //getPastTotalSupply(uint256) => DISPATCHER(true)
+
+    getPastVotes(address, uint256) returns uint256 envfree => DISPATCHER(true)
 }
 
 //////////////////////////////////////////////////////////////////////////////
@@ -91,7 +99,6 @@ invariant proposalInitiated(uint256 pId)
         }}*/
         
 
-
 /*
  * A proposal cannot end unless it started.
  */

certora/specs/GovernorCountingSimple.spec

@@ -12,14 +12,6 @@ methods {
     quorumNumerator() returns uint256
     updateQuorumNumerator(uint256)
     _executor() returns address
-
-    getVotes(address, uint256) returns uint256 envfree => DISPATCHER(true)
-    //getVotes(address, uint256) => DISPATCHER(true)
-
-    getPastTotalSupply(uint256) returns uint256 envfree => DISPATCHER(true)
-    //getPastTotalSupply(uint256) => DISPATCHER(true)
-
-    getPastVotes(address, uint256) returns uint256 envfree => DISPATCHER(true)
 }
 
 //////////////////////////////////////////////////////////////////////////////
@@ -39,9 +31,9 @@ ghost sum_all_votes_power() returns uint256 {
 	init_state axiom sum_all_votes_power() == 0;
 }
 
-//hook Sstore ghost_sum_vote_power_by_id [KEY uint256 pId] uint256 current_power(uint256 old_power) STORAGE {
-//	havoc sum_all_votes_power assuming sum_all_votes_power@new() == sum_all_votes_power@old() - old_power + current_power;
-//}
+hook Sstore ghost_sum_vote_power_by_id [KEY uint256 pId] uint256 current_power(uint256 old_power) STORAGE {
+	havoc sum_all_votes_power assuming sum_all_votes_power@new() == sum_all_votes_power@old() - old_power + current_power;
+}
 
 ghost tracked_weight(uint256) returns uint256 {
 	init_state axiom forall uint256 p. tracked_weight(p) == 0;