diff --git a/certora/diff/governance_utils_Votes.sol.patch b/certora/diff/governance_utils_Votes.sol.patch new file mode 100644 index 000000000..553302d06 --- /dev/null +++ b/certora/diff/governance_utils_Votes.sol.patch @@ -0,0 +1,26 @@ +--- governance/utils/Votes.sol 2023-08-21 16:07:18.144728664 +0200 ++++ governance/utils/Votes.sol 2023-08-25 10:52:12.904396821 +0200 +@@ -217,6 +217,10 @@ + return SafeCast.toUint32(_delegateCheckpoints[account].length()); + } + ++ function _numCheckpointsTotalSupply() internal view virtual returns (uint32) { ++ return SafeCast.toUint32(_totalCheckpoints[account].length()); ++ } ++ + /** + * @dev Get the `pos`-th checkpoint for `account`. + */ +@@ -227,6 +231,12 @@ + return _delegateCheckpoints[account].at(pos); + } + ++ function _checkpointsTotalSupply( ++ uint32 pos ++ ) internal view virtual returns (Checkpoints.Checkpoint224 memory) { ++ return _totalCheckpoints.at(pos); ++ } ++ + function _push( + Checkpoints.Trace224 storage store, + function(uint224, uint224) view returns (uint224) op, diff --git a/certora/diff/utils_structs_Checkpoints.sol.patch b/certora/diff/utils_structs_Checkpoints.sol.patch index 96f6ee5a0..52531359c 100644 --- a/certora/diff/utils_structs_Checkpoints.sol.patch +++ b/certora/diff/utils_structs_Checkpoints.sol.patch @@ -1,13 +1,15 @@ --- 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 @@ ++++ utils/structs/Checkpoints.sol 2023-08-25 10:51:17.586593500 +0200 +@@ -199,11 +199,12 @@ + function _unsafeAccess( Checkpoint224[] storage self, uint256 pos - ) private pure returns (Checkpoint224 storage result) { +- ) private pure returns (Checkpoint224 storage result) { - assembly { - mstore(0, self.slot) - result.slot := add(keccak256(0, 0x20), pos) - } ++ ) private view returns (Checkpoint224 storage result) { + return self[pos]; // explicit (safe) for formal verification hooking + // assembly { + // mstore(0, self.slot) @@ -16,14 +18,16 @@ } struct Trace160 { -@@ -387,9 +388,10 @@ +@@ -386,10 +387,11 @@ + function _unsafeAccess( Checkpoint160[] storage self, uint256 pos - ) private pure returns (Checkpoint160 storage result) { +- ) private pure returns (Checkpoint160 storage result) { - assembly { - mstore(0, self.slot) - result.slot := add(keccak256(0, 0x20), pos) - } ++ ) private view returns (Checkpoint160 storage result) { + return self[pos]; // explicit (safe) for formal verification hooking + // assembly { + // mstore(0, self.slot) diff --git a/certora/harnesses/ERC20VotesHarness.sol b/certora/harnesses/ERC20VotesHarness.sol index a9f3c670f..12ecfeb74 100644 --- a/certora/harnesses/ERC20VotesHarness.sol +++ b/certora/harnesses/ERC20VotesHarness.sol @@ -2,10 +2,11 @@ pragma solidity ^0.8.0; -import "../patched/token/ERC20/extensions/ERC20Votes.sol"; +import {ERC20Votes, ERC20} from "../patched/token/ERC20/extensions/ERC20Votes.sol"; +import {EIP712} from "../patched/utils/cryptography/EIP712.sol"; contract ERC20VotesHarness is ERC20Votes { - constructor(string memory name, string memory symbol) ERC20(name, symbol) {} + constructor(string memory name, string memory symbol) ERC20(name, symbol) EIP712(name, "1") {} function mint(address account, uint256 amount) external { _mint(account, amount); @@ -16,20 +17,24 @@ contract ERC20VotesHarness is ERC20Votes { } // inspection - function ckptFromBlock(address account, uint32 pos) public view returns (uint32) { - return checkpoints(account, pos).fromBlock; + function ckptClock(address account, uint32 pos) public view returns (uint32) { + return checkpoints(account, pos)._key; } function ckptVotes(address account, uint32 pos) public view returns (uint224) { - return checkpoints(account, pos).votes; + return checkpoints(account, pos)._value; } - function ckptFromBlockTotalSupply(uint32 pos) public view returns (uint32) { - return checkpointsTotalSupply(pos).fromBlock; + function numCheckpointsTotalSupply() public view returns (uint32) { + return _numCheckpointsTotalSupply(); + } + + function ckptClockTotalSupply(uint32 pos) public view returns (uint32) { + return _checkpointsTotalSupply(pos)._key; } function ckptVotesTotalSupply(uint32 pos) public view returns (uint224) { - return checkpointsTotalSupply(pos).votes; + return _checkpointsTotalSupply(pos)._value; } function maxSupply() public view returns (uint224) { diff --git a/certora/run.js b/certora/run.js index 68f34aab2..ad25c2549 100755 --- a/certora/run.js +++ b/certora/run.js @@ -64,7 +64,7 @@ if (process.exitCode) { } for (const { spec, contract, files, options = [] } of specs) { - limit(runCertora, spec, contract, files, [...options.flatMap(opt => opt.split(' ')), ...argv.options]); + limit(runCertora, spec, contract, files, [...options, ...argv.options].flatMap(opt => opt.split(' '))); } // Run certora, aggregate the output and print it at the end diff --git a/certora/specs/ERC20Votes.spec b/certora/specs/ERC20Votes.spec index 204a954bf..20afa1bcb 100644 --- a/certora/specs/ERC20Votes.spec +++ b/certora/specs/ERC20Votes.spec @@ -4,99 +4,83 @@ 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; + function numCheckpoints(address) external returns (uint32) envfree; + function ckptClock(address, uint32) external returns (uint32) envfree; + function ckptVotes(address, uint32) external returns (uint224) envfree; + function numCheckpointsTotalSupply() external returns (uint32) envfree; + function ckptClockTotalSupply(uint32) external returns (uint32) envfree; + function ckptVotesTotalSupply(uint32) external returns (uint224) envfree; + function maxSupply() external returns (uint224) envfree; } /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Ghost & hooks: total delegated │ +│ Invariant: clock │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -// // 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]; +function clockSanity(env e) returns bool { + return clock(e) <= max_uint32; +} + +invariant clockMode(env e) + assert_uint256(clock(e)) == e.block.number || assert_uint256(clock(e)) == e.block.timestamp; /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Invariant: copied from ERC20.spec (can't be imported because of hook conflicts) │ +│ Ghost & hooks: total delegated │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -// invariant totalSupplyIsSumOfBalances() -// totalSupply() == sumOfBalances() && -// totalSupply() <= max_uint256 - +// copied from ERC20.spec (can't be imported because of hook conflicts) +ghost mathint sumOfBalances { + init_state axiom sumOfBalances == 0; +} +ghost mapping(address => mathint) balance { + init_state axiom forall address a. balance[a] == 0; +} +ghost mapping(address => address) delegate { + init_state axiom forall address a. delegate[a] == 0; +} +ghost mapping(address => mathint) votes { + init_state axiom forall address a. votes[a] == 0; +} +hook Sload uint256 balance _balances[KEY address addr] STORAGE { + require sumOfBalances >= to_mathint(balance); +} +hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) STORAGE { + balance[addr] = newValue; + sumOfBalances = sumOfBalances - oldValue + newValue; + votes[delegate[addr]] = votes[delegate[addr]] + newValue - oldValue; +} +hook Sstore _delegatee[KEY address addr] address newDelegate (address oldDelegate) STORAGE { + delegate[addr] = newDelegate; + votes[oldDelegate] = votes[oldDelegate] - balance[addr]; + votes[newDelegate] = votes[newDelegate] + balance[addr]; +} +// all votes (total supply) minus the votes balances delegated to 0 +definition totalVotes() returns mathint = sumOfBalances - votes[0]; /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Invariant: clock │ +│ Invariant: copied from ERC20.spec (can't be imported because of hook conflicts) │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -invariant clockMode(env e) - clock(e) == e.block.number || clock(e) == e.block.timestamp; - - - - - - - - - - - - - - +invariant totalSupplyIsSumOfBalances() + to_mathint(totalSupply()) == sumOfBalances; /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ Invariant: zero address has no delegate, no votes and no checkpoints │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -invariant zeroConsistency() +invariant zeroAddressConsistency() + balanceOf(0) == 0 && delegates(0) == 0 && getVotes(0) == 0 && numCheckpoints(0) == 0 @@ -107,216 +91,232 @@ invariant zeroConsistency() } } -// 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(); -// } -// } +// TODO: forall address a. +invariant balanceDelegateAndVoteConsistency(address a) + delegates(a) == delegate[a] && + to_mathint(balanceOf(a)) == balance[a] && + a != 0 => to_mathint(getVotes(a)) == votes[a]; + +// TODO: forall address a. +invariant voteBiggerThanDelegatedBalances(address a) + getVotes(delegates(a)) >= balanceOf(a) + { + preserved { + requireInvariant zeroAddressConsistency(); + } + } -// WIP -// invariant userVotesLessTotalVotes(address a) -// numCheckpoints(a) > 0 => getVotes(a) <= totalVotes() -// { -// preserved { -// requireInvariant totalSupplyIsSumOfBalances; -// } -// } +// TODO: forall address a. +invariant userVotesLessTotalVotes(address a) + votes[a] <= totalVotes() + { + preserved { + requireInvariant totalSupplyIsSumOfBalances; + } + } /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Invariant: totalSupply is checkpointed │ +│ Checkpoints: number, ordering and consistency with clock │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -invariant totalSupplyTracked() - totalSupply() > 0 => numCheckpointsTotalSupply() > 0; +// TODO: forall address a. +invariant checkpointInThePast(env e, address a) + forall uint32 i. + numCheckpoints(a) > i => to_mathint(ckptClock(a, i)) <= to_mathint(clock(e)) + { + preserved with (env e2) { + require clock(e2) <= clock(e); + } + } -invariant totalSupplyLatest() - numCheckpointsTotalSupply() > 0 => ckptVotesTotalSupply(numCheckpointsTotalSupply() - 1) == totalSupply(); +invariant totalCheckpointInThePast(env e) + forall uint32 i. + numCheckpointsTotalSupply() > i => to_mathint(ckptClockTotalSupply(i)) <= to_mathint(clock(e)) + { + preserved with (env e2) { + require clock(e2) <= clock(e); + } + } + +// TODO: forall address a. +invariant checkpointClockIncreassing(address a) + forall uint32 i. + forall uint32 j. + (i < j && j < numCheckpoints(a)) => ckptClock(a, i) < ckptClock(a, j) + { + preserved with (env e) { + requireInvariant checkpointInThePast(e, a); + } + } + +invariant totalCheckpointClockIncreassing() + forall uint32 i. + forall uint32 j. + (i < j && j < numCheckpointsTotalSupply()) => ckptClockTotalSupply(i) < ckptClockTotalSupply(j) + { + preserved with (env e) { + requireInvariant totalCheckpointInThePast(e); + } + } + +// TODO: forall address a. +invariant checkpointCountLowerThanClock(env e, address a) + numCheckpoints(a) <= assert_uint32(clock(e)) + { + preserved { + require clockSanity(e); + requireInvariant checkpointInThePast(e, a); + } + } + +invariant totalCheckpointCountLowerThanClock(env e) + numCheckpointsTotalSupply() <= assert_uint32(clock(e)) + { + preserved { + require clockSanity(e); + requireInvariant totalCheckpointInThePast(e); + } + } /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Invariant: checkpoint is not in the future │ +│ Invariant: totalSupply is checkpointed │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -// 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 totalSupplyTracked() + totalSupply() > 0 => numCheckpointsTotalSupply() > 0; -// invariant totalCheckpointInThePast(env e) -// numCheckpointsTotalSupply() > 0 => ckptFromBlockTotalSupply(numCheckpointsTotalSupply() - 1) <= clock(e) -// { -// preserved with (env e2) { -// require clock(e2) <= clock(e); -// } -// } +invariant totalSupplyLatest() + numCheckpointsTotalSupply() > 0 => totalSupply() == assert_uint256(ckptVotesTotalSupply(require_uint32(numCheckpointsTotalSupply() - 1))) + { + preserved { + requireInvariant totalSupplyTracked(); + } + } /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Invariant: checkpoint clock is strictly increassing (implies no duplicate) │ +│ Invariant: Delegate must have a checkpoint │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -// invariant checkpointClockIncreassing(address a) -// numCheckpoints(a) > 1 => ckptFromBlock(a, numCheckpoints(a) - 2) < ckptFromBlock(a, numCheckpoints(a) - 1) +// WIP +// invariant delegateHasCheckpoint(address a) +// (balanceOf(a) > 0 && delegates(a) != 0) => numCheckpoints(delegates(a)) > 0 // { -// preserved with (env e) { -// requireInvariant checkpointInThePast(e, a); +// preserved delegate(address delegatee) with (env e) { +// require numCheckpoints(delegatee) < max_uint256; // } -// } - -// invariant totalCheckpointClockIncreassing() -// numCheckpointsTotalSupply() > 1 => ckptFromBlockTotalSupply(numCheckpointsTotalSupply() - 2) < ckptFromBlockTotalSupply(numCheckpointsTotalSupply() - 1) -// { -// preserved with (env e) { -// requireInvariant totalCheckpointInThePast(e); +// preserved delegateBySig(address delegatee, uint256 nonce, uint256 expiry, uint8 v, bytes32 r, bytes32 s) with (env e) { +// require numCheckpoints(delegatee) < max_uint256; // } // } /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Invariant: Don't track votes delegated to address 0 │ +│ Invariant: Checkpoints are immutables │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -/* rule checkpointsImmutable(env e, method f) filtered { f -> !f.isView } { address account; uint32 index; - require index < numCheckpoints(account); + require clockSanity(e); + requireInvariant checkpointCountLowerThanClock(e, account); + uint224 valueBefore = ckptVotes(account, index); - uint32 clockBefore = ckptFromBlock(account, index); + uint32 clockBefore = ckptClock(account, index); calldataarg args; f(e, args); uint224 valueAfter = ckptVotes@withrevert(account, index); assert !lastReverted; - uint32 clockAfter = ckptFromBlock@withrevert(account, index); + uint32 clockAfter = ckptClock@withrevert(account, index); assert !lastReverted; assert clockAfter == clockBefore; - assert valueAfter != valueBefore => clockBefore == clock(e); + assert valueAfter != valueBefore => clockBefore == assert_uint32(clock(e)); } rule totalCheckpointsImmutable(env e, method f) filtered { f -> !f.isView } { - uint32 index; + uint32 index; + + require clockSanity(e); + requireInvariant totalCheckpointCountLowerThanClock(e); - require index < numCheckpointsTotalSupply(); uint224 valueBefore = ckptVotesTotalSupply(index); - uint32 clockBefore = ckptFromBlockTotalSupply(index); + uint32 clockBefore = ckptClockTotalSupply(index); calldataarg args; f(e, args); uint224 valueAfter = ckptVotesTotalSupply@withrevert(index); assert !lastReverted; - uint32 clockAfter = ckptFromBlockTotalSupply@withrevert(index); + uint32 clockAfter = ckptClockTotalSupply@withrevert(index); assert !lastReverted; assert clockAfter == clockBefore; - assert valueAfter != valueBefore => clockBefore == clock(e); + assert valueAfter != valueBefore => clockBefore == assert_uint32(clock(e)); } -*/ - - - - - - - - - - - - - - - - /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ Rules: what function can lead to state changes │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -/* rule changes(env e, method f) filtered { f -> !f.isView } { address account; - calldataarg args; + + require clockSanity(e); uint32 ckptsBefore = numCheckpoints(account); uint256 votesBefore = getVotes(account); address delegatesBefore = delegates(account); - f(e, args); + calldataarg args; 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) && + ckptsAfter == assert_uint32(ckptsBefore + 1) && + ckptClock(account, ckptsBefore) == assert_uint32(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 + f.selector == sig:mint(address,uint256).selector || + f.selector == sig:burn(address,uint256).selector || + f.selector == sig:transfer(address,uint256).selector || + f.selector == sig:transferFrom(address,address,uint256).selector || + f.selector == sig:delegate(address).selector || + f.selector == sig: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 + f.selector == sig:mint(address,uint256).selector || + f.selector == sig:burn(address,uint256).selector || + f.selector == sig:transfer(address,uint256).selector || + f.selector == sig:transferFrom(address,address,uint256).selector || + f.selector == sig:delegate(address).selector || + f.selector == sig: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 + f.selector == sig:delegate(address).selector || + f.selector == sig:delegateBySig(address,uint256,uint256,uint8,bytes32,bytes32).selector ); } -*/ + /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ Rules: mint updates votes │