fix: address PR review

morpho-org · Oct 30, 2024 · 02d514d · 02d514d
1 parent e997f43
commit 02d514d
Show file tree

Hide file tree

Showing 10 changed files with 12 additions and 6 deletions.
diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
@@ -41,7 +41,7 @@ jobs:
         run: |
           wget https://github.com/ethereum/solidity/releases/download/v0.8.24/solc-static-linux
           chmod +x solc-static-linux
-          sudo mv solc-static-linux /usr/local/bin/solc
+          sudo mv solc-static-linux /usr/local/bin/solc-0.8.24
 
       - name: Verify ${{ matrix.conf }} specification
         run: certoraRun certora/confs/${{ matrix.conf }}.conf

diff --git a/certora/README.md b/certora/README.md
@@ -10,7 +10,7 @@ This folder contains the [CVL](https://docs.certora.com/en/latest/docs/cvl/index
 - [CompoundV3MigrationBundlerV2](../src/migration/CompoundV3MigrationBundlerV2.sol)
 - [EthereumBundlerV2](../src/ethereum/EthereumBundlerV2.sol)
 
-## Getting Started
+## Getting started
 
 To verify a specification, run the command `certoraRun Spec.conf` where `Spec.conf` is one of the configuration files in [`certora/confs`](confs).
 
@@ -19,7 +19,7 @@ You must have set the `CERTORAKEY` environment variable to a valid Certora key.
 ## Overview
 
 Bundler methods used during a bundle execution have the `protected` modifier. This modifier ensures that:
-- An initiator has been set, and
+- an initiator has been set;
 - the caller is the bundle initiator or the Morpho contract.
 
 The `Protected.spec` file checks that all bundler functions, except noted exceptions, respect the requirements of the `protected` modifier when an initiator has been set.

diff --git a/certora/confs/AaveV2MigrationBundlerV2.conf b/certora/confs/AaveV2MigrationBundlerV2.conf
@@ -2,6 +2,7 @@
   "files": [
     "src/migration/AaveV2MigrationBundlerV2.sol"
   ],
+  "solc": "solc-0.8.24",
   "verify": "AaveV2MigrationBundlerV2:certora/specs/Protected.spec",
   "rule_sanity": "basic",
   "server": "production",

diff --git a/certora/confs/AaveV3MigrationBundlerV2.conf b/certora/confs/AaveV3MigrationBundlerV2.conf
@@ -2,6 +2,7 @@
   "files": [
     "src/migration/AaveV3MigrationBundlerV2.sol"
   ],
+  "solc": "solc-0.8.24",
   "verify": "AaveV3MigrationBundlerV2:certora/specs/Protected.spec",
   "rule_sanity": "basic",
   "server": "production",

diff --git a/certora/confs/AaveV3OptimizerMigrationBundlerV2.conf b/certora/confs/AaveV3OptimizerMigrationBundlerV2.conf
@@ -2,6 +2,7 @@
   "files": [
     "src/migration/AaveV3OptimizerMigrationBundlerV2.sol"
   ],
+  "solc": "solc-0.8.24",
   "verify": "AaveV3OptimizerMigrationBundlerV2:certora/specs/Protected.spec",
   "rule_sanity": "basic",
   "server": "production",

diff --git a/certora/confs/ChainAgnosticBundlerV2.conf b/certora/confs/ChainAgnosticBundlerV2.conf
@@ -2,6 +2,7 @@
   "files": [
     "src/chain-agnostic/ChainAgnosticBundlerV2.sol"
   ],
+  "solc": "solc-0.8.24",
   "verify": "ChainAgnosticBundlerV2:certora/specs/Protected.spec",
   "rule_sanity": "basic",
   "server": "production",

diff --git a/certora/confs/CompoundV2MigrationBundlerV2.conf b/certora/confs/CompoundV2MigrationBundlerV2.conf
@@ -2,6 +2,7 @@
   "files": [
     "src/migration/CompoundV2MigrationBundlerV2.sol"
   ],
+  "solc": "solc-0.8.24",
   "verify": "CompoundV2MigrationBundlerV2:certora/specs/Protected.spec",
   "rule_sanity": "basic",
   "server": "production",

diff --git a/certora/confs/CompoundV3MigrationBundlerV2.conf b/certora/confs/CompoundV3MigrationBundlerV2.conf
@@ -2,6 +2,7 @@
   "files": [
     "src/migration/CompoundV3MigrationBundlerV2.sol"
   ],
+  "solc": "solc-0.8.24",
   "verify": "CompoundV3MigrationBundlerV2:certora/specs/Protected.spec",
   "rule_sanity": "basic",
   "server": "production",

diff --git a/certora/confs/EthereumBundlerV2.conf b/certora/confs/EthereumBundlerV2.conf
@@ -2,6 +2,7 @@
   "files": [
     "src/ethereum/EthereumBundlerV2.sol"
   ],
+  "solc": "solc-0.8.24",
   "verify": "EthereumBundlerV2:certora/specs/Protected.spec",
   "rule_sanity": "basic",
   "server": "production",

diff --git a/certora/specs/Protected.spec b/certora/specs/Protected.spec
@@ -13,8 +13,7 @@ rule protectedWithSetInitiator(method f, env e, calldataarg data) filtered {
     f -> !f.isView && !f.isFallback && f.selector != sig:multicall(bytes[]).selector
 }
 {
-    require e.msg.sender != initiator();
-    require e.msg.sender != MORPHO();
     f@withrevert(e,data);
-    assert lastReverted;
+    bool reverted = lastReverted;
+    assert e.msg.sender != initiator() && e.msg.sender != MORPHO() => reverted;
 }