From 2d6a89f09316211dbe6359d3c45810dc8324ccd7 Mon Sep 17 00:00:00 2001 From: Hadrien Croubois Date: Thu, 9 Mar 2023 13:16:35 +0100 Subject: [PATCH] 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