typechecker error and skipped require bug

certora/harnesses/ERC20VotesHarness.sol

@@ -19,6 +19,10 @@ contract ERC20VotesHarness is ERC20Votes {
         _burn(account, amount);
     }
 
+    function unsafeNumCheckpoints(address account) public view returns (uint256) {
+        return _checkpoints[account].length;
+    }
+
     function delegateBySig(
         address delegatee,
         uint256 nonce,

certora/scripts/ERC20VotesRule.sh

@@ -19,4 +19,5 @@ certoraRun \
     --optimistic_loop \
     --rule ${rule} \
     --msg "${msg}" \
+    --staging "Eyal/SanityWithoutCallTrace" \
     # --rule_sanity \

certora/scripts/verifyERC20Votes.sh

@@ -19,4 +19,5 @@ certoraRun \
     --solc solc8.2 \
     --optimistic_loop \
     --loop_iter 4 \
+    --staging "Eyal/SanityWithoutCallTrace" \
     --msg "${msg}"

certora/specs/ERC20Votes.spec

@@ -19,6 +19,7 @@ methods {
     ckptVotes(address, uint32) returns (uint224) envfree
     mint(address, uint256)
     burn(address, uint256)
+    unsafeNumCheckpoints(address) returns (uint256) envfree
 
     // solidity generated getters
     _delegates(address) returns (address) envfree
@@ -32,13 +33,17 @@ ghost userVotes(address) returns uint224;
 
 // sums the total votes for all users
 ghost totalVotes() returns mathint {
+    init_state axiom totalVotes() == 0;
     axiom totalVotes() >= 0;
 }
 
+ghost lastIndex(address) returns uint32;
+
 // helper
 
-invariant totalVotes_gte_accounts(address a, address b)
-    totalVotes() >= getVotes(a) + getVotes(b)
+// blocked by tool error
+invariant totalVotes_gte_accounts()
+    forall address a. forall address b. a != b => totalVotes() >= getVotes(a) + getVotes(b)
 
 
 hook Sstore _checkpoints[KEY address account][INDEX uint32 index].votes uint224 newVotes (uint224 oldVotes) STORAGE {
@@ -47,6 +52,9 @@ hook Sstore _checkpoints[KEY address account][INDEX uint32 index].votes uint224
 
     havoc totalVotes assuming
         totalVotes@new() == totalVotes@old() + to_mathint(newVotes) - to_mathint(userVotes(account));
+
+    havoc lastIndex assuming
+        lastIndex@new(account) == index;
 }
 
 
@@ -57,12 +65,14 @@ ghost doubleFromBlock(address) returns bool {
 }
 
 
+
+
 hook Sstore _checkpoints[KEY address account][INDEX uint32 index].fromBlock uint32 newBlock (uint32 oldBlock) STORAGE {
     havoc lastFromBlock assuming
         lastFromBlock@new(account) == newBlock;
     
     havoc doubleFromBlock assuming 
-        doubleFromBlock@new(account) == (newBlock == oldBlock);
+        doubleFromBlock@new(account) == (newBlock == lastFromBlock(account));
 }
 
 rule sanity(method f) {
@@ -77,8 +87,13 @@ invariant sanity_invariant()
     totalSupply() >= 0
 
 // sum of user balances is >= total amount of delegated votes
+// blocked by tool error
 invariant votes_solvency()
     to_mathint(totalSupply()) >= totalVotes()
+{ preserved {
+    require forall address account. unsafeNumCheckpoints(account) < 4294967295;
+    requireInvariant totalVotes_gte_accounts();
+}}
 
 // for some checkpoint, the fromBlock is less than the current block number
 // passes but fails rule sanity from hash on delegate by sig
@@ -90,54 +105,135 @@ invariant timestamp_constrains_fromBlock(address account, uint32 index, env e)
     }
 }
 
-// numCheckpoints are less than maxInt
-// passes
-invariant maxInt_constrains_numBlocks(address account)
-    numCheckpoints(account) <= 4294967295 // 2^32
+// TODO add a note about this in the report
+// // numCheckpoints are less than maxInt
+// // passes because numCheckpoints does a safeCast
+// invariant maxInt_constrains_numBlocks(address account)
+//     numCheckpoints(account) < 4294967295 // 2^32
+
+// // fails because there are no checks to stop it 
+// invariant maxInt_constrains_ckptsLength(address account)
+//     unsafeNumCheckpoints(account) < 4294967295 // 2^32
 
 // can't have more checkpoints for a given account than the last from block
+// passes
 invariant fromBlock_constrains_numBlocks(address account)
-    numCheckpoints(account) <= lastFromBlock(account)
+    numCheckpoints(account) <= ckptFromBlock(account, numCheckpoints(account) - 1)
+{ preserved with(env e) {
+    uint32 pos;
+    uint32 pos2;
+    requireInvariant fromBlock_greaterThanEq_pos(account, pos);
+    requireInvariant fromBlock_increasing(account, pos, pos2);
+    require e.block.number >= ckptFromBlock(account, numCheckpoints(account) - 1); // this should be true from the invariant above!!
+}}
 
-// this fails, which makes sense because there is no require about the previous fromBlock
-invariant unique_checkpoints(address account)
-    !doubleFromBlock(account)
+// for any given checkpoint, the fromBlock must be greater than the checkpoint
+// this proves the above invariant in combination with the below invariant
+// if checkpoint has a greater fromBlock than the last, and the FromBlock is always greater than the pos. 
+// Then the number of positions must be less than the currentFromBlock
+// ^note that the tool is assuming it's possible for the starting fromBlock to be 0 or anything, and does not know the current starting block
+// passes + rule sanity
+invariant fromBlock_greaterThanEq_pos(address account, uint32 pos)
+    ckptFromBlock(account, pos) >= pos
 
-// if an account has been delegated too, then both accounts must have a checkpoint
-invariant delegated_implies_checkpoints(address delegator, address delegatee)
-    delegates(delegator) == delegatee => numCheckpoints(delegator) > 0 && numCheckpoints(delegatee) > 0
-{ preserved with (env e) {
+// a larger index must have a larger fromBlock
+// passes + rule sanity
+invariant fromBlock_increasing(address account, uint32 pos, uint32 pos2)
+    pos > pos2 => ckptFromBlock(account, pos) > ckptFromBlock(account, pos2)
+
+
+invariant no_delegate_no_checkpoints(address account)
+    delegates(account) == 0x0 => numCheckpoints(account) == 0
+{ preserved delegate(address delegatee) with(env e) {
+    require delegatee != 0;
+} preserved _delegate(address delegator, address delegatee) with(env e) {
     require delegatee != 0;
-    require balanceOf(e, delegator) > 0;
 }}
 
+// converted from an invariant to a rule to slightly change the logic
+// if the fromBlock is the same as before, then the number of checkpoints stays the same
+// however if the fromBlock is new than the number of checkpoints increases
+rule unique_checkpoints_rule(method f) {
+    env e; calldataarg args;
+
+    require e.block.number > 0; // we don't care about this exception
+
+    address account;
+
+    require unsafeNumCheckpoints(account) < 4294967295; // 2^32 // we don't want to deal with the checkpoint overflow error here
+
+    uint32 num_ckpts_ = numCheckpoints(account); 
+    uint32 fromBlock_ = num_ckpts_ == 0 ? 0 : ckptFromBlock(account, num_ckpts_ - 1);
+
+    f(e, args);
+
+    uint32 _num_ckpts = numCheckpoints(account);
+    uint32 _fromBlock = _num_ckpts == 0 ? 0 : ckptFromBlock(account, _num_ckpts - 1);
+    
+
+    // assert fromBlock_ == _fromBlock => num_ckpts_ == _num_ckpts, "same fromBlock, new checkpoint";
+    assert doubleFromBlock(account) => num_ckpts_ == _num_ckpts, "same fromBlock, new checkpoint";
+    // this assert fails consistently
+    // assert !doubleFromBlock(account) => ckpts_ != _ckpts, "new fromBlock but total checkpoints not being increased";
+}
+
 // assumes neither account has delegated
+// currently fails due to this scenario. A has maxint number of checkpoints
+// an additional checkpoint is added which overflows and sets A's votes to 0
 rule transfer_safe() {
     env e;
     uint256 amount;
     address a; address b;
     require a != b;
+    require delegates(a) != delegates(b); // confirmed if they both delegate to the same person then transfer keeps the votes the sameå
+    // requireInvariant fromBlock_constrains_numBlocks(a);
+    // requireInvariant fromBlock_constrains_numBlocks(b);
     // requireInvariant totalVotes_gte_accounts(a, b);
 
-    address delegateA = delegates(a);
-    address delegateB = delegates(b);
+    uint256 votesA_pre = getVotes(delegates(a));
+    uint256 votesB_pre = getVotes(delegates(b));
 
-    uint256 votesA_pre = getVotes(delegateA);
-    uint256 votesB_pre = getVotes(delegateB);
+    // for debugging
+    uint256 balA_ = balanceOf(e, a);
+    uint256 balB_ = balanceOf(e, b);
 
     mathint totalVotes_pre = totalVotes();
 
     erc20votes.transferFrom(e, a, b, amount);
 
+    
+    require lastIndex(delegates(a)) < 1000000;
+    require lastIndex(delegates(b)) < 1000000;
+    
     mathint totalVotes_post = totalVotes();
-    uint256 votesA_post = getVotes(delegateA);
-    uint256 votesB_post = getVotes(delegateB);
+    uint256 votesA_post = getVotes(delegates(a));
+    uint256 votesB_post = getVotes(delegates(b));
+
+    // for debugging
+    uint256 _balA = balanceOf(e, a);
+    uint256 _balB = balanceOf(e, b);
 
     // if an account that has not delegated transfers balance to an account that has, it will increase the total supply of votes
     assert totalVotes_pre == totalVotes_post, "transfer changed total supply";
-    assert delegateA == delegates(a) && delegateB == delegates(b), "delegates changed by transfer";
-    assert delegateA != 0 => votesA_pre - votesA_post == amount, "a lost the proper amount of votes";
-    assert delegateB != 0 => votesB_post - votesB_pre == amount, "b lost the proper amount of votes";
+    assert delegates(a) != 0 => votesA_pre - votesA_post == amount, "A lost the wrong amount of votes";
+    assert delegates(b) != 0 => votesB_post - votesB_pre == amount, "B lost the wrong amount of votes";
+}
+
+// for any given function f, if the delegate is changed the function must be delegate or delegateBySig
+// passes
+rule delegates_safe(method f) filtered {f -> (f.selector != delegate(address).selector &&
+                                                f.selector != _delegate(address, address).selector &&
+                                                f.selector != delegateBySig(address, uint256, uint256, uint8, bytes32, bytes32).selector) }
+{
+    env e; calldataarg args;
+    address account;
+    address pre = delegates(account);
+
+    f(e, args);
+
+    address post = delegates(account);
+
+    assert pre == post, "invalid delegate change";
 }
 
 
@@ -158,18 +254,22 @@ rule delegator_votes_removed() {
     assert post == pre - balance, "delegator retained votes";
 }
 
+// delegates increases the delegatee's votes by the proper amount
+// passes + rule sanity
 rule delegatee_receives_votes() {
     env e; 
     address delegator; address delegatee;
 
-    require delegator != delegatee;
     require delegates(delegator) != delegatee;
+    require delegatee != 0x0;
 
     uint256 delegator_bal = balanceOf(e, delegator);
     uint256 votes_= getVotes(delegatee);
 
     _delegate(e, delegator, delegatee);
 
+    require lastIndex(delegatee) < 1000000;
+
     uint256 _votes = getVotes(delegatee);
 
     assert _votes == votes_ + delegator_bal, "delegatee did not receive votes";
@@ -246,6 +346,8 @@ rule delegate_no_frontrunning(method f) {
     assert other_ == _other, "delegate not contained";
 }
 
+
+
 // passes
 rule mint_increases_totalSupply() {