From 61fa061ecf805257c754baa8e02561b08f170188 Mon Sep 17 00:00:00 2001 From: Aleksander Kryukov Date: Tue, 8 Mar 2022 16:38:11 +0000 Subject: [PATCH] erc20votes pointers workaround and preset --- .../munged/governance/TimelockController.sol | 2 +- .../token/ERC20/extensions/ERC20Votes.sol | 49 ++++++++++++++++--- certora/scripts/sanity.sh | 28 +++++------ certora/scripts/verifyERC20Votes.sh | 8 +++ certora/scripts/verifyTimelock.sh | 7 +++ certora/specs/ERC20Votes.spec | 6 +++ certora/specs/TimelockController.spec | 36 ++++++++++++++ certora/specs/sanity.spec | 3 +- 8 files changed, 115 insertions(+), 24 deletions(-) create mode 100644 certora/scripts/verifyERC20Votes.sh create mode 100644 certora/scripts/verifyTimelock.sh create mode 100644 certora/specs/ERC20Votes.spec create mode 100644 certora/specs/TimelockController.spec diff --git a/certora/munged/governance/TimelockController.sol b/certora/munged/governance/TimelockController.sol index c375f0744..621ebd87b 100644 --- a/certora/munged/governance/TimelockController.sol +++ b/certora/munged/governance/TimelockController.sol @@ -353,4 +353,4 @@ contract TimelockController is AccessControl { emit MinDelayChange(_minDelay, newDelay); _minDelay = newDelay; } -} +} diff --git a/certora/munged/token/ERC20/extensions/ERC20Votes.sol b/certora/munged/token/ERC20/extensions/ERC20Votes.sol index c0e88bc19..be127239b 100644 --- a/certora/munged/token/ERC20/extensions/ERC20Votes.sol +++ b/certora/munged/token/ERC20/extensions/ERC20Votes.sol @@ -163,7 +163,7 @@ abstract contract ERC20Votes is IVotes, ERC20Permit { super._mint(account, amount); require(totalSupply() <= _maxSupply(), "ERC20Votes: total supply risks overflowing votes"); - _writeCheckpoint(_totalSupplyCheckpoints, _add, amount); + _writeCheckpointAdd(_totalSupplyCheckpoints, amount); // HARNESS: new version without pointer } /** @@ -172,7 +172,7 @@ abstract contract ERC20Votes is IVotes, ERC20Permit { function _burn(address account, uint256 amount) internal virtual override { super._burn(account, amount); - _writeCheckpoint(_totalSupplyCheckpoints, _subtract, amount); + _writeCheckpointSub(_totalSupplyCheckpoints, amount); // HARNESS: new version without pointer } /** @@ -187,7 +187,7 @@ abstract contract ERC20Votes is IVotes, ERC20Permit { ) internal virtual override { super._afterTokenTransfer(from, to, amount); - _moveVotingPower(delegates(from), delegates(to), amount); + _moveVotingPower(delegates(from), delegates(to), amount); } /** @@ -212,25 +212,25 @@ abstract contract ERC20Votes is IVotes, ERC20Permit { ) private { if (src != dst && amount > 0) { if (src != address(0)) { - (uint256 oldWeight, uint256 newWeight) = _writeCheckpoint(_checkpoints[src], _subtract, amount); + (uint256 oldWeight, uint256 newWeight) = _writeCheckpointSub(_checkpoints[src], amount); // HARNESS: new version without pointer emit DelegateVotesChanged(src, oldWeight, newWeight); } if (dst != address(0)) { - (uint256 oldWeight, uint256 newWeight) = _writeCheckpoint(_checkpoints[dst], _add, amount); + (uint256 oldWeight, uint256 newWeight) = _writeCheckpointAdd(_checkpoints[dst], amount); // HARNESS: new version without pointer emit DelegateVotesChanged(dst, oldWeight, newWeight); } } } - function _writeCheckpoint( + // HARNESS: split _writeCheckpoint() to two functions as a workaround for function pointers that cannot be managed by the tool + function _writeCheckpointAdd( Checkpoint[] storage ckpts, - function(uint256, uint256) view returns (uint256) op, uint256 delta ) private returns (uint256 oldWeight, uint256 newWeight) { uint256 pos = ckpts.length; oldWeight = pos == 0 ? 0 : ckpts[pos - 1].votes; - newWeight = op(oldWeight, delta); + newWeight = _add(oldWeight, delta); if (pos > 0 && ckpts[pos - 1].fromBlock == block.number) { ckpts[pos - 1].votes = SafeCast.toUint224(newWeight); @@ -239,6 +239,39 @@ abstract contract ERC20Votes is IVotes, ERC20Permit { } } + function _writeCheckpointSub( + Checkpoint[] storage ckpts, + uint256 delta + ) private returns (uint256 oldWeight, uint256 newWeight) { + uint256 pos = ckpts.length; + oldWeight = pos == 0 ? 0 : ckpts[pos - 1].votes; + newWeight = _subtract(oldWeight, delta); + + if (pos > 0 && ckpts[pos - 1].fromBlock == block.number) { + ckpts[pos - 1].votes = SafeCast.toUint224(newWeight); + } else { + ckpts.push(Checkpoint({fromBlock: SafeCast.toUint32(block.number), votes: SafeCast.toUint224(newWeight)})); + } + } + + // backup of original function + // + // function _writeCheckpoint( + // Checkpoint[] storage ckpts, + // function(uint256, uint256) view returns (uint256) op, + // uint256 delta + // ) private returns (uint256 oldWeight, uint256 newWeight) { + // uint256 pos = ckpts.length; + // oldWeight = pos == 0 ? 0 : ckpts[pos - 1].votes; + // newWeight = op(oldWeight, delta); + // + // if (pos > 0 && ckpts[pos - 1].fromBlock == block.number) { + // ckpts[pos - 1].votes = SafeCast.toUint224(newWeight); + // } else { + // ckpts.push(Checkpoint({fromBlock: SafeCast.toUint32(block.number), votes: SafeCast.toUint224(newWeight)})); + // } + // } + function _add(uint256 a, uint256 b) private pure returns (uint256) { return a + b; } diff --git a/certora/scripts/sanity.sh b/certora/scripts/sanity.sh index 84d76159e..afead788d 100644 --- a/certora/scripts/sanity.sh +++ b/certora/scripts/sanity.sh @@ -14,22 +14,22 @@ # done # TimelockController -# certoraRun \ -# certora/harnesses/TimelockControllerHarness.sol \ -# --verify TimelockControllerHarness:certora/specs/sanity.spec \ -# --solc solc8.2 \ -# --optimistic_loop \ -# --cloud \ -# --msg "sanity" - - -# Votes certoraRun \ - certora/harnesses/VotesHarness.sol \ - --verify VotesHarness:certora/specs/sanity.spec \ + certora/harnesses/TimelockControllerHarness.sol \ + --verify TimelockControllerHarness:certora/specs/sanity.spec \ --solc solc8.2 \ --optimistic_loop \ --cloud \ - --settings -strictDecompiler=false,-assumeUnwindCond \ - --msg "sanityVotes" + --msg "sanity and keccak check" + + +# Votes +# certoraRun \ +# certora/harnesses/VotesHarness.sol \ +# --verify VotesHarness:certora/specs/sanity.spec \ +# --solc solc8.2 \ +# --optimistic_loop \ +# --cloud \ +# --settings -strictDecompiler=false,-assumeUnwindCond \ +# --msg "sanityVotes" diff --git a/certora/scripts/verifyERC20Votes.sh b/certora/scripts/verifyERC20Votes.sh new file mode 100644 index 000000000..5d70e1f25 --- /dev/null +++ b/certora/scripts/verifyERC20Votes.sh @@ -0,0 +1,8 @@ +certoraRun \ + certora/harnesses/ERC20VotesHarness.sol \ + --verify ERC20VotesHarness:certora/specs/ERC20Votes.spec \ + --solc solc8.2 \ + --optimistic_loop \ + --cloud \ + --settings -strictDecompiler=false,-assumeUnwindCond \ + --msg "sanityVotes" diff --git a/certora/scripts/verifyTimelock.sh b/certora/scripts/verifyTimelock.sh new file mode 100644 index 000000000..e8ac5548b --- /dev/null +++ b/certora/scripts/verifyTimelock.sh @@ -0,0 +1,7 @@ +certoraRun \ + certora/harnesses/TimelockControllerHarness.sol \ + --verify TimelockControllerHarness:certora/specs/TimelockController.spec \ + --solc solc8.2 \ + --optimistic_loop \ + --cloud \ + --msg "sanity" \ No newline at end of file diff --git a/certora/specs/ERC20Votes.spec b/certora/specs/ERC20Votes.spec new file mode 100644 index 000000000..b08c6cf4e --- /dev/null +++ b/certora/specs/ERC20Votes.spec @@ -0,0 +1,6 @@ +rule sanity(method f) { + env e; + calldataarg arg; + f(e, arg); + assert false; +} \ No newline at end of file diff --git a/certora/specs/TimelockController.spec b/certora/specs/TimelockController.spec new file mode 100644 index 000000000..9c0b99c5f --- /dev/null +++ b/certora/specs/TimelockController.spec @@ -0,0 +1,36 @@ +methods { + // hashOperation(address target, uint256 value, bytes data, bytes32 predecessor, bytes32 salt) returns(bytes32) => uniqueHashGhost(target, value, data, predecessor, salt) +} + +// ghost uniqueHashGhost(address, uint256, bytes, bytes32, bytes32) returns bytes32; +// +// Assuming the hash is deterministic, and correlates the trio properly +// function hashUniquness(address target1, uint256 value1, bytes data1, bytes32 predecessor1, bytes32 salt1, +// address target2, uint256 value2, bytes data2, bytes32 predecessor2, bytes32 salt2){ +// require ((target1 != target2) || (value1 != value2) || (data1 != data2) || (predecessor1 != predecessor2) || (salt1 != salt2)) <=> +// (uniqueHashGhost(target1, value1, data1, predecessor1, salt1) != uniqueHashGhost(target2, value2, data2, predecessor2, salt2)); +// } +// +// +// rule keccakCheck(method f, env e){ +// address target; +// uint256 value; +// bytes data; +// bytes32 predecessor; +// bytes32 salt; +// +// hashUniquness(target, value, data, predecessor, salt, +// target, value, data, predecessor, salt); +// +// bytes32 a = hashOperation(e, target, value, data, predecessor, salt); +// bytes32 b = hashOperation(e, target, value, data, predecessor, salt); +// +// assert a == b, "hashes are different"; +// } + +rule sanity(method f) { + env e; + calldataarg arg; + f(e, arg); + assert false; +} \ No newline at end of file diff --git a/certora/specs/sanity.spec b/certora/specs/sanity.spec index e08f68845..bd184841a 100644 --- a/certora/specs/sanity.spec +++ b/certora/specs/sanity.spec @@ -5,7 +5,8 @@ How it works: - If there is a non-reverting execution path, we reach the false assertion, and the sanity fails. - If all execution paths are reverting, we never call the assertion, and the method will pass this rule vacuously. */ - + + rule sanity(method f) { env e; calldataarg arg;