diff --git a/certora/diff/utils_structs_Checkpoints.sol.patch b/certora/diff/utils_structs_Checkpoints.sol.patch new file mode 100644 index 000000000..96f6ee5a0 --- /dev/null +++ b/certora/diff/utils_structs_Checkpoints.sol.patch @@ -0,0 +1,33 @@ +--- utils/structs/Checkpoints.sol 2023-08-21 16:07:18.151395512 +0200 ++++ utils/structs/Checkpoints.sol 2023-08-25 10:43:19.822052443 +0200 +@@ -200,10 +200,11 @@ + Checkpoint224[] storage self, + uint256 pos + ) private pure returns (Checkpoint224 storage result) { +- assembly { +- mstore(0, self.slot) +- result.slot := add(keccak256(0, 0x20), pos) +- } ++ return self[pos]; // explicit (safe) for formal verification hooking ++ // assembly { ++ // mstore(0, self.slot) ++ // result.slot := add(keccak256(0, 0x20), pos) ++ // } + } + + struct Trace160 { +@@ -387,9 +388,10 @@ + Checkpoint160[] storage self, + uint256 pos + ) private pure returns (Checkpoint160 storage result) { +- assembly { +- mstore(0, self.slot) +- result.slot := add(keccak256(0, 0x20), pos) +- } ++ return self[pos]; // explicit (safe) for formal verification hooking ++ // assembly { ++ // mstore(0, self.slot) ++ // result.slot := add(keccak256(0, 0x20), pos) ++ // } + } + } diff --git a/certora/harnesses/ERC20VotesHarness.sol b/certora/harnesses/ERC20VotesHarness.sol new file mode 100644 index 000000000..a9f3c670f --- /dev/null +++ b/certora/harnesses/ERC20VotesHarness.sol @@ -0,0 +1,38 @@ +// 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) {} + + 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 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/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 3e5acb568..1933d45bb 100644 --- a/certora/specs.json +++ b/certora/specs.json @@ -44,6 +44,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/ERC20Votes.spec b/certora/specs/ERC20Votes.spec new file mode 100644 index 000000000..204a954bf --- /dev/null +++ b/certora/specs/ERC20Votes.spec @@ -0,0 +1,425 @@ +import "helpers/helpers.spec"; +import "methods/IERC20.spec"; +import "methods/IERC5805.spec"; +import "methods/IERC6372.spec"; + +methods { + function numCheckpoints(address) external returns (uint32) envfree; + function ckptFromBlock(address, uint32) external returns (uint32) envfree; + function ckptVotes(address, uint32) external returns (uint224) envfree; + function numCheckpointsTotalSupply() external returns (uint32) envfree; + function ckptFromBlockTotalSupply(uint32) external returns (uint32) envfree; + function ckptVotesTotalSupply(uint32) external returns (uint224) envfree; + function maxSupply() external returns (uint224) envfree; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Ghost & hooks: total delegated │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +// // copied from ERC20.spec (can't be imported because of hook conflicts) +// ghost mathint sumOfBalances { +// init_state axiom sumOfBalances == 0; +// } +// +// ghost mapping(address => uint256) balanceOf { +// init_state axiom forall address a. balanceOf[a] == 0; +// } +// +// ghost mapping(address => address) delegates { +// init_state axiom forall address a. delegates[a] == 0; +// } +// +// ghost mapping(address => uint256) getVotes { +// init_state axiom forall address a. getVotes[a] == 0; +// } +// +// 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; +// } +// +// 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]; +// } +// +// // 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 │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +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 balanceAndDelegationConsistency(address a) +// balanceOf(a) == balanceOf[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; +// } +// } + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ 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 checkpointInThePast(env e, address a) +// numCheckpoints(a) > 0 => ckptFromBlock(a, numCheckpoints(a) - 1) <= clock(e) +// { +// preserved with (env e2) { +// require clock(e2) <= clock(e); +// } +// } + +// 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) │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +// invariant checkpointClockIncreassing(address a) +// numCheckpoints(a) > 1 => ckptFromBlock(a, numCheckpoints(a) - 2) < ckptFromBlock(a, numCheckpoints(a) - 1) +// { +// preserved with (env e) { +// requireInvariant checkpointInThePast(e, a); +// } +// } + +// invariant totalCheckpointClockIncreassing() +// numCheckpointsTotalSupply() > 1 => ckptFromBlockTotalSupply(numCheckpointsTotalSupply() - 2) < ckptFromBlockTotalSupply(numCheckpointsTotalSupply() - 1) +// { +// preserved with (env e) { +// requireInvariant totalCheckpointInThePast(e); +// } +// } + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ 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 diff --git a/certora/specs/methods/IERC5805.spec b/certora/specs/methods/IERC5805.spec new file mode 100644 index 000000000..b180e1434 --- /dev/null +++ b/certora/specs/methods/IERC5805.spec @@ -0,0 +1,11 @@ +methods { + // view + function getVotes(address) external returns (uint256) envfree; + function getPastVotes(address, uint256) external returns (uint256); + function getPastTotalSupply(uint256) external returns (uint256); + function delegates(address) external returns (address) envfree; + + // external + function delegate(address) external; + function delegateBySig(address, uint256, uint256, uint8, bytes32, bytes32) external; +} diff --git a/certora/specs/methods/IERC6372.spec b/certora/specs/methods/IERC6372.spec new file mode 100644 index 000000000..496b37f55 --- /dev/null +++ b/certora/specs/methods/IERC6372.spec @@ -0,0 +1,4 @@ +methods { + function clock() external returns (uint48); + function CLOCK_MODE() external returns (string); +}