From 8f6a03204e9efb4e7c32a6d85ad1a08d464d10e5 Mon Sep 17 00:00:00 2001 From: Hadrien Croubois Date: Mon, 26 Sep 2022 19:09:34 +0200 Subject: [PATCH] Start working on ERC20 specs --- certora/applyHarness.patch | 12 -- certora/harnesses/ERC20PermitHarness.sol | 13 +- certora/harnesses/ERC20VotesHarness.sol | 18 +- certora/harnesses/ERC20WrapperHarness.sol | 4 +- certora/scripts/Round2/verifyAccessControl.sh | 3 +- certora/scripts/Round2/verifyERC1155.sh | 3 +- .../scripts/Round2/verifyERC20FlashMint.sh | 3 +- certora/scripts/Round2/verifyERC20Votes.sh | 3 +- certora/scripts/Round2/verifyERC20Wrapper.sh | 3 +- certora/scripts/Round2/verifyERC721Votes.sh | 3 +- certora/scripts/Round2/verifyTimelock.sh | 3 +- certora/scripts/verifyERC20.sh | 10 + .../verifyGovernorPreventLateQuorum.sh | 5 +- certora/specs/ERC20.spec | 157 +++++++++++++++ certora/specs/ERC20FlashMint.spec | 12 +- certora/specs/ERC20Votes.spec | 188 +++++++++--------- certora/specs/ERC20Wrapper.spec | 128 ++++++------ certora/specs/erc20.spec | 18 +- 18 files changed, 390 insertions(+), 196 deletions(-) create mode 100644 certora/scripts/verifyERC20.sh create mode 100644 certora/specs/ERC20.spec diff --git a/certora/applyHarness.patch b/certora/applyHarness.patch index c69692496..83802405a 100644 --- a/certora/applyHarness.patch +++ b/certora/applyHarness.patch @@ -278,18 +278,6 @@ diff -ruN token/ERC1155/ERC1155.sol token/ERC1155/ERC1155.sol 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-09-20 13:34:47.024598756 +0200 -+++ token/ERC20/ERC20.sol 2022-09-20 14:34:24.809915708 +0200 -@@ -282,7 +282,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 { // HARNESS: internal -> public - require(account != address(0), "ERC20: burn from the zero address"); - - _beforeTokenTransfer(account, address(0), amount); diff -ruN token/ERC20/extensions/ERC20FlashMint.sol token/ERC20/extensions/ERC20FlashMint.sol --- token/ERC20/extensions/ERC20FlashMint.sol 2022-09-20 11:01:10.432848512 +0200 +++ token/ERC20/extensions/ERC20FlashMint.sol 2022-09-20 14:34:24.809915708 +0200 diff --git a/certora/harnesses/ERC20PermitHarness.sol b/certora/harnesses/ERC20PermitHarness.sol index 67fa937df..9e56d2fe2 100644 --- a/certora/harnesses/ERC20PermitHarness.sol +++ b/certora/harnesses/ERC20PermitHarness.sol @@ -1,5 +1,14 @@ +import "../munged/token/ERC20/ERC20.sol"; import "../munged/token/ERC20/extensions/draft-ERC20Permit.sol"; -contract ERC20PermitHarness is ERC20Permit { - constructor(string memory _name, string memory _symbol) ERC20(_name, _symbol) ERC20Permit(_name) {} +contract ERC20Harness is ERC20, ERC20Permit { + constructor(string memory name, string memory symbol) ERC20(name, symbol) ERC20Permit(name) {} + + function mint(address account, uint256 amount) public { + _mint(account, amount); + } + + function burn(address account, uint256 amount) public { + _burn(account, amount); + } } diff --git a/certora/harnesses/ERC20VotesHarness.sol b/certora/harnesses/ERC20VotesHarness.sol index 5f1ad6e19..d4912e780 100644 --- a/certora/harnesses/ERC20VotesHarness.sol +++ b/certora/harnesses/ERC20VotesHarness.sol @@ -1,15 +1,7 @@ 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; - } + constructor(string memory name, string memory symbol) ERC20(name, symbol) ERC20Permit(name) {} function mint(address account, uint256 amount) public { _mint(account, amount); @@ -19,6 +11,14 @@ contract ERC20VotesHarness is ERC20Votes { _burn(account, amount); } + 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 unsafeNumCheckpoints(address account) public view returns (uint256) { return _checkpoints[account].length; } diff --git a/certora/harnesses/ERC20WrapperHarness.sol b/certora/harnesses/ERC20WrapperHarness.sol index edd3bf7d4..8a0149128 100644 --- a/certora/harnesses/ERC20WrapperHarness.sol +++ b/certora/harnesses/ERC20WrapperHarness.sol @@ -2,10 +2,10 @@ import "../munged/token/ERC20/extensions/ERC20Wrapper.sol"; contract ERC20WrapperHarness is ERC20Wrapper { constructor( - IERC20 underlyingToken, + IERC20 _underlying, string memory _name, string memory _symbol - ) ERC20Wrapper(underlyingToken) ERC20(_name, _symbol) {} + ) ERC20(_name, _symbol) ERC20Wrapper(_underlying) {} function underlyingTotalSupply() public view returns (uint256) { return underlying.totalSupply(); diff --git a/certora/scripts/Round2/verifyAccessControl.sh b/certora/scripts/Round2/verifyAccessControl.sh index 83ab08018..312a4c22a 100644 --- a/certora/scripts/Round2/verifyAccessControl.sh +++ b/certora/scripts/Round2/verifyAccessControl.sh @@ -7,4 +7,5 @@ certoraRun \ --verify AccessControlHarness:certora/specs/AccessControl.spec \ --solc solc \ --optimistic_loop \ - --msg "AccessControl verification" + --msg "AccessControl verification" \ + $@ diff --git a/certora/scripts/Round2/verifyERC1155.sh b/certora/scripts/Round2/verifyERC1155.sh index 3bccdc0f6..3d336d3aa 100644 --- a/certora/scripts/Round2/verifyERC1155.sh +++ b/certora/scripts/Round2/verifyERC1155.sh @@ -8,4 +8,5 @@ certoraRun \ --solc solc \ --optimistic_loop \ --loop_iter 3 \ - --msg "ERC1155" + --msg "ERC1155" \ + $@ diff --git a/certora/scripts/Round2/verifyERC20FlashMint.sh b/certora/scripts/Round2/verifyERC20FlashMint.sh index 7370d4bec..c0a0f2d40 100644 --- a/certora/scripts/Round2/verifyERC20FlashMint.sh +++ b/certora/scripts/Round2/verifyERC20FlashMint.sh @@ -10,4 +10,5 @@ certoraRun \ --verify ERC20FlashMintHarness:certora/specs/ERC20FlashMint.spec \ --solc solc \ --optimistic_loop \ - --msg "ERC20FlashMint verification" + --msg "ERC20FlashMint verification" \ + $@ diff --git a/certora/scripts/Round2/verifyERC20Votes.sh b/certora/scripts/Round2/verifyERC20Votes.sh index 79530d58d..797f38ddb 100644 --- a/certora/scripts/Round2/verifyERC20Votes.sh +++ b/certora/scripts/Round2/verifyERC20Votes.sh @@ -8,4 +8,5 @@ certoraRun \ --solc solc \ --optimistic_loop \ --settings -copyLoopUnroll=4 \ - --msg "ERC20Votes" \ No newline at end of file + --msg "ERC20Votes" \ + $@ \ No newline at end of file diff --git a/certora/scripts/Round2/verifyERC20Wrapper.sh b/certora/scripts/Round2/verifyERC20Wrapper.sh index 71d49cf0f..de119e579 100644 --- a/certora/scripts/Round2/verifyERC20Wrapper.sh +++ b/certora/scripts/Round2/verifyERC20Wrapper.sh @@ -7,4 +7,5 @@ certoraRun \ --verify ERC20WrapperHarness:certora/specs/ERC20Wrapper.spec \ --solc solc \ --optimistic_loop \ - --msg "ERC20Wrapper verification" + --msg "ERC20Wrapper verification" \ + $@ diff --git a/certora/scripts/Round2/verifyERC721Votes.sh b/certora/scripts/Round2/verifyERC721Votes.sh index b9e7a8340..42724444e 100644 --- a/certora/scripts/Round2/verifyERC721Votes.sh +++ b/certora/scripts/Round2/verifyERC721Votes.sh @@ -9,4 +9,5 @@ certoraRun \ --optimistic_loop \ --disableLocalTypeChecking \ --settings -copyLoopUnroll=4 \ - --msg "ERC721Votes" + --msg "ERC721Votes" \ + $@ diff --git a/certora/scripts/Round2/verifyTimelock.sh b/certora/scripts/Round2/verifyTimelock.sh index 2de5d4388..14599a6a4 100644 --- a/certora/scripts/Round2/verifyTimelock.sh +++ b/certora/scripts/Round2/verifyTimelock.sh @@ -9,4 +9,5 @@ certoraRun \ --optimistic_loop \ --loop_iter 3 \ --settings -byteMapHashingPrecision=32 \ - --msg "TimelockController verification" + --msg "TimelockController verification" \ + $@ diff --git a/certora/scripts/verifyERC20.sh b/certora/scripts/verifyERC20.sh new file mode 100644 index 000000000..aaffd5629 --- /dev/null +++ b/certora/scripts/verifyERC20.sh @@ -0,0 +1,10 @@ +#!/usr/bin/env bash + +set -euxo pipefail + +certoraRun \ + certora/harnesses/ERC20Harness.sol \ + --verify ERC20Harness:certora/specs/ERC20.spec \ + --solc solc \ + --optimistic_loop \ + $@ \ No newline at end of file diff --git a/certora/scripts/verifyGovernorPreventLateQuorum.sh b/certora/scripts/verifyGovernorPreventLateQuorum.sh index 53e24a999..720caf0aa 100644 --- a/certora/scripts/verifyGovernorPreventLateQuorum.sh +++ b/certora/scripts/verifyGovernorPreventLateQuorum.sh @@ -3,7 +3,10 @@ set -euxo pipefail certoraRun \ - certora/harnesses/ERC721VotesHarness.sol certora/munged/governance/TimelockController.sol certora/harnesses/GovernorPreventLateQuorumHarness.sol \ + certora/harnesses/ERC20VotesHarness.sol \ + certora/harnesses/ERC721VotesHarness.sol \ + certora/munged/governance/TimelockController.sol \ + certora/harnesses/GovernorPreventLateQuorumHarness.sol \ --verify GovernorPreventLateQuorumHarness:certora/specs/GovernorPreventLateQuorum.spec \ --solc solc \ --optimistic_loop \ diff --git a/certora/specs/ERC20.spec b/certora/specs/ERC20.spec new file mode 100644 index 000000000..629ed89b8 --- /dev/null +++ b/certora/specs/ERC20.spec @@ -0,0 +1,157 @@ +import "erc20.spec" + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Ghost & hooks: sum of all balances │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +ghost sumOfBalances() returns uint256 { + init_state axiom sumOfBalances() == 0; +} + +hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) STORAGE { + havoc sumOfBalances assuming sumOfBalances@new() == sumOfBalances@old() + newValue - oldValue; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Invariant: totalSupply is the sum of all balances │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +invariant totalSupplyIsSumOfBalances() + totalSupply() == sumOfBalances() + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Invariant: balance of address(0) is 0 │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +invariant zeroAddressNoBalance() + balanceOf(0) == 0 + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rules: totalSupply only changes through mint or burn │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule noChangeTotalSupply() { + requireInvariant totalSupplyIsSumOfBalances(); + + env e; + method f; + calldataarg args; + + uint256 totalSupplyBefore = totalSupply(); + f(e, args); + uint256 totalSupplyAfter = totalSupply(); + + assert (totalSupplyAfter > totalSupplyBefore) => (f.selector == mint(address,uint256).selector); + assert (totalSupplyAfter < totalSupplyBefore) => (f.selector == burn(address,uint256).selector); +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rules: totalSupply change matches minted or burned amount │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule mintIncreasesTotalSupply() { + requireInvariant totalSupplyIsSumOfBalances(); + + env e; + address to; + uint256 amount; + + uint256 totalSupplyBefore = totalSupply(); + mint(e, to, amount); + uint256 totalSupplyAfter = totalSupply(); + + assert totalSupplyAfter == totalSupplyBefore + amount; +} + +rule burnDecreasesTotalSupply() { + requireInvariant totalSupplyIsSumOfBalances(); + + env e; + address from; + uint256 amount; + + uint256 totalSupplyBefore = totalSupply(); + burn(e, from, amount); + uint256 totalSupplyAfter = totalSupply(); + + assert totalSupplyAfter == totalSupplyBefore - amount; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rules: Balance of an account can only decrease if the tx was sent by owner or by approved │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule onlyAuthorizedCanTransfer() { + requireInvariant totalSupplyIsSumOfBalances(); + + env e; + method f; + calldataarg args; + address account; + + uint256 allowanceBefore = allowance(account, e.msg.sender); + uint256 balanceBefore = balanceOf(account); + f(e, args); + uint256 balanceAfter = balanceOf(account); + + assert ( + balanceAfter < balanceBefore + ) => ( + f.selector == burn(address,uint256).selector || + e.msg.sender == account || + balanceBefore - balanceAfter <= allowanceBefore + ); +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: transfer moves correct amount from sender to receiver │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule transferAmount() { + requireInvariant totalSupplyIsSumOfBalances(); + + env e; + address holder = e.msg.sender; + address recipient; + uint256 amount; + + uint256 holderBalanceBefore = balanceOf(holder); + uint256 recipientBalanceBefore = balanceOf(recipient); + + transfer(e, recipient, amount); + + assert balanceOf(holder) == holderBalanceBefore - (holder == recipient ? 0 : amount); + assert balanceOf(recipient) == recipientBalanceBefore + (holder == recipient ? 0 : amount); +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: transferFrom moves correct amount from holder to receiver, and updates allowance │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule transferFomAmountAndApproval() { + requireInvariant totalSupplyIsSumOfBalances(); + + env e; + address holder; + address recipient; + uint256 amount; + + uint256 allowanceBefore = allowance(holder, e.msg.sender); + uint256 holderBalanceBefore = balanceOf(holder); + uint256 recipientBalanceBefore = balanceOf(recipient); + + transferFrom(e, holder, recipient, amount); + + assert allowanceBefore >= amount; + assert allowance(holder, e.msg.sender) == (allowanceBefore == max_uint256 ? to_uint256(max_uint256) : allowanceBefore - amount); + assert balanceOf(holder) == holderBalanceBefore - (holder == recipient ? 0 : amount); + assert balanceOf(recipient) == recipientBalanceBefore + (holder == recipient ? 0 : amount); +} diff --git a/certora/specs/ERC20FlashMint.spec b/certora/specs/ERC20FlashMint.spec index 3142f508f..e014147f8 100644 --- a/certora/specs/ERC20FlashMint.spec +++ b/certora/specs/ERC20FlashMint.spec @@ -7,16 +7,18 @@ methods { ghost mapping(address => uint256) trackedBurnAmount; -function specBurn(address account, uint256 amount) returns bool { // retuns needed to overcome current CVL limitations: "could not type expression "specBurn(account,amount)", message: A summary must return a simple type, but specBurn(account,amount) returns 'void'" +// retuns needed to overcome current CVL limitations: "could not type expression "specBurn(account,amount)", message: A summary must return a simple type, but specBurn(account,amount) returns 'void'" +function specBurn(address account, uint256 amount) returns bool { trackedBurnAmount[account] = amount; return true; } - -// STATUS - verified // Check that if flashLoan() call is successful, then proper amount of tokens was burnt(fee + flashLoan amount) -rule letsWatchItBurns(env e){ - address receiver; address token; uint256 amount; bytes data; +rule letsWatchItBurns(env e) { + address receiver; + address token; + uint256 amount; + bytes data; uint256 feeBefore = flashFee(e, token, amount); diff --git a/certora/specs/ERC20Votes.spec b/certora/specs/ERC20Votes.spec index f0b9cde0d..3b133c2f2 100644 --- a/certora/specs/ERC20Votes.spec +++ b/certora/specs/ERC20Votes.spec @@ -1,28 +1,46 @@ +import "erc20.spec" + methods { - // functions + // IVotes + getVotes(address) returns (uint256) envfree + getPastVotes(address, uint256) returns (uint256) // not envfree (reads block.number) + getPastTotalSupply(uint256) returns (uint256) // not envfree (reads block.number) + delegates(address) returns (address) envfree + delegate(address) // not envfree (reads msg.sender) + // delegateBySig(address, uint256, uint256, uint8, bytes32, bytes32) + + // ERC20Votes 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 + _delegate(address, address) // not envfree (reads block.number when creating checkpoint) // harnesss functions ckptFromBlock(address, uint32) returns (uint32) envfree ckptVotes(address, uint32) returns (uint224) envfree - mint(address, uint256) - burn(address, uint256) unsafeNumCheckpoints(address) returns (uint256) envfree + mint(address, uint256) // not envfree (reads block.number when creating checkpoint) + burn(address, uint256) // not envfree (reads block.number when creating checkpoint) + // solidity generated getters _delegates(address) returns (address) envfree - - // external functions } + + + + + + + + + + + + + + + + // gets the most recent votes for a user ghost userVotes(address) returns uint224 { init_state axiom forall address a. userVotes(a) == 0; @@ -32,10 +50,11 @@ ghost userVotes(address) returns uint224 { ghost totalVotes() returns uint224 { init_state axiom totalVotes() == 0; } -ghost lastIndex(address) returns uint32; -// helper -hook Sstore _checkpoints[KEY address account][INDEX uint32 index].votes uint224 newVotes (uint224 oldVotes) STORAGE { +ghost lastIndex(address) returns uint32; + +// helper +hook Sstore _checkpoints[KEY address account][INDEX uint32 index].votes uint224 newVotes (uint224 oldVotes) STORAGE { havoc userVotes assuming userVotes@new(account) == newVotes; @@ -46,38 +65,39 @@ hook Sstore _checkpoints[KEY address account][INDEX uint32 index].votes uint224 lastIndex@new(account) == index; } - 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 + + havoc doubleFromBlock assuming doubleFromBlock@new(account) == (newBlock == lastFromBlock(account)); } +/////////////////////////////////////////////////////////////////////////////////////////////////////////////////////// +// Invariants // +/////////////////////////////////////////////////////////////////////////////////////////////////////////////////////// + // sum of user balances is >= total amount of delegated votes // fails on burn. This is because burn does not remove votes from the users invariant votes_solvency() totalSupply() >= to_uint256(totalVotes()) -filtered { f -> f.selector != _burn(address, uint256).selector} -{ preserved with(env e) { - require forall address account. numCheckpoints(account) < 1000000; -} preserved burn(address a, uint256 amount) with(env e){ - require _delegates(0) == 0; - require forall address a2. (_delegates(a) != _delegates(a2)) && (balanceOf(e, _delegates(a)) + balanceOf(e, _delegates(a2)) <= totalVotes()); - require balanceOf(e, _delegates(a)) < totalVotes(); - require amount < 100000; -}} - + filtered { f -> f.selector != _burn(address, uint256).selector } +{ + preserved with(env e) { + require forall address account. numCheckpoints(account) < 1000000; + } preserved burn(address a, uint256 amount) with(env e) { + require _delegates(0) == 0; + require forall address a2. (_delegates(a) != _delegates(a2)) && (balanceOf(e, _delegates(a)) + balanceOf(e, _delegates(a2)) <= totalVotes()); + require balanceOf(e, _delegates(a)) < totalVotes(); + require amount < 100000; + } +} // for some checkpoint, the fromBlock is less than the current block number invariant blockNum_constrains_fromBlock(address account, uint32 index, env e) @@ -88,23 +108,24 @@ invariant blockNum_constrains_fromBlock(address account, uint32 index, env e) require index < numCheckpoints(account); } } + // numCheckpoints are less than maxInt -// passes because numCheckpoints does a safeCast -// invariant maxInt_constrains_numBlocks(address account) -// numCheckpoints(account) < 4294967295 // 2^32 +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 -// passes invariant fromBlock_constrains_numBlocks(address account) numCheckpoints(account) <= ckptFromBlock(account, numCheckpoints(account) - 1) filtered { f -> !f.isView } -{ preserved with(env e) { - require e.block.number >= ckptFromBlock(account, numCheckpoints(account) - 1); // this should be true from the invariant above!! -}} +{ + 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. +// 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 @@ -118,6 +139,9 @@ invariant fromBlock_increasing(address account, uint32 pos, uint32 pos2) pos > pos2 => ckptFromBlock(account, pos) > ckptFromBlock(account, pos2) filtered { f -> !f.isView } +/////////////////////////////////////////////////////////////////////////////////////////////////////////////////////// +// Rules // +/////////////////////////////////////////////////////////////////////////////////////////////////////////////////////// // 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 @@ -126,14 +150,13 @@ invariant fromBlock_increasing(address account, uint32 pos, uint32 pos2) rule unique_checkpoints_rule(method f) { env e; calldataarg args; address account; - uint32 num_ckpts_ = numCheckpoints(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"; } @@ -153,7 +176,7 @@ rule transfer_safe() { uint256 votesB_pre = getVotes(delegates(b)); uint224 totalVotes_pre = totalVotes(); transferFrom(e, a, b, amount); - + uint224 totalVotes_post = totalVotes(); uint256 votesA_post = getVotes(delegates(a)); uint256 votesB_post = getVotes(delegates(b)); @@ -164,9 +187,12 @@ rule transfer_safe() { } // 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) } +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; @@ -175,16 +201,16 @@ rule delegates_safe(method f) filtered {f -> (f.selector != delegate(address).se 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; + env e; address delegator; address delegatee; require delegates(delegator) != delegatee; require delegatee != 0x0; - uint256 delegator_bal = balanceOf(e, delegator); uint256 votes_= getVotes(delegatee); @@ -222,7 +248,7 @@ rule delegate_contained() { address delegator; address delegatee; address other; require other != delegatee; - require other != delegates(delegator); + require other != delegates(delegator); uint256 votes_ = getVotes(other); @@ -237,12 +263,9 @@ 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); @@ -270,63 +293,42 @@ rule delegate_no_frontrunning(method f) { assert other_votes_ == _other_votes, "delegate not contained"; } - - // passes -rule mint_increases_totalSupply() { - +rule onMint() { env e; - uint256 amount; address account; + uint256 amount; + address account; uint256 fromBlock = e.block.number; - uint256 totalSupply_ = totalSupply(); + uint224 totalVotesBefore = totalVotes(); + uint256 totalSupplyBefore = totalSupply(); mint(e, account, amount); - uint256 _totalSupply = totalSupply(); - require _totalSupply < _maxSupply(); + uint224 totalVotesAfter = totalVotes(); + uint256 totalSupplyAfter = totalSupply(); - assert _totalSupply == totalSupply_ + amount, "totalSupply not increased properly"; - assert getPastTotalSupply(e, fromBlock) == totalSupply_ , "previous total supply not saved properly"; + assert totalVotes() == totalVotesBefore, "totalVotes decreased"; + assert totalSupplyAfter == totalSupplyBefore + amount, "totalSupply not increased properly"; + assert getPastTotalSupply(e, fromBlock) == totalSupplyBefore , "previous total supply not saved properly"; } // passes -rule burn_decreases_totalSupply() { +rule onBurn() { env e; - uint256 amount; address account; + uint256 amount; + address account; uint256 fromBlock = e.block.number; - uint256 totalSupply_ = totalSupply(); + uint224 totalVotesBefore = totalVotes(); + uint256 totalSupplyBefore = totalSupply(); burn(e, account, amount); - uint256 _totalSupply = totalSupply(); + uint224 totalVotesAfter = totalVotes(); + uint256 totalSupplyAfter = totalSupply(); - assert _totalSupply == totalSupply_ - amount, "totalSupply not decreased properly"; - assert getPastTotalSupply(e, fromBlock) == totalSupply_ , "previous total supply not saved properly"; + assert totalVotes() == totalVotesBefore, "totalVotes decreased"; + assert totalSupplyAfter == totalSupplyBefore - amount, "totalSupply not decreased properly"; + assert getPastTotalSupply(e, fromBlock) == totalSupplyBefore , "previous total supply not saved properly"; } - - - -// passes -rule mint_doesnt_increase_totalVotes() { - env e; - uint256 amount; address account; - - uint224 totalVotes_ = totalVotes(); - - mint(e, account, amount); - - assert totalVotes() == totalVotes_, "totalVotes increased"; -} -// passes -rule burn_doesnt_decrease_totalVotes() { - env e; - uint256 amount; address account; - - uint224 totalVotes_ = totalVotes(); - - burn(e, account, amount); - - assert totalVotes() == totalVotes_, "totalVotes decreased"; -} \ No newline at end of file diff --git a/certora/specs/ERC20Wrapper.spec b/certora/specs/ERC20Wrapper.spec index 1ab9012c2..0e44026cc 100644 --- a/certora/specs/ERC20Wrapper.spec +++ b/certora/specs/ERC20Wrapper.spec @@ -10,12 +10,14 @@ methods { _recover(address) returns(uint256) } +/////////////////////////////////////////////////////////////////////////////////////////////////////////////////////// +// Invariants // +/////////////////////////////////////////////////////////////////////////////////////////////////////////////////////// -// STATUS - verified // totalsupply of wrapped should be less than or equal to underlying (assuming no external transfer) - solvency invariant whatAboutTotal(env e) totalSupply(e) <= underlyingTotalSupply() - filtered { f -> f.selector != certorafallback_0().selector && !f.isView} + filtered { f -> f.selector != certorafallback_0().selector && !f.isView } { preserved { require underlyingBalanceOf(currentContract) <= underlyingTotalSupply(); @@ -25,8 +27,6 @@ invariant whatAboutTotal(env e) } } - -// STATUS - verified // totalsupply of wrapped should be less than or equal to the underlying balanceOf contract (assuming no external transfer) - solvency invariant underTotalAndContractBalanceOfCorrelation(env e) totalSupply(e) <= underlyingBalanceOf(currentContract) @@ -38,11 +38,14 @@ invariant underTotalAndContractBalanceOfCorrelation(env e) } } +/////////////////////////////////////////////////////////////////////////////////////////////////////////////////////// +// Rules // +/////////////////////////////////////////////////////////////////////////////////////////////////////////////////////// -// STATUS - verified // Check that values are updated correctly by `depositFor()` -rule depositForSpecBasic(env e){ - address account; uint256 amount; +rule depositForSpecBasic(env e) { + address account; + uint256 amount; require e.msg.sender != currentContract; require underlying() != currentContract; @@ -62,11 +65,10 @@ rule depositForSpecBasic(env e){ assert underlyingThisBalanceBefore == underlyingThisBalanceAfter - amount, "underlying this balance wrong update"; } - -// STATUS - verified // Check that values are updated correctly by `depositFor()` -rule depositForSpecWrapper(env e){ - address account; uint256 amount; +rule depositForSpecWrapper(env e) { + address account; + uint256 amount; require underlying() != currentContract; @@ -78,18 +80,20 @@ rule depositForSpecWrapper(env e){ uint256 wrapperUserBalanceAfter = balanceOf(e, account); uint256 wrapperSenderBalanceAfter = balanceOf(e, e.msg.sender); - assert account == e.msg.sender => wrapperUserBalanceBefore == wrapperSenderBalanceBefore - && wrapperUserBalanceAfter == wrapperSenderBalanceAfter - && wrapperUserBalanceBefore == wrapperUserBalanceAfter - amount, "wrapper balances wrong update"; + assert account == e.msg.sender => wrapperUserBalanceBefore == wrapperSenderBalanceBefore + && wrapperUserBalanceAfter == wrapperSenderBalanceAfter + && wrapperUserBalanceBefore == wrapperUserBalanceAfter - amount + , "wrapper balances wrong update"; + assert account != e.msg.sender => wrapperUserBalanceBefore == wrapperUserBalanceAfter - amount - && wrapperSenderBalanceBefore == wrapperSenderBalanceAfter, "wrapper balances wrong update"; + && wrapperSenderBalanceBefore == wrapperSenderBalanceAfter + , "wrapper balances wrong update"; } - -// STATUS - verified // Check that values are updated correctly by `depositFor()` -rule depositForSpecUnderlying(env e){ - address account; uint256 amount; +rule depositForSpecUnderlying(env e) { + address account; + uint256 amount; require e.msg.sender != currentContract; require underlying() != currentContract; @@ -103,21 +107,25 @@ rule depositForSpecUnderlying(env e){ uint256 underlyingUserBalanceAfter = underlyingBalanceOf(account); assert account == e.msg.sender => underlyingSenderBalanceBefore == underlyingUserBalanceBefore - && underlyingSenderBalanceAfter == underlyingUserBalanceAfter - && underlyingSenderBalanceBefore == underlyingSenderBalanceAfter + amount, "underlying balances wrong update"; - - assert account != e.msg.sender && account == currentContract => underlyingSenderBalanceBefore == underlyingSenderBalanceAfter + amount - && underlyingUserBalanceBefore == underlyingUserBalanceAfter - amount, "underlying balances wrong update"; - - assert account != e.msg.sender && account != currentContract => underlyingSenderBalanceBefore == underlyingSenderBalanceAfter + amount - && underlyingUserBalanceBefore == underlyingUserBalanceAfter, "underlying balances wrong update"; + && underlyingSenderBalanceAfter == underlyingUserBalanceAfter + && underlyingSenderBalanceBefore == underlyingSenderBalanceAfter + amount + , "underlying balances wrong update"; + + assert account != e.msg.sender + && account == currentContract => underlyingSenderBalanceBefore == underlyingSenderBalanceAfter + amount + && underlyingUserBalanceBefore == underlyingUserBalanceAfter - amount + , "underlying balances wrong update"; + + assert account != e.msg.sender + && account != currentContract => underlyingSenderBalanceBefore == underlyingSenderBalanceAfter + amount + && underlyingUserBalanceBefore == underlyingUserBalanceAfter + , "underlying balances wrong update"; } - -// STATUS - verified // Check that values are updated correctly by `withdrawTo()` -rule withdrawToSpecBasic(env e){ - address account; uint256 amount; +rule withdrawToSpecBasic(env e) { + address account; + uint256 amount; require underlying() != currentContract; @@ -133,10 +141,8 @@ rule withdrawToSpecBasic(env e){ assert underlyingTotalBefore == underlyingTotalAfter, "underlying total was updated"; } - -// STATUS - verified // Check that values are updated correctly by `withdrawTo()` -rule withdrawToSpecWrapper(env e){ +rule withdrawToSpecWrapper(env e) { address account; uint256 amount; require underlying() != currentContract; @@ -148,18 +154,21 @@ rule withdrawToSpecWrapper(env e){ uint256 wrapperUserBalanceAfter = balanceOf(e, account); uint256 wrapperSenderBalanceAfter = balanceOf(e, e.msg.sender); - + assert account == e.msg.sender => wrapperUserBalanceBefore == wrapperSenderBalanceBefore - && wrapperUserBalanceAfter == wrapperSenderBalanceAfter - && wrapperUserBalanceBefore == wrapperUserBalanceAfter + amount, "wrapper user balance wrong update"; + && wrapperUserBalanceAfter == wrapperSenderBalanceAfter + && wrapperUserBalanceBefore == wrapperUserBalanceAfter + amount + , "wrapper user balance wrong update"; + assert account != e.msg.sender => wrapperSenderBalanceBefore == wrapperSenderBalanceAfter + amount - && wrapperUserBalanceBefore == wrapperUserBalanceAfter, "wrapper user balance wrong update"; + && wrapperUserBalanceBefore == wrapperUserBalanceAfter + , "wrapper user balance wrong update"; } // STATUS - verified -// cCheck that values are updated correctly by `withdrawTo()` -rule withdrawToSpecUnderlying(env e){ +// Check that values are updated correctly by `withdrawTo()` +rule withdrawToSpecUnderlying(env e) { address account; uint256 amount; require e.msg.sender != currentContract; @@ -175,22 +184,25 @@ rule withdrawToSpecUnderlying(env e){ uint256 underlyingUserBalanceAfter = underlyingBalanceOf(account); uint256 underlyingThisBalanceAfter = underlyingBalanceOf(currentContract); - assert account == e.msg.sender => underlyingSenderBalanceBefore == underlyingUserBalanceBefore - && underlyingSenderBalanceAfter == underlyingUserBalanceAfter - && underlyingUserBalanceBefore == underlyingUserBalanceAfter - amount, "underlying balances wrong update (acc == sender)"; - + assert account == e.msg.sender => underlyingSenderBalanceBefore == underlyingUserBalanceBefore + && underlyingSenderBalanceAfter == underlyingUserBalanceAfter + && underlyingUserBalanceBefore == underlyingUserBalanceAfter - amount + , "underlying balances wrong update (acc == sender)"; + assert account != e.msg.sender && account == currentContract => underlyingUserBalanceBefore == underlyingUserBalanceAfter - && underlyingSenderBalanceBefore == underlyingSenderBalanceAfter, "underlying balances wrong update (acc == contract)"; + && underlyingSenderBalanceBefore == underlyingSenderBalanceAfter + , "underlying balances wrong update (acc == contract)"; + assert account != e.msg.sender && account != currentContract => underlyingUserBalanceBefore == underlyingUserBalanceAfter - amount - && underlyingSenderBalanceBefore == underlyingSenderBalanceAfter - && underlyingThisBalanceBefore == underlyingThisBalanceAfter + amount, "underlying balances wrong update (acc != contract)"; + && underlyingSenderBalanceBefore == underlyingSenderBalanceAfter + && underlyingThisBalanceBefore == underlyingThisBalanceAfter + amount + , "underlying balances wrong update (acc != contract)"; } - -// STATUS - verified // Check that values are updated correctly by `_recover()` -rule recoverSpec(env e){ - address account; uint256 amount; +rule recoverSpec(env e) { + address account; + uint256 amount; uint256 wrapperTotalBefore = totalSupply(e); uint256 wrapperUserBalanceBefore = balanceOf(e, account); @@ -204,11 +216,15 @@ rule recoverSpec(env e){ uint256 wrapperTotalAfter = totalSupply(e); uint256 wrapperUserBalanceAfter = balanceOf(e, account); uint256 wrapperSenderBalanceAfter = balanceOf(e, e.msg.sender); - + assert wrapperTotalBefore == wrapperTotalAfter - value, "wrapper total wrong update"; + assert e.msg.sender == account => wrapperUserBalanceBefore == wrapperSenderBalanceBefore - && wrapperUserBalanceAfter == wrapperSenderBalanceAfter - && wrapperUserBalanceBefore == wrapperUserBalanceAfter - value, "wrapper balances wrong update"; + && wrapperUserBalanceAfter == wrapperSenderBalanceAfter + && wrapperUserBalanceBefore == wrapperUserBalanceAfter - value + , "wrapper balances wrong update"; + assert e.msg.sender != account => wrapperUserBalanceBefore == wrapperUserBalanceAfter - value - && wrapperSenderBalanceBefore == wrapperSenderBalanceAfter, "wrapper balances wrong update"; -} \ No newline at end of file + && wrapperSenderBalanceBefore == wrapperSenderBalanceAfter + , "wrapper balances wrong update"; +} diff --git a/certora/specs/erc20.spec b/certora/specs/erc20.spec index b12fec167..bb231962a 100644 --- a/certora/specs/erc20.spec +++ b/certora/specs/erc20.spec @@ -1,12 +1,12 @@ // erc20 methods methods { - name() returns (string) => DISPATCHER(true) - symbol() returns (string) => DISPATCHER(true) - decimals() returns (string) => DISPATCHER(true) - totalSupply() returns (uint256) => DISPATCHER(true) - balanceOf(address) returns (uint256) => DISPATCHER(true) - allowance(address,address) returns (uint) => DISPATCHER(true) - approve(address,uint256) returns (bool) => DISPATCHER(true) - transfer(address,uint256) returns (bool) => DISPATCHER(true) - transferFrom(address,address,uint256) returns (bool) => DISPATCHER(true) + name() returns (string) envfree => DISPATCHER(true) + symbol() returns (string) envfree => DISPATCHER(true) + decimals() returns (uint8) envfree => DISPATCHER(true) + totalSupply() returns (uint256) envfree => DISPATCHER(true) + balanceOf(address) returns (uint256) envfree => DISPATCHER(true) + allowance(address,address) returns (uint256) envfree => DISPATCHER(true) + approve(address,uint256) returns (bool) => DISPATCHER(true) + transfer(address,uint256) returns (bool) => DISPATCHER(true) + transferFrom(address,address,uint256) returns (bool) => DISPATCHER(true) }