[Certora] Verify delegation correctness

.github/workflows/certora.yml

@@ -16,6 +16,8 @@ jobs:
 
       matrix:
         conf:
+          - DelegationEthereum
+          - DelegationOptimism
           - ERC20Ethereum
           - ERC20Optimism
           - ExternalCallsEthereum
@@ -40,6 +42,9 @@ jobs:
           chmod +x solc-static-linux
           sudo mv solc-static-linux /usr/local/bin/solc-0.8.27
 
+      - name: Apply munging
+        run: make -C certora munged
+
       - name: Verify ${{ matrix.conf }} specification
         run: certoraRun certora/confs/${{ matrix.conf }}.conf
         env:

certora/Makefile

@@ -0,0 +1,12 @@
+munged: $(wildcard ../src/*.sol) applyMunging.patch
+	@rm -rf munged
+	@cp -r ../src munged
+	@patch -p0 -d munged < applyMunging.patch
+
+record:
+	diff -ruN ../src munged | sed 's+\.\./src/++g' | sed 's+munged/++g' > applyMunging.patch
+
+clean:
+	rm -rf munged
+
+.PHONY: help clean # do not add munged here, as it is useful to protect munged edits

certora/README.md

@@ -4,6 +4,12 @@ This folder contains the [CVL](https://docs.certora.com/en/latest/docs/cvl/index
 
 ## Getting started
 
+The verification is performed on modified source files, which can generated with the command:
+
+```
+make -C certora munged
+```
+
 This project depends on [Solidity](https://soliditylang.org/) which is required for running the verification.
 The compiler binary should be available in the path:
 
@@ -28,14 +34,20 @@ This is checked in [`ExternalCalls.spec`](specs/ExternalCalls.spec).
 
 This is checked in [`ERC20.spec`](specs/ERC20.spec).
 
+### Delegation Correctness
+
+This is checked in [`Delegation.spec`](specs/Delegation.spec).
+
 ## Verification architecture
 
 ### Folders and file structure
 
 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;
-- [`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) 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.
 
 The [`certora/confs`](confs) folder contains a configuration file for each corresponding specification file for both the Ethereum and the Optimism version.
+
+The [`certora/Makefile`](Makefile) is used to track and perform the required modifications on source files.

certora/applyMunging.patch

@@ -0,0 +1,109 @@
+diff -ruN DelegationToken.sol DelegationToken.sol
+--- DelegationToken.sol	2024-11-06 18:57:11.000000000 +0100
++++ DelegationToken.sol	2024-11-08 16:22:14.000000000 +0100
+@@ -1,17 +1,17 @@
+ // SPDX-License-Identifier: GPL-2.0-or-later
+ pragma solidity ^0.8.27;
+
+-import {IDelegation, Signature, Delegation} from "./interfaces/IDelegation.sol";
++import {IDelegation, Signature, Delegation} from "../../src/interfaces/IDelegation.sol";
+
+ import {ERC20PermitUpgradeable} from
+-    "../lib/openzeppelin-contracts-upgradeable/contracts/token/ERC20/extensions/ERC20PermitUpgradeable.sol";
++    "../../lib/openzeppelin-contracts-upgradeable/contracts/token/ERC20/extensions/ERC20PermitUpgradeable.sol";
+ import {ECDSA} from
+-    "../lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/contracts/utils/cryptography/ECDSA.sol";
++    "../../lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/contracts/utils/cryptography/ECDSA.sol";
+ import {Ownable2StepUpgradeable} from
+-    "../lib/openzeppelin-contracts-upgradeable/contracts/access/Ownable2StepUpgradeable.sol";
+-import {UUPSUpgradeable} from "../lib/openzeppelin-contracts-upgradeable/contracts/proxy/utils/UUPSUpgradeable.sol";
++    "../../lib/openzeppelin-contracts-upgradeable/contracts/access/Ownable2StepUpgradeable.sol";
++import {UUPSUpgradeable} from "../../lib/openzeppelin-contracts-upgradeable/contracts/proxy/utils/UUPSUpgradeable.sol";
+ import {ERC1967Utils} from
+-    "../lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/contracts/proxy/ERC1967/ERC1967Utils.sol";
++    "../../lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/contracts/proxy/ERC1967/ERC1967Utils.sol";
+
+ /// @title DelegationToken
+ /// @author Morpho Association
+@@ -44,6 +44,9 @@
+         mapping(address => uint256) _delegationNonce;
+     }
+
++    // A ghost variable to track the theoretical voting power of address zero.
++    uint256 _zeroVirtualVotingPower = 0;
++
+     /* ERRORS */
+
+     /// @notice The signature used has expired.
+@@ -148,12 +151,16 @@
+                 uint256 newValue = oldValue - amount;
+                 $._delegatedVotingPower[from] = newValue;
+                 emit DelegatedVotingPowerChanged(from, oldValue, newValue);
++            } else {
++                _zeroVirtualVotingPower -= amount;
+             }
+             if (to != address(0)) {
+                 uint256 oldValue = $._delegatedVotingPower[to];
+                 uint256 newValue = oldValue + amount;
+                 $._delegatedVotingPower[to] = newValue;
+                 emit DelegatedVotingPowerChanged(to, oldValue, newValue);
++            } else {
++                _zeroVirtualVotingPower += amount;
+             }
+         }
+     }
+diff -ruN MorphoTokenEthereum.sol MorphoTokenEthereum.sol
+--- MorphoTokenEthereum.sol	2024-11-06 18:57:11.000000000 +0100
++++ MorphoTokenEthereum.sol	2024-11-08 16:34:08.000000000 +0100
+@@ -25,17 +25,20 @@
+         __ERC20_init(NAME, SYMBOL);
+         __ERC20Permit_init(NAME);
+         __Ownable_init(owner);
+-
++        require(totalSupply() == 0);
++        _zeroVirtualVotingPower = 1_000_000_000e18;
+         _mint(wrapper, 1_000_000_000e18); // Mint 1B to the wrapper contract.
+     }
+
+     /// @notice Mints tokens.
+     function mint(address to, uint256 amount) external onlyOwner {
++        _zeroVirtualVotingPower += amount;
+         _mint(to, amount);
+     }
+
+     /// @notice Burns sender's tokens.
+     function burn(uint256 amount) external {
+         _burn(_msgSender(), amount);
++        _zeroVirtualVotingPower -= amount;
+     }
+ }
+diff -ruN MorphoTokenOptimism.sol MorphoTokenOptimism.sol
+--- MorphoTokenOptimism.sol	2024-11-06 18:57:11.000000000 +0100
++++ MorphoTokenOptimism.sol	2024-11-08 16:33:51.000000000 +0100
+@@ -1,9 +1,9 @@
+ // SPDX-License-Identifier: GPL-2.0-or-later
+ pragma solidity 0.8.27;
+
+-import {IOptimismMintableERC20} from "./interfaces/IOptimismMintableERC20.sol";
++import {IOptimismMintableERC20} from "../../src/interfaces/IOptimismMintableERC20.sol";
+ import {IERC165} from
+-    "../lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/contracts/utils/introspection/IERC165.sol";
++    "../../lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/contracts/utils/introspection/IERC165.sol";
+
+ import {DelegationToken} from "./DelegationToken.sol";
+
+@@ -69,12 +69,14 @@
+
+     /// @dev Allows the StandardBridge on this network to mint tokens.
+     function mint(address to, uint256 amount) external onlyBridge {
++        _zeroVirtualVotingPower += amount;
+         _mint(to, amount);
+     }
+
+     /// @dev Allows the StandardBridge on this network to burn tokens.
+     function burn(address from, uint256 amount) external onlyBridge {
+         _burn(from, amount);
++        _zeroVirtualVotingPower -= amount;
+     }
+
+     /// @notice ERC165 interface check function.

certora/confs/DelegationEthereum.conf

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

certora/confs/DelegationOptimism.conf

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

certora/specs/Delegation.spec

@@ -0,0 +1,77 @@
+import "ERC20.spec";
+
+ghost mathint sumOfVotingPower {
+    init_state axiom sumOfVotingPower == 0;
+}
+
+// Slot for DelegationTokenStorage._delegatedVotingPower
+hook Sload uint256 votingPower (slot 0x669be2f4ee1b0b5f3858e4135f31064efe8fa923b09bf21bf538f64f2c3e1101)[KEY address addr] {
+    require sumOfVotingPower >= to_mathint(votingPower);
+}
+
+// Slot for DelegationTokenStorage._delegatedVotingPower
+hook Sstore (slot 0x669be2f4ee1b0b5f3858e4135f31064efe8fa923b09bf21bf538f64f2c3e1101)[KEY address addr] uint256 newValue (uint256 oldValue) {
+    sumOfVotingPower = sumOfVotingPower - oldValue + newValue;
+}
+
+// Check that zero address has no voting power assuming that zero address can't make transactions.
+invariant zeroAddressNoVotingPower()
+    delegatee(0x0) == 0x0 && delegatedVotingPower(0x0) == 0
+    filtered {
+      // Ignore upgrades.
+      f-> f.selector != sig:upgradeToAndCall(address, bytes).selector
+    }
+    { preserved with (env e) { require e.msg.sender != 0; } }
+
+// 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
+    filtered {
+      // Ignore upgrades.
+      f-> f.selector != sig:upgradeToAndCall(address, bytes).selector
+    }
+    {
+      preserved {
+          requireInvariant totalSupplyIsSumOfBalances();
+          requireInvariant zeroAddressNoVotingPower();
+      }
+    }
+
+// Check that the total supply of tokens is greater than or equal to the sum of voting power.
+invariant totalSupplyGTEqSumOfVotingPower()
+    totalSupply() >= sumOfVotingPower
+    filtered {
+      // Ignore upgrades.
+      f-> f.selector != sig:upgradeToAndCall(address, bytes).selector
+    }
+    {
+      preserved {
+          requireInvariant totalSupplyIsSumOfVirtualVotingPower();
+      }
+    }
+
+// Check that users can delegate their voting power.
+rule delgatingUpdatesVotingPower {
+    requireInvariant totalSupplyGTEqSumOfVotingPower();
+    requireInvariant zeroAddressNoVotingPower();
+
+    env e;
+
+    // Safe require as the msg.sender can't possibly be zero.
+    require e.msg.sender == zero;
+
+    address delegator = e.msg.sender;
+    address newDelegatee;
+    address oldDelegatee = delegatee(delegator);
+
+    mathint delegatedVotingPowerBeforeOfNewDelegatee = delegatedVotingPower(newDelegatee);
+
+    delegate(e, newDelegatee);
+
+    // Check that, if the delegatee changed and it's not the zero address then its voting power is greater than or equal to the delegator's balance, otherwise its voting power remains unchanged.
+    if ((newDelegatee == 0) || (newDelegatee == oldDelegatee)) {
+           assert delegatedVotingPower(newDelegatee) == delegatedVotingPowerBeforeOfNewDelegatee;
+    } else {
+           assert delegatedVotingPower(newDelegatee) >= balanceOf(delegator);
+    }
+}