From e9f53ebc02b8601f9200bd8a191c14f6a7364505 Mon Sep 17 00:00:00 2001 From: Hadrien Croubois Date: Fri, 9 Sep 2022 13:33:55 +0200 Subject: [PATCH] run prettier --write --- certora/harnesses/AccessControlHarness.sol | 4 +- .../ERC1155/ERC1155BurnableHarness.sol | 5 +- certora/harnesses/ERC1155/ERC1155Harness.sol | 16 +-- .../ERC1155/ERC1155PausableHarness.sol | 11 +- .../ERC1155/ERC1155SupplyHarness.sol | 20 ++-- certora/harnesses/ERC20PermitHarness.sol | 6 +- certora/harnesses/ERC20VotesHarness.sol | 6 +- certora/harnesses/ERC20WrapperHarness.sol | 12 +- certora/harnesses/ERC721VotesHarness.sol | 4 +- .../GovernorPreventLateQuorumHarness.sol | 104 ++++++++++-------- .../IERC3156FlashBorrowerHarness.sol | 2 +- .../harnesses/InitializableBasicHarness.sol | 35 +++--- .../harnesses/InitializableComplexHarness.sol | 37 ++++--- .../harnesses/TimelockControllerHarness.sol | 10 +- .../harnesses/WizardControlFirstPriority.sol | 92 +++++++++------- certora/harnesses/WizardFirstTry.sol | 76 +++++++------ 16 files changed, 240 insertions(+), 200 deletions(-) diff --git a/certora/harnesses/AccessControlHarness.sol b/certora/harnesses/AccessControlHarness.sol index 3ae6e7e8c..e5cce2306 100644 --- a/certora/harnesses/AccessControlHarness.sol +++ b/certora/harnesses/AccessControlHarness.sol @@ -5,6 +5,4 @@ pragma solidity ^0.8.0; import "../munged/access/AccessControl.sol"; -contract AccessControlHarness is AccessControl { - -} +contract AccessControlHarness is AccessControl {} diff --git a/certora/harnesses/ERC1155/ERC1155BurnableHarness.sol b/certora/harnesses/ERC1155/ERC1155BurnableHarness.sol index 5f7fbd706..119f1231e 100644 --- a/certora/harnesses/ERC1155/ERC1155BurnableHarness.sol +++ b/certora/harnesses/ERC1155/ERC1155BurnableHarness.sol @@ -1,8 +1,5 @@ import "../../munged/token/ERC1155/extensions/ERC1155Burnable.sol"; contract ERC1155BurnableHarness is ERC1155Burnable { - constructor(string memory uri_) - ERC1155(uri_) - {} + constructor(string memory uri_) ERC1155(uri_) {} } - diff --git a/certora/harnesses/ERC1155/ERC1155Harness.sol b/certora/harnesses/ERC1155/ERC1155Harness.sol index 94581511c..5ec49657d 100644 --- a/certora/harnesses/ERC1155/ERC1155Harness.sol +++ b/certora/harnesses/ERC1155/ERC1155Harness.sol @@ -3,14 +3,16 @@ pragma solidity ^0.8.2; import "../../munged/token/ERC1155/ERC1155.sol"; contract ERC1155Harness is ERC1155 { + constructor(string memory uri_) ERC1155(uri_) {} - constructor(string memory uri_) - ERC1155(uri_) - {} - - function burn( address from, uint256 id, uint256 amount) public virtual { + function burn( + address from, + uint256 id, + uint256 amount + ) public virtual { _burn(from, id, amount); } + function burnBatch( address from, uint256[] memory ids, @@ -33,7 +35,7 @@ contract ERC1155Harness is ERC1155 { uint256[] memory ids, uint256[] memory amounts, bytes memory data - ) public virtual { + ) public virtual { _mintBatch(to, ids, amounts, data); } -} \ No newline at end of file +} diff --git a/certora/harnesses/ERC1155/ERC1155PausableHarness.sol b/certora/harnesses/ERC1155/ERC1155PausableHarness.sol index 134a78748..ed31d28b6 100644 --- a/certora/harnesses/ERC1155/ERC1155PausableHarness.sol +++ b/certora/harnesses/ERC1155/ERC1155PausableHarness.sol @@ -1,9 +1,7 @@ import "../../munged/token/ERC1155/extensions/ERC1155Pausable.sol"; contract ERC1155PausableHarness is ERC1155Pausable { - constructor(string memory uri_) - ERC1155(uri_) - {} + constructor(string memory uri_) ERC1155(uri_) {} function pause() public { _pause(); @@ -13,10 +11,7 @@ contract ERC1155PausableHarness is ERC1155Pausable { _unpause(); } - function onlyWhenPausedMethod() public whenPaused { - } + function onlyWhenPausedMethod() public whenPaused {} - function onlyWhenNotPausedMethod() public whenNotPaused { - } + function onlyWhenNotPausedMethod() public whenNotPaused {} } - diff --git a/certora/harnesses/ERC1155/ERC1155SupplyHarness.sol b/certora/harnesses/ERC1155/ERC1155SupplyHarness.sol index 6702ede58..675a3b9d2 100644 --- a/certora/harnesses/ERC1155/ERC1155SupplyHarness.sol +++ b/certora/harnesses/ERC1155/ERC1155SupplyHarness.sol @@ -1,8 +1,8 @@ import "../../munged/token/ERC1155/extensions/ERC1155Supply.sol"; - contract ERC1155SupplyHarness is ERC1155Supply { address public owner; + constructor(string memory uri_) ERC1155(uri_) { owner = msg.sender; } @@ -12,19 +12,24 @@ contract ERC1155SupplyHarness is ERC1155Supply { return exists(id); } - // These rules were not implemented in the base but there are changes in supply - // that are affected by the internal contracts so we implemented them. We assume - // only the owner can call any of these functions to be able to test them but also + // These rules were not implemented in the base but there are changes in supply + // that are affected by the internal contracts so we implemented them. We assume + // only the owner can call any of these functions to be able to test them but also // limit false positives. - modifier onlyOwner { + modifier onlyOwner() { require(msg.sender == owner); _; } - function burn( address from, uint256 id, uint256 amount) public virtual onlyOwner { + function burn( + address from, + uint256 id, + uint256 amount + ) public virtual onlyOwner { _burn(from, id, amount); } + function burnBatch( address from, uint256[] memory ids, @@ -47,7 +52,7 @@ contract ERC1155SupplyHarness is ERC1155Supply { uint256[] memory ids, uint256[] memory amounts, bytes memory data - ) public virtual onlyOwner { + ) public virtual onlyOwner { _mintBatch(to, ids, amounts, data); } @@ -58,4 +63,3 @@ contract ERC1155SupplyHarness is ERC1155Supply { return _balances[id][account]; } } - diff --git a/certora/harnesses/ERC20PermitHarness.sol b/certora/harnesses/ERC20PermitHarness.sol index 29d060232..67fa937df 100644 --- a/certora/harnesses/ERC20PermitHarness.sol +++ b/certora/harnesses/ERC20PermitHarness.sol @@ -1,9 +1,5 @@ import "../munged/token/ERC20/extensions/draft-ERC20Permit.sol"; contract ERC20PermitHarness is ERC20Permit { - constructor(string memory _name, string memory _symbol) - ERC20(_name, _symbol) - ERC20Permit(_name) - {} + constructor(string memory _name, string memory _symbol) ERC20(_name, _symbol) ERC20Permit(_name) {} } - diff --git a/certora/harnesses/ERC20VotesHarness.sol b/certora/harnesses/ERC20VotesHarness.sol index c2cad2f6d..5f1ad6e19 100644 --- a/certora/harnesses/ERC20VotesHarness.sol +++ b/certora/harnesses/ERC20VotesHarness.sol @@ -6,7 +6,7 @@ contract ERC20VotesHarness is ERC20Votes { 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].fromBlock; } @@ -30,7 +30,5 @@ contract ERC20VotesHarness is ERC20Votes { uint8 v, bytes32 r, bytes32 s - ) public virtual override { } - + ) public virtual override {} } - diff --git a/certora/harnesses/ERC20WrapperHarness.sol b/certora/harnesses/ERC20WrapperHarness.sol index b000afde4..edd3bf7d4 100644 --- a/certora/harnesses/ERC20WrapperHarness.sol +++ b/certora/harnesses/ERC20WrapperHarness.sol @@ -1,11 +1,11 @@ import "../munged/token/ERC20/extensions/ERC20Wrapper.sol"; contract ERC20WrapperHarness is ERC20Wrapper { - - constructor(IERC20 underlyingToken, string memory _name, string memory _symbol) - ERC20Wrapper(underlyingToken) - ERC20(_name, _symbol) - {} + constructor( + IERC20 underlyingToken, + string memory _name, + string memory _symbol + ) ERC20Wrapper(underlyingToken) ERC20(_name, _symbol) {} function underlyingTotalSupply() public view returns (uint256) { return underlying.totalSupply(); @@ -14,4 +14,4 @@ contract ERC20WrapperHarness is ERC20Wrapper { function underlyingBalanceOf(address account) public view returns (uint256) { return underlying.balanceOf(account); } -} \ No newline at end of file +} diff --git a/certora/harnesses/ERC721VotesHarness.sol b/certora/harnesses/ERC721VotesHarness.sol index 9ff8911cd..2741ac9e0 100644 --- a/certora/harnesses/ERC721VotesHarness.sol +++ b/certora/harnesses/ERC721VotesHarness.sol @@ -3,7 +3,7 @@ pragma solidity ^0.8.0; import "../munged/token/ERC721/extensions/draft-ERC721Votes.sol"; contract ERC721VotesHarness is ERC721Votes { - constructor(string memory name, string memory symbol) ERC721(name, symbol) EIP712(name, symbol){} + constructor(string memory name, string memory symbol) ERC721(name, symbol) EIP712(name, symbol) {} function delegateBySig( address delegatee, @@ -23,4 +23,4 @@ contract ERC721VotesHarness is ERC721Votes { function burn(uint256 tokenID) public { _burn(tokenID); } -} \ No newline at end of file +} diff --git a/certora/harnesses/GovernorPreventLateQuorumHarness.sol b/certora/harnesses/GovernorPreventLateQuorumHarness.sol index 7cc9f5b97..2a9e54b66 100644 --- a/certora/harnesses/GovernorPreventLateQuorumHarness.sol +++ b/certora/harnesses/GovernorPreventLateQuorumHarness.sol @@ -9,10 +9,23 @@ import "../munged/governance/extensions/GovernorVotesQuorumFraction.sol"; import "../munged/governance/extensions/GovernorTimelockControl.sol"; import "../munged/token/ERC20/extensions/ERC20Votes.sol"; -contract GovernorPreventLateQuorumHarness is Governor, GovernorCountingSimple, GovernorVotes, GovernorVotesQuorumFraction, GovernorTimelockControl, GovernorPreventLateQuorum { +contract GovernorPreventLateQuorumHarness is + Governor, + GovernorCountingSimple, + GovernorVotes, + GovernorVotesQuorumFraction, + GovernorTimelockControl, + GovernorPreventLateQuorum +{ using SafeCast for uint256; using Timers for Timers.BlockNumber; - constructor(IVotes _token, TimelockController _timelock, uint64 initialVoteExtension, uint256 quorumNumeratorValue) + + constructor( + IVotes _token, + TimelockController _timelock, + uint64 initialVoteExtension, + uint256 quorumNumeratorValue + ) Governor("Harness") GovernorVotes(_token) GovernorVotesQuorumFraction(quorumNumeratorValue) @@ -26,65 +39,71 @@ contract GovernorPreventLateQuorumHarness is Governor, GovernorCountingSimple, G uint256 public latestCastVoteCall; // Harness from GovernorPreventLateQuorum // - - function getVoteExtension() public view returns(uint64) { + + function getVoteExtension() public view returns (uint64) { return _voteExtension; } - function getExtendedDeadlineIsUnset(uint256 proposalId) public view returns(bool) { + function getExtendedDeadlineIsUnset(uint256 proposalId) public view returns (bool) { return _extendedDeadlines[proposalId].isUnset(); } - function getExtendedDeadlineIsStarted(uint256 proposalId) public view returns(bool) { + function getExtendedDeadlineIsStarted(uint256 proposalId) public view returns (bool) { return _extendedDeadlines[proposalId].isStarted(); } - function getExtendedDeadline(uint256 proposalId) public view returns(uint64) { + function getExtendedDeadline(uint256 proposalId) public view returns (uint64) { return _extendedDeadlines[proposalId].getDeadline(); } - // Harness from GovernorCountingSimple // + // Harness from GovernorCountingSimple // - function getAgainstVotes(uint256 proposalId) public view returns(uint256) { + function getAgainstVotes(uint256 proposalId) public view returns (uint256) { ProposalVote storage proposalvote = _proposalVotes[proposalId]; return proposalvote.againstVotes; } - function getAbstainVotes(uint256 proposalId) public view returns(uint256) { + function getAbstainVotes(uint256 proposalId) public view returns (uint256) { ProposalVote storage proposalvote = _proposalVotes[proposalId]; return proposalvote.abstainVotes; } - function getForVotes(uint256 proposalId) public view returns(uint256) { + function getForVotes(uint256 proposalId) public view returns (uint256) { ProposalVote storage proposalvote = _proposalVotes[proposalId]; return proposalvote.forVotes; } - - function quorumReached(uint256 proposalId) public view returns(bool) { + + function quorumReached(uint256 proposalId) public view returns (bool) { return _quorumReached(proposalId); } - function voteSucceeded(uint256 proposalId) public view returns(bool) { + function voteSucceeded(uint256 proposalId) public view returns (bool) { return _voteSucceeded(proposalId); } // Harness from Governor // - function getExecutor() public view returns (address){ + 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 proposalDeadline(uint256 proposalId) public view virtual override(Governor, GovernorPreventLateQuorum, IGovernor) returns (uint256) { + function proposalDeadline(uint256 proposalId) + public + view + virtual + override(Governor, GovernorPreventLateQuorum, IGovernor) + returns (uint256) + { return super.proposalDeadline(proposalId); } @@ -100,7 +119,7 @@ contract GovernorPreventLateQuorumHarness is Governor, GovernorCountingSimple, G // added to run GovernorCountingSimple.spec uint256 deltaWeight = super._castVote(proposalId, account, support, reason, params); - ghost_sum_vote_power_by_id[proposalId] += deltaWeight; + ghost_sum_vote_power_by_id[proposalId] += deltaWeight; return deltaWeight; } @@ -132,44 +151,39 @@ contract GovernorPreventLateQuorumHarness is Governor, GovernorCountingSimple, G return super.quorum(blockNumber); } - function state(uint256 proposalId) - public - view - override(Governor, GovernorTimelockControl) - returns (ProposalState) - { + 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) - { + 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) - { + 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) - { + 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) - { + function _executor() internal view override(Governor, GovernorTimelockControl) returns (address) { return super._executor(); } @@ -181,4 +195,4 @@ contract GovernorPreventLateQuorumHarness is Governor, GovernorCountingSimple, G { return super.supportsInterface(interfaceId); } -} \ No newline at end of file +} diff --git a/certora/harnesses/IERC3156FlashBorrowerHarness.sol b/certora/harnesses/IERC3156FlashBorrowerHarness.sol index 097a5c2fd..131c35be1 100644 --- a/certora/harnesses/IERC3156FlashBorrowerHarness.sol +++ b/certora/harnesses/IERC3156FlashBorrowerHarness.sol @@ -14,7 +14,7 @@ contract IERC3156FlashBorrowerHarness is IERC3156FlashBorrower { uint256 amount, uint256 fee, bytes calldata data - ) external override returns (bytes32){ + ) external override returns (bytes32) { return somethingToReturn; } } diff --git a/certora/harnesses/InitializableBasicHarness.sol b/certora/harnesses/InitializableBasicHarness.sol index 94495ea54..850af3de8 100644 --- a/certora/harnesses/InitializableBasicHarness.sol +++ b/certora/harnesses/InitializableBasicHarness.sol @@ -4,7 +4,6 @@ pragma solidity ^0.8.2; import "../munged/proxy/utils/Initializable.sol"; contract InitializableBasicHarness is Initializable { - uint256 public val; uint256 public a; uint256 public b; @@ -19,13 +18,22 @@ contract InitializableBasicHarness is Initializable { _; } - function initialize(uint256 _val, uint256 _a, uint256 _b) public initializer { + function initialize( + uint256 _val, + uint256 _a, + uint256 _b + ) public initializer { a = _a; b = _b; val = _val; } - function reinitialize(uint256 _val, uint256 _a, uint256 _b, uint8 n) public reinitializer(n) { + function reinitialize( + uint256 _val, + uint256 _a, + uint256 _b, + uint8 n + ) public reinitializer(n) { a = _a; b = _b; val = _val; @@ -33,41 +41,40 @@ contract InitializableBasicHarness is Initializable { // Versioned return functions for testing - function returnsV1() public view version1 returns(uint256) { + function returnsV1() public view version1 returns (uint256) { return val; } - function returnsVN(uint8 n) public view versionN(n) returns(uint256) { + function returnsVN(uint8 n) public view versionN(n) returns (uint256) { return val; } - - function returnsAV1() public view version1 returns(uint256) { + + function returnsAV1() public view version1 returns (uint256) { return a; } - function returnsAVN(uint8 n) public view versionN(n) returns(uint256) { + function returnsAVN(uint8 n) public view versionN(n) returns (uint256) { return a; } - function returnsBV1() public view version1 returns(uint256) { + function returnsBV1() public view version1 returns (uint256) { return b; } - function returnsBVN(uint8 n) public view versionN(n) returns(uint256) { + function returnsBVN(uint8 n) public view versionN(n) returns (uint256) { return b; } // Harness // - function initialized() public view returns(uint8) { + function initialized() public view returns (uint8) { return _initialized; } - function initializing() public view returns(bool) { + function initializing() public view returns (bool) { return _initializing; } - function thisIsContract() public view returns(bool) { + function thisIsContract() public view returns (bool) { return !Address.isContract(address(this)); } - } diff --git a/certora/harnesses/InitializableComplexHarness.sol b/certora/harnesses/InitializableComplexHarness.sol index e76af78bc..730c18704 100644 --- a/certora/harnesses/InitializableComplexHarness.sol +++ b/certora/harnesses/InitializableComplexHarness.sol @@ -5,7 +5,7 @@ import "../munged/proxy/utils/Initializable.sol"; contract InitializableA is Initializable { uint256 public a; - + modifier version1() { require(_initialized == 1); _; @@ -15,30 +15,32 @@ contract InitializableA is Initializable { require(_initialized == n); _; } + function __InitializableA_init(uint256 _a) internal onlyInitializing { a = _a; } - - function returnsAV1() public view version1 returns(uint256) { + + function returnsAV1() public view version1 returns (uint256) { return a; } - function returnsAVN(uint8 n) public view versionN(n) returns(uint256) { + function returnsAVN(uint8 n) public view versionN(n) returns (uint256) { return a; } } contract InitializableB is Initializable, InitializableA { uint256 public b; + function __InitializableB_init(uint256 _b) internal onlyInitializing { b = _b; } - function returnsBV1() public view version1 returns(uint256) { + function returnsBV1() public view version1 returns (uint256) { return b; } - function returnsBVN(uint8 n) public view versionN(n) returns(uint256) { + function returnsBVN(uint8 n) public view versionN(n) returns (uint256) { return b; } } @@ -46,36 +48,45 @@ contract InitializableB is Initializable, InitializableA { contract InitializableComplexHarness is Initializable, InitializableB { uint256 public val; - function initialize(uint256 _val, uint256 _a, uint256 _b) initializer public { + function initialize( + uint256 _val, + uint256 _a, + uint256 _b + ) public initializer { val = _val; __InitializableA_init(_a); __InitializableB_init(_b); } - function reinitialize(uint256 _val, uint256 _a, uint256 _b, uint8 n) reinitializer(n) public { + function reinitialize( + uint256 _val, + uint256 _a, + uint256 _b, + uint8 n + ) public reinitializer(n) { val = _val; __InitializableA_init(_a); __InitializableB_init(_b); } - function returnsV1() public view version1 returns(uint256) { + function returnsV1() public view version1 returns (uint256) { return val; } - function returnsVN(uint8 n) public view versionN(n) returns(uint256) { + function returnsVN(uint8 n) public view versionN(n) returns (uint256) { return val; } // Harness // - function initialized() public view returns(uint8) { + function initialized() public view returns (uint8) { return _initialized; } - function initializing() public view returns(bool) { + function initializing() public view returns (bool) { return _initializing; } - function thisIsContract() public view returns(bool) { + function thisIsContract() public view returns (bool) { return !Address.isContract(address(this)); } } diff --git a/certora/harnesses/TimelockControllerHarness.sol b/certora/harnesses/TimelockControllerHarness.sol index 8c3f794fa..63676be4a 100644 --- a/certora/harnesses/TimelockControllerHarness.sol +++ b/certora/harnesses/TimelockControllerHarness.sol @@ -2,12 +2,10 @@ pragma solidity ^0.8.0; import "../munged/governance/TimelockController.sol"; - contract TimelockControllerHarness is TimelockController { - constructor( +contract TimelockControllerHarness is TimelockController { + constructor( uint256 minDelay, address[] memory proposers, address[] memory executors - ) TimelockController(minDelay, proposers, executors) { - - } -} \ No newline at end of file + ) TimelockController(minDelay, proposers, executors) {} +} diff --git a/certora/harnesses/WizardControlFirstPriority.sol b/certora/harnesses/WizardControlFirstPriority.sol index da9fe8581..856b688fd 100644 --- a/certora/harnesses/WizardControlFirstPriority.sol +++ b/certora/harnesses/WizardControlFirstPriority.sol @@ -16,8 +16,20 @@ ERC20Votes TimelockController */ -contract WizardControlFirstPriority is Governor, GovernorProposalThreshold, GovernorCountingSimple, GovernorVotes, GovernorVotesQuorumFraction, GovernorTimelockControl { - constructor(ERC20Votes _token, TimelockController _timelock, string memory name, uint256 quorumFraction) +contract WizardControlFirstPriority is + Governor, + GovernorProposalThreshold, + GovernorCountingSimple, + GovernorVotes, + GovernorVotesQuorumFraction, + GovernorTimelockControl +{ + constructor( + ERC20Votes _token, + TimelockController _timelock, + string memory name, + uint256 quorumFraction + ) Governor(name) GovernorVotes(_token) GovernorVotesQuorumFraction(quorumFraction) @@ -29,7 +41,7 @@ contract WizardControlFirstPriority is Governor, GovernorProposalThreshold, Gove function isExecuted(uint256 proposalId) public view returns (bool) { return _proposals[proposalId].executed; } - + function isCanceled(uint256 proposalId) public view returns (bool) { return _proposals[proposalId].canceled; } @@ -47,35 +59,36 @@ contract WizardControlFirstPriority is Governor, GovernorProposalThreshold, Gove address account, uint8 support, string memory reason - ) internal override virtual returns (uint256) { - - uint256 deltaWeight = super._castVote(proposalId, account, support, reason); //HARNESS + ) internal virtual override returns (uint256) { + uint256 deltaWeight = super._castVote(proposalId, account, support, reason); //HARNESS ghost_sum_vote_power_by_id[proposalId] += deltaWeight; - return deltaWeight; + return deltaWeight; } - + function snapshot(uint256 proposalId) public view returns (uint64) { return _proposals[proposalId].voteStart._deadline; } - - function getExecutor() public view returns (address){ + function getExecutor() public view returns (address) { return _executor(); } // original code, harnessed - function votingDelay() public view override returns (uint256) { // HARNESS: pure -> view - return _votingDelay; // HARNESS: parametric + function votingDelay() public view override returns (uint256) { + // HARNESS: pure -> view + return _votingDelay; // HARNESS: parametric } - function votingPeriod() public view override returns (uint256) { // HARNESS: pure -> view - return _votingPeriod; // HARNESS: parametric + function votingPeriod() public view override returns (uint256) { + // HARNESS: pure -> view + return _votingPeriod; // HARNESS: parametric } - function proposalThreshold() public view override returns (uint256) { // HARNESS: pure -> view - return _proposalThreshold; // HARNESS: parametric + function proposalThreshold() public view override returns (uint256) { + // HARNESS: pure -> view + return _proposalThreshold; // HARNESS: parametric } // original code, not harnessed @@ -99,44 +112,39 @@ contract WizardControlFirstPriority is Governor, GovernorProposalThreshold, Gove return super.getVotes(account, blockNumber); } - function state(uint256 proposalId) - public - view - override(Governor, GovernorTimelockControl) - returns (ProposalState) - { + 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, GovernorProposalThreshold, IGovernor) - returns (uint256) - { + function propose( + address[] memory targets, + uint256[] memory values, + bytes[] memory calldatas, + string memory description + ) public override(Governor, GovernorProposalThreshold, 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) - { + 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) - { + 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) - { + function _executor() internal view override(Governor, GovernorTimelockControl) returns (address) { return super._executor(); } diff --git a/certora/harnesses/WizardFirstTry.sol b/certora/harnesses/WizardFirstTry.sol index 4e986ed32..2c8b382f1 100644 --- a/certora/harnesses/WizardFirstTry.sol +++ b/certora/harnesses/WizardFirstTry.sol @@ -14,8 +14,19 @@ ERC20Votes TimelockCompound */ -contract WizardFirstTry is Governor, GovernorCountingSimple, GovernorVotes, GovernorVotesQuorumFraction, GovernorTimelockCompound { - constructor(ERC20Votes _token, ICompoundTimelock _timelock, string memory name, uint256 quorumFraction) +contract WizardFirstTry is + Governor, + GovernorCountingSimple, + GovernorVotes, + GovernorVotesQuorumFraction, + GovernorTimelockCompound +{ + constructor( + ERC20Votes _token, + ICompoundTimelock _timelock, + string memory name, + uint256 quorumFraction + ) Governor(name) GovernorVotes(_token) GovernorVotesQuorumFraction(quorumFraction) @@ -27,7 +38,7 @@ contract WizardFirstTry is Governor, GovernorCountingSimple, GovernorVotes, Gove function isExecuted(uint256 proposalId) public view returns (bool) { return _proposals[proposalId].executed; } - + function isCanceled(uint256 proposalId) public view returns (bool) { return _proposals[proposalId].canceled; } @@ -36,7 +47,7 @@ contract WizardFirstTry is Governor, GovernorCountingSimple, GovernorVotes, Gove return _proposals[proposalId].voteStart._deadline; } - function getExecutor() public view returns (address){ + function getExecutor() public view returns (address) { return _executor(); } @@ -51,22 +62,23 @@ contract WizardFirstTry is Governor, GovernorCountingSimple, GovernorVotes, Gove address account, uint8 support, string memory reason - ) internal override virtual returns (uint256) { - - uint256 deltaWeight = super._castVote(proposalId, account, support, reason); //HARNESS + ) internal virtual override returns (uint256) { + uint256 deltaWeight = super._castVote(proposalId, account, support, reason); //HARNESS ghost_sum_vote_power_by_id[proposalId] += deltaWeight; - return deltaWeight; + return deltaWeight; } // original code, harnessed - function votingDelay() public view override virtual returns (uint256) { // HARNESS: pure -> view - return _votingDelay; // HARNESS: parametric + function votingDelay() public view virtual override returns (uint256) { + // HARNESS: pure -> view + return _votingDelay; // HARNESS: parametric } - function votingPeriod() public view override virtual returns (uint256) { // HARNESS: pure -> view - return _votingPeriod; // HARNESS: parametric + function votingPeriod() public view virtual override returns (uint256) { + // HARNESS: pure -> view + return _votingPeriod; // HARNESS: parametric } // original code, not harnessed @@ -99,35 +111,35 @@ contract WizardFirstTry is Governor, GovernorCountingSimple, GovernorVotes, Gove return super.state(proposalId); } - function propose(address[] memory targets, uint256[] memory values, bytes[] memory calldatas, string memory description) - public - override(Governor, IGovernor) - returns (uint256) - { + 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, GovernorTimelockCompound) - { + function _execute( + uint256 proposalId, + address[] memory targets, + uint256[] memory values, + bytes[] memory calldatas, + bytes32 descriptionHash + ) internal override(Governor, GovernorTimelockCompound) { super._execute(proposalId, targets, values, calldatas, descriptionHash); } - function _cancel(address[] memory targets, uint256[] memory values, bytes[] memory calldatas, bytes32 descriptionHash) - internal - override(Governor, GovernorTimelockCompound) - returns (uint256) - { + function _cancel( + address[] memory targets, + uint256[] memory values, + bytes[] memory calldatas, + bytes32 descriptionHash + ) internal override(Governor, GovernorTimelockCompound) returns (uint256) { return super._cancel(targets, values, calldatas, descriptionHash); } - function _executor() - internal - view - override(Governor, GovernorTimelockCompound) - returns (address) - { + function _executor() internal view override(Governor, GovernorTimelockCompound) returns (address) { return super._executor(); }