finish ERC20 base specs + move all other specs to noCI for the time being

certora/applyHarness.patch

@@ -1,6 +1,6 @@
 diff -ruN access/AccessControl.sol access/AccessControl.sol
---- access/AccessControl.sol	2022-09-20 11:01:10.429515094 +0200
-+++ access/AccessControl.sol	2022-09-20 14:34:08.629602185 +0200
+--- access/AccessControl.sol	2022-09-27 10:26:58.548890299 +0200
++++ access/AccessControl.sol	2022-09-27 17:51:32.011301116 +0200
 @@ -93,7 +93,7 @@
       *
       * _Available since v4.6._
@@ -9,68 +9,68 @@ diff -ruN access/AccessControl.sol access/AccessControl.sol
 +    function _checkRole(bytes32 role) public view virtual {         // HARNESS: internal -> public
          _checkRole(role, _msgSender());
      }
-
+ 
 diff -ruN governance/extensions/GovernorCountingSimple.sol governance/extensions/GovernorCountingSimple.sol
---- governance/extensions/GovernorCountingSimple.sol	2022-09-20 11:01:10.432848512 +0200
-+++ governance/extensions/GovernorCountingSimple.sol	2022-09-20 14:34:08.632935582 +0200
+--- governance/extensions/GovernorCountingSimple.sol	2022-09-27 10:26:58.548890299 +0200
++++ governance/extensions/GovernorCountingSimple.sol	2022-09-27 17:51:32.011301116 +0200
 @@ -27,7 +27,7 @@
          mapping(address => bool) hasVoted;
      }
-
+ 
 -    mapping(uint256 => ProposalVote) private _proposalVotes;
 +    mapping(uint256 => ProposalVote) internal _proposalVotes;
-
+ 
      /**
       * @dev See {IGovernor-COUNTING_MODE}.
 diff -ruN governance/extensions/GovernorPreventLateQuorum.sol governance/extensions/GovernorPreventLateQuorum.sol
 --- governance/extensions/GovernorPreventLateQuorum.sol	2022-08-31 13:44:36.377724869 +0200
-+++ governance/extensions/GovernorPreventLateQuorum.sol	2022-09-20 14:34:08.632935582 +0200
++++ governance/extensions/GovernorPreventLateQuorum.sol	2022-09-27 17:51:32.011301116 +0200
 @@ -21,8 +21,8 @@
      using SafeCast for uint256;
      using Timers for Timers.BlockNumber;
-
+ 
 -    uint64 private _voteExtension;
 -    mapping(uint256 => Timers.BlockNumber) private _extendedDeadlines;
 +    uint64 internal _voteExtension;                                         // PRIVATE => INTERNAL
 +    mapping(uint256 => Timers.BlockNumber) internal _extendedDeadlines;     // PRIVATE => INTERNAL
-
+ 
      /// @dev Emitted when a proposal deadline is pushed back due to reaching quorum late in its voting period.
      event ProposalExtended(uint256 indexed proposalId, uint64 extendedDeadline);
 diff -ruN governance/Governor.sol governance/Governor.sol
---- governance/Governor.sol	2022-09-20 11:01:10.429515094 +0200
-+++ governance/Governor.sol	2022-09-20 14:34:08.629602185 +0200
+--- governance/Governor.sol	2022-09-27 10:26:58.548890299 +0200
++++ governance/Governor.sol	2022-09-27 17:51:32.014634743 +0200
 @@ -44,7 +44,7 @@
-
+ 
      string private _name;
-
+ 
 -    mapping(uint256 => ProposalCore) private _proposals;
 +    mapping(uint256 => ProposalCore) internal _proposals;
-
+ 
      // This queue keeps track of the governor operating on itself. Calls to functions protected by the
      // {onlyGovernance} modifier needs to be whitelisted in this queue. Whitelisting is set in {_beforeExecute},
 diff -ruN governance/TimelockController.sol governance/TimelockController.sol
---- governance/TimelockController.sol	2022-09-09 10:15:55.887175731 +0200
-+++ governance/TimelockController.sol	2022-09-20 14:34:08.629602185 +0200
+--- governance/TimelockController.sol	2022-09-27 10:26:58.548890299 +0200
++++ governance/TimelockController.sol	2022-09-27 17:51:32.014634743 +0200
 @@ -28,10 +28,10 @@
      bytes32 public constant PROPOSER_ROLE = keccak256("PROPOSER_ROLE");
      bytes32 public constant EXECUTOR_ROLE = keccak256("EXECUTOR_ROLE");
      bytes32 public constant CANCELLER_ROLE = keccak256("CANCELLER_ROLE");
 -    uint256 internal constant _DONE_TIMESTAMP = uint256(1);
 +    uint256 public constant _DONE_TIMESTAMP = uint256(1);
-
+ 
      mapping(bytes32 => uint256) private _timestamps;
 -    uint256 private _minDelay;
 +    uint256 public _minDelay;
-
+ 
      /**
       * @dev Emitted when a call is scheduled as part of operation `id`.
 diff -ruN governance/utils/Votes.sol governance/utils/Votes.sol
---- governance/utils/Votes.sol	2022-09-20 14:24:58.010074267 +0200
-+++ governance/utils/Votes.sol	2022-09-20 14:34:08.632935582 +0200
+--- governance/utils/Votes.sol	2022-09-27 10:26:58.548890299 +0200
++++ governance/utils/Votes.sol	2022-09-27 17:51:32.014634743 +0200
 @@ -35,7 +35,25 @@
      bytes32 private constant _DELEGATION_TYPEHASH =
          keccak256("Delegation(address delegatee,uint256 nonce,uint256 expiry)");
-
+ 
 -    mapping(address => address) private _delegation;
 +    // HARNESS : Hooks cannot access any information from Checkpoints yet, so I am also updating votes and fromBlock in this struct
 +    struct Ckpt {
@@ -93,7 +93,7 @@ diff -ruN governance/utils/Votes.sol governance/utils/Votes.sol
 +    mapping(address => address) public _delegation;
      mapping(address => Checkpoints.History) private _delegateCheckpoints;
      Checkpoints.History private _totalCheckpoints;
-
+ 
 @@ -124,7 +142,7 @@
       *
       * Emits events {DelegateChanged} and {DelegateVotesChanged}.
@@ -102,7 +102,7 @@ diff -ruN governance/utils/Votes.sol governance/utils/Votes.sol
 +    function _delegate(address account, address delegatee) public virtual {
          address oldDelegate = delegates(account);
          _delegation[account] = delegatee;
-
+ 
 @@ -142,10 +160,10 @@
          uint256 amount
      ) internal virtual {
@@ -140,20 +140,20 @@ diff -ruN governance/utils/Votes.sol governance/utils/Votes.sol
 +    function _getVotingUnits(address) public virtual returns (uint256); // HARNESS: internal -> public
  }
 diff -ruN mocks/SafeERC20Helper.sol mocks/SafeERC20Helper.sol
---- mocks/SafeERC20Helper.sol	2022-09-20 14:24:58.013407601 +0200
-+++ mocks/SafeERC20Helper.sol	2022-09-20 15:09:17.135329080 +0200
+--- mocks/SafeERC20Helper.sol	2022-09-26 19:10:21.166619395 +0200
++++ mocks/SafeERC20Helper.sol	2022-09-27 17:51:32.014634743 +0200
 @@ -4,7 +4,6 @@
-
+ 
  import "../utils/Context.sol";
  import "../token/ERC20/IERC20.sol";
 -import "../token/ERC20/extensions/draft-ERC20Permit.sol";
  import "../token/ERC20/utils/SafeERC20.sol";
-
+ 
  contract ERC20ReturnFalseMock is Context {
 @@ -106,42 +105,43 @@
      }
  }
-
+ 
 -contract ERC20PermitNoRevertMock is
 -    ERC20("ERC20PermitNoRevertMock", "ERC20PermitNoRevertMock"),
 -    ERC20Permit("ERC20PermitNoRevertMock")
@@ -227,37 +227,37 @@ diff -ruN mocks/SafeERC20Helper.sol mocks/SafeERC20Helper.sol
 +//         }
 +//     }
 +// }
-
+ 
  contract SafeERC20Wrapper is Context {
      using SafeERC20 for IERC20;
 diff -ruN proxy/utils/Initializable.sol proxy/utils/Initializable.sol
---- proxy/utils/Initializable.sol	2022-09-20 11:16:48.456850883 +0200
-+++ proxy/utils/Initializable.sol	2022-09-20 14:34:24.806582310 +0200
+--- proxy/utils/Initializable.sol	2022-09-27 10:26:58.548890299 +0200
++++ proxy/utils/Initializable.sol	2022-09-27 17:51:32.014634743 +0200
 @@ -59,12 +59,12 @@
       * @dev Indicates that the contract has been initialized.
       * @custom:oz-retyped-from bool
       */
 -    uint8 private _initialized;
 +    uint8 internal _initialized;
-
+ 
      /**
       * @dev Indicates that the contract is in the process of being initialized.
       */
 -    bool private _initializing;
 +    bool internal _initializing;
-
+ 
      /**
       * @dev Triggered when the contract has been initialized or reinitialized.
 diff -ruN token/ERC1155/ERC1155.sol token/ERC1155/ERC1155.sol
---- token/ERC1155/ERC1155.sol	2022-09-20 11:01:10.432848512 +0200
-+++ token/ERC1155/ERC1155.sol	2022-09-20 14:34:24.809915708 +0200
+--- token/ERC1155/ERC1155.sol	2022-09-27 10:26:58.548890299 +0200
++++ token/ERC1155/ERC1155.sol	2022-09-27 17:51:32.014634743 +0200
 @@ -21,7 +21,7 @@
      using Address for address;
-
+ 
      // Mapping from token ID to account balances
 -    mapping(uint256 => mapping(address => uint256)) private _balances;
 +    mapping(uint256 => mapping(address => uint256)) internal _balances; // MUNGED private => internal
-
+ 
      // Mapping from account to operator approvals
      mapping(address => mapping(address => bool)) private _operatorApprovals;
 @@ -471,7 +471,7 @@
@@ -278,9 +278,30 @@ diff -ruN token/ERC1155/ERC1155.sol token/ERC1155/ERC1155.sol
          if (to.isContract()) {
              try IERC1155Receiver(to).onERC1155BatchReceived(operator, from, ids, amounts, data) returns (
                  bytes4 response
+diff -ruN token/ERC20/ERC20.sol token/ERC20/ERC20.sol
+--- token/ERC20/ERC20.sol	2022-09-27 10:26:58.548890299 +0200
++++ token/ERC20/ERC20.sol	2022-09-27 22:22:40.377802680 +0200
+@@ -256,7 +256,7 @@
+      *
+      * - `account` cannot be the zero address.
+      */
+-    function _mint(address account, uint256 amount) internal virtual {
++    function _mint(address account, uint256 amount) public virtual { // HARNESS: internal -> public
+         require(account != address(0), "ERC20: mint to the zero address");
+ 
+         _beforeTokenTransfer(address(0), account, amount);
+@@ -282,7 +282,7 @@
+      * - `account` cannot be the zero address.
+      * - `account` must have at least `amount` tokens.
+      */
+-    function _burn(address account, uint256 amount) internal virtual {
++    function _burn(address account, uint256 amount) public virtual { // HARNESS: internal -> public
+         require(account != address(0), "ERC20: burn from the zero address");
+ 
+         _beforeTokenTransfer(account, address(0), amount);
 diff -ruN token/ERC20/extensions/ERC20FlashMint.sol token/ERC20/extensions/ERC20FlashMint.sol
---- token/ERC20/extensions/ERC20FlashMint.sol	2022-09-20 11:01:10.432848512 +0200
-+++ token/ERC20/extensions/ERC20FlashMint.sol	2022-09-20 14:34:24.809915708 +0200
+--- token/ERC20/extensions/ERC20FlashMint.sol	2022-09-27 10:26:58.548890299 +0200
++++ token/ERC20/extensions/ERC20FlashMint.sol	2022-09-27 17:51:32.014634743 +0200
 @@ -51,9 +51,11 @@
          // silence warning about unused variable without the addition of bytecode.
          token;
@@ -288,25 +309,25 @@ diff -ruN token/ERC20/extensions/ERC20FlashMint.sol token/ERC20/extensions/ERC20
 -        return 0;
 +        return fee;                 // HARNESS: made "return" nonzero
      }
-
+ 
 +    uint256 public fee;             // HARNESS: added it to simulate random fee amount
 +
      /**
       * @dev Returns the receiver address of the flash fee. By default this
       * implementation returns the address(0) which means the fee amount will be burnt.
 diff -ruN token/ERC20/extensions/ERC20Votes.sol token/ERC20/extensions/ERC20Votes.sol
---- token/ERC20/extensions/ERC20Votes.sol	2022-09-20 14:24:58.016740934 +0200
-+++ token/ERC20/extensions/ERC20Votes.sol	2022-09-20 15:05:11.770836991 +0200
+--- token/ERC20/extensions/ERC20Votes.sol	2022-09-27 10:26:58.548890299 +0200
++++ token/ERC20/extensions/ERC20Votes.sol	2022-09-27 17:51:32.014634743 +0200
 @@ -33,8 +33,8 @@
      bytes32 private constant _DELEGATION_TYPEHASH =
          keccak256("Delegation(address delegatee,uint256 nonce,uint256 expiry)");
-
+ 
 -    mapping(address => address) private _delegates;
 -    mapping(address => Checkpoint[]) private _checkpoints;
 +    mapping(address => address) public _delegates;
 +    mapping(address => Checkpoint[]) public _checkpoints;
      Checkpoint[] private _totalSupplyCheckpoints;
-
+ 
      /**
 @@ -165,7 +165,7 @@
      /**
@@ -316,26 +337,26 @@ diff -ruN token/ERC20/extensions/ERC20Votes.sol token/ERC20/extensions/ERC20Vote
 +    function _maxSupply() public view virtual returns (uint224) { //harnessed to public
          return type(uint224).max;
      }
-
+ 
 @@ -176,16 +176,16 @@
          super._mint(account, amount);
          require(totalSupply() <= _maxSupply(), "ERC20Votes: total supply risks overflowing votes");
-
+ 
 -        _writeCheckpoint(_totalSupplyCheckpoints, _add, amount);
 +        _writeCheckpointAdd(_totalSupplyCheckpoints, amount);           // HARNESS: new version without pointer
      }
-
+ 
      /**
       * @dev Snapshots the totalSupply after it has been decreased.
       */
 -    function _burn(address account, uint256 amount) internal virtual override {
 +    function _burn(address account, uint256 amount) public virtual override { // HARNESS: internal -> public (to comply with the ERC20 harness)
          super._burn(account, amount);
-
+ 
 -        _writeCheckpoint(_totalSupplyCheckpoints, _subtract, amount);
 +        _writeCheckpointSub(_totalSupplyCheckpoints, amount);           // HARNESS: new version without pointer
      }
-
+ 
      /**
 @@ -208,7 +208,7 @@
       *
@@ -355,7 +376,7 @@ diff -ruN token/ERC20/extensions/ERC20Votes.sol token/ERC20/extensions/ERC20Vote
 +
                  emit DelegateVotesChanged(src, oldWeight, newWeight);
              }
-
+ 
              if (dst != address(0)) {
 -                (uint256 oldWeight, uint256 newWeight) = _writeCheckpoint(_checkpoints[dst], _add, amount);
 +                (uint256 oldWeight, uint256 newWeight) = _writeCheckpointAdd(_checkpoints[dst], amount); // HARNESS: new version without pointer
@@ -365,7 +386,7 @@ diff -ruN token/ERC20/extensions/ERC20Votes.sol token/ERC20/extensions/ERC20Vote
 @@ -255,6 +256,55 @@
          }
      }
-
+ 
 +    // HARNESS: split _writeCheckpoint() to two functions as a workaround for function pointers that cannot be managed by the tool
 +    function _writeCheckpointAdd(
 +        Checkpoint[] storage ckpts,
@@ -420,8 +441,8 @@ 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-08-31 13:44:36.381058287 +0200
-+++ token/ERC20/extensions/ERC20Wrapper.sol	2022-09-20 14:34:24.809915708 +0200
-@@ -55,7 +44,7 @@
++++ token/ERC20/extensions/ERC20Wrapper.sol	2022-09-27 17:51:32.014634743 +0200
+@@ -55,7 +55,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.
       */
@@ -431,8 +452,8 @@ diff -ruN token/ERC20/extensions/ERC20Wrapper.sol token/ERC20/extensions/ERC20Wr
          _mint(account, value);
          return value;
 diff -ruN token/ERC721/extensions/draft-ERC721Votes.sol token/ERC721/extensions/draft-ERC721Votes.sol
---- token/ERC721/extensions/draft-ERC721Votes.sol	2022-09-20 14:24:58.016740934 +0200
-+++ token/ERC721/extensions/draft-ERC721Votes.sol	2022-09-20 14:34:28.259983206 +0200
+--- token/ERC721/extensions/draft-ERC721Votes.sol	2022-09-27 10:26:58.548890299 +0200
++++ token/ERC721/extensions/draft-ERC721Votes.sol	2022-09-27 17:51:32.014634743 +0200
 @@ -49,7 +49,7 @@
      /**
       * @dev Returns the balance of `account`.
@@ -443,8 +464,8 @@ diff -ruN token/ERC721/extensions/draft-ERC721Votes.sol token/ERC721/extensions/
      }
  }
 diff -ruN utils/Address.sol utils/Address.sol
---- utils/Address.sol	2022-09-20 11:01:10.432848512 +0200
-+++ utils/Address.sol	2022-09-20 14:34:28.259983206 +0200
+--- utils/Address.sol	2022-09-27 10:26:58.552223642 +0200
++++ utils/Address.sol	2022-09-27 17:51:32.014634743 +0200
 @@ -131,6 +131,7 @@
          uint256 value,
          string memory errorMessage

certora/harnesses/ERC20PermitHarness.sol

@@ -1,14 +1,5 @@
-import "../munged/token/ERC20/ERC20.sol";
 import "../munged/token/ERC20/extensions/draft-ERC20Permit.sol";
 
-contract ERC20Harness is ERC20, ERC20Permit {
+contract ERC20PermitHarness is ERC20, ERC20Permit {
     constructor(string memory name, string memory symbol) ERC20(name, symbol) ERC20Permit(name) {}
-
-    function mint(address account, uint256 amount) public {
-        _mint(account, amount);
-    }
-
-    function burn(address account, uint256 amount) public {
-        _burn(account, amount);
-    }
 }

certora/harnesses/ERC20VotesHarness.sol

@@ -3,14 +3,6 @@ import "../munged/token/ERC20/extensions/ERC20Votes.sol";
 contract ERC20VotesHarness is ERC20Votes {
     constructor(string memory name, string memory symbol) ERC20(name, symbol) ERC20Permit(name) {}
 
-    function mint(address account, uint256 amount) public {
-        _mint(account, amount);
-    }
-
-    function burn(address account, uint256 amount) public {
-        _burn(account, amount);
-    }
-
     function ckptFromBlock(address account, uint32 pos) public view returns (uint32) {
         return _checkpoints[account][pos].fromBlock;
     }

certora/scripts/verifyERC20.sh

@@ -3,8 +3,8 @@
 set -euxo pipefail
 
 certoraRun \
-    certora/harnesses/ERC20Harness.sol \
-    --verify ERC20Harness:certora/specs/ERC20.spec \
+    certora/harnesses/ERC20PermitHarness.sol \
+    --verify ERC20PermitHarness:certora/specs/ERC20.spec \
     --solc solc \
     --optimistic_loop \
     $@

certora/specs/ERC20.spec

@@ -1,4 +1,4 @@
-import "erc20.spec"
+import "interfaces/erc20.spec"
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
@@ -45,8 +45,8 @@ rule noChangeTotalSupply() {
     f(e, args);
     uint256 totalSupplyAfter = totalSupply();
 
-    assert (totalSupplyAfter > totalSupplyBefore) => (f.selector == mint(address,uint256).selector);
-    assert (totalSupplyAfter < totalSupplyBefore) => (f.selector == burn(address,uint256).selector);
+    assert (totalSupplyAfter > totalSupplyBefore) => (f.selector == _mint(address,uint256).selector);
+    assert (totalSupplyAfter < totalSupplyBefore) => (f.selector == _burn(address,uint256).selector);
 }
 
 /*
@@ -62,7 +62,7 @@ rule mintIncreasesTotalSupply() {
     uint256 amount;
 
     uint256 totalSupplyBefore = totalSupply();
-    mint(e, to, amount);
+    _mint(e, to, amount);
     uint256 totalSupplyAfter = totalSupply();
 
     assert totalSupplyAfter == totalSupplyBefore + amount;
@@ -76,7 +76,7 @@ rule burnDecreasesTotalSupply() {
     uint256 amount;
 
     uint256 totalSupplyBefore = totalSupply();
-    burn(e, from, amount);
+    _burn(e, from, amount);
     uint256 totalSupplyAfter = totalSupply();
 
     assert totalSupplyAfter == totalSupplyBefore - amount;
@@ -84,7 +84,7 @@ rule burnDecreasesTotalSupply() {
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rules: Balance of an account can only decrease if the tx was sent by owner or by approved                           │
+│ Rules: Balance can only decrease if the tx was sent by holder or by approved spender                                │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 rule onlyAuthorizedCanTransfer() {
@@ -103,55 +103,240 @@ rule onlyAuthorizedCanTransfer() {
     assert (
         balanceAfter < balanceBefore
     ) => (
-        f.selector == burn(address,uint256).selector ||
+        f.selector == _burn(address,uint256).selector ||
         e.msg.sender == account ||
         balanceBefore - balanceAfter <= allowanceBefore
     );
 }
 
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rules: Allowance can only change if holder calls approve or spender uses allowance                                  │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule onlyHolderOfSpenderCanChangeAllowance() {
+    requireInvariant totalSupplyIsSumOfBalances();
+
+    env e;
+    method f;
+    calldataarg args;
+    address holder;
+    address spender;
+
+    uint256 allowanceBefore = allowance(holder, spender);
+    f(e, args);
+    uint256 allowanceAfter = allowance(holder, spender);
+
+    assert (
+        allowanceAfter > allowanceBefore
+    ) => (
+        (f.selector == approve(address,uint256).selector           && e.msg.sender == holder) ||
+        (f.selector == increaseAllowance(address,uint256).selector && e.msg.sender == holder) ||
+        (f.selector == permit(address,address,uint256,uint256,uint8,bytes32,bytes32).selector)
+    );
+
+    assert (
+        allowanceAfter < allowanceBefore
+    ) => (
+        (f.selector == approve(address,uint256).selector              && e.msg.sender == holder ) ||
+        (f.selector == decreaseAllowance(address,uint256).selector    && e.msg.sender == holder ) ||
+        (f.selector == transferFrom(address,address,uint256).selector && e.msg.sender == spender) ||
+        (f.selector == permit(address,address,uint256,uint256,uint8,bytes32,bytes32).selector)
+    );
+}
+
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
 │ Rule: transfer moves correct amount from sender to receiver                                                         │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
-rule transferAmount() {
+rule transfer() {
     requireInvariant totalSupplyIsSumOfBalances();
 
     env e;
     address holder = e.msg.sender;
     address recipient;
+    address other;
     uint256 amount;
 
+    // env: function is not payable
+    require e.msg.sender != 0;
+    require e.msg.value  == 0;
+
+    // cache state
     uint256 holderBalanceBefore    = balanceOf(holder);
     uint256 recipientBalanceBefore = balanceOf(recipient);
+    uint256 otherBalanceBefore     = balanceOf(other);
+
+    // run transaction
+    transfer@withrevert(e, recipient, amount);
 
-    transfer(e, recipient, amount);
+    // check outcome
+    if (lastReverted) {
+        assert holder == 0 || recipient == 0 || amount > holderBalanceBefore;
+    } else {
+        // balances of holder and recipient are updated
+        assert balanceOf(holder)    == holderBalanceBefore    - (holder == recipient ? 0 : amount);
+        assert balanceOf(recipient) == recipientBalanceBefore + (holder == recipient ? 0 : amount);
 
-    assert balanceOf(holder)    == holderBalanceBefore    - (holder == recipient ? 0 : amount);
-    assert balanceOf(recipient) == recipientBalanceBefore + (holder == recipient ? 0 : amount);
+        // no other balance is modified
+        assert balanceOf(other) != otherBalanceBefore => (other == holder || other == recipient);
+    }
 }
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rule: transferFrom moves correct amount from holder to receiver, and updates allowance                              │
+│ Rule: transferFrom moves correct amount from holder to receiver and updates allowance                               │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
-rule transferFomAmountAndApproval() {
+rule transferFrom() {
     requireInvariant totalSupplyIsSumOfBalances();
 
     env e;
     address holder;
     address recipient;
+    address other;
     uint256 amount;
 
+    // env: function is not payable
+    require e.msg.sender != 0;
+    require e.msg.value  == 0;
+
+    // cache state
     uint256 allowanceBefore        = allowance(holder, e.msg.sender);
     uint256 holderBalanceBefore    = balanceOf(holder);
     uint256 recipientBalanceBefore = balanceOf(recipient);
+    uint256 otherBalanceBefore     = balanceOf(other);
+
+    // run transaction
+    transferFrom@withrevert(e, holder, recipient, amount);
+
+    // check outcome
+    if (lastReverted) {
+        assert holder == 0 || recipient == 0 || amount > holderBalanceBefore || amount > allowanceBefore;
+    } else {
+        // allowance is valid & updated
+        assert allowanceBefore                 >= amount;
+        assert allowance(holder, e.msg.sender) == (allowanceBefore == max_uint256 ? to_uint256(max_uint256) : allowanceBefore - amount);
+
+        // balances of holder and recipient are updated
+        assert balanceOf(holder)               == holderBalanceBefore    - (holder == recipient ? 0 : amount);
+        assert balanceOf(recipient)            == recipientBalanceBefore + (holder == recipient ? 0 : amount);
+
+        // no other balance is modified
+        assert balanceOf(other) != otherBalanceBefore => (other == holder || other == recipient);
+    }
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: approve sets allowance                                                                                        │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule approve() {
+    requireInvariant totalSupplyIsSumOfBalances();
+
+    env e;
+    address holder = e.msg.sender;
+    address spender;
+    address otherHolder;
+    address otherSpender;
+    uint256 amount;
+
+    // env: function is not payable
+    require e.msg.sender != 0;
+    require e.msg.value  == 0;
+
+    // cache state
+    uint256 otherAllowanceBefore = allowance(otherHolder, otherSpender);
 
-    transferFrom(e, holder, recipient, amount);
+    // run transaction
+    approve@withrevert(e, spender, amount);
 
-    assert allowanceBefore                 >= amount;
-    assert allowance(holder, e.msg.sender) == (allowanceBefore == max_uint256 ? to_uint256(max_uint256) : allowanceBefore - amount);
-    assert balanceOf(holder)               == holderBalanceBefore    - (holder == recipient ? 0 : amount);
-    assert balanceOf(recipient)            == recipientBalanceBefore + (holder == recipient ? 0 : amount);
+    // check outcome
+    if (lastReverted) {
+        assert spender == 0;
+    } else {
+        // allowance is updated
+        assert allowance(holder, spender) == amount;
+
+        // other allowances are untouched
+        assert allowance(otherHolder, otherSpender) != otherAllowanceBefore => (otherHolder == holder && otherSpender == spender);
+    }
 }
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: calling increaseAllowance increases the allowance                                                             │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule increaseAllowance() {
+    requireInvariant totalSupplyIsSumOfBalances();
+
+    env e;
+    address holder = e.msg.sender;
+    address spender;
+    address otherHolder;
+    address otherSpender;
+    uint256 amount;
+
+    // env: function is not payable
+    require e.msg.sender != 0;
+    require e.msg.value  == 0;
+
+    // cache state
+    uint256 allowanceBefore      = allowance(holder, spender);
+    uint256 otherAllowanceBefore = allowance(otherHolder, otherSpender);
+
+    // run transaction
+    increaseAllowance@withrevert(e, spender, amount);
+
+    // check outcome
+    if (lastReverted) {
+        assert spender == 0 || allowanceBefore + amount > max_uint256;
+    } else {
+        // allowance is updated
+        assert allowance(holder, spender) == allowanceBefore + amount;
+
+        // other allowances are untouched
+        assert allowance(otherHolder, otherSpender) != otherAllowanceBefore => (otherHolder == holder && otherSpender == spender);
+    }
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: calling decreaseAllowance decreases the allowance                                                             │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule decreaseAllowance() {
+    requireInvariant totalSupplyIsSumOfBalances();
+
+    env e;
+    address holder = e.msg.sender;
+    address spender;
+    address otherHolder;
+    address otherSpender;
+    uint256 amount;
+
+    // env: function is not payable
+    require e.msg.sender != 0;
+    require e.msg.value  == 0;
+
+    // cache state
+    uint256 allowanceBefore      = allowance(holder, spender);
+    uint256 otherAllowanceBefore = allowance(otherHolder, otherSpender);
+
+    // run transaction
+    decreaseAllowance@withrevert(e, spender, amount);
+
+    // check outcome
+    if (lastReverted) {
+        assert spender == 0 || allowanceBefore < amount;
+    } else {
+        // allowance is updated
+        assert allowance(holder, spender) == allowanceBefore - amount;
+
+        // other allowances are untouched
+        assert allowance(otherHolder, otherSpender) != otherAllowanceBefore => (otherHolder == holder && otherSpender == spender);
+    }
+}

certora/specs/ERC721Votes.spec

@@ -62,8 +62,8 @@ ghost doubleFromBlock(address) returns bool {
 hook Sstore _checkpoints[KEY address account].fromBlock uint32 newBlock (uint32 oldBlock) STORAGE {
     havoc lastFromBlock assuming
         lastFromBlock@new(account) == newBlock;
-    
-    havoc doubleFromBlock assuming 
+
+    havoc doubleFromBlock assuming
         doubleFromBlock@new(account) == (newBlock == lastFromBlock(account));
 }
 
@@ -94,7 +94,7 @@ invariant fromBlock_constrains_numBlocks(address 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. 
+// 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
@@ -116,14 +116,14 @@ invariant fromBlock_increasing(address account, uint32 pos, uint32 pos2)
 rule unique_checkpoints_rule(method f) {
     env e; calldataarg args;
     address account;
-    uint32 num_ckpts_ = numCheckpoints(account); 
+    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 || _num_ckpts == 1, "same fromBlock, new checkpoint";
     // this assert fails consistently
@@ -149,7 +149,7 @@ rule transfer_safe() {
     mathint totalVotes_pre = totalVotes();
 
     transferFrom(e, a, b, ID);
-    
+
     mathint totalVotes_post = totalVotes();
     uint256 votesA_post = getVotes(delegates(a));
     uint256 votesB_post = getVotes(delegates(b));
@@ -180,7 +180,7 @@ rule delegates_safe(method f) filtered {f -> (f.selector != delegate(address).se
 // delegates increases the delegatee's votes by the proper amount
 // passes + rule sanity
 rule delegatee_receives_votes() {
-    env e; 
+    env e;
     address delegator; address delegatee;
 
     require numCheckpoints(delegatee) < 1000000;
@@ -222,7 +222,7 @@ rule delegate_contained() {
     address delegator; address delegatee; address other;
 
     require other != delegatee;
-    require other != delegates(delegator); 
+    require other != delegates(delegator);
 
     uint256 votes_ = getVotes(other);