From 3f1ee399102bb888577338a62e40fbb426ada4c7 Mon Sep 17 00:00:00 2001 From: Nick Armstrong Date: Mon, 28 Mar 2022 12:05:33 -0700 Subject: [PATCH] call trace error --- certora/applyHarness.patch | 14 +++---- certora/harnesses/ERC20VotesHarness.sol | 10 +++++ certora/scripts/ERC20VotesRule.sh | 1 - certora/specs/ERC20Votes.spec | 50 +++++++++++++++++-------- 4 files changed, 51 insertions(+), 24 deletions(-) diff --git a/certora/applyHarness.patch b/certora/applyHarness.patch index e7b66d707..7af5f82c8 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 16:41:46.000000000 -0700 ++++ access/AccessControl.sol 2022-03-24 18:08:46.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 16:41:46.000000000 -0700 ++++ governance/TimelockController.sol 2022-03-24 18:08: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"); @@ -41,7 +41,7 @@ diff -ruN governance/TimelockController.sol governance/TimelockController.sol +} 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 ++++ governance/utils/Votes.sol 2022-03-24 18:08:46.000000000 -0700 @@ -207,5 +207,5 @@ /** * @dev Must return the voting units held by an account. @@ -51,7 +51,7 @@ diff -ruN governance/utils/Votes.sol governance/utils/Votes.sol } 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 ++++ token/ERC20/ERC20.sol 2022-03-24 18:08:46.000000000 -0700 @@ -277,7 +277,7 @@ * - `account` cannot be the zero address. * - `account` must have at least `amount` tokens. @@ -72,7 +72,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 16:41:46.000000000 -0700 ++++ token/ERC20/extensions/ERC20FlashMint.sol 2022-03-24 18:08:46.000000000 -0700 @@ -40,9 +40,11 @@ require(token == address(this), "ERC20FlashMint: wrong token"); // silence warning about unused variable without the addition of bytecode. @@ -97,7 +97,7 @@ diff -ruN token/ERC20/extensions/ERC20FlashMint.sol token/ERC20/extensions/ERC20 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 ++++ token/ERC20/extensions/ERC20Votes.sol 2022-03-25 13:13:49.000000000 -0700 @@ -33,8 +33,8 @@ bytes32 private constant _DELEGATION_TYPEHASH = keccak256("Delegation(address delegatee,uint256 nonce,uint256 expiry)"); @@ -230,7 +230,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 16:41:46.000000000 -0700 ++++ token/ERC20/extensions/ERC20Wrapper.sol 2022-03-24 18:08: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. diff --git a/certora/harnesses/ERC20VotesHarness.sol b/certora/harnesses/ERC20VotesHarness.sol index 14b170bbf..b87879f80 100644 --- a/certora/harnesses/ERC20VotesHarness.sol +++ b/certora/harnesses/ERC20VotesHarness.sol @@ -18,5 +18,15 @@ contract ERC20VotesHarness is ERC20Votes { function burn(address account, uint256 amount) public { _burn(account, amount); } + + function delegateBySig( + address delegatee, + uint256 nonce, + uint256 expiry, + uint8 v, + bytes32 r, + bytes32 s + ) public virtual override { } + } diff --git a/certora/scripts/ERC20VotesRule.sh b/certora/scripts/ERC20VotesRule.sh index a29fd1ff9..6aac06c6c 100644 --- a/certora/scripts/ERC20VotesRule.sh +++ b/certora/scripts/ERC20VotesRule.sh @@ -19,5 +19,4 @@ certoraRun \ --optimistic_loop \ --rule ${rule} \ --msg "${msg}" \ - --staging \ # --rule_sanity \ \ No newline at end of file diff --git a/certora/specs/ERC20Votes.spec b/certora/specs/ERC20Votes.spec index 7adb3cca1..d3c95973d 100644 --- a/certora/specs/ERC20Votes.spec +++ b/certora/specs/ERC20Votes.spec @@ -10,7 +10,7 @@ methods { getPastTotalSupply(uint256) returns (uint256) delegate(address) _delegate(address, address) - delegateBySig(address, uint256, uint256, uint8, bytes32, bytes32) + // delegateBySig(address, uint256, uint256, uint8, bytes32, bytes32) totalSupply() returns (uint256) envfree _maxSupply() returns (uint224) envfree @@ -32,9 +32,13 @@ ghost userVotes(address) returns uint224; // sums the total votes for all users ghost totalVotes() returns mathint { - axiom totalVotes() > 0; + axiom totalVotes() >= 0; } +// helper + +invariant totalVotes_gte_accounts(address a, address b) + totalVotes() >= getVotes(a) + getVotes(b) hook Sstore _checkpoints[KEY address account][INDEX uint32 index].votes uint224 newVotes (uint224 oldVotes) STORAGE { @@ -95,32 +99,45 @@ invariant maxInt_constrains_numBlocks(address account) invariant fromBlock_constrains_numBlocks(address account) numCheckpoints(account) <= lastFromBlock(account) +// this fails, which makes sense because there is no require about the previous fromBlock invariant unique_checkpoints(address account) !doubleFromBlock(account) +// if an account has been delegated too, then both accounts must have a checkpoint +invariant delegated_implies_checkpoints(address delegator, address delegatee) + delegates(delegator) == delegatee => numCheckpoints(delegator) > 0 && numCheckpoints(delegatee) > 0 +{ preserved with (env e) { + require delegatee != 0; + require balanceOf(e, delegator) > 0; +}} + +// assumes neither account has delegated rule transfer_safe() { env e; uint256 amount; address a; address b; require a != b; + // requireInvariant totalVotes_gte_accounts(a, b); - uint256 votesA_pre = getVotes(a); - uint256 votesB_pre = getVotes(b); + address delegateA = delegates(a); + address delegateB = delegates(b); - require votesA_pre == erc20votes.balanceOf(e, a); - require votesB_pre == erc20votes.balanceOf(e, b); + uint256 votesA_pre = getVotes(delegateA); + uint256 votesB_pre = getVotes(delegateB); mathint totalVotes_pre = totalVotes(); erc20votes.transferFrom(e, a, b, amount); mathint totalVotes_post = totalVotes(); - uint256 votesA_post = getVotes(a); - uint256 votesB_post = getVotes(b); + uint256 votesA_post = getVotes(delegateA); + uint256 votesB_post = getVotes(delegateB); + // 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 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"; + assert delegateA == delegates(a) && delegateB == delegates(b), "delegates changed by transfer"; + assert delegateA != 0 => votesA_pre - votesA_post == amount, "a lost the proper amount of votes"; + assert delegateB != 0 => votesB_post - votesB_pre == amount, "b lost the proper amount of votes"; } @@ -144,7 +161,9 @@ rule delegator_votes_removed() { rule delegatee_receives_votes() { env e; address delegator; address delegatee; + require delegator != delegatee; + require delegates(delegator) != delegatee; uint256 delegator_bal = balanceOf(e, delegator); uint256 votes_= getVotes(delegatee); @@ -156,13 +175,14 @@ rule delegatee_receives_votes() { assert _votes == votes_ + delegator_bal, "delegatee did not receive votes"; } -rule previous_delegatee_zerod() { +rule previous_delegatee_zeroed() { env e; address delegator; address delegatee; address third; - require delegator != delegatee; require third != delegatee; require third != delegator; + require delegates(delegator) == third; + // for third to have been delegated to, it must have a checkpoint uint256 delegator_bal = balanceOf(e, delegator); uint256 votes_ = getVotes(third); @@ -171,16 +191,14 @@ rule previous_delegatee_zerod() { uint256 _votes = getVotes(third); - assert votes_ == votes_ - delegator_bal, "votes not removed from the previous delegatee"; + assert _votes == votes_ - delegator_bal, "votes not removed from the previous delegatee"; } -// passes +// passes with rule sanity rule delegate_contained() { env e; address delegator; address delegatee; address other; - require delegator != delegatee; - require other != delegator; require other != delegatee; require other != delegates(delegator);