From 67a00ccaea62daff509bc18add4354fbd8cc40df Mon Sep 17 00:00:00 2001 From: Hadrien Croubois Date: Fri, 17 Mar 2023 11:14:02 +0100 Subject: [PATCH] disable specs we can't fix :/ --- certora/specs.js | 6 ++- certora/specs/GovernorBaseRules.spec | 23 +++++++--- certora/specs/GovernorStates.spec | 65 ++++++++++++++++++---------- 3 files changed, 62 insertions(+), 32 deletions(-) diff --git a/certora/specs.js b/certora/specs.js index ac0dce088..0b7c36cb8 100644 --- a/certora/specs.js +++ b/certora/specs.js @@ -73,8 +73,9 @@ module.exports = [].concat( options: [ `--link ${contract}:token=${token}`, `--link ${contract}:_timelock=TimelockControllerHarness`, - '--optimistic_loop', '--optimistic_hashing', + '--optimistic_loop', + '--loop_iter 3', ], })), product( @@ -93,8 +94,9 @@ module.exports = [].concat( options: [ `--link ${contract}:token=${token}`, `--link ${contract}:_timelock=TimelockControllerHarness`, - '--optimistic_loop', '--optimistic_hashing', + '--optimistic_loop', + '--loop_iter 3', '--rules', ...['liveness', 'effect', 'sideeffect'].map(kind => `${fn}_${kind}`), ], diff --git a/certora/specs/GovernorBaseRules.spec b/certora/specs/GovernorBaseRules.spec index ad5115727..cac8da2a3 100644 --- a/certora/specs/GovernorBaseRules.spec +++ b/certora/specs/GovernorBaseRules.spec @@ -73,18 +73,27 @@ rule noDoubleVoting(uint256 pId, env e, method f) │ Rule: Voting against a proposal does not count towards quorum. │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -rule againstVotesDontCountTowardsQuorum(uint256 pId, env e, method f) - filtered { f -> voting(f) } +rule againstVotesDontCountTowardsQuorum(uint256 pId, env e) { - address voter; - bool quorumReachedBefore = quorumReached(pId); - - helperVoteWithRevert(e, f, pId, voter, 0); // support 0 = against - + castVote(e, pId, 0); assert quorumReached(pId) == quorumReachedBefore, "quorum must not be reached with an against vote"; } +/// This version is more exaustive, but to slow because "quorumReached" is a FV nightmare +// rule againstVotesDontCountTowardsQuorum(uint256 pId, env e, method f) +// filtered { f -> voting(f) } +// { +// address voter; +// +// bool quorumReachedBefore = quorumReached(pId); +// +// helperVoteWithRevert(e, f, pId, voter, 0); // support 0 = against +// +// assert quorumReached(pId) == quorumReachedBefore, "quorum must not be reached with an against vote"; +// } + + /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ Rule: A proposal could be executed only if quorum was reached and vote succeeded │ diff --git a/certora/specs/GovernorStates.spec b/certora/specs/GovernorStates.spec index eece8bf09..a1dc7eada 100644 --- a/certora/specs/GovernorStates.spec +++ b/certora/specs/GovernorStates.spec @@ -3,7 +3,7 @@ import "Governor.helpers.spec" import "GovernorInvariants.spec" use invariant proposalStateConsistency -use invariant votesImplySnapshotPassed +// use invariant votesImplySnapshotPassed /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ @@ -131,27 +131,46 @@ rule stateIsConsistentWithVotes(uint256 pId, env e) { /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Rule: `updateQuorumNumerator` cannot cause quorumReached to change. │ +│ [NEED WORK] Rule: `updateQuorumNumerator` cannot cause quorumReached to change. │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -rule onlyVoteCanChangeQuorumReached(uint256 pId, env e, method f, calldataarg args) - filtered { f -> !skip(f) } -{ - require clockSanity(e); - requireInvariant votesImplySnapshotPassed(e, pId); - - bool quorumReachedBefore = quorumReached(pId); - - uint256 snapshot = proposalSnapshot(pId); - uint256 totalSupply = token_getPastTotalSupply(snapshot); - - f(e, args); - - // Needed because the prover doesn't understand the checkpoint properties of the voting token. - require clock(e) > snapshot => token_getPastTotalSupply(snapshot) == totalSupply; - - assert quorumReached(pId) != quorumReachedBefore => ( - !quorumReachedBefore && - votingAll(f) - ); -} +//// This would be nice, but its way to slow to run because "quorumReached" is a FV nightmare +//// Also, for it to work we need to prove that the checkpoints have (strictly) increase values ... what a nightmare +// rule onlyVoteCanChangeQuorumReached(uint256 pId, env e, method f, calldataarg args) +// filtered { f -> !skip(f) } +// { +// require clockSanity(e); +// require clock(e) > proposalSnapshot(pId); // vote has started +// require quorumNumeratorLength() < max_uint256; // sanity +// +// bool quorumReachedBefore = quorumReached(pId); +// +// uint256 snapshot = proposalSnapshot(pId); +// uint256 totalSupply = token_getPastTotalSupply(snapshot); +// +// f(e, args); +// +// // Needed because the prover doesn't understand the checkpoint properties of the voting token. +// require clock(e) > snapshot => token_getPastTotalSupply(snapshot) == totalSupply; +// +// assert quorumReached(pId) != quorumReachedBefore => ( +// !quorumReachedBefore && +// votingAll(f) +// ); +// } + +//// To prove that, we need to prove that the checkpoints have (strictly) increase values ... what a nightmare +//// otherwise it gives us counter example where the checkpoint history has keys: +//// [ 12,12,13,13,12] and the lookup obviously fail to get the correct value +// rule quorumUpdateDoesntAffectPastProposals(uint256 pId, env e) { +// require clockSanity(e); +// require clock(e) > proposalSnapshot(pId); // vote has started +// require quorumNumeratorLength() < max_uint256; // sanity +// +// bool quorumReachedBefore = quorumReached(pId); +// +// uint256 newQuorumNumerator; +// updateQuorumNumerator(e, newQuorumNumerator); +// +// assert quorumReached(pId) == quorumReachedBefore; +// }