fix: implement review comment

morpho-org · Nov 26, 2024 · 83b19c4 · 83b19c4
1 parent 04ecb92
commit 83b19c4
Show file tree

Hide file tree

Showing 2 changed files with 75 additions and 22 deletions.
diff --git a/certora/applyMunging.patch b/certora/applyMunging.patch
@@ -1,6 +1,6 @@
 diff -ruN DelegationToken.sol DelegationToken.sol
---- DelegationToken.sol	2024-11-14 11:00:56.877231237 +0100
-+++ DelegationToken.sol	2024-11-20 16:18:55.750677310 +0100
+--- DelegationToken.sol	2024-11-06 18:57:11.000000000 +0100
++++ DelegationToken.sol	2024-11-26 11:36:31.000000000 +0100
 @@ -4,14 +4,14 @@
  import {IDelegation, Signature, Delegation} from "./interfaces/IDelegation.sol";
 
@@ -31,7 +31,27 @@ diff -ruN DelegationToken.sol DelegationToken.sol
      /* ERRORS */
 
      /// @notice The signature used has expired.
-@@ -148,12 +151,16 @@
+@@ -102,6 +105,19 @@
+         _delegate(delegator, newDelegatee);
+     }
+
++    function _delegatorFromSig(Delegation calldata delegation, Signature calldata signature)
++        external
++        returns (address)
++    {
++        address delegator = ECDSA.recover(
++            _hashTypedDataV4(keccak256(abi.encode(DELEGATION_TYPEHASH, delegation))),
++            signature.v,
++            signature.r,
++            signature.s
++        );
++        return delegator;
++    }
++
+     /// @notice Delegates the balance of the signer to `newDelegatee`.
+     /// @dev Delegating to the zero address effectively removes the delegation, incidentally making transfers cheaper.
+     /// @dev Delegating to the previous delegatee effectively revokes past signatures with the same nonce.
+@@ -148,12 +164,16 @@
                  uint256 newValue = oldValue - amount;
                  $._delegatedVotingPower[from] = newValue;
                  emit DelegatedVotingPowerChanged(from, oldValue, newValue);
@@ -48,21 +68,9 @@ diff -ruN DelegationToken.sol DelegationToken.sol
              }
          }
      }
-diff -ruN interfaces/IOptimismMintableERC20.sol interfaces/IOptimismMintableERC20.sol
---- interfaces/IOptimismMintableERC20.sol	2024-11-14 11:00:56.877231237 +0100
-+++ interfaces/IOptimismMintableERC20.sol	2024-11-20 16:30:24.300071161 +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
 diff -ruN MorphoTokenEthereum.sol MorphoTokenEthereum.sol
---- MorphoTokenEthereum.sol	2024-11-14 11:00:56.877231237 +0100
-+++ MorphoTokenEthereum.sol	2024-11-20 13:29:38.986459880 +0100
+--- 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);
@@ -84,8 +92,8 @@ diff -ruN MorphoTokenEthereum.sol MorphoTokenEthereum.sol
      }
  }
 diff -ruN MorphoTokenOptimism.sol MorphoTokenOptimism.sol
---- MorphoTokenOptimism.sol	2024-11-14 11:00:56.877231237 +0100
-+++ MorphoTokenOptimism.sol	2024-11-20 16:19:11.314241653 +0100
+--- 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";
@@ -110,3 +118,15 @@ diff -ruN MorphoTokenOptimism.sol MorphoTokenOptimism.sol
      }
 
      /// @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
diff --git a/certora/specs/Delegation.spec b/certora/specs/Delegation.spec
@@ -1,5 +1,10 @@
 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;
 }
@@ -45,14 +50,42 @@ rule delegatingUpdatesVotingPower(env e, address newDelegatee) {
 
     address oldDelegatee = delegatee(e.msg.sender);
 
-    mathint delegatedVotingPowerBeforeOfNewDelegatee = delegatedVotingPower(newDelegatee);
+    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) == delegatedVotingPowerBeforeOfNewDelegatee;
+        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;
+    // assert Utils.delegatorFromSig(delegation, signature) == delegator;
+
+    // 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(newDelegatee) >= balanceOf(e.msg.sender);
+        assert delegatedVotingPower(delegation.delegatee) == delegatedVotingPowerBefore + balanceOf(delegator);
     }
 }