some erc20Votes specs working

certora/specs/ERC20Votes.spec

@@ -19,55 +19,39 @@ use invariant totalSupplyIsSumOfBalances
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 definition max_uint224() returns uint224 = 0xffffffffffffffffffffffffffff;
-definition lastCheckpoint(address a) returns uint32 = to_uint32(numCheckpoints(a) - 1);
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
 │ Ghost & hooks                                                                                                       │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
-
-
-/*
 ghost totalVotes() returns uint224 {
     init_state axiom totalVotes() == 0;
 }
 
-ghost mapping(address => uint256) userVotes {
+ghost mapping(address => uint224) userVotes {
     init_state axiom forall address a. userVotes[a] == 0;
 }
 
-ghost mapping(address => uint32) userLast {
-    init_state axiom forall address a. userLast[a] == 0;
-}
-
 ghost mapping(address => uint32) userClock {
     init_state axiom forall address a. userClock[a] == 0;
 }
 
+ghost mapping(address => uint32) userCkpts {
+    init_state axiom forall address a. userCkpts[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];
 
     userVotes[account] = newVotes;
-    userLast[account] = index;
+    userCkpts[account] = index;
 }
 
 hook Sstore currentContract._checkpoints[KEY address account][INDEX uint32 index].fromBlock uint32 newTimepoint (uint32 oldTimepoint) STORAGE {
     userClock[account] = newTimepoint;
+    userCkpts[account] = index;
 }
-*/
-
-
-
-
-
-
-
-
-
-
-
-
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
@@ -77,13 +61,26 @@ hook Sstore currentContract._checkpoints[KEY address account][INDEX uint32 index
 invariant clockMode(env e)
     clock(e) == e.block.number || clock(e) == e.block.timestamp
 
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: hook correctly track lastest checkpoint                                                                  │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant hooksAreCorrect(address a)
+    numCheckpoints(a) > 0 => (
+        userVotes[a] == getVotes(a) &&
+        userVotes[a] == ckptVotes(a, numCheckpoints(a) - 1) &&
+        userClock[a] == ckptFromBlock(a, numCheckpoints(a) - 1) &&
+        userCkpts[a] == numCheckpoints(a) - 1
+    )
 
-
+/*
-
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-
+│ Invariant: checkpoint is not in the future                                                                          │
-
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
 invariant userClockInThePast(env e, address a)
-    numCheckpoints(a) > 0 => ckptFromBlock(lastCheckpoint(a)) <= clock(e)
+    numCheckpoints(a) > 0 => ckptFromBlock(a, numCheckpoints(a) - 1) <= clock(e)
     {
         preserved with (env e2) {
             require clock(e2) <= clock(e);
@@ -91,69 +88,39 @@ invariant userClockInThePast(env e, address a)
     }
 
 /*
-invariant hooksAreCorrect(env e, address a)
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-    numCheckpoints(a) > 0 => (
+│ Invariant: checkpoint clock is strictly increassing (implies no duplicate)                                          │
-        userLast(a)  == ckptFromBlock(lastCheckpoint(a)) &&
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-        userVotes(a) == ckptVotes(lastCheckpoint(a))
-    )
 */
-
+invariant checkpointClockIncreassing(address a)
-
+    numCheckpoints(a) > 1 => ckptFromBlock(a, numCheckpoints(a) - 2) < ckptFromBlock(a, numCheckpoints(a) - 1)
-
-
-
-
-
-
-/*
-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()
-    )
-*/
-
-
-
-
-
-
-
-
-/*
-invariant noDuplicate(address a)
-    !lastUserDuplicate(a)
-
-// passes
-invariant userVotesOverflow()
-    forall address a. lastUserVotes(a) <= max_uint256
-
-invariant userVotes(env e)
-    forall address a. userCkptNumber(a) > 0 => lastUserVotes(a) == getVotes(e, a)
     {
-        preserved {
+        preserved with (env e) {
-            requireInvariant totalSupplyIsSumOfBalances;
+            requireInvariant userClockInThePast(e, a);
         }
     }
 
-invariant userVotesLessTotalVotes()
-    forall address a. userCkptNumber(a) > 0 => lastUserVotes(a) <= totalVotes()
-    {
-        preserved {
-            requireInvariant totalSupplyIsSumOfBalances;
-        }
-    }
 
-// passes
+
-invariant totalVotesLessTotalSupply()
+
-    totalVotes() <= totalSupply()
+
-    {
+
-        preserved {
+/// For some reason "sumOfBalances" is not tracking correctly ...
-            requireInvariant totalSupplyIsSumOfBalances;
+/// ... and we get counter example where totalSupply is more than the sum of involved balances
-        }
+// invariant totalVotesLessTotalSupply()
-    }
+//     totalVotes() <= totalSupply()
-*/
+//     {
+//         preserved {
+//             requireInvariant totalSupplyIsSumOfBalances;
+//         }
+//     }
+
+/// For some reason "sumOfBalances" is not tracking correctly ...
+/// ... and we get counter example where totalSupply is more than the sum of involved balances
+// invariant userVotesLessTotalVotes(address a)
+//     numCheckpoints(a) > 0 => getVotes(a) <= totalVotes()
+//     {
+//         preserved {
+//             requireInvariant totalSupplyIsSumOfBalances;
+//         }
+//     }

certora/specs/methods/IERC5805.spec

@@ -1,6 +1,6 @@
 methods {
     // view
-    getVotes(address)              returns (uint256)
+    getVotes(address)              returns (uint256) envfree
     getPastVotes(address, uint256) returns (uint256)
     getPastTotalSupply(uint256)    returns (uint256)
     delegates(address)             returns (address) envfree