fix simple vote end before start

pull/2997/head
Shelly Grossman 3 years ago
parent 0ebc0d5844
commit ac729e0ecf
  1. 4
      certora/specs/GovernorBase.spec

@ -21,8 +21,8 @@ methods {
*/ */
//invariant voteStartBeforeVoteEnd1(uint256 pId) proposalSnapshot(pId) < proposalDeadline(pId) //invariant voteStartBeforeVoteEnd1(uint256 pId) proposalSnapshot(pId) < proposalDeadline(pId)
invariant voteStartBeforeVoteEnd(uint256 pId) invariant voteStartBeforeVoteEnd(uint256 pId)
(proposalSnapshot(pId) == 0 <=> proposalDeadline(pId) == 0) && (proposalSnapshot(pId) > 0 => proposalSnapshot(pId) < proposalDeadline(pId))
proposalSnapshot(pId) < proposalDeadline(pId) && (proposalSnapshot(pId) == 0 => proposalDeadline(pId) == 0)
/** /**
* A proposal cannot be both executed and canceled. * A proposal cannot be both executed and canceled.

Loading…
Cancel
Save