diff --git a/certora/applyHarness.patch b/certora/applyHarness.patch index 7af5f82c8..3957b54f3 100644 --- a/certora/applyHarness.patch +++ b/certora/applyHarness.patch @@ -1,6 +1,6 @@ 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 18:08:46.000000000 -0700 ++++ access/AccessControl.sol 2022-04-08 17:31:22.000000000 -0700 @@ -93,7 +93,7 @@ * * _Available since v4.6._ @@ -12,7 +12,7 @@ diff -ruN access/AccessControl.sol access/AccessControl.sol 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 18:08:46.000000000 -0700 ++++ governance/TimelockController.sol 2022-04-08 17:31:22.000000000 -0700 @@ -24,10 +24,10 @@ bytes32 public constant TIMELOCK_ADMIN_ROLE = keccak256("TIMELOCK_ADMIN_ROLE"); bytes32 public constant PROPOSER_ROLE = keccak256("PROPOSER_ROLE"); @@ -26,32 +26,147 @@ diff -ruN governance/TimelockController.sol governance/TimelockController.sol /** * @dev Emitted when a call is scheduled as part of operation `id`. -@@ -353,4 +353,11 @@ +@@ -353,4 +353,4 @@ 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 18:08:46.000000000 -0700 -@@ -207,5 +207,5 @@ ++++ governance/utils/Votes.sol 2022-04-08 17:44:19.000000000 -0700 +@@ -35,7 +35,25 @@ + bytes32 private constant _DELEGATION_TYPEHASH = + keccak256("Delegation(address delegatee,uint256 nonce,uint256 expiry)"); + +- mapping(address => address) private _delegation; ++ // HARNESS : Hooks cannot access any information from Checkpoints yet, so I am also updating votes and fromBlock in this struct ++ struct Ckpt { ++ uint32 fromBlock; ++ uint224 votes; ++ } ++ mapping(address => Ckpt) public _checkpoints; ++ ++ // HARNESSED getters ++ function numCheckpoints(address account) public view returns (uint32) { ++ return SafeCast.toUint32(_delegateCheckpoints[account]._checkpoints.length); ++ } ++ function ckptFromBlock(address account, uint32 pos) public view returns (uint32) { ++ return _delegateCheckpoints[account]._checkpoints[pos]._blockNumber; ++ } ++ function ckptVotes(address account, uint32 pos) public view returns (uint224) { ++ return _delegateCheckpoints[account]._checkpoints[pos]._value; ++ } ++ ++ mapping(address => address) public _delegation; + mapping(address => Checkpoints.History) private _delegateCheckpoints; + Checkpoints.History private _totalCheckpoints; + +@@ -124,7 +142,7 @@ + * + * Emits events {DelegateChanged} and {DelegateVotesChanged}. + */ +- function _delegate(address account, address delegatee) internal virtual { ++ function _delegate(address account, address delegatee) public virtual { + address oldDelegate = delegates(account); + _delegation[account] = delegatee; + +@@ -142,10 +160,10 @@ + uint256 amount + ) internal virtual { + if (from == address(0)) { +- _totalCheckpoints.push(_add, amount); ++ _totalCheckpoints.push(_totalCheckpoints.latest() + amount); // Harnessed to remove function pointers + } + if (to == address(0)) { +- _totalCheckpoints.push(_subtract, amount); ++ _totalCheckpoints.push(_totalCheckpoints.latest() - amount); // Harnessed to remove function pointers + } + _moveDelegateVotes(delegates(from), delegates(to), amount); + } +@@ -160,11 +178,13 @@ + ) private { + if (from != to && amount > 0) { + if (from != address(0)) { +- (uint256 oldValue, uint256 newValue) = _delegateCheckpoints[from].push(_subtract, amount); ++ (uint256 oldValue, uint256 newValue) = _delegateCheckpoints[from].push(_delegateCheckpoints[from].latest() - amount); // HARNESSED TO REMOVE FUNCTION POINTERS ++ _checkpoints[from] = Ckpt({fromBlock: SafeCast.toUint32(block.number), votes: SafeCast.toUint224(newValue)}); // HARNESS + emit DelegateVotesChanged(from, oldValue, newValue); + } + if (to != address(0)) { +- (uint256 oldValue, uint256 newValue) = _delegateCheckpoints[to].push(_add, amount); ++ (uint256 oldValue, uint256 newValue) = _delegateCheckpoints[to].push(_delegateCheckpoints[to].latest() + amount); // HARNESSED TO REMOVE FUNCTION POINTERS ++ _checkpoints[to] = Ckpt({fromBlock: SafeCast.toUint32(block.number), votes: SafeCast.toUint224(newValue)}); // HARNESS + emit DelegateVotesChanged(to, oldValue, newValue); + } + } +@@ -207,5 +227,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/ERC1155/ERC1155.sol token/ERC1155/ERC1155.sol +--- token/ERC1155/ERC1155.sol 2022-03-02 09:14:55.000000000 -0800 ++++ token/ERC1155/ERC1155.sol 2022-04-08 17:31:22.000000000 -0700 +@@ -268,7 +268,7 @@ + uint256 id, + uint256 amount, + bytes memory data +- ) internal virtual { ++ ) public virtual { // HARNESS: internal -> public + require(to != address(0), "ERC1155: mint to the zero address"); + + address operator = _msgSender(); +@@ -299,7 +299,7 @@ + uint256[] memory ids, + uint256[] memory amounts, + bytes memory data +- ) internal virtual { ++ ) public virtual { // HARNESS: internal -> public + require(to != address(0), "ERC1155: mint to the zero address"); + require(ids.length == amounts.length, "ERC1155: ids and amounts length mismatch"); + +@@ -330,7 +330,7 @@ + address from, + uint256 id, + uint256 amount +- ) internal virtual { ++ ) public virtual { // HARNESS: internal -> public + require(from != address(0), "ERC1155: burn from the zero address"); + + address operator = _msgSender(); +@@ -361,7 +361,7 @@ + address from, + uint256[] memory ids, + uint256[] memory amounts +- ) internal virtual { ++ ) public virtual { // HARNESS: internal -> public + require(from != address(0), "ERC1155: burn from the zero address"); + require(ids.length == amounts.length, "ERC1155: ids and amounts length mismatch"); + +@@ -465,7 +465,7 @@ + uint256 id, + uint256 amount, + bytes memory data +- ) private { ++ ) public { // HARNESS: private -> public + if (to.isContract()) { + try IERC1155Receiver(to).onERC1155Received(operator, from, id, amount, data) returns (bytes4 response) { + if (response != IERC1155Receiver.onERC1155Received.selector) { +@@ -486,7 +486,7 @@ + uint256[] memory ids, + uint256[] memory amounts, + bytes memory data +- ) private { ++ ) public { // HARNESS: private -> public + if (to.isContract()) { + try IERC1155Receiver(to).onERC1155BatchReceived(operator, from, ids, amounts, data) returns ( + bytes4 response 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 18:08:46.000000000 -0700 ++++ token/ERC20/ERC20.sol 2022-04-08 17:31:22.000000000 -0700 @@ -277,7 +277,7 @@ * - `account` cannot be the zero address. * - `account` must have at least `amount` tokens. @@ -72,7 +187,7 @@ diff -ruN token/ERC20/ERC20.sol token/ERC20/ERC20.sol /** 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 18:08:46.000000000 -0700 ++++ token/ERC20/extensions/ERC20FlashMint.sol 2022-04-08 17:31:22.000000000 -0700 @@ -40,9 +40,11 @@ require(token == address(this), "ERC20FlashMint: wrong token"); // silence warning about unused variable without the addition of bytecode. @@ -86,18 +201,9 @@ diff -ruN token/ERC20/extensions/ERC20FlashMint.sol token/ERC20/extensions/ERC20 /** * @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-25 13:13:49.000000000 -0700 ++++ token/ERC20/extensions/ERC20Votes.sol 2022-04-08 17:31:22.000000000 -0700 @@ -33,8 +33,8 @@ bytes32 private constant _DELEGATION_TYPEHASH = keccak256("Delegation(address delegatee,uint256 nonce,uint256 expiry)"); @@ -230,7 +336,7 @@ diff -ruN token/ERC20/extensions/ERC20Votes.sol token/ERC20/extensions/ERC20Vote } diff -ruN token/ERC20/extensions/ERC20Wrapper.sol token/ERC20/extensions/ERC20Wrapper.sol --- token/ERC20/extensions/ERC20Wrapper.sol 2022-03-02 09:14:55.000000000 -0800 -+++ token/ERC20/extensions/ERC20Wrapper.sol 2022-03-24 18:08:46.000000000 -0700 ++++ token/ERC20/extensions/ERC20Wrapper.sol 2022-04-08 17:31:22.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. @@ -240,3 +346,15 @@ diff -ruN token/ERC20/extensions/ERC20Wrapper.sol token/ERC20/extensions/ERC20Wr uint256 value = underlying.balanceOf(address(this)) - totalSupply(); _mint(account, value); return value; +diff -ruN token/ERC721/extensions/draft-ERC721Votes.sol token/ERC721/extensions/draft-ERC721Votes.sol +--- token/ERC721/extensions/draft-ERC721Votes.sol 2022-03-02 09:14:55.000000000 -0800 ++++ token/ERC721/extensions/draft-ERC721Votes.sol 2022-04-08 17:31:22.000000000 -0700 +@@ -34,7 +34,7 @@ + /** + * @dev Returns the balance of `account`. + */ +- function _getVotingUnits(address account) internal virtual override returns (uint256) { ++ function _getVotingUnits(address account) public virtual override returns (uint256) { + return balanceOf(account); + } + } diff --git a/certora/harnesses/ERC721VotesHarness.sol b/certora/harnesses/ERC721VotesHarness.sol new file mode 100644 index 000000000..9ff8911cd --- /dev/null +++ b/certora/harnesses/ERC721VotesHarness.sol @@ -0,0 +1,26 @@ +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){} + + function delegateBySig( + address delegatee, + uint256 nonce, + uint256 expiry, + uint8 v, + bytes32 r, + bytes32 s + ) public virtual override { + assert(true); + } + + function mint(address account, uint256 tokenID) public { + _mint(account, tokenID); + } + + function burn(uint256 tokenID) public { + _burn(tokenID); + } +} \ No newline at end of file diff --git a/certora/harnesses/VotesHarness.sol b/certora/harnesses/VotesHarness.sol deleted file mode 100644 index e57405d20..000000000 --- a/certora/harnesses/VotesHarness.sol +++ /dev/null @@ -1,14 +0,0 @@ -pragma solidity ^0.8.0; - -import "../munged/governance/utils/Votes.sol"; - - contract VotesHarness is Votes { - - constructor(string memory name, string memory version) EIP712(name, version) { - - } - - function _getVotingUnits(address) public override returns (uint256) { - return 0; - } -} \ No newline at end of file diff --git a/certora/munged/governance/utils/Votes.sol b/certora/munged/governance/utils/Votes.sol index 6afdc7cfe..df58c2561 100644 --- a/certora/munged/governance/utils/Votes.sol +++ b/certora/munged/governance/utils/Votes.sol @@ -35,7 +35,25 @@ abstract contract Votes is IVotes, Context, EIP712 { bytes32 private constant _DELEGATION_TYPEHASH = keccak256("Delegation(address delegatee,uint256 nonce,uint256 expiry)"); - mapping(address => address) private _delegation; + // HARNESS : Hooks cannot access any information from Checkpoints yet, so I am also updating votes and fromBlock in this struct + struct Ckpt { + uint32 fromBlock; + uint224 votes; + } + mapping(address => Ckpt) public _checkpoints; + + // HARNESSED getters + function numCheckpoints(address account) public view returns (uint32) { + return SafeCast.toUint32(_delegateCheckpoints[account]._checkpoints.length); + } + function ckptFromBlock(address account, uint32 pos) public view returns (uint32) { + return _delegateCheckpoints[account]._checkpoints[pos]._blockNumber; + } + function ckptVotes(address account, uint32 pos) public view returns (uint224) { + return _delegateCheckpoints[account]._checkpoints[pos]._value; + } + + mapping(address => address) public _delegation; mapping(address => Checkpoints.History) private _delegateCheckpoints; Checkpoints.History private _totalCheckpoints; @@ -124,7 +142,7 @@ abstract contract Votes is IVotes, Context, EIP712 { * * Emits events {DelegateChanged} and {DelegateVotesChanged}. */ - function _delegate(address account, address delegatee) internal virtual { + function _delegate(address account, address delegatee) public virtual { address oldDelegate = delegates(account); _delegation[account] = delegatee; @@ -142,10 +160,10 @@ abstract contract Votes is IVotes, Context, EIP712 { uint256 amount ) internal virtual { if (from == address(0)) { - _totalCheckpoints.push(_add, amount); + _totalCheckpoints.push(_totalCheckpoints.latest() + amount); // Harnessed to remove function pointers } if (to == address(0)) { - _totalCheckpoints.push(_subtract, amount); + _totalCheckpoints.push(_totalCheckpoints.latest() - amount); // Harnessed to remove function pointers } _moveDelegateVotes(delegates(from), delegates(to), amount); } @@ -160,11 +178,13 @@ abstract contract Votes is IVotes, Context, EIP712 { ) private { if (from != to && amount > 0) { if (from != address(0)) { - (uint256 oldValue, uint256 newValue) = _delegateCheckpoints[from].push(_subtract, amount); + (uint256 oldValue, uint256 newValue) = _delegateCheckpoints[from].push(_delegateCheckpoints[from].latest() - amount); // HARNESSED TO REMOVE FUNCTION POINTERS + _checkpoints[from] = Ckpt({fromBlock: SafeCast.toUint32(block.number), votes: SafeCast.toUint224(newValue)}); // HARNESS emit DelegateVotesChanged(from, oldValue, newValue); } if (to != address(0)) { - (uint256 oldValue, uint256 newValue) = _delegateCheckpoints[to].push(_add, amount); + (uint256 oldValue, uint256 newValue) = _delegateCheckpoints[to].push(_delegateCheckpoints[to].latest() + amount); // HARNESSED TO REMOVE FUNCTION POINTERS + _checkpoints[to] = Ckpt({fromBlock: SafeCast.toUint32(block.number), votes: SafeCast.toUint224(newValue)}); // HARNESS emit DelegateVotesChanged(to, oldValue, newValue); } } diff --git a/certora/munged/token/ERC721/extensions/draft-ERC721Votes.sol b/certora/munged/token/ERC721/extensions/draft-ERC721Votes.sol index 7d23c4921..67c584fc6 100644 --- a/certora/munged/token/ERC721/extensions/draft-ERC721Votes.sol +++ b/certora/munged/token/ERC721/extensions/draft-ERC721Votes.sol @@ -34,7 +34,7 @@ abstract contract ERC721Votes is ERC721, Votes { /** * @dev Returns the balance of `account`. */ - function _getVotingUnits(address account) internal virtual override returns (uint256) { + function _getVotingUnits(address account) public virtual override returns (uint256) { return balanceOf(account); } } diff --git a/certora/scripts/verifyERC721Votes.sh b/certora/scripts/verifyERC721Votes.sh new file mode 100644 index 000000000..cb23c2c64 --- /dev/null +++ b/certora/scripts/verifyERC721Votes.sh @@ -0,0 +1,25 @@ +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/ERC721VotesHarness.sol \ + certora/munged/utils/Checkpoints.sol \ + --verify ERC721VotesHarness:certora/specs/ERC721Votes.spec \ + --solc solc8.2 \ + --optimistic_loop \ + --loop_iter 4 \ + --staging "alex/new-dt-hashing-alpha" \ + --msg "${msg}" \ + # --rule_sanity \ No newline at end of file diff --git a/certora/specs/ERC20Votes.spec b/certora/specs/ERC20Votes.spec index 9f453d8b2..d24e400b8 100644 --- a/certora/specs/ERC20Votes.spec +++ b/certora/specs/ERC20Votes.spec @@ -1,5 +1,3 @@ -using ERC20VotesHarness as erc20votes - methods { // functions checkpoints(address, uint32) envfree @@ -164,14 +162,8 @@ rule transfer_safe() { env e; uint256 amount; address a; address b; - // require a != b; require delegates(a) != delegates(b); // confirmed if they both delegate to the same person then transfer keeps the votes the same - // requireInvariant fromBlock_constrains_numBlocks(a); - // requireInvariant fromBlock_constrains_numBlocks(b); - // requireInvariant totalVotes_gte_accounts(a, b); - // require lastIndex(delegates(a)) < 1000000; - // require lastIndex(delegates(b)) < 1000000; require numCheckpoints(delegates(a)) < 1000000; require numCheckpoints(delegates(b)) < 1000000; @@ -180,7 +172,7 @@ rule transfer_safe() { mathint totalVotes_pre = totalVotes(); - erc20votes.transferFrom(e, a, b, amount); + transferFrom(e, a, b, amount); mathint totalVotes_post = totalVotes(); uint256 votesA_post = getVotes(delegates(a)); diff --git a/certora/specs/ERC721Votes.spec b/certora/specs/ERC721Votes.spec new file mode 100644 index 000000000..e53fdb9e4 --- /dev/null +++ b/certora/specs/ERC721Votes.spec @@ -0,0 +1,351 @@ +using Checkpoints as Checkpoints + +methods { + // functions + checkpoints(address, uint32) envfree + numCheckpoints(address) returns (uint32) envfree + getVotes(address) returns (uint256) envfree + getPastVotes(address, uint256) returns (uint256) + getPastTotalSupply(uint256) returns (uint256) + delegates(address) returns (address) envfree + delegate(address) + _delegate(address, address) + delegateBySig(address, uint256, uint256, uint8, bytes32, bytes32) + nonces(address) returns (uint256) + 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(uint256) + unsafeNumCheckpoints(address) returns (uint256) envfree + + // solidity generated getters + _delegation(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 { + init_state axiom totalVotes() == 0; + axiom totalVotes() >= 0; +} + +hook Sstore _checkpoints[KEY address account].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].fromBlock uint32 newBlock (uint32 oldBlock) STORAGE { + havoc lastFromBlock assuming + lastFromBlock@new(account) == newBlock; + + havoc doubleFromBlock assuming + doubleFromBlock@new(account) == (newBlock == lastFromBlock(account)); +} + +rule sanity(method f) { + env e; + calldataarg arg; + f(e, arg); + assert false; +} + +// something stupid just to see +invariant sanity_invariant() + totalSupply() >= 0 + +// sum of user balances is >= total amount of delegated votes +// blocked by tool error +invariant votes_solvency() + to_mathint(totalSupply()) >= totalVotes() +{ preserved with(env e) { + require forall address account. numCheckpoints(account) < 1000000; + requireInvariant totalVotes_sums_accounts(); +} } + +invariant totalVotes_sums_accounts() + forall address a. forall address b. (a != b && a != 0x0 && b != 0x0) => totalVotes() >= getVotes(delegates(a)) + getVotes(delegates(b)) + + +// 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); + } +} + +// TODO add a note about this in the report +// // numCheckpoints are less than maxInt +// // passes because numCheckpoints does a safeCast +// invariant maxInt_constrains_numBlocks(address account) +// numCheckpoints(account) < 4294967295 // 2^32 + +// // fails because there are no checks to stop it +// invariant maxInt_constrains_ckptsLength(address account) +// unsafeNumCheckpoints(account) < 4294967295 // 2^32 + +// can't have more checkpoints for a given account than the last from block +// passes +invariant fromBlock_constrains_numBlocks(address account) + numCheckpoints(account) <= ckptFromBlock(account, numCheckpoints(account) - 1) +{ preserved with(env e) { + require e.block.number >= ckptFromBlock(account, numCheckpoints(account) - 1); // this should be true from the invariant above!! +}} + +// for any given checkpoint, the fromBlock must be greater than the checkpoint +// this proves the above invariant in combination with the below invariant +// if checkpoint has a greater fromBlock than the last, and the FromBlock is always greater than the pos. +// Then the number of positions must be less than the currentFromBlock +// ^note that the tool is assuming it's possible for the starting fromBlock to be 0 or anything, and does not know the current starting block +// passes + rule sanity +invariant fromBlock_greaterThanEq_pos(address account, uint32 pos) + ckptFromBlock(account, pos) >= pos + +// a larger index must have a larger fromBlock +// passes + rule sanity +invariant fromBlock_increasing(address account, uint32 pos, uint32 pos2) + pos > pos2 => ckptFromBlock(account, pos) > ckptFromBlock(account, pos2) + + +// converted from an invariant to a rule to slightly change the logic +// if the fromBlock is the same as before, then the number of checkpoints stays the same +// however if the fromBlock is new than the number of checkpoints increases +// passes, fails rule sanity because tautology check seems to be bugged +rule unique_checkpoints_rule(method f) { + env e; calldataarg args; + address account; + uint32 num_ckpts_ = numCheckpoints(account); + uint32 fromBlock_ = num_ckpts_ == 0 ? 0 : ckptFromBlock(account, num_ckpts_ - 1); + + f(e, args); + + uint32 _num_ckpts = numCheckpoints(account); + uint32 _fromBlock = _num_ckpts == 0 ? 0 : ckptFromBlock(account, _num_ckpts - 1); + + + assert fromBlock_ == _fromBlock => num_ckpts_ == _num_ckpts || _num_ckpts == 1, "same fromBlock, new checkpoint"; + // this assert fails consistently + // assert !doubleFromBlock(account) => ckpts_ != _ckpts, "new fromBlock but total checkpoints not being increased"; +} + +// assumes neither account has delegated +// currently fails due to this scenario. A has maxint number of checkpoints +// an additional checkpoint is added which overflows and sets A's votes to 0 +// passes + rule sanity (- a bad tautology check) +rule transfer_safe() { + env e; + uint256 ID; + address a; address b; + + require delegates(a) != delegates(b); // confirmed if they both delegate to the same person then transfer keeps the votes the same + require numCheckpoints(delegates(a)) < 1000000; + require numCheckpoints(delegates(b)) < 1000000; + + uint256 votesA_pre = getVotes(delegates(a)); + uint256 votesB_pre = getVotes(delegates(b)); + + mathint totalVotes_pre = totalVotes(); + + transferFrom(e, a, b, ID); + + mathint totalVotes_post = totalVotes(); + uint256 votesA_post = getVotes(delegates(a)); + uint256 votesB_post = getVotes(delegates(b)); + + // if an account that has not delegated transfers balance to an account that has, it will increase the total supply of votes + assert totalVotes_pre == totalVotes_post, "transfer changed total supply"; + assert delegates(a) != 0 => votesA_pre - 1 == votesA_post, "A lost the wrong amount of votes"; + assert delegates(b) != 0 => votesB_pre + 1 == votesB_post, "B gained the wrong amount of votes"; +} + +// for any given function f, if the delegate is changed the function must be delegate or delegateBySig +// passes +rule delegates_safe(method f) filtered {f -> (f.selector != delegate(address).selector && + f.selector != _delegate(address, address).selector && + f.selector != delegateBySig(address, uint256, uint256, uint8, bytes32, bytes32).selector) } +{ + env e; calldataarg args; + address account; + address pre = delegates(account); + + f(e, args); + + address post = delegates(account); + + assert pre == post, "invalid delegate change"; +} + +// delegates increases the delegatee's votes by the proper amount +// passes + rule sanity +rule delegatee_receives_votes() { + env e; + address delegator; address delegatee; + + require numCheckpoints(delegatee) < 1000000; + require delegates(delegator) != delegatee; + require delegatee != 0x0; + + + 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"; +} + +// passes + rule sanity +rule previous_delegatee_votes_removed() { + env e; + address delegator; address delegatee; address third; + + require third != delegatee; + require delegates(delegator) == third; + require numCheckpoints(third) < 1000000; + + uint256 delegator_bal = balanceOf(e, delegator); + uint256 votes_ = getVotes(third); + + _delegate(e, delegator, delegatee); + + uint256 _votes = getVotes(third); + + assert third != 0x0 => _votes == votes_ - delegator_bal, "votes not removed from the previous delegatee"; +} + +// passes with rule sanity +rule delegate_contained() { + env e; + address delegator; address delegatee; address other; + + 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"; +} + +rule delegate_no_frontrunning(method f) { + env e; calldataarg args; + address delegator; address delegatee; address third; address other; + + + + require numCheckpoints(delegatee) < 1000000; + require numCheckpoints(third) < 1000000; + + + f(e, args); + + uint256 delegator_bal = balanceOf(e, delegator); + uint256 delegatee_votes_ = getVotes(delegatee); + uint256 third_votes_ = getVotes(third); + uint256 other_votes_ = getVotes(other); + require delegates(delegator) == third; + require third != delegatee; + require other != third; + require other != delegatee; + require delegatee != 0x0; + + _delegate(e, delegator, delegatee); + + uint256 _delegatee_votes = getVotes(delegatee); + uint256 _third_votes = getVotes(third); + uint256 _other_votes = getVotes(other); + + + // previous delegatee loses all of their votes + // delegatee gains that many votes + // third loses any votes delegated to them + assert _delegatee_votes == delegatee_votes_ + delegator_bal, "delegatee did not receive votes"; + assert third != 0 => _third_votes == third_votes_ - delegator_bal, "votes not removed from third"; + assert other_votes_ == _other_votes, "delegate not contained"; +} + + +// mint and burn need to be handled differently for ERC721 + +// 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"; +// } + +// rule burn_decreases_totalSupply() { +// env e; +// uint256 amount; address account; + +// uint256 fromBlock = e.block.number; +// uint256 totalSupply_ = totalSupply(); + +// burn(e, account, amount); + +// uint256 _totalSupply = totalSupply(); + +// assert _totalSupply == totalSupply_ - amount, "totalSupply not decreased properly"; +// assert getPastTotalSupply(e, fromBlock) == totalSupply_ , "previous total supply not saved properly"; +// } + + +// rule mint_doesnt_increase_totalVotes() { +// env e; +// uint256 amount; address account; + +// mathint totalVotes_ = totalVotes(); + +// mint(e, account, amount); + +// assert totalVotes() == totalVotes_, "totalVotes increased"; +// } + +// rule burn_doesnt_decrease_totalVotes() { +// env e; +// uint256 amount; address account; + +// mathint totalVotes_ = totalVotes(); + +// burn(e, account, amount); + +// assert totalVotes() == totalVotes_, "totalVotes decreased"; +// }