docs: add README.md & docs, fix workflow file

.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-0.8.24
+          sudo mv solc-static-linux /usr/local/bin/solc
 
       - name: Verify ${{ matrix.conf }} specification
         run: certoraRun certora/confs/${{ matrix.conf }}.conf

certora/README.md

@@ -0,0 +1,35 @@
+# Bundlers Formal Verification
+
+This folder contains the [CVL](https://docs.certora.com/en/latest/docs/cvl/index.html) specification and verification setup for the following bundler contracts:
+
+- [AaveV2MigrationBundlerV2](../src/migration/AaveV2MigrationBundlerV2.sol)
+- [AaveV3MigrationBundlerV2](../src/migration/AaveV3MigrationBundlerV2.sol)
+- [AaveV3OptimizerMigrationBundlerV2](../src/migration/AaveV3OptimizerMigrationBundlerV2.sol)
+- [ChainAgnosticBundlerV2](../src/chain-agnostic/ChainAgnosticBundlerV2.sol)
+- [CompoundV2MigrationBundlerV2](../src/migration/CompoundV2MigrationBundlerV2.sol)
+- [CompoundV3MigrationBundlerV2](../src/migration/CompoundV3MigrationBundlerV2.sol)
+- [EthereumBundlerV2](../src/ethereum/EthereumBundlerV2.sol)
+
+## 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).
+
+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
+- 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.
+
+## Verification architecture
+
+### Folders and file structure
+
+The [`certora/specs`](specs) folder contains the following files:
+
+- [`Protected.spec`](specs/Protected.spec) checks that all methods except noted exceptions respect the `protected` modifier when an initiator has been set.
+
+The [`certora/confs`](confs) folder contains a configuration file for each deployed bundler.

certora/specs/Protected.spec

@@ -8,7 +8,11 @@ methods {
 }
 
 
-rule protectedMethodsComplete(method f, env e, calldataarg data) filtered {
+// Check that all methods except those noted below comply with the `protected` modifier when an initiator has been set.
+rule protectedWithSetInitiator(method f, env e, calldataarg data) filtered {
+    // Do not check view functions.
+    // Do not check the fallback function.
+    // Do not check multicall, which is used to start a new bundle.
     f -> !f.isView && !f.isFallback && f.selector != sig:multicall(bytes[]).selector
 }
 {