[Certora] Delegation invariant

.github/workflows/certora.yml

@@ -18,7 +18,9 @@ jobs:
         conf:
           - DelegationEthereum
           - DelegationOptimism
+          - ERC20InvariantsEthereum
           - ERC20Ethereum
+          - ERC20InvariantsOptimism
           - ERC20Optimism
           - ExternalCallsEthereum
           - ExternalCallsOptimism

certora/README.md

@@ -30,9 +30,9 @@ Note: the compiled contracts may include loops related to handling strings from
 
 This is checked in [`ExternalCalls.spec`](specs/ExternalCalls.spec).
 
-### ERC20 Compliance
+### ERC20 Compliance and Correctness
 
-This is checked in [`ERC20.spec`](specs/ERC20.spec).
+This is checked in [`ERC20.spec`](specs/ERC20.spec) and [`ERC20Invariants.spec`](specs/ERC20Invariants.spec) .
 
 ### Delegation Correctness
 
@@ -45,6 +45,7 @@ This is checked in [`Delegation.spec`](specs/Delegation.spec).
 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;
 - [`Delegation.spec`](specs/Delegation.spec) checks the logic for voting power delegation.
 

certora/confs/ERC20InvariantsEthereum.conf

@@ -0,0 +1,18 @@
+{
+  "files": [
+    "src/MorphoTokenEthereum.sol"
+  ],
+  "parametric_contracts": [
+    "MorphoTokenEthereum"
+  ],
+  "solc": "solc-0.8.27",
+  "verify": "MorphoTokenEthereum:certora/specs/ERC20Invariants.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"
+}

certora/confs/ERC20InvariantsOptimism.conf

@@ -0,0 +1,18 @@
+{
+  "files": [
+    "src/MorphoTokenOptimism.sol"
+  ],
+  "parametric_contracts": [
+    "MorphoTokenOptimism"
+  ],
+  "solc": "solc-0.8.27",
+  "verify": "MorphoTokenOptimism:certora/specs/ERC20Invariants.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"
+}

certora/specs/Delegation.spec

@@ -1,24 +1,101 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
 import "ERC20.spec";
 
 methods {
     function delegatorFromSig(DelegationToken.Delegation, DelegationToken.Signature) external returns address envfree;
     function delegationNonce(address) external returns uint256 envfree;
 }
 
+// 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;
 }
 
-// Slot for DelegationTokenStorage._delegatedVotingPower
-hook Sstore (slot 0x669be2f4ee1b0b5f3858e4135f31064efe8fa923b09bf21bf538f64f2c3e1101)[KEY address addr] uint256 newValue (uint256 oldValue) {
-    sumOfVotingPower = sumOfVotingPower - oldValue + newValue;
+// Ghost copy of DelegationTokenStorage._delegatedVotingPower.
+ghost mapping(address => uint256) ghostDelegatedVotingPower {
+    init_state axiom forall address account. ghostDelegatedVotingPower[account] == 0;
+}
+
+hook Sload uint256 votingPower (slot 0x669be2f4ee1b0b5f3858e4135f31064efe8fa923b09bf21bf538f64f2c3e1101)[KEY address account] {
+    require ghostDelegatedVotingPower[account] == votingPower;
+}
+
+// Slot is DelegationTokenStorage._delegatedVotingPower.
+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;
 }
 
 // Check that zero address has no voting power assuming that zero address can't make transactions.
 invariant zeroAddressNoVotingPower()
     delegatee(0x0) == 0x0 && delegatedVotingPower(0x0) == 0
     { preserved with (env e) { require e.msg.sender != 0; } }
 
+// Check that initially zero votes are delegated to parameterized address A.
+invariant sumOfVotesStartsAtZero()
+    sumsOfVotesDelegatedToA[0] == 0;
+
+invariant sumOfVotesGrowsCorrectly()
+    forall address account. sumsOfVotesDelegatedToA[to_mathint(account) + 1] ==
+    sumsOfVotesDelegatedToA[to_mathint(account)] + (ghostDelegatee[account] == A ? ghostBalances[account] : 0) ;
+
+invariant sumOfVotesMonotone()
+    forall mathint i. forall mathint j. i <= j => sumsOfVotesDelegatedToA[i] <= sumsOfVotesDelegatedToA[j]
+    {
+        preserved {
+            requireInvariant sumOfVotesStartsAtZero();
+            requireInvariant sumOfVotesGrowsCorrectly();
+        }
+    }
+
+invariant delegatedLTEqPartialSum()
+    forall address account. ghostDelegatee[account] == A =>
+      ghostBalances[account] <= sumsOfVotesDelegatedToA[to_mathint(account)+1]
+    {
+        preserved {
+            requireInvariant sumOfVotesStartsAtZero();
+            requireInvariant sumOfVotesGrowsCorrectly();
+            requireInvariant sumOfVotesMonotone();
+        }
+    }
+
+
+invariant sumOfVotesIsDelegatedToA()
+    sumsOfVotesDelegatedToA[2^160] == ghostDelegatedVotingPower[A]
+    {
+        preserved {
+            requireInvariant zeroAddressNoVotingPower();
+            requireInvariant sumOfVotesStartsAtZero();
+            requireInvariant sumOfVotesGrowsCorrectly();
+            requireInvariant sumOfVotesMonotone();
+        }
+    }
+
+invariant delegatedLTEqDelegateeVP()
+    forall address account.
+      ghostDelegatee[account] == A =>
+      ghostBalances[account] <= ghostDelegatedVotingPower[A]
+    {
+        preserved with (env e){
+            requireInvariant zeroAddressNoVotingPower();
+            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
@@ -36,6 +113,7 @@ invariant totalSupplyIsSumOfVirtualVotingPower()
         preserved {
             requireInvariant totalSupplyIsSumOfBalances();
             requireInvariant zeroAddressNoVotingPower();
+            requireInvariant balancesLTEqTotalSupply();
         }
     }
 

certora/specs/ERC20.spec

@@ -1,41 +1,19 @@
 // This is spec is taken from the Open Zeppelin repositories at https://github.com/OpenZeppelin/openzeppelin-contracts/blob/448efeea6640bbbc09373f03fbc9c88e280147ba/certora/specs/ERC20.spec, and patched to support the DelegationToken.
 // Note: the scope of this specification encompases only the implementation contract and not the interactions with the implementation contract and the proxy.
 
+import "ERC20Invariants.spec";
+
 definition nonpayable(env e) returns bool = e.msg.value == 0;
 definition nonzerosender(env e) returns bool = e.msg.sender != 0;
 
 methods {
     function name()                                external returns (string)  envfree;
     function symbol()                              external returns (string)  envfree;
     function decimals()                            external returns (uint8)   envfree;
-    function totalSupply()                         external returns (uint256) envfree;
-    function balanceOf(address)                    external returns (uint256) envfree;
     function allowance(address,address)            external returns (uint256) envfree;
     function owner()                               external returns address   envfree;
-    function delegatedVotingPower(address)         external returns uint256   envfree;
-    function delegatee(address)                    external returns address   envfree;
     function nonces(address)                       external returns (uint256) envfree;
     function DOMAIN_SEPARATOR()                    external returns (bytes32) envfree;
-    function upgradeToAndCall(address, bytes)      external => NONDET DELETE;
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Ghost & hooks: sum of all balances                                                                                  │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-ghost mathint sumOfBalances {
-    init_state axiom sumOfBalances == 0;
-}
-
-// Slot is ERC20Storage._balances slot
-hook Sload uint256 balance (slot 0x52c63247e1f47db19d5ce0460030c497f067ca4cebf71ba98eeadabe20bace00)[KEY address addr] {
-   require sumOfBalances >= to_mathint(balance);
-}
-
-// Slot is ERC20Storage._balances slot
-hook Sstore (slot 0x52c63247e1f47db19d5ce0460030c497f067ca4cebf71ba98eeadabe20bace00)[KEY address addr] uint256 newValue (uint256 oldValue) {
-   sumOfBalances = sumOfBalances - oldValue + newValue;
 }
 
 /*
@@ -44,18 +22,15 @@ hook Sstore (slot 0x52c63247e1f47db19d5ce0460030c497f067ca4cebf71ba98eeadabe20ba
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 
-invariant totalSupplyIsSumOfBalances()
-    to_mathint(totalSupply()) == sumOfBalances;
-
+use invariant totalSupplyIsSumOfBalances;
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
 │ Invariant: balance of address(0) is 0                                                                               │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 
-invariant zeroAddressNoBalance()
-    balanceOf(0) == 0;
+use invariant zeroAddressNoBalance;
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
@@ -98,6 +73,7 @@ rule transfer(env e) {
     requireInvariant totalSupplyIsSumOfBalances();
     require nonpayable(e);
 
+
     address holder = e.msg.sender;
     address recipient;
     address other;
@@ -110,6 +86,9 @@ rule transfer(env e) {
     uint256 recipientVotingPowerBefore = delegatedVotingPower(delegatee(recipient));
     uint256 otherBalanceBefore     = balanceOf(other);
 
+    // Safe require as it's proven by the rule twoBalancesCannotExceedTotalSupply.
+    require holder != recipient => balanceOf(holder) + balanceOf(recipient) <= totalSupply();
+
     // run transaction
     transfer@withrevert(e, recipient, amount);
 
@@ -151,6 +130,9 @@ rule transferFrom(env e) {
     uint256 recipientVotingPowerBefore = delegatedVotingPower(delegatee(recipient));
     uint256 otherBalanceBefore     = balanceOf(other);
 
+    // Safe require as it's proven by the rule twoBalancesCannotExceedTotalSupply.
+    require holder != recipient => balanceOf(holder) + balanceOf(recipient) <= totalSupply();
+
     // run transaction
     transferFrom@withrevert(e, holder, recipient, amount);