Merge branch 'main' into colin@verif/mint-burn

.github/workflows/certora.yml

@@ -26,6 +26,10 @@ jobs:
           - ExternalCallsOptimism
           - MintBurnEthereum
           - MintBurnOptimism
+          - RevertsERC20Ethereum
+          - RevertsERC20Optimism
+          - RevertsMintBurnEthereum
+          - RevertsMintBurnOptimism
 
     steps:
       - uses: actions/checkout@v4

certora/README.md

@@ -38,6 +38,10 @@ This is checked in [`ERC20.spec`](specs/ERC20.spec), [`ERC20Invariants.spec`](sp
 
 This is checked in [`Delegation.spec`](specs/Delegation.spec).
 
+### Reverts
+
+This is checks in [`RevertsERC20.spec`](specs/RevertsERC20.spec), [`RevertsMintBurnEthereum.spec`](specs/RevertsMintBurnEthereum.spec) and [`RevertsMintBurnOptimism.spec`](specs/RevertsMintBurnOptimism.spec).
+
 ## Verification architecture
 
 ### Folders and file structure
@@ -48,6 +52,7 @@ The [`certora/specs`](specs) folder contains the following files:
 - [`ERC20Invariants.spec`](specs/ERC20Invariants.spec) common hooks and invariants to be shared in different specs;
 - [`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.
+- [`RevertsERC20.spec`](specs/RevertsERC20.spec), [`RevertsMintBurnEthereum.spec`](specs/RevertsMintBurnEthereum.spec) and [`RevertsMintBurnOptimism.spec`](specs/RevertsMintBurnOptimism.spec) check that conditions for reverts and inputs are correctly validated.
 
 The [`certora/confs`](confs) folder contains a configuration file for each corresponding specification file for both the Ethereum and the Optimism version.
 

certora/confs/RevertsERC20Ethereum.conf

@@ -0,0 +1,18 @@
+{
+  "files": [
+    "src/MorphoTokenEthereum.sol"
+  ],
+  "parametric_contracts": [
+    "MorphoTokenEthereum"
+  ],
+  "solc": "solc-0.8.27",
+  "verify": "MorphoTokenEthereum:certora/specs/RevertsERC20.spec",
+  "rule_sanity": "basic",
+  "server": "production",
+  "packages": [
+    "@openzeppelin/contracts/=lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/contracts"
+  ],
+  "loop_iter": "3",
+  "optimistic_loop": true,
+  "msg": "Morpho token ERC20 Reverts Ethereum"
+}

certora/confs/RevertsERC20Optimism.conf

@@ -0,0 +1,18 @@
+{
+  "files": [
+    "src/MorphoTokenOptimism.sol"
+  ],
+  "parametric_contracts": [
+    "MorphoTokenOptimism"
+  ],
+  "solc": "solc-0.8.27",
+  "verify": "MorphoTokenOptimism:certora/specs/RevertsERC20.spec",
+  "rule_sanity": "basic",
+  "server": "production",
+  "packages": [
+    "@openzeppelin/contracts/=lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/contracts"
+  ],
+  "loop_iter": "3",
+  "optimistic_loop": true,
+  "msg": "Morpho token ERC20 Reverts Optimism"
+}

certora/confs/RevertsMintBurnEthereum.conf

@@ -0,0 +1,18 @@
+{
+  "files": [
+    "src/MorphoTokenEthereum.sol"
+  ],
+  "parametric_contracts": [
+    "MorphoTokenEthereum"
+  ],
+  "solc": "solc-0.8.27",
+  "verify": "MorphoTokenEthereum:certora/specs/RevertsMintBurnEthereum.spec",
+  "rule_sanity": "basic",
+  "server": "production",
+  "packages": [
+    "@openzeppelin/contracts/=lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/contracts"
+  ],
+  "loop_iter": "3",
+  "optimistic_loop": true,
+  "msg": "Morpho token ERC20 Mint Burn Reverts"
+}

certora/confs/RevertsMintBurnOptimism.conf

@@ -0,0 +1,18 @@
+{
+  "files": [
+    "src/MorphoTokenOptimism.sol"
+  ],
+  "parametric_contracts": [
+    "MorphoTokenOptimism"
+  ],
+  "solc": "solc-0.8.27",
+  "verify": "MorphoTokenOptimism:certora/specs/RevertsMintBurnOptimism.spec",
+  "rule_sanity": "basic",
+  "server": "production",
+  "packages": [
+    "@openzeppelin/contracts/=lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/contracts"
+  ],
+  "loop_iter": "3",
+  "optimistic_loop": true,
+  "msg": "Morpho token ERC20 Mint Burn Reverts"
+}

certora/specs/Delegation.spec

@@ -7,16 +7,14 @@ methods {
 }
 
 // Ghost variable to hold the sum of voting power.
-// To reason exhaustively on the value of of delegated voting power we proceed to compute the partial sum of balances for each possible address.
-// We call the partial sum of votes to parameter A up to an addrress a, to sum of delegated votes to parameter A for all addresses within the range [0..a[.
-// Formally, we write ∀ a:address, sumsOfVotesDelegatedToA[a] = Σ balanceOf(i), where the sum ranges over addresses i such that i < a and delegatee(i) = A, provided that the address zero holds no voting power and that it never performs transactions.
-// With this approach, we are able to write and check more abstract properties about the computation of the total delegated voting power using universal quantifiers.
-// From this follows the property such that, ∀ a:address, delegatee(a) = A ⇒ balanceOf(a) ≤ delegatedVotingPower(A).
-// In particular, we have the equality sumsOfVotesDelegatedToA[2^160] = delegatedVotingPower(A).
-// Finally, we reason by parametricity to observe since we have ∀ a:address, delegatee(a) = A ⇒ balanceOf(a) ≤ delegatedVotingPower(A).
-// We also have ∀ A:address, ∀ a:address, A ≠ 0 ∧ delegatee(a) = A ⇒ balanceOf(a) ≤ delegatedVotingPower(A), which is what we want to show.
-ghost mathint sumOfVotingPower {
-    init_state axiom sumOfVotingPower == 0;
+// To reason exhaustively on the value of the sum of voting power we proceed to compute the partial sum of voting power for each possible address.
+// We call the partial sum of balances up to an addrress a, to sum of balances for all addresses within the range [0..a[.
+// Formally, we write ∀ a:address, sumOfVotes[a] = Σ delegatedVotingPower(i) where the sum ranges over addresses i < a, provided that the address zero holds no token and that it never performs transactions.
+// With this approach, we are able to write and check more abstract properties about the computation of the total voting power using universal quantifiers.
+// From this follows the property such that, ∀ a:address, delegatedVotingpower(a) ≤ total sum of votes.
+// In particular, we are able to to show that the sum voting powers of two different accounts is lesser than or equal to the total sum of votes.
+ghost mapping (mathint => mathint) sumOfVotes {
+    init_state axiom forall mathint account. sumOfVotes[account] == 0;
 }
 
 // Ghost copy of DelegationTokenStorage._delegatedVotingPower.
@@ -32,8 +30,10 @@ hook Sload uint256 votingPower (slot 0x669be2f4ee1b0b5f3858e4135f31064efe8fa923b
 hook Sstore (slot 0x669be2f4ee1b0b5f3858e4135f31064efe8fa923b09bf21bf538f64f2c3e1101)[KEY address account] uint256 votingPower (uint256 votingPowerOld) {
     // Update DelegationTokenStorage._delegatedVotingPower
     ghostDelegatedVotingPower[account] = votingPower;
-    // Track changes of total voting power.
-    sumOfVotingPower = sumOfVotingPower - votingPowerOld + votingPower;
+    // Track balance changes in sum of votes.
+    havoc sumOfVotes assuming
+        forall mathint x. sumOfVotes@new[x] ==
+            sumOfVotes@old[x] + (to_mathint(account) < x ? votingPower - votingPowerOld : 0);
 }
 
 // Check that zero address has no voting power assuming that zero address can't make transactions.
@@ -42,19 +42,19 @@ invariant zeroAddressNoVotingPower()
     { preserved with (env e) { require e.msg.sender != 0; } }
 
 // Check that initially zero votes are delegated to parameterized address A.
-invariant sumOfVotesStartsAtZero()
+invariant sumOfVotesDelegatedToAStartsAtZero()
     sumsOfVotesDelegatedToA[0] == 0;
 
-invariant sumOfVotesGrowsCorrectly()
+invariant sumOfVotesDelegatedToAGrowsCorrectly()
     forall address account. sumsOfVotesDelegatedToA[to_mathint(account) + 1] ==
     sumsOfVotesDelegatedToA[to_mathint(account)] + (ghostDelegatee[account] == A ? ghostBalances[account] : 0) ;
 
-invariant sumOfVotesMonotone()
+invariant sumOfVotesDelegatedToAMonotone()
     forall mathint i. forall mathint j. i <= j => sumsOfVotesDelegatedToA[i] <= sumsOfVotesDelegatedToA[j]
     {
         preserved {
-            requireInvariant sumOfVotesStartsAtZero();
-            requireInvariant sumOfVotesGrowsCorrectly();
+            requireInvariant sumOfVotesDelegatedToAStartsAtZero();
+            requireInvariant sumOfVotesDelegatedToAGrowsCorrectly();
         }
     }
 
@@ -63,21 +63,21 @@ invariant delegatedLTEqPartialSum()
       ghostBalances[account] <= sumsOfVotesDelegatedToA[to_mathint(account)+1]
     {
         preserved {
-            requireInvariant sumOfVotesStartsAtZero();
-            requireInvariant sumOfVotesGrowsCorrectly();
-            requireInvariant sumOfVotesMonotone();
+            requireInvariant sumOfVotesDelegatedToAStartsAtZero();
+            requireInvariant sumOfVotesDelegatedToAGrowsCorrectly();
+            requireInvariant sumOfVotesDelegatedToAMonotone();
         }
     }
 
 
-invariant sumOfVotesIsDelegatedToA()
+invariant sumOfVotesDelegatedToAIsDelegatedToA()
     sumsOfVotesDelegatedToA[2^160] == ghostDelegatedVotingPower[A]
     {
         preserved {
             requireInvariant zeroAddressNoVotingPower();
-            requireInvariant sumOfVotesStartsAtZero();
-            requireInvariant sumOfVotesGrowsCorrectly();
-            requireInvariant sumOfVotesMonotone();
+            requireInvariant sumOfVotesDelegatedToAStartsAtZero();
+            requireInvariant sumOfVotesDelegatedToAGrowsCorrectly();
+            requireInvariant sumOfVotesDelegatedToAMonotone();
         }
     }
 
@@ -88,38 +88,81 @@ invariant delegatedLTEqDelegateeVP()
     {
         preserved with (env e){
             requireInvariant zeroAddressNoVotingPower();
+            requireInvariant sumOfVotesDelegatedToAStartsAtZero();
+            requireInvariant sumOfVotesDelegatedToAGrowsCorrectly();
+            requireInvariant sumOfVotesDelegatedToAMonotone();
+            requireInvariant delegatedLTEqPartialSum();
+            requireInvariant sumOfVotesDelegatedToAIsDelegatedToA();
+        }
+    }
+
+invariant sumOfVotesStartsAtZero()
+    sumOfVotes[0] == 0;
+
+invariant sumOfVotesGrowsCorrectly()
+    forall address addr. sumOfVotes[to_mathint(addr) + 1] ==
+      sumOfVotes[to_mathint(addr)] + ghostDelegatedVotingPower[addr];
+
+invariant sumOfVotesMonotone()
+    forall mathint i. forall mathint j. i <= j => sumOfVotes[i] <= sumOfVotes[j]
+    {
+        preserved {
             requireInvariant sumOfVotesStartsAtZero();
             requireInvariant sumOfVotesGrowsCorrectly();
-            requireInvariant sumOfVotesMonotone();
-            requireInvariant delegatedLTEqPartialSum();
-            requireInvariant sumOfVotesIsDelegatedToA();
         }
     }
 
 // Check that the voting power plus the virtual voting power of address zero is equal to the total supply of tokens.
 invariant totalSupplyIsSumOfVirtualVotingPower()
-    to_mathint(totalSupply()) == sumOfVotingPower + currentContract._zeroVirtualVotingPower
+    sumOfVotes[2^160] + currentContract._zeroVirtualVotingPower == to_mathint(totalSupply())
     {
+        preserved {
+            requireInvariant sumOfBalancesStartsAtZero();
+            requireInvariant sumOfBalancesGrowsCorrectly();
+            requireInvariant sumOfBalancesMonotone();
+            requireInvariant totalSupplyIsSumOfBalances();
+            requireInvariant zeroAddressNoVotingPower();
+            requireInvariant balancesLTEqTotalSupply();
+
+        }
         preserved MorphoTokenOptimismHarness.initialize(address _) with (env e) {
-            // Safe requires because the proxy contract should be initialized right after construction.
+            // Safe require because the proxy contract should be initialized right after construction.
             require totalSupply() == 0;
-            require sumOfVotingPower == 0;
         }
         preserved MorphoTokenEthereumHarness.initialize(address _, address _) with (env e) {
             // Safe requires because the proxy contract should be initialized right after construction.
             require totalSupply() == 0;
-            require sumOfVotingPower == 0;
+            require forall mathint account. sumOfVotes[account] == 0;
         }
+    }
+
+invariant delegatedVotingPowerLTEqTotalVotingPower()
+    forall address a. ghostDelegatedVotingPower[a] <= sumOfVotes[2^160]
+    {
         preserved {
-            requireInvariant totalSupplyIsSumOfBalances();
-            requireInvariant zeroAddressNoVotingPower();
-            requireInvariant balancesLTEqTotalSupply();
+            requireInvariant sumOfVotesStartsAtZero();
+            requireInvariant sumOfVotesGrowsCorrectly();
+            requireInvariant sumOfVotesMonotone();
+            requireInvariant totalSupplyIsSumOfVirtualVotingPower();
+        }
+    }
+
+invariant sumOfTwoDelegatedVPLTEqTotalVP()
+    forall address a. forall address b. a != b => ghostDelegatedVotingPower[a] + ghostDelegatedVotingPower[b] <= sumOfVotes[2^160]
+    {
+        preserved {
+            requireInvariant delegatedVotingPowerLTEqTotalVotingPower();
+            requireInvariant sumOfVotesStartsAtZero();
+            requireInvariant sumOfVotesGrowsCorrectly();
+            requireInvariant sumOfVotesMonotone();
+            requireInvariant totalSupplyIsSumOfVirtualVotingPower();
         }
     }
 
+
 function isTotalSupplyGTEqSumOfVotingPower() returns bool {
     requireInvariant totalSupplyIsSumOfVirtualVotingPower();
-    return totalSupply() >= sumOfVotingPower;
+    return totalSupply() >= sumOfVotes[2^160];
 }
 
 // Check that the total supply of tokens is greater than or equal to the sum of voting power.

certora/specs/ERC20Invariants.spec

@@ -13,7 +13,16 @@ persistent ghost address A {
     axiom A != 0;
 }
 
-// Partial sum of delegated votes to parameterized address A.
+// Ghost variable to hold the sum of delegated votes to parameterized address A.
+// To reason exhaustively on the value of of delegated voting power we proceed to compute the partial sum of delegated votes to parameter A for each possible address.
+// We call the partial sum of votes to parameter A up to an addrress a, to sum of delegated votes to parameter A for all addresses within the range [0..a[.
+// Formally, we write ∀ a:address, sumsOfVotesDelegatedToA[a] = Σ balanceOf(i), where the sum ranges over addresses i such that i < a and delegatee(i) = A, provided that the address zero holds no voting power and that it never performs transactions.
+// With this approach, we are able to write and check more abstract properties about the computation of the total delegated voting power using universal quantifiers.
+// From this follows the property such that, ∀ a:address, delegatee(a) = A ⇒ balanceOf(a) ≤ delegatedVotingPower(A).
+// In particular, we have the equality sumsOfVotesDelegatedToA[2^160] = delegatedVotingPower(A).
+// Finally, we reason by parametricity to observe since we have ∀ a:address, delegatee(a) = A ⇒ balanceOf(a) ≤ delegatedVotingPower(A).
+// We also have ∀ A:address, ∀ a:address, A ≠ 0 ∧ delegatee(a) = A ⇒ balanceOf(a) ≤ delegatedVotingPower(A), which is what we want to show.
+
 // sumOfvotes[x] = \sum_{i=0}^{x-1} balances[i] when delegatee[i] == A;
 ghost mapping(mathint => mathint) sumsOfVotesDelegatedToA {
     init_state axiom forall mathint account. sumsOfVotesDelegatedToA[account] == 0;

certora/specs/RevertsERC20.spec

@@ -0,0 +1,54 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+
+methods {
+    function totalSupply() external returns uint256 envfree;
+    function balanceOf(address) external returns uint256 envfree;
+    function allowance(address, address) external returns uint256 envfree;
+    function delegatee(address) external returns address envfree;
+    function delegatedVotingPower(address) external returns uint256 envfree;
+}
+
+// Check the revert conditions for the transfer function.
+rule transferRevertConditions(env e, address to, uint256 amount) {
+    uint256 balanceOfSenderBefore = balanceOf(e.msg.sender);
+    uint256 senderVotingPowerBefore = delegatedVotingPower(delegatee(e.msg.sender));
+    uint256 recipientVotingPowerBefore = delegatedVotingPower(delegatee(to));
+
+    // Safe require as it is verified in delegatedLTEqDelegateeVP.
+    require senderVotingPowerBefore >= balanceOfSenderBefore;
+    // Safe require that follows from sumOfTwoDelegatedVPLTEqTotalVP() and totalSupplyIsSumOfVirtualVotingPower().
+    require delegatee(to) != delegatee(e.msg.sender) => recipientVotingPowerBefore + senderVotingPowerBefore <= totalSupply();
+
+    transfer@withrevert(e, to, amount);
+    assert lastReverted <=> e.msg.sender == 0 || to == 0 || balanceOfSenderBefore < amount || e.msg.value != 0;
+}
+
+// Check the revert conditions for the transferFrom function.
+rule transferFromRevertConditions(env e, address from, address to, uint256 amount) {
+    uint256 allowanceOfSenderBefore = allowance(from, e.msg.sender);
+    uint256 balanceOfHolderBefore = balanceOf(from);
+    uint256 holderVotingPowerBefore = delegatedVotingPower(delegatee(from));
+    uint256 recipientVotingPowerBefore = delegatedVotingPower(delegatee(to));
+
+    // Safe require as it is verified in delegatedLTEqDelegateeVP.
+    require holderVotingPowerBefore >= balanceOfHolderBefore;
+    // Safe require that follows from sumOfTwoDelegatedVPLTEqTotalVP() and totalSupplyIsSumOfVirtualVotingPower().
+    require delegatee(to) != delegatee(from) => recipientVotingPowerBefore + holderVotingPowerBefore <= totalSupply();
+
+    transferFrom@withrevert(e, from, to, amount);
+
+    bool generalRevertConditions = from == 0 || to == 0 || balanceOfHolderBefore < amount || e.msg.value != 0;
+
+    if (allowanceOfSenderBefore != max_uint256) {
+        assert lastReverted <=>  e.msg.sender == 0 || allowanceOfSenderBefore < amount || generalRevertConditions;
+    } else {
+        assert lastReverted <=> generalRevertConditions;
+    }
+
+}
+
+// Check the revert conditions for the approve function.
+rule approveRevertConditions(env e, address to, uint256 value) {
+    approve@withrevert(e, to, value);
+    assert lastReverted <=> e.msg.sender == 0 || to == 0 || e.msg.value != 0;
+}