82 lines
5.8 KiB
Ruby
82 lines
5.8 KiB
Ruby
import "helpers.spec"
|
|
import "methods/IGovernor.spec"
|
|
import "Governor.helpers.spec"
|
|
|
|
/*
|
|
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
|
│ Invariant: clock is consistent between the goernor and the token │
|
|
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
|
*/
|
|
rule clockMode(env e) {
|
|
assert clock(e) == e.block.number || clock(e) == e.block.timestamp;
|
|
assert clock(e) == token_clock(e);
|
|
}
|
|
|
|
/*
|
|
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
|
│ Invariant: Proposal is UNSET iff the proposer, the snapshot and the deadline are unset. │
|
|
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
|
*/
|
|
invariant createdConsistency(env e, uint256 pId)
|
|
safeState(e, pId) == UNSET() <=> proposalProposer(pId) == 0 &&
|
|
safeState(e, pId) == UNSET() <=> proposalSnapshot(pId) == 0 &&
|
|
safeState(e, pId) == UNSET() <=> proposalDeadline(pId) == 0 &&
|
|
safeState(e, pId) == UNSET() => !isExecuted(pId) &&
|
|
safeState(e, pId) == UNSET() => !isCanceled(pId)
|
|
{
|
|
preserved {
|
|
require clock(e) > 0;
|
|
}
|
|
}
|
|
|
|
invariant createdConsistencyWeak(uint256 pId)
|
|
proposalProposer(pId) == 0 <=> proposalSnapshot(pId) == 0 &&
|
|
proposalProposer(pId) == 0 <=> proposalDeadline(pId) == 0
|
|
{
|
|
preserved with (env e) {
|
|
require clock(e) > 0;
|
|
}
|
|
}
|
|
|
|
/*
|
|
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
|
│ Invariant: Votes start before it ends │
|
|
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
|
*/
|
|
invariant voteStartBeforeVoteEnd(uint256 pId)
|
|
proposalSnapshot(pId) <= proposalDeadline(pId)
|
|
{
|
|
preserved {
|
|
requireInvariant createdConsistencyWeak(pId);
|
|
}
|
|
}
|
|
|
|
/*
|
|
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
|
│ Invariant: A proposal cannot be both executed and canceled simultaneously │
|
|
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
|
*/
|
|
invariant noBothExecutedAndCanceled(uint256 pId)
|
|
!isExecuted(pId) || !isCanceled(pId)
|
|
|
|
/*
|
|
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
|
│ Rule: Once a proposal is created, voteStart, voteEnd and proposer are immutable │
|
|
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
|
*/
|
|
rule immutableFieldsAfterProposalCreation(uint256 pId, env e, method f, calldataarg arg)
|
|
filtered { f -> !skip(f) }
|
|
{
|
|
require state(e, pId) != UNSET();
|
|
|
|
uint256 voteStart = proposalSnapshot(pId);
|
|
uint256 voteEnd = proposalDeadline(pId);
|
|
address proposer = proposalProposer(pId);
|
|
|
|
f(e, arg);
|
|
|
|
assert voteStart == proposalSnapshot(pId), "Start date was changed";
|
|
assert voteEnd == proposalDeadline(pId), "End date was changed";
|
|
assert proposer == proposalProposer(pId), "Proposer was changed";
|
|
}
|