wip

certora/diff/token_ERC20_extensions_ERC20Votes.sol.patch

@@ -0,0 +1,19 @@
+--- token/ERC20/extensions/ERC20Votes.sol	2023-04-27 13:16:53.923627178 +0200
++++ token/ERC20/extensions/ERC20Votes.sol	2023-04-27 13:27:00.856088231 +0200
+@@ -281,10 +281,11 @@
+     /**
+      * @dev Access an element of the array without performing bounds check. The position is assumed to be within bounds.
+      */
+-    function _unsafeAccess(Checkpoint[] storage ckpts, uint256 pos) private pure returns (Checkpoint storage result) {
+-        assembly {
+-            mstore(0, ckpts.slot)
+-            result.slot := add(keccak256(0, 0x20), pos)
+-        }
++    function _unsafeAccess(Checkpoint[] storage ckpts, uint256 pos) private view returns (Checkpoint storage result) {
++        return ckpts[pos]; // explicit (safe) for formal verification hooking
++        // assembly {
++        //     mstore(0, ckpts.slot)
++        //     result.slot := add(keccak256(0, 0x20), pos)
++        // }
+     }
+ }

certora/specs/ERC20Votes.spec

@@ -15,97 +15,108 @@ use invariant totalSupplyIsSumOfBalances
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Ghost: user (current) voting weight                                                                                 │
+│ Helpers                                                                                                             │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
-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;
+definition max_uint224() returns uint224 = 0xffffffffffffffffffffffffffff;
+definition lastCheckpoint(address a) returns uint32 = to_uint32(numCheckpoints(a) - 1);
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Ghost: total voting weight                                                                                          │
+│ Ghost & hooks                                                                                                       │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
+
+
+/*
 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;
+ghost mapping(address => uint256) userVotes {
+    init_state axiom forall address a. userVotes[a] == 0;
 }
 
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Hook                                                                                                                │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-hook Sstore currentContract._checkpoints[KEY address account][INDEX uint32 index].votes uint224 newVotes (uint224 oldVotes) STORAGE {
-    havoc lastUserVotes assuming
-        lastUserVotes@new(account) == newVotes;
+ghost mapping(address => uint32) userLast {
+    init_state axiom forall address a. userLast[a] == 0;
+}
 
-    havoc totalVotes assuming
-        totalVotes@new() == totalVotes@old() + newVotes - lastUserVotes(account);
+ghost mapping(address => uint32) userClock {
+    init_state axiom forall address a. userClock[a] == 0;
+}
+
+hook Sstore currentContract._checkpoints[KEY address account][INDEX uint32 index].votes uint224 newVotes (uint224 oldVotes) STORAGE {
+    havoc totalVotes assuming totalVotes@new() == totalVotes@old() + newVotes - userVotes[account];
 
-    havoc lastUserIndex assuming
-        lastUserIndex@new(account) == index;
+    userVotes[account] = newVotes;
+    userLast[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;
+    userClock[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: clock                                                                                                    │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
 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)
+
+
+
+invariant userClockInThePast(env e, address a)
+    numCheckpoints(a) > 0 => ckptFromBlock(lastCheckpoint(a)) <= clock(e)
+    {
+        preserved with (env e2) {
+            require clock(e2) <= clock(e);
+        }
+    }
+
+/*
+invariant hooksAreCorrect(env e, 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()
+        userLast(a)  == ckptFromBlock(lastCheckpoint(a)) &&
+        userVotes(a) == ckptVotes(lastCheckpoint(a))
     )
+*/
+
+
+
+
 
 
 
 
+/*
+invariant userVotesAndClockConsistency(address a)
+    numCheckpoints(a) > 0 => (
+        userLast(a)  == numCheckpoints(a) - 1              &&
+        userLast(a)  <= max_uint32                         &&
+        userVotes(a) == ckptVotes(a, lastUserIndex(a))     &&
+        userVotes(a) <= max_uint224()                      &&
+        userClock(a) == ckptFromBlock(a, lastUserIndex(a)) &&
+        userClock(a) <= max_uint224()
+    )
+*/
+