[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,112 @@
+diff -ruN DelegationToken.sol DelegationToken.sol
+--- DelegationToken.sol	2024-11-26 11:51:35.000000000 +0100
++++ DelegationToken.sol	2024-11-28 18:57:16.000000000 +0100
+@@ -4,14 +4,14 @@
+ import {IDelegation, Signature, Delegation} from "./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-26 11:45:12.000000000 +0100
+@@ -26,16 +26,19 @@
+         __ERC20Permit_init(NAME);
+         __Ownable_init(owner);
+
++        _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-21 11:29:06.000000000 +0100
+@@ -3,7 +3,7 @@
+
+ import {IOptimismMintableERC20} from "./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.
+diff -ruN interfaces/IOptimismMintableERC20.sol interfaces/IOptimismMintableERC20.sol
+--- interfaces/IOptimismMintableERC20.sol	2024-11-06 18:57:11.000000000 +0100
++++ interfaces/IOptimismMintableERC20.sol	2024-11-21 11:29:06.000000000 +0100
+@@ -2,7 +2,7 @@
+ pragma solidity >=0.5.0;
+
+ 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";
+
+ /// @title IOptimismMintableERC20
+ /// @author Morpho Association

certora/confs/DelegationEthereum.conf

@@ -0,0 +1,18 @@
+{
+  "files": [
+    "certora/helpers/MorphoTokenEthereumHarness.sol"
+  ],
+  "parametric_contracts": [
+    "MorphoTokenEthereumHarness",
+  ],
+  "solc": "solc-0.8.27",
+  "verify": "MorphoTokenEthereumHarness: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/helpers/MorphoTokenOptimismHarness.sol"
+  ],
+  "parametric_contracts": [
+    "MorphoTokenOptimismHarness"
+  ],
+  "solc": "solc-0.8.27",
+  "verify": "MorphoTokenOptimismHarness: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/helpers/MorphoTokenEthereumHarness.sol

@@ -0,0 +1,23 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+pragma solidity 0.8.27;
+
+import {DelegationToken, Signature, Delegation} from "../munged/DelegationToken.sol";
+import "../munged/MorphoTokenEthereum.sol";
+import {ECDSA} from
+    "../../lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/contracts/utils/cryptography/ECDSA.sol";
+
+contract MorphoTokenEthereumHarness is MorphoTokenEthereum {
+    function delegatorFromSig(Delegation calldata delegation, Signature calldata signature)
+        external
+        view
+        returns (address)
+    {
+        address delegator = ECDSA.recover(
+            _hashTypedDataV4(keccak256(abi.encode(DELEGATION_TYPEHASH, delegation))),
+            signature.v,
+            signature.r,
+            signature.s
+        );
+        return delegator;
+    }
+}

certora/helpers/MorphoTokenOptimismHarness.sol

@@ -0,0 +1,25 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+pragma solidity 0.8.27;
+
+import {DelegationToken, Signature, Delegation} from "../munged/DelegationToken.sol";
+import "../munged/MorphoTokenOptimism.sol";
+import {ECDSA} from
+    "../../lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/contracts/utils/cryptography/ECDSA.sol";
+
+contract MorphoTokenOptimismHarness is MorphoTokenOptimism {
+    constructor(address newRemoteToken, address newBridge) MorphoTokenOptimism(newRemoteToken, newBridge) {}
+
+    function delegatorFromSig(Delegation calldata delegation, Signature calldata signature)
+        external
+        view
+        returns (address)
+    {
+        address delegator = ECDSA.recover(
+            _hashTypedDataV4(keccak256(abi.encode(DELEGATION_TYPEHASH, delegation))),
+            signature.v,
+            signature.r,
+            signature.s
+        );
+        return delegator;
+    }
+}

certora/specs/Delegation.spec

@@ -0,0 +1,90 @@
+import "ERC20.spec";
+
+methods {
+    function delegatorFromSig(DelegationToken.Delegation, DelegationToken.Signature) external returns address envfree;
+    function delegationNonce(address) external returns uint256 envfree;
+}
+
+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;
+}
+
+// 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 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
+    {
+      preserved {
+          // Safe requires because the proxy contract should be initialized right after construction.
+          require totalSupply() == 0;
+          require sumOfVotingPower == 0;
+
+          requireInvariant totalSupplyIsSumOfBalances();
+          requireInvariant zeroAddressNoVotingPower();
+      }
+    }
+
+function isTotalSupplyGTEqSumOfVotingPower() returns bool {
+    requireInvariant totalSupplyIsSumOfVirtualVotingPower();
+    return totalSupply() >= sumOfVotingPower;
+}
+
+// Check that the total supply of tokens is greater than or equal to the sum of voting power.
+rule totalSupplyGTEqSumOfVotingPower {
+    assert isTotalSupplyGTEqSumOfVotingPower();
+}
+
+// Check that users can delegate their voting power.
+rule delegatingUpdatesVotingPower(env e, address newDelegatee) {
+    requireInvariant zeroAddressNoVotingPower();
+    assert isTotalSupplyGTEqSumOfVotingPower();
+
+    address oldDelegatee = delegatee(e.msg.sender);
+
+    mathint delegatedVotingPowerBefore = 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) == delegatedVotingPowerBefore;
+    } else {
+        assert delegatedVotingPower(newDelegatee) == delegatedVotingPowerBefore + balanceOf(e.msg.sender);
+    }
+}
+
+// Check that users can delegate their voting power.
+rule delegatingWithSigUpdatesVotingPower(env e, DelegationToken.Delegation delegation, DelegationToken.Signature signature) {
+    requireInvariant zeroAddressNoVotingPower();
+    assert isTotalSupplyGTEqSumOfVotingPower();
+
+    address delegator = delegatorFromSig(delegation, signature);
+
+    address oldDelegatee = delegatee(delegator);
+    mathint delegationNonceBefore = delegationNonce(delegator);
+
+    mathint delegatedVotingPowerBefore = delegatedVotingPower(delegation.delegatee);
+
+    delegateWithSig(e, delegation, signature);
+
+    // Check that the delegation's nonce matches the delegator's nonce.
+    assert delegation.nonce == delegationNonceBefore;
+    // Check that the current block timestamp is not later than the delegation's expiry timestamp.
+    assert e.block.timestamp <= delegation.expiry;
+
+    // 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 ((delegation.delegatee == 0) || (delegation.delegatee == oldDelegatee)) {
+        assert delegatedVotingPower(delegation.delegatee) == delegatedVotingPowerBefore;
+    } else {
+        assert delegatedVotingPower(delegation.delegatee) == delegatedVotingPowerBefore + balanceOf(delegator);
+    }
+}