diff --git a/certora/applyHarness.patch b/certora/applyHarness.patch index 42b10fab5..e7b66d707 100644 --- a/certora/applyHarness.patch +++ b/certora/applyHarness.patch @@ -1,101 +1,242 @@ -diff -ruN .gitignore .gitignore ---- .gitignore 1969-12-31 19:00:00.000000000 -0500 -+++ .gitignore 2021-12-09 14:46:33.923637220 -0500 -@@ -0,0 +1,2 @@ -+* -+!.gitignore -diff -ruN governance/compatibility/GovernorCompatibilityBravo.sol governance/compatibility/GovernorCompatibilityBravo.sol ---- governance/compatibility/GovernorCompatibilityBravo.sol 2021-12-03 15:24:56.523654357 -0500 -+++ governance/compatibility/GovernorCompatibilityBravo.sol 2021-12-09 14:46:33.923637220 -0500 -@@ -245,7 +245,7 @@ - /** - * @dev See {Governor-_quorumReached}. In this module, only forVotes count toward the quorum. - */ -- function _quorumReached(uint256 proposalId) internal view virtual override returns (bool) { -+ function _quorumReached(uint256 proposalId) public view virtual override returns (bool) { // HARNESS: changed to public from internal - ProposalDetails storage details = _proposalDetails[proposalId]; - return quorum(proposalSnapshot(proposalId)) <= details.forVotes; - } -@@ -253,7 +253,7 @@ - /** - * @dev See {Governor-_voteSucceeded}. In this module, the forVotes must be scritly over the againstVotes. - */ -- function _voteSucceeded(uint256 proposalId) internal view virtual override returns (bool) { -+ function _voteSucceeded(uint256 proposalId) public view virtual override returns (bool) { // HARNESS: changed to public from internal - ProposalDetails storage details = _proposalDetails[proposalId]; - return details.forVotes > details.againstVotes; - } -diff -ruN governance/extensions/GovernorCountingSimple.sol governance/extensions/GovernorCountingSimple.sol ---- governance/extensions/GovernorCountingSimple.sol 2021-12-03 15:24:56.523654357 -0500 -+++ governance/extensions/GovernorCountingSimple.sol 2021-12-09 14:46:33.923637220 -0500 -@@ -64,7 +64,7 @@ - /** - * @dev See {Governor-_quorumReached}. - */ -- function _quorumReached(uint256 proposalId) internal view virtual override returns (bool) { -+ function _quorumReached(uint256 proposalId) public view virtual override returns (bool) { - ProposalVote storage proposalvote = _proposalVotes[proposalId]; - - return quorum(proposalSnapshot(proposalId)) <= proposalvote.forVotes + proposalvote.abstainVotes; -@@ -73,7 +73,7 @@ - /** - * @dev See {Governor-_voteSucceeded}. In this module, the forVotes must be strictly over the againstVotes. - */ -- function _voteSucceeded(uint256 proposalId) internal view virtual override returns (bool) { -+ function _voteSucceeded(uint256 proposalId) public view virtual override returns (bool) { - ProposalVote storage proposalvote = _proposalVotes[proposalId]; - - return proposalvote.forVotes > proposalvote.againstVotes; -diff -ruN governance/extensions/GovernorTimelockControl.sol governance/extensions/GovernorTimelockControl.sol ---- governance/extensions/GovernorTimelockControl.sol 2021-12-03 15:24:56.523654357 -0500 -+++ governance/extensions/GovernorTimelockControl.sol 2021-12-09 14:46:33.923637220 -0500 -@@ -111,7 +111,7 @@ - bytes[] memory calldatas, - bytes32 descriptionHash - ) internal virtual override { -- _timelock.executeBatch{value: msg.value}(targets, values, calldatas, 0, descriptionHash); -+ _timelock.executeBatch{value: msg.value}(targets, values, calldatas, 0, descriptionHash); - } - - /** -diff -ruN governance/Governor.sol governance/Governor.sol ---- governance/Governor.sol 2021-12-03 15:24:56.523654357 -0500 -+++ governance/Governor.sol 2021-12-09 14:46:56.411503587 -0500 -@@ -38,8 +38,8 @@ - - string private _name; - -- mapping(uint256 => ProposalCore) private _proposals; -- -+ mapping(uint256 => ProposalCore) public _proposals; -+ - /** - * @dev Restrict access to governor executing address. Some module might override the _executor function to make - * sure this modifier is consistant with the execution model. -@@ -167,12 +167,12 @@ - /** - * @dev Amount of votes already cast passes the threshold limit. - */ -- function _quorumReached(uint256 proposalId) internal view virtual returns (bool); -+ function _quorumReached(uint256 proposalId) public view virtual returns (bool); // HARNESS: changed to public from internal - - /** - * @dev Is the proposal successful or not. - */ -- function _voteSucceeded(uint256 proposalId) internal view virtual returns (bool); -+ function _voteSucceeded(uint256 proposalId) public view virtual returns (bool); // HARNESS: changed to public from internal - - /** - * @dev Register a vote with a given support and voting weight. -diff -ruN token/ERC20/extensions/ERC20Votes.sol token/ERC20/extensions/ERC20Votes.sol ---- token/ERC20/extensions/ERC20Votes.sol 2021-12-03 15:24:56.527654330 -0500 -+++ token/ERC20/extensions/ERC20Votes.sol 2021-12-09 14:46:33.927637196 -0500 -@@ -84,7 +84,7 @@ +diff -ruN access/AccessControl.sol access/AccessControl.sol +--- access/AccessControl.sol 2022-03-02 09:14:55.000000000 -0800 ++++ access/AccessControl.sol 2022-03-24 16:41:46.000000000 -0700 +@@ -93,7 +93,7 @@ * - * - `blockNumber` must have been already mined + * _Available since v4.6._ */ -- function getPastVotes(address account, uint256 blockNumber) public view returns (uint256) { -+ function getPastVotes(address account, uint256 blockNumber) public view virtual returns (uint256) { - require(blockNumber < block.number, "ERC20Votes: block not yet mined"); - return _checkpointsLookup(_checkpoints[account], blockNumber); +- function _checkRole(bytes32 role) internal view virtual { ++ function _checkRole(bytes32 role) public view virtual { // HARNESS: internal -> public + _checkRole(role, _msgSender()); } + +diff -ruN governance/TimelockController.sol governance/TimelockController.sol +--- governance/TimelockController.sol 2022-03-02 09:14:55.000000000 -0800 ++++ governance/TimelockController.sol 2022-03-24 16:41:46.000000000 -0700 +@@ -24,10 +24,10 @@ + bytes32 public constant TIMELOCK_ADMIN_ROLE = keccak256("TIMELOCK_ADMIN_ROLE"); + bytes32 public constant PROPOSER_ROLE = keccak256("PROPOSER_ROLE"); + bytes32 public constant EXECUTOR_ROLE = keccak256("EXECUTOR_ROLE"); +- uint256 internal constant _DONE_TIMESTAMP = uint256(1); ++ uint256 public constant _DONE_TIMESTAMP = uint256(1); // HARNESS: internal -> public + + mapping(bytes32 => uint256) private _timestamps; +- uint256 private _minDelay; ++ uint256 public _minDelay; // HARNESS: private -> public + + /** + * @dev Emitted when a call is scheduled as part of operation `id`. +@@ -353,4 +353,11 @@ + emit MinDelayChange(_minDelay, newDelay); + _minDelay = newDelay; + } +-} ++ ++ ++ ++ function scheduleCheck1(bytes32 id) public virtual onlyRole(PROPOSER_ROLE) { ++ bool tmp = false; ++ require(tmp); ++ } ++} +diff -ruN governance/utils/Votes.sol governance/utils/Votes.sol +--- governance/utils/Votes.sol 2022-03-02 09:14:55.000000000 -0800 ++++ governance/utils/Votes.sol 2022-03-24 16:41:46.000000000 -0700 +@@ -207,5 +207,5 @@ + /** + * @dev Must return the voting units held by an account. + */ +- function _getVotingUnits(address) internal virtual returns (uint256); ++ function _getVotingUnits(address) public virtual returns (uint256); // HARNESS: internal -> public + } +diff -ruN token/ERC20/ERC20.sol token/ERC20/ERC20.sol +--- token/ERC20/ERC20.sol 2022-03-02 09:14:55.000000000 -0800 ++++ token/ERC20/ERC20.sol 2022-03-24 16:41:46.000000000 -0700 +@@ -277,7 +277,7 @@ + * - `account` cannot be the zero address. + * - `account` must have at least `amount` tokens. + */ +- function _burn(address account, uint256 amount) internal virtual { ++ function _burn(address account, uint256 amount) public virtual returns (bool) { // HARNESS: internal -> public + require(account != address(0), "ERC20: burn from the zero address"); + + _beforeTokenTransfer(account, address(0), amount); +@@ -292,6 +292,8 @@ + emit Transfer(account, address(0), amount); + + _afterTokenTransfer(account, address(0), amount); ++ ++ return true; + } + + /** +diff -ruN token/ERC20/extensions/ERC20FlashMint.sol token/ERC20/extensions/ERC20FlashMint.sol +--- token/ERC20/extensions/ERC20FlashMint.sol 2022-03-02 09:14:55.000000000 -0800 ++++ token/ERC20/extensions/ERC20FlashMint.sol 2022-03-24 16:41:46.000000000 -0700 +@@ -40,9 +40,11 @@ + require(token == address(this), "ERC20FlashMint: wrong token"); + // silence warning about unused variable without the addition of bytecode. + amount; +- return 0; ++ return fee; // HARNESS: made "return" nonzero + } + ++ uint256 public fee; // HARNESS: added it to simulate random fee amount ++ + /** + * @dev Performs a flash loan. New tokens are minted and sent to the + * `receiver`, who is required to implement the {IERC3156FlashBorrower} +@@ -70,7 +72,7 @@ + uint256 fee = flashFee(token, amount); + _mint(address(receiver), amount); + require( +- receiver.onFlashLoan(msg.sender, token, amount, fee, data) == _RETURN_VALUE, ++ receiver.onFlashLoan(msg.sender, token, amount, fee, data) == _RETURN_VALUE, // HAVOC_ALL + "ERC20FlashMint: invalid return value" + ); + uint256 currentAllowance = allowance(address(receiver), address(this)); +diff -ruN token/ERC20/extensions/ERC20Votes.sol token/ERC20/extensions/ERC20Votes.sol +--- token/ERC20/extensions/ERC20Votes.sol 2022-03-02 09:14:55.000000000 -0800 ++++ token/ERC20/extensions/ERC20Votes.sol 2022-03-24 17:15:51.000000000 -0700 +@@ -33,8 +33,8 @@ + bytes32 private constant _DELEGATION_TYPEHASH = + keccak256("Delegation(address delegatee,uint256 nonce,uint256 expiry)"); + +- mapping(address => address) private _delegates; +- mapping(address => Checkpoint[]) private _checkpoints; ++ mapping(address => address) public _delegates; ++ mapping(address => Checkpoint[]) public _checkpoints; + Checkpoint[] private _totalSupplyCheckpoints; + + /** +@@ -152,7 +152,7 @@ + /** + * @dev Maximum token supply. Defaults to `type(uint224).max` (2^224^ - 1). + */ +- function _maxSupply() internal view virtual returns (uint224) { ++ function _maxSupply() public view virtual returns (uint224) { //harnessed to public + return type(uint224).max; + } + +@@ -163,16 +163,17 @@ + super._mint(account, amount); + require(totalSupply() <= _maxSupply(), "ERC20Votes: total supply risks overflowing votes"); + +- _writeCheckpoint(_totalSupplyCheckpoints, _add, amount); ++ _writeCheckpointAdd(_totalSupplyCheckpoints, amount); // HARNESS: new version without pointer + } + + /** + * @dev Snapshots the totalSupply after it has been decreased. + */ +- function _burn(address account, uint256 amount) internal virtual override { ++ function _burn(address account, uint256 amount) public virtual override returns (bool){ // HARNESS: internal -> public (to comply with the ERC20 harness) + super._burn(account, amount); + +- _writeCheckpoint(_totalSupplyCheckpoints, _subtract, amount); ++ _writeCheckpointSub(_totalSupplyCheckpoints, amount); // HARNESS: new version without pointer ++ return true; + } + + /** +@@ -187,7 +188,7 @@ + ) internal virtual override { + super._afterTokenTransfer(from, to, amount); + +- _moveVotingPower(delegates(from), delegates(to), amount); ++ _moveVotingPower(delegates(from), delegates(to), amount); + } + + /** +@@ -195,7 +196,7 @@ + * + * Emits events {DelegateChanged} and {DelegateVotesChanged}. + */ +- function _delegate(address delegator, address delegatee) internal virtual { ++ function _delegate(address delegator, address delegatee) public virtual { // HARNESSED TO MAKE PUBLIC + address currentDelegate = delegates(delegator); + uint256 delegatorBalance = balanceOf(delegator); + _delegates[delegator] = delegatee; +@@ -212,25 +213,25 @@ + ) private { + if (src != dst && amount > 0) { + if (src != address(0)) { +- (uint256 oldWeight, uint256 newWeight) = _writeCheckpoint(_checkpoints[src], _subtract, amount); ++ (uint256 oldWeight, uint256 newWeight) = _writeCheckpointSub(_checkpoints[src], amount); // HARNESS: new version without pointer + emit DelegateVotesChanged(src, oldWeight, newWeight); + } + + if (dst != address(0)) { +- (uint256 oldWeight, uint256 newWeight) = _writeCheckpoint(_checkpoints[dst], _add, amount); ++ (uint256 oldWeight, uint256 newWeight) = _writeCheckpointAdd(_checkpoints[dst], amount); // HARNESS: new version without pointer + emit DelegateVotesChanged(dst, oldWeight, newWeight); + } + } + } + +- function _writeCheckpoint( ++ // HARNESS: split _writeCheckpoint() to two functions as a workaround for function pointers that cannot be managed by the tool ++ function _writeCheckpointAdd( + Checkpoint[] storage ckpts, +- function(uint256, uint256) view returns (uint256) op, + uint256 delta + ) private returns (uint256 oldWeight, uint256 newWeight) { + uint256 pos = ckpts.length; + oldWeight = pos == 0 ? 0 : ckpts[pos - 1].votes; +- newWeight = op(oldWeight, delta); ++ newWeight = _add(oldWeight, delta); + + if (pos > 0 && ckpts[pos - 1].fromBlock == block.number) { + ckpts[pos - 1].votes = SafeCast.toUint224(newWeight); +@@ -239,6 +240,39 @@ + } + } + ++ function _writeCheckpointSub( ++ Checkpoint[] storage ckpts, ++ uint256 delta ++ ) private returns (uint256 oldWeight, uint256 newWeight) { ++ uint256 pos = ckpts.length; ++ oldWeight = pos == 0 ? 0 : ckpts[pos - 1].votes; ++ newWeight = _subtract(oldWeight, delta); ++ ++ if (pos > 0 && ckpts[pos - 1].fromBlock == block.number) { ++ ckpts[pos - 1].votes = SafeCast.toUint224(newWeight); ++ } else { ++ ckpts.push(Checkpoint({fromBlock: SafeCast.toUint32(block.number), votes: SafeCast.toUint224(newWeight)})); ++ } ++ } ++ ++ // backup of original function ++ // ++ // function _writeCheckpoint( ++ // Checkpoint[] storage ckpts, ++ // function(uint256, uint256) view returns (uint256) op, ++ // uint256 delta ++ // ) private returns (uint256 oldWeight, uint256 newWeight) { ++ // uint256 pos = ckpts.length; ++ // oldWeight = pos == 0 ? 0 : ckpts[pos - 1].votes; ++ // newWeight = op(oldWeight, delta); ++ // ++ // if (pos > 0 && ckpts[pos - 1].fromBlock == block.number) { ++ // ckpts[pos - 1].votes = SafeCast.toUint224(newWeight); ++ // } else { ++ // ckpts.push(Checkpoint({fromBlock: SafeCast.toUint32(block.number), votes: SafeCast.toUint224(newWeight)})); ++ // } ++ // } ++ + function _add(uint256 a, uint256 b) private pure returns (uint256) { + return a + b; + } +diff -ruN token/ERC20/extensions/ERC20Wrapper.sol token/ERC20/extensions/ERC20Wrapper.sol +--- token/ERC20/extensions/ERC20Wrapper.sol 2022-03-02 09:14:55.000000000 -0800 ++++ token/ERC20/extensions/ERC20Wrapper.sol 2022-03-24 16:41:46.000000000 -0700 +@@ -44,7 +44,7 @@ + * @dev Mint wrapped token to cover any underlyingTokens that would have been transferred by mistake. Internal + * function that can be exposed with access control if desired. + */ +- function _recover(address account) internal virtual returns (uint256) { ++ function _recover(address account) public virtual returns (uint256) { // HARNESS: internal -> public + uint256 value = underlying.balanceOf(address(this)) - totalSupply(); + _mint(account, value); + return value; diff --git a/certora/harnesses/ERC20VotesHarness.sol b/certora/harnesses/ERC20VotesHarness.sol index 3bf03732f..14b170bbf 100644 --- a/certora/harnesses/ERC20VotesHarness.sol +++ b/certora/harnesses/ERC20VotesHarness.sol @@ -2,4 +2,21 @@ import "../munged/token/ERC20/extensions/ERC20Votes.sol"; contract ERC20VotesHarness is ERC20Votes { constructor(string memory name, string memory symbol) ERC20Permit(name) ERC20(name, symbol) {} + + 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; + } + + function mint(address account, uint256 amount) public { + _mint(account, amount); + } + + function burn(address account, uint256 amount) public { + _burn(account, amount); + } } + diff --git a/certora/munged/token/ERC20/extensions/ERC20Votes.sol b/certora/munged/token/ERC20/extensions/ERC20Votes.sol index be127239b..a8de4825e 100644 --- a/certora/munged/token/ERC20/extensions/ERC20Votes.sol +++ b/certora/munged/token/ERC20/extensions/ERC20Votes.sol @@ -33,8 +33,8 @@ abstract contract ERC20Votes is IVotes, ERC20Permit { bytes32 private constant _DELEGATION_TYPEHASH = keccak256("Delegation(address delegatee,uint256 nonce,uint256 expiry)"); - mapping(address => address) private _delegates; - mapping(address => Checkpoint[]) private _checkpoints; + mapping(address => address) public _delegates; + mapping(address => Checkpoint[]) public _checkpoints; Checkpoint[] private _totalSupplyCheckpoints; /** @@ -152,7 +152,7 @@ abstract contract ERC20Votes is IVotes, ERC20Permit { /** * @dev Maximum token supply. Defaults to `type(uint224).max` (2^224^ - 1). */ - function _maxSupply() internal view virtual returns (uint224) { + function _maxSupply() public view virtual returns (uint224) { //harnessed to public return type(uint224).max; } @@ -169,10 +169,11 @@ abstract contract ERC20Votes is IVotes, ERC20Permit { /** * @dev Snapshots the totalSupply after it has been decreased. */ - function _burn(address account, uint256 amount) internal virtual override { + function _burn(address account, uint256 amount) public virtual override returns (bool){ // HARNESS: internal -> public (to comply with the ERC20 harness) super._burn(account, amount); _writeCheckpointSub(_totalSupplyCheckpoints, amount); // HARNESS: new version without pointer + return true; } /** @@ -195,7 +196,7 @@ abstract contract ERC20Votes is IVotes, ERC20Permit { * * Emits events {DelegateChanged} and {DelegateVotesChanged}. */ - function _delegate(address delegator, address delegatee) internal virtual { + function _delegate(address delegator, address delegatee) public virtual { // HARNESSED TO MAKE PUBLIC address currentDelegate = delegates(delegator); uint256 delegatorBalance = balanceOf(delegator); _delegates[delegator] = delegatee; diff --git a/certora/scripts/ERC20VotesRule.sh b/certora/scripts/ERC20VotesRule.sh new file mode 100644 index 000000000..a29fd1ff9 --- /dev/null +++ b/certora/scripts/ERC20VotesRule.sh @@ -0,0 +1,23 @@ +if [ -z "$2" ] + then + echo "Incorrect number of arguments" + echo "" + echo "Usage: (from git root)" + echo " ./certora/scripts/`basename $0` [message describing the run] [rule or invariant]" + echo "" + exit 1 +fi + +rule=$1 +msg=$2 +shift 2 + +certoraRun \ + certora/harnesses/ERC20VotesHarness.sol \ + --verify ERC20VotesHarness:certora/specs/ERC20Votes.spec \ + --solc solc8.2 \ + --optimistic_loop \ + --rule ${rule} \ + --msg "${msg}" \ + --staging \ + # --rule_sanity \ \ No newline at end of file diff --git a/certora/scripts/verifyERC20Votes.sh b/certora/scripts/verifyERC20Votes.sh index bb8c8e749..7b23e29fe 100644 --- a/certora/scripts/verifyERC20Votes.sh +++ b/certora/scripts/verifyERC20Votes.sh @@ -1,7 +1,22 @@ +make -C certora munged + +if [ -z "$1" ] + then + echo "Incorrect number of arguments" + echo "" + echo "Usage: (from git root)" + echo " ./certora/scripts/`basename $0` [message describing the run]" + echo "" + exit 1 +fi + +msg=$1 +shift 1 + certoraRun \ certora/harnesses/ERC20VotesHarness.sol \ --verify ERC20VotesHarness:certora/specs/ERC20Votes.spec \ --solc solc8.2 \ --optimistic_loop \ - --cloud \ - --msg "sanityVotes" + --loop_iter 4 \ + --msg "${msg}" diff --git a/certora/specs/ERC20Votes.spec b/certora/specs/ERC20Votes.spec index b08c6cf4e..7adb3cca1 100644 --- a/certora/specs/ERC20Votes.spec +++ b/certora/specs/ERC20Votes.spec @@ -1,6 +1,314 @@ +using ERC20VotesHarness as erc20votes + +methods { + // functions + checkpoints(address, uint32) envfree + numCheckpoints(address) returns (uint32) envfree + delegates(address) returns (address) envfree + getVotes(address) returns (uint256) envfree + getPastVotes(address, uint256) returns (uint256) + getPastTotalSupply(uint256) returns (uint256) + delegate(address) + _delegate(address, address) + delegateBySig(address, uint256, uint256, uint8, bytes32, bytes32) + totalSupply() returns (uint256) envfree + _maxSupply() returns (uint224) envfree + + // harnesss functions + ckptFromBlock(address, uint32) returns (uint32) envfree + ckptVotes(address, uint32) returns (uint224) envfree + mint(address, uint256) + burn(address, uint256) + + // solidity generated getters + _delegates(address) returns (address) envfree + + // external functions + + +} +// gets the most recent votes for a user +ghost userVotes(address) returns uint224; + +// sums the total votes for all users +ghost totalVotes() returns mathint { + axiom totalVotes() > 0; +} + + + +hook Sstore _checkpoints[KEY address account][INDEX uint32 index].votes uint224 newVotes (uint224 oldVotes) STORAGE { + havoc userVotes assuming + userVotes@new(account) == newVotes; + + havoc totalVotes assuming + totalVotes@new() == totalVotes@old() + to_mathint(newVotes) - to_mathint(userVotes(account)); +} + + +ghost lastFromBlock(address) returns uint32; + +ghost doubleFromBlock(address) returns bool { + init_state axiom forall address a. doubleFromBlock(a) == false; +} + + +hook Sstore _checkpoints[KEY address account][INDEX uint32 index].fromBlock uint32 newBlock (uint32 oldBlock) STORAGE { + havoc lastFromBlock assuming + lastFromBlock@new(account) == newBlock; + + havoc doubleFromBlock assuming + doubleFromBlock@new(account) == (newBlock == oldBlock); +} + rule sanity(method f) { env e; calldataarg arg; f(e, arg); assert false; -} \ No newline at end of file +} + +// something stupid just to see +invariant sanity_invariant() + totalSupply() >= 0 + +// sum of user balances is >= total amount of delegated votes +invariant votes_solvency() + to_mathint(totalSupply()) >= totalVotes() + +// for some checkpoint, the fromBlock is less than the current block number +// passes but fails rule sanity from hash on delegate by sig +invariant timestamp_constrains_fromBlock(address account, uint32 index, env e) + ckptFromBlock(account, index) < e.block.number +{ + preserved { + require index < numCheckpoints(account); + } +} + +// numCheckpoints are less than maxInt +// passes +invariant maxInt_constrains_numBlocks(address account) + numCheckpoints(account) <= 4294967295 // 2^32 + +// can't have more checkpoints for a given account than the last from block +invariant fromBlock_constrains_numBlocks(address account) + numCheckpoints(account) <= lastFromBlock(account) + +invariant unique_checkpoints(address account) + !doubleFromBlock(account) + +rule transfer_safe() { + env e; + uint256 amount; + address a; address b; + require a != b; + + uint256 votesA_pre = getVotes(a); + uint256 votesB_pre = getVotes(b); + + require votesA_pre == erc20votes.balanceOf(e, a); + require votesB_pre == erc20votes.balanceOf(e, b); + + mathint totalVotes_pre = totalVotes(); + + erc20votes.transferFrom(e, a, b, amount); + + mathint totalVotes_post = totalVotes(); + uint256 votesA_post = getVotes(a); + uint256 votesB_post = getVotes(b); + + assert totalVotes_pre == totalVotes_post, "transfer changed total supply"; + assert votesA_pre - votesA_post == amount, "a lost the proper amount of votes"; + assert votesB_post - votesB_pre == amount, "b lost the proper amount of votes"; +} + + +rule delegator_votes_removed() { + env e; + address delegator; address delegatee; + + require delegator != delegatee; + require delegates(delegator) == 0; // has not delegated + + uint256 pre = getVotes(delegator); + + _delegate(e, delegator, delegatee); + + uint256 balance = balanceOf(e, delegator); + + uint256 post = getVotes(delegator); + assert post == pre - balance, "delegator retained votes"; +} + +rule delegatee_receives_votes() { + env e; + address delegator; address delegatee; + require delegator != delegatee; + + uint256 delegator_bal = balanceOf(e, delegator); + uint256 votes_= getVotes(delegatee); + + _delegate(e, delegator, delegatee); + + uint256 _votes = getVotes(delegatee); + + assert _votes == votes_ + delegator_bal, "delegatee did not receive votes"; +} + +rule previous_delegatee_zerod() { + env e; + address delegator; address delegatee; address third; + + require delegator != delegatee; + require third != delegatee; + require third != delegator; + + uint256 delegator_bal = balanceOf(e, delegator); + uint256 votes_ = getVotes(third); + + _delegate(e, delegator, delegatee); + + uint256 _votes = getVotes(third); + + assert votes_ == votes_ - delegator_bal, "votes not removed from the previous delegatee"; +} + +// passes +rule delegate_contained() { + env e; + address delegator; address delegatee; address other; + + require delegator != delegatee; + require other != delegator; + require other != delegatee; + require other != delegates(delegator); + + uint256 votes_ = getVotes(other); + + _delegate(e, delegator, delegatee); + + uint256 _votes = getVotes(other); + + assert votes_ == _votes, "votes not contained"; +} + +// checks all of the above rules with front running +rule delegate_no_frontrunning(method f) { + env e; calldataarg args; + address delegator; address delegatee; address third; address other; + + require delegator != delegatee; + require delegates(delegator) == third; + require other != third; + + uint256 delegator_bal = erc20votes.balanceOf(e, delegator); + + uint256 dr_ = getVotes(delegator); + uint256 de_ = getVotes(delegatee); + uint256 third_ = getVotes(third); + uint256 other_ = getVotes(other); + + // require third is address for previous delegator + f(e, args); + _delegate(e, delegator, delegatee); + + uint256 _dr = getVotes(delegator); + uint256 _de = getVotes(delegatee); + uint256 _third = getVotes(third); + uint256 _other = getVotes(other); + + + // delegator loses all of their votes + // delegatee gains that many votes + // third loses any votes delegated to them + assert _dr == 0, "delegator retained votes"; + assert _de == de_ + delegator_bal, "delegatee not received votes"; + assert _third != 0 => _third == third_ - delegator_bal, "votes not removed from third"; + assert other_ == _other, "delegate not contained"; +} + +// passes +rule mint_increases_totalSupply() { + + env e; + uint256 amount; address account; + + uint256 fromBlock = e.block.number; + uint256 totalSupply_ = totalSupply(); + + mint(e, account, amount); + + uint256 _totalSupply = totalSupply(); + require _totalSupply < _maxSupply(); + + assert _totalSupply == totalSupply_ + amount, "totalSupply not increased properly"; + assert getPastTotalSupply(e, fromBlock) == totalSupply_ , "previous total supply not saved properly"; +} + +// passes +rule burn_decreases_totalSupply() { + env e; + uint256 amount; address account; + + uint256 fromBlock = e.block.number; + uint256 totalSupply_ = totalSupply(); + require totalSupply_ > balanceOf(e, account); + + burn(e, account, amount); + + uint256 _totalSupply = totalSupply(); + require _totalSupply < _maxSupply(); + + assert _totalSupply == totalSupply_ - amount, "totalSupply not decreased properly"; + assert getPastTotalSupply(e, fromBlock) == totalSupply_ , "previous total supply not saved properly"; +} + + + +// passes +rule mint_doesnt_increase_totalVotes() { + env e; + uint256 amount; address account; + + mathint totalVotes_ = totalVotes(); + + mint(e, account, amount); + + assert totalVotes() == totalVotes_, "totalVotes increased"; +} +// passes +rule burn_doesnt_decrease_totalVotes() { + env e; + uint256 amount; address account; + + mathint totalVotes_ = totalVotes(); + + burn(e, account, amount); + + assert totalVotes() == totalVotes_, "totalVotes decreased"; +} + +// // fails +// rule mint_increases_totalVotes() { +// env e; +// uint256 amount; address account; + +// mathint totalVotes_ = totalVotes(); + +// mint(e, account, amount); + +// assert totalVotes() == totalVotes_ + to_mathint(amount), "totalVotes not increased"; +// } + +// // fails +// rule burn_decreases_totalVotes() { +// env e; +// uint256 amount; address account; + +// mathint totalVotes_ = totalVotes(); + +// burn(e, account, amount); + +// assert totalVotes() == totalVotes_ - to_mathint(amount), "totalVotes not decreased"; +// }