[Certora] Check Missing Reverts

.github/workflows/certora.yml

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

certora/README.md

@@ -28,14 +28,18 @@ This is checked in [`ExternalCalls.spec`](specs/ExternalCalls.spec).
 
 This is checked in [`ERC20.spec`](specs/ERC20.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
 
 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;
-- [`ERC20.spec`](specs/ERC20.spec) ensure that the Morpho token is compliant with the [ERC20](https://eips.ethereum.org/EIPS/eip-20) specification.
-
+- [`ERC20.spec`](specs/ERC20.spec) ensure that the Morpho token is compliant with the [ERC20](https://eips.ethereum.org/EIPS/eip-20) specification;
+- [`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,38 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+
+methods {
+    function balanceOf(address) external returns uint256 envfree;
+    function allowance(address, address) external returns uint256 envfree;
+
+    // Avoids checking delegation related overflows.
+    function _._moveDelegateVotes(address, address, uint256) internal => CONSTANT;
+}
+
+// Check the revert conditions for the transfer function.
+rule transferRevertConditions(env e, address to, uint256 amount) {
+    uint256 balanceOfSenderBefore = balanceOf(e.msg.sender);
+
+    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 balanceOfFromBefore = balanceOf(from);
+
+    transferFrom@withrevert(e, from, to, amount);
+    bool generalRevertConditions = from == 0 || to == 0 || balanceOfFromBefore < 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,27 @@
+// 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;
+
+    // Avoids checking delegation related overflows.
+    function _._moveDelegateVotes(address, address, uint256) internal => CONSTANT;
+}
+
+// Check the revert conditions for the burn function.
+rule mintRevertConditions(env e, address to, uint256 amount) {
+    mathint totalSupplyBefore = 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, address from, uint256 amount) {
+    uint256 balanceOfSenderBefore = balanceOf(e.msg.sender);
+    require e.msg.value == 0 ;
+
+    burn@withrevert(e, amount);
+    assert lastReverted <=> e.msg.sender == 0 || balanceOfSenderBefore < amount || e.msg.value != 0;
+}

certora/specs/RevertsMintBurnOptimism.spec

@@ -0,0 +1,24 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+
+methods {
+    function totalSupply() external returns uint256 envfree;
+    function balanceOf(address) external returns uint256 envfree;
+
+    // Avoids checking delegation related overflows.
+    function _._moveDelegateVotes(address, address, uint256) internal => CONSTANT;
+}
+
+// Check the revert conditions for the mint function.
+rule mintRevertConditions(env e, address to, uint256 amount) {
+    mathint totalSupplyBefore = 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);
+    burn@withrevert(e, from, amount);
+    assert lastReverted <=> e.msg.sender != currentContract.bridge || from == 0 || balanceOfFromBefore < amount ||  e.msg.value != 0;
+}