[Certora] Check Missing Reverts

.github/workflows/certora.yml

@@ -24,6 +24,10 @@ jobs:
           - ERC20Optimism
           - ExternalCallsEthereum
           - ExternalCallsOptimism
+          - RevertsERC20Ethereum
+          - RevertsERC20Optimism
+          - RevertsMintBurnEthereum
+          - RevertsMintBurnOptimism
 
     steps:
       - uses: actions/checkout@v4

certora/README.md

@@ -38,6 +38,10 @@ This is checked in [`ERC20.spec`](specs/ERC20.spec) and [`ERC20Invariants.spec`]
 
 This is checked in [`Delegation.spec`](specs/Delegation.spec).
 
+### Reverts
+
+This is checks in [`RevertsERC20.spec`](specs/RevertsERC20.spec), [`RevertsMintBurnEthereum.spec`](specs/RevertsMintBurnEthereum.spec) and [`RevertsMintBurnOptimism.spec`](specs/RevertsMintBurnOptimism.spec).
+
 ## Verification architecture
 
 ### Folders and file structure
@@ -48,6 +52,7 @@ The [`certora/specs`](specs) folder contains the following files:
 - [`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.
+- [`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.
 

certora/confs/RevertsERC20Ethereum.conf

@@ -0,0 +1,18 @@
+{
+  "files": [
+    "src/MorphoTokenEthereum.sol"
+  ],
+  "parametric_contracts": [
+    "MorphoTokenEthereum"
+  ],
+  "solc": "solc-0.8.27",
+  "verify": "MorphoTokenEthereum:certora/specs/RevertsERC20.spec",
+  "rule_sanity": "basic",
+  "server": "production",
+  "packages": [
+    "@openzeppelin/contracts/=lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/contracts"
+  ],
+  "loop_iter": "3",
+  "optimistic_loop": true,
+  "msg": "Morpho token ERC20 Reverts Ethereum"
+}

certora/confs/RevertsERC20Optimism.conf

@@ -0,0 +1,18 @@
+{
+  "files": [
+    "src/MorphoTokenOptimism.sol"
+  ],
+  "parametric_contracts": [
+    "MorphoTokenOptimism"
+  ],
+  "solc": "solc-0.8.27",
+  "verify": "MorphoTokenOptimism:certora/specs/RevertsERC20.spec",
+  "rule_sanity": "basic",
+  "server": "production",
+  "packages": [
+    "@openzeppelin/contracts/=lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/contracts"
+  ],
+  "loop_iter": "3",
+  "optimistic_loop": true,
+  "msg": "Morpho token ERC20 Reverts Optimism"
+}

certora/confs/RevertsMintBurnEthereum.conf

@@ -0,0 +1,18 @@
+{
+  "files": [
+    "src/MorphoTokenEthereum.sol"
+  ],
+  "parametric_contracts": [
+    "MorphoTokenEthereum"
+  ],
+  "solc": "solc-0.8.27",
+  "verify": "MorphoTokenEthereum:certora/specs/RevertsMintBurnEthereum.spec",
+  "rule_sanity": "basic",
+  "server": "production",
+  "packages": [
+    "@openzeppelin/contracts/=lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/contracts"
+  ],
+  "loop_iter": "3",
+  "optimistic_loop": true,
+  "msg": "Morpho token ERC20 Mint Burn Reverts"
+}

certora/confs/RevertsMintBurnOptimism.conf

@@ -0,0 +1,18 @@
+{
+  "files": [
+    "src/MorphoTokenOptimism.sol"
+  ],
+  "parametric_contracts": [
+    "MorphoTokenOptimism"
+  ],
+  "solc": "solc-0.8.27",
+  "verify": "MorphoTokenOptimism:certora/specs/RevertsMintBurnOptimism.spec",
+  "rule_sanity": "basic",
+  "server": "production",
+  "packages": [
+    "@openzeppelin/contracts/=lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/contracts"
+  ],
+  "loop_iter": "3",
+  "optimistic_loop": true,
+  "msg": "Morpho token ERC20 Mint Burn Reverts"
+}

certora/specs/RevertsERC20.spec

@@ -0,0 +1,54 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+
+methods {
+    function totalSupply() external returns uint256 envfree;
+    function balanceOf(address) external returns uint256 envfree;
+    function allowance(address, address) external returns uint256 envfree;
+    function delegatee(address) external returns address envfree;
+    function delegatedVotingPower(address) external returns uint256 envfree;
+}
+
+// Check the revert conditions for the transfer function.
+rule transferRevertConditions(env e, address to, uint256 amount) {
+    uint256 balanceOfSenderBefore = balanceOf(e.msg.sender);
+    uint256 senderVotingPowerBefore = delegatedVotingPower(delegatee(e.msg.sender));
+    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();
+
+    transfer@withrevert(e, to, amount);
+    assert lastReverted <=> e.msg.sender == 0 || to == 0 || balanceOfSenderBefore < amount || e.msg.value != 0;
+}
+
+// Check the revert conditions for the transferFrom function.
+rule transferFromRevertConditions(env e, address from, address to, uint256 amount) {
+    uint256 allowanceOfSenderBefore = allowance(from, e.msg.sender);
+    uint256 balanceOfHolderBefore = balanceOf(from);
+    uint256 holderVotingPowerBefore = delegatedVotingPower(delegatee(from));
+    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();
+
+    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;
+    } else {
+        assert lastReverted <=> generalRevertConditions;
+    }
+
+}
+
+// Check the revert conditions for the approve function.
+rule approveRevertConditions(env e, address to, uint256 value) {
+    approve@withrevert(e, to, value);
+    assert lastReverted <=> e.msg.sender == 0 || to == 0 || e.msg.value != 0;
+}

certora/specs/RevertsMintBurnEthereum.spec

@@ -0,0 +1,40 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+
+methods {
+    function owner() external returns address envfree;
+    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;
+}
+
+// Check the revert conditions for the burn function.
+rule mintRevertConditions(env e, address to, uint256 amount) {
+    mathint totalSupplyBefore = totalSupply();
+    uint256 balanceOfSenderBefore = balanceOf(e.msg.sender);
+    uint256 toVotingPowerBefore = delegatedVotingPower(delegatee(to));
+
+    // Safe require as zero address can't possibly delegate voting power which is verified in zeroAddressNoVotingPower .
+    require delegatee(0) == 0;
+
+    // Safe require as it is verified in totalSupplyGTEqSumOfVotingPower.
+    require toVotingPowerBefore <= totalSupply();
+
+    mint@withrevert(e, to, amount);
+    assert lastReverted <=> e.msg.sender != owner() || to == 0 || e.msg.value != 0 || totalSupplyBefore + amount > max_uint256;
+}
+
+// Check the revert conditions for the burn function.
+rule burnRevertConditions(env e, uint256 amount) {
+    uint256 balanceOfSenderBefore = balanceOf(e.msg.sender);
+    uint256 delegateeVotingPowerBefore = delegatedVotingPower(delegatee(e.msg.sender));
+
+    // Safe require as zero address can't possibly delegate voting power which is verified in zeroAddressNoVotingPower .
+    require delegatee(0) == 0;
+
+    // Safe require as it is verified in delegatedLTEqDelegateeVP.
+    require delegateeVotingPowerBefore >= balanceOfSenderBefore;
+
+    burn@withrevert(e, amount);
+    assert lastReverted <=> e.msg.sender == 0 || balanceOfSenderBefore < amount || e.msg.value != 0;
+}

certora/specs/RevertsMintBurnOptimism.spec

@@ -0,0 +1,38 @@
+// 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;
+}
+
+// Check the revert conditions for the mint function.
+rule mintRevertConditions(env e, address to, uint256 amount) {
+    mathint totalSupplyBefore = totalSupply();
+    uint256 toVotingPowerBefore = delegatedVotingPower(delegatee(to));
+
+    // Safe require as zero address can't possibly delegate voting power which is verified in zeroAddressNoVotingPower.
+    require delegatee(0) == 0;
+
+    // Safe require as it is verified in totalSupplyGTEqSumOfVotingPower.
+    require toVotingPowerBefore <= totalSupply();
+
+    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) {
+    uint256 balanceOfFromBefore = balanceOf(from);
+    uint256 fromVotingPowerBefore = delegatedVotingPower(delegatee(from));
+
+    // Safe require as zero address can't possibly delegate voting power which is verified in zeroAddressNoVotingPower.
+    require delegatee(0) == 0;
+
+    // Safe require as it is verified in delegatedLTEqDelegateeVP.
+    require fromVotingPowerBefore >= balanceOfFromBefore;
+
+    burn@withrevert(e, from, amount);
+    assert lastReverted <=> e.msg.sender != currentContract.bridge || from == 0 || balanceOfFromBefore < amount ||  e.msg.value != 0;
+}