NoBey/openzeppelin-contracts
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

update governor specs

Browse Source
This commit is contained in:
Hadrien Croubois
2023-03-13 17:26:38 +01:00
parent 4b11b4d3a6
commit c33e7bd340
10 changed files with 144 additions and 46 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
certora/diff/governance_Governor.sol.patch
View File

@ -1,5 +1,5 @@
--- governance/Governor.sol 2023-03-07 10:48:47.730155491 +0100
+++ governance/Governor.sol 2023-03-13 14:07:30.704202049 +0100
+++ governance/Governor.sol 2023-03-13 15:30:49.107167674 +0100
@@ -216,6 +216,21 @@
return _proposals[proposalId].proposer;
}

14
certora/diff/governance_extensions_GovernorTimelockControl.sol.patch Normal file
View File

@ -0,0 +1,14 @@
--- governance/extensions/GovernorTimelockControl.sol 2023-03-07 10:48:47.733488857 +0100
+++ governance/extensions/GovernorTimelockControl.sol 2023-03-13 16:18:10.255122179 +0100
@@ -84,6 +84,11 @@
return eta == 1 ? 0 : eta; // _DONE_TIMESTAMP (1) should be replaced with a 0 value
}
+ // FV
+ function _proposalQueueId(uint256 proposalId) internal view returns (bytes32) {
+ return _timelockIds[proposalId];
+ }
+
/**
* @dev Function to queue a proposal to the timelock.
*/

4
certora/harnesses/GovernorHarness.sol
View File

@ -64,6 +64,10 @@ contract GovernorHarness is
return _isCanceled(proposalId);
}
function isQueued(uint256 proposalId) public view returns (bool) {
return _proposalQueueId(proposalId) != bytes32(0);
}
function governanceCallLength() public view returns (uint256) {
return _governanceCallLength();
}

38
certora/specs.js
View File

@ -44,22 +44,36 @@ module.exports = [
},
// Governor
...product(
['GovernorInvariants', 'GovernorBaseRules', 'GovernorStates'],
['GovernorInvariants', 'GovernorBaseRules', 'GovernorChanges', 'GovernorStates'],
['ERC20VotesBlocknumberHarness', 'ERC20VotesTimestampHarness'],
).map(([spec, token]) => ({
spec,
contract: 'GovernorHarness',
files: ['certora/harnesses/GovernorHarness.sol', `certora/harnesses/${token}.sol`],
options: [`--link GovernorHarness:token=${token}`, '--optimistic_loop', '--optimistic_hashing'],
files: [
'certora/harnesses/GovernorHarness.sol',
`certora/harnesses/${token}.sol`,
],
options: [
`--link GovernorHarness:token=${token}`,
'--optimistic_loop',
'--optimistic_hashing',
],
})),
// WIP part
// ...product(
// ['GovernorFunctions'],
// ['ERC20VotesBlocknumberHarness'],
// ).map(([spec, token]) => ({
// spec,
// contract: 'GovernorHarness',
// files: ['certora/harnesses/GovernorHarness.sol', `certora/harnesses/${token}.sol`],
// options: [`--link GovernorHarness:token=${token}`, '--optimistic_loop', '--optimistic_hashing'],
// })),
...product(
['GovernorFunctions'],
['ERC20VotesBlocknumberHarness'],
).map(([spec, token]) => ({
spec,
contract: 'GovernorHarness',
files: [
'certora/harnesses/GovernorHarness.sol',
`certora/harnesses/${token}.sol`,
],
options: [
`--link GovernorHarness:token=${token}`,
'--optimistic_loop',
'--optimistic_hashing',
],
})),
];

18
certora/specs/Governor.helpers.spec
View File

@ -1,5 +1,18 @@
import "helpers.spec"
import "methods/IGovernor.spec"
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Sanity │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
function clockSanity(env e) returns bool {
return
e.block.number < max_uint48() &&
e.block.timestamp < max_uint48() &&
clock(e) > 0;
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ States │
@ -16,8 +29,7 @@ definition EXPIRED() returns uint8 = 6;
definition EXECUTED() returns uint8 = 7;
function safeState(env e, uint256 pId) returns uint8 {
uint8 result = state@withrevert(e, pId);
return lastReverted ? UNSET() : result;
return proposalCreated(pId) ? state(e, pId): UNSET();
}
definition proposalCreated(uint256 pId) returns bool =
@ -122,4 +134,4 @@ function helperFunctionsWithRevert(env e, method f, uint256 pId) {
{
require false;
}
}
}

27
certora/specs/GovernorChanges.spec Normal file
View File

@ -0,0 +1,27 @@
import "helpers.spec"
import "methods/IGovernor.spec"
import "Governor.helpers.spec"
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: internal variables can only change though specific functions calls │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule changes(uint256 pId, env e) {
require nonpayable(e);
require clockSanity(e);
address user;
bool isExecutedBefore = isExecuted(pId);
bool isCanceledBefore = isCanceled(pId);
bool isQueuedBefore = isQueued(pId);
bool hasVotedBefore = hasVoted(pId, user);
method f; calldataarg args; f(e, args);
assert isExecuted(pId) != isExecutedBefore => (!isExecutedBefore && f.selector == execute(address[],uint256[],bytes[],bytes32).selector);
assert isCanceled(pId) != isCanceledBefore => (!isCanceledBefore && f.selector == cancel(address[],uint256[],bytes[],bytes32).selector);
assert isQueued(pId) != isQueuedBefore => (!isQueuedBefore && f.selector == queue(address[],uint256[],bytes[],bytes32).selector);
assert hasVoted(pId, user) != hasVotedBefore => (!hasVotedBefore && voting(f));
}

48
certora/specs/GovernorFunctions.spec
View File

@ -9,6 +9,7 @@ import "Governor.helpers.spec"
*/
rule propose(uint256 pId, env e) {
require nonpayable(e);
require clockSanity(e);
uint256 otherId;
@ -18,8 +19,8 @@ rule propose(uint256 pId, env e) {
uint256 otherVoteEnd = proposalDeadline(otherId);
address otherProposer = proposalProposer(otherId);
address[] targets; uint256[] values; bytes[] calldatas; string reason;
require pId == propose@withrevert(e, targets, values, calldatas, reason);
address[] targets; uint256[] values; bytes[] calldatas; string descr;
require pId == propose@withrevert(e, targets, values, calldatas, descr);
bool success = !lastReverted;
// liveness & double proposal
@ -49,6 +50,7 @@ rule castVote(uint256 pId, env e, method f)
filtered { f -> voting(f) }
{
require nonpayable(e);
require clockSanity(e);
uint8 support;
address voter;
@ -96,17 +98,24 @@ rule castVote(uint256 pId, env e, method f)
assert getAbstainVotes(otherId) != otherAbstainVotesBefore => (otherId == pId);
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: queue effect and liveness. │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule queue(uint256 pId, env e) {
require nonpayable(e);
require clockSanity(e);
uint256 otherId;
uint8 stateBefore = state(e, pId);
uint8 otherStateBefore = state(e, otherId);
uint8 stateBefore = state(e, pId);
uint8 otherStateBefore = state(e, otherId);
bool queuedBefore = isQueued(pId)
bool otherQueuedBefore = isQueued(otherId)
address[] targets; uint256[] values; bytes[] calldatas; string reason;
require pId == queue@withrevert(e, targets, values, calldatas, reason);
address[] targets; uint256[] values; bytes[] calldatas; bytes32 descrHash;
require pId == queue@withrevert(e, targets, values, calldatas, descrHash);
bool success = !lastReverted;
// liveness
@ -115,22 +124,31 @@ rule queue(uint256 pId, env e) {
// effect
assert success => (
state(e, pId) == QUEUED()
!queuedBefore &&
isQueued(pId)
);
// no side-effect
assert state(e, otherId) != otherStateBefore => otherId == pId;
assert isQueued(otherId) != queuedBefore => otherId == pId;
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: execute effect and liveness. │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule execute(uint256 pId, env e) {
require nonpayable(e);
require clockSanity(e);
uint256 otherId;
uint8 stateBefore = state(e, pId);
uint8 otherStateBefore = state(e, otherId);
address[] targets; uint256[] values; bytes[] calldatas; string reason;
require pId == execute@withrevert(e, targets, values, calldatas, reason);
address[] targets; uint256[] values; bytes[] calldatas; bytes32 descrHash;
require pId == execute@withrevert(e, targets, values, calldatas, descrHash);
bool success = !lastReverted;
// liveness: can't check full equivalence because of execution call reverts
@ -145,16 +163,22 @@ rule execute(uint256 pId, env e) {
assert state(e, otherId) != otherStateBefore => otherId == pId;
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: cancel (public) effect and liveness. │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule cancel(uint256 pId, env e) {
require nonpayable(e);
require clockSanity(e);
uint256 otherId;
uint8 stateBefore = state(e, pId);
uint8 otherStateBefore = state(e, otherId);
address[] targets; uint256[] values; bytes[] calldatas; string reason;
require pId == cancel@withrevert(e, targets, values, calldatas, reason);
address[] targets; uint256[] values; bytes[] calldatas; bytes32 descrHash;
require pId == cancel@withrevert(e, targets, values, calldatas, descrHash);
bool success = !lastReverted;
// liveness
@ -170,4 +194,4 @@ rule cancel(uint256 pId, env e) {
// no side-effect
assert state(e, otherId) != otherStateBefore => otherId == pId;
}
}

21
certora/specs/GovernorInvariants.spec
View File

@ -8,7 +8,7 @@ import "Governor.helpers.spec"
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule clockMode(env e) {
require e.block.number < max_uint48() && e.block.timestamp < max_uint48();
require clockSanity(e);
assert clock(e) == e.block.number || clock(e) == e.block.timestamp;
assert clock(e) == token_clock(e);
@ -31,7 +31,7 @@ invariant proposalStateConsistency(uint256 pId)
(proposalProposer(pId) == 0 <=> proposalDeadline(pId) == 0)
{
preserved with (env e) {
require clock(e) > 0;
require clockSanity(e);
}
}
@ -44,8 +44,8 @@ invariant canceledImplyCreated(uint pId)
isCanceled(pId) => proposalCreated(pId)
{
preserved with (env e) {
require clockSanity(e);
requireInvariant proposalStateConsistency(pId);
require clock(e) > 0;
}
}
@ -58,21 +58,22 @@ invariant executedImplyCreated(uint pId)
isExecuted(pId) => proposalCreated(pId)
{
preserved with (env e) {
require clockSanity(e);
requireInvariant proposalStateConsistency(pId);
require clock(e) > 0;
}
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: The state UNSET() correctly catch uninitialized proposal. │
│ Invariant: queued => created │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant proposalStateConsistencyUnset(env e, uint256 pId)
proposalCreated(pId) <=> safeState(e, pId) == UNSET()
invariant queuedImplyCreated(uint pId)
isQueued(pId) => proposalCreated(pId)
{
preserved {
require clock(e) > 0;
preserved with (env e) {
require clockSanity(e);
requireInvariant proposalStateConsistency(pId);
}
}
@ -103,4 +104,4 @@ invariant noBothExecutedAndCanceled(uint256 pId)
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant governanceCallLength()
governanceCallLength() == 0
governanceCallLength() == 0

17
certora/specs/GovernorStates.spec
View File

@ -31,7 +31,7 @@ rule stateConsistency(env e, uint256 pId) {
rule stateTransitionFn(uint256 pId, env e, method f, calldataarg args)
filtered { f -> !skip(f) }
{
require clock(e) > 0; // Sanity
require clockSanity(e);
uint8 stateBefore = state(e, pId);
f(e, args);
@ -64,7 +64,8 @@ rule stateTransitionFn(uint256 pId, env e, method f, calldataarg args)
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule stateTransitionWait(uint256 pId, env e1, env e2) {
require clock(e1) > 0; // Sanity
require clockSanity(e1);
require clockSanity(e2);
require clock(e2) > clock(e1);
uint8 stateBefore = state(e1, pId);
@ -87,25 +88,25 @@ rule stateTransitionWait(uint256 pId, env e1, env e2) {
│ Rule: State corresponds to the vote timing and results │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule stateFollowsVoteTimmingAndResult(uint256 pId, env e) {
require clock(e) > 0; // Sanity
rule stateIsConsistentWithVotes(uint256 pId, env e) {
require clockSanity(e);
requireInvariant proposalStateConsistency(pId);
uint8 currentState = state(e, pId);
uint48 currentClock = clock(e);
// Pending = before vote starts
// Pending: before vote starts
assert currentState == PENDING() => (
proposalSnapshot(pId) >= currentClock
);
// Active = after vote starts & before vote ends
// Active: after vote starts & before vote ends
assert currentState == ACTIVE() => (
proposalSnapshot(pId) < currentClock &&
proposalDeadline(pId) >= currentClock
);
// Succeeded = after vote end, with vote successful and quorum reached
// Succeeded: after vote end, with vote successful and quorum reached
assert currentState == SUCCEEDED() => (
proposalDeadline(pId) < currentClock &&
(
@ -114,7 +115,7 @@ rule stateFollowsVoteTimmingAndResult(uint256 pId, env e) {
)
);
// Succeeded = after vote end, with vote not successful or quorum not reached
// Defeated: after vote end, with vote not successful or quorum not reached
assert currentState == DEFEATED() => (
proposalDeadline(pId) < currentClock &&
(

1
certora/specs/methods/IGovernor.spec
View File

@ -39,6 +39,7 @@ methods {
voteSucceeded(uint256) returns bool envfree
isExecuted(uint256) returns bool envfree
isCanceled(uint256) returns bool envfree
isQueued(uint256) returns bool envfree
governanceCallLength() returns uint256 envfree
getAgainstVotes(uint256) returns uint256 envfree
getForVotes(uint256) returns uint256 envfree