call trace error

certora/applyHarness.patch

@@ -1,6 +1,6 @@
 diff -ruN access/AccessControl.sol access/AccessControl.sol
 --- access/AccessControl.sol	2022-03-02 09:14:55.000000000 -0800
-+++ access/AccessControl.sol	2022-03-24 16:41:46.000000000 -0700
++++ access/AccessControl.sol	2022-03-24 18:08:46.000000000 -0700
 @@ -93,7 +93,7 @@
       *
       * _Available since v4.6._
@@ -12,7 +12,7 @@ diff -ruN access/AccessControl.sol access/AccessControl.sol
  
 diff -ruN governance/TimelockController.sol governance/TimelockController.sol
 --- governance/TimelockController.sol	2022-03-02 09:14:55.000000000 -0800
-+++ governance/TimelockController.sol	2022-03-24 16:41:46.000000000 -0700
++++ governance/TimelockController.sol	2022-03-24 18:08:46.000000000 -0700
 @@ -24,10 +24,10 @@
      bytes32 public constant TIMELOCK_ADMIN_ROLE = keccak256("TIMELOCK_ADMIN_ROLE");
      bytes32 public constant PROPOSER_ROLE = keccak256("PROPOSER_ROLE");
@@ -41,7 +41,7 @@ diff -ruN governance/TimelockController.sol governance/TimelockController.sol
 +} 
 diff -ruN governance/utils/Votes.sol governance/utils/Votes.sol
 --- governance/utils/Votes.sol	2022-03-02 09:14:55.000000000 -0800
-+++ governance/utils/Votes.sol	2022-03-24 16:41:46.000000000 -0700
++++ governance/utils/Votes.sol	2022-03-24 18:08:46.000000000 -0700
 @@ -207,5 +207,5 @@
      /**
       * @dev Must return the voting units held by an account.
@@ -51,7 +51,7 @@ diff -ruN governance/utils/Votes.sol governance/utils/Votes.sol
  }
 diff -ruN token/ERC20/ERC20.sol token/ERC20/ERC20.sol
 --- token/ERC20/ERC20.sol	2022-03-02 09:14:55.000000000 -0800
-+++ token/ERC20/ERC20.sol	2022-03-24 16:41:46.000000000 -0700
++++ token/ERC20/ERC20.sol	2022-03-24 18:08:46.000000000 -0700
 @@ -277,7 +277,7 @@
       * - `account` cannot be the zero address.
       * - `account` must have at least `amount` tokens.
@@ -72,7 +72,7 @@ diff -ruN token/ERC20/ERC20.sol token/ERC20/ERC20.sol
      /**
 diff -ruN token/ERC20/extensions/ERC20FlashMint.sol token/ERC20/extensions/ERC20FlashMint.sol
 --- token/ERC20/extensions/ERC20FlashMint.sol	2022-03-02 09:14:55.000000000 -0800
-+++ token/ERC20/extensions/ERC20FlashMint.sol	2022-03-24 16:41:46.000000000 -0700
++++ token/ERC20/extensions/ERC20FlashMint.sol	2022-03-24 18:08:46.000000000 -0700
 @@ -40,9 +40,11 @@
          require(token == address(this), "ERC20FlashMint: wrong token");
          // silence warning about unused variable without the addition of bytecode.
@@ -97,7 +97,7 @@ diff -ruN token/ERC20/extensions/ERC20FlashMint.sol token/ERC20/extensions/ERC20
          uint256 currentAllowance = allowance(address(receiver), address(this));
 diff -ruN token/ERC20/extensions/ERC20Votes.sol token/ERC20/extensions/ERC20Votes.sol
 --- token/ERC20/extensions/ERC20Votes.sol	2022-03-02 09:14:55.000000000 -0800
-+++ token/ERC20/extensions/ERC20Votes.sol	2022-03-24 17:15:51.000000000 -0700
++++ token/ERC20/extensions/ERC20Votes.sol	2022-03-25 13:13:49.000000000 -0700
 @@ -33,8 +33,8 @@
      bytes32 private constant _DELEGATION_TYPEHASH =
          keccak256("Delegation(address delegatee,uint256 nonce,uint256 expiry)");
@@ -230,7 +230,7 @@ diff -ruN token/ERC20/extensions/ERC20Votes.sol token/ERC20/extensions/ERC20Vote
      }
 diff -ruN token/ERC20/extensions/ERC20Wrapper.sol token/ERC20/extensions/ERC20Wrapper.sol
 --- token/ERC20/extensions/ERC20Wrapper.sol	2022-03-02 09:14:55.000000000 -0800
-+++ token/ERC20/extensions/ERC20Wrapper.sol	2022-03-24 16:41:46.000000000 -0700
++++ token/ERC20/extensions/ERC20Wrapper.sol	2022-03-24 18:08:46.000000000 -0700
 @@ -44,7 +44,7 @@
       * @dev Mint wrapped token to cover any underlyingTokens that would have been transferred by mistake. Internal
       * function that can be exposed with access control if desired.

certora/harnesses/ERC20VotesHarness.sol

@@ -18,5 +18,15 @@ contract ERC20VotesHarness is ERC20Votes {
     function burn(address account, uint256 amount) public {
         _burn(account, amount);
     }
+
+    function delegateBySig(
+        address delegatee,
+        uint256 nonce,
+        uint256 expiry,
+        uint8 v,
+        bytes32 r,
+        bytes32 s
+    ) public virtual override { }
+
 }
 

certora/scripts/ERC20VotesRule.sh

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

certora/specs/ERC20Votes.spec

@@ -10,7 +10,7 @@ methods {
     getPastTotalSupply(uint256) returns (uint256)
     delegate(address)
     _delegate(address, address)
-    delegateBySig(address, uint256, uint256, uint8, bytes32, bytes32)
+    // delegateBySig(address, uint256, uint256, uint8, bytes32, bytes32)
     totalSupply() returns (uint256) envfree
     _maxSupply() returns (uint224) envfree
 
@@ -32,9 +32,13 @@ ghost userVotes(address) returns uint224;
 
 // sums the total votes for all users
 ghost totalVotes() returns mathint {
-    axiom totalVotes() > 0;
+    axiom totalVotes() >= 0;
 }
 
+// helper
+
+invariant totalVotes_gte_accounts(address a, address b)
+    totalVotes() >= getVotes(a) + getVotes(b)
 
 
 hook Sstore _checkpoints[KEY address account][INDEX uint32 index].votes uint224 newVotes (uint224 oldVotes) STORAGE {
@@ -95,32 +99,45 @@ invariant maxInt_constrains_numBlocks(address account)
 invariant fromBlock_constrains_numBlocks(address account)
     numCheckpoints(account) <= lastFromBlock(account)
 
+// this fails, which makes sense because there is no require about the previous fromBlock
 invariant unique_checkpoints(address account)
     !doubleFromBlock(account)
 
+// 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) {
+    require delegatee != 0;
+    require balanceOf(e, delegator) > 0;
+}}
+
+// assumes neither account has delegated
 rule transfer_safe() {
     env e;
     uint256 amount;
     address a; address b;
     require a != b;
+    // requireInvariant totalVotes_gte_accounts(a, b);
 
-    uint256 votesA_pre = getVotes(a);
+    address delegateA = delegates(a);
-    uint256 votesB_pre = getVotes(b);
+    address delegateB = delegates(b);
 
-    require votesA_pre == erc20votes.balanceOf(e, a);
+    uint256 votesA_pre = getVotes(delegateA);
-    require votesB_pre == erc20votes.balanceOf(e, b);
+    uint256 votesB_pre = getVotes(delegateB);
 
     mathint totalVotes_pre = totalVotes();
 
     erc20votes.transferFrom(e, a, b, amount);
     
     mathint totalVotes_post = totalVotes();
-    uint256 votesA_post = getVotes(a);
+    uint256 votesA_post = getVotes(delegateA);
-    uint256 votesB_post = getVotes(b);
+    uint256 votesB_post = getVotes(delegateB);
 
+    // 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 votesA_pre - votesA_post == amount, "a lost the proper amount of votes";
+    assert delegateA == delegates(a) && delegateB == delegates(b), "delegates changed by transfer";
-    assert votesB_post - votesB_pre == amount, "b lost the proper amount of votes";
+    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";
 }
 
 
@@ -144,7 +161,9 @@ rule delegator_votes_removed() {
 rule delegatee_receives_votes() {
     env e; 
     address delegator; address delegatee;
+
     require delegator != delegatee;
+    require delegates(delegator) != delegatee;
 
     uint256 delegator_bal = balanceOf(e, delegator);
     uint256 votes_= getVotes(delegatee);
@@ -156,13 +175,14 @@ rule delegatee_receives_votes() {
     assert _votes == votes_ + delegator_bal, "delegatee did not receive votes";
 }
 
-rule previous_delegatee_zerod() {
+rule previous_delegatee_zeroed() {
     env e;
     address delegator; address delegatee; address third;
 
-    require delegator != delegatee;
     require third != delegatee;
     require third != delegator;
+    require delegates(delegator) == third;
+    // for third to have been delegated to, it must have a checkpoint
 
     uint256 delegator_bal = balanceOf(e, delegator);
     uint256 votes_ = getVotes(third);
@@ -171,16 +191,14 @@ rule previous_delegatee_zerod() {
 
     uint256 _votes = getVotes(third);
 
-    assert votes_ == votes_ - delegator_bal, "votes not removed from the previous delegatee";
+    assert _votes == votes_ - delegator_bal, "votes not removed from the previous delegatee";
 }
 
-// passes
+// passes with rule sanity
 rule delegate_contained() {
     env e;
     address delegator; address delegatee; address other;
 
-    require delegator != delegatee;
-    require other != delegator;
     require other != delegatee;
     require other != delegates(delegator);