From c7a544d5689b4007bb61977174e12b284b2d5c00 Mon Sep 17 00:00:00 2001 From: Hadrien Croubois Date: Thu, 29 Sep 2022 18:40:14 +0200 Subject: [PATCH] move passing scripts out of noCI --- certora/applyHarness.patch | 40 +++-- ...rumHarness.sol => GovernorFullHarness.sol} | 16 +- certora/harnesses/GovernorHarness.sol | 159 ++++++++++++++++++ certora/harnesses/WizardFirstTry.sol | 2 +- certora/scripts/noCI/Round1/Governor.sh | 12 -- .../Round1/GovernorCountingSimple-counting.sh | 11 -- .../noCI/Round1/WizardControlFirstPriority.sh | 4 +- certora/scripts/noCI/Round1/WizardFirstTry.sh | 4 +- .../scripts/noCI/Round2/verifyERC20Wrapper.sh | 2 +- .../Round3/verifyGovernorPreventLateQuorum.sh | 10 +- .../Round2 => passes}/verifyERC20FlashMint.sh | 3 - .../Round2 => passes}/verifyERC20Votes.sh | 1 - certora/scripts/passes/verifyGovernor.sh | 16 ++ .../passes/verifyGovernorCountingSimple.sh | 13 ++ certora/specs/ERC20Votes.spec | 83 +++------ certora/specs/ERC20Wrapper.spec | 51 +++--- certora/specs/GovernorBase.spec | 12 +- certora/specs/GovernorPreventLateQuorum.spec | 81 +++++---- 18 files changed, 329 insertions(+), 191 deletions(-) rename certora/harnesses/{GovernorPreventLateQuorumHarness.sol => GovernorFullHarness.sol} (98%) create mode 100644 certora/harnesses/GovernorHarness.sol delete mode 100755 certora/scripts/noCI/Round1/Governor.sh delete mode 100644 certora/scripts/noCI/Round1/GovernorCountingSimple-counting.sh rename certora/scripts/{noCI/Round2 => passes}/verifyERC20FlashMint.sh (64%) rename certora/scripts/{noCI/Round2 => passes}/verifyERC20Votes.sh (90%) create mode 100755 certora/scripts/passes/verifyGovernor.sh create mode 100644 certora/scripts/passes/verifyGovernorCountingSimple.sh diff --git a/certora/applyHarness.patch b/certora/applyHarness.patch index d3c404866..b36796bb5 100644 --- a/certora/applyHarness.patch +++ b/certora/applyHarness.patch @@ -37,7 +37,7 @@ diff -ruN governance/extensions/GovernorPreventLateQuorum.sol governance/extensi /// @dev Emitted when a proposal deadline is pushed back due to reaching quorum late in its voting period. event ProposalExtended(uint256 indexed proposalId, uint64 extendedDeadline); diff -ruN governance/Governor.sol governance/Governor.sol ---- governance/Governor.sol 2022-09-27 10:26:58.548890299 +0200 +--- governance/Governor.sol 2022-09-29 10:07:27.126075551 +0200 +++ governance/Governor.sol 2022-09-27 17:51:32.014634743 +0200 @@ -44,7 +44,7 @@ @@ -49,7 +49,7 @@ diff -ruN governance/Governor.sol governance/Governor.sol // This queue keeps track of the governor operating on itself. Calls to functions protected by the // {onlyGovernance} modifier needs to be whitelisted in this queue. Whitelisting is set in {_beforeExecute}, diff -ruN governance/TimelockController.sol governance/TimelockController.sol ---- governance/TimelockController.sol 2022-09-27 10:26:58.548890299 +0200 +--- governance/TimelockController.sol 2022-09-29 10:07:27.126075551 +0200 +++ governance/TimelockController.sol 2022-09-27 17:51:32.014634743 +0200 @@ -28,10 +28,10 @@ bytes32 public constant PROPOSER_ROLE = keccak256("PROPOSER_ROLE"); @@ -231,7 +231,7 @@ diff -ruN mocks/SafeERC20Helper.sol mocks/SafeERC20Helper.sol contract SafeERC20Wrapper is Context { using SafeERC20 for IERC20; diff -ruN proxy/utils/Initializable.sol proxy/utils/Initializable.sol ---- proxy/utils/Initializable.sol 2022-09-27 10:26:58.548890299 +0200 +--- proxy/utils/Initializable.sol 2022-09-29 10:07:27.126075551 +0200 +++ proxy/utils/Initializable.sol 2022-09-27 17:51:32.014634743 +0200 @@ -59,12 +59,12 @@ * @dev Indicates that the contract has been initialized. @@ -280,7 +280,7 @@ diff -ruN token/ERC1155/ERC1155.sol token/ERC1155/ERC1155.sol bytes4 response diff -ruN token/ERC20/ERC20.sol token/ERC20/ERC20.sol --- token/ERC20/ERC20.sol 2022-09-27 10:26:58.548890299 +0200 -+++ token/ERC20/ERC20.sol 2022-09-27 22:22:40.377802680 +0200 ++++ token/ERC20/ERC20.sol 2022-09-29 10:09:07.479688477 +0200 @@ -256,7 +256,7 @@ * * - `account` cannot be the zero address. @@ -299,8 +299,20 @@ diff -ruN token/ERC20/ERC20.sol token/ERC20/ERC20.sol require(account != address(0), "ERC20: burn from the zero address"); _beforeTokenTransfer(account, address(0), amount); +diff -ruN token/ERC20/extensions/ERC20Capped.sol token/ERC20/extensions/ERC20Capped.sol +--- token/ERC20/extensions/ERC20Capped.sol 2022-08-31 13:44:36.381058287 +0200 ++++ token/ERC20/extensions/ERC20Capped.sol 2022-09-29 10:09:41.376517581 +0200 +@@ -30,7 +30,7 @@ + /** + * @dev See {ERC20-_mint}. + */ +- function _mint(address account, uint256 amount) internal virtual override { ++ function _mint(address account, uint256 amount) public virtual override { // HARNESS: internal -> public + require(ERC20.totalSupply() + amount <= cap(), "ERC20Capped: cap exceeded"); + super._mint(account, amount); + } diff -ruN token/ERC20/extensions/ERC20FlashMint.sol token/ERC20/extensions/ERC20FlashMint.sol ---- token/ERC20/extensions/ERC20FlashMint.sol 2022-09-27 10:26:58.548890299 +0200 +--- token/ERC20/extensions/ERC20FlashMint.sol 2022-09-29 10:07:27.126075551 +0200 +++ token/ERC20/extensions/ERC20FlashMint.sol 2022-09-27 17:51:32.014634743 +0200 @@ -51,9 +51,11 @@ // silence warning about unused variable without the addition of bytecode. @@ -317,7 +329,7 @@ diff -ruN token/ERC20/extensions/ERC20FlashMint.sol token/ERC20/extensions/ERC20 * implementation returns the address(0) which means the fee amount will be burnt. diff -ruN token/ERC20/extensions/ERC20Votes.sol token/ERC20/extensions/ERC20Votes.sol --- token/ERC20/extensions/ERC20Votes.sol 2022-09-27 10:26:58.548890299 +0200 -+++ token/ERC20/extensions/ERC20Votes.sol 2022-09-27 17:51:32.014634743 +0200 ++++ token/ERC20/extensions/ERC20Votes.sol 2022-09-29 10:09:45.489874234 +0200 @@ -33,8 +33,8 @@ bytes32 private constant _DELEGATION_TYPEHASH = keccak256("Delegation(address delegatee,uint256 nonce,uint256 expiry)"); @@ -329,7 +341,7 @@ diff -ruN token/ERC20/extensions/ERC20Votes.sol token/ERC20/extensions/ERC20Vote Checkpoint[] private _totalSupplyCheckpoints; /** -@@ -165,7 +165,7 @@ +@@ -165,27 +165,27 @@ /** * @dev Maximum token supply. Defaults to `type(uint224).max` (2^224^ - 1). */ @@ -338,7 +350,11 @@ diff -ruN token/ERC20/extensions/ERC20Votes.sol token/ERC20/extensions/ERC20Vote return type(uint224).max; } -@@ -176,16 +176,16 @@ + /** + * @dev Snapshots the totalSupply after it has been increased. + */ +- function _mint(address account, uint256 amount) internal virtual override { ++ function _mint(address account, uint256 amount) public virtual override { // HARNESS: internal -> public super._mint(account, amount); require(totalSupply() <= _maxSupply(), "ERC20Votes: total supply risks overflowing votes"); @@ -441,18 +457,18 @@ diff -ruN token/ERC20/extensions/ERC20Votes.sol token/ERC20/extensions/ERC20Vote } diff -ruN token/ERC20/extensions/ERC20Wrapper.sol token/ERC20/extensions/ERC20Wrapper.sol --- token/ERC20/extensions/ERC20Wrapper.sol 2022-08-31 13:44:36.381058287 +0200 -+++ token/ERC20/extensions/ERC20Wrapper.sol 2022-09-27 17:51:32.014634743 +0200 ++++ token/ERC20/extensions/ERC20Wrapper.sol 2022-09-28 11:25:39.319711517 +0200 @@ -55,7 +55,7 @@ * @dev Mint wrapped token to cover any underlyingTokens that would have been transferred by mistake. Internal * function that can be exposed with access control if desired. */ - function _recover(address account) internal virtual returns (uint256) { -+ function _recover(address account) public virtual returns (uint256) { // HARNESS: internal -> public ++ function _recover(address account) public virtual returns (uint256) { // HARNESS: internal -> public uint256 value = underlying.balanceOf(address(this)) - totalSupply(); _mint(account, value); return value; diff -ruN token/ERC721/extensions/draft-ERC721Votes.sol token/ERC721/extensions/draft-ERC721Votes.sol ---- token/ERC721/extensions/draft-ERC721Votes.sol 2022-09-27 10:26:58.548890299 +0200 +--- token/ERC721/extensions/draft-ERC721Votes.sol 2022-09-29 10:07:27.126075551 +0200 +++ token/ERC721/extensions/draft-ERC721Votes.sol 2022-09-27 17:51:32.014634743 +0200 @@ -49,7 +49,7 @@ /** @@ -464,7 +480,7 @@ diff -ruN token/ERC721/extensions/draft-ERC721Votes.sol token/ERC721/extensions/ } } diff -ruN utils/Address.sol utils/Address.sol ---- utils/Address.sol 2022-09-27 10:26:58.552223642 +0200 +--- utils/Address.sol 2022-09-29 10:07:27.126075551 +0200 +++ utils/Address.sol 2022-09-27 17:51:32.014634743 +0200 @@ -131,6 +131,7 @@ uint256 value, diff --git a/certora/harnesses/GovernorPreventLateQuorumHarness.sol b/certora/harnesses/GovernorFullHarness.sol similarity index 98% rename from certora/harnesses/GovernorPreventLateQuorumHarness.sol rename to certora/harnesses/GovernorFullHarness.sol index 2a9e54b66..026a32eae 100644 --- a/certora/harnesses/GovernorPreventLateQuorumHarness.sol +++ b/certora/harnesses/GovernorFullHarness.sol @@ -1,21 +1,21 @@ // SPDX-License-Identifier: MIT pragma solidity ^0.8.2; -import "../munged/governance/extensions/GovernorPreventLateQuorum.sol"; import "../munged/governance/Governor.sol"; import "../munged/governance/extensions/GovernorCountingSimple.sol"; +import "../munged/governance/extensions/GovernorPreventLateQuorum.sol"; +import "../munged/governance/extensions/GovernorTimelockControl.sol"; import "../munged/governance/extensions/GovernorVotes.sol"; import "../munged/governance/extensions/GovernorVotesQuorumFraction.sol"; -import "../munged/governance/extensions/GovernorTimelockControl.sol"; import "../munged/token/ERC20/extensions/ERC20Votes.sol"; -contract GovernorPreventLateQuorumHarness is +contract GovernorFullHarness is Governor, GovernorCountingSimple, - GovernorVotes, - GovernorVotesQuorumFraction, GovernorTimelockControl, - GovernorPreventLateQuorum + GovernorPreventLateQuorum, + GovernorVotes, + GovernorVotesQuorumFraction { using SafeCast for uint256; using Timers for Timers.BlockNumber; @@ -27,10 +27,10 @@ contract GovernorPreventLateQuorumHarness is uint256 quorumNumeratorValue ) Governor("Harness") + GovernorPreventLateQuorum(initialVoteExtension) + GovernorTimelockControl(_timelock) GovernorVotes(_token) GovernorVotesQuorumFraction(quorumNumeratorValue) - GovernorTimelockControl(_timelock) - GovernorPreventLateQuorum(initialVoteExtension) {} mapping(uint256 => uint256) public ghost_sum_vote_power_by_id; diff --git a/certora/harnesses/GovernorHarness.sol b/certora/harnesses/GovernorHarness.sol new file mode 100644 index 000000000..2f6151f12 --- /dev/null +++ b/certora/harnesses/GovernorHarness.sol @@ -0,0 +1,159 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.2; + +import "../munged/governance/Governor.sol"; +import "../munged/governance/extensions/GovernorCountingSimple.sol"; +import "../munged/governance/extensions/GovernorTimelockControl.sol"; +import "../munged/governance/extensions/GovernorVotes.sol"; +import "../munged/governance/extensions/GovernorVotesQuorumFraction.sol"; +import "../munged/token/ERC20/extensions/ERC20Votes.sol"; + +contract GovernorHarness is + Governor, + GovernorCountingSimple, + GovernorVotes, + GovernorVotesQuorumFraction, + GovernorTimelockControl +{ + using SafeCast for uint256; + using Timers for Timers.BlockNumber; + + constructor( + IVotes _token, + TimelockController _timelock, + uint64 initialVoteExtension, + uint256 quorumNumeratorValue + ) + Governor("Harness") + GovernorVotes(_token) + GovernorVotesQuorumFraction(quorumNumeratorValue) + GovernorTimelockControl(_timelock) + {} + + mapping(uint256 => uint256) public ghost_sum_vote_power_by_id; + + // variable added to check when _castVote is called + uint256 public latestCastVoteCall; + + // Harness from GovernorCountingSimple // + + function getAgainstVotes(uint256 proposalId) public view returns (uint256) { + ProposalVote storage proposalvote = _proposalVotes[proposalId]; + return proposalvote.againstVotes; + } + + function getAbstainVotes(uint256 proposalId) public view returns (uint256) { + ProposalVote storage proposalvote = _proposalVotes[proposalId]; + return proposalvote.abstainVotes; + } + + function getForVotes(uint256 proposalId) public view returns (uint256) { + ProposalVote storage proposalvote = _proposalVotes[proposalId]; + return proposalvote.forVotes; + } + + function quorumReached(uint256 proposalId) public view returns (bool) { + return _quorumReached(proposalId); + } + + function voteSucceeded(uint256 proposalId) public view returns (bool) { + return _voteSucceeded(proposalId); + } + + // Harness from Governor // + + function getExecutor() public view returns (address) { + return _executor(); + } + + function isExecuted(uint256 proposalId) public view returns (bool) { + return _proposals[proposalId].executed; + } + + function isCanceled(uint256 proposalId) public view returns (bool) { + return _proposals[proposalId].canceled; + } + + // The following functions are overrides required by Solidity added by Certora. // + + function _castVote( + uint256 proposalId, + address account, + uint8 support, + string memory reason, + bytes memory params + ) internal virtual override returns (uint256) { + // flag for when _castVote is called + latestCastVoteCall = block.number; + + // added to run GovernorCountingSimple.spec + uint256 deltaWeight = super._castVote(proposalId, account, support, reason, params); + ghost_sum_vote_power_by_id[proposalId] += deltaWeight; + + return deltaWeight; + } + + // The following functions are overrides required by Solidity added by OZ Wizard. // + + function votingDelay() public pure override returns (uint256) { + return 1; // 1 block + } + + function votingPeriod() public pure override returns (uint256) { + return 45818; // 1 week + } + + function quorum(uint256 blockNumber) + public + view + override(IGovernor, GovernorVotesQuorumFraction) + returns (uint256) + { + return super.quorum(blockNumber); + } + + function state(uint256 proposalId) public view override(Governor, GovernorTimelockControl) returns (ProposalState) { + return super.state(proposalId); + } + + function propose( + address[] memory targets, + uint256[] memory values, + bytes[] memory calldatas, + string memory description + ) public override(Governor, IGovernor) returns (uint256) { + return super.propose(targets, values, calldatas, description); + } + + function _execute( + uint256 proposalId, + address[] memory targets, + uint256[] memory values, + bytes[] memory calldatas, + bytes32 descriptionHash + ) internal override(Governor, GovernorTimelockControl) { + super._execute(proposalId, targets, values, calldatas, descriptionHash); + } + + function _cancel( + address[] memory targets, + uint256[] memory values, + bytes[] memory calldatas, + bytes32 descriptionHash + ) internal override(Governor, GovernorTimelockControl) returns (uint256) { + return super._cancel(targets, values, calldatas, descriptionHash); + } + + function _executor() internal view override(Governor, GovernorTimelockControl) returns (address) { + return super._executor(); + } + + function supportsInterface(bytes4 interfaceId) + public + view + override(Governor, GovernorTimelockControl) + returns (bool) + { + return super.supportsInterface(interfaceId); + } +} diff --git a/certora/harnesses/WizardFirstTry.sol b/certora/harnesses/WizardFirstTry.sol index 2c8b382f1..17fee0c14 100644 --- a/certora/harnesses/WizardFirstTry.sol +++ b/certora/harnesses/WizardFirstTry.sol @@ -8,7 +8,7 @@ import "../munged/governance/extensions/GovernorVotesQuorumFraction.sol"; import "../munged/governance/extensions/GovernorTimelockCompound.sol"; import "../munged/token/ERC20/extensions/ERC20Votes.sol"; -/* +/* Wizard options: ERC20Votes TimelockCompound diff --git a/certora/scripts/noCI/Round1/Governor.sh b/certora/scripts/noCI/Round1/Governor.sh deleted file mode 100755 index 525731d97..000000000 --- a/certora/scripts/noCI/Round1/Governor.sh +++ /dev/null @@ -1,12 +0,0 @@ -#!/usr/bin/env bash - -set -euxo pipefail - -# Changed: GovernorHarness → GovernorPreventLateQuorumHarness -certoraRun \ - certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorPreventLateQuorumHarness.sol \ - --verify GovernorPreventLateQuorumHarness:certora/specs/GovernorBase.spec \ - --solc solc \ - --optimistic_loop \ - --settings -copyLoopUnroll=4 \ - --rule voteStartBeforeVoteEnd diff --git a/certora/scripts/noCI/Round1/GovernorCountingSimple-counting.sh b/certora/scripts/noCI/Round1/GovernorCountingSimple-counting.sh deleted file mode 100644 index 2ead5ae58..000000000 --- a/certora/scripts/noCI/Round1/GovernorCountingSimple-counting.sh +++ /dev/null @@ -1,11 +0,0 @@ -#!/usr/bin/env bash - -set -euxo pipefail - -# Changed: GovernorBasicHarness → GovernorPreventLateQuorumHarness -certoraRun \ - certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorPreventLateQuorumHarness.sol \ - --verify GovernorPreventLateQuorumHarness:certora/specs/GovernorCountingSimple.spec \ - --solc solc \ - --optimistic_loop \ - --settings -copyLoopUnroll=4 diff --git a/certora/scripts/noCI/Round1/WizardControlFirstPriority.sh b/certora/scripts/noCI/Round1/WizardControlFirstPriority.sh index da7d172a4..4d64fb411 100644 --- a/certora/scripts/noCI/Round1/WizardControlFirstPriority.sh +++ b/certora/scripts/noCI/Round1/WizardControlFirstPriority.sh @@ -4,10 +4,10 @@ set -euxo pipefail certoraRun \ certora/harnesses/ERC20VotesHarness.sol certora/harnesses/WizardControlFirstPriority.sol \ - --link WizardControlFirstPriority:token=ERC20VotesHarness \ --verify WizardControlFirstPriority:certora/specs/GovernorBase.spec \ + --link WizardControlFirstPriority:token=ERC20VotesHarness \ --solc solc \ --optimistic_loop \ --disableLocalTypeChecking \ --settings -copyLoopUnroll=4 \ - --rule canVoteDuringVotingPeriod + $@ diff --git a/certora/scripts/noCI/Round1/WizardFirstTry.sh b/certora/scripts/noCI/Round1/WizardFirstTry.sh index 8d2f546db..5780072eb 100644 --- a/certora/scripts/noCI/Round1/WizardFirstTry.sh +++ b/certora/scripts/noCI/Round1/WizardFirstTry.sh @@ -5,7 +5,9 @@ set -euxo pipefail certoraRun \ certora/harnesses/ERC20VotesHarness.sol certora/harnesses/WizardFirstTry.sol \ --verify WizardFirstTry:certora/specs/GovernorBase.spec \ + --link WizardFirstTry:token=ERC20VotesHarness \ --solc solc \ --optimistic_loop \ --disableLocalTypeChecking \ - --settings -copyLoopUnroll=4 + --settings -copyLoopUnroll=4 \ + $@ diff --git a/certora/scripts/noCI/Round2/verifyERC20Wrapper.sh b/certora/scripts/noCI/Round2/verifyERC20Wrapper.sh index de119e579..b5ff53587 100644 --- a/certora/scripts/noCI/Round2/verifyERC20Wrapper.sh +++ b/certora/scripts/noCI/Round2/verifyERC20Wrapper.sh @@ -2,10 +2,10 @@ set -euxo pipefail + # --link ERC20WrapperHarness:underlying=DummyERC20A \ certoraRun \ certora/harnesses/ERC20WrapperHarness.sol certora/helpers/DummyERC20A.sol certora/helpers/DummyERC20B.sol \ --verify ERC20WrapperHarness:certora/specs/ERC20Wrapper.spec \ --solc solc \ --optimistic_loop \ - --msg "ERC20Wrapper verification" \ $@ diff --git a/certora/scripts/noCI/Round3/verifyGovernorPreventLateQuorum.sh b/certora/scripts/noCI/Round3/verifyGovernorPreventLateQuorum.sh index 720caf0aa..8b74837e1 100644 --- a/certora/scripts/noCI/Round3/verifyGovernorPreventLateQuorum.sh +++ b/certora/scripts/noCI/Round3/verifyGovernorPreventLateQuorum.sh @@ -3,13 +3,11 @@ set -euxo pipefail certoraRun \ - certora/harnesses/ERC20VotesHarness.sol \ - certora/harnesses/ERC721VotesHarness.sol \ - certora/munged/governance/TimelockController.sol \ - certora/harnesses/GovernorPreventLateQuorumHarness.sol \ - --verify GovernorPreventLateQuorumHarness:certora/specs/GovernorPreventLateQuorum.spec \ + certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorFullHarness.sol \ + --verify GovernorFullHarness:certora/specs/GovernorPreventLateQuorum.spec \ + --link GovernorFullHarness:token=ERC20VotesHarness \ --solc solc \ --optimistic_loop \ --loop_iter 1 \ --rule_sanity advanced \ - --msg "all sanity" \ + $@ diff --git a/certora/scripts/noCI/Round2/verifyERC20FlashMint.sh b/certora/scripts/passes/verifyERC20FlashMint.sh similarity index 64% rename from certora/scripts/noCI/Round2/verifyERC20FlashMint.sh rename to certora/scripts/passes/verifyERC20FlashMint.sh index c0a0f2d40..ff7020733 100644 --- a/certora/scripts/noCI/Round2/verifyERC20FlashMint.sh +++ b/certora/scripts/passes/verifyERC20FlashMint.sh @@ -5,10 +5,7 @@ set -euxo pipefail certoraRun \ certora/harnesses/ERC20FlashMintHarness.sol \ certora/harnesses/IERC3156FlashBorrowerHarness.sol \ - certora/munged/token/ERC20/ERC20.sol \ - certora/helpers/DummyERC20A.sol certora/helpers/DummyERC20B.sol \ --verify ERC20FlashMintHarness:certora/specs/ERC20FlashMint.spec \ --solc solc \ --optimistic_loop \ - --msg "ERC20FlashMint verification" \ $@ diff --git a/certora/scripts/noCI/Round2/verifyERC20Votes.sh b/certora/scripts/passes/verifyERC20Votes.sh similarity index 90% rename from certora/scripts/noCI/Round2/verifyERC20Votes.sh rename to certora/scripts/passes/verifyERC20Votes.sh index 797f38ddb..7d3980af7 100644 --- a/certora/scripts/noCI/Round2/verifyERC20Votes.sh +++ b/certora/scripts/passes/verifyERC20Votes.sh @@ -8,5 +8,4 @@ certoraRun \ --solc solc \ --optimistic_loop \ --settings -copyLoopUnroll=4 \ - --msg "ERC20Votes" \ $@ \ No newline at end of file diff --git a/certora/scripts/passes/verifyGovernor.sh b/certora/scripts/passes/verifyGovernor.sh new file mode 100755 index 000000000..3e061745d --- /dev/null +++ b/certora/scripts/passes/verifyGovernor.sh @@ -0,0 +1,16 @@ +#!/usr/bin/env bash + +set -euxo pipefail + +# Changed: GovernorHarness missing +# +# Note: rule `immutableFieldsAfterProposalCreation` fails with +# GovernorFullHarness because of late quorum changing the vote's end. +certoraRun \ + certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorHarness.sol \ + --verify GovernorHarness:certora/specs/GovernorBase.spec \ + --link GovernorHarness:token=ERC20VotesHarness \ + --solc solc \ + --optimistic_loop \ + --settings -copyLoopUnroll=4 \ + $@ \ No newline at end of file diff --git a/certora/scripts/passes/verifyGovernorCountingSimple.sh b/certora/scripts/passes/verifyGovernorCountingSimple.sh new file mode 100644 index 000000000..1112d749c --- /dev/null +++ b/certora/scripts/passes/verifyGovernorCountingSimple.sh @@ -0,0 +1,13 @@ +#!/usr/bin/env bash + +set -euxo pipefail + +# Changed: GovernorBasicHarness missing +certoraRun \ + certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorHarness.sol \ + --verify GovernorHarness:certora/specs/GovernorCountingSimple.spec \ + --link GovernorHarness:token=ERC20VotesHarness \ + --solc solc \ + --optimistic_loop \ + --settings -copyLoopUnroll=4 \ + $@ diff --git a/certora/specs/ERC20Votes.spec b/certora/specs/ERC20Votes.spec index 3b133c2f2..b99895f45 100644 --- a/certora/specs/ERC20Votes.spec +++ b/certora/specs/ERC20Votes.spec @@ -2,45 +2,28 @@ import "erc20.spec" methods { // IVotes - getVotes(address) returns (uint256) envfree - getPastVotes(address, uint256) returns (uint256) // not envfree (reads block.number) - getPastTotalSupply(uint256) returns (uint256) // not envfree (reads block.number) - delegates(address) returns (address) envfree - delegate(address) // not envfree (reads msg.sender) - // delegateBySig(address, uint256, uint256, uint8, bytes32, bytes32) + getVotes(address) returns (uint256) envfree + getPastVotes(address, uint256) returns (uint256) // not envfree (reads block.number) + getPastTotalSupply(uint256) returns (uint256) // not envfree (reads block.number) + delegates(address) returns (address) envfree + delegate(address) // not envfree (reads msg.sender) + delegateBySig(address, uint256, uint256, uint8, bytes32, bytes32) // not envfree (reads msg.sender) // ERC20Votes - checkpoints(address, uint32) envfree - numCheckpoints(address) returns (uint32) envfree - _maxSupply() returns (uint224) envfree - _delegate(address, address) // not envfree (reads block.number when creating checkpoint) + checkpoints(address, uint32) envfree + numCheckpoints(address) returns (uint32) envfree + _maxSupply() returns (uint224) envfree + _delegate(address, address) // not envfree (reads block.number when creating checkpoint) // harnesss functions - ckptFromBlock(address, uint32) returns (uint32) envfree - ckptVotes(address, uint32) returns (uint224) envfree - unsafeNumCheckpoints(address) returns (uint256) envfree - mint(address, uint256) // not envfree (reads block.number when creating checkpoint) - burn(address, uint256) // not envfree (reads block.number when creating checkpoint) + ckptFromBlock(address, uint32) returns (uint32) envfree + ckptVotes(address, uint32) returns (uint224) envfree + unsafeNumCheckpoints(address) returns (uint256) envfree // solidity generated getters - _delegates(address) returns (address) envfree + _delegates(address) returns (address) envfree } - - - - - - - - - - - - - - - // gets the most recent votes for a user ghost userVotes(address) returns uint224 { init_state axiom forall address a. userVotes(a) == 0; @@ -91,28 +74,14 @@ invariant votes_solvency() { preserved with(env e) { require forall address account. numCheckpoints(account) < 1000000; - } preserved burn(address a, uint256 amount) with(env e) { + } preserved _burn(address a, uint256 amount) with(env e) { require _delegates(0) == 0; - require forall address a2. (_delegates(a) != _delegates(a2)) && (balanceOf(e, _delegates(a)) + balanceOf(e, _delegates(a2)) <= totalVotes()); - require balanceOf(e, _delegates(a)) < totalVotes(); + require forall address a2. (_delegates(a) != _delegates(a2)) && (balanceOf(_delegates(a)) + balanceOf(_delegates(a2)) <= totalVotes()); + require balanceOf(_delegates(a)) < totalVotes(); require amount < 100000; } } -// for some checkpoint, the fromBlock is less than the current block number -invariant blockNum_constrains_fromBlock(address account, uint32 index, env e) - ckptFromBlock(account, index) < e.block.number - filtered { f -> !f.isView } -{ - preserved { - require index < numCheckpoints(account); - } -} - -// numCheckpoints are less than maxInt -invariant maxInt_constrains_numBlocks(address account) - numCheckpoints(account) < 4294967295 // 2^32 - // can't have more checkpoints for a given account than the last from block invariant fromBlock_constrains_numBlocks(address account) numCheckpoints(account) <= ckptFromBlock(account, numCheckpoints(account) - 1) @@ -211,7 +180,7 @@ rule delegatee_receives_votes() { require delegates(delegator) != delegatee; require delegatee != 0x0; - uint256 delegator_bal = balanceOf(e, delegator); + uint256 delegator_bal = balanceOf(delegator); uint256 votes_= getVotes(delegatee); _delegate(e, delegator, delegatee); @@ -232,7 +201,7 @@ rule previous_delegatee_votes_removed() { require delegates(delegator) == third; require numCheckpoints(third) < 1000000; - uint256 delegator_bal = balanceOf(e, delegator); + uint256 delegator_bal = balanceOf(delegator); uint256 votes_ = getVotes(third); _delegate(e, delegator, delegatee); @@ -268,7 +237,7 @@ rule delegate_no_frontrunning(method f) { f(e, args); - uint256 delegator_bal = balanceOf(e, delegator); + uint256 delegator_bal = balanceOf(delegator); uint256 delegatee_votes_ = getVotes(delegatee); uint256 third_votes_ = getVotes(third); uint256 other_votes_ = getVotes(other); @@ -303,13 +272,9 @@ rule onMint() { uint224 totalVotesBefore = totalVotes(); uint256 totalSupplyBefore = totalSupply(); - mint(e, account, amount); - - uint224 totalVotesAfter = totalVotes(); - uint256 totalSupplyAfter = totalSupply(); + _mint(e, account, amount); assert totalVotes() == totalVotesBefore, "totalVotes decreased"; - assert totalSupplyAfter == totalSupplyBefore + amount, "totalSupply not increased properly"; assert getPastTotalSupply(e, fromBlock) == totalSupplyBefore , "previous total supply not saved properly"; } @@ -323,12 +288,8 @@ rule onBurn() { uint224 totalVotesBefore = totalVotes(); uint256 totalSupplyBefore = totalSupply(); - burn(e, account, amount); - - uint224 totalVotesAfter = totalVotes(); - uint256 totalSupplyAfter = totalSupply(); + _burn(e, account, amount); assert totalVotes() == totalVotesBefore, "totalVotes decreased"; - assert totalSupplyAfter == totalSupplyBefore - amount, "totalSupply not decreased properly"; assert getPastTotalSupply(e, fromBlock) == totalSupplyBefore , "previous total supply not saved properly"; } diff --git a/certora/specs/ERC20Wrapper.spec b/certora/specs/ERC20Wrapper.spec index 0e44026cc..a7da353ed 100644 --- a/certora/specs/ERC20Wrapper.spec +++ b/certora/specs/ERC20Wrapper.spec @@ -1,13 +1,12 @@ import "erc20.spec" methods { - underlying() returns(address) envfree - underlyingTotalSupply() returns(uint256) envfree + underlying() returns(address) envfree + underlyingTotalSupply() returns(uint256) envfree underlyingBalanceOf(address) returns(uint256) envfree - depositFor(address, uint256) returns(bool) withdrawTo(address, uint256) returns(bool) - _recover(address) returns(uint256) + _recover(address) returns(uint256) } /////////////////////////////////////////////////////////////////////////////////////////////////////////////////////// @@ -16,20 +15,20 @@ methods { // totalsupply of wrapped should be less than or equal to underlying (assuming no external transfer) - solvency invariant whatAboutTotal(env e) - totalSupply(e) <= underlyingTotalSupply() + totalSupply() <= underlyingTotalSupply() filtered { f -> f.selector != certorafallback_0().selector && !f.isView } { preserved { require underlyingBalanceOf(currentContract) <= underlyingTotalSupply(); } - preserved depositFor(address account, uint256 amount) with (env e2){ - require totalSupply(e) + amount <= underlyingTotalSupply(); + preserved depositFor(address account, uint256 amount) with (env e2) { + require totalSupply() + amount <= underlyingTotalSupply(); } } // totalsupply of wrapped should be less than or equal to the underlying balanceOf contract (assuming no external transfer) - solvency invariant underTotalAndContractBalanceOfCorrelation(env e) - totalSupply(e) <= underlyingBalanceOf(currentContract) + totalSupply() <= underlyingBalanceOf(currentContract) { preserved with (env e2) { require underlying() != currentContract; @@ -50,13 +49,13 @@ rule depositForSpecBasic(env e) { require e.msg.sender != currentContract; require underlying() != currentContract; - uint256 wrapperTotalBefore = totalSupply(e); + uint256 wrapperTotalBefore = totalSupply(); uint256 underlyingTotalBefore = underlyingTotalSupply(); uint256 underlyingThisBalanceBefore = underlyingBalanceOf(currentContract); depositFor(e, account, amount); - uint256 wrapperTotalAfter = totalSupply(e); + uint256 wrapperTotalAfter = totalSupply(); uint256 underlyingTotalAfter = underlyingTotalSupply(); uint256 underlyingThisBalanceAfter = underlyingBalanceOf(currentContract); @@ -72,13 +71,13 @@ rule depositForSpecWrapper(env e) { require underlying() != currentContract; - uint256 wrapperUserBalanceBefore = balanceOf(e, account); - uint256 wrapperSenderBalanceBefore = balanceOf(e, e.msg.sender); + uint256 wrapperUserBalanceBefore = balanceOf(account); + uint256 wrapperSenderBalanceBefore = balanceOf(e.msg.sender); depositFor(e, account, amount); - uint256 wrapperUserBalanceAfter = balanceOf(e, account); - uint256 wrapperSenderBalanceAfter = balanceOf(e, e.msg.sender); + uint256 wrapperUserBalanceAfter = balanceOf(account); + uint256 wrapperSenderBalanceAfter = balanceOf(e.msg.sender); assert account == e.msg.sender => wrapperUserBalanceBefore == wrapperSenderBalanceBefore && wrapperUserBalanceAfter == wrapperSenderBalanceAfter @@ -129,12 +128,12 @@ rule withdrawToSpecBasic(env e) { require underlying() != currentContract; - uint256 wrapperTotalBefore = totalSupply(e); + uint256 wrapperTotalBefore = totalSupply(); uint256 underlyingTotalBefore = underlyingTotalSupply(); withdrawTo(e, account, amount); - uint256 wrapperTotalAfter = totalSupply(e); + uint256 wrapperTotalAfter = totalSupply(); uint256 underlyingTotalAfter = underlyingTotalSupply(); assert wrapperTotalBefore == wrapperTotalAfter + amount, "wrapper total wrong update"; @@ -147,13 +146,13 @@ rule withdrawToSpecWrapper(env e) { require underlying() != currentContract; - uint256 wrapperUserBalanceBefore = balanceOf(e, account); - uint256 wrapperSenderBalanceBefore = balanceOf(e, e.msg.sender); + uint256 wrapperUserBalanceBefore = balanceOf(account); + uint256 wrapperSenderBalanceBefore = balanceOf(e.msg.sender); withdrawTo(e, account, amount); - uint256 wrapperUserBalanceAfter = balanceOf(e, account); - uint256 wrapperSenderBalanceAfter = balanceOf(e, e.msg.sender); + uint256 wrapperUserBalanceAfter = balanceOf(account); + uint256 wrapperSenderBalanceAfter = balanceOf(e.msg.sender); assert account == e.msg.sender => wrapperUserBalanceBefore == wrapperSenderBalanceBefore && wrapperUserBalanceAfter == wrapperSenderBalanceAfter @@ -204,18 +203,18 @@ rule recoverSpec(env e) { address account; uint256 amount; - uint256 wrapperTotalBefore = totalSupply(e); - uint256 wrapperUserBalanceBefore = balanceOf(e, account); - uint256 wrapperSenderBalanceBefore = balanceOf(e, e.msg.sender); + uint256 wrapperTotalBefore = totalSupply(); + uint256 wrapperUserBalanceBefore = balanceOf(account); + uint256 wrapperSenderBalanceBefore = balanceOf(e.msg.sender); uint256 underlyingThisBalanceBefore = underlyingBalanceOf(currentContract); mathint value = underlyingThisBalanceBefore - wrapperTotalBefore; _recover(e, account); - uint256 wrapperTotalAfter = totalSupply(e); - uint256 wrapperUserBalanceAfter = balanceOf(e, account); - uint256 wrapperSenderBalanceAfter = balanceOf(e, e.msg.sender); + uint256 wrapperTotalAfter = totalSupply(); + uint256 wrapperUserBalanceAfter = balanceOf(account); + uint256 wrapperSenderBalanceAfter = balanceOf(e.msg.sender); assert wrapperTotalBefore == wrapperTotalAfter - value, "wrapper total wrong update"; diff --git a/certora/specs/GovernorBase.spec b/certora/specs/GovernorBase.spec index 583cb6288..c0fce61b2 100644 --- a/certora/specs/GovernorBase.spec +++ b/certora/specs/GovernorBase.spec @@ -38,7 +38,7 @@ methods { // proposal was created - relation proved in noStartBeforeCreation -definition proposalCreated(uint256 pId) returns bool = +definition proposalCreated(uint256 pId) returns bool = proposalSnapshot(pId) > 0 && proposalDeadline(pId) > 0; @@ -160,7 +160,7 @@ rule executionOnlyIfQuoromReachedAndVoteSucceeded(uint256 pId, env e, method f){ bool isExecutedBefore = isExecuted(pId); bool quorumReachedBefore = quorumReached(e, pId); bool voteSucceededBefore = voteSucceeded(pId); - + calldataarg args; f(e, args); @@ -289,7 +289,9 @@ rule allFunctionsRevertIfExecuted(method f) filtered { f -> && f.selector != queue(address[],uint256[],bytes[],bytes32).selector && f.selector != relay(address,uint256,bytes).selector && f.selector != 0xb9a61961 // __acceptAdmin() - && f.selector != setLateQuorumVoteExtension(uint64).selector + && f.selector != onERC721Received(address,address,uint256,bytes).selector + && f.selector != onERC1155Received(address,address,uint256,uint256,bytes).selector + && f.selector != onERC1155BatchReceived(address,address,uint256[],uint256[],bytes).selector } { env e; calldataarg args; uint256 pId; @@ -312,7 +314,9 @@ rule allFunctionsRevertIfCanceled(method f) filtered { && f.selector != queue(address[],uint256[],bytes[],bytes32).selector && f.selector != relay(address,uint256,bytes).selector && f.selector != 0xb9a61961 // __acceptAdmin() - && f.selector != setLateQuorumVoteExtension(uint64).selector + && f.selector != onERC721Received(address,address,uint256,bytes).selector + && f.selector != onERC1155Received(address,address,uint256,uint256,bytes).selector + && f.selector != onERC1155BatchReceived(address,address,uint256[],uint256[],bytes).selector } { env e; calldataarg args; uint256 pId; diff --git a/certora/specs/GovernorPreventLateQuorum.spec b/certora/specs/GovernorPreventLateQuorum.spec index 861e57ae8..baf932e19 100644 --- a/certora/specs/GovernorPreventLateQuorum.spec +++ b/certora/specs/GovernorPreventLateQuorum.spec @@ -1,7 +1,5 @@ import "GovernorCountingSimple.spec" -using ERC721VotesHarness as erc721votes - methods { quorumDenominator() returns uint256 envfree votingPeriod() returns uint256 envfree @@ -15,13 +13,13 @@ methods { getAgainstVotes(uint256) returns uint256 envfree getAbstainVotes(uint256) returns uint256 envfree getForVotes(uint256) returns uint256 envfree - + // more robust check than f.selector == _castVote(...).selector - latestCastVoteCall() returns uint256 envfree + latestCastVoteCall() returns uint256 envfree // timelock dispatch getMinDelay() returns uint256 => DISPATCHER(true) - + hashOperationBatch(address[], uint256[], bytes[], bytes32, bytes32) => DISPATCHER(true) executeBatch(address[], uint256[], bytes[], bytes32, bytes32) => CONSTANT scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256) => CONSTANT @@ -56,16 +54,16 @@ function helperFunctionsWithRevertOnlyCastVote(uint256 proposalId, method f, env ////////////////////////////////////////////////////////////////////////////// // proposal deadline can be extended (but isn't) -definition deadlineExtendable(env e, uint256 pId) returns bool = +definition deadlineExtendable(env e, uint256 pId) returns bool = getExtendedDeadlineIsUnset(pId) // deadline == 0 && !quorumReached(e, pId); // proposal deadline has been extended -definition deadlineExtended(env e, uint256 pId) returns bool = +definition deadlineExtended(env e, uint256 pId) returns bool = getExtendedDeadlineIsStarted(pId) // deadline > 0 && quorumReached(e, pId); -definition proposalNotCreated(env e, uint256 pId) returns bool = +definition proposalNotCreated(env e, uint256 pId) returns bool = proposalSnapshot(pId) == 0 && proposalDeadline(pId) == 0 && getExtendedDeadlineIsUnset(pId) @@ -83,7 +81,7 @@ definition proposalNotCreated(env e, uint256 pId) returns bool = * I1: If a proposal has reached quorum then the proposal snapshot (start block.number) must be non-zero * INVARIANT NOT PASSING // fails for updateQuorumNumerator and in the initial state when voting token total supply is 0 (causes quoromReached to return true) * ADVANCED SANITY NOT RAN - */ + */ invariant quorumReachedEffect(env e, uint256 pId) quorumReached(e, pId) => proposalCreated(pId) // bug: 0 supply 0 votes => quorumReached // filtered { f -> f.selector != updateQuorumNumerator(uint256).selector } // * fails for this function @@ -100,9 +98,9 @@ invariant proposalNotCreatedEffects(env e, uint256 pId) /* * I3: A created propsal must be in state deadlineExtendable or deadlineExtended. * INVARIANT NOT PASSING // fails for updateQuorumNumerator and in the initial state when voting token total supply is 0 (causes quoromReached to return true) - * ADVANCED SANITY NOT RAN + * ADVANCED SANITY NOT RAN */ -invariant proposalInOneState(env e, uint256 pId) +invariant proposalInOneState(env e, uint256 pId) proposalNotCreated(e, pId) || deadlineExtendable(e, pId) || deadlineExtended(e, pId) // filtered { f -> f.selector != updateQuorumNumerator(uint256).selector } // * fails for this function { preserved { requireInvariant proposalNotCreatedEffects(e, pId); }} @@ -118,17 +116,17 @@ invariant proposalInOneState(env e, uint256 pId) /* * R1: If deadline increases then we are in deadlineExtended state and castVote was called. * RULE PASSING - * ADVANCED SANITY PASSING - */ + * ADVANCED SANITY PASSING + */ rule deadlineChangeEffects(method f) filtered {f -> !f.isView} { env e; calldataarg args; uint256 pId; requireInvariant quorumReachedEffect(e, pId); - + uint256 deadlineBefore = proposalDeadline(pId); f(e, args); uint256 deadlineAfter = proposalDeadline(pId); - + assert(deadlineAfter > deadlineBefore => latestCastVoteCall() == e.block.number && deadlineExtended(e, pId)); } @@ -136,9 +134,9 @@ rule deadlineChangeEffects(method f) filtered {f -> !f.isView} { /* * R2: A proposal can't leave deadlineExtended state. * RULE PASSING* - * ADVANCED SANITY PASSING - */ -rule deadlineCantBeUnextended(method f) + * ADVANCED SANITY PASSING + */ +rule deadlineCantBeUnextended(method f) filtered { f -> !f.isView // && f.selector != updateQuorumNumerator(uint256).selector // * fails for this function @@ -147,9 +145,9 @@ rule deadlineCantBeUnextended(method f) require(deadlineExtended(e, pId)); requireInvariant quorumReachedEffect(e, pId); - + f(e, args); - + assert(deadlineExtended(e, pId)); } @@ -157,18 +155,18 @@ rule deadlineCantBeUnextended(method f) /* * R3: A proposal's deadline can't change in deadlineExtended state. * RULE PASSING - * ADVANCED SANITY PASSING - */ + * ADVANCED SANITY PASSING + */ rule canExtendDeadlineOnce(method f) filtered {f -> !f.isView} { env e; calldataarg args; uint256 pId; require(deadlineExtended(e, pId)); - requireInvariant quorumReachedEffect(e, pId); - + requireInvariant quorumReachedEffect(e, pId); + uint256 deadlineBefore = proposalDeadline(pId); f(e, args); uint256 deadlineAfter = proposalDeadline(pId); - + assert(deadlineBefore == deadlineAfter, "deadline can not be extended twice"); } @@ -187,7 +185,7 @@ rule hasVotedCorrelationNonzero(uint256 pId, method f, env e) filtered {f -> !f. address acc = e.msg.sender; require(getVotes(e, acc, proposalSnapshot(pId)) > 0); // assuming voter has non-zero voting power - + uint256 againstBefore = votesAgainst(); uint256 forBefore = votesFor(); uint256 abstainBefore = votesAbstain(); @@ -199,16 +197,16 @@ rule hasVotedCorrelationNonzero(uint256 pId, method f, env e) filtered {f -> !f. uint256 againstAfter = votesAgainst(); uint256 forAfter = votesFor(); uint256 abstainAfter = votesAbstain(); - + bool hasVotedAfter = hasVoted(e, pId, acc); // want all vote categories to not decrease and at least one category to increase - assert - (!hasVotedBefore && hasVotedAfter) => - (againstBefore <= againstAfter && forBefore <= forAfter && abstainBefore <= abstainAfter), + assert + (!hasVotedBefore && hasVotedAfter) => + (againstBefore <= againstAfter && forBefore <= forAfter && abstainBefore <= abstainAfter), "after a vote is cast, the number of votes for each category must not decrease"; // currently vacous but keeping for CI tests - assert - (!hasVotedBefore && hasVotedAfter) => + assert + (!hasVotedBefore && hasVotedAfter) => (againstBefore < againstAfter || forBefore < forAfter || abstainBefore < abstainAfter), "after a vote is cast, the number of votes of at least one category must increase"; } @@ -220,9 +218,9 @@ rule hasVotedCorrelationNonzero(uint256 pId, method f, env e) filtered {f -> !f. * --ADVANCED SANITY PASSING vacuous but keeping */ rule againstVotesDontCount(method f) filtered {f -> !f.isView} { - env e; calldataarg args; uint256 pId; + env e; calldataarg args; uint256 pId; address acc = e.msg.sender; - + bool quorumBefore = quorumReached(e, pId); uint256 againstBefore = votesAgainst(); @@ -231,19 +229,19 @@ rule againstVotesDontCount(method f) filtered {f -> !f.isView} { bool quorumAfter = quorumReached(e, pId); uint256 againstAfter = votesAgainst(); - assert (againstBefore < againstAfter) => quorumBefore == quorumAfter, "quorum must not be reached with an against vote"; + assert (againstBefore < againstAfter) => quorumBefore == quorumAfter, "quorum must not be reached with an against vote"; } /* * R6: Deadline can only be extended from a `deadlineExtendible` state with quorum being reached with <= `lateQuorumVoteExtension` time left to vote * RULE PASSING - * ADVANCED SANITY PASSING + * ADVANCED SANITY PASSING */ rule deadlineExtenededIfQuorumReached(method f) filtered {f -> !f.isView} { env e; calldataarg args; uint256 pId; requireInvariant proposalInOneState(e, pId); - requireInvariant quorumReachedEffect(e, pId); + requireInvariant quorumReachedEffect(e, pId); requireInvariant proposalNotCreatedEffects(e, pId); bool wasDeadlineExtendable = deadlineExtendable(e, pId); @@ -251,7 +249,7 @@ rule deadlineExtenededIfQuorumReached(method f) filtered {f -> !f.isView} { uint256 deadlineBefore = proposalDeadline(pId); f(e, args); uint256 deadlineAfter = proposalDeadline(pId); - + assert deadlineAfter > deadlineBefore => wasDeadlineExtendable, "deadline must have been extendable for the deadline to be extended"; assert deadlineAfter > deadlineBefore => deadlineBefore - e.block.number <= extension, "deadline extension should not be used"; } @@ -259,18 +257,18 @@ rule deadlineExtenededIfQuorumReached(method f) filtered {f -> !f.isView} { /* * R7: `extendedDeadlineField` is set iff `_castVote` is called and quroum is reached. * RULE PASSING - * ADVANCED SANITY PASSING + * ADVANCED SANITY PASSING */ rule extendedDeadlineValueSetIfQuorumReached(method f) filtered {f -> !f.isView} { env e; calldataarg args; uint256 pId; requireInvariant proposalInOneState(e, pId); - + bool extendedBefore = deadlineExtended(e, pId); f(e, args); bool extendedAfter = deadlineExtended(e, pId); uint256 extDeadline = getExtendedDeadline(pId); - + assert( !extendedBefore && extendedAfter => extDeadline == e.block.number + lateQuorumVoteExtension(), @@ -295,4 +293,3 @@ rule deadlineNeverReduced(method f) filtered {f -> !f.isView} { assert(deadlineAfter >= deadlineBefore); } -