[Certora] Verify mint and burn

.github/workflows/certora.yml

@@ -24,6 +24,8 @@ jobs:
           - ERC20Optimism
           - ExternalCallsEthereum
           - ExternalCallsOptimism
+          - MintBurnEthereum
+          - MintBurnOptimism
 
     steps:
       - uses: actions/checkout@v4

certora/README.md

@@ -32,7 +32,7 @@ This is checked in [`ExternalCalls.spec`](specs/ExternalCalls.spec).
 
 ### ERC20 Compliance and Correctness
 
-This is checked in [`ERC20.spec`](specs/ERC20.spec) and [`ERC20Invariants.spec`](specs/ERC20Invariants.spec) .
+This is checked in [`ERC20.spec`](specs/ERC20.spec), [`ERC20Invariants.spec`](specs/ERC20Invariants.spec), [`MintBurnEthereum.spec`](specs/MintBurnEthereum.spec) and [`MintBurnOptimism.spec`](specs/MintBurnOptimism.spec).
 
 ### Delegation Correctness
 
@@ -46,7 +46,7 @@ The [`certora/specs`](specs) folder contains the following files:
 
 - [`ExternalCalls.spec`](specs/ExternalCalls.spec) checks that the Morpho token implementation is reentrancy safe by ensuring that no function is making and external calls and, that the implementation is immutable as it doesn't perform any delegate call;
 - [`ERC20Invariants.spec`](specs/ERC20Invariants.spec) common hooks and invariants to be shared in different specs;
-- [`ERC20.spec`](specs/ERC20.spec) ensure that the Morpho token is compliant with the [ERC20](https://eips.ethereum.org/EIPS/eip-20) specification;
+- [`ERC20.spec`](specs/ERC20.spec) ensures that the Morpho token is compliant with the [ERC20](https://eips.ethereum.org/EIPS/eip-20) specification, we also check Morpho token `burn` and `mint` functions in [`MintBurnEthereum`](specs/MintBurnEthereum.spec) and [`MintBurnOptimism`](specs/MintBurnOptimism.spec);
 - [`Delegation.spec`](specs/Delegation.spec) checks the logic for voting power delegation.
 
 The [`certora/confs`](confs) folder contains a configuration file for each corresponding specification file for both the Ethereum and the Optimism version.

certora/confs/DelegationEthereum.conf

@@ -4,7 +4,7 @@
     "certora/helpers/MorphoTokenOptimismHarness.sol"
   ],
   "parametric_contracts": [
-    "MorphoTokenEthereumHarness",
+    "MorphoTokenEthereumHarness"
   ],
   "solc": "solc-0.8.27",
   "verify": "MorphoTokenEthereumHarness:certora/specs/Delegation.spec",

certora/confs/MintBurnEthereum.conf

@@ -0,0 +1,18 @@
+{
+  "files": [
+    "certora/helpers/MorphoTokenEthereumHarness.sol"
+  ],
+  "parametric_contracts": [
+    "MorphoTokenEthereumHarness"
+  ],
+  "solc": "solc-0.8.27",
+  "verify": "MorphoTokenEthereumHarness:certora/specs/MintBurnEthereum.spec",
+  "packages": [
+    "@openzeppelin/contracts/=lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/contracts"
+  ],
+  "loop_iter": "3",
+  "optimistic_loop": true,
+  "rule_sanity": "basic",
+  "server": "production",
+  "msg": "Morpho Token Ethereum ERC20 mint and burn"
+}

certora/confs/MintBurnOptimism.conf

@@ -0,0 +1,18 @@
+{
+  "files": [
+    "certora/helpers/MorphoTokenOptimismHarness.sol"
+  ],
+  "parametric_contracts": [
+    "MorphoTokenOptimismHarness"
+  ],
+  "solc": "solc-0.8.27",
+  "verify": "MorphoTokenOptimismHarness:certora/specs/MintBurnOptimism.spec",
+  "packages": [
+    "@openzeppelin/contracts/=lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/contracts"
+  ],
+  "loop_iter": "3",
+  "optimistic_loop": true,
+  "rule_sanity": "basic",
+  "server": "production",
+  "msg": "Morpho Token Optimism ERC20 mint and burn"
+}

certora/specs/ERC20Invariants.spec

@@ -126,18 +126,17 @@ invariant balancesLTEqTotalSupply()
         }
     }
 
-rule twoBalancesCannotExceedTotalSupply(address accountA, address accountB) {
-    requireInvariant sumOfBalancesStartsAtZero();
-    requireInvariant sumOfBalancesGrowsCorrectly();
-    requireInvariant sumOfBalancesMonotone();
-    requireInvariant totalSupplyIsSumOfBalances();
-    uint256 balanceA = balanceOf(accountA);
-    uint256 balanceB = balanceOf(accountB);
-
-    assert accountA != accountB =>
-        balanceA + balanceB <= to_mathint(totalSupply());
-    satisfy(accountA != accountB && balanceA > 0 && balanceB > 0);
-}
+invariant twoBalancesLTEqTotalSupply()
+    forall address a. forall address b. a != b => ghostBalances[a] + ghostBalances[b] <= sumOfBalances[2^160]
+    {
+        preserved {
+            requireInvariant balancesLTEqTotalSupply();
+            requireInvariant sumOfBalancesStartsAtZero();
+            requireInvariant sumOfBalancesGrowsCorrectly();
+            requireInvariant sumOfBalancesMonotone();
+            requireInvariant totalSupplyIsSumOfBalances();
+        }
+    }
 
 // Check that zero address's balance is equal to zero.
 invariant zeroAddressNoBalance()

certora/specs/MintBurnEthereum.spec

@@ -0,0 +1,130 @@
+import "Delegation.spec";
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rules: only the token holder or an approved third party can reduce an account's balance                             │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule onlyAuthorizedCanTransfer(env e, method f) {
+    requireInvariant totalSupplyIsSumOfBalances();
+    requireInvariant balancesLTEqTotalSupply();
+    requireInvariant twoBalancesLTEqTotalSupply();
+
+    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
+    ) => (
+        e.msg.sender == account ||
+        f.selector == sig:transferFrom(address, address, uint256).selector && balanceBefore - balanceAfter <= to_mathint(allowanceBefore)
+    );
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rules: only mint and burn can change total supply                                                                   │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule noChangeTotalSupply(env e, method f) {
+    requireInvariant totalSupplyIsSumOfBalances();
+    requireInvariant balancesLTEqTotalSupply();
+
+    calldataarg args;
+
+    uint256 totalSupplyBefore = totalSupply();
+    f(e, args);
+    uint256 totalSupplyAfter = totalSupply();
+
+    assert totalSupplyAfter > totalSupplyBefore => f.selector == sig:mint(address,uint256).selector || f.selector == sig:initialize(address, address).selector;
+    assert totalSupplyAfter < totalSupplyBefore => f.selector == sig:burn(uint256).selector;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rules: mint behavior and side effects                                                                               │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule mint(env e) {
+    requireInvariant totalSupplyIsSumOfBalances();
+    requireInvariant balancesLTEqTotalSupply();
+    assert isTotalSupplyGTEqSumOfVotingPower();
+    requireInvariant zeroAddressNoVotingPower();
+    require nonpayable(e);
+
+    address to;
+    address other;
+    uint256 amount;
+
+    // cache state
+    uint256 toBalanceBefore    = balanceOf(to);
+    uint256 toVotingPowerBefore = delegatedVotingPower(delegatee(to));
+    uint256 otherBalanceBefore = balanceOf(other);
+    uint256 totalSupplyBefore  = totalSupply();
+
+    // Safe require thats avoid absurd counter-examples.
+    require toVotingPowerBefore <= sumOfVotingPower;
+
+    // run transaction
+    mint@withrevert(e, to, amount);
+
+    // check outcome
+    if (lastReverted) {
+        assert e.msg.sender != owner() || to == 0 || totalSupplyBefore + amount > max_uint256 ||
+            toVotingPowerBefore + amount > max_uint256;
+    } else {
+        // updates balance and totalSupply
+        assert e.msg.sender == owner();
+        assert to_mathint(balanceOf(to)) == toBalanceBefore   + amount;
+        assert to_mathint(totalSupply()) == totalSupplyBefore + amount;
+
+        // no other balance is modified
+        assert balanceOf(other) != otherBalanceBefore => other == to;
+    }
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rules: burn behavior and side effects                                                                               │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule burn(env e) {
+    requireInvariant balancesLTEqTotalSupply();
+    assert isTotalSupplyGTEqSumOfVotingPower();
+    requireInvariant zeroAddressNoVotingPower();
+    require nonpayable(e);
+
+    address from;
+    address other;
+    uint256 amount;
+    require from == e.msg.sender;
+    // cache state
+    uint256 fromBalanceBefore  = balanceOf(from);
+    uint256 fromVotingPowerBefore = delegatedVotingPower(delegatee(from));
+    uint256 toVotingPowerBefore = delegatedVotingPower(delegatee(0x0));
+    uint256 otherBalanceBefore = balanceOf(other);
+    uint256 totalSupplyBefore  = totalSupply();
+
+    // Safe require that avoids absurd counter-examples.
+    require fromVotingPowerBefore <= sumOfVotingPower;
+
+    // run transaction
+    burn@withrevert(e, amount);
+
+    // check outcome
+    if (lastReverted) {
+        assert e.msg.sender == 0x0 ||  fromBalanceBefore < amount || fromVotingPowerBefore < amount ;
+    } else {
+        // updates balance and totalSupply
+        assert to_mathint(balanceOf(from)) == fromBalanceBefore - amount;
+        assert to_mathint(totalSupply())   == totalSupplyBefore - amount;
+
+        // no other balance is modified
+        assert balanceOf(other) != otherBalanceBefore => other == from;
+    }
+}

certora/specs/MintBurnOptimism.spec

@@ -0,0 +1,132 @@
+import "Delegation.spec";
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rules: only the token holder or an approved third party can reduce an account's balance                             │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule onlyAuthorizedCanTransfer(env e, method f) {
+    requireInvariant totalSupplyIsSumOfBalances();
+    requireInvariant balancesLTEqTotalSupply();
+    requireInvariant twoBalancesLTEqTotalSupply();
+
+    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 == sig:burn(address, uint256).selector ||
+        e.msg.sender == account ||
+        f.selector == sig:transferFrom(address, address, uint256).selector && balanceBefore - balanceAfter <= to_mathint(allowanceBefore)
+    );
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rules: only mint and burn can change total supply                                                                   │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule noChangeTotalSupply(env e, method f) {
+    requireInvariant totalSupplyIsSumOfBalances();
+    requireInvariant balancesLTEqTotalSupply();
+
+    calldataarg args;
+
+    uint256 totalSupplyBefore = totalSupply();
+    f(e, args);
+    uint256 totalSupplyAfter = totalSupply();
+
+    assert totalSupplyAfter > totalSupplyBefore => f.selector == sig:mint(address, uint256).selector;
+    assert totalSupplyAfter < totalSupplyBefore => f.selector == sig:burn(address, uint256).selector;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rules: mint behavior and side effects                                                                               │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule mint(env e) {
+    requireInvariant totalSupplyIsSumOfBalances();
+    requireInvariant balancesLTEqTotalSupply();
+    assert isTotalSupplyGTEqSumOfVotingPower();
+    requireInvariant zeroAddressNoVotingPower();
+    require nonpayable(e);
+
+    address to;
+    address other;
+    uint256 amount;
+
+    // cache state
+    uint256 toBalanceBefore    = balanceOf(to);
+    uint256 toVotingPowerBefore = delegatedVotingPower(delegatee(to));
+    uint256 otherBalanceBefore = balanceOf(other);
+    uint256 totalSupplyBefore  = totalSupply();
+
+    // Safe require that avoids absurd counter-examples.
+    require toVotingPowerBefore <= sumOfVotingPower;
+
+    // run transaction
+    mint@withrevert(e, to, amount);
+
+    // check outcome
+    if (lastReverted) {
+        assert e.msg.sender != owner() || to == 0 || totalSupplyBefore + amount > max_uint256 ||
+            toVotingPowerBefore + amount > max_uint256 || e.msg.sender != currentContract.bridge;
+    } else {
+        // updates balance and totalSupply
+        assert e.msg.sender == currentContract.bridge;
+        assert to_mathint(balanceOf(to)) == toBalanceBefore   + amount;
+        assert to_mathint(totalSupply()) == totalSupplyBefore + amount;
+
+        // no other balance is modified
+        assert balanceOf(other) != otherBalanceBefore => other == to;
+    }
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rules: burn behavior and side effects                                                                               │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule burn(env e) {
+    requireInvariant balancesLTEqTotalSupply();
+    assert isTotalSupplyGTEqSumOfVotingPower();
+    requireInvariant zeroAddressNoVotingPower();
+    require nonpayable(e);
+
+    address from;
+    address other;
+    uint256 amount;
+    require from == e.msg.sender;
+    // cache state
+    uint256 fromBalanceBefore  = balanceOf(from);
+    uint256 fromVotingPowerBefore = delegatedVotingPower(delegatee(from));
+    uint256 toVotingPowerBefore = delegatedVotingPower(delegatee(0x0));
+    uint256 otherBalanceBefore = balanceOf(other);
+    uint256 totalSupplyBefore  = totalSupply();
+
+    // Safe require that avoids absurd counter-examples.
+    require fromVotingPowerBefore <= sumOfVotingPower;
+
+    // run transaction
+    burn@withrevert(e, from,  amount);
+
+    // check outcome
+    if (lastReverted) {
+           assert e.msg.sender == 0x0 ||  fromBalanceBefore < amount || fromVotingPowerBefore < amount
+               || e.msg.sender != currentContract.bridge;
+    } else {
+        // updates balance and totalSupply
+        assert to_mathint(balanceOf(from)) == fromBalanceBefore - amount;
+        assert to_mathint(totalSupply())   == totalSupplyBefore - amount;
+
+        // no other balance is modified
+        assert balanceOf(other) != otherBalanceBefore => other == from;
+    }
+}