diff --git a/certora/diff/governance_Governor.sol.patch b/certora/diff/governance_Governor.sol.patch new file mode 100644 index 00000000000..7bdca832ee9 --- /dev/null +++ b/certora/diff/governance_Governor.sol.patch @@ -0,0 +1,24 @@ +--- governance/Governor.sol 2023-05-03 09:17:45.566699712 +0200 ++++ governance/Governor.sol 2023-05-04 15:18:42.667741565 +0200 +@@ -224,6 +224,21 @@ + return _proposals[proposalId].proposer; + } + ++ // FV ++ function _isExecuted(uint256 proposalId) internal view returns (bool) { ++ return _proposals[proposalId].executed; ++ } ++ ++ // FV ++ function _isCanceled(uint256 proposalId) internal view returns (bool) { ++ return _proposals[proposalId].canceled; ++ } ++ ++ // FV ++ function _governanceCallLength() internal view returns (uint256) { ++ return _governanceCall.length(); ++ } ++ + /** + * @dev Amount of votes already cast passes the threshold limit. + */ diff --git a/certora/diff/governance_extensions_GovernorPreventLateQuorum.sol.patch b/certora/diff/governance_extensions_GovernorPreventLateQuorum.sol.patch new file mode 100644 index 00000000000..1d387b37684 --- /dev/null +++ b/certora/diff/governance_extensions_GovernorPreventLateQuorum.sol.patch @@ -0,0 +1,14 @@ +--- governance/extensions/GovernorPreventLateQuorum.sol 2023-05-03 09:17:45.566699712 +0200 ++++ governance/extensions/GovernorPreventLateQuorum.sol 2023-05-04 15:18:42.657742113 +0200 +@@ -82,6 +82,11 @@ + return _voteExtension; + } + ++ // FV ++ function _getExtendedDeadline(uint256 proposalId) internal view returns (uint64) { ++ return _extendedDeadlines[proposalId]; ++ } ++ + /** + * @dev Changes the {lateQuorumVoteExtension}. This operation can only be performed by the governance executor, + * generally through a governance proposal. diff --git a/certora/diff/governance_extensions_GovernorTimelockControl.sol.patch b/certora/diff/governance_extensions_GovernorTimelockControl.sol.patch new file mode 100644 index 00000000000..7213188a642 --- /dev/null +++ b/certora/diff/governance_extensions_GovernorTimelockControl.sol.patch @@ -0,0 +1,33 @@ +--- governance/extensions/GovernorTimelockControl.sol 2023-05-04 11:44:55.587737817 +0200 ++++ governance/extensions/GovernorTimelockControl.sol 2023-05-04 15:18:42.661075263 +0200 +@@ -24,7 +24,7 @@ + * _Available since v4.3._ + */ + abstract contract GovernorTimelockControl is IGovernorTimelock, Governor { +- TimelockController private _timelock; ++ TimelockController public _timelock; // FV: public for link + mapping(uint256 => bytes32) private _timelockIds; + + /** +@@ -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. + */ +@@ -163,4 +168,9 @@ + emit TimelockChange(address(_timelock), address(newTimelock)); + _timelock = newTimelock; + } ++ ++ // FV ++ function timelockId(uint256 proposalId) public view returns (bytes32) { ++ return _timelockIds[proposalId]; ++ } + } diff --git a/certora/diff/governance_extensions_GovernorVotesQuorumFraction.sol.patch b/certora/diff/governance_extensions_GovernorVotesQuorumFraction.sol.patch new file mode 100644 index 00000000000..bdf9d1b114e --- /dev/null +++ b/certora/diff/governance_extensions_GovernorVotesQuorumFraction.sol.patch @@ -0,0 +1,14 @@ +--- governance/extensions/GovernorVotesQuorumFraction.sol 2023-05-03 09:17:45.570033048 +0200 ++++ governance/extensions/GovernorVotesQuorumFraction.sol 2023-05-04 15:18:42.664408414 +0200 +@@ -61,6 +61,11 @@ + return _quorumNumeratorHistory.upperLookupRecent(SafeCast.toUint32(timepoint)); + } + ++ // FV ++ function quorumNumeratorLength() public view returns (uint256) { ++ return _quorumNumeratorHistory._checkpoints.length; ++ } ++ + /** + * @dev Returns the quorum denominator. Defaults to 100, but may be overridden. + */ diff --git a/certora/diff/token_ERC721_ERC721.sol.patch b/certora/diff/token_ERC721_ERC721.sol.patch index c3eae357a4c..0c53650aad6 100644 --- a/certora/diff/token_ERC721_ERC721.sol.patch +++ b/certora/diff/token_ERC721_ERC721.sol.patch @@ -1,5 +1,5 @@ ---- token/ERC721/ERC721.sol 2023-03-07 10:48:47.736822221 +0100 -+++ token/ERC721/ERC721.sol 2023-03-09 19:49:39.669338673 +0100 +--- token/ERC721/ERC721.sol 2023-04-27 22:16:54.864065073 +0200 ++++ token/ERC721/ERC721.sol 2023-05-04 15:18:42.671074716 +0200 @@ -199,6 +199,11 @@ return _owners[tokenId]; } diff --git a/certora/harnesses/AccessControlHarness.sol b/certora/harnesses/AccessControlHarness.sol index 0cb1e55d41c..b869bd7dcb6 100644 --- a/certora/harnesses/AccessControlHarness.sol +++ b/certora/harnesses/AccessControlHarness.sol @@ -1,5 +1,4 @@ // SPDX-License-Identifier: MIT - pragma solidity ^0.8.0; import "../patched/access/AccessControl.sol"; diff --git a/certora/harnesses/ERC20FlashMintHarness.sol b/certora/harnesses/ERC20FlashMintHarness.sol index 119eb4768fb..39af9371f93 100644 --- a/certora/harnesses/ERC20FlashMintHarness.sol +++ b/certora/harnesses/ERC20FlashMintHarness.sol @@ -1,5 +1,4 @@ // SPDX-License-Identifier: MIT - pragma solidity ^0.8.0; import "../patched/token/ERC20/ERC20.sol"; diff --git a/certora/harnesses/ERC20PermitHarness.sol b/certora/harnesses/ERC20PermitHarness.sol index dd0aacae2fa..effae5f9b25 100644 --- a/certora/harnesses/ERC20PermitHarness.sol +++ b/certora/harnesses/ERC20PermitHarness.sol @@ -1,5 +1,4 @@ // SPDX-License-Identifier: MIT - pragma solidity ^0.8.0; import "../patched/token/ERC20/extensions/ERC20Permit.sol"; diff --git a/certora/harnesses/ERC20VotesBlocknumberHarness.sol b/certora/harnesses/ERC20VotesBlocknumberHarness.sol new file mode 100644 index 00000000000..f00e3ec057d --- /dev/null +++ b/certora/harnesses/ERC20VotesBlocknumberHarness.sol @@ -0,0 +1,29 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.0; + +import "../patched/token/ERC20/extensions/ERC20Votes.sol"; + +contract ERC20VotesBlocknumberHarness is ERC20Votes { + constructor(string memory name, string memory symbol) ERC20(name, symbol) ERC20Permit(name) {} + + function mint(address account, uint256 amount) external { + _mint(account, amount); + } + + function burn(address account, uint256 amount) external { + _burn(account, amount); + } + + // inspection + function ckptFromBlock(address account, uint32 pos) public view returns (uint32) { + return checkpoints(account, pos).fromBlock; + } + + function ckptVotes(address account, uint32 pos) public view returns (uint224) { + return checkpoints(account, pos).votes; + } + + function maxSupply() public view returns (uint224) { + return _maxSupply(); + } +} diff --git a/certora/harnesses/ERC20VotesTimestampHarness.sol b/certora/harnesses/ERC20VotesTimestampHarness.sol new file mode 100644 index 00000000000..e8b96cf3fea --- /dev/null +++ b/certora/harnesses/ERC20VotesTimestampHarness.sol @@ -0,0 +1,39 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.0; + +import "../patched/token/ERC20/extensions/ERC20Votes.sol"; + +contract ERC20VotesTimestampHarness is ERC20Votes { + constructor(string memory name, string memory symbol) ERC20(name, symbol) ERC20Permit(name) {} + + function mint(address account, uint256 amount) external { + _mint(account, amount); + } + + function burn(address account, uint256 amount) external { + _burn(account, amount); + } + + // inspection + function ckptFromBlock(address account, uint32 pos) public view returns (uint32) { + return checkpoints(account, pos).fromBlock; + } + + function ckptVotes(address account, uint32 pos) public view returns (uint224) { + return checkpoints(account, pos).votes; + } + + function maxSupply() public view returns (uint224) { + return _maxSupply(); + } + + // clock + function clock() public view override returns (uint48) { + return uint48(block.timestamp); + } + + // solhint-disable-next-line func-name-mixedcase + function CLOCK_MODE() public view virtual override returns (string memory) { + return "mode=timestamp"; + } +} diff --git a/certora/harnesses/ERC20WrapperHarness.sol b/certora/harnesses/ERC20WrapperHarness.sol index 50a96cc170a..2ff93e749a1 100644 --- a/certora/harnesses/ERC20WrapperHarness.sol +++ b/certora/harnesses/ERC20WrapperHarness.sol @@ -1,5 +1,4 @@ // SPDX-License-Identifier: MIT - pragma solidity ^0.8.0; import "../patched/token/ERC20/extensions/ERC20Wrapper.sol"; diff --git a/certora/harnesses/ERC3156FlashBorrowerHarness.sol b/certora/harnesses/ERC3156FlashBorrowerHarness.sol index 0ad29a16e24..c9cb829aaa3 100644 --- a/certora/harnesses/ERC3156FlashBorrowerHarness.sol +++ b/certora/harnesses/ERC3156FlashBorrowerHarness.sol @@ -1,9 +1,8 @@ // SPDX-License-Identifier: MIT +pragma solidity ^0.8.0; import "../patched/interfaces/IERC3156FlashBorrower.sol"; -pragma solidity ^0.8.0; - contract ERC3156FlashBorrowerHarness is IERC3156FlashBorrower { bytes32 somethingToReturn; diff --git a/certora/harnesses/GovernorHarness.sol b/certora/harnesses/GovernorHarness.sol new file mode 100644 index 00000000000..4d26775db2f --- /dev/null +++ b/certora/harnesses/GovernorHarness.sol @@ -0,0 +1,153 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.2; + +import "../patched/governance/Governor.sol"; +import "../patched/governance/extensions/GovernorCountingSimple.sol"; +import "../patched/governance/extensions/GovernorTimelockControl.sol"; +import "../patched/governance/extensions/GovernorVotes.sol"; +import "../patched/governance/extensions/GovernorVotesQuorumFraction.sol"; +import "../patched/token/ERC20/extensions/ERC20Votes.sol"; + +contract GovernorHarness is + Governor, + GovernorCountingSimple, + GovernorTimelockControl, + GovernorVotes, + GovernorVotesQuorumFraction +{ + constructor(IVotes _token, TimelockController _timelock, uint256 _quorumNumeratorValue) + Governor("Harness") + GovernorTimelockControl(_timelock) + GovernorVotes(_token) + GovernorVotesQuorumFraction(_quorumNumeratorValue) + {} + + // Harness from Votes + function token_getPastTotalSupply(uint256 blockNumber) public view returns(uint256) { + return token.getPastTotalSupply(blockNumber); + } + + function token_getPastVotes(address account, uint256 blockNumber) public view returns(uint256) { + return token.getPastVotes(account, blockNumber); + } + + function token_clock() public view returns (uint48) { + return token.clock(); + } + + function token_CLOCK_MODE() public view returns (string memory) { + return token.CLOCK_MODE(); + } + + // Harness from Governor + function hashProposal(address[] memory targets,uint256[] memory values,bytes[] memory calldatas,string memory description) public pure returns (uint256) { + return hashProposal(targets, values, calldatas, keccak256(bytes(description))); + } + + function getExecutor() public view returns (address) { + return _executor(); + } + + function quorumReached(uint256 proposalId) public view returns (bool) { + return _quorumReached(proposalId); + } + + function voteSucceeded(uint256 proposalId) public view returns (bool) { + return _voteSucceeded(proposalId); + } + + function isExecuted(uint256 proposalId) public view returns (bool) { + return _isExecuted(proposalId); + } + + function isCanceled(uint256 proposalId) public view returns (bool) { + return _isCanceled(proposalId); + } + + function isQueued(uint256 proposalId) public view returns (bool) { + return _proposalQueueId(proposalId) != bytes32(0); + } + + function governanceCallLength() public view returns (uint256) { + return _governanceCallLength(); + } + + // Harness from GovernorCountingSimple + function getAgainstVotes(uint256 proposalId) public view returns (uint256) { + (uint256 againstVotes,,) = proposalVotes(proposalId); + return againstVotes; + } + + function getForVotes(uint256 proposalId) public view returns (uint256) { + (,uint256 forVotes,) = proposalVotes(proposalId); + return forVotes; + } + + function getAbstainVotes(uint256 proposalId) public view returns (uint256) { + (,,uint256 abstainVotes) = proposalVotes(proposalId); + return abstainVotes; + } + + // 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/GovernorPreventLateHarness.sol b/certora/harnesses/GovernorPreventLateHarness.sol new file mode 100644 index 00000000000..1adb8eb9080 --- /dev/null +++ b/certora/harnesses/GovernorPreventLateHarness.sol @@ -0,0 +1,176 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.2; + +import "../patched/governance/Governor.sol"; +import "../patched/governance/extensions/GovernorCountingSimple.sol"; +import "../patched/governance/extensions/GovernorPreventLateQuorum.sol"; +import "../patched/governance/extensions/GovernorTimelockControl.sol"; +import "../patched/governance/extensions/GovernorVotes.sol"; +import "../patched/governance/extensions/GovernorVotesQuorumFraction.sol"; +import "../patched/token/ERC20/extensions/ERC20Votes.sol"; + +contract GovernorPreventLateHarness is + Governor, + GovernorCountingSimple, + GovernorPreventLateQuorum, + GovernorTimelockControl, + GovernorVotes, + GovernorVotesQuorumFraction +{ + constructor(IVotes _token, TimelockController _timelock, uint256 _quorumNumeratorValue, uint64 _initialVoteExtension) + Governor("Harness") + GovernorPreventLateQuorum(_initialVoteExtension) + GovernorTimelockControl(_timelock) + GovernorVotes(_token) + GovernorVotesQuorumFraction(_quorumNumeratorValue) + {} + + // Harness from Votes + function token_getPastTotalSupply(uint256 blockNumber) public view returns(uint256) { + return token.getPastTotalSupply(blockNumber); + } + + function token_getPastVotes(address account, uint256 blockNumber) public view returns(uint256) { + return token.getPastVotes(account, blockNumber); + } + + function token_clock() public view returns (uint48) { + return token.clock(); + } + + function token_CLOCK_MODE() public view returns (string memory) { + return token.CLOCK_MODE(); + } + + // Harness from Governor + function hashProposal(address[] memory targets,uint256[] memory values,bytes[] memory calldatas,string memory description) public pure returns (uint256) { + return hashProposal(targets, values, calldatas, keccak256(bytes(description))); + } + + function getExecutor() public view returns (address) { + return _executor(); + } + + function quorumReached(uint256 proposalId) public view returns (bool) { + return _quorumReached(proposalId); + } + + function voteSucceeded(uint256 proposalId) public view returns (bool) { + return _voteSucceeded(proposalId); + } + + function isExecuted(uint256 proposalId) public view returns (bool) { + return _isExecuted(proposalId); + } + + function isCanceled(uint256 proposalId) public view returns (bool) { + return _isCanceled(proposalId); + } + + function isQueued(uint256 proposalId) public view returns (bool) { + return _proposalQueueId(proposalId) != bytes32(0); + } + + function governanceCallLength() public view returns (uint256) { + return _governanceCallLength(); + } + + // Harness from GovernorPreventLateQuorum + function getExtendedDeadline(uint256 proposalId) public view returns (uint64) { + return _getExtendedDeadline(proposalId); + } + + // Harness from GovernorCountingSimple + function getAgainstVotes(uint256 proposalId) public view returns (uint256) { + (uint256 againstVotes,,) = proposalVotes(proposalId); + return againstVotes; + } + + function getForVotes(uint256 proposalId) public view returns (uint256) { + (,uint256 forVotes,) = proposalVotes(proposalId); + return forVotes; + } + + function getAbstainVotes(uint256 proposalId) public view returns (uint256) { + (,,uint256 abstainVotes) = proposalVotes(proposalId); + return abstainVotes; + } + + // 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 proposalDeadline(uint256 proposalId) public view override(IGovernor, Governor, GovernorPreventLateQuorum) returns (uint256) { + return super.proposalDeadline(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 _castVote( + uint256 proposalId, + address account, + uint8 support, + string memory reason, + bytes memory params + ) internal override(Governor, GovernorPreventLateQuorum) returns (uint256) { + return super._castVote(proposalId, account, support, reason, params); + } + + function _executor() internal view override(Governor, GovernorTimelockControl) returns (address) { + return super._executor(); + } + + function supportsInterface(bytes4 interfaceId) + public + view + virtual + override(Governor, GovernorTimelockControl) + returns (bool) + { + return super.supportsInterface(interfaceId); + } +} diff --git a/certora/harnesses/Ownable2StepHarness.sol b/certora/harnesses/Ownable2StepHarness.sol index 4d30e504189..dd53cc6fe4c 100644 --- a/certora/harnesses/Ownable2StepHarness.sol +++ b/certora/harnesses/Ownable2StepHarness.sol @@ -1,5 +1,4 @@ // SPDX-License-Identifier: MIT - pragma solidity ^0.8.0; import "../patched/access/Ownable2Step.sol"; diff --git a/certora/harnesses/OwnableHarness.sol b/certora/harnesses/OwnableHarness.sol index 93cbb4770c2..c9e06d1dc78 100644 --- a/certora/harnesses/OwnableHarness.sol +++ b/certora/harnesses/OwnableHarness.sol @@ -1,5 +1,4 @@ // SPDX-License-Identifier: MIT - pragma solidity ^0.8.0; import "../patched/access/Ownable.sol"; diff --git a/certora/run.js b/certora/run.js index fdee42d2ed4..195d96817c8 100755 --- a/certora/run.js +++ b/certora/run.js @@ -21,7 +21,7 @@ const argv = require('yargs') spec: { alias: 's', type: 'string', - default: __dirname + '/specs.json', + default: __dirname + '/specs.js', }, parallel: { alias: 'p', @@ -59,12 +59,17 @@ if (process.exitCode) { } for (const { spec, contract, files, options = [] } of specs) { - limit(runCertora, spec, contract, files, [...options.flatMap(opt => opt.split(' ')), ...argv.options]); + limit(runCertora, spec, contract, files, [...options, ...argv.options]); } // Run certora, aggregate the output and print it at the end async function runCertora(spec, contract, files, options = []) { - const args = [...files, '--verify', `${contract}:certora/specs/${spec}.spec`, ...options]; + const args = [ + ...files, + '--verify', + `${contract}:certora/specs/${spec}.spec`, + ...options.flatMap(opt => opt.split(' ')), + ]; const child = proc.spawn('certoraRun', args); const stream = new PassThrough(); diff --git a/certora/specs.js b/certora/specs.js new file mode 100644 index 00000000000..67f8fcb9bdf --- /dev/null +++ b/certora/specs.js @@ -0,0 +1,129 @@ +const product = (...arrays) => arrays.reduce((a, b) => a.flatMap(ai => b.map(bi => [ai, bi].flat()))); + +module.exports = [].concat( + // AccessControl + { + spec: 'AccessControl', + contract: 'AccessControlHarness', + files: ['certora/harnesses/AccessControlHarness.sol'], + }, + { + spec: 'AccessControlDefaultAdminRules', + contract: 'AccessControlDefaultAdminRulesHarness', + files: ['certora/harnesses/AccessControlDefaultAdminRulesHarness.sol'], + }, + { + spec: 'Ownable', + contract: 'OwnableHarness', + files: ['certora/harnesses/OwnableHarness.sol'], + }, + { + spec: 'Ownable2Step', + contract: 'Ownable2StepHarness', + files: ['certora/harnesses/Ownable2StepHarness.sol'], + }, + // Tokens + { + spec: 'ERC20', + contract: 'ERC20PermitHarness', + files: ['certora/harnesses/ERC20PermitHarness.sol'], + options: ['--optimistic_loop'], + }, + { + spec: 'ERC20FlashMint', + contract: 'ERC20FlashMintHarness', + files: ['certora/harnesses/ERC20FlashMintHarness.sol', 'certora/harnesses/ERC3156FlashBorrowerHarness.sol'], + options: ['--optimistic_loop'], + }, + { + spec: 'ERC20Wrapper', + contract: 'ERC20WrapperHarness', + files: ['certora/harnesses/ERC20PermitHarness.sol', 'certora/harnesses/ERC20WrapperHarness.sol'], + options: ['--link ERC20WrapperHarness:_underlying=ERC20PermitHarness', '--optimistic_loop'], + }, + { + spec: 'ERC721', + contract: 'ERC721Harness', + files: ['certora/harnesses/ERC721Harness.sol', 'certora/harnesses/ERC721ReceiverHarness.sol'], + options: ['--optimistic_loop'], + }, + // Security + { + spec: 'Pausable', + contract: 'PausableHarness', + files: ['certora/harnesses/PausableHarness.sol'], + }, + // Proxy + { + spec: 'Initializable', + contract: 'InitializableHarness', + files: ['certora/harnesses/InitializableHarness.sol'], + }, + // Structures + { + spec: 'DoubleEndedQueue', + contract: 'DoubleEndedQueueHarness', + files: ['certora/harnesses/DoubleEndedQueueHarness.sol'], + }, + { + spec: 'EnumerableSet', + contract: 'EnumerableSetHarness', + files: ['certora/harnesses/EnumerableSetHarness.sol'], + }, + { + spec: 'EnumerableMap', + contract: 'EnumerableMapHarness', + files: ['certora/harnesses/EnumerableMapHarness.sol'], + }, + // Governance + { + spec: 'TimelockController', + contract: 'TimelockControllerHarness', + files: ['certora/harnesses/TimelockControllerHarness.sol'], + options: ['--optimistic_hashing', '--optimistic_loop'], + }, + // Governor + product( + [ + ...product(['GovernorHarness'], ['GovernorInvariants', 'GovernorBaseRules', 'GovernorChanges', 'GovernorStates']), + ...product(['GovernorPreventLateHarness'], ['GovernorPreventLateQuorum']), + ], + ['ERC20VotesBlocknumberHarness', 'ERC20VotesTimestampHarness'], + ).map(([contract, spec, token]) => ({ + spec, + contract, + files: [ + `certora/harnesses/${contract}.sol`, + `certora/harnesses/${token}.sol`, + `certora/harnesses/TimelockControllerHarness.sol`, + ], + options: [ + `--link ${contract}:token=${token}`, + `--link ${contract}:_timelock=TimelockControllerHarness`, + '--optimistic_hashing', + '--optimistic_loop', + ], + })), + product( + ['GovernorHarness'], + ['GovernorFunctions'], + ['ERC20VotesBlocknumberHarness', 'ERC20VotesTimestampHarness'], + ['castVote', 'execute'], // 'propose', 'queue', 'cancel' // these rules timeout/fail + ).map(([contract, spec, token, fn]) => ({ + spec, + contract, + files: [ + `certora/harnesses/${contract}.sol`, + `certora/harnesses/${token}.sol`, + `certora/harnesses/TimelockControllerHarness.sol`, + ], + options: [ + `--link ${contract}:token=${token}`, + `--link ${contract}:_timelock=TimelockControllerHarness`, + '--optimistic_hashing', + '--optimistic_loop', + '--rules', + ...['liveness', 'effect', 'sideeffect'].map(kind => `${fn}_${kind}`), + ], + })), +); diff --git a/certora/specs.json b/certora/specs.json deleted file mode 100644 index 3e5acb568b8..00000000000 --- a/certora/specs.json +++ /dev/null @@ -1,86 +0,0 @@ -[ - { - "spec": "Pausable", - "contract": "PausableHarness", - "files": ["certora/harnesses/PausableHarness.sol"] - }, - { - "spec": "AccessControl", - "contract": "AccessControlHarness", - "files": ["certora/harnesses/AccessControlHarness.sol"] - }, - { - "spec": "AccessControlDefaultAdminRules", - "contract": "AccessControlDefaultAdminRulesHarness", - "files": ["certora/harnesses/AccessControlDefaultAdminRulesHarness.sol"] - }, - { - "spec": "DoubleEndedQueue", - "contract": "DoubleEndedQueueHarness", - "files": ["certora/harnesses/DoubleEndedQueueHarness.sol"] - }, - { - "spec": "Ownable", - "contract": "OwnableHarness", - "files": ["certora/harnesses/OwnableHarness.sol"] - }, - { - "spec": "Ownable2Step", - "contract": "Ownable2StepHarness", - "files": ["certora/harnesses/Ownable2StepHarness.sol"] - }, - { - "spec": "ERC20", - "contract": "ERC20PermitHarness", - "files": ["certora/harnesses/ERC20PermitHarness.sol"], - "options": ["--optimistic_loop"] - }, - { - "spec": "ERC20FlashMint", - "contract": "ERC20FlashMintHarness", - "files": [ - "certora/harnesses/ERC20FlashMintHarness.sol", - "certora/harnesses/ERC3156FlashBorrowerHarness.sol" - ], - "options": ["--optimistic_loop"] - }, - { - "spec": "ERC20Wrapper", - "contract": "ERC20WrapperHarness", - "files": [ - "certora/harnesses/ERC20PermitHarness.sol", - "certora/harnesses/ERC20WrapperHarness.sol" - ], - "options": [ - "--link ERC20WrapperHarness:_underlying=ERC20PermitHarness", - "--optimistic_loop" - ] - }, - { - "spec": "ERC721", - "contract": "ERC721Harness", - "files": ["certora/harnesses/ERC721Harness.sol", "certora/harnesses/ERC721ReceiverHarness.sol"], - "options": ["--optimistic_loop"] - }, - { - "spec": "Initializable", - "contract": "InitializableHarness", - "files": ["certora/harnesses/InitializableHarness.sol"] - }, - { - "spec": "EnumerableSet", - "contract": "EnumerableSetHarness", - "files": ["certora/harnesses/EnumerableSetHarness.sol"] - }, - { - "spec": "EnumerableMap", - "contract": "EnumerableMapHarness", - "files": ["certora/harnesses/EnumerableMapHarness.sol"] - }, - { - "spec": "TimelockController", - "contract": "TimelockControllerHarness", - "files": ["certora/harnesses/TimelockControllerHarness.sol"], - "options": ["--optimistic_hashing", "--optimistic_loop"] - } -] diff --git a/certora/specs/GovernorBaseRules.spec b/certora/specs/GovernorBaseRules.spec new file mode 100644 index 00000000000..2f206de2257 --- /dev/null +++ b/certora/specs/GovernorBaseRules.spec @@ -0,0 +1,202 @@ +import "helpers/helpers.spec" +import "helpers/Governor.helpers.spec" +import "GovernorInvariants.spec" + +use invariant proposalStateConsistency +use invariant canceledImplyCreated +use invariant executedImplyCreated +use invariant noBothExecutedAndCanceled + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: No double proposition │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule noDoublePropose(uint256 pId, env e) { + require proposalCreated(pId); + + address[] targets; uint256[] values; bytes[] calldatas; string reason; + uint256 result = propose(e, targets, values, calldatas, reason); + + assert result != pId, "double proposal"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: Once a proposal is created, voteStart, voteEnd and proposer are immutable │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule immutableFieldsAfterProposalCreation(uint256 pId, env e, method f, calldataarg args) + filtered { f -> !assumedSafe(f) } +{ + require proposalCreated(pId); + + uint256 voteStart = proposalSnapshot(pId); + uint256 voteEnd = proposalDeadline(pId); + address proposer = proposalProposer(pId); + + f(e, args); + + assert voteStart == proposalSnapshot(pId), "Start date was changed"; + assert voteEnd == proposalDeadline(pId), "End date was changed"; + assert proposer == proposalProposer(pId), "Proposer was changed"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: A user cannot vote twice │ +│ │ +│ This rule is checked for castVote, castVoteWithReason and castVoteWithReasonAndParams. For the signature variants │ +│ (castVoteBySig and castVoteWithReasonAndParamsBySig) we basically assume that the signature referendum is correct │ +│ without checking it. │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule noDoubleVoting(uint256 pId, env e, method f) + filtered { f -> voting(f) } +{ + address voter; + uint8 support; + + bool votedCheck = hasVoted(pId, voter); + + helperVoteWithRevert(e, f, pId, voter, support); + + assert votedCheck => lastReverted, "double voting occurred"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: Voting against a proposal does not count towards quorum. │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule againstVotesDontCountTowardsQuorum(uint256 pId, env e) +{ + bool quorumReachedBefore = quorumReached(pId); + + // Ideally we would use `helperVoteWithRevert` here, but it causes timeout. Consider changing it if/when the prover improves. + castVote(e, pId, 0); + + 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 │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule executionOnlyIfQuoromReachedAndVoteSucceeded(uint256 pId, env e, method f, calldataarg args) + filtered { f -> !assumedSafe(f) } +{ + require !isExecuted(pId); + + bool quorumReachedBefore = quorumReached(pId); + bool voteSucceededBefore = voteSucceeded(pId); + + f(e, args); + + assert isExecuted(pId) => (quorumReachedBefore && voteSucceededBefore), "quorum not met or vote not successful"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: Voting cannot start at a block number prior to proposal’s creation block number │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule noStartBeforeCreation(uint256 pId, env e, method f, calldataarg args) + filtered { f -> !assumedSafe(f) } +{ + require !proposalCreated(pId); + + f(e, args); + + assert proposalCreated(pId) => proposalSnapshot(pId) >= clock(e), "starts before proposal"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: A proposal cannot be executed before it ends │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule noExecuteBeforeDeadline(uint256 pId, env e, method f, calldataarg args) + filtered { f -> !assumedSafe(f) } +{ + require !isExecuted(pId); + + f(e, args); + + assert isExecuted(pId) => proposalDeadline(pId) <= clock(e), "executed before deadline"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Invariant: The quorum numerator is always less than or equal to the quorum denominator │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +invariant quorumRatioLessThanOne() + quorumNumerator() <= quorumDenominator() + filtered { f -> !assumedSafe(f) } + { + preserved { + require quorumNumeratorLength() < max_uint256; + } + } + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: All proposal specific (non-view) functions should revert if proposal is executed │ +│ │ +│ In this rule we show that if a function is executed, i.e. execute() was called on the proposal ID, none of the │ +│ proposal specific functions can make changes again. Note that we prove that only the `execute()` function can set | +| isExecuted() to true in in `GorvernorChanges.spec`. | +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule allFunctionsRevertIfExecuted(uint256 pId, env e, method f, calldataarg args) + filtered { f -> operateOnProposal(f) } +{ + require isExecuted(pId); + requireInvariant noBothExecutedAndCanceled(pId); + requireInvariant executedImplyCreated(pId); + + helperFunctionsWithRevert(e, f, pId); + + assert lastReverted, "Function was not reverted"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: All proposal specific (non-view) functions should revert if proposal is canceled │ +│ │ +│ In this rule we show that if a function is executed, i.e. execute() was called on the proposal ID, non of the │ +│ proposal specific functions can make changes again. Note that we prove that only the `execute()` function can set | +| isExecuted() to true in in `GorvernorChanges.spec`. | +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule allFunctionsRevertIfCanceled(uint256 pId, env e, method f, calldataarg args) + filtered { f -> operateOnProposal(f) } +{ + require isCanceled(pId); + requireInvariant noBothExecutedAndCanceled(pId); + requireInvariant canceledImplyCreated(pId); + + helperFunctionsWithRevert(e, f, pId); + + assert lastReverted, "Function was not reverted"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: Update operation are restricted to executor │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule privilegedUpdate(env e, method f, calldataarg args) + filtered { f -> !assumedSafe(f) } +{ + address executorBefore = getExecutor(); + uint256 quorumNumeratorBefore = quorumNumerator(); + address timelockBefore = timelock(); + + f(e, args); + + assert quorumNumerator() != quorumNumeratorBefore => e.msg.sender == executorBefore; + assert timelock() != timelockBefore => e.msg.sender == executorBefore; +} diff --git a/certora/specs/GovernorChanges.spec b/certora/specs/GovernorChanges.spec new file mode 100644 index 00000000000..2940500357a --- /dev/null +++ b/certora/specs/GovernorChanges.spec @@ -0,0 +1,56 @@ +import "helpers/helpers.spec" +import "helpers/Governor.helpers.spec" +import "GovernorInvariants.spec" + +use invariant proposalStateConsistency + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: Proposal can be switched state only by specific functions │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule changes(uint256 pId, env e, method f, calldataarg args) + filtered { f -> !assumedSafe(f) } +{ + require clockSanity(e); + requireInvariant proposalStateConsistency(pId); + + address user; + + bool existBefore = proposalCreated(pId); + bool isExecutedBefore = isExecuted(pId); + bool isCanceledBefore = isCanceled(pId); + bool isQueuedBefore = isQueued(pId); + bool hasVotedBefore = hasVoted(pId, user); + uint256 votesAgainstBefore = getAgainstVotes(pId); + uint256 votesForBefore = getForVotes(pId); + uint256 votesAbstainBefore = getAbstainVotes(pId); + + f(e, args); + + bool existAfter = proposalCreated(pId); + bool isExecutedAfter = isExecuted(pId); + bool isCanceledAfter = isCanceled(pId); + bool isQueuedAfter = isQueued(pId); + bool hasVotedAfter = hasVoted(pId, user); + uint256 votesAgainstAfter = getAgainstVotes(pId); + uint256 votesForAfter = getForVotes(pId); + uint256 votesAbstainAfter = getAbstainVotes(pId); + + // propose, execute, cancel + assert existAfter != existBefore => (!existBefore && f.selector == propose(address[],uint256[],bytes[],string).selector); + assert isExecutedAfter != isExecutedBefore => (!isExecutedBefore && f.selector == execute(address[],uint256[],bytes[],bytes32).selector); + assert isCanceledAfter != isCanceledBefore => (!isCanceledBefore && f.selector == cancel(address[],uint256[],bytes[],bytes32).selector); + + // queue is cleared on cancel + assert isQueuedAfter != isQueuedBefore => ( + (!isQueuedBefore && f.selector == queue(address[],uint256[],bytes[],bytes32).selector) || + (isQueuedBefore && f.selector == cancel(address[],uint256[],bytes[],bytes32).selector) + ); + + // votes + assert hasVotedAfter != hasVotedBefore => (!hasVotedBefore && votingAll(f)); + assert votesAgainstAfter != votesAgainstBefore => (votesAgainstAfter > votesAgainstBefore && votingAll(f)); + assert votesForAfter != votesForBefore => (votesForAfter > votesForBefore && votingAll(f)); + assert votesAbstainAfter != votesAbstainBefore => (votesAbstainAfter > votesAbstainBefore && votingAll(f)); +} diff --git a/certora/specs/GovernorFunctions.spec b/certora/specs/GovernorFunctions.spec new file mode 100644 index 00000000000..11560bdd7fb --- /dev/null +++ b/certora/specs/GovernorFunctions.spec @@ -0,0 +1,276 @@ +import "helpers/helpers.spec" +import "helpers/Governor.helpers.spec" +import "GovernorInvariants.spec" + +use invariant proposalStateConsistency +use invariant queuedImplyDeadlineOver + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: propose effect and liveness. Includes "no double proposition" │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule propose_liveness(uint256 pId, env e) { + require nonpayable(e); + require clockSanity(e); + + uint8 stateBefore = state(e, pId); + + address[] targets; uint256[] values; bytes[] calldatas; string descr; + require pId == hashProposal(targets, values, calldatas, descr); + + propose@withrevert(e, targets, values, calldatas, descr); + + // liveness & double proposal + assert !lastReverted <=> ( + stateBefore == UNSET() && + validProposal(targets, values, calldatas) + ); +} + +rule propose_effect(uint256 pId, env e) { + address[] targets; uint256[] values; bytes[] calldatas; string descr; + require pId == hashProposal(targets, values, calldatas, descr); + + propose(e, targets, values, calldatas, descr); + + // effect + assert state(e, pId) == PENDING(); + assert proposalProposer(pId) == e.msg.sender; + assert proposalSnapshot(pId) == clock(e) + votingDelay(); + assert proposalDeadline(pId) == clock(e) + votingDelay() + votingPeriod(); +} + +rule propose_sideeffect(uint256 pId, env e, uint256 otherId) { + uint8 otherStateBefore = state(e, otherId); + uint256 otherVoteStart = proposalSnapshot(otherId); + uint256 otherVoteEnd = proposalDeadline(otherId); + address otherProposer = proposalProposer(otherId); + + address[] targets; uint256[] values; bytes[] calldatas; string descr; + require pId == hashProposal(targets, values, calldatas, descr); + + propose(e, targets, values, calldatas, descr); + + // no side-effect + assert state(e, otherId) != otherStateBefore => otherId == pId; + assert proposalSnapshot(otherId) == otherVoteStart; + assert proposalDeadline(otherId) == otherVoteEnd; + assert proposalProposer(otherId) == otherProposer; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: votes effect and liveness. Includes "A user cannot vote twice" │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule castVote_liveness(uint256 pId, env e, method f) + filtered { f -> voting(f) } +{ + require nonpayable(e); + require clockSanity(e); + + uint8 support; + address voter; + + uint8 stateBefore = state(e, pId); + bool hasVotedBefore = hasVoted(pId, voter); + uint256 voterWeight = token_getPastVotes(voter, proposalSnapshot(pId)); + + // voting weight overflow check + require getAgainstVotes(pId) + voterWeight <= max_uint256; + require getForVotes(pId) + voterWeight <= max_uint256; + require getAbstainVotes(pId) + voterWeight <= max_uint256; + + helperVoteWithRevert(e, f, pId, voter, support); + + assert !lastReverted <=> ( + stateBefore == ACTIVE() && + !hasVotedBefore && + (support == 0 || support == 1 || support == 2) + ); +} + +rule castVote_effect(uint256 pId, env e, method f) + filtered { f -> voting(f) } +{ + uint8 support; + address voter; + + uint256 againstVotesBefore = getAgainstVotes(pId); + uint256 forVotesBefore = getForVotes(pId); + uint256 abstainVotesBefore = getAbstainVotes(pId); + uint256 voterWeight = token_getPastVotes(voter, proposalSnapshot(pId)); + + uint256 weight = helperVoteWithRevert(e, f, pId, voter, support); + require !lastReverted; + + assert state(e, pId) == ACTIVE(); + assert voterWeight == weight; + assert getAgainstVotes(pId) == againstVotesBefore + (support == 0 ? weight : 0); + assert getForVotes(pId) == forVotesBefore + (support == 1 ? weight : 0); + assert getAbstainVotes(pId) == abstainVotesBefore + (support == 2 ? weight : 0); + assert hasVoted(pId, voter); +} + +rule castVote_sideeffect(uint256 pId, env e, method f) + filtered { f -> voting(f) } +{ + uint8 support; + address voter; + address otherVoter; + uint256 otherId; + + bool otherVotedBefore = hasVoted(otherId, otherVoter); + uint256 otherAgainstVotesBefore = getAgainstVotes(otherId); + uint256 otherForVotesBefore = getForVotes(otherId); + uint256 otherAbstainVotesBefore = getAbstainVotes(otherId); + + helperVoteWithRevert(e, f, pId, voter, support); + require !lastReverted; + + // no side-effect + assert hasVoted(otherId, otherVoter) != otherVotedBefore => (otherId == pId && otherVoter == voter); + assert getAgainstVotes(otherId) != otherAgainstVotesBefore => (otherId == pId); + assert getForVotes(otherId) != otherForVotesBefore => (otherId == pId); + assert getAbstainVotes(otherId) != otherAbstainVotesBefore => (otherId == pId); +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: queue effect and liveness. │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule queue_liveness(uint256 pId, env e) { + require nonpayable(e); + require clockSanity(e); + + uint8 stateBefore = state(e, pId); + + address[] targets; uint256[] values; bytes[] calldatas; bytes32 descrHash; + require pId == hashProposal(targets, values, calldatas, descrHash); + + queue@withrevert(e, targets, values, calldatas, descrHash); + + // liveness + assert !lastReverted <=> stateBefore == SUCCEEDED(); +} + +rule queue_effect(uint256 pId, env e) { + uint8 stateBefore = state(e, pId); + bool queuedBefore = isQueued(pId); + + address[] targets; uint256[] values; bytes[] calldatas; bytes32 descrHash; + require pId == hashProposal(targets, values, calldatas, descrHash); + + queue(e, targets, values, calldatas, descrHash); + + assert state(e, pId) == QUEUED(); + assert isQueued(pId); + assert !queuedBefore; +} + +rule queue_sideeffect(uint256 pId, env e, uint256 otherId) { + uint8 otherStateBefore = state(e, otherId); + bool otherQueuedBefore = isQueued(otherId); + + address[] targets; uint256[] values; bytes[] calldatas; bytes32 descrHash; + require pId == hashProposal(targets, values, calldatas, descrHash); + + queue(e, targets, values, calldatas, descrHash); + + // no side-effect + assert state(e, otherId) != otherStateBefore => otherId == pId; + assert isQueued(otherId) != otherQueuedBefore => otherId == pId; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: execute effect and liveness. │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule execute_liveness(uint256 pId, env e) { + require nonpayable(e); + require clockSanity(e); + + uint8 stateBefore = state(e, pId); + + address[] targets; uint256[] values; bytes[] calldatas; bytes32 descrHash; + require pId == hashProposal(targets, values, calldatas, descrHash); + + execute@withrevert(e, targets, values, calldatas, descrHash); + + // liveness: can't check full equivalence because of execution call reverts + assert !lastReverted => (stateBefore == SUCCEEDED() || stateBefore == QUEUED()); +} + +rule execute_effect(uint256 pId, env e) { + address[] targets; uint256[] values; bytes[] calldatas; bytes32 descrHash; + require pId == hashProposal(targets, values, calldatas, descrHash); + + execute(e, targets, values, calldatas, descrHash); + + // effect + assert state(e, pId) == EXECUTED(); +} + +rule execute_sideeffect(uint256 pId, env e, uint256 otherId) { + uint8 otherStateBefore = state(e, otherId); + + address[] targets; uint256[] values; bytes[] calldatas; bytes32 descrHash; + require pId == hashProposal(targets, values, calldatas, descrHash); + + execute(e, targets, values, calldatas, descrHash); + + // no side-effect + assert state(e, otherId) != otherStateBefore => otherId == pId; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: cancel (public) effect and liveness. │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule cancel_liveness(uint256 pId, env e) { + require nonpayable(e); + require clockSanity(e); + requireInvariant queuedImplyDeadlineOver(e, pId); + + uint8 stateBefore = state(e, pId); + + address[] targets; uint256[] values; bytes[] calldatas; bytes32 descrHash; + require pId == hashProposal(targets, values, calldatas, descrHash); + + cancel@withrevert(e, targets, values, calldatas, descrHash); + + // liveness + assert !lastReverted <=> ( + stateBefore == PENDING() && + e.msg.sender == proposalProposer(pId) + ); +} + +rule cancel_effect(uint256 pId, env e) { + address[] targets; uint256[] values; bytes[] calldatas; bytes32 descrHash; + require pId == hashProposal(targets, values, calldatas, descrHash); + + cancel(e, targets, values, calldatas, descrHash); + + // effect + assert state(e, pId) == CANCELED(); + assert !isQueued(pId); // cancel resets timelockId +} + +rule cancel_sideeffect(uint256 pId, env e, uint256 otherId) { + uint8 otherStateBefore = state(e, otherId); + bool otherQueuedBefore = isQueued(otherId); + + address[] targets; uint256[] values; bytes[] calldatas; bytes32 descrHash; + require pId == hashProposal(targets, values, calldatas, descrHash); + + cancel(e, targets, values, calldatas, descrHash); + + // no side-effect + assert state(e, otherId) != otherStateBefore => otherId == pId; + assert isQueued(otherId) != otherQueuedBefore => otherId == pId; +} diff --git a/certora/specs/GovernorInvariants.spec b/certora/specs/GovernorInvariants.spec new file mode 100644 index 00000000000..255c5c3449c --- /dev/null +++ b/certora/specs/GovernorInvariants.spec @@ -0,0 +1,153 @@ +import "helpers/helpers.spec" +import "helpers/Governor.helpers.spec" + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Invariant: clock is consistent between the goernor and the token │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule clockMode(env e) { + require clockSanity(e); + + assert clock(e) == e.block.number || clock(e) == e.block.timestamp; + assert clock(e) == token_clock(e); + + /// This causes a failure in the prover + // assert CLOCK_MODE(e) == token_CLOCK_MODE(e); +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Invariant: Votes start and end are either initialized (non zero) or uninitialized (zero) simultaneously │ +│ │ +│ This invariant assumes that the block number cannot be 0 at any stage of the contract cycle │ +│ This is very safe assumption as usually the 0 block is genesis block which is uploaded with data │ +│ by the developers and will not be valid to raise proposals (at the current way that block chain is functioning) │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +invariant proposalStateConsistency(uint256 pId) + (proposalProposer(pId) == 0 <=> proposalSnapshot(pId) == 0) && + (proposalProposer(pId) == 0 <=> proposalDeadline(pId) == 0) + { + preserved with (env e) { + require clockSanity(e); + } + } + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Invariant: votes recorded => created │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +invariant votesImplyCreated(uint256 pId) + ( + getAgainstVotes(pId) > 0 || + getForVotes(pId) > 0 || + getAbstainVotes(pId) > 0 + ) => proposalCreated(pId) + { + preserved with (env e) { + require clockSanity(e); + requireInvariant proposalStateConsistency(pId); + } + } + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Invariant: cancel => created │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +invariant canceledImplyCreated(uint pId) + isCanceled(pId) => proposalCreated(pId) + { + preserved with (env e) { + require clockSanity(e); + requireInvariant proposalStateConsistency(pId); + } + } + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Invariant: executed => created │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +invariant executedImplyCreated(uint pId) + isExecuted(pId) => proposalCreated(pId) + { + preserved with (env e) { + require clockSanity(e); + requireInvariant proposalStateConsistency(pId); + } + } + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Invariant: queued => created │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +invariant queuedImplyCreated(uint pId) + isQueued(pId) => proposalCreated(pId) + { + preserved with (env e) { + require clockSanity(e); + requireInvariant proposalStateConsistency(pId); + } + } + + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Invariant: timings │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +invariant votesImplySnapshotPassed(env e, uint256 pId) + ( + getAgainstVotes(pId) > 0 || + getForVotes(pId) > 0 || + getAbstainVotes(pId) > 0 + ) => proposalSnapshot(pId) < clock(e) + { + preserved with (env e2) { + // In this invariant, `env e` is representing the present. And `clock(e)` the current timestamp. + // It should hold for any transitions in the pasts + require clock(e2) <= clock(e); + } + } + +invariant queuedImplyDeadlineOver(env e, uint pId) + isQueued(pId) => proposalDeadline(pId) < clock(e) + { + preserved { + require clockSanity(e); + requireInvariant proposalStateConsistency(pId); + } + } + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Invariant: Votes start before it ends │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +invariant voteStartBeforeVoteEnd(uint256 pId) + proposalSnapshot(pId) <= proposalDeadline(pId) + { + preserved { + requireInvariant proposalStateConsistency(pId); + } + } + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Invariant: A proposal cannot be both executed and canceled simultaneously │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +invariant noBothExecutedAndCanceled(uint256 pId) + !isExecuted(pId) || !isCanceled(pId) + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Invariant: the "governance call" dequeue is empty │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +invariant governanceCallLength() + governanceCallLength() == 0 diff --git a/certora/specs/GovernorPreventLateQuorum.spec b/certora/specs/GovernorPreventLateQuorum.spec new file mode 100644 index 00000000000..c12f6ae8a95 --- /dev/null +++ b/certora/specs/GovernorPreventLateQuorum.spec @@ -0,0 +1,68 @@ +import "helpers/helpers.spec" +import "helpers/Governor.helpers.spec" +import "GovernorInvariants.spec" + +methods { + lateQuorumVoteExtension() returns uint64 envfree + getExtendedDeadline(uint256) returns uint64 envfree +} + +use invariant proposalStateConsistency +use invariant votesImplySnapshotPassed + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ 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. │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +// invariant deadlineExtendedEquivQuorumReached(uint256 pId) +// getExtendedDeadline(pId) > 0 <=> (quorumReached(pId) && !isCanceled(pId)) + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ 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 -> !assumedSafe(f) } +{ + require clockSanity(e); + requireInvariant proposalStateConsistency(pId); + requireInvariant votesImplySnapshotPassed(e, pId); + + uint256 deadlineBefore = proposalDeadline(pId); + bool deadlineExtendedBefore = getExtendedDeadline(pId) > 0; + + f(e, args); + + uint256 deadlineAfter = proposalDeadline(pId); + bool deadlineExtendedAfter = getExtendedDeadline(pId) > 0; + + // deadline can never be reduced + assert deadlineBefore <= deadlineAfter; + + // 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 && + 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; +} diff --git a/certora/specs/GovernorStates.spec b/certora/specs/GovernorStates.spec new file mode 100644 index 00000000000..dc449f5fbd3 --- /dev/null +++ b/certora/specs/GovernorStates.spec @@ -0,0 +1,238 @@ +import "helpers/helpers.spec" +import "helpers/Governor.helpers.spec" +import "GovernorInvariants.spec" + +use invariant proposalStateConsistency +use invariant votesImplySnapshotPassed + +definition assumedSafeOrDuplicate(method f) returns bool = + assumedSafe(f) + || f.selector == castVoteWithReason(uint256,uint8,string).selector + || f.selector == castVoteWithReasonAndParams(uint256,uint8,string,bytes).selector + || f.selector == castVoteBySig(uint256,uint8,uint8,bytes32,bytes32).selector + || f.selector == castVoteWithReasonAndParamsBySig(uint256,uint8,string,bytes,uint8,bytes32,bytes32).selector; + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: state returns one of the value in the enumeration │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule stateDomain(env e, uint256 pId) { + uint8 result = safeState(e, pId); + assert ( + result == UNSET() || + result == PENDING() || + result == ACTIVE() || + result == CANCELED() || + result == DEFEATED() || + result == SUCCEEDED() || + result == QUEUED() || + result == EXECUTED() + ); +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ [DISABLED] Rule: State transitions caused by function calls │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +/// Previous version that results in the prover timing out. +// rule stateTransitionFn(uint256 pId, env e, method f, calldataarg args) +// filtered { f -> !assumedSafeOrDuplicate(f) } +// { +// require clockSanity(e); +// require quorumNumeratorLength() < max_uint256; // sanity +// +// uint8 stateBefore = safeState(e, pId); +// f(e, args); +// uint8 stateAfter = safeState(e, pId); +// +// assert (stateBefore != stateAfter) => ( +// (stateBefore == UNSET() && stateAfter == PENDING() && f.selector == propose(address[],uint256[],bytes[],string).selector ) || +// (stateBefore == PENDING() && stateAfter == CANCELED() && f.selector == cancel(address[],uint256[],bytes[],bytes32).selector ) || +// (stateBefore == SUCCEEDED() && stateAfter == QUEUED() && f.selector == queue(address[],uint256[],bytes[],bytes32).selector ) || +// (stateBefore == SUCCEEDED() && stateAfter == EXECUTED() && f.selector == execute(address[],uint256[],bytes[],bytes32).selector) || +// (stateBefore == QUEUED() && stateAfter == EXECUTED() && f.selector == execute(address[],uint256[],bytes[],bytes32).selector) +// ); +// } + +/// This version also causes a lot of timeouts so we comment it out of now +// function stateTransitionFnHelper(method f, uint8 s) returns uint8 { +// uint256 pId; env e; calldataarg args; +// +// require clockSanity(e); +// require quorumNumeratorLength() < max_uint256; // sanity +// +// require safeState(e, pId) == s; // constrain state before +// f(e, args); +// require safeState(e, pId) != s; // constrain state after +// +// return safeState(e, pId); +// } +// +// rule stateTransitionFn_UNSET(method f) filtered { f -> !assumedSafeOrDuplicate(f) } { +// uint8 stateAfter = stateTransitionFnHelper(f, UNSET()); +// assert stateAfter == PENDING() && f.selector == propose(address[],uint256[],bytes[],string).selector; +// } +// +// rule stateTransitionFn_PENDING(method f) filtered { f -> !assumedSafeOrDuplicate(f) } { +// uint8 stateAfter = stateTransitionFnHelper(f, PENDING()); +// assert stateAfter == CANCELED() && f.selector == cancel(address[],uint256[],bytes[],bytes32).selector; +// } +// +// rule stateTransitionFn_ACTIVE(method f) filtered { f -> !assumedSafeOrDuplicate(f) } { +// uint8 stateAfter = stateTransitionFnHelper(f, ACTIVE()); +// assert false; +// } +// +// rule stateTransitionFn_CANCELED(method f) filtered { f -> !assumedSafeOrDuplicate(f) } { +// uint8 stateAfter = stateTransitionFnHelper(f, CANCELED()); +// assert false; +// } +// +// rule stateTransitionFn_DEFEATED(method f) filtered { f -> !assumedSafeOrDuplicate(f) } { +// uint8 stateAfter = stateTransitionFnHelper(f, DEFEATED()); +// assert false; +// } +// +// rule stateTransitionFn_SUCCEEDED(method f) filtered { f -> !assumedSafeOrDuplicate(f) } { +// uint8 stateAfter = stateTransitionFnHelper(f, SUCCEEDED()); +// assert ( +// (stateAfter == QUEUED() && f.selector == queue(address[],uint256[],bytes[],bytes32).selector) || +// (stateAfter == EXECUTED() && f.selector == execute(address[],uint256[],bytes[],bytes32).selector) +// ); +// } +// +// rule stateTransitionFn_QUEUED(method f) filtered { f -> !assumedSafeOrDuplicate(f) } { +// uint8 stateAfter = stateTransitionFnHelper(f, QUEUED()); +// assert stateAfter == EXECUTED() && f.selector == execute(address[],uint256[],bytes[],bytes32).selector; +// } +// +// rule stateTransitionFn_EXECUTED(method f) filtered { f -> !assumedSafeOrDuplicate(f) } { +// uint8 stateAfter = stateTransitionFnHelper(f, EXECUTED()); +// assert false; +// } + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: State transitions caused by time passing │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +// The timelockId can be set in states QUEUED, EXECUTED and CANCELED. However, checking the full scope of this results +// in a timeout. This is a weaker version that is still useful. Ideally we would check `safeState`. +invariant noTimelockBeforeEndOfVote(env e, uint256 pId) + state(e, pId) == ACTIVE() => timelockId(pId) == 0 + +rule stateTransitionWait(uint256 pId, env e1, env e2) { + require clockSanity(e1); + require clockSanity(e2); + require clock(e2) > clock(e1); + + // Force the state to be consistent with e1 (before). We want the storage related to `pId` to match what is + // possible before the time passes. We don't want the state transition include elements that cannot have happened + // before e1. This ensure that the e1 → e2 state transition is purelly a consequence of time passing. + requireInvariant votesImplySnapshotPassed(e1, pId); + requireInvariant noTimelockBeforeEndOfVote(e1, pId); + + uint8 stateBefore = state(e1, pId); // Ideally we would use "safeState(e1, pId)" + uint8 stateAfter = state(e2, pId); // Ideally we would use "safeState(e2, pId)" + + assert (stateBefore != stateAfter) => ( + (stateBefore == PENDING() && stateAfter == ACTIVE() ) || + (stateBefore == PENDING() && stateAfter == DEFEATED() ) || + (stateBefore == ACTIVE() && stateAfter == SUCCEEDED()) || + (stateBefore == ACTIVE() && stateAfter == DEFEATED() ) + ); +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: State corresponds to the vote timing and results │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule stateIsConsistentWithVotes(uint256 pId, env e) { + require clockSanity(e); + requireInvariant proposalStateConsistency(pId); + + uint48 currentClock = clock(e); + uint8 currentState = safeState(e, pId); + uint256 snapshot = proposalSnapshot(pId); + uint256 deadline = proposalDeadline(pId); + bool quorumSuccess = quorumReached(pId); + bool voteSuccess = voteSucceeded(pId); + + // Pending: before vote starts + assert currentState == PENDING() => ( + snapshot >= currentClock + ); + + // Active: after vote starts & before vote ends + assert currentState == ACTIVE() => ( + snapshot < currentClock && + deadline >= currentClock + ); + + // Succeeded: after vote end, with vote successful and quorum reached + assert currentState == SUCCEEDED() => ( + deadline < currentClock && + ( + quorumSuccess && + voteSuccess + ) + ); + + // Defeated: after vote end, with vote not successful or quorum not reached + assert currentState == DEFEATED() => ( + deadline < currentClock && + ( + !quorumSuccess || + !voteSuccess + ) + ); +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ [NEED WORK] Rule: `updateQuorumNumerator` cannot cause quorumReached to change. │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +//// 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) increasing keys. +// rule onlyVoteCanChangeQuorumReached(uint256 pId, env e, method f, calldataarg args) +// filtered { f -> !assumedSafeOrDuplicate(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) increasing keys. +//// 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; +// } diff --git a/certora/specs/TimelockController.spec b/certora/specs/TimelockController.spec index 05ecb1340f0..105331c915b 100644 --- a/certora/specs/TimelockController.spec +++ b/certora/specs/TimelockController.spec @@ -1,29 +1,6 @@ import "helpers/helpers.spec" import "methods/IAccessControl.spec" - -methods { - TIMELOCK_ADMIN_ROLE() returns (bytes32) envfree - PROPOSER_ROLE() returns (bytes32) envfree - EXECUTOR_ROLE() returns (bytes32) envfree - CANCELLER_ROLE() returns (bytes32) envfree - isOperation(bytes32) returns (bool) envfree - isOperationPending(bytes32) returns (bool) envfree - isOperationReady(bytes32) returns (bool) - isOperationDone(bytes32) returns (bool) envfree - getTimestamp(bytes32) returns (uint256) envfree - getMinDelay() returns (uint256) envfree - - hashOperation(address, uint256, bytes, bytes32, bytes32) returns(bytes32) envfree - hashOperationBatch(address[], uint256[], bytes[], bytes32, bytes32) returns(bytes32) envfree - - schedule(address, uint256, bytes, bytes32, bytes32, uint256) - scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256) - execute(address, uint256, bytes, bytes32, bytes32) - executeBatch(address[], uint256[], bytes[], bytes32, bytes32) - cancel(bytes32) - - updateDelay(uint256) -} +import "methods/ITimelockController.spec" /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ diff --git a/certora/specs/helpers/Governor.helpers.spec b/certora/specs/helpers/Governor.helpers.spec new file mode 100644 index 00000000000..de452c68974 --- /dev/null +++ b/certora/specs/helpers/Governor.helpers.spec @@ -0,0 +1,186 @@ +import "helpers.spec" +import "../methods/IGovernor.spec" +import "../methods/ITimelockController.spec" + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Sanity │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +function clockSanity(env e) returns bool { + return e.block.number < max_uint48() + && e.block.timestamp < max_uint48() + && clock(e) > 0; +} + +function validProposal(address[] targets, uint256[] values, bytes[] calldatas) returns bool { + return targets.length > 0 + && targets.length == values.length + && targets.length == calldatas.length; +} + +function sanityString(string s) returns bool { + return s.length < 0xffff; +} + +function sanityBytes(bytes b) returns bool { + return b.length < 0xffff; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ States │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +definition UNSET() returns uint8 = 255; +definition PENDING() returns uint8 = 0; +definition ACTIVE() returns uint8 = 1; +definition CANCELED() returns uint8 = 2; +definition DEFEATED() returns uint8 = 3; +definition SUCCEEDED() returns uint8 = 4; +definition QUEUED() returns uint8 = 5; +definition EXPIRED() returns uint8 = 6; +definition EXECUTED() returns uint8 = 7; + +// This helper is an alternative to state(e, pId) that will return UNSET() instead of reverting when then proposal +// does not exist (not created yet) +function safeState(env e, uint256 pId) returns uint8 { + return proposalCreated(pId) ? state(e, pId): UNSET(); +} + +definition proposalCreated(uint256 pId) returns bool = + proposalSnapshot(pId) > 0 && proposalDeadline(pId) > 0 && proposalProposer(pId) != 0; + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Filters │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +definition assumedSafe(method f) returns bool = + f.isView || + f.isFallback || + f.selector == relay(address,uint256,bytes).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; + +// These function are covered by helperFunctionsWithRevert +definition operateOnProposal(method f) returns bool = + f.selector == propose(address[],uint256[],bytes[],string).selector || + f.selector == queue(address[],uint256[],bytes[],bytes32).selector || + f.selector == execute(address[],uint256[],bytes[],bytes32).selector || + f.selector == cancel(address[],uint256[],bytes[],bytes32).selector || + f.selector == castVote(uint256,uint8).selector || + f.selector == castVoteWithReason(uint256,uint8,string).selector || + f.selector == castVoteWithReasonAndParams(uint256,uint8,string,bytes).selector || + f.selector == castVoteBySig(uint256,uint8,uint8,bytes32,bytes32).selector || + f.selector == castVoteWithReasonAndParamsBySig(uint256,uint8,string,bytes,uint8,bytes32,bytes32).selector; + +// These function are covered by helperVoteWithRevert +definition voting(method f) returns bool = + f.selector == castVote(uint256,uint8).selector || + f.selector == castVoteWithReason(uint256,uint8,string).selector || + f.selector == castVoteWithReasonAndParams(uint256,uint8,string,bytes).selector; + +definition votingBySig(method f) returns bool = + f.selector == castVoteBySig(uint256,uint8,uint8,bytes32,bytes32).selector || + f.selector == castVoteWithReasonAndParamsBySig(uint256,uint8,string,bytes,uint8,bytes32,bytes32).selector; + +definition votingAll(method f) returns bool = + voting(f) || votingBySig(f); + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Helper functions │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +function helperVoteWithRevert(env e, method f, uint256 pId, address voter, uint8 support) returns uint256 { + if (f.selector == castVote(uint256,uint8).selector) + { + require e.msg.sender == voter; + return castVote@withrevert(e, pId, support); + } + else if (f.selector == castVoteWithReason(uint256,uint8,string).selector) + { + string reason; + require e.msg.sender == voter && sanityString(reason); + return castVoteWithReason@withrevert(e, pId, support, reason); + } + else if (f.selector == castVoteWithReasonAndParams(uint256,uint8,string,bytes).selector) + { + string reason; bytes params; + require e.msg.sender == voter && sanityString(reason) && sanityBytes(params); + return castVoteWithReasonAndParams@withrevert(e, pId, support, reason, params); + } + else + { + calldataarg args; + f(e, args); + return 0; + } +} + +// Governor function that operates on a given proposalId may or may not include the proposalId in the arguments. This +// helper restricts the call to method `f` in a way that it's operating on a specific proposal. +// +// This can be used to say "consider any function call that operates on proposal `pId`" or "consider a propose call +// that corresponds to a given pId". +// +// This is for example used when proving that not 2 proposals can be proposed with the same id: Once the proposal is +// proposed a first time, we want to prove that "any propose call that corresponds to the same id should revert". +function helperFunctionsWithRevert(env e, method f, uint256 pId) { + if (f.selector == propose(address[],uint256[],bytes[],string).selector) + { + address[] targets; uint256[] values; bytes[] calldatas; string descr; + require pId == hashProposal(targets, values, calldatas, descr); + propose@withrevert(e, targets, values, calldatas, descr); + } + else if (f.selector == queue(address[],uint256[],bytes[],bytes32).selector) + { + address[] targets; uint256[] values; bytes[] calldatas; bytes32 descrHash; + require pId == hashProposal(targets, values, calldatas, descrHash); + queue@withrevert(e, targets, values, calldatas, descrHash); + } + else if (f.selector == execute(address[],uint256[],bytes[],bytes32).selector) + { + address[] targets; uint256[] values; bytes[] calldatas; bytes32 descrHash; + require pId == hashProposal(targets, values, calldatas, descrHash); + execute@withrevert(e, targets, values, calldatas, descrHash); + } + else if (f.selector == cancel(address[],uint256[],bytes[],bytes32).selector) + { + address[] targets; uint256[] values; bytes[] calldatas; bytes32 descrHash; + require pId == hashProposal(targets, values, calldatas, descrHash); + cancel@withrevert(e, targets, values, calldatas, descrHash); + } + else if (f.selector == castVote(uint256,uint8).selector) + { + uint8 support; + castVote@withrevert(e, pId, support); + } + else if (f.selector == castVoteWithReason(uint256,uint8,string).selector) + { + uint8 support; string reason; + castVoteWithReason@withrevert(e, pId, support, reason); + } + else if (f.selector == castVoteWithReasonAndParams(uint256,uint8,string,bytes).selector) + { + uint8 support; string reason; bytes params; + castVoteWithReasonAndParams@withrevert(e, pId, support, reason, params); + } + else if (f.selector == castVoteBySig(uint256,uint8,uint8,bytes32,bytes32).selector) + { + uint8 support; uint8 v; bytes32 r; bytes32 s; + castVoteBySig@withrevert(e, pId, support, v, r, s); + } + else if (f.selector == castVoteWithReasonAndParamsBySig(uint256,uint8,string,bytes,uint8,bytes32,bytes32).selector) + { + uint8 support; string reason; bytes params; uint8 v; bytes32 r; bytes32 s; + castVoteWithReasonAndParamsBySig@withrevert(e, pId, support, reason, params, v, r, s); + } + else + { + calldataarg args; + f(e, args); + } +} diff --git a/certora/specs/methods/IGovernor.spec b/certora/specs/methods/IGovernor.spec new file mode 100644 index 00000000000..25abb6c22ef --- /dev/null +++ b/certora/specs/methods/IGovernor.spec @@ -0,0 +1,56 @@ +// includes some non standard (from extension) and harness functions +methods { + name() returns string envfree + version() returns string envfree + token() returns address envfree + timelock() returns address envfree + clock() returns uint48 + CLOCK_MODE() returns string + COUNTING_MODE() returns string envfree + hashProposal(address[],uint256[],bytes[],bytes32) returns uint256 envfree + state(uint256) returns uint8 + proposalThreshold() returns uint256 envfree + proposalSnapshot(uint256) returns uint256 envfree + proposalDeadline(uint256) returns uint256 envfree + votingDelay() returns uint256 envfree + votingPeriod() returns uint256 envfree + quorum(uint256) returns uint256 envfree + getVotes(address,uint256) returns uint256 envfree + getVotesWithParams(address,uint256,bytes) returns uint256 envfree + hasVoted(uint256,address) returns bool envfree + quorumNumerator() returns uint256 envfree + quorumNumerator(uint256) returns uint256 envfree + quorumDenominator() returns uint256 envfree + + propose(address[],uint256[],bytes[],string) returns uint256 + execute(address[],uint256[],bytes[],bytes32) returns uint256 + queue(address[], uint256[], bytes[], bytes32) returns uint256 + cancel(address[],uint256[],bytes[],bytes32) returns uint256 + castVote(uint256,uint8) returns uint256 + castVoteWithReason(uint256,uint8,string) returns uint256 + castVoteWithReasonAndParams(uint256,uint8,string,bytes) returns uint256 + castVoteBySig(uint256,uint8,uint8,bytes32,bytes32) returns uint256 + castVoteWithReasonAndParamsBySig(uint256,uint8,string,bytes,uint8,bytes32,bytes32) returns uint256 + updateQuorumNumerator(uint256) + updateTimelock(address) + + // harness + token_getPastTotalSupply(uint256) returns uint256 envfree + token_getPastVotes(address,uint256) returns uint256 envfree + token_clock() returns uint48 + token_CLOCK_MODE() returns string + hashProposal(address[],uint256[],bytes[],string) returns uint256 envfree + getExecutor() returns address envfree + proposalProposer(uint256) returns address envfree + quorumReached(uint256) returns bool envfree + 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 + getAbstainVotes(uint256) returns uint256 envfree + quorumNumeratorLength() returns uint256 envfree + timelockId(uint256) returns bytes32 envfree +} diff --git a/certora/specs/methods/ITimelockController.spec b/certora/specs/methods/ITimelockController.spec new file mode 100644 index 00000000000..a91fe211acf --- /dev/null +++ b/certora/specs/methods/ITimelockController.spec @@ -0,0 +1,22 @@ +methods { + TIMELOCK_ADMIN_ROLE() returns (bytes32) envfree => DISPATCHER(true) + PROPOSER_ROLE() returns (bytes32) envfree => DISPATCHER(true) + EXECUTOR_ROLE() returns (bytes32) envfree => DISPATCHER(true) + CANCELLER_ROLE() returns (bytes32) envfree => DISPATCHER(true) + isOperation(bytes32) returns (bool) envfree => DISPATCHER(true) + isOperationPending(bytes32) returns (bool) envfree => DISPATCHER(true) + isOperationReady(bytes32) returns (bool) => DISPATCHER(true) + isOperationDone(bytes32) returns (bool) envfree => DISPATCHER(true) + getTimestamp(bytes32) returns (uint256) envfree => DISPATCHER(true) + getMinDelay() returns (uint256) envfree => DISPATCHER(true) + + hashOperation(address, uint256, bytes, bytes32, bytes32) returns(bytes32) envfree => DISPATCHER(true) + hashOperationBatch(address[], uint256[], bytes[], bytes32, bytes32) returns(bytes32) envfree => DISPATCHER(true) + + schedule(address, uint256, bytes, bytes32, bytes32, uint256) => DISPATCHER(true) + scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256) => DISPATCHER(true) + execute(address, uint256, bytes, bytes32, bytes32) => DISPATCHER(true) + executeBatch(address[], uint256[], bytes[], bytes32, bytes32) => DISPATCHER(true) + cancel(bytes32) => DISPATCHER(true) + updateDelay(uint256) => DISPATCHER(true) +} \ No newline at end of file diff --git a/requirements.txt b/requirements.txt index da3e95766cb..5aad982b2f5 100644 --- a/requirements.txt +++ b/requirements.txt @@ -1 +1 @@ -certora-cli==3.6.4 +certora-cli==3.6.8