NoBey/openzeppelin-contracts
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Merge branch 'certora/erc20' of github.com:Certora/openzeppelin-contracts into certora/erc20

Browse Source
This commit is contained in:
Aleksander Kryukov
2022-03-27 16:06:49 +01:00
parent a35ad6dfc3 140f019155
commit 4b9500cf25
6 changed files with 611 additions and 106 deletions
Download Patch File Download Diff File Expand all files Collapse all files

337
certora/applyHarness.patch
View File

@ -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;

17
certora/harnesses/ERC20VotesHarness.sol
View File

@ -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);
}
}

11
certora/munged/token/ERC20/extensions/ERC20Votes.sol
View File

@ -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;

23
certora/scripts/ERC20VotesRule.sh Normal file
View File

@ -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 \

19
certora/scripts/verifyERC20Votes.sh
View File

@ -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}"

310
certora/specs/ERC20Votes.spec
View File

@ -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;
}
}
// 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";
// }