Merge branch 'fv/ERC20Votes' into chore/certora-CVL2

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)
++        // }
+     }
+ }

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();
+    }
+}

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);
+    }
+}

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",

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;
+}
+*/

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;
+}

certora/specs/methods/IERC6372.spec

@@ -0,0 +1,4 @@
+methods {
+    function clock()      external returns (uint48);
+    function CLOCK_MODE() external returns (string);
+}