diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml index 255fb33..4362ff0 100644 --- a/.github/workflows/certora.yml +++ b/.github/workflows/certora.yml @@ -18,7 +18,9 @@ jobs: conf: - DelegationEthereum - DelegationOptimism + - ERC20InvariantsEthereum - ERC20Ethereum + - ERC20InvariantsOptimism - ERC20Optimism - ExternalCallsEthereum - ExternalCallsOptimism diff --git a/certora/README.md b/certora/README.md index c05e3d4..405a375 100644 --- a/certora/README.md +++ b/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. diff --git a/certora/confs/ERC20InvariantsEthereum.conf b/certora/confs/ERC20InvariantsEthereum.conf new file mode 100644 index 0000000..205d712 --- /dev/null +++ b/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" +} diff --git a/certora/confs/ERC20InvariantsOptimism.conf b/certora/confs/ERC20InvariantsOptimism.conf new file mode 100644 index 0000000..7b11d5e --- /dev/null +++ b/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" +} diff --git a/certora/specs/Delegation.spec b/certora/specs/Delegation.spec index ea68bd2..6578434 100644 --- a/certora/specs/Delegation.spec +++ b/certora/specs/Delegation.spec @@ -1,3 +1,4 @@ +// SPDX-License-Identifier: GPL-2.0-or-later import "ERC20.spec"; methods { @@ -5,13 +6,34 @@ methods { 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. @@ -19,6 +41,61 @@ 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(); } } diff --git a/certora/specs/ERC20.spec b/certora/specs/ERC20.spec index 72e2db4..69d7e2a 100644 --- a/certora/specs/ERC20.spec +++ b/certora/specs/ERC20.spec @@ -1,6 +1,8 @@ // 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; @@ -8,34 +10,10 @@ 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,9 +22,7 @@ hook Sstore (slot 0x52c63247e1f47db19d5ce0460030c497f067ca4cebf71ba98eeadabe20ba └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -invariant totalSupplyIsSumOfBalances() - to_mathint(totalSupply()) == sumOfBalances; - +use invariant totalSupplyIsSumOfBalances; /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ @@ -54,8 +30,7 @@ invariant totalSupplyIsSumOfBalances() └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -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); diff --git a/certora/specs/ERC20Invariants.spec b/certora/specs/ERC20Invariants.spec new file mode 100644 index 0000000..e7bd7fe --- /dev/null +++ b/certora/specs/ERC20Invariants.spec @@ -0,0 +1,144 @@ +// 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) sumsOfVotesDelegatedToA { + init_state axiom forall mathint account. sumsOfVotesDelegatedToA[account] == 0; +} + +// Ghost copy of DelegationTokenStorage._delegatee for quantification. +ghost mapping(address => address) ghostDelegatee { + init_state axiom forall address account. ghostDelegatee[account] == 0; +} + +// Slot is DelegationTokenStorage._delegatee. +hook Sload address delegatee (slot 0x669be2f4ee1b0b5f3858e4135f31064efe8fa923b09bf21bf538f64f2c3e1100)[KEY address account] { + require ghostDelegatee[account] == delegatee; +} + +// Slot is DelegationTokenStorage._delegatee. +hook Sstore (slot 0x669be2f4ee1b0b5f3858e4135f31064efe8fa923b09bf21bf538f64f2c3e1100)[KEY address account] address delegatee (address delegateeOld) { + mathint changeOfAccountVotesForA; + // Track delegation changes from the parameterized address. + if (delegateeOld == A && delegatee != A) { + require changeOfAccountVotesForA == - ghostBalances[account]; + // Track delegation changes to the prameterized address. + } else if (delegateeOld != A && delegatee == A) { + require changeOfAccountVotesForA == ghostBalances[account]; + } else { + require changeOfAccountVotesForA == 0; + } + // Update partial sums for x > to_mathint(account) + havoc sumsOfVotesDelegatedToA assuming + forall mathint x. sumsOfVotesDelegatedToA@new[x] == + sumsOfVotesDelegatedToA@old[x] + (to_mathint(account) < x ? changeOfAccountVotesForA : 0); + // Update ghost copy of DelegationTokenStorage._delegatee. + ghostDelegatee[account] = delegatee; +} + +// Ghost variable to hold the sum of balances. +// To reason exhaustively on the value of the sum of balances we proceed to compute the partial sum of balances for each possible address. +// We call the partial sum of balances up to an addrress a, to sum of balances for all addresses within the range [0..a[. +// Formally, we write ∀ a:address, sumOfBalances[a] = Σ balanceOf(i) where the sum ranges over addresses i < a, provided that the address zero holds no token 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 supply of tokens using universal quantifiers. +// From this follows the property such that, ∀ a:address, balanceOf(a) ≤ totalSupply(). +// In particular we have the equality, sumOfBalances[2^160] = totalSupply() and we are able to to show that the sum of two different balances is lesser than or equal to the total supply. +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) ghostBalances { + init_state axiom forall address account. ghostBalances[account] == 0; +} + +// Slot is ERC20Storage._balances slot. +hook Sload uint256 balance (slot 0x52c63247e1f47db19d5ce0460030c497f067ca4cebf71ba98eeadabe20bace00)[KEY address account] { + require ghostBalances[account] == 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 (ghostDelegatee[account] == A) { + havoc sumsOfVotesDelegatedToA assuming + forall mathint x. sumsOfVotesDelegatedToA@new[x] == + sumsOfVotesDelegatedToA@old[x] + (to_mathint(account) < x ? newValue - oldValue : 0); + } + // Update ghost copy of ERC20Storage._balances. + ghostBalances[account] = newValue; +} + +invariant sumOfBalancesStartsAtZero() + sumOfBalances[0] == 0; + +invariant sumOfBalancesGrowsCorrectly() + forall address addr. sumOfBalances[to_mathint(addr) + 1] == + sumOfBalances[to_mathint(addr)] + ghostBalances[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. ghostBalances[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;