From 66213402e413ddebefa7d2e789ef08ca372d9b5e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= Date: Mon, 16 Dec 2024 09:40:49 +0100 Subject: [PATCH 01/14] fix: typo --- certora/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/certora/README.md b/certora/README.md index 25c5e48..2955006 100644 --- a/certora/README.md +++ b/certora/README.md @@ -51,7 +51,7 @@ 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) ensures that the Morpho token is compliant with the [ERC20](https://eips.ethereum.org/EIPS/eip-20) specification, we also check Morpho token `burn` and `mint` functions in [`MintBurnEthereum`](specs/MintBurnEthereum.spec) and [`MintBurnOptimism`](specs/MintBurnOptimism.spec); -- [`Delegation.spec`](specs/Delegation.spec) checks the logic for voting power delegation. +- [`Delegation.spec`](specs/Delegation.spec) checks the logic for voting power delegation; - [`RevertsERC20.spec`](specs/RevertsERC20.spec), [`RevertsMintBurnEthereum.spec`](specs/RevertsMintBurnEthereum.spec) and [`RevertsMintBurnOptimism.spec`](specs/RevertsMintBurnOptimism.spec) check that conditions for reverts and inputs are correctly validated. The [`certora/confs`](confs) folder contains a configuration file for each corresponding specification file for both the Ethereum and the Optimism version. From 2ebbdff19540c913d270724512e46c042716cb86 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= Date: Mon, 16 Dec 2024 09:41:03 +0100 Subject: [PATCH 02/14] refactor: add require statements --- certora/specs/ERC20.spec | 18 ++++++++++++------ 1 file changed, 12 insertions(+), 6 deletions(-) diff --git a/certora/specs/ERC20.spec b/certora/specs/ERC20.spec index 5fad14f..319920b 100644 --- a/certora/specs/ERC20.spec +++ b/certora/specs/ERC20.spec @@ -87,14 +87,17 @@ rule transfer(env e) { uint256 recipientVotingPowerBefore = delegatedVotingPower(delegatee(recipient)); uint256 otherBalanceBefore = balanceOf(other); + // Safe require as it is verified in delegatedLTEqDelegateeVP. + require holderBalanceBefore <= holderVotingPowerBefore; + // Safe require as it is verified in totalSupplyGTEqSumOfVotingPower. + require delegatee(holder) != delegatee(recipient) => holderBalanceBefore + recipientVotingPowerBefore <= totalSupply(); + // run transaction transfer@withrevert(e, recipient, amount); // check outcome if (lastReverted) { - assert holder == 0 || recipient == 0 || amount > holderBalanceBefore || - // Handle overflows in delegation, should not be possible. - recipientVotingPowerBefore + amount > max_uint256 || holderVotingPowerBefore < amount ; + assert holder == 0 || recipient == 0 || amount > holderBalanceBefore; } else { // balances of holder and recipient are updated assert to_mathint(balanceOf(holder)) == holderBalanceBefore - (holder == recipient ? 0 : amount); @@ -129,14 +132,17 @@ rule transferFrom(env e) { uint256 recipientVotingPowerBefore = delegatedVotingPower(delegatee(recipient)); uint256 otherBalanceBefore = balanceOf(other); + // Safe require as it is verified in delegatedLTEqDelegateeVP. + require holderBalanceBefore <= holderVotingPowerBefore; + // Safe require as it is verified in totalSupplyGTEqSumOfVotingPower. + require delegatee(holder) != delegatee(recipient) => holderBalanceBefore + recipientVotingPowerBefore <= totalSupply(); + // run transaction transferFrom@withrevert(e, holder, recipient, amount); // check outcome if (lastReverted) { - assert holder == 0 || recipient == 0 || spender == 0 || amount > holderBalanceBefore || amount > allowanceBefore - // Handle overflows in delegation, should not be possible. - || amount + recipientVotingPowerBefore > max_uint256 || holderVotingPowerBefore < amount ; + assert holder == 0 || recipient == 0 || spender == 0 || amount > holderBalanceBefore || amount > allowanceBefore; } else { // allowance is valid & updated assert allowanceBefore >= amount; From 6ab5bad1d890e43892fab7fec54fe11c6f320a55 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= Date: Mon, 16 Dec 2024 13:31:06 +0100 Subject: [PATCH 03/14] refactor: simplify revert causes --- certora/specs/MintBurnEthereum.spec | 4 +--- certora/specs/MintBurnOptimism.spec | 3 +-- 2 files changed, 2 insertions(+), 5 deletions(-) diff --git a/certora/specs/MintBurnEthereum.spec b/certora/specs/MintBurnEthereum.spec index 7524696..4a1fe0f 100644 --- a/certora/specs/MintBurnEthereum.spec +++ b/certora/specs/MintBurnEthereum.spec @@ -67,7 +67,6 @@ rule mint(env e) { // cache state uint256 toBalanceBefore = balanceOf(to); - uint256 toVotingPowerBefore = delegatedVotingPower(delegatee(to)); uint256 otherBalanceBefore = balanceOf(other); uint256 totalSupplyBefore = totalSupply(); @@ -76,8 +75,7 @@ rule mint(env e) { // check outcome if (lastReverted) { - assert e.msg.sender != owner() || to == 0 || totalSupplyBefore + amount > max_uint256 || - toVotingPowerBefore + amount > max_uint256; + assert e.msg.sender != owner() || to == 0 || totalSupplyBefore + amount > max_uint256 ; } else { // updates balance and totalSupply assert e.msg.sender == owner(); diff --git a/certora/specs/MintBurnOptimism.spec b/certora/specs/MintBurnOptimism.spec index 5a91f51..d40cf83 100644 --- a/certora/specs/MintBurnOptimism.spec +++ b/certora/specs/MintBurnOptimism.spec @@ -68,7 +68,6 @@ rule mint(env e) { // cache state uint256 toBalanceBefore = balanceOf(to); - uint256 toVotingPowerBefore = delegatedVotingPower(delegatee(to)); uint256 otherBalanceBefore = balanceOf(other); uint256 totalSupplyBefore = totalSupply(); @@ -78,7 +77,7 @@ rule mint(env e) { // check outcome if (lastReverted) { assert e.msg.sender != owner() || to == 0 || totalSupplyBefore + amount > max_uint256 || - toVotingPowerBefore + amount > max_uint256 || e.msg.sender != currentContract.bridge; + e.msg.sender != currentContract.bridge; } else { // updates balance and totalSupply assert e.msg.sender == currentContract.bridge; From 2279357852287b8d993b4c8414c9edf52cc30645 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Tue, 14 Jan 2025 12:36:46 +0100 Subject: [PATCH 04/14] refactor: safe require in MintBurn --- certora/specs/MintBurnEthereum.spec | 7 ++++++- certora/specs/MintBurnOptimism.spec | 8 ++++++-- 2 files changed, 12 insertions(+), 3 deletions(-) diff --git a/certora/specs/MintBurnEthereum.spec b/certora/specs/MintBurnEthereum.spec index 4a1fe0f..3181d6b 100644 --- a/certora/specs/MintBurnEthereum.spec +++ b/certora/specs/MintBurnEthereum.spec @@ -110,12 +110,17 @@ rule burn(env e) { uint256 otherBalanceBefore = balanceOf(other); uint256 totalSupplyBefore = totalSupply(); + // Safe require as zeroVirtualVotingPower represents the virtual sum of votes delegated to zero. + require delegatee(from) == 0 => fromBalanceBefore <= currentContract._zeroVirtualVotingPower; + // Safe require as it is verified in delegatedLTEqDelegateeVP. + require delegatee(from) != 0 => fromBalanceBefore <= fromVotingPowerBefore; + // run transaction burn@withrevert(e, amount); // check outcome if (lastReverted) { - assert e.msg.sender == 0x0 || fromBalanceBefore < amount || fromVotingPowerBefore < amount ; + assert e.msg.sender == 0x0 || fromBalanceBefore < amount; } else { // updates balance and totalSupply assert to_mathint(balanceOf(from)) == fromBalanceBefore - amount; diff --git a/certora/specs/MintBurnOptimism.spec b/certora/specs/MintBurnOptimism.spec index d40cf83..b7516ec 100644 --- a/certora/specs/MintBurnOptimism.spec +++ b/certora/specs/MintBurnOptimism.spec @@ -112,13 +112,17 @@ rule burn(env e) { uint256 otherBalanceBefore = balanceOf(other); uint256 totalSupplyBefore = totalSupply(); + // Safe require as zeroVirtualVotingPower represents the virtual sum of votes delegated to zero. + require delegatee(from) == 0 => fromBalanceBefore <= currentContract._zeroVirtualVotingPower; + // Safe require as it is verified in delegatedLTEqDelegateeVP. + require delegatee(from) != 0 => fromBalanceBefore <= fromVotingPowerBefore; + // run transaction burn@withrevert(e, from, amount); // check outcome if (lastReverted) { - assert e.msg.sender == 0x0 || fromBalanceBefore < amount || fromVotingPowerBefore < amount - || e.msg.sender != currentContract.bridge; + assert e.msg.sender == 0x0 || fromBalanceBefore < amount || e.msg.sender != currentContract.bridge; } else { // updates balance and totalSupply assert to_mathint(balanceOf(from)) == fromBalanceBefore - amount; From f55c0980a477be9fe67cfcda379b2ba35925f72f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= Date: Wed, 15 Jan 2025 15:19:43 +0100 Subject: [PATCH 05/14] fix: change unsafe require --- certora/specs/Delegation.spec | 31 +++++++++++++++++++++- certora/specs/RevertsERC20.spec | 13 ++++----- certora/specs/RevertsMintBurnEthereum.spec | 2 +- certora/specs/RevertsMintBurnOptimism.spec | 2 +- 4 files changed, 39 insertions(+), 9 deletions(-) diff --git a/certora/specs/Delegation.spec b/certora/specs/Delegation.spec index 3e081bc..f824ea5 100644 --- a/certora/specs/Delegation.spec +++ b/certora/specs/Delegation.spec @@ -159,7 +159,6 @@ invariant sumOfTwoDelegatedVPLTEqTotalVP() } } - function isTotalSupplyGTEqSumOfVotingPower() returns bool { requireInvariant totalSupplyIsSumOfVirtualVotingPower(); return totalSupply() >= sumOfVotes[2^160]; @@ -215,3 +214,33 @@ rule delegatingWithSigUpdatesVotingPower(env e, DelegationToken.Delegation deleg assert delegatedVotingPower(delegation.delegatee) == delegatedVotingPowerBefore + balanceOf(delegator); } } + +// Check that the delegated voting power of a delegatee after an update is lesser than or equal to the total supply of tokens. +rule updatedDelegatedVPLTEqTotalSupply(env e, address to, uint256 amount) { + // Safe require as implementation woud revert. + require amount <= balanceOf(e.msg.sender); + + // Safe rquire as zero address can't initiate transactions. + require e.msg.sender != 0; + + // Safe require as since we consider only updates. + require delegatee(to) != delegatee(e.msg.sender); + + delegate(e, e.msg.sender); + + assert delegatee(e.msg.sender) == e.msg.sender && delegatee(e.msg.sender) != 0; + + // Safe require that follows from delegatedLTEqDelegateeVP. + require amount <= delegatedVotingPower(e.msg.sender) ; + + requireInvariant delegatedVotingPowerLTEqTotalVotingPower(); + requireInvariant sumOfVotesStartsAtZero(); + requireInvariant sumOfVotesGrowsCorrectly(); + requireInvariant sumOfVotesMonotone(); + requireInvariant totalSupplyIsSumOfVirtualVotingPower(); + requireInvariant sumOfTwoDelegatedVPLTEqTotalVP(); + + assert isTotalSupplyGTEqSumOfVotingPower(); + + assert delegatedVotingPower(to) + amount <= totalSupply(); +} diff --git a/certora/specs/RevertsERC20.spec b/certora/specs/RevertsERC20.spec index a8e8d96..128a0df 100644 --- a/certora/specs/RevertsERC20.spec +++ b/certora/specs/RevertsERC20.spec @@ -15,9 +15,10 @@ rule transferRevertConditions(env e, address to, uint256 amount) { uint256 recipientVotingPowerBefore = delegatedVotingPower(delegatee(to)); // Safe require as it is verified in delegatedLTEqDelegateeVP. - require senderVotingPowerBefore >= balanceOfSenderBefore; - // Safe require that follows from sumOfTwoDelegatedVPLTEqTotalVP() and totalSupplyIsSumOfVirtualVotingPower(). - require delegatee(to) != delegatee(e.msg.sender) => recipientVotingPowerBefore + senderVotingPowerBefore <= totalSupply(); + require delegatee(e.msg.sender) != 0 => senderVotingPowerBefore >= balanceOfSenderBefore; + + // Safe require that follows from sumOfTwoDelegatedVPLTEqTotalVP() and totalSupplyIsSumOfVirtualVotingPower() and rule updatedDelegatedVPLTEqTotalSupply. + require delegatee(to) != delegatee(e.msg.sender) => recipientVotingPowerBefore + amount <= totalSupply(); transfer@withrevert(e, to, amount); assert lastReverted <=> e.msg.sender == 0 || to == 0 || balanceOfSenderBefore < amount || e.msg.value != 0; @@ -31,9 +32,9 @@ rule transferFromRevertConditions(env e, address from, address to, uint256 amoun uint256 recipientVotingPowerBefore = delegatedVotingPower(delegatee(to)); // Safe require as it is verified in delegatedLTEqDelegateeVP. - require holderVotingPowerBefore >= balanceOfHolderBefore; - // Safe require that follows from sumOfTwoDelegatedVPLTEqTotalVP() and totalSupplyIsSumOfVirtualVotingPower(). - require delegatee(to) != delegatee(from) => recipientVotingPowerBefore + holderVotingPowerBefore <= totalSupply(); + require delegatee(from) != 0 => holderVotingPowerBefore >= balanceOfHolderBefore; + // Safe require that follows from sumOfTwoDelegatedVPLTEqTotalVP() and totalSupplyIsSumOfVirtualVotingPower() and rule updatedDelegatedVPLTEqTotalSupply + require delegatee(to) != delegatee(from) => recipientVotingPowerBefore + amount <= totalSupply(); transferFrom@withrevert(e, from, to, amount); diff --git a/certora/specs/RevertsMintBurnEthereum.spec b/certora/specs/RevertsMintBurnEthereum.spec index bbc5d1b..3917431 100644 --- a/certora/specs/RevertsMintBurnEthereum.spec +++ b/certora/specs/RevertsMintBurnEthereum.spec @@ -33,7 +33,7 @@ rule burnRevertConditions(env e, uint256 amount) { require delegatee(0) == 0; // Safe require as it is verified in delegatedLTEqDelegateeVP. - require delegateeVotingPowerBefore >= balanceOfSenderBefore; + require delegatee(e.msg.sender) != 0 => delegateeVotingPowerBefore >= balanceOfSenderBefore; burn@withrevert(e, amount); assert lastReverted <=> e.msg.sender == 0 || balanceOfSenderBefore < amount || e.msg.value != 0; diff --git a/certora/specs/RevertsMintBurnOptimism.spec b/certora/specs/RevertsMintBurnOptimism.spec index 4e65492..4f13fc7 100644 --- a/certora/specs/RevertsMintBurnOptimism.spec +++ b/certora/specs/RevertsMintBurnOptimism.spec @@ -31,7 +31,7 @@ rule burnRevertConditions(env e, address from, uint256 amount) { require delegatee(0) == 0; // Safe require as it is verified in delegatedLTEqDelegateeVP. - require fromVotingPowerBefore >= balanceOfFromBefore; + require delegatee(from) != 0 =>fromVotingPowerBefore >= balanceOfFromBefore; burn@withrevert(e, from, amount); assert lastReverted <=> e.msg.sender != currentContract.bridge || from == 0 || balanceOfFromBefore < amount || e.msg.value != 0; From 273104e733d8fb0ae78edc596282eb70bc238daf Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= Date: Wed, 15 Jan 2025 16:31:09 +0100 Subject: [PATCH 06/14] refactor: improve updatedDelegatedVPLTEqTotalSupply --- certora/specs/Delegation.spec | 27 +++++++++++++++------------ 1 file changed, 15 insertions(+), 12 deletions(-) diff --git a/certora/specs/Delegation.spec b/certora/specs/Delegation.spec index f824ea5..75eb9de 100644 --- a/certora/specs/Delegation.spec +++ b/certora/specs/Delegation.spec @@ -226,21 +226,24 @@ rule updatedDelegatedVPLTEqTotalSupply(env e, address to, uint256 amount) { // Safe require as since we consider only updates. require delegatee(to) != delegatee(e.msg.sender); - delegate(e, e.msg.sender); + delegate@withrevert(e, e.msg.sender); - assert delegatee(e.msg.sender) == e.msg.sender && delegatee(e.msg.sender) != 0; + if (!lastReverted) { - // Safe require that follows from delegatedLTEqDelegateeVP. - require amount <= delegatedVotingPower(e.msg.sender) ; + assert delegatee(e.msg.sender) == e.msg.sender && delegatee(e.msg.sender) != 0; - requireInvariant delegatedVotingPowerLTEqTotalVotingPower(); - requireInvariant sumOfVotesStartsAtZero(); - requireInvariant sumOfVotesGrowsCorrectly(); - requireInvariant sumOfVotesMonotone(); - requireInvariant totalSupplyIsSumOfVirtualVotingPower(); - requireInvariant sumOfTwoDelegatedVPLTEqTotalVP(); + // Safe require that follows from delegatedLTEqDelegateeVP. + require amount <= delegatedVotingPower(e.msg.sender) ; - assert isTotalSupplyGTEqSumOfVotingPower(); + requireInvariant delegatedVotingPowerLTEqTotalVotingPower(); + requireInvariant sumOfVotesStartsAtZero(); + requireInvariant sumOfVotesGrowsCorrectly(); + requireInvariant sumOfVotesMonotone(); + requireInvariant totalSupplyIsSumOfVirtualVotingPower(); + requireInvariant sumOfTwoDelegatedVPLTEqTotalVP(); - assert delegatedVotingPower(to) + amount <= totalSupply(); + assert isTotalSupplyGTEqSumOfVotingPower(); + + assert delegatedVotingPower(to) + amount <= totalSupply(); + } } From a73bda183cd40971f7f487aff9634d24ecaae994 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= Date: Wed, 15 Jan 2025 16:46:04 +0100 Subject: [PATCH 07/14] fix: change style --- certora/specs/Delegation.spec | 26 ++++++++++++-------------- 1 file changed, 12 insertions(+), 14 deletions(-) diff --git a/certora/specs/Delegation.spec b/certora/specs/Delegation.spec index 75eb9de..ed76464 100644 --- a/certora/specs/Delegation.spec +++ b/certora/specs/Delegation.spec @@ -227,23 +227,21 @@ rule updatedDelegatedVPLTEqTotalSupply(env e, address to, uint256 amount) { require delegatee(to) != delegatee(e.msg.sender); delegate@withrevert(e, e.msg.sender); + bool reverted = lastReverted; - if (!lastReverted) { + assert delegatee(e.msg.sender) == e.msg.sender && delegatee(e.msg.sender) != 0; - assert delegatee(e.msg.sender) == e.msg.sender && delegatee(e.msg.sender) != 0; + // Safe require that follows from delegatedLTEqDelegateeVP. + require amount <= delegatedVotingPower(e.msg.sender) ; - // Safe require that follows from delegatedLTEqDelegateeVP. - require amount <= delegatedVotingPower(e.msg.sender) ; - - requireInvariant delegatedVotingPowerLTEqTotalVotingPower(); - requireInvariant sumOfVotesStartsAtZero(); - requireInvariant sumOfVotesGrowsCorrectly(); - requireInvariant sumOfVotesMonotone(); - requireInvariant totalSupplyIsSumOfVirtualVotingPower(); - requireInvariant sumOfTwoDelegatedVPLTEqTotalVP(); + requireInvariant delegatedVotingPowerLTEqTotalVotingPower(); + requireInvariant sumOfVotesStartsAtZero(); + requireInvariant sumOfVotesGrowsCorrectly(); + requireInvariant sumOfVotesMonotone(); + requireInvariant totalSupplyIsSumOfVirtualVotingPower(); + requireInvariant sumOfTwoDelegatedVPLTEqTotalVP(); - assert isTotalSupplyGTEqSumOfVotingPower(); + assert isTotalSupplyGTEqSumOfVotingPower(); - assert delegatedVotingPower(to) + amount <= totalSupply(); - } + assert !reverted => delegatedVotingPower(to) + amount <= totalSupply(); } From f6f5b89d72d643d46d6c527c0f68a5ec11dd7d93 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= Date: Wed, 15 Jan 2025 17:05:04 +0100 Subject: [PATCH 08/14] fix: syntax --- certora/specs/Delegation.spec | 37 +++++++++++++++++++---------------- 1 file changed, 20 insertions(+), 17 deletions(-) diff --git a/certora/specs/Delegation.spec b/certora/specs/Delegation.spec index ed76464..37b1c00 100644 --- a/certora/specs/Delegation.spec +++ b/certora/specs/Delegation.spec @@ -227,21 +227,24 @@ rule updatedDelegatedVPLTEqTotalSupply(env e, address to, uint256 amount) { require delegatee(to) != delegatee(e.msg.sender); delegate@withrevert(e, e.msg.sender); - bool reverted = lastReverted; - - assert delegatee(e.msg.sender) == e.msg.sender && delegatee(e.msg.sender) != 0; - - // Safe require that follows from delegatedLTEqDelegateeVP. - require amount <= delegatedVotingPower(e.msg.sender) ; - - requireInvariant delegatedVotingPowerLTEqTotalVotingPower(); - requireInvariant sumOfVotesStartsAtZero(); - requireInvariant sumOfVotesGrowsCorrectly(); - requireInvariant sumOfVotesMonotone(); - requireInvariant totalSupplyIsSumOfVirtualVotingPower(); - requireInvariant sumOfTwoDelegatedVPLTEqTotalVP(); - - assert isTotalSupplyGTEqSumOfVotingPower(); - - assert !reverted => delegatedVotingPower(to) + amount <= totalSupply(); + if (!lastReverted) { + assert delegatee(e.msg.sender) == e.msg.sender && delegatee(e.msg.sender) != 0; + + // Safe require that follows from delegatedLTEqDelegateeVP. + require amount <= delegatedVotingPower(e.msg.sender) ; + + requireInvariant delegatedVotingPowerLTEqTotalVotingPower(); + requireInvariant sumOfVotesStartsAtZero(); + requireInvariant sumOfVotesGrowsCorrectly(); + requireInvariant sumOfVotesMonotone(); + requireInvariant totalSupplyIsSumOfVirtualVotingPower(); + requireInvariant sumOfTwoDelegatedVPLTEqTotalVP(); + + assert isTotalSupplyGTEqSumOfVotingPower(); + + assert delegatedVotingPower(to) + amount <= totalSupply(); + } else { + // Do not check anything + assert true; + } } From f121755090c5ddeb8ec4545d61a6c3569519cc22 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= Date: Thu, 16 Jan 2025 15:47:59 +0100 Subject: [PATCH 09/14] fix: add missing hypothesis in transfer rules --- certora/specs/ERC20.spec | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/certora/specs/ERC20.spec b/certora/specs/ERC20.spec index 319920b..efc2c17 100644 --- a/certora/specs/ERC20.spec +++ b/certora/specs/ERC20.spec @@ -88,9 +88,9 @@ rule transfer(env e) { uint256 otherBalanceBefore = balanceOf(other); // Safe require as it is verified in delegatedLTEqDelegateeVP. - require holderBalanceBefore <= holderVotingPowerBefore; + require delegatee(holder) != 0 => holderBalanceBefore <= holderVotingPowerBefore; // Safe require as it is verified in totalSupplyGTEqSumOfVotingPower. - require delegatee(holder) != delegatee(recipient) => holderBalanceBefore + recipientVotingPowerBefore <= totalSupply(); + require delegatee(holder) != delegatee(recipient) => recipientVotingPowerBefore + holderBalanceBefore <= totalSupply(); // run transaction transfer@withrevert(e, recipient, amount); @@ -133,9 +133,9 @@ rule transferFrom(env e) { uint256 otherBalanceBefore = balanceOf(other); // Safe require as it is verified in delegatedLTEqDelegateeVP. - require holderBalanceBefore <= holderVotingPowerBefore; + require delegatee(holder) != 0 => holderBalanceBefore <= holderVotingPowerBefore; // Safe require as it is verified in totalSupplyGTEqSumOfVotingPower. - require delegatee(holder) != delegatee(recipient) => holderBalanceBefore + recipientVotingPowerBefore <= totalSupply(); + require delegatee(holder) != delegatee(recipient) => recipientVotingPowerBefore + holderBalanceBefore <= totalSupply(); // run transaction transferFrom@withrevert(e, holder, recipient, amount); From fdbcc9753bb268a2ed70029676f121b41dd7ce06 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= Date: Thu, 16 Jan 2025 16:38:38 +0100 Subject: [PATCH 10/14] fix: require statements --- certora/specs/RevertsERC20.spec | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/certora/specs/RevertsERC20.spec b/certora/specs/RevertsERC20.spec index 128a0df..0d4e980 100644 --- a/certora/specs/RevertsERC20.spec +++ b/certora/specs/RevertsERC20.spec @@ -18,7 +18,7 @@ rule transferRevertConditions(env e, address to, uint256 amount) { require delegatee(e.msg.sender) != 0 => senderVotingPowerBefore >= balanceOfSenderBefore; // Safe require that follows from sumOfTwoDelegatedVPLTEqTotalVP() and totalSupplyIsSumOfVirtualVotingPower() and rule updatedDelegatedVPLTEqTotalSupply. - require delegatee(to) != delegatee(e.msg.sender) => recipientVotingPowerBefore + amount <= totalSupply(); + require e.msg.sender != 0 => amount <= balanceOfSenderBefore => delegatee(to) != delegatee(e.msg.sender) => recipientVotingPowerBefore + amount <= totalSupply(); transfer@withrevert(e, to, amount); assert lastReverted <=> e.msg.sender == 0 || to == 0 || balanceOfSenderBefore < amount || e.msg.value != 0; @@ -34,7 +34,7 @@ rule transferFromRevertConditions(env e, address from, address to, uint256 amoun // Safe require as it is verified in delegatedLTEqDelegateeVP. require delegatee(from) != 0 => holderVotingPowerBefore >= balanceOfHolderBefore; // Safe require that follows from sumOfTwoDelegatedVPLTEqTotalVP() and totalSupplyIsSumOfVirtualVotingPower() and rule updatedDelegatedVPLTEqTotalSupply - require delegatee(to) != delegatee(from) => recipientVotingPowerBefore + amount <= totalSupply(); + require from != 0 => amount <= balanceOfHolderBefore => delegatee(to) != delegatee(from) => recipientVotingPowerBefore + amount <= totalSupply(); transferFrom@withrevert(e, from, to, amount); From 389f418fab19f1a688943caf7c5fc2971330637e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= Date: Thu, 16 Jan 2025 17:07:17 +0100 Subject: [PATCH 11/14] fix: repair unsound rule --- certora/specs/Delegation.spec | 47 ++++++++++++++++++----------------- 1 file changed, 24 insertions(+), 23 deletions(-) diff --git a/certora/specs/Delegation.spec b/certora/specs/Delegation.spec index 37b1c00..ba5c3bf 100644 --- a/certora/specs/Delegation.spec +++ b/certora/specs/Delegation.spec @@ -215,36 +215,37 @@ rule delegatingWithSigUpdatesVotingPower(env e, DelegationToken.Delegation deleg } } -// Check that the delegated voting power of a delegatee after an update is lesser than or equal to the total supply of tokens. +// Check that the delegated voting power of a delegatee after a transfer is lesser than or equal to the total supply of tokens. rule updatedDelegatedVPLTEqTotalSupply(env e, address to, uint256 amount) { - // Safe require as implementation woud revert. + // Safe require as the ERC20 implementation woud revert. require amount <= balanceOf(e.msg.sender); - // Safe rquire as zero address can't initiate transactions. + // Safe require as zero address can't initiate transactions. require e.msg.sender != 0; // Safe require as since we consider only updates. require delegatee(to) != delegatee(e.msg.sender); delegate@withrevert(e, e.msg.sender); - if (!lastReverted) { - assert delegatee(e.msg.sender) == e.msg.sender && delegatee(e.msg.sender) != 0; - - // Safe require that follows from delegatedLTEqDelegateeVP. - require amount <= delegatedVotingPower(e.msg.sender) ; - - requireInvariant delegatedVotingPowerLTEqTotalVotingPower(); - requireInvariant sumOfVotesStartsAtZero(); - requireInvariant sumOfVotesGrowsCorrectly(); - requireInvariant sumOfVotesMonotone(); - requireInvariant totalSupplyIsSumOfVirtualVotingPower(); - requireInvariant sumOfTwoDelegatedVPLTEqTotalVP(); - - assert isTotalSupplyGTEqSumOfVotingPower(); - - assert delegatedVotingPower(to) + amount <= totalSupply(); - } else { - // Do not check anything - assert true; - } + + // Show that delegate doesn't always revert. + bool reverted = lastReverted; + satisfy !reverted; + require !reverted; + + assert delegatee(e.msg.sender) == e.msg.sender && delegatee(e.msg.sender) != 0; + + // Safe require that follows from delegatedLTEqDelegateeVP. + require amount <= delegatedVotingPower(e.msg.sender) ; + + requireInvariant delegatedVotingPowerLTEqTotalVotingPower(); + requireInvariant sumOfVotesStartsAtZero(); + requireInvariant sumOfVotesGrowsCorrectly(); + requireInvariant sumOfVotesMonotone(); + requireInvariant totalSupplyIsSumOfVirtualVotingPower(); + requireInvariant sumOfTwoDelegatedVPLTEqTotalVP(); + + assert isTotalSupplyGTEqSumOfVotingPower(); + + assert delegatedVotingPower(to) + amount <= totalSupply(); } From 376c4fded4eafc0b423eba85e085e5cf8583980e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= Date: Thu, 16 Jan 2025 23:12:37 +0100 Subject: [PATCH 12/14] fix: assert delegation doesn't revert --- certora/specs/Delegation.spec | 29 ++++++++++++++--------------- 1 file changed, 14 insertions(+), 15 deletions(-) diff --git a/certora/specs/Delegation.spec b/certora/specs/Delegation.spec index ba5c3bf..d264a09 100644 --- a/certora/specs/Delegation.spec +++ b/certora/specs/Delegation.spec @@ -215,37 +215,36 @@ rule delegatingWithSigUpdatesVotingPower(env e, DelegationToken.Delegation deleg } } -// Check that the delegated voting power of a delegatee after a transfer is lesser than or equal to the total supply of tokens. +// Check that the updated voting power of a delegatee after a transfer is lesser than or equal to the total supply of tokens. rule updatedDelegatedVPLTEqTotalSupply(env e, address to, uint256 amount) { // Safe require as the ERC20 implementation woud revert. require amount <= balanceOf(e.msg.sender); // Safe require as zero address can't initiate transactions. require e.msg.sender != 0; + // Safe require as transfers are non-payable functions. + require e.msg.value == 0; // Safe require as since we consider only updates. require delegatee(to) != delegatee(e.msg.sender); - delegate@withrevert(e, e.msg.sender); + requireInvariant sumOfTwoDelegatedVPLTEqTotalVP(); + assert isTotalSupplyGTEqSumOfVotingPower(); - // Show that delegate doesn't always revert. - bool reverted = lastReverted; - satisfy !reverted; - require !reverted; + // Safe require as zeroVirtualVotingPower accounts for the delegated votes to address zero. + require delegatee(e.msg.sender) == 0 => currentContract._zeroVirtualVotingPower >= balanceOf(e.msg.sender); + + // Safe require as it is proven by delegatedLTEqDelegateeVP. + // The invariant itself can't be required as it's using a parameterized variable. + require delegatee(e.msg.sender) != 0 => delegatedVotingPower(delegatee(e.msg.sender)) >= balanceOf(e.msg.sender); + + delegate@withrevert(e, e.msg.sender); + assert(!lastReverted); assert delegatee(e.msg.sender) == e.msg.sender && delegatee(e.msg.sender) != 0; // Safe require that follows from delegatedLTEqDelegateeVP. require amount <= delegatedVotingPower(e.msg.sender) ; - requireInvariant delegatedVotingPowerLTEqTotalVotingPower(); - requireInvariant sumOfVotesStartsAtZero(); - requireInvariant sumOfVotesGrowsCorrectly(); - requireInvariant sumOfVotesMonotone(); - requireInvariant totalSupplyIsSumOfVirtualVotingPower(); - requireInvariant sumOfTwoDelegatedVPLTEqTotalVP(); - - assert isTotalSupplyGTEqSumOfVotingPower(); - assert delegatedVotingPower(to) + amount <= totalSupply(); } From 65567c20c873a62fcb8ad05586eb13431e77c7f1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= Date: Thu, 16 Jan 2025 23:15:35 +0100 Subject: [PATCH 13/14] docs: improve comment --- certora/specs/RevertsERC20.spec | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/certora/specs/RevertsERC20.spec b/certora/specs/RevertsERC20.spec index 0d4e980..782f007 100644 --- a/certora/specs/RevertsERC20.spec +++ b/certora/specs/RevertsERC20.spec @@ -17,7 +17,7 @@ rule transferRevertConditions(env e, address to, uint256 amount) { // Safe require as it is verified in delegatedLTEqDelegateeVP. require delegatee(e.msg.sender) != 0 => senderVotingPowerBefore >= balanceOfSenderBefore; - // Safe require that follows from sumOfTwoDelegatedVPLTEqTotalVP() and totalSupplyIsSumOfVirtualVotingPower() and rule updatedDelegatedVPLTEqTotalSupply. + // Safe require as it proven in rule updatedDelegatedVPLTEqTotalSupply. require e.msg.sender != 0 => amount <= balanceOfSenderBefore => delegatee(to) != delegatee(e.msg.sender) => recipientVotingPowerBefore + amount <= totalSupply(); transfer@withrevert(e, to, amount); @@ -33,7 +33,7 @@ rule transferFromRevertConditions(env e, address from, address to, uint256 amoun // Safe require as it is verified in delegatedLTEqDelegateeVP. require delegatee(from) != 0 => holderVotingPowerBefore >= balanceOfHolderBefore; - // Safe require that follows from sumOfTwoDelegatedVPLTEqTotalVP() and totalSupplyIsSumOfVirtualVotingPower() and rule updatedDelegatedVPLTEqTotalSupply + // Safe require as it proven in rule updatedDelegatedVPLTEqTotalSupply. require from != 0 => amount <= balanceOfHolderBefore => delegatee(to) != delegatee(from) => recipientVotingPowerBefore + amount <= totalSupply(); transferFrom@withrevert(e, from, to, amount); From 06b6407b16f39bb7b8e45ba12cf0d3f8b2bb2e21 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= Date: Mon, 20 Jan 2025 16:23:43 +0100 Subject: [PATCH 14/14] fix: usage and docs of rule --- certora/specs/Delegation.spec | 21 +++++++-------------- certora/specs/RevertsERC20.spec | 17 ++++++++++++++--- 2 files changed, 21 insertions(+), 17 deletions(-) diff --git a/certora/specs/Delegation.spec b/certora/specs/Delegation.spec index d264a09..6c46d18 100644 --- a/certora/specs/Delegation.spec +++ b/certora/specs/Delegation.spec @@ -217,34 +217,27 @@ rule delegatingWithSigUpdatesVotingPower(env e, DelegationToken.Delegation deleg // Check that the updated voting power of a delegatee after a transfer is lesser than or equal to the total supply of tokens. rule updatedDelegatedVPLTEqTotalSupply(env e, address to, uint256 amount) { - // Safe require as the ERC20 implementation woud revert. - require amount <= balanceOf(e.msg.sender); - - // Safe require as zero address can't initiate transactions. - require e.msg.sender != 0; - // Safe require as transfers are non-payable functions. require e.msg.value == 0; + require e.msg.sender != 0; - // Safe require as since we consider only updates. + require amount <= balanceOf(e.msg.sender); require delegatee(to) != delegatee(e.msg.sender); requireInvariant sumOfTwoDelegatedVPLTEqTotalVP(); assert isTotalSupplyGTEqSumOfVotingPower(); - // Safe require as zeroVirtualVotingPower accounts for the delegated votes to address zero. + // This require avoids an impossible revert as zeroVirtualVotingPower operations comme from munging. require delegatee(e.msg.sender) == 0 => currentContract._zeroVirtualVotingPower >= balanceOf(e.msg.sender); - // Safe require as it is proven by delegatedLTEqDelegateeVP. - // The invariant itself can't be required as it's using a parameterized variable. + // This invariant can't be required as it's using a parameterized variable. + // But it is proven by delegatedLTEqDelegateeVP. require delegatee(e.msg.sender) != 0 => delegatedVotingPower(delegatee(e.msg.sender)) >= balanceOf(e.msg.sender); delegate@withrevert(e, e.msg.sender); - assert(!lastReverted); - assert delegatee(e.msg.sender) == e.msg.sender && delegatee(e.msg.sender) != 0; + assert(!lastReverted); - // Safe require that follows from delegatedLTEqDelegateeVP. - require amount <= delegatedVotingPower(e.msg.sender) ; + assert delegatee(e.msg.sender) == e.msg.sender; assert delegatedVotingPower(to) + amount <= totalSupply(); } diff --git a/certora/specs/RevertsERC20.spec b/certora/specs/RevertsERC20.spec index 782f007..e87281d 100644 --- a/certora/specs/RevertsERC20.spec +++ b/certora/specs/RevertsERC20.spec @@ -16,9 +16,14 @@ rule transferRevertConditions(env e, address to, uint256 amount) { // Safe require as it is verified in delegatedLTEqDelegateeVP. require delegatee(e.msg.sender) != 0 => senderVotingPowerBefore >= balanceOfSenderBefore; + // Safe require as it is verified in sumOfTwoDelegatedVPLTEqTotalVP. + require senderVotingPowerBefore + recipientVotingPowerBefore <= totalSupply(); // Safe require as it proven in rule updatedDelegatedVPLTEqTotalSupply. - require e.msg.sender != 0 => amount <= balanceOfSenderBefore => delegatee(to) != delegatee(e.msg.sender) => recipientVotingPowerBefore + amount <= totalSupply(); + require + e.msg.sender != 0 => e.msg.value == 0 => + amount <= balanceOfSenderBefore => + delegatee(to) != delegatee(e.msg.sender) => recipientVotingPowerBefore + amount <= totalSupply(); transfer@withrevert(e, to, amount); assert lastReverted <=> e.msg.sender == 0 || to == 0 || balanceOfSenderBefore < amount || e.msg.value != 0; @@ -33,15 +38,21 @@ rule transferFromRevertConditions(env e, address from, address to, uint256 amoun // Safe require as it is verified in delegatedLTEqDelegateeVP. require delegatee(from) != 0 => holderVotingPowerBefore >= balanceOfHolderBefore; + // Safe require as it is verified in sumOfTwoDelegatedVPLTEqTotalVP. + require holderVotingPowerBefore + recipientVotingPowerBefore <= totalSupply(); + // Safe require as it proven in rule updatedDelegatedVPLTEqTotalSupply. - require from != 0 => amount <= balanceOfHolderBefore => delegatee(to) != delegatee(from) => recipientVotingPowerBefore + amount <= totalSupply(); + require + from != 0 => e.msg.value == 0 => + amount <= balanceOfHolderBefore => + delegatee(to) != delegatee(from) => recipientVotingPowerBefore + amount <= totalSupply(); transferFrom@withrevert(e, from, to, amount); bool generalRevertConditions = from == 0 || to == 0 || balanceOfHolderBefore < amount || e.msg.value != 0; if (allowanceOfSenderBefore != max_uint256) { - assert lastReverted <=> e.msg.sender == 0 || allowanceOfSenderBefore < amount || generalRevertConditions; + assert lastReverted <=> e.msg.sender == 0 || allowanceOfSenderBefore < amount || generalRevertConditions; } else { assert lastReverted <=> generalRevertConditions; }