Merge pull request #390 from morpho-org/certora/reverts

[Certora] Reverts
morpho-org · Jan 17, 2024 · 74284aa · 74284aa
2 parents cf0bb56 + 0c2438f
commit 74284aa
Show file tree

Hide file tree

Showing 5 changed files with 417 additions and 9 deletions.
diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
@@ -17,6 +17,7 @@ jobs:
       matrix:
         conf:
           - ConsistentState
+          - Reverts
           - Roles
 
     steps:
@@ -30,7 +31,13 @@ jobs:
       - name: Install certora
         run: pip install certora-cli-beta
 
-      - name: Install solc
+      - name: Install solc (0.8.19)
+        run: |
+          wget https://github.com/ethereum/solidity/releases/download/v0.8.19/solc-static-linux
+          chmod +x solc-static-linux
+          sudo mv solc-static-linux /usr/local/bin/solc8.19
+
+      - name: Install solc (0.8.21)
         run: |
           wget https://github.com/ethereum/solidity/releases/download/v0.8.21/solc-static-linux
           chmod +x solc-static-linux

diff --git a/certora/confs/Reverts.conf b/certora/confs/Reverts.conf
@@ -0,0 +1,25 @@
+{
+    "files": [
+        "lib/morpho-blue/certora/harness/MorphoHarness.sol",
+        "certora/harness/MetaMorphoHarness.sol",
+        "certora/dispatch/ERC20Standard.sol",
+    ],
+    "solc_map": {
+        "MorphoHarness": "solc8.19",
+        "MetaMorphoHarness": "solc",
+        "ERC20Standard": "solc",
+    },
+    "link": [
+        "MetaMorphoHarness:MORPHO=MorphoHarness",
+    ],
+    "verify": "MetaMorphoHarness:certora/specs/Reverts.spec",
+    "optimistic_loop": true,
+    "prover_args": [
+        "-depth 3",
+        "-mediumTimeout 20",
+        "-timeout 120",
+    ],
+    "rule_sanity": "basic",
+    "server": "production",
+    "msg": "MetaMorpho Reverts"
+}
diff --git a/certora/harness/MetaMorphoHarness.sol b/certora/harness/MetaMorphoHarness.sol
@@ -13,6 +13,14 @@ contract MetaMorphoHarness is MetaMorpho {
         string memory _symbol
     ) MetaMorpho(owner, morpho, initialTimelock, _asset, _name, _symbol) {}
 
+    function balanceOf(address token, address user) external view returns (uint256) {
+        return IERC20(token).balanceOf(user);
+    }
+
+    function totalSupply(address token) external view returns (uint256) {
+        return IERC20(token).totalSupply();
+    }
+
     function minTimelock() external view returns (uint256) {
         return ConstantsLib.MIN_TIMELOCK;
     }

diff --git a/certora/specs/ConsistentState.spec b/certora/specs/ConsistentState.spec
@@ -3,19 +3,20 @@ methods {
     function multicall(bytes[]) external returns(bytes[]) => NONDET DELETE;
 
     function pendingTimelock() external returns(uint192, uint64) envfree;
-    function timelock() external returns (uint256) envfree;
-    function guardian() external returns (address) envfree;
+    function timelock() external returns(uint256) envfree;
+    function guardian() external returns(address) envfree;
     function pendingGuardian() external returns(address, uint64) envfree;
     function pendingCap(MetaMorphoHarness.Id) external returns(uint192, uint64) envfree;
     function config(MetaMorphoHarness.Id) external returns(uint184, bool, uint64) envfree;
     function supplyQueueLength() external returns(uint256) envfree;
     function withdrawQueueLength() external returns(uint256) envfree;
-    function fee() external returns (uint96) envfree;
+    function fee() external returns(uint96) envfree;
+    function feeRecipient() external returns(address) envfree;
 
-    function minTimelock() external returns (uint256) envfree;
-    function maxTimelock() external returns (uint256) envfree;
-    function maxQueueLength() external returns (uint256) envfree;
-    function maxFee() external returns (uint256) envfree;
+    function minTimelock() external returns(uint256) envfree;
+    function maxTimelock() external returns(uint256) envfree;
+    function maxQueueLength() external returns(uint256) envfree;
+    function maxFee() external returns(uint256) envfree;
 }
 
 invariant feeInRange()
@@ -32,8 +33,12 @@ function isPendingTimelockInRange() returns bool {
 invariant pendingTimelockInRange()
     isPendingTimelockInRange();
 
+function isTimelockInRange() returns bool {
+    return timelock() <= maxTimelock() && timelock() >= minTimelock();
+}
+
 invariant timelockInRange()
-    timelock() <= maxTimelock() && timelock() >= minTimelock()
+    isTimelockInRange()
 {
     preserved {
         requireInvariant pendingTimelockInRange();
@@ -138,3 +143,17 @@ function isDifferentPendingGuardian() returns bool {
 
 invariant differentPendingGuardian()
     isDifferentPendingGuardian();
+
+invariant noFeeToUnsetFeeRecipient()
+    feeRecipient() == 0 => fee() == 0;
+
+function hasSupplyCapIsEnabled(MetaMorphoHarness.Id id) returns bool {
+    uint192 supplyCap;
+    bool enabled;
+    supplyCap, enabled, _ = config(id);
+
+    return supplyCap > 0 => enabled;
+}
+
+invariant supplyCapIsEnabled(MetaMorphoHarness.Id id)
+    hasSupplyCapIsEnabled(id);