From d66a6f2443ea980ea283cc3d29dfbeebd4015312 Mon Sep 17 00:00:00 2001 From: Hadrien Croubois Date: Thu, 27 Apr 2023 14:16:17 +0200 Subject: [PATCH] wip --- ...oken_ERC20_extensions_ERC20Votes.sol.patch | 19 +++ certora/specs/ERC20Votes.spec | 113 ++++++++++-------- 2 files changed, 81 insertions(+), 51 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,93 +15,88 @@ 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; +} + +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; } -/* -┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ 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 - userVotes[account]; - havoc totalVotes assuming - totalVotes@new() == totalVotes@old() + newVotes - lastUserVotes(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; - - havoc userCkptNumber assuming - userCkptNumber@new(account) == index + 1; - - havoc lastUserDuplicate assuming - lastUserDuplicate@new(account) == (newTimepoint == lastUserTimepoint(account)); - + userClock[account] = newTimepoint; } +*/ -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)) ) +*/ @@ -110,6 +105,22 @@ invariant lastUserVotesAndTimepointConsistency(address 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() + ) +*/ + + + + +