From f53d88d91efa7b48557af6f8353e8616600fb806 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= Date: Mon, 9 Dec 2024 15:35:39 +0100 Subject: [PATCH] Revert "chore: update specs" This reverts commit 94fef53c70387af12e07e830685f67c5fdd127cf. --- certora/confs/RevertsMintBurnEthereum.conf | 7 +++---- certora/confs/RevertsMintBurnOptimism.conf | 7 +++---- certora/specs/RevertsMintBurnEthereum.spec | 24 ++++++++-------------- certora/specs/RevertsMintBurnOptimism.spec | 20 ++++++------------ 4 files changed, 20 insertions(+), 38 deletions(-) diff --git a/certora/confs/RevertsMintBurnEthereum.conf b/certora/confs/RevertsMintBurnEthereum.conf index 586b14c..44d9375 100644 --- a/certora/confs/RevertsMintBurnEthereum.conf +++ b/certora/confs/RevertsMintBurnEthereum.conf @@ -1,13 +1,12 @@ { "files": [ - "certora/helpers/MorphoTokenEthereumHarness.sol", - "certora/helpers/MorphoTokenOptimismHarness.sol" + "src/MorphoTokenEthereum.sol" ], "parametric_contracts": [ - "MorphoTokenEthereumHarness" + "MorphoTokenEthereum" ], "solc": "solc-0.8.27", - "verify": "MorphoTokenEthereumHarness:certora/specs/RevertsMintBurnEthereum.spec", + "verify": "MorphoTokenEthereum:certora/specs/RevertsMintBurnEthereum.spec", "rule_sanity": "basic", "server": "production", "packages": [ diff --git a/certora/confs/RevertsMintBurnOptimism.conf b/certora/confs/RevertsMintBurnOptimism.conf index 75a27fd..dce299b 100644 --- a/certora/confs/RevertsMintBurnOptimism.conf +++ b/certora/confs/RevertsMintBurnOptimism.conf @@ -1,13 +1,12 @@ { "files": [ - "certora/helpers/MorphoTokenEthereumHarness.sol", - "certora/helpers/MorphoTokenOptimismHarness.sol" + "src/MorphoTokenOptimism.sol" ], "parametric_contracts": [ - "MorphoTokenOptimismHarness" + "MorphoTokenOptimism" ], "solc": "solc-0.8.27", - "verify": "MorphoTokenOptimismHarness:certora/specs/RevertsMintBurnOptimism.spec", + "verify": "MorphoTokenOptimism:certora/specs/RevertsMintBurnOptimism.spec", "rule_sanity": "basic", "server": "production", "packages": [ diff --git a/certora/specs/RevertsMintBurnEthereum.spec b/certora/specs/RevertsMintBurnEthereum.spec index 94772b0..63a1d1f 100644 --- a/certora/specs/RevertsMintBurnEthereum.spec +++ b/certora/specs/RevertsMintBurnEthereum.spec @@ -1,7 +1,5 @@ // SPDX-License-Identifier: GPL-2.0-or-later -import "Delegation.spec"; - methods { function owner() external returns address envfree; function totalSupply() external returns uint256 envfree; @@ -12,17 +10,15 @@ methods { // Check the revert conditions for the burn function. rule mintRevertConditions(env e, address to, uint256 amount) { - requireInvariant zeroAddressNoVotingPower(); - assert isTotalSupplyGTEqSumOfVotingPower(); mathint totalSupplyBefore = totalSupply(); uint256 balanceOfSenderBefore = balanceOf(e.msg.sender); uint256 toVotingPowerBefore = delegatedVotingPower(delegatee(to)); - // Safe require because if the delegatee is not zero the recipient's delegatee's voting power is lesser than or equal to the total supply of tokens. - require delegatee(to) != 0 => toVotingPowerBefore <= totalSupply(); + // Safe require as zero address can't possibly delegate voting power. + require delegatee(0) == 0; - // Safe require thats avoid absurd counter-examples introduced by munging the sources. - require toVotingPowerBefore <= sumOfVotingPower; + // Safe require because if the delegatee is not zero the recipient's delegatee's voting power is lesser than or equal to the total supply of tokens + require delegatee(to) != 0 => toVotingPowerBefore <= totalSupply(); mint@withrevert(e, to, amount); assert lastReverted <=> e.msg.sender != owner() || to == 0 || e.msg.value != 0 || totalSupplyBefore + amount > max_uint256; @@ -30,18 +26,14 @@ rule mintRevertConditions(env e, address to, uint256 amount) { // Check the revert conditions for the burn function. rule burnRevertConditions(env e, uint256 amount) { - requireInvariant zeroAddressNoVotingPower(); - assert isTotalSupplyGTEqSumOfVotingPower(); - uint256 balanceOfSenderBefore = balanceOf(e.msg.sender); uint256 delegateeVotingPowerBefore = delegatedVotingPower(delegatee(e.msg.sender)); - // Safe requires because a holder's balance is added to the delegatee's voting power upon delegation. - require delegatee(e.msg.sender) != 0 => balanceOfSenderBefore <= delegateeVotingPowerBefore; + // Safe require as zero address can't possibly delegate voting power. + require delegatee(0) == 0; - // Safe requires thats avoid absurd counter-examples introduced by munging the sources. - require delegateeVotingPowerBefore <= sumOfVotingPower; - require amount <= delegateeVotingPowerBefore; + // Safe require because a holder's balance is added to the delegatee's voting power upon delegation. + 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 54fa5dc..5d2b1fe 100644 --- a/certora/specs/RevertsMintBurnOptimism.spec +++ b/certora/specs/RevertsMintBurnOptimism.spec @@ -1,7 +1,5 @@ // SPDX-License-Identifier: GPL-2.0-or-later -import "Delegation.spec"; - methods { function totalSupply() external returns uint256 envfree; function balanceOf(address) external returns uint256 envfree; @@ -11,36 +9,30 @@ methods { // Check the revert conditions for the mint function. rule mintRevertConditions(env e, address to, uint256 amount) { - requireInvariant zeroAddressNoVotingPower(); - assert isTotalSupplyGTEqSumOfVotingPower(); mathint totalSupplyBefore = totalSupply(); uint256 toVotingPowerBefore = delegatedVotingPower(delegatee(to)); + // Safe require as zero address can't possibly delegate voting power. + require delegatee(0) == 0; + // Safe require because if the delegatee is not zero the recipient's delegatee's voting power is lesser than or equal to the total supply of tokens require delegatee(to) != 0 => toVotingPowerBefore <= totalSupply(); - // Safe require thats avoid absurd counter-examples introduced by munging the sources. - require toVotingPowerBefore <= sumOfVotingPower; - - mint@withrevert(e, to, amount); assert lastReverted <=> e.msg.sender != currentContract.bridge || to == 0 || e.msg.value != 0 || totalSupplyBefore + amount > max_uint256; } // Check the revert conditions for the burn function. rule burnRevertConditions(env e, address from, uint256 amount) { - requireInvariant zeroAddressNoVotingPower(); - assert isTotalSupplyGTEqSumOfVotingPower(); uint256 balanceOfFromBefore = balanceOf(from); uint256 fromVotingPowerBefore = delegatedVotingPower(delegatee(from)); + // Safe require as zero address can't possibly delegate voting power. + require delegatee(0) == 0; + // Safe require because a holder's balance is added to the delegatee's voting power upon delegation. require delegatee(from) != 0 => fromVotingPowerBefore >= balanceOfFromBefore; - // Safe requires thats avoid absurd counter-examples introduced by munging the sources. - require fromVotingPowerBefore <= sumOfVotingPower; - require amount <= fromVotingPowerBefore; - burn@withrevert(e, from, amount); assert lastReverted <=> e.msg.sender != currentContract.bridge || from == 0 || balanceOfFromBefore < amount || e.msg.value != 0; }