fix for oneUserVotesInCast

certora/specs/GovernorCountingSimple.spec

@@ -146,11 +146,21 @@ rule someOtherRuleToRemoveLater(uint256 num){
 /*
  * Checks that only one user is updated in the system when calling cast vote functions (assuming hasVoted is changing correctly, false->true, with every vote cast)
  */
-rule oneUserVotesInCast(uint256 pId, method f) filtered { f -> ((f.selector == castVote(uint256, uint8).selector) || 
-                                                                f.selector == castVoteBySig(uint256, uint8, uint8, bytes32, bytes32).selector) }{
-    env e; calldataarg args;
-    uint256 ghost_Before = hasVoteGhost(pId);
-    f(e, args);
+rule oneUserVotesInCast(uint256 pId, uint8 sup, method f) filtered {f -> f.selector == castVote(uint256, uint8).selector || f.selector == castVoteBySig(uint256, uint8, uint8, bytes32, bytes32).selector} {
+    env e; calldataarg args;                                                            //              ^                           ^
+    uint256 ghost_Before = hasVoteGhost(pId);                                           //           propose                castVoteWithReason
+    if (f.selector == castVote(uint256, uint8).selector)
+	{
+		castVote(e, pId, sup);
+	} /*else if (f.selector == 0x7b3c71d3) {
+        require(_pId_Harness() == proposalId);
+		f(e,args);
+	}*/ else if (f.selector == castVoteBySig(uint256, uint8, uint8, bytes32, bytes32).selector) {
+        uint8 v; bytes32 r; bytes32 s;
+        castVoteBySig(e, pId, sup, v, r, s);
+    } else{
+        f(e, args);
+    }
     uint256 ghost_After = hasVoteGhost(pId);
     assert(ghost_After == ghost_Before + 1, "Raised by more than 1");
 }
@@ -158,17 +168,16 @@ rule oneUserVotesInCast(uint256 pId, method f) filtered { f -> ((f.selector == c
 /*
  * Checks that in any call to cast vote functions only the sender's value is updated
  */
- /*
+
 rule noVoteForSomeoneElse(uint256 pId, uint8 support){
     env e;
     address voter = e.msg.sender;
-    bool hasVotedBefore = hasVoted(pId, voter);
+    bool hasVotedBefore = hasVoted(e, pId, voter);
     require(!hasVotedBefore);
     castVote(e, pId, support);
-    bool hasVotedAfter = hasVoted(pId, voter);
-    assert(hasVotedBefore != hasVotedAfter => forall address user. user != voter);
+    bool hasVotedAfter = hasVoted(e, pId, voter);
+    assert(hasVotedBefore != hasVotedAfter => (forall address user. user != voter => !hasVoted(e, pId, user)));
 }
-*/
 
 // ok
 rule votingWeightMonotonicity(method f){