import "helpers.spec" import "methods/IGovernor.spec" import "Governor.helpers.spec" import "GovernorInvariants.spec" methods { lateQuorumVoteExtension() returns uint64 envfree getExtendedDeadline(uint256) returns uint64 envfree } use invariant proposalStateConsistency use invariant votesImplySnapshotPassed /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ Rule: │ │ * Deadline can never be reduced │ │ * If deadline increases then we are in `deadlineExtended` state and `castVote` was called. │ │ * A proposal's deadline can't change in `deadlineExtended` state. │ │ * A proposal's deadline can't be unextended. │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ rule deadlineChangeToPreventLateQuorum(uint256 pId, env e, method f, calldataarg args) filtered { f -> !skip(f) } { require clockSanity(e); requireInvariant proposalStateConsistency(pId); requireInvariant votesImplySnapshotPassed(e, pId); // This is not (easily) provable as an invariant because the prover think `_totalSupplyCheckpoints` // can arbitrarily change, which causes the quorum() to change. Not sure how to fix that. require quorumReached(pId) <=> getExtendedDeadline(pId) > 0; uint256 deadlineBefore = proposalDeadline(pId); bool deadlineExtendedBefore = getExtendedDeadline(pId) > 0; bool quorumReachedBefore = quorumReached(pId); f(e, args); uint256 deadlineAfter = proposalDeadline(pId); bool deadlineExtendedAfter = getExtendedDeadline(pId) > 0; bool quorumReachedAfter = quorumReached(pId); // deadline can never be reduced assert deadlineBefore <= proposalDeadline(pId); // deadline can only be extended in proposal or on cast vote assert deadlineAfter != deadlineBefore => ( ( !deadlineExtendedBefore && !deadlineExtendedAfter && f.selector == propose(address[], uint256[], bytes[], string).selector ) || ( !deadlineExtendedBefore && deadlineExtendedAfter && !quorumReachedBefore && quorumReachedAfter && deadlineAfter == clock(e) + lateQuorumVoteExtension() && votingAll(f) ) ); // a deadline can only be extended once assert deadlineExtendedBefore => deadlineBefore == deadlineAfter; // a deadline cannot be un-extended assert deadlineExtendedBefore => deadlineExtendedAfter; }