GovernorPreventLateQuorum.spec 11 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298
  1. import "GovernorCountingSimple.spec"
  2. using ERC721VotesHarness as erc721votes
  3. methods {
  4. quorumDenominator() returns uint256 envfree
  5. votingPeriod() returns uint256 envfree
  6. lateQuorumVoteExtension() returns uint64 envfree
  7. propose(address[], uint256[], bytes[], string)
  8. // harness
  9. getExtendedDeadlineIsUnset(uint256) returns bool envfree
  10. getExtendedDeadlineIsStarted(uint256) returns bool envfree
  11. getExtendedDeadline(uint256) returns uint64 envfree
  12. getAgainstVotes(uint256) returns uint256 envfree
  13. getAbstainVotes(uint256) returns uint256 envfree
  14. getForVotes(uint256) returns uint256 envfree
  15. // more robust check than f.selector == _castVote(...).selector
  16. latestCastVoteCall() returns uint256 envfree
  17. // timelock dispatch
  18. getMinDelay() returns uint256 => DISPATCHER(true)
  19. hashOperationBatch(address[], uint256[], bytes[], bytes32, bytes32) => DISPATCHER(true)
  20. executeBatch(address[], uint256[], bytes[], bytes32, bytes32) => CONSTANT
  21. scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256) => CONSTANT
  22. }
  23. //////////////////////////////////////////////////////////////////////////////
  24. ///////////////////////////// Helper Functions ///////////////////////////////
  25. //////////////////////////////////////////////////////////////////////////////
  26. function helperFunctionsWithRevertOnlyCastVote(uint256 proposalId, method f, env e) {
  27. string reason; uint8 support; uint8 v; bytes32 r; bytes32 s; bytes params;
  28. if (f.selector == castVote(uint256, uint8).selector) {
  29. castVote@withrevert(e, proposalId, support);
  30. } else if (f.selector == castVoteWithReason(uint256, uint8, string).selector) {
  31. castVoteWithReason@withrevert(e, proposalId, support, reason);
  32. } else if (f.selector == castVoteBySig(uint256, uint8,uint8, bytes32, bytes32).selector) {
  33. castVoteBySig@withrevert(e, proposalId, support, v, r, s);
  34. } else if (f.selector == castVoteWithReasonAndParamsBySig(uint256,uint8,string,bytes,uint8,bytes32,bytes32).selector) {
  35. castVoteWithReasonAndParamsBySig@withrevert(e, proposalId, support, reason, params, v, r, s);
  36. } else if (f.selector == castVoteWithReasonAndParams(uint256,uint8,string,bytes).selector) {
  37. castVoteWithReasonAndParams@withrevert(e, proposalId, support, reason, params);
  38. } else {
  39. calldataarg args;
  40. f@withrevert(e, args);
  41. }
  42. }
  43. //////////////////////////////////////////////////////////////////////////////
  44. //////////////////////////////// Definitions /////////////////////////////////
  45. //////////////////////////////////////////////////////////////////////////////
  46. // proposal deadline can be extended (but isn't)
  47. definition deadlineExtendable(env e, uint256 pId) returns bool =
  48. getExtendedDeadlineIsUnset(pId) // deadline == 0
  49. && !quorumReached(e, pId);
  50. // proposal deadline has been extended
  51. definition deadlineExtended(env e, uint256 pId) returns bool =
  52. getExtendedDeadlineIsStarted(pId) // deadline > 0
  53. && quorumReached(e, pId);
  54. definition proposalNotCreated(env e, uint256 pId) returns bool =
  55. proposalSnapshot(pId) == 0
  56. && proposalDeadline(pId) == 0
  57. && getExtendedDeadlineIsUnset(pId)
  58. && getAgainstVotes(pId) == 0
  59. && getAbstainVotes(pId) == 0
  60. && getForVotes(pId) == 0
  61. && !quorumReached(e, pId);
  62. //////////////////////////////////////////////////////////////////////////////
  63. ///////////////////////////////// Invariants /////////////////////////////////
  64. //////////////////////////////////////////////////////////////////////////////
  65. /*
  66. * I1: If a proposal has reached quorum then the proposal snapshot (start block.number) must be non-zero
  67. * INVARIANT NOT PASSING // fails for updateQuorumNumerator and in the initial state when voting token total supply is 0 (causes quoromReached to return true)
  68. * ADVANCED SANITY NOT RAN
  69. */
  70. invariant quorumReachedEffect(env e, uint256 pId)
  71. quorumReached(e, pId) => proposalCreated(pId) // bug: 0 supply 0 votes => quorumReached
  72. // filtered { f -> f.selector != updateQuorumNumerator(uint256).selector } // * fails for this function
  73. /*
  74. * I2: A non-existant proposal must meet the definition of one.
  75. * INVARIANT NOT PASSING // fails for updateQuorumNumerator and in the initial state when voting token total supply is 0 (causes quoromReached to return true)
  76. * ADVANCED SANITY NOT RAN
  77. */
  78. invariant proposalNotCreatedEffects(env e, uint256 pId)
  79. !proposalCreated(pId) => proposalNotCreated(e, pId)
  80. // filtered { f -> f.selector != updateQuorumNumerator(uint256).selector } // * fails for this function
  81. /*
  82. * I3: A created propsal must be in state deadlineExtendable or deadlineExtended.
  83. * INVARIANT NOT PASSING // fails for updateQuorumNumerator and in the initial state when voting token total supply is 0 (causes quoromReached to return true)
  84. * ADVANCED SANITY NOT RAN
  85. */
  86. invariant proposalInOneState(env e, uint256 pId)
  87. proposalNotCreated(e, pId) || deadlineExtendable(e, pId) || deadlineExtended(e, pId)
  88. // filtered { f -> f.selector != updateQuorumNumerator(uint256).selector } // * fails for this function
  89. { preserved { requireInvariant proposalNotCreatedEffects(e, pId); }}
  90. //////////////////////////////////////////////////////////////////////////////
  91. ////////////////////////////////// Rules /////////////////////////////////////
  92. //////////////////////////////////////////////////////////////////////////////
  93. ///////////////////////////// first set of rules /////////////////////////////
  94. // R1 and R2 are assumed in R3, so we prove them first
  95. /*
  96. * R1: If deadline increases then we are in deadlineExtended state and castVote was called.
  97. * RULE PASSING
  98. * ADVANCED SANITY PASSING
  99. */
  100. rule deadlineChangeEffects(method f) filtered {f -> !f.isView} {
  101. env e; calldataarg args; uint256 pId;
  102. requireInvariant quorumReachedEffect(e, pId);
  103. uint256 deadlineBefore = proposalDeadline(pId);
  104. f(e, args);
  105. uint256 deadlineAfter = proposalDeadline(pId);
  106. assert(deadlineAfter > deadlineBefore => latestCastVoteCall() == e.block.number && deadlineExtended(e, pId));
  107. }
  108. /*
  109. * R2: A proposal can't leave deadlineExtended state.
  110. * RULE PASSING*
  111. * ADVANCED SANITY PASSING
  112. */
  113. rule deadlineCantBeUnextended(method f)
  114. filtered {
  115. f -> !f.isView
  116. // && f.selector != updateQuorumNumerator(uint256).selector // * fails for this function
  117. } {
  118. env e; calldataarg args; uint256 pId;
  119. require(deadlineExtended(e, pId));
  120. requireInvariant quorumReachedEffect(e, pId);
  121. f(e, args);
  122. assert(deadlineExtended(e, pId));
  123. }
  124. /*
  125. * R3: A proposal's deadline can't change in deadlineExtended state.
  126. * RULE PASSING
  127. * ADVANCED SANITY PASSING
  128. */
  129. rule canExtendDeadlineOnce(method f) filtered {f -> !f.isView} {
  130. env e; calldataarg args; uint256 pId;
  131. require(deadlineExtended(e, pId));
  132. requireInvariant quorumReachedEffect(e, pId);
  133. uint256 deadlineBefore = proposalDeadline(pId);
  134. f(e, args);
  135. uint256 deadlineAfter = proposalDeadline(pId);
  136. assert(deadlineBefore == deadlineAfter, "deadline can not be extended twice");
  137. }
  138. //////////////////////////// second set of rules ////////////////////////////
  139. // HIGH LEVEL RULE R6: deadline can only extended if quorum reached w/ <= timeOfExtension left to vote
  140. // I3, R4 and R5 are assumed in R6 so we prove them first
  141. /*
  142. * R4: A change in hasVoted must be correlated with an increasing of the vote supports, i.e. casting a vote increases the total number of votes.
  143. * RULE PASSING
  144. * ADVANCED SANITY PASSING
  145. */
  146. rule hasVotedCorrelationNonzero(uint256 pId, method f, env e) filtered {f -> !f.isView} {
  147. address acc = e.msg.sender;
  148. require(getVotes(e, acc, proposalSnapshot(pId)) > 0); // assuming voter has non-zero voting power
  149. uint256 againstBefore = votesAgainst();
  150. uint256 forBefore = votesFor();
  151. uint256 abstainBefore = votesAbstain();
  152. bool hasVotedBefore = hasVoted(e, pId, acc);
  153. helperFunctionsWithRevertOnlyCastVote(pId, f, e); // should be f(e, args)
  154. uint256 againstAfter = votesAgainst();
  155. uint256 forAfter = votesFor();
  156. uint256 abstainAfter = votesAbstain();
  157. bool hasVotedAfter = hasVoted(e, pId, acc);
  158. // want all vote categories to not decrease and at least one category to increase
  159. assert
  160. (!hasVotedBefore && hasVotedAfter) =>
  161. (againstBefore <= againstAfter && forBefore <= forAfter && abstainBefore <= abstainAfter),
  162. "after a vote is cast, the number of votes for each category must not decrease"; // currently vacous but keeping for CI tests
  163. assert
  164. (!hasVotedBefore && hasVotedAfter) =>
  165. (againstBefore < againstAfter || forBefore < forAfter || abstainBefore < abstainAfter),
  166. "after a vote is cast, the number of votes of at least one category must increase";
  167. }
  168. /*
  169. * R5: An against vote does not make a proposal reach quorum.
  170. * RULE PASSING
  171. * --ADVANCED SANITY PASSING vacuous but keeping
  172. */
  173. rule againstVotesDontCount(method f) filtered {f -> !f.isView} {
  174. env e; calldataarg args; uint256 pId;
  175. address acc = e.msg.sender;
  176. bool quorumBefore = quorumReached(e, pId);
  177. uint256 againstBefore = votesAgainst();
  178. f(e, args);
  179. bool quorumAfter = quorumReached(e, pId);
  180. uint256 againstAfter = votesAgainst();
  181. assert (againstBefore < againstAfter) => quorumBefore == quorumAfter, "quorum must not be reached with an against vote";
  182. }
  183. /*
  184. * R6: Deadline can only be extended from a `deadlineExtendible` state with quorum being reached with <= `lateQuorumVoteExtension` time left to vote
  185. * RULE PASSING
  186. * ADVANCED SANITY PASSING
  187. */
  188. rule deadlineExtenededIfQuorumReached(method f) filtered {f -> !f.isView} {
  189. env e; calldataarg args; uint256 pId;
  190. requireInvariant proposalInOneState(e, pId);
  191. requireInvariant quorumReachedEffect(e, pId);
  192. requireInvariant proposalNotCreatedEffects(e, pId);
  193. bool wasDeadlineExtendable = deadlineExtendable(e, pId);
  194. uint64 extension = lateQuorumVoteExtension();
  195. uint256 deadlineBefore = proposalDeadline(pId);
  196. f(e, args);
  197. uint256 deadlineAfter = proposalDeadline(pId);
  198. assert deadlineAfter > deadlineBefore => wasDeadlineExtendable, "deadline must have been extendable for the deadline to be extended";
  199. assert deadlineAfter > deadlineBefore => deadlineBefore - e.block.number <= extension, "deadline extension should not be used";
  200. }
  201. /*
  202. * R7: `extendedDeadlineField` is set iff `_castVote` is called and quroum is reached.
  203. * RULE PASSING
  204. * ADVANCED SANITY PASSING
  205. */
  206. rule extendedDeadlineValueSetIfQuorumReached(method f) filtered {f -> !f.isView} {
  207. env e; calldataarg args; uint256 pId;
  208. requireInvariant proposalInOneState(e, pId);
  209. bool extendedBefore = deadlineExtended(e, pId);
  210. f(e, args);
  211. bool extendedAfter = deadlineExtended(e, pId);
  212. uint256 extDeadline = getExtendedDeadline(pId);
  213. assert(
  214. !extendedBefore && extendedAfter
  215. => extDeadline == e.block.number + lateQuorumVoteExtension(),
  216. "extended deadline was not set"
  217. );
  218. }
  219. /*
  220. * R8: Deadline can never be reduced.
  221. * RULE PASSING
  222. * ADVANCED SANITY PASSING
  223. */
  224. rule deadlineNeverReduced(method f) filtered {f -> !f.isView} {
  225. env e; calldataarg args; uint256 pId;
  226. requireInvariant quorumReachedEffect(e, pId);
  227. requireInvariant proposalNotCreatedEffects(e, pId);
  228. uint256 deadlineBefore = proposalDeadline(pId);
  229. f(e, args);
  230. uint256 deadlineAfter = proposalDeadline(pId);
  231. assert(deadlineAfter >= deadlineBefore);
  232. }