Start working on ERC20 specs

certora/applyHarness.patch

@@ -278,18 +278,6 @@ 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-20 13:34:47.024598756 +0200
-+++ token/ERC20/ERC20.sol	2022-09-20 14:34:24.809915708 +0200
-@@ -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

certora/harnesses/ERC20PermitHarness.sol

@@ -1,5 +1,14 @@
+import "../munged/token/ERC20/ERC20.sol";
 import "../munged/token/ERC20/extensions/draft-ERC20Permit.sol";
 
-contract ERC20PermitHarness is ERC20Permit {
-    constructor(string memory _name, string memory _symbol) ERC20(_name, _symbol) ERC20Permit(_name) {}
+contract ERC20Harness 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

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

certora/harnesses/ERC20WrapperHarness.sol

@@ -2,10 +2,10 @@ import "../munged/token/ERC20/extensions/ERC20Wrapper.sol";
 
 contract ERC20WrapperHarness is ERC20Wrapper {
     constructor(
-        IERC20 underlyingToken,
+        IERC20 _underlying,
         string memory _name,
         string memory _symbol
-    ) ERC20Wrapper(underlyingToken) ERC20(_name, _symbol) {}
+    ) ERC20(_name, _symbol) ERC20Wrapper(_underlying) {}
 
     function underlyingTotalSupply() public view returns (uint256) {
         return underlying.totalSupply();

certora/scripts/Round2/verifyAccessControl.sh

@@ -7,4 +7,5 @@ certoraRun \
     --verify AccessControlHarness:certora/specs/AccessControl.spec \
     --solc solc \
     --optimistic_loop \
-    --msg "AccessControl verification"
+    --msg "AccessControl verification" \
+    $@

certora/scripts/Round2/verifyERC1155.sh

@@ -8,4 +8,5 @@ certoraRun \
     --solc solc \
     --optimistic_loop \
     --loop_iter 3 \
-    --msg "ERC1155"
+    --msg "ERC1155" \
+    $@

certora/scripts/Round2/verifyERC20FlashMint.sh

@@ -10,4 +10,5 @@ certoraRun \
     --verify ERC20FlashMintHarness:certora/specs/ERC20FlashMint.spec \
     --solc solc \
     --optimistic_loop \
-    --msg "ERC20FlashMint verification"
+    --msg "ERC20FlashMint verification" \
+    $@

certora/scripts/Round2/verifyERC20Votes.sh

@@ -8,4 +8,5 @@ certoraRun \
     --solc solc \
     --optimistic_loop \
     --settings -copyLoopUnroll=4 \
-    --msg "ERC20Votes"
+    --msg "ERC20Votes" \
+    $@

certora/scripts/Round2/verifyERC20Wrapper.sh

@@ -7,4 +7,5 @@ certoraRun \
     --verify ERC20WrapperHarness:certora/specs/ERC20Wrapper.spec \
     --solc solc \
     --optimistic_loop \
-    --msg "ERC20Wrapper verification"
+    --msg "ERC20Wrapper verification" \
+    $@

certora/scripts/Round2/verifyERC721Votes.sh

@@ -9,4 +9,5 @@ certoraRun \
     --optimistic_loop \
     --disableLocalTypeChecking \
     --settings -copyLoopUnroll=4 \
-    --msg "ERC721Votes"
+    --msg "ERC721Votes" \
+    $@

certora/scripts/Round2/verifyTimelock.sh

@@ -9,4 +9,5 @@ certoraRun \
     --optimistic_loop \
     --loop_iter 3 \
     --settings -byteMapHashingPrecision=32 \
-    --msg "TimelockController verification"
+    --msg "TimelockController verification" \
+    $@

certora/scripts/verifyERC20.sh

@@ -0,0 +1,10 @@
+#!/usr/bin/env bash
+
+set -euxo pipefail
+
+certoraRun \
+    certora/harnesses/ERC20Harness.sol \
+    --verify ERC20Harness:certora/specs/ERC20.spec \
+    --solc solc \
+    --optimistic_loop \
+    $@

certora/scripts/verifyGovernorPreventLateQuorum.sh

@@ -3,7 +3,10 @@
 set -euxo pipefail
 
 certoraRun \
-    certora/harnesses/ERC721VotesHarness.sol certora/munged/governance/TimelockController.sol certora/harnesses/GovernorPreventLateQuorumHarness.sol \
+    certora/harnesses/ERC20VotesHarness.sol \
+    certora/harnesses/ERC721VotesHarness.sol \
+    certora/munged/governance/TimelockController.sol \
+    certora/harnesses/GovernorPreventLateQuorumHarness.sol \
     --verify GovernorPreventLateQuorumHarness:certora/specs/GovernorPreventLateQuorum.spec \
     --solc solc \
     --optimistic_loop \

certora/specs/ERC20.spec

@@ -0,0 +1,157 @@
+import "erc20.spec"
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Ghost & hooks: sum of all balances                                                                                  │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+ghost sumOfBalances() returns uint256 {
+  init_state axiom sumOfBalances() == 0;
+}
+
+hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) STORAGE {
+    havoc sumOfBalances assuming sumOfBalances@new() == sumOfBalances@old() + newValue - oldValue;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: totalSupply is the sum of all balances                                                                   │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant totalSupplyIsSumOfBalances()
+    totalSupply() == sumOfBalances()
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: balance of address(0) is 0                                                                               │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant zeroAddressNoBalance()
+    balanceOf(0) == 0
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rules: totalSupply only changes through mint or burn                                                                │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule noChangeTotalSupply() {
+    requireInvariant totalSupplyIsSumOfBalances();
+
+    env e;
+    method f;
+    calldataarg args;
+
+    uint256 totalSupplyBefore = totalSupply();
+    f(e, args);
+    uint256 totalSupplyAfter = totalSupply();
+
+    assert (totalSupplyAfter > totalSupplyBefore) => (f.selector == mint(address,uint256).selector);
+    assert (totalSupplyAfter < totalSupplyBefore) => (f.selector == burn(address,uint256).selector);
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rules: totalSupply change matches minted or burned amount                                                           │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule mintIncreasesTotalSupply() {
+    requireInvariant totalSupplyIsSumOfBalances();
+
+    env e;
+    address to;
+    uint256 amount;
+
+    uint256 totalSupplyBefore = totalSupply();
+    mint(e, to, amount);
+    uint256 totalSupplyAfter = totalSupply();
+
+    assert totalSupplyAfter == totalSupplyBefore + amount;
+}
+
+rule burnDecreasesTotalSupply() {
+    requireInvariant totalSupplyIsSumOfBalances();
+
+    env e;
+    address from;
+    uint256 amount;
+
+    uint256 totalSupplyBefore = totalSupply();
+    burn(e, from, amount);
+    uint256 totalSupplyAfter = totalSupply();
+
+    assert totalSupplyAfter == totalSupplyBefore - amount;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rules: Balance of an account can only decrease if the tx was sent by owner or by approved                           │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule onlyAuthorizedCanTransfer() {
+    requireInvariant totalSupplyIsSumOfBalances();
+
+    env e;
+    method f;
+    calldataarg args;
+    address account;
+
+    uint256 allowanceBefore = allowance(account, e.msg.sender);
+    uint256 balanceBefore   = balanceOf(account);
+    f(e, args);
+    uint256 balanceAfter    = balanceOf(account);
+
+    assert (
+        balanceAfter < balanceBefore
+    ) => (
+        f.selector == burn(address,uint256).selector ||
+        e.msg.sender == account ||
+        balanceBefore - balanceAfter <= allowanceBefore
+    );
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: transfer moves correct amount from sender to receiver                                                         │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule transferAmount() {
+    requireInvariant totalSupplyIsSumOfBalances();
+
+    env e;
+    address holder = e.msg.sender;
+    address recipient;
+    uint256 amount;
+
+    uint256 holderBalanceBefore    = balanceOf(holder);
+    uint256 recipientBalanceBefore = balanceOf(recipient);
+
+    transfer(e, recipient, amount);
+
+    assert balanceOf(holder)    == holderBalanceBefore    - (holder == recipient ? 0 : amount);
+    assert balanceOf(recipient) == recipientBalanceBefore + (holder == recipient ? 0 : amount);
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: transferFrom moves correct amount from holder to receiver, and updates allowance                              │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule transferFomAmountAndApproval() {
+    requireInvariant totalSupplyIsSumOfBalances();
+
+    env e;
+    address holder;
+    address recipient;
+    uint256 amount;
+
+    uint256 allowanceBefore        = allowance(holder, e.msg.sender);
+    uint256 holderBalanceBefore    = balanceOf(holder);
+    uint256 recipientBalanceBefore = balanceOf(recipient);
+
+    transferFrom(e, holder, recipient, 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);
+}

certora/specs/ERC20FlashMint.spec

@@ -7,16 +7,18 @@ methods {
 
 ghost mapping(address => uint256) trackedBurnAmount;
 
-function specBurn(address account, uint256 amount) returns bool {   // retuns needed to overcome current CVL limitations: "could not type expression "specBurn(account,amount)", message: A summary must return a simple type, but specBurn(account,amount) returns 'void'"
+// retuns needed to overcome current CVL limitations: "could not type expression "specBurn(account,amount)", message: A summary must return a simple type, but specBurn(account,amount) returns 'void'"
+function specBurn(address account, uint256 amount) returns bool {
     trackedBurnAmount[account] = amount;
     return true;
 }
 
-
-// STATUS - verified
 // Check that if flashLoan() call is successful, then proper amount of tokens was burnt(fee + flashLoan amount)
-rule letsWatchItBurns(env e){
-    address receiver; address token; uint256 amount; bytes data;
+rule letsWatchItBurns(env e) {
+    address receiver;
+    address token;
+    uint256 amount;
+    bytes data;
 
     uint256 feeBefore = flashFee(e, token, amount);
 

certora/specs/ERC20Votes.spec

@@ -1,28 +1,46 @@
+import "erc20.spec"
+
 methods {
-    // functions
-    checkpoints(address, uint32) envfree
-    numCheckpoints(address) returns (uint32) envfree
-    delegates(address) returns (address) envfree
+    // IVotes
     getVotes(address) returns (uint256) envfree
-    getPastVotes(address, uint256) returns (uint256)
-    getPastTotalSupply(uint256) returns (uint256)
-    delegate(address)
-    _delegate(address, address)
+    getPastVotes(address, uint256) returns (uint256) // not envfree (reads block.number)
+    getPastTotalSupply(uint256) returns (uint256) // not envfree (reads block.number)
+    delegates(address) returns (address) envfree
+    delegate(address) // not envfree (reads msg.sender)
     // delegateBySig(address, uint256, uint256, uint8, bytes32, bytes32)
-    totalSupply() returns (uint256) envfree
+
+    // ERC20Votes
+    checkpoints(address, uint32) envfree
+    numCheckpoints(address) returns (uint32) envfree
     _maxSupply() returns (uint224) envfree
+    _delegate(address, address) // not envfree (reads block.number when creating checkpoint)
 
     // harnesss functions
     ckptFromBlock(address, uint32) returns (uint32) envfree
     ckptVotes(address, uint32) returns (uint224) envfree
-    mint(address, uint256)
-    burn(address, uint256)
     unsafeNumCheckpoints(address) returns (uint256) envfree
+    mint(address, uint256) // not envfree (reads block.number when creating checkpoint)
+    burn(address, uint256) // not envfree (reads block.number when creating checkpoint)
+
     // solidity generated getters
     _delegates(address) returns (address) envfree
-
-    // external functions
 }
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
 // gets the most recent votes for a user
 ghost userVotes(address) returns uint224 {
     init_state axiom forall address a. userVotes(a) == 0;
@@ -32,10 +50,11 @@ ghost userVotes(address) returns uint224 {
 ghost totalVotes() returns uint224 {
     init_state axiom totalVotes() == 0;
 }
+
 ghost lastIndex(address) returns uint32;
-// helper
 
-hook Sstore _checkpoints[KEY address account][INDEX uint32 index].votes uint224 newVotes (uint224 oldVotes) STORAGE {    
+// helper
+hook Sstore _checkpoints[KEY address account][INDEX uint32 index].votes uint224 newVotes (uint224 oldVotes) STORAGE {
     havoc userVotes assuming
         userVotes@new(account) == newVotes;
 
@@ -46,38 +65,39 @@ hook Sstore _checkpoints[KEY address account][INDEX uint32 index].votes uint224
         lastIndex@new(account) == index;
 }
 
-
 ghost lastFromBlock(address) returns uint32;
 
 ghost doubleFromBlock(address) returns bool {
     init_state axiom forall address a. doubleFromBlock(a) == false;
 }
 
-
-
-
 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 
+
+    havoc doubleFromBlock assuming
         doubleFromBlock@new(account) == (newBlock == lastFromBlock(account));
 }
 
+///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
+//                                                    Invariants                                                     //
+///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
+
 // sum of user balances is >= total amount of delegated votes
 // fails on burn. This is because burn does not remove votes from the users
 invariant votes_solvency()
     totalSupply() >= to_uint256(totalVotes())
-filtered { f -> f.selector != _burn(address, uint256).selector}
-{ preserved with(env e) {
-    require forall address account. numCheckpoints(account) < 1000000;
-} preserved burn(address a, uint256 amount) with(env e){
-    require _delegates(0) == 0;
-    require forall address a2. (_delegates(a) != _delegates(a2)) && (balanceOf(e, _delegates(a)) + balanceOf(e, _delegates(a2)) <= totalVotes());
-    require balanceOf(e, _delegates(a)) < totalVotes();
-    require amount < 100000;
-}}
-
+    filtered { f -> f.selector != _burn(address, uint256).selector }
+{
+    preserved with(env e) {
+        require forall address account. numCheckpoints(account) < 1000000;
+    } preserved burn(address a, uint256 amount) with(env e) {
+        require _delegates(0) == 0;
+        require forall address a2. (_delegates(a) != _delegates(a2)) && (balanceOf(e, _delegates(a)) + balanceOf(e, _delegates(a2)) <= totalVotes());
+        require balanceOf(e, _delegates(a)) < totalVotes();
+        require amount < 100000;
+    }
+}
 
 // for some checkpoint, the fromBlock is less than the current block number
 invariant blockNum_constrains_fromBlock(address account, uint32 index, env e)
@@ -88,23 +108,24 @@ invariant blockNum_constrains_fromBlock(address account, uint32 index, env e)
         require index < numCheckpoints(account);
     }
 }
+
 // numCheckpoints are less than maxInt
-// passes because numCheckpoints does a safeCast
-// invariant maxInt_constrains_numBlocks(address account)
-//     numCheckpoints(account) < 4294967295 // 2^32
+invariant maxInt_constrains_numBlocks(address account)
+    numCheckpoints(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) <= ckptFromBlock(account, numCheckpoints(account) - 1)
     filtered { f -> !f.isView }
-{ preserved with(env e) {
-    require e.block.number >= ckptFromBlock(account, numCheckpoints(account) - 1); // this should be true from the invariant above!!
-}}
+{
+    preserved with(env e) {
+        require e.block.number >= ckptFromBlock(account, numCheckpoints(account) - 1); // this should be true from the invariant above!!
+    }
+}
 
 // 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
@@ -118,6 +139,9 @@ invariant fromBlock_increasing(address account, uint32 pos, uint32 pos2)
     pos > pos2 => ckptFromBlock(account, pos) > ckptFromBlock(account, pos2)
     filtered { f -> !f.isView }
 
+///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
+//                                                       Rules                                                       //
+///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
 
 // 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
@@ -126,14 +150,13 @@ 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";
 }
@@ -153,7 +176,7 @@ rule transfer_safe() {
     uint256 votesB_pre = getVotes(delegates(b));
     uint224 totalVotes_pre = totalVotes();
     transferFrom(e, a, b, amount);
-    
+
     uint224 totalVotes_post = totalVotes();
     uint256 votesA_post = getVotes(delegates(a));
     uint256 votesB_post = getVotes(delegates(b));
@@ -164,9 +187,12 @@ rule transfer_safe() {
 }
 // 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) }
+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;
@@ -175,16 +201,16 @@ rule delegates_safe(method f) filtered {f -> (f.selector != delegate(address).se
     address post = delegates(account);
     assert pre == post, "invalid delegate change";
 }
+
 // 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 delegates(delegator) != delegatee;
     require delegatee != 0x0;
 
-
     uint256 delegator_bal = balanceOf(e, delegator);
     uint256 votes_= getVotes(delegatee);
 
@@ -222,7 +248,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);
 
@@ -237,12 +263,9 @@ rule delegate_no_frontrunning(method f) {
     env e; calldataarg args;
     address delegator; address delegatee; address third; address other;
 
-
-
     require numCheckpoints(delegatee) < 1000000;
     require numCheckpoints(third) < 1000000;
 
-
     f(e, args);
 
     uint256 delegator_bal = balanceOf(e, delegator);
@@ -270,63 +293,42 @@ rule delegate_no_frontrunning(method f) {
     assert other_votes_ == _other_votes, "delegate not contained";
 }
 
-
-
 // passes
-rule mint_increases_totalSupply() {
-
+rule onMint() {
     env e;
-    uint256 amount; address account;
+    uint256 amount;
+    address account;
 
     uint256 fromBlock = e.block.number;
-    uint256 totalSupply_ = totalSupply();
+    uint224 totalVotesBefore = totalVotes();
+    uint256 totalSupplyBefore = totalSupply();
 
     mint(e, account, amount);
 
-    uint256 _totalSupply = totalSupply();
-    require _totalSupply < _maxSupply();
+    uint224 totalVotesAfter = totalVotes();
+    uint256 totalSupplyAfter = totalSupply();
 
-    assert _totalSupply == totalSupply_ + amount, "totalSupply not increased properly";
-    assert getPastTotalSupply(e, fromBlock) == totalSupply_ , "previous total supply not saved properly";
+    assert totalVotes() == totalVotesBefore, "totalVotes decreased";
+    assert totalSupplyAfter == totalSupplyBefore + amount, "totalSupply not increased properly";
+    assert getPastTotalSupply(e, fromBlock) == totalSupplyBefore , "previous total supply not saved properly";
 }
 
 // passes
-rule burn_decreases_totalSupply() {
+rule onBurn() {
     env e;
-    uint256 amount; address account;
+    uint256 amount;
+    address account;
 
     uint256 fromBlock = e.block.number;
-    uint256 totalSupply_ = totalSupply();
+    uint224 totalVotesBefore = totalVotes();
+    uint256 totalSupplyBefore = totalSupply();
 
     burn(e, account, amount);
 
-    uint256 _totalSupply = totalSupply();
-
-    assert _totalSupply == totalSupply_ - amount, "totalSupply not decreased properly";
-    assert getPastTotalSupply(e, fromBlock) == totalSupply_ , "previous total supply not saved properly";
-}
-
-
-
-// passes
-rule mint_doesnt_increase_totalVotes() {
-    env e;
-    uint256 amount; address account;
-
-    uint224 totalVotes_ = totalVotes();
-
-    mint(e, account, amount);
+    uint224 totalVotesAfter = totalVotes();
+    uint256 totalSupplyAfter = totalSupply();
 
-    assert totalVotes() == totalVotes_, "totalVotes increased";
+    assert totalVotes() == totalVotesBefore, "totalVotes decreased";
+    assert totalSupplyAfter == totalSupplyBefore - amount, "totalSupply not decreased properly";
+    assert getPastTotalSupply(e, fromBlock) == totalSupplyBefore , "previous total supply not saved properly";
 }
-// passes
-rule burn_doesnt_decrease_totalVotes() {
-    env e;
-    uint256 amount; address account;
-
-    uint224 totalVotes_ = totalVotes();
-
-    burn(e, account, amount);
-
-    assert totalVotes() == totalVotes_, "totalVotes decreased";
-}

certora/specs/ERC20Wrapper.spec

@@ -10,12 +10,14 @@ methods {
     _recover(address) returns(uint256)
 }
 
+///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
+//                                                    Invariants                                                     //
+///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
 
-// STATUS - verified
 // totalsupply of wrapped should be less than or equal to underlying (assuming no external transfer) - solvency
 invariant whatAboutTotal(env e)
     totalSupply(e) <= underlyingTotalSupply()
-    filtered { f -> f.selector != certorafallback_0().selector && !f.isView}
+    filtered { f -> f.selector != certorafallback_0().selector && !f.isView }
     {
         preserved {
             require underlyingBalanceOf(currentContract) <= underlyingTotalSupply();
@@ -25,8 +27,6 @@ invariant whatAboutTotal(env e)
         }
     }
 
-
-// STATUS - verified
 // totalsupply of wrapped should be less than or equal to the underlying balanceOf contract (assuming no external transfer) - solvency
 invariant underTotalAndContractBalanceOfCorrelation(env e)
     totalSupply(e) <= underlyingBalanceOf(currentContract)
@@ -38,11 +38,14 @@ invariant underTotalAndContractBalanceOfCorrelation(env e)
         }
     }
 
+///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
+//                                                       Rules                                                       //
+///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
 
-// STATUS - verified
 // Check that values are updated correctly by `depositFor()`
-rule depositForSpecBasic(env e){
-    address account; uint256 amount;
+rule depositForSpecBasic(env e) {
+    address account;
+    uint256 amount;
 
     require e.msg.sender != currentContract;
     require underlying() != currentContract;
@@ -62,11 +65,10 @@ rule depositForSpecBasic(env e){
     assert underlyingThisBalanceBefore == underlyingThisBalanceAfter - amount, "underlying this balance wrong update";
 }
 
-
-// STATUS - verified
 // Check that values are updated correctly by `depositFor()`
-rule depositForSpecWrapper(env e){
-    address account; uint256 amount;
+rule depositForSpecWrapper(env e) {
+    address account;
+    uint256 amount;
 
     require underlying() != currentContract;
 
@@ -78,18 +80,20 @@ rule depositForSpecWrapper(env e){
     uint256 wrapperUserBalanceAfter = balanceOf(e, account);
     uint256 wrapperSenderBalanceAfter = balanceOf(e, e.msg.sender);
 
-    assert account == e.msg.sender => wrapperUserBalanceBefore == wrapperSenderBalanceBefore 
-                && wrapperUserBalanceAfter == wrapperSenderBalanceAfter 
-                && wrapperUserBalanceBefore == wrapperUserBalanceAfter - amount, "wrapper balances wrong update";
+    assert account == e.msg.sender => wrapperUserBalanceBefore == wrapperSenderBalanceBefore
+        && wrapperUserBalanceAfter == wrapperSenderBalanceAfter
+        && wrapperUserBalanceBefore == wrapperUserBalanceAfter - amount
+        , "wrapper balances wrong update";
+
     assert account != e.msg.sender => wrapperUserBalanceBefore == wrapperUserBalanceAfter - amount
-                && wrapperSenderBalanceBefore == wrapperSenderBalanceAfter, "wrapper balances wrong update";
+        && wrapperSenderBalanceBefore == wrapperSenderBalanceAfter
+        , "wrapper balances wrong update";
 }
 
-
-// STATUS - verified
 // Check that values are updated correctly by `depositFor()`
-rule depositForSpecUnderlying(env e){
-    address account; uint256 amount;
+rule depositForSpecUnderlying(env e) {
+    address account;
+    uint256 amount;
 
     require e.msg.sender != currentContract;
     require underlying() != currentContract;
@@ -103,21 +107,25 @@ rule depositForSpecUnderlying(env e){
     uint256 underlyingUserBalanceAfter = underlyingBalanceOf(account);
 
     assert account == e.msg.sender => underlyingSenderBalanceBefore == underlyingUserBalanceBefore
-                && underlyingSenderBalanceAfter == underlyingUserBalanceAfter
-                && underlyingSenderBalanceBefore == underlyingSenderBalanceAfter + amount, "underlying balances wrong update";
-    
-    assert account != e.msg.sender && account == currentContract => underlyingSenderBalanceBefore == underlyingSenderBalanceAfter + amount
-                && underlyingUserBalanceBefore == underlyingUserBalanceAfter - amount, "underlying balances wrong update";
-    
-    assert account != e.msg.sender && account != currentContract => underlyingSenderBalanceBefore == underlyingSenderBalanceAfter + amount
-                && underlyingUserBalanceBefore == underlyingUserBalanceAfter, "underlying balances wrong update";
+        && underlyingSenderBalanceAfter == underlyingUserBalanceAfter
+        && underlyingSenderBalanceBefore == underlyingSenderBalanceAfter + amount
+        , "underlying balances wrong update";
+
+    assert account != e.msg.sender
+        && account == currentContract => underlyingSenderBalanceBefore == underlyingSenderBalanceAfter + amount
+        && underlyingUserBalanceBefore == underlyingUserBalanceAfter - amount
+        , "underlying balances wrong update";
+
+    assert account != e.msg.sender
+        && account != currentContract => underlyingSenderBalanceBefore == underlyingSenderBalanceAfter + amount
+        && underlyingUserBalanceBefore == underlyingUserBalanceAfter
+        , "underlying balances wrong update";
 }
 
-
-// STATUS - verified
 // Check that values are updated correctly by `withdrawTo()`
-rule withdrawToSpecBasic(env e){
-    address account; uint256 amount;
+rule withdrawToSpecBasic(env e) {
+    address account;
+    uint256 amount;
 
     require underlying() != currentContract;
 
@@ -133,10 +141,8 @@ rule withdrawToSpecBasic(env e){
     assert underlyingTotalBefore == underlyingTotalAfter, "underlying total was updated";
 }
 
-
-// STATUS - verified
 // Check that values are updated correctly by `withdrawTo()`
-rule withdrawToSpecWrapper(env e){
+rule withdrawToSpecWrapper(env e) {
     address account; uint256 amount;
 
     require underlying() != currentContract;
@@ -148,18 +154,21 @@ rule withdrawToSpecWrapper(env e){
 
     uint256 wrapperUserBalanceAfter = balanceOf(e, account);
     uint256 wrapperSenderBalanceAfter = balanceOf(e, e.msg.sender);
-    
+
     assert account == e.msg.sender => wrapperUserBalanceBefore == wrapperSenderBalanceBefore
-                && wrapperUserBalanceAfter == wrapperSenderBalanceAfter
-                && wrapperUserBalanceBefore == wrapperUserBalanceAfter + amount, "wrapper user balance wrong update";
+        && wrapperUserBalanceAfter == wrapperSenderBalanceAfter
+        && wrapperUserBalanceBefore == wrapperUserBalanceAfter + amount
+        , "wrapper user balance wrong update";
+
     assert account != e.msg.sender => wrapperSenderBalanceBefore == wrapperSenderBalanceAfter + amount
-                && wrapperUserBalanceBefore == wrapperUserBalanceAfter, "wrapper user balance wrong update";
+        && wrapperUserBalanceBefore == wrapperUserBalanceAfter
+        , "wrapper user balance wrong update";
 }
 
 
 // STATUS - verified
-// cCheck that values are updated correctly by `withdrawTo()`
-rule withdrawToSpecUnderlying(env e){
+// Check that values are updated correctly by `withdrawTo()`
+rule withdrawToSpecUnderlying(env e) {
     address account; uint256 amount;
 
     require e.msg.sender != currentContract;
@@ -175,22 +184,25 @@ rule withdrawToSpecUnderlying(env e){
     uint256 underlyingUserBalanceAfter = underlyingBalanceOf(account);
     uint256 underlyingThisBalanceAfter = underlyingBalanceOf(currentContract);
 
-    assert account == e.msg.sender => underlyingSenderBalanceBefore == underlyingUserBalanceBefore 
-                && underlyingSenderBalanceAfter == underlyingUserBalanceAfter 
-                && underlyingUserBalanceBefore == underlyingUserBalanceAfter - amount, "underlying balances wrong update (acc == sender)";
-    
+    assert account == e.msg.sender => underlyingSenderBalanceBefore == underlyingUserBalanceBefore
+        && underlyingSenderBalanceAfter == underlyingUserBalanceAfter
+        && underlyingUserBalanceBefore == underlyingUserBalanceAfter - amount
+        , "underlying balances wrong update (acc == sender)";
+
     assert account != e.msg.sender && account == currentContract => underlyingUserBalanceBefore == underlyingUserBalanceAfter
-                && underlyingSenderBalanceBefore == underlyingSenderBalanceAfter, "underlying balances wrong update (acc == contract)"; 
+        && underlyingSenderBalanceBefore == underlyingSenderBalanceAfter
+        , "underlying balances wrong update (acc == contract)";
+
     assert account != e.msg.sender && account != currentContract => underlyingUserBalanceBefore == underlyingUserBalanceAfter - amount
-                && underlyingSenderBalanceBefore == underlyingSenderBalanceAfter
-                && underlyingThisBalanceBefore == underlyingThisBalanceAfter + amount, "underlying balances wrong update (acc != contract)";   
+        && underlyingSenderBalanceBefore == underlyingSenderBalanceAfter
+        && underlyingThisBalanceBefore == underlyingThisBalanceAfter + amount
+        , "underlying balances wrong update (acc != contract)";
 }
 
-
-// STATUS - verified
 // Check that values are updated correctly by `_recover()`
-rule recoverSpec(env e){
-    address account; uint256 amount;
+rule recoverSpec(env e) {
+    address account;
+    uint256 amount;
 
     uint256 wrapperTotalBefore = totalSupply(e);
     uint256 wrapperUserBalanceBefore = balanceOf(e, account);
@@ -204,11 +216,15 @@ rule recoverSpec(env e){
     uint256 wrapperTotalAfter = totalSupply(e);
     uint256 wrapperUserBalanceAfter = balanceOf(e, account);
     uint256 wrapperSenderBalanceAfter = balanceOf(e, e.msg.sender);
-    
+
     assert wrapperTotalBefore == wrapperTotalAfter - value, "wrapper total wrong update";
+
     assert e.msg.sender == account => wrapperUserBalanceBefore == wrapperSenderBalanceBefore
-                && wrapperUserBalanceAfter == wrapperSenderBalanceAfter
-                && wrapperUserBalanceBefore == wrapperUserBalanceAfter - value, "wrapper balances wrong update";
+        && wrapperUserBalanceAfter == wrapperSenderBalanceAfter
+        && wrapperUserBalanceBefore == wrapperUserBalanceAfter - value
+        , "wrapper balances wrong update";
+
     assert e.msg.sender != account => wrapperUserBalanceBefore == wrapperUserBalanceAfter - value
-                && wrapperSenderBalanceBefore == wrapperSenderBalanceAfter, "wrapper balances wrong update";
-}
+        && wrapperSenderBalanceBefore == wrapperSenderBalanceAfter
+        , "wrapper balances wrong update";
+}

certora/specs/erc20.spec

@@ -1,12 +1,12 @@
 // erc20 methods
 methods {
-    name()                                returns (string)  => DISPATCHER(true)
-    symbol()                              returns (string)  => DISPATCHER(true)
-    decimals()                            returns (string)  => DISPATCHER(true)
-    totalSupply()                         returns (uint256) => DISPATCHER(true)
-    balanceOf(address)                    returns (uint256) => DISPATCHER(true)
-    allowance(address,address)            returns (uint)    => DISPATCHER(true)
-    approve(address,uint256)              returns (bool)    => DISPATCHER(true)
-    transfer(address,uint256)             returns (bool)    => DISPATCHER(true)
-    transferFrom(address,address,uint256) returns (bool)    => DISPATCHER(true)
+    name()                                returns (string)  envfree => DISPATCHER(true)
+    symbol()                              returns (string)  envfree => DISPATCHER(true)
+    decimals()                            returns (uint8)   envfree => DISPATCHER(true)
+    totalSupply()                         returns (uint256) envfree => DISPATCHER(true)
+    balanceOf(address)                    returns (uint256) envfree => DISPATCHER(true)
+    allowance(address,address)            returns (uint256) envfree => DISPATCHER(true)
+    approve(address,uint256)              returns (bool)            => DISPATCHER(true)
+    transfer(address,uint256)             returns (bool)            => DISPATCHER(true)
+    transferFrom(address,address,uint256) returns (bool)            => DISPATCHER(true)
 }