From 2d6a89f09316211dbe6359d3c45810dc8324ccd7 Mon Sep 17 00:00:00 2001 From: Hadrien Croubois Date: Thu, 9 Mar 2023 13:16:35 +0100 Subject: [PATCH 1/9] wip --- certora/harnesses/ERC20VotesHarness.sol | 30 +++++ certora/harnesses/ERC721VotesHarness.sol | 17 +++ certora/specs.json | 6 + certora/specs/ERC20.spec | 3 +- certora/specs/ERC20Votes.spec | 148 +++++++++++++++++++++++ certora/specs/methods/IERC5805.spec | 11 ++ certora/specs/methods/IERC6372.spec | 4 + 7 files changed, 218 insertions(+), 1 deletion(-) create mode 100644 certora/harnesses/ERC20VotesHarness.sol create mode 100644 certora/harnesses/ERC721VotesHarness.sol create mode 100644 certora/specs/ERC20Votes.spec create mode 100644 certora/specs/methods/IERC5805.spec create mode 100644 certora/specs/methods/IERC6372.spec diff --git a/certora/harnesses/ERC20VotesHarness.sol b/certora/harnesses/ERC20VotesHarness.sol new file mode 100644 index 000000000..c4bc1b3a5 --- /dev/null +++ b/certora/harnesses/ERC20VotesHarness.sol @@ -0,0 +1,30 @@ +// SPDX-License-Identifier: MIT + +pragma solidity ^0.8.0; + +import "../patched/token/ERC20/extensions/ERC20Votes.sol"; + +contract ERC20VotesHarness is ERC20Votes { + constructor(string memory name, string memory symbol) ERC20(name, symbol) ERC20Permit(name) {} + + function mint(address account, uint256 amount) external { + _mint(account, amount); + } + + function burn(address account, uint256 amount) external { + _burn(account, amount); + } + + // inspection + 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).votes; + } + + function maxSupply() public view returns (uint224) { + return _maxSupply(); + } +} diff --git a/certora/harnesses/ERC721VotesHarness.sol b/certora/harnesses/ERC721VotesHarness.sol new file mode 100644 index 000000000..318ac80c7 --- /dev/null +++ b/certora/harnesses/ERC721VotesHarness.sol @@ -0,0 +1,17 @@ +// SPDX-License-Identifier: MIT + +pragma solidity ^0.8.0; + +import "../patched/token/ERC721/extensions/ERC721Votes.sol"; + +contract ERC721VotesHarness is ERC721Votes { + constructor(string memory name, string memory symbol) ERC721(name, symbol) EIP712(name, symbol) {} + + function mint(address account, uint256 tokenID) public { + _mint(account, tokenID); + } + + function burn(uint256 tokenID) public { + _burn(tokenID); + } +} diff --git a/certora/specs.json b/certora/specs.json index 228e85fe4..c85c72ca0 100644 --- a/certora/specs.json +++ b/certora/specs.json @@ -29,6 +29,12 @@ ], "options": ["--optimistic_loop"] }, + { + "spec": "ERC20Votes", + "contract": "ERC20VotesHarness", + "files": ["certora/harnesses/ERC20VotesHarness.sol"], + "options": ["--optimistic_loop"] + }, { "spec": "ERC20Wrapper", "contract": "ERC20WrapperHarness", diff --git a/certora/specs/ERC20.spec b/certora/specs/ERC20.spec index 85f95e706..3cc5c1d77 100644 --- a/certora/specs/ERC20.spec +++ b/certora/specs/ERC20.spec @@ -31,7 +31,8 @@ hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) STOR └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ invariant totalSupplyIsSumOfBalances() - totalSupply() == sumOfBalances() + totalSupply() == sumOfBalances() && + totalSupply() <= max_uint256 /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ diff --git a/certora/specs/ERC20Votes.spec b/certora/specs/ERC20Votes.spec new file mode 100644 index 000000000..4efe423dc --- /dev/null +++ b/certora/specs/ERC20Votes.spec @@ -0,0 +1,148 @@ +import "helpers.spec" +import "methods/IERC20.spec" +import "methods/IERC5805.spec" +import "methods/IERC6372.spec" +import "ERC20.spec" + +methods { + numCheckpoints(address) returns (uint32) envfree + ckptFromBlock(address, uint32) returns (uint32) envfree + ckptVotes(address, uint32) returns (uint224) envfree + maxSupply() returns (uint224) envfree +} + +use invariant totalSupplyIsSumOfBalances + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Ghost: user (current) voting weight │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +ghost lastUserVotes(address) returns uint224 { + init_state axiom forall address a. lastUserVotes(a) == 0; +} + +ghost userCkptNumber(address) returns uint32 { + init_state axiom forall address a. userCkptNumber(a) == 0; +} + +ghost lastUserIndex(address) returns uint32; +ghost lastUserTimepoint(address) returns uint32; + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Ghost: total voting weight │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +ghost totalVotes() returns uint224 { + init_state axiom totalVotes() == 0; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Ghost: duplicate checkpoint detection │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +ghost lastUserDuplicate(address) returns bool { + init_state axiom forall address a. lastUserDuplicate(a) == false; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Hook │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +hook Sstore currentContract._checkpoints[KEY address account][INDEX uint32 index].votes uint224 newVotes (uint224 oldVotes) STORAGE { + havoc lastUserVotes assuming + lastUserVotes@new(account) == newVotes; + + havoc totalVotes assuming + totalVotes@new() == totalVotes@old() + newVotes - lastUserVotes(account); + + havoc lastUserIndex assuming + lastUserIndex@new(account) == index; +} + +hook Sstore currentContract._checkpoints[KEY address account][INDEX uint32 index].fromBlock uint32 newTimepoint (uint32 oldTimepoint) STORAGE { + havoc lastUserTimepoint assuming + lastUserTimepoint@new(account) == newTimepoint; + + havoc userCkptNumber assuming + userCkptNumber@new(account) == index + 1; + + havoc lastUserDuplicate assuming + lastUserDuplicate@new(account) == (newTimepoint == lastUserTimepoint(account)); + +} + + + + + + +definition max_uint224() returns uint224 = 0xffffffffffffffffffffffffffff; + + + + +invariant clockMode(env e) + clock(e) == e.block.number || clock(e) == e.block.timestamp + + +invariant numCheckpointsConsistency(address a) + userCkptNumber(a) == numCheckpoints(a) && + userCkptNumber(a) <= max_uint32 + +invariant lastUserVotesAndTimepointConsistency(address a) + numCheckpoints(a) > 0 => ( + lastUserIndex(a) == numCheckpoints(a) - 1 && + lastUserIndex(a) <= max_uint32 && + lastUserVotes(a) == ckptVotes(a, lastUserIndex(a)) && + lastUserVotes(a) <= max_uint224() && + lastUserTimepoint(a) == ckptFromBlock(a, lastUserIndex(a)) && + lastUserTimepoint(a) <= max_uint224() + ) + + + + + + + + + + + +/* +invariant noDuplicate(address a) + !lastUserDuplicate(a) + +// passes +invariant userVotesOverflow() + forall address a. lastUserVotes(a) <= max_uint256 + +invariant userVotes(env e) + forall address a. userCkptNumber(a) > 0 => lastUserVotes(a) == getVotes(e, a) + { + preserved { + requireInvariant totalSupplyIsSumOfBalances; + } + } + +invariant userVotesLessTotalVotes() + forall address a. userCkptNumber(a) > 0 => lastUserVotes(a) <= totalVotes() + { + preserved { + requireInvariant totalSupplyIsSumOfBalances; + } + } + +// passes +invariant totalVotesLessTotalSupply() + totalVotes() <= totalSupply() + { + preserved { + requireInvariant totalSupplyIsSumOfBalances; + } + } +*/ \ No newline at end of file diff --git a/certora/specs/methods/IERC5805.spec b/certora/specs/methods/IERC5805.spec new file mode 100644 index 000000000..04251a302 --- /dev/null +++ b/certora/specs/methods/IERC5805.spec @@ -0,0 +1,11 @@ +methods { + // view + getVotes(address) returns (uint256) + getPastVotes(address, uint256) returns (uint256) + getPastTotalSupply(uint256) returns (uint256) + delegates(address) returns (address) envfree + + // external + delegate(address) + delegateBySig(address, uint256, uint256, uint8, bytes32, bytes32) +} \ No newline at end of file diff --git a/certora/specs/methods/IERC6372.spec b/certora/specs/methods/IERC6372.spec new file mode 100644 index 000000000..606bfe3e0 --- /dev/null +++ b/certora/specs/methods/IERC6372.spec @@ -0,0 +1,4 @@ +methods { + clock() returns (uint48) + CLOCK_MODE() returns (string) +} \ No newline at end of file From d66a6f2443ea980ea283cc3d29dfbeebd4015312 Mon Sep 17 00:00:00 2001 From: Hadrien Croubois Date: Thu, 27 Apr 2023 14:16:17 +0200 Subject: [PATCH 2/9] wip --- ...oken_ERC20_extensions_ERC20Votes.sol.patch | 19 +++ certora/specs/ERC20Votes.spec | 109 ++++++++++-------- 2 files changed, 79 insertions(+), 49 deletions(-) create mode 100644 certora/diff/token_ERC20_extensions_ERC20Votes.sol.patch diff --git a/certora/diff/token_ERC20_extensions_ERC20Votes.sol.patch b/certora/diff/token_ERC20_extensions_ERC20Votes.sol.patch new file mode 100644 index 000000000..7aa07ec68 --- /dev/null +++ b/certora/diff/token_ERC20_extensions_ERC20Votes.sol.patch @@ -0,0 +1,19 @@ +--- token/ERC20/extensions/ERC20Votes.sol 2023-04-27 13:16:53.923627178 +0200 ++++ token/ERC20/extensions/ERC20Votes.sol 2023-04-27 13:27:00.856088231 +0200 +@@ -281,10 +281,11 @@ + /** + * @dev Access an element of the array without performing bounds check. The position is assumed to be within bounds. + */ +- function _unsafeAccess(Checkpoint[] storage ckpts, uint256 pos) private pure returns (Checkpoint storage result) { +- assembly { +- mstore(0, ckpts.slot) +- result.slot := add(keccak256(0, 0x20), pos) +- } ++ function _unsafeAccess(Checkpoint[] storage ckpts, uint256 pos) private view returns (Checkpoint storage result) { ++ return ckpts[pos]; // explicit (safe) for formal verification hooking ++ // assembly { ++ // mstore(0, ckpts.slot) ++ // result.slot := add(keccak256(0, 0x20), pos) ++ // } + } + } diff --git a/certora/specs/ERC20Votes.spec b/certora/specs/ERC20Votes.spec index 4efe423dc..d20f6fb78 100644 --- a/certora/specs/ERC20Votes.spec +++ b/certora/specs/ERC20Votes.spec @@ -15,97 +15,108 @@ use invariant totalSupplyIsSumOfBalances /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Ghost: user (current) voting weight │ +│ Helpers │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -ghost lastUserVotes(address) returns uint224 { - init_state axiom forall address a. lastUserVotes(a) == 0; -} - -ghost userCkptNumber(address) returns uint32 { - init_state axiom forall address a. userCkptNumber(a) == 0; -} - -ghost lastUserIndex(address) returns uint32; -ghost lastUserTimepoint(address) returns uint32; +definition max_uint224() returns uint224 = 0xffffffffffffffffffffffffffff; +definition lastCheckpoint(address a) returns uint32 = to_uint32(numCheckpoints(a) - 1); /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Ghost: total voting weight │ +│ Ghost & hooks │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ + + +/* ghost totalVotes() returns uint224 { init_state axiom totalVotes() == 0; } -/* -┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Ghost: duplicate checkpoint detection │ -└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ -*/ -ghost lastUserDuplicate(address) returns bool { - init_state axiom forall address a. lastUserDuplicate(a) == false; +ghost mapping(address => uint256) userVotes { + init_state axiom forall address a. userVotes[a] == 0; } -/* -┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Hook │ -└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ -*/ -hook Sstore currentContract._checkpoints[KEY address account][INDEX uint32 index].votes uint224 newVotes (uint224 oldVotes) STORAGE { - havoc lastUserVotes assuming - lastUserVotes@new(account) == newVotes; +ghost mapping(address => uint32) userLast { + init_state axiom forall address a. userLast[a] == 0; +} - havoc totalVotes assuming - totalVotes@new() == totalVotes@old() + newVotes - lastUserVotes(account); +ghost mapping(address => uint32) userClock { + init_state axiom forall address a. userClock[a] == 0; +} + +hook Sstore currentContract._checkpoints[KEY address account][INDEX uint32 index].votes uint224 newVotes (uint224 oldVotes) STORAGE { + havoc totalVotes assuming totalVotes@new() == totalVotes@old() + newVotes - userVotes[account]; - havoc lastUserIndex assuming - lastUserIndex@new(account) == index; + userVotes[account] = newVotes; + userLast[account] = index; } hook Sstore currentContract._checkpoints[KEY address account][INDEX uint32 index].fromBlock uint32 newTimepoint (uint32 oldTimepoint) STORAGE { - havoc lastUserTimepoint assuming - lastUserTimepoint@new(account) == newTimepoint; + userClock[account] = newTimepoint; +} +*/ - havoc userCkptNumber assuming - userCkptNumber@new(account) == index + 1; - havoc lastUserDuplicate assuming - lastUserDuplicate@new(account) == (newTimepoint == lastUserTimepoint(account)); -} -definition max_uint224() returns uint224 = 0xffffffffffffffffffffffffffff; +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Invariant: clock │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ invariant clockMode(env e) clock(e) == e.block.number || clock(e) == e.block.timestamp -invariant numCheckpointsConsistency(address a) - userCkptNumber(a) == numCheckpoints(a) && - userCkptNumber(a) <= max_uint32 -invariant lastUserVotesAndTimepointConsistency(address a) + + + +invariant userClockInThePast(env e, address a) + numCheckpoints(a) > 0 => ckptFromBlock(lastCheckpoint(a)) <= clock(e) + { + preserved with (env e2) { + require clock(e2) <= clock(e); + } + } + +/* +invariant hooksAreCorrect(env e, address a) numCheckpoints(a) > 0 => ( - lastUserIndex(a) == numCheckpoints(a) - 1 && - lastUserIndex(a) <= max_uint32 && - lastUserVotes(a) == ckptVotes(a, lastUserIndex(a)) && - lastUserVotes(a) <= max_uint224() && - lastUserTimepoint(a) == ckptFromBlock(a, lastUserIndex(a)) && - lastUserTimepoint(a) <= max_uint224() + userLast(a) == ckptFromBlock(lastCheckpoint(a)) && + userVotes(a) == ckptVotes(lastCheckpoint(a)) ) +*/ + + + + +/* +invariant userVotesAndClockConsistency(address a) + numCheckpoints(a) > 0 => ( + userLast(a) == numCheckpoints(a) - 1 && + userLast(a) <= max_uint32 && + userVotes(a) == ckptVotes(a, lastUserIndex(a)) && + userVotes(a) <= max_uint224() && + userClock(a) == ckptFromBlock(a, lastUserIndex(a)) && + userClock(a) <= max_uint224() + ) +*/ + From 96661f8639e5c00efcdf2ce6e6cb7d086180f4ae Mon Sep 17 00:00:00 2001 From: Hadrien Croubois Date: Thu, 27 Apr 2023 22:58:32 +0200 Subject: [PATCH 3/9] some erc20Votes specs working --- certora/specs/ERC20Votes.spec | 139 +++++++++++----------------- certora/specs/methods/IERC5805.spec | 2 +- 2 files changed, 54 insertions(+), 87 deletions(-) diff --git a/certora/specs/ERC20Votes.spec b/certora/specs/ERC20Votes.spec index d20f6fb78..430b149e1 100644 --- a/certora/specs/ERC20Votes.spec +++ b/certora/specs/ERC20Votes.spec @@ -19,55 +19,39 @@ use invariant totalSupplyIsSumOfBalances └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ definition max_uint224() returns uint224 = 0xffffffffffffffffffffffffffff; -definition lastCheckpoint(address a) returns uint32 = to_uint32(numCheckpoints(a) - 1); /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ Ghost & hooks │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ - - -/* ghost totalVotes() returns uint224 { init_state axiom totalVotes() == 0; } -ghost mapping(address => uint256) userVotes { +ghost mapping(address => uint224) userVotes { init_state axiom forall address a. userVotes[a] == 0; } -ghost mapping(address => uint32) userLast { - init_state axiom forall address a. userLast[a] == 0; -} - ghost mapping(address => uint32) userClock { init_state axiom forall address a. userClock[a] == 0; } +ghost mapping(address => uint32) userCkpts { + init_state axiom forall address a. userCkpts[a] == 0; +} + hook Sstore currentContract._checkpoints[KEY address account][INDEX uint32 index].votes uint224 newVotes (uint224 oldVotes) STORAGE { havoc totalVotes assuming totalVotes@new() == totalVotes@old() + newVotes - userVotes[account]; userVotes[account] = newVotes; - userLast[account] = index; + userCkpts[account] = index; } hook Sstore currentContract._checkpoints[KEY address account][INDEX uint32 index].fromBlock uint32 newTimepoint (uint32 oldTimepoint) STORAGE { userClock[account] = newTimepoint; + userCkpts[account] = index; } -*/ - - - - - - - - - - - - /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ @@ -77,13 +61,26 @@ hook Sstore currentContract._checkpoints[KEY address account][INDEX uint32 index invariant clockMode(env e) clock(e) == e.block.number || clock(e) == e.block.timestamp +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Invariant: hook correctly track lastest checkpoint │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +invariant hooksAreCorrect(address a) + numCheckpoints(a) > 0 => ( + userVotes[a] == getVotes(a) && + userVotes[a] == ckptVotes(a, numCheckpoints(a) - 1) && + userClock[a] == ckptFromBlock(a, numCheckpoints(a) - 1) && + userCkpts[a] == numCheckpoints(a) - 1 + ) - - - - +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Invariant: checkpoint is not in the future │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ invariant userClockInThePast(env e, address a) - numCheckpoints(a) > 0 => ckptFromBlock(lastCheckpoint(a)) <= clock(e) + numCheckpoints(a) > 0 => ckptFromBlock(a, numCheckpoints(a) - 1) <= clock(e) { preserved with (env e2) { require clock(e2) <= clock(e); @@ -91,69 +88,39 @@ invariant userClockInThePast(env e, address a) } /* -invariant hooksAreCorrect(env e, address a) - numCheckpoints(a) > 0 => ( - userLast(a) == ckptFromBlock(lastCheckpoint(a)) && - userVotes(a) == ckptVotes(lastCheckpoint(a)) - ) -*/ - - - - - - - - -/* -invariant userVotesAndClockConsistency(address a) - numCheckpoints(a) > 0 => ( - userLast(a) == numCheckpoints(a) - 1 && - userLast(a) <= max_uint32 && - userVotes(a) == ckptVotes(a, lastUserIndex(a)) && - userVotes(a) <= max_uint224() && - userClock(a) == ckptFromBlock(a, lastUserIndex(a)) && - userClock(a) <= max_uint224() - ) +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Invariant: checkpoint clock is strictly increassing (implies no duplicate) │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ +invariant checkpointClockIncreassing(address a) + numCheckpoints(a) > 1 => ckptFromBlock(a, numCheckpoints(a) - 2) < ckptFromBlock(a, numCheckpoints(a) - 1) + { + preserved with (env e) { + requireInvariant userClockInThePast(e, a); + } + } +/// For some reason "sumOfBalances" is not tracking correctly ... +/// ... and we get counter example where totalSupply is more than the sum of involved balances +// invariant totalVotesLessTotalSupply() +// totalVotes() <= totalSupply() +// { +// preserved { +// requireInvariant totalSupplyIsSumOfBalances; +// } +// } - -/* -invariant noDuplicate(address a) - !lastUserDuplicate(a) - -// passes -invariant userVotesOverflow() - forall address a. lastUserVotes(a) <= max_uint256 - -invariant userVotes(env e) - forall address a. userCkptNumber(a) > 0 => lastUserVotes(a) == getVotes(e, a) - { - preserved { - requireInvariant totalSupplyIsSumOfBalances; - } - } - -invariant userVotesLessTotalVotes() - forall address a. userCkptNumber(a) > 0 => lastUserVotes(a) <= totalVotes() - { - preserved { - requireInvariant totalSupplyIsSumOfBalances; - } - } - -// passes -invariant totalVotesLessTotalSupply() - totalVotes() <= totalSupply() - { - preserved { - requireInvariant totalSupplyIsSumOfBalances; - } - } -*/ \ No newline at end of file +/// For some reason "sumOfBalances" is not tracking correctly ... +/// ... and we get counter example where totalSupply is more than the sum of involved balances +// invariant userVotesLessTotalVotes(address a) +// numCheckpoints(a) > 0 => getVotes(a) <= totalVotes() +// { +// preserved { +// requireInvariant totalSupplyIsSumOfBalances; +// } +// } diff --git a/certora/specs/methods/IERC5805.spec b/certora/specs/methods/IERC5805.spec index 04251a302..f1950c130 100644 --- a/certora/specs/methods/IERC5805.spec +++ b/certora/specs/methods/IERC5805.spec @@ -1,6 +1,6 @@ methods { // view - getVotes(address) returns (uint256) + getVotes(address) returns (uint256) envfree getPastVotes(address, uint256) returns (uint256) getPastTotalSupply(uint256) returns (uint256) delegates(address) returns (address) envfree From 1aee3b40f2b4d502163b105ecd7ea552dc343d14 Mon Sep 17 00:00:00 2001 From: Hadrien Croubois Date: Thu, 27 Apr 2023 23:01:25 +0200 Subject: [PATCH 4/9] Merge branch 'CI/FV/run-on-ACMR' into fv/ERC20Votes --- .github/workflows/formal-verification.yml | 14 ++++- certora/run.js | 64 ++++++++++++++++------- certora/specs/Ownable.spec | 4 +- 3 files changed, 61 insertions(+), 21 deletions(-) diff --git a/.github/workflows/formal-verification.yml b/.github/workflows/formal-verification.yml index 29c02541c..833d02619 100644 --- a/.github/workflows/formal-verification.yml +++ b/.github/workflows/formal-verification.yml @@ -33,8 +33,20 @@ jobs: if: github.event_name != 'pull_request' || contains(github.event.pull_request.labels.*.name, 'formal-verification') steps: - uses: actions/checkout@v3 + with: + fetch-depth: 0 - name: Set up environment uses: ./.github/actions/setup + - name: identify specs that need to be run + id: arguments + run: | + if [[ ${{ github.event_name }} = 'pull_request' ]]; + then + RESULT=$(git diff ${{ github.event.pull_request.head.sha }}..${{ github.event.pull_request.base.sha }} --name-only certora/specs/*.spec | while IFS= read -r file; do [[ -f $file ]] && basename "${file%.spec}"; done) + else + RESULT='--all' + fi + echo "result=$RESULT" >> "$GITHUB_OUTPUT" - name: Install python uses: actions/setup-python@v4 with: @@ -55,6 +67,6 @@ jobs: - name: Verify specification run: | make -C certora apply - node certora/run.js >> "$GITHUB_STEP_SUMMARY" + node certora/run.js ${{ steps.arguments.outputs.result }} >> "$GITHUB_STEP_SUMMARY" env: CERTORAKEY: ${{ secrets.CERTORAKEY }} diff --git a/certora/run.js b/certora/run.js index f3234c1a3..2dc7d0181 100644 --- a/certora/run.js +++ b/certora/run.js @@ -1,37 +1,65 @@ #!/usr/bin/env node // USAGE: -// node certora/run.js [[CONTRACT_NAME:]SPEC_NAME] [OPTIONS...] +// node certora/run.js [[CONTRACT_NAME:]SPEC_NAME]* [--all] [--options OPTIONS...] [--specs PATH] // EXAMPLES: +// node certora/run.js --all // node certora/run.js AccessControl // node certora/run.js AccessControlHarness:AccessControl -const MAX_PARALLEL = 4; - -let specs = require(__dirname + '/specs.json'); - const proc = require('child_process'); const { PassThrough } = require('stream'); const events = require('events'); -const limit = require('p-limit')(MAX_PARALLEL); -let [, , request = '', ...extraOptions] = process.argv; -if (request.startsWith('-')) { - extraOptions.unshift(request); - request = ''; +const argv = require('yargs') + .env('') + .options({ + all: { + alias: 'a', + type: 'boolean', + }, + spec: { + alias: 's', + type: 'string', + default: __dirname + '/specs.json', + }, + parallel: { + alias: 'p', + type: 'number', + default: 4, + }, + options: { + alias: 'o', + type: 'array', + default: [], + }, + }).argv; + +function match(entry, request) { + const [reqSpec, reqContract] = request.split(':').reverse(); + return entry.spec == reqSpec && (!reqContract || entry.contract == reqContract); } -if (request) { - const [reqSpec, reqContract] = request.split(':').reverse(); - specs = Object.values(specs).filter(s => reqSpec === s.spec && (!reqContract || reqContract === s.contract)); - if (specs.length === 0) { - console.error(`Error: Requested spec '${request}' not found in specs.json`); - process.exit(1); +const specs = require(argv.spec).filter(s => argv.all || argv._.some(r => match(s, r))); +const limit = require('p-limit')(argv.parallel); + +if (argv._.length == 0 && !argv.all) { + console.error(`Warning: No specs requested. Did you forgot to toggle '--all'?`); +} + +for (const r of argv._) { + if (!specs.some(s => match(s, r))) { + console.error(`Error: Requested spec '${r}' not found in ${argv.spec}`); + process.exitCode = 1; } } -for (const { spec, contract, files, options = [] } of Object.values(specs)) { - limit(runCertora, spec, contract, files, [...options.flatMap(opt => opt.split(' ')), ...extraOptions]); +if (process.exitCode) { + process.exit(process.exitCode); +} + +for (const { spec, contract, files, options = [] } of specs) { + limit(runCertora, spec, contract, files, [...options.flatMap(opt => opt.split(' ')), ...argv.options]); } // Run certora, aggregate the output and print it at the end diff --git a/certora/specs/Ownable.spec b/certora/specs/Ownable.spec index 48bd84d13..4fdfeb09c 100644 --- a/certora/specs/Ownable.spec +++ b/certora/specs/Ownable.spec @@ -62,10 +62,10 @@ rule onlyCurrentOwnerCanCallOnlyOwner(env e) { │ Rule: ownership can only change in specific ways │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -rule onlyOwnerOrPendingOwnerCanChangeOwnership(env e, method f) { +rule onlyOwnerOrPendingOwnerCanChangeOwnership(env e) { address oldCurrent = owner(); - calldataarg args; + method f; calldataarg args; f(e, args); address newCurrent = owner(); From 26f7ce20813083882ed0b4081f7e97a1a349eecd Mon Sep 17 00:00:00 2001 From: Hadrien Croubois Date: Thu, 27 Apr 2023 23:16:27 +0200 Subject: [PATCH 5/9] fix CI --- .github/workflows/formal-verification.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/formal-verification.yml b/.github/workflows/formal-verification.yml index 833d02619..f94152a52 100644 --- a/.github/workflows/formal-verification.yml +++ b/.github/workflows/formal-verification.yml @@ -42,7 +42,7 @@ jobs: run: | if [[ ${{ github.event_name }} = 'pull_request' ]]; then - RESULT=$(git diff ${{ github.event.pull_request.head.sha }}..${{ github.event.pull_request.base.sha }} --name-only certora/specs/*.spec | while IFS= read -r file; do [[ -f $file ]] && basename "${file%.spec}"; done) + RESULT=$(git diff ${{ github.event.pull_request.head.sha }}..${{ github.event.pull_request.base.sha }} --name-only certora/specs/*.spec | while IFS= read -r file; do [[ -f $file ]] && basename "${file%.spec}"; done | tr "\n" " ") else RESULT='--all' fi From 9cd73f76b2e734a1383613d0ff419b8da263fef4 Mon Sep 17 00:00:00 2001 From: Hadrien Croubois Date: Thu, 27 Apr 2023 23:16:33 +0200 Subject: [PATCH 6/9] codespell --- certora/specs/ERC20Votes.spec | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/certora/specs/ERC20Votes.spec b/certora/specs/ERC20Votes.spec index 430b149e1..dbc83cd62 100644 --- a/certora/specs/ERC20Votes.spec +++ b/certora/specs/ERC20Votes.spec @@ -63,7 +63,7 @@ invariant clockMode(env e) /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Invariant: hook correctly track lastest checkpoint │ +│ Invariant: hook correctly track latest checkpoint │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ invariant hooksAreCorrect(address a) From 19b6505a6220d2996dbfa2c0d17060b84f6e72c1 Mon Sep 17 00:00:00 2001 From: Hadrien Croubois Date: Thu, 27 Apr 2023 23:19:17 +0200 Subject: [PATCH 7/9] lint --- certora/specs/methods/IERC5805.spec | 2 +- certora/specs/methods/IERC6372.spec | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/certora/specs/methods/IERC5805.spec b/certora/specs/methods/IERC5805.spec index f1950c130..278239db7 100644 --- a/certora/specs/methods/IERC5805.spec +++ b/certora/specs/methods/IERC5805.spec @@ -8,4 +8,4 @@ methods { // external delegate(address) delegateBySig(address, uint256, uint256, uint8, bytes32, bytes32) -} \ No newline at end of file +} diff --git a/certora/specs/methods/IERC6372.spec b/certora/specs/methods/IERC6372.spec index 606bfe3e0..70978df08 100644 --- a/certora/specs/methods/IERC6372.spec +++ b/certora/specs/methods/IERC6372.spec @@ -1,4 +1,4 @@ methods { clock() returns (uint48) CLOCK_MODE() returns (string) -} \ No newline at end of file +} From 5e7a95e638e12d083da7002eddcf504f54b3bff6 Mon Sep 17 00:00:00 2001 From: Hadrien Croubois Date: Fri, 28 Apr 2023 14:51:14 +0200 Subject: [PATCH 8/9] wip --- certora/harnesses/ERC20VotesHarness.sol | 8 + certora/specs/ERC20Votes.spec | 326 ++++++++++++++++++++---- 2 files changed, 288 insertions(+), 46 deletions(-) diff --git a/certora/harnesses/ERC20VotesHarness.sol b/certora/harnesses/ERC20VotesHarness.sol index c4bc1b3a5..7c155299a 100644 --- a/certora/harnesses/ERC20VotesHarness.sol +++ b/certora/harnesses/ERC20VotesHarness.sol @@ -24,6 +24,14 @@ contract ERC20VotesHarness is ERC20Votes { return checkpoints(account, pos).votes; } + function ckptFromBlockTotalSupply(uint32 pos) public view returns (uint32) { + return checkpointsTotalSupply(pos).fromBlock; + } + + function ckptVotesTotalSupply(uint32 pos) public view returns (uint224) { + return checkpointsTotalSupply(pos).votes; + } + function maxSupply() public view returns (uint224) { return _maxSupply(); } diff --git a/certora/specs/ERC20Votes.spec b/certora/specs/ERC20Votes.spec index dbc83cd62..4c2fe6f2b 100644 --- a/certora/specs/ERC20Votes.spec +++ b/certora/specs/ERC20Votes.spec @@ -5,10 +5,13 @@ import "methods/IERC6372.spec" import "ERC20.spec" methods { - numCheckpoints(address) returns (uint32) envfree - ckptFromBlock(address, uint32) returns (uint32) envfree - ckptVotes(address, uint32) returns (uint224) envfree - maxSupply() returns (uint224) envfree + numCheckpoints(address) returns (uint32) envfree + ckptFromBlock(address, uint32) returns (uint32) envfree + ckptVotes(address, uint32) returns (uint224) envfree + numCheckpointsTotalSupply() returns (uint32) envfree + ckptFromBlockTotalSupply(uint32) returns (uint32) envfree + ckptVotesTotalSupply(uint32) returns (uint224) envfree + maxSupply() returns (uint224) envfree } use invariant totalSupplyIsSumOfBalances @@ -22,35 +25,30 @@ definition max_uint224() returns uint224 = 0xffffffffffffffffffffffffffff; /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Ghost & hooks │ +│ Ghost & hooks: total delegated │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -ghost totalVotes() returns uint224 { - init_state axiom totalVotes() == 0; +ghost mapping(address => uint256) balanceOf { + init_state axiom forall address a. balanceOf[a] == 0; } -ghost mapping(address => uint224) userVotes { - init_state axiom forall address a. userVotes[a] == 0; +ghost mapping(address => address) delegates { + init_state axiom forall address a. delegates[a] == 0; } -ghost mapping(address => uint32) userClock { - init_state axiom forall address a. userClock[a] == 0; +ghost mapping(address => uint256) getVotes { + init_state axiom forall address a. getVotes[a] == 0; } -ghost mapping(address => uint32) userCkpts { - init_state axiom forall address a. userCkpts[a] == 0; +hook Sstore _balances[KEY address account] uint256 newAmount (uint256 oldAmount) STORAGE { + balanceOf[account] = newAmount; + getVotes[delegates[account]] = getVotes[delegates[account]] + newAmount - oldAmount; } -hook Sstore currentContract._checkpoints[KEY address account][INDEX uint32 index].votes uint224 newVotes (uint224 oldVotes) STORAGE { - havoc totalVotes assuming totalVotes@new() == totalVotes@old() + newVotes - userVotes[account]; - - userVotes[account] = newVotes; - userCkpts[account] = index; -} - -hook Sstore currentContract._checkpoints[KEY address account][INDEX uint32 index].fromBlock uint32 newTimepoint (uint32 oldTimepoint) STORAGE { - userClock[account] = newTimepoint; - userCkpts[account] = index; +hook Sstore _delegates[KEY address account] address newDelegate (address oldDelegate) STORAGE { + delegates[account] = newDelegate; + getVotes[oldDelegate] = getVotes[oldDelegate] - balanceOf[account]; + getVotes[newDelegate] = getVotes[newDelegate] + balanceOf[account]; } /* @@ -66,20 +64,28 @@ invariant clockMode(env e) │ Invariant: hook correctly track latest checkpoint │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -invariant hooksAreCorrect(address a) - numCheckpoints(a) > 0 => ( - userVotes[a] == getVotes(a) && - userVotes[a] == ckptVotes(a, numCheckpoints(a) - 1) && - userClock[a] == ckptFromBlock(a, numCheckpoints(a) - 1) && - userCkpts[a] == numCheckpoints(a) - 1 - ) +invariant delegationConsistency(address a) + balanceOf(a) == balanceOf[a] && + delegates(a) == delegates[a] && + getVotes(a) == (a == 0 ? 0 : getVotes[a]) + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Invariant: totalSupply is checkpointed │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +invariant totalSupplyTracked() + totalSupply() > 0 => numCheckpointsTotalSupply() > 0 + +invariant totalSupplyLatest() + numCheckpointsTotalSupply() > 0 => ckptVotesTotalSupply(numCheckpointsTotalSupply() - 1) == totalSupply() /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ Invariant: checkpoint is not in the future │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -invariant userClockInThePast(env e, address a) +invariant checkpointInThePast(env e, address a) numCheckpoints(a) > 0 => ckptFromBlock(a, numCheckpoints(a) - 1) <= clock(e) { preserved with (env e2) { @@ -87,6 +93,14 @@ invariant userClockInThePast(env e, address a) } } +invariant totalCheckpointInThePast(env e) + numCheckpointsTotalSupply() > 0 => ckptFromBlockTotalSupply(numCheckpointsTotalSupply() - 1) <= clock(e) + { + preserved with (env e2) { + require clock(e2) <= clock(e); + } + } + /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ Invariant: checkpoint clock is strictly increassing (implies no duplicate) │ @@ -96,24 +110,17 @@ invariant checkpointClockIncreassing(address a) numCheckpoints(a) > 1 => ckptFromBlock(a, numCheckpoints(a) - 2) < ckptFromBlock(a, numCheckpoints(a) - 1) { preserved with (env e) { - requireInvariant userClockInThePast(e, a); + requireInvariant checkpointInThePast(e, a); } } - - - - - -/// For some reason "sumOfBalances" is not tracking correctly ... -/// ... and we get counter example where totalSupply is more than the sum of involved balances -// invariant totalVotesLessTotalSupply() -// totalVotes() <= totalSupply() -// { -// preserved { -// requireInvariant totalSupplyIsSumOfBalances; -// } -// } +invariant totalCheckpointClockIncreassing() + numCheckpointsTotalSupply() > 1 => ckptFromBlockTotalSupply(numCheckpointsTotalSupply() - 2) < ckptFromBlockTotalSupply(numCheckpointsTotalSupply() - 1) + { + preserved with (env e) { + requireInvariant totalCheckpointInThePast(e); + } + } /// For some reason "sumOfBalances" is not tracking correctly ... /// ... and we get counter example where totalSupply is more than the sum of involved balances @@ -124,3 +131,230 @@ invariant checkpointClockIncreassing(address a) // requireInvariant totalSupplyIsSumOfBalances; // } // } + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Invariant: Don't track votes delegated to address 0 │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +invariant addressZeroNoCheckpoints() + numCheckpoints(0) == 0 + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Invariant: Don't track votes delegated to address 0 │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule checkpointsImmutable(env e, method f) + filtered { f -> !f.isView } +{ + address account; + uint32 index; + + require index < numCheckpoints(account); + uint224 valueBefore = ckptVotes(account, index); + uint32 clockBefore = ckptFromBlock(account, index); + + calldataarg args; f(e, args); + + uint224 valueAfter = ckptVotes@withrevert(account, index); + assert !lastReverted; + uint32 clockAfter = ckptFromBlock@withrevert(account, index); + assert !lastReverted; + + assert clockAfter == clockBefore; + assert valueAfter != valueBefore => clockBefore == clock(e); +} + +rule totalCheckpointsImmutable(env e, method f) + filtered { f -> !f.isView } +{ + uint32 index; + + require index < numCheckpointsTotalSupply(); + uint224 valueBefore = ckptVotesTotalSupply(index); + uint32 clockBefore = ckptFromBlockTotalSupply(index); + + calldataarg args; f(e, args); + + uint224 valueAfter = ckptVotesTotalSupply@withrevert(index); + assert !lastReverted; + uint32 clockAfter = ckptFromBlockTotalSupply@withrevert(index); + assert !lastReverted; + + assert clockAfter == clockBefore; + assert valueAfter != valueBefore => clockBefore == clock(e); +} + + + + + + + + + + + + + + + + + + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rules: what function can lead to state changes │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule changes(env e, method f) + filtered { f -> !f.isView } +{ + address account; + calldataarg args; + + uint32 ckptsBefore = numCheckpoints(account); + uint256 votesBefore = getVotes(account); + address delegatesBefore = delegates(account); + + f(e, args); + + uint32 ckptsAfter = numCheckpoints(account); + uint256 votesAfter = getVotes(account); + address delegatesAfter = delegates(account); + + assert ckptsAfter != ckptsBefore => ( + ckptsAfter == ckptsBefore + 1 && + ckptFromBlock(account, ckptsAfter - 1) == clock(e) && + ( + f.selector == mint(address,uint256).selector || + f.selector == burn(address,uint256).selector || + f.selector == transfer(address,uint256).selector || + f.selector == transferFrom(address,address,uint256).selector || + f.selector == delegate(address).selector || + f.selector == delegateBySig(address,uint256,uint256,uint8,bytes32,bytes32).selector + ) + ); + + assert votesAfter != votesBefore => ( + f.selector == mint(address,uint256).selector || + f.selector == burn(address,uint256).selector || + f.selector == transfer(address,uint256).selector || + f.selector == transferFrom(address,address,uint256).selector || + f.selector == delegate(address).selector || + f.selector == delegateBySig(address,uint256,uint256,uint8,bytes32,bytes32).selector + ); + + assert delegatesAfter != delegatesBefore => ( + f.selector == delegate(address).selector || + f.selector == delegateBySig(address,uint256,uint256,uint8,bytes32,bytes32).selector + ); +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rules: mint updates votes │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +/* WIP +rule mint(env e) { + requireInvariant totalSupplyIsSumOfBalances(); + requireInvariant totalSupplyTracked(); + requireInvariant totalSupplyLatest(); + require nonpayable(e); + + address to; + address toDelegate = delegates(to); + address other; + uint256 amount; + + // cache state + uint256 totalSupplyBefore = totalSupply(); + uint256 votesBefore = getVotes(toDelegate); + uint32 ckptsBefore = numCheckpoints(toDelegate); + mathint clockBefore = ckptsBefore == 0 ? -1 : numCheckpoints(toDelegate); + uint256 otherVotesBefore = getVotes(other); + uint256 otherCkptsBefore = numCheckpoints(other); + + // run transaction + mint@withrevert(e, to, amount); + bool success = !lastReverted; + + uint256 votesAfter = getVotes(toDelegate); + uint32 ckptsAfter = numCheckpoints(toDelegate); + mathint clockAfter = ckptsAfter == 0 ? -1 : numCheckpoints(toDelegate); + uint256 otherVotesAfter = getVotes(other); + uint256 otherCkptsAfter = numCheckpoints(other); + + // liveness + assert success <=> (to != 0 || totalSupplyBefore + amount <= max_uint256); + + // effects + assert ( + success && + toDelegate != 0 + ) => ( + votesAfter == votesBefore + amount && + ckptsAfter == ckptsBefore + to_mathint(clockBefore == clockAfter ? 0 : 1) && + clockAfter == clock(e) + ); + + // no side effects + assert otherVotesAfter != otherVotesBefore => other == toDelegate; + assert otherCkptsAfter != otherCkptsBefore => other == toDelegate; +} +*/ +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rules: burn updates votes │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +/* WIP +rule burn(env e) { + requireInvariant totalSupplyIsSumOfBalances(); + requireInvariant totalSupplyTracked(); + requireInvariant totalSupplyLatest(); + require nonpayable(e); + + address from; + address fromDelegate = delegates(from); + address other; + uint256 amount; + + // cache state + uint256 fromBalanceBefore = balanceOf(from); + uint256 votesBefore = getVotes(fromDelegate); + uint32 ckptsBefore = numCheckpoints(fromDelegate); + mathint clockBefore = ckptsBefore == 0 ? -1 : numCheckpoints(fromDelegate); + uint256 otherVotesBefore = getVotes(other); + uint256 otherCkptsBefore = numCheckpoints(other); + + // run transaction + burn@withrevert(e, from, amount); + bool success = !lastReverted; + + uint256 votesAfter = getVotes(fromDelegate); + uint32 ckptsAfter = numCheckpoints(fromDelegate); + mathint clockAfter = ckptsAfter == 0 ? -1 : numCheckpoints(fromDelegate); + uint256 otherVotesAfter = getVotes(other); + uint256 otherCkptsAfter = numCheckpoints(other); + + // liveness + assert success <=> (from != 0 || amount <= fromBalanceBefore); + + // effects + assert ( + success && + fromDelegate != 0 + ) => ( + votesAfter == votesBefore + amount && + ckptsAfter == ckptsBefore + to_mathint(clockBefore == clockAfter ? 0 : 1) && + clockAfter == clock(e) + ); + + // no side effects + assert otherVotesAfter != otherVotesBefore => other == fromDelegate; + assert otherCkptsAfter != otherCkptsBefore => other == fromDelegate; +} +*/ \ No newline at end of file From a40bb5a123f5f9dee53dcc3e41dfef8caf64c29d Mon Sep 17 00:00:00 2001 From: Hadrien Croubois Date: Tue, 2 May 2023 18:06:04 +0200 Subject: [PATCH 9/9] wip --- certora/specs/ERC20Votes.spec | 96 ++++++++++++++++++++++++++--------- 1 file changed, 72 insertions(+), 24 deletions(-) diff --git a/certora/specs/ERC20Votes.spec b/certora/specs/ERC20Votes.spec index 4c2fe6f2b..1b25f2b21 100644 --- a/certora/specs/ERC20Votes.spec +++ b/certora/specs/ERC20Votes.spec @@ -2,7 +2,6 @@ import "helpers.spec" import "methods/IERC20.spec" import "methods/IERC5805.spec" import "methods/IERC6372.spec" -import "ERC20.spec" methods { numCheckpoints(address) returns (uint32) envfree @@ -14,8 +13,6 @@ methods { maxSupply() returns (uint224) envfree } -use invariant totalSupplyIsSumOfBalances - /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ Helpers │ @@ -28,6 +25,11 @@ definition max_uint224() returns uint224 = 0xffffffffffffffffffffffffffff; │ Ghost & hooks: total delegated │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ +// copied from ERC20.spec (can't be imported because of hook conflicts) +ghost sumOfBalances() returns uint256 { + init_state axiom sumOfBalances() == 0; +} + ghost mapping(address => uint256) balanceOf { init_state axiom forall address a. balanceOf[a] == 0; } @@ -41,6 +43,9 @@ ghost mapping(address => uint256) getVotes { } hook Sstore _balances[KEY address account] uint256 newAmount (uint256 oldAmount) STORAGE { + // copied from ERC20.spec (can't be imported because of hook conflicts) + havoc sumOfBalances assuming sumOfBalances@new() == sumOfBalances@old() + newAmount - oldAmount; + balanceOf[account] = newAmount; getVotes[delegates[account]] = getVotes[delegates[account]] + newAmount - oldAmount; } @@ -51,6 +56,18 @@ hook Sstore _delegates[KEY address account] address newDelegate (address oldDele getVotes[newDelegate] = getVotes[newDelegate] + balanceOf[account]; } +// all votes (total supply) minus the votes balances delegated to 0 +definition totalVotes() returns uint256 = sumOfBalances() - getVotes[0]; + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Invariant: copied from ERC20.spec (can't be imported because of hook conflicts) │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +invariant totalSupplyIsSumOfBalances() + totalSupply() == sumOfBalances() && + totalSupply() <= max_uint256 + /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ Invariant: clock │ @@ -59,15 +76,64 @@ hook Sstore _delegates[KEY address account] address newDelegate (address oldDele invariant clockMode(env e) clock(e) == e.block.number || clock(e) == e.block.timestamp +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Invariant: zero address has no delegate, no votes and no checkpoints │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +invariant zeroConsistency() + delegates(0) == 0 && + getVotes(0) == 0 && + numCheckpoints(0) == 0 + { + preserved with (env e) { + // we assume address 0 cannot perform any call + require e.msg.sender != 0; + } + } + +// WIP +invariant delegateHasCheckpoint(address a) + (balanceOf(a) > 0 && delegates(a) != 0) => numCheckpoints(delegates(a)) > 0 + { + preserved delegate(address delegatee) with (env e) { + require numCheckpoints(delegatee) < max_uint256; + } + preserved delegateBySig(address delegatee, uint256 nonce, uint256 expiry, uint8 v, bytes32 r, bytes32 s) with (env e) { + require numCheckpoints(delegatee) < max_uint256; + } + } + /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ Invariant: hook correctly track latest checkpoint │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -invariant delegationConsistency(address a) +invariant balanceAndDelegationConsistency(address a) balanceOf(a) == balanceOf[a] && - delegates(a) == delegates[a] && - getVotes(a) == (a == 0 ? 0 : getVotes[a]) + delegates(a) == delegates[a] + +// WIP +invariant votesConsistency(address a) + a != 0 => getVotes(a) == getVotes[a] + +// WIP +invariant voteBiggerThanDelegatedBalances(address a) + getVotes(delegates(a)) >= balanceOf(a) + { + preserved { + requireInvariant zeroConsistency(); + } + } + +// WIP +invariant userVotesLessTotalVotes(address a) + numCheckpoints(a) > 0 => getVotes(a) <= totalVotes() + { + preserved { + requireInvariant totalSupplyIsSumOfBalances; + } + } /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ @@ -122,24 +188,6 @@ invariant totalCheckpointClockIncreassing() } } -/// For some reason "sumOfBalances" is not tracking correctly ... -/// ... and we get counter example where totalSupply is more than the sum of involved balances -// invariant userVotesLessTotalVotes(address a) -// numCheckpoints(a) > 0 => getVotes(a) <= totalVotes() -// { -// preserved { -// requireInvariant totalSupplyIsSumOfBalances; -// } -// } - -/* -┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Invariant: Don't track votes delegated to address 0 │ -└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ -*/ -invariant addressZeroNoCheckpoints() - numCheckpoints(0) == 0 - /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ Invariant: Don't track votes delegated to address 0 │