[Certora] Delegation invariant

certora/README.md

@@ -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/specs/Delegation.spec

@@ -1,24 +1,93 @@
+// 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.
 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) ghost_delegatedVotingPower {
+    init_state axiom forall address account. ghost_delegatedVotingPower[account] == 0;
+}
+
+hook Sload uint256 votingPower (slot 0x669be2f4ee1b0b5f3858e4135f31064efe8fa923b09bf21bf538f64f2c3e1101)[KEY address account] {
+    require ghost_delegatedVotingPower[account] == votingPower;
+}
+
+// Slot is DelegationTokenStorage._delegatedVotingPower.
+hook Sstore (slot 0x669be2f4ee1b0b5f3858e4135f31064efe8fa923b09bf21bf538f64f2c3e1101)[KEY address account] uint256 votingPower (uint256 votingPowerOld) {
+    // Update DelegationTokenStorage._delegatedVotingPower
+    ghost_delegatedVotingPower[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()
+    sumsOfVotes[0] == 0;
+
+invariant sumOfVotesGrowsCorrectly()
+    forall address account. sumsOfVotes[to_mathint(account) + 1] ==
+    sumsOfVotes[to_mathint(account)] + (ghost_delegatee[account] == A ? ghost_balances[account] : 0) ;
+
+invariant sumOfVotesMonotone()
+    forall mathint i. forall mathint j. i <= j => sumsOfVotes[i] <= sumsOfVotes[j]
+    {
+        preserved {
+            requireInvariant sumOfVotesStartsAtZero();
+            requireInvariant sumOfVotesGrowsCorrectly();
+        }
+    }
+
+invariant delegatedLTEqPartialSum()
+    forall address account. ghost_delegatee[account] == A =>
+      ghost_balances[account] <= sumsOfVotes[to_mathint(account)+1]
+    {
+        preserved {
+            requireInvariant sumOfVotesStartsAtZero();
+            requireInvariant sumOfVotesGrowsCorrectly();
+            requireInvariant sumOfVotesMonotone();
+        }
+    }
+
+
+invariant sumOfVotesIsDelegatedToA()
+    sumsOfVotes[2^160] == ghost_delegatedVotingPower[A]
+    {
+        preserved {
+            requireInvariant zeroAddressNoVotingPower();
+            requireInvariant sumOfVotesStartsAtZero();
+            requireInvariant sumOfVotesGrowsCorrectly();
+            requireInvariant sumOfVotesMonotone();
+        }
+    }
+
+invariant delegatedLTEqDelegateeVP()
+    forall address account.
+      ghost_delegatee[account] == A =>
+      ghost_balances[account] <= ghost_delegatedVotingPower[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 +105,7 @@ invariant totalSupplyIsSumOfVirtualVotingPower()
         preserved {
             requireInvariant totalSupplyIsSumOfBalances();
             requireInvariant zeroAddressNoVotingPower();
+            requireInvariant balancesLTEqTotalSupply();
         }
     }
 

certora/specs/ERC20.spec

@@ -1,61 +1,46 @@
 // 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                                                                                  │
+│ Invariant: totalSupply is the 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);
-}
+use invariant sumOfBalancesStartsAtZero;
 
-// Slot is ERC20Storage._balances slot
-hook Sstore (slot 0x52c63247e1f47db19d5ce0460030c497f067ca4cebf71ba98eeadabe20bace00)[KEY address addr] uint256 newValue (uint256 oldValue) {
-   sumOfBalances = sumOfBalances - oldValue + newValue;
-}
+use invariant sumOfBalancesGrowsCorrectly;
 
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Invariant: totalSupply is the sum of all balances                                                                   │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
+use invariant sumOfBalancesMonotone;
+
+use invariant totalSupplyIsSumOfBalances;
 
-invariant totalSupplyIsSumOfBalances()
-    to_mathint(totalSupply()) == sumOfBalances;
+use rule twoBalancesCannotExceedTotalSupply;
 
+use invariant balancesLTEqTotalSupply;
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
 │ Invariant: balance of address(0) is 0                                                                               │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 
-invariant zeroAddressNoBalance()
-    balanceOf(0) == 0;
+use invariant zeroAddressNoBalance;
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
@@ -98,6 +83,7 @@ rule transfer(env e) {
     requireInvariant totalSupplyIsSumOfBalances();
     require nonpayable(e);
 
+
     address holder = e.msg.sender;
     address recipient;
     address other;
@@ -110,6 +96,9 @@ rule transfer(env e) {
     uint256 recipientVotingPowerBefore = delegatedVotingPower(delegatee(recipient));
     uint256 otherBalanceBefore     = balanceOf(other);
 
+    // Safe require as it's proven by rule twoBalancesCannotExceedTotalSupply
+    require balanceOf(holder)+balanceOf(recipient) <= totalSupply();
+
     // run transaction
     transfer@withrevert(e, recipient, amount);
 
@@ -151,6 +140,9 @@ rule transferFrom(env e) {
     uint256 recipientVotingPowerBefore = delegatedVotingPower(delegatee(recipient));
     uint256 otherBalanceBefore     = balanceOf(other);
 
+    // Safe require as it's proven by rule twoBalancesCannotExceedTotalSupply
+    require balanceOf(holder)+balanceOf(recipient) <= totalSupply();
+
     // run transaction
     transferFrom@withrevert(e, holder, recipient, amount);
 

certora/specs/ERC20Invariants.spec

@@ -0,0 +1,139 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+
+methods {
+    function totalSupply() external returns uint256 envfree;
+    function balanceOf(address) external returns uint256 envfree;
+    function delegatee(address) external returns address envfree;
+    function delegatedVotingPower(address) external returns uint256 envfree;
+    function upgradeToAndCall(address, bytes) external => NONDET DELETE;
+}
+
+// Paramater for any address that is not the zero address.
+persistent ghost address A {
+    axiom A != 0;
+}
+
+// Partial sum of delegated votes to parameterized address A.
+// sumOfvotes[x] = \sum_{i=0}^{x-1} balances[i] when delegatee[i] == A;
+ghost mapping(mathint => mathint) sumsOfVotes {
+    init_state axiom forall mathint account. sumsOfVotes[account] == 0;
+}
+
+// Ghost copy of DelegationTokenStorage._delegatee for quantification.
+ghost mapping(address => address) ghost_delegatee {
+    init_state axiom forall address account. ghost_delegatee[account] == 0;
+}
+
+// Slot is DelegationTokenStorage._delegatee.
+hook Sload address delegatee (slot 0x669be2f4ee1b0b5f3858e4135f31064efe8fa923b09bf21bf538f64f2c3e1100)[KEY address account] {
+    require ghost_delegatee[account] == delegatee;
+}
+
+// Slot is DelegationTokenStorage._delegatee.
+hook Sstore (slot 0x669be2f4ee1b0b5f3858e4135f31064efe8fa923b09bf21bf538f64f2c3e1100)[KEY address account] address delegatee (address delegateeOld) {
+    // Update partial sums for x > to_mathint(account)
+    // Track delegation changes from the parameterized address.
+    if (delegateeOld == A && delegatee != A) {
+        havoc sumsOfVotes assuming
+            forall mathint x. sumsOfVotes@new[x] ==
+            sumsOfVotes@old[x] - (to_mathint(account) < x ? ghost_balances[account] : 0);
+    }
+    // Track delegation changes to the pramaeterized address.
+    else if (delegateeOld != A && delegatee == A) {
+        havoc sumsOfVotes assuming
+            forall mathint x. sumsOfVotes@new[x] ==
+                sumsOfVotes@old[x] + (to_mathint(account) < x ? ghost_balances[account] : 0);
+    }
+    // Update ghost copy of DelegationTokenStorage._delegatee.
+    ghost_delegatee[account] = delegatee;
+}
+
+// Ghost variable to hold the sum of balances.
+ghost mapping(mathint => mathint) sumOfBalances {
+    init_state axiom forall mathint addr. sumOfBalances[addr] == 0;
+}
+
+// Ghost copy of ERC20Storage._balances for quantification.
+ghost mapping(address => uint256) ghost_balances {
+    init_state axiom forall address account. ghost_balances[account] == 0;
+}
+
+//Slot is ERC20Storage._balances slot.
+hook Sload uint256 balance (slot 0x52c63247e1f47db19d5ce0460030c497f067ca4cebf71ba98eeadabe20bace00)[KEY address account] {
+    require ghost_balances[account] == balance;
+    // Safe require as accounts can't hold more tokens than the total supply in preconditions.
+    //require sumOfBalances >= to_mathint(balance);
+}
+
+//Slot is ERC20Storage._balances slot
+hook Sstore (slot 0x52c63247e1f47db19d5ce0460030c497f067ca4cebf71ba98eeadabe20bace00)[KEY address account] uint256 newValue (uint256 oldValue) {
+    // Update partial sum of balances, for x > to_mathint(account)
+    // Track balance changes in balances.
+    havoc sumOfBalances assuming
+        forall mathint x. sumOfBalances@new[x] ==
+            sumOfBalances@old[x] + (to_mathint(account) < x ? newValue - oldValue : 0);
+    // Update partial sums of votes delegated to the parameterized address, for x > to_mathint(account)
+    // Track balance changes when the delegatee is the parameterized address.
+    if (ghost_delegatee[account] == A) {
+        havoc sumsOfVotes assuming
+            forall mathint x. sumsOfVotes@new[x] ==
+                sumsOfVotes@old[x] + (to_mathint(account) < x ? newValue - oldValue : 0);
+    }
+    // Update ghost copy of ERC20Storage._balances.
+    ghost_balances[account] = newValue;
+}
+
+invariant sumOfBalancesStartsAtZero()
+    sumOfBalances[0] == 0;
+
+invariant sumOfBalancesGrowsCorrectly()
+    forall address addr. sumOfBalances[to_mathint(addr) + 1] ==
+        sumOfBalances[to_mathint(addr)] + ghost_balances[addr];
+
+invariant sumOfBalancesMonotone()
+    forall mathint i. forall mathint j. i <= j => sumOfBalances[i] <= sumOfBalances[j]
+    {
+        preserved {
+            requireInvariant sumOfBalancesStartsAtZero();
+            requireInvariant sumOfBalancesGrowsCorrectly();
+        }
+    }
+
+// Check that the sum of balances equals the total supply.
+invariant totalSupplyIsSumOfBalances()
+    sumOfBalances[2^160] == to_mathint(totalSupply())
+    {
+        preserved {
+            requireInvariant sumOfBalancesStartsAtZero();
+            requireInvariant sumOfBalancesGrowsCorrectly();
+            requireInvariant sumOfBalancesMonotone();
+        }
+    }
+
+invariant balancesLTEqTotalSupply()
+    forall address a. ghost_balances[a] <= sumOfBalances[2^160]
+    {
+        preserved {
+            requireInvariant sumOfBalancesStartsAtZero();
+            requireInvariant sumOfBalancesGrowsCorrectly();
+            requireInvariant sumOfBalancesMonotone();
+            requireInvariant totalSupplyIsSumOfBalances();
+        }
+    }
+
+rule twoBalancesCannotExceedTotalSupply(address accountA, address accountB) {
+    requireInvariant sumOfBalancesStartsAtZero();
+    requireInvariant sumOfBalancesGrowsCorrectly();
+    requireInvariant sumOfBalancesMonotone();
+    requireInvariant totalSupplyIsSumOfBalances();
+    uint256 balanceA = balanceOf(accountA);
+    uint256 balanceB = balanceOf(accountB);
+
+    assert accountA != accountB =>
+        balanceA + balanceB <= to_mathint(totalSupply());
+    satisfy(accountA != accountB && balanceA > 0 && balanceB > 0);
+}
+
+// Check that zero address's balance is equal to zero.
+invariant zeroAddressNoBalance()
+    balanceOf(0) == 0;