Certora formal verification rules

.github/workflows/certora-prover.yml

@@ -0,0 +1,59 @@
+name: Certora Prover Submission Workflow
+description: |-
+  This workflow submits Certora Prover jobs on the specified configurations. Once all
+  jobs are successfully submitted, it will add a pending commit status to the commit.
+  This status will be periodically updated with verification results of the jobs, along
+  with the verification summary comment on the pull request.
+
+  For more information, please visit https://github.com/certora/certora-run-action.
+
+on:
+  pull_request:
+    branches:
+      - master
+  workflow_dispatch:
+
+jobs:
+  certora_run_submission:
+    runs-on: ubuntu-latest
+    permissions:
+      contents: read
+      statuses: write
+      pull-requests: write
+      id-token: write
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v4
+        with:
+          submodules: recursive
+
+      # Run Certora munge script
+      - name: Certora munge
+        run: ./certora/scripts/patch.sh
+
+      # Submit verification jobs to Certora Prover
+      - name: Submit verification jobs to Certora Prover
+        uses: Certora/certora-run-action@v2
+        with:
+          # Add your configurations as lines, each line is separated.
+          # Specify additional options for each configuration by adding them after the configuration.
+          configurations: |-
+            certora/confs/Balances.conf
+            certora/confs/ConsistentState.conf
+            certora/confs/Enabled.conf
+            certora/confs/Immutability.conf
+            certora/confs/Liveness.conf
+            certora/confs/PendingValues.conf
+            certora/confs/Range.conf
+            certora/confs/Reentrancy.conf
+            certora/confs/Reverts.conf
+            certora/confs/Roles.conf
+            certora/confs/Timelock.conf
+            certora/confs/LostAssets.conf
+          solc-versions: 0.8.17 0.8.26
+          cli-release: beta
+          job-name: "Verified Rules"
+          certora-key: ${{ secrets.CERTORAKEY }}
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+

.gitignore

@@ -12,4 +12,7 @@ broadcast/
 .env
 
 # System Files
-.DS_Store
+.DS_Store
+
+# certora generated files
+.certora_internal

certora/README.md

@@ -0,0 +1,59 @@
+This folder contains the verification of EulerEarn using the Certora Prover.
+
+The verification was inspired by the previous verification projects for Metamorpho and SiloVault (see https://github.com/morpho-org/metamorpho/tree/main/certora)
+
+## Getting started
+
+The code is compiled using 2 versions of solidity, which must be installed to run the verification as:
+
+- `solc-0.8.17` for solidity compiler version 0.8.17 which is used for compiling Permit2
+- `solc-0.8.19` for solidity compiler version 0.8.26 which is used for compiling the rest of the solidity files.
+
+Follow Certora installation instructions: https://docs.certora.com/en/latest/docs/user-guide/install.html and the repository build installation for EulerEarn.
+
+## Folders and file structure
+
+The [`certora/specs`](specs) folder contains the following files:
+
+- [`ConsistentState.spec`](specs/ConsistentState.spec) checks various properties specifying what is the consistent state of EulerEarn, what are the reachable setting configurations (such as caps and fee).
+- [`Balances.spec`](specs/Balances.spec) checks that tokens are not kept on the EulerEarn contract. Any deposit ends up in the underlying vaults and any withdrawal is forwarded to the user.
+- [`Enabled.spec`](specs/Enabled.spec) checks properties about enabled flag of market, notably that it correctly tracks the fact that the market is in the withdraw queue.
+- [`Immutability.spec`](specs/Immutability.spec) checks that EulerEarn is immutable.
+- [`Liveness.spec`](specs/Liveness.spec) checks some liveness properties of EulerEarn, notably that some emergency procedures are always available.
+- [`PendingValues.spec`](specs/PendingValues.spec) checks properties on the values that are still under timelock. Those properties are notably useful to prove that actual storage variables, when set to the pending value, use a consistent value.
+- [`Range.spec`](specs/Range.spec) checks the bounds (if any) of storage variables.
+- [`Reentrancy.spec`](specs/Reentrancy.spec) checks that EulerEarn is reentrancy safe by making sure that there are no untrusted external calls.
+- [`Reverts.spec`](specs/Reverts.spec) checks the revert conditions on entrypoints.
+- [`Roles.spec`](specs/Roles.spec) checks the access control and authorization granted by the respective EulerEarn roles. In particular it checks the hierarchy of roles.
+- [`Timelock.spec`](specs/Timelock.spec) verifies computations for periods during which we know the values are under timelock.
+
+The [`certora/specs/summaries`](specs/summaries) folder contains summaries for different functions that simplify the behavior of different functions, namely mathematical functions in [`Math.spec`], and dispatching summaries that allow the prover to recognize the appropriate function to resolve to when we have external calls to underlying vaults.
+
+The [`certora/confs`](confs) folder contains a configuration file for each corresponding specification file.
+
+The [`certora/harnesses`](harnesses) folder contains harness contracts that enable the verification of EulerEarn, by exposing internal functions and fields. 
+
+The [`certora/mocks`](mocks) folder contains mock contracts that simplify the verification of EulerEarn, by fixing reference implementations for the underlying token and vaults. 
+
+The [`certora/scripts`](mocks) folder contains a patch that applies a simple modification to the EulerEarn contract that introduces ghost variables that simplify verification, and the `PatchAndCertoraRun.sh` script that is used to run rules after the patch is applied.
+
+The [`certora/gambit`](gambit) folder contains mutation testing - modified versions of the EulerEarn contract that have been injected with bugs and configuration files to run different rules on EulerEarn and the mutations to show that these bugs can be found by the given rules.
+
+## Specification imports graph
+
+Most rules follow the same setup starting with `Range.spec`, with the exception of Roles, Reentrancy, Immutability, Balances, and MarketInteractions that require a different setup with non-standard summaries that have assertions or modifications to rule-specific flags.  
+
+```mermaid
+graph
+Liveness --> Reverts
+Reverts --> ConsistentState
+ConsistentState --> Timelock
+Timelock --> Enabled
+Enabled --> PendingValues
+PendingValues --> Range
+Roles
+Reentrancy
+Immutability
+Balances
+LostAssets --> Range
+```

certora/confs/Balances.conf

@@ -0,0 +1,60 @@
+{
+    "verify": "EulerEarnHarness:certora/specs/Balances.spec",
+    "msg": "Euler Earn - Rules about Balances",
+    "loop_iter": "2",
+    "optimistic_loop": true,
+    "global_timeout": "7200",
+    "parametric_contracts": "EulerEarnHarness",
+    "rule_sanity": "none",
+    "files": [
+        "certora/harnesses/EulerEarnHarness.sol",
+        "lib/ethereum-vault-connector/src/EthereumVaultConnector.sol",
+        "lib/euler-vault-kit/lib/permit2/src/Permit2.sol",
+        "src/EulerEarnFactory.sol",
+        "test/mocks/PerspectiveMock.sol",
+        "certora/mocks/VaultMock0.sol",
+        "certora/mocks/VaultMock1.sol",
+        "certora/mocks/Token0.sol",
+        "certora/harnesses/ERC20Helper.sol"
+    ],
+    "link": [
+        "EulerEarnHarness:evc=EthereumVaultConnector",
+        "EulerEarnHarness:permit2Address=Permit2",
+        "EulerEarnFactory:permit2Address=Permit2",
+        "EulerEarnFactory:perspective=PerspectiveMock",
+        "VaultMock0:_asset=Token0",
+        "VaultMock1:_asset=Token0",
+        "EulerEarnHarness:_asset=Token0"
+    ],
+    "packages": [
+        "ethereum-vault-connector=lib/ethereum-vault-connector/src",
+        "euler-vault-kit=lib/euler-vault-kit/src",
+        "forge-std=lib/forge-std/src",
+        "solmate=lib/euler-vault-kit/lib/permit2/lib/solmate"
+    ],
+    "compiler_map": {
+        "EulerEarnHarness": "solc-0.8.26",
+        "EthereumVaultConnector": "solc-0.8.26",
+        "Permit2": "solc-0.8.17",
+        "EulerEarnFactory": "solc-0.8.26",
+        "PerspectiveMock": "solc-0.8.26",
+        "IRMLinearKink": "solc-0.8.26",
+        "VaultMock0": "solc-0.8.26",
+        "VaultMock1": "solc-0.8.26",
+        "Token0": "solc-0.8.26",
+        "ERC20Helper": "solc-0.8.26"
+    },
+    "solc_optimize": "200",
+    "solc_via_ir": true,
+    "assert_autofinder_success": true,
+    "contract_recursion_limit": "1",
+    "process": "emv",
+    "prover_args": [
+        "-verifyCache ",
+        "-verifyTACDumps",
+        "-testMode",
+        "-checkRuleDigest",
+        "-callTraceHardFail on",
+        "-cvlFunctionRevert true"
+    ]
+}

certora/confs/ConsistentState.conf

@@ -0,0 +1,60 @@
+{
+    "verify": "EulerEarnHarness:certora/specs/ConsistentState.spec",
+    "msg": "Euler Earn - Rules about Consistency of State",
+    "loop_iter": "2",
+    "optimistic_loop": true,
+    "global_timeout": "7200",
+    "parametric_contracts": "EulerEarnHarness",
+    "rule_sanity": "none",
+    "files": [
+        "certora/harnesses/EulerEarnHarness.sol",
+        "lib/ethereum-vault-connector/src/EthereumVaultConnector.sol",
+        "lib/euler-vault-kit/lib/permit2/src/Permit2.sol",
+        "src/EulerEarnFactory.sol",
+        "test/mocks/PerspectiveMock.sol",
+        "certora/mocks/VaultMock0.sol",
+        "certora/mocks/VaultMock1.sol",
+        "certora/mocks/Token0.sol",
+        "certora/harnesses/ERC20Helper.sol"
+    ],
+    "link": [
+        "EulerEarnHarness:evc=EthereumVaultConnector",
+        "EulerEarnHarness:permit2Address=Permit2",
+        "EulerEarnFactory:permit2Address=Permit2",
+        "EulerEarnFactory:perspective=PerspectiveMock",
+        "VaultMock0:_asset=Token0",
+        "VaultMock1:_asset=Token0",
+        "EulerEarnHarness:_asset=Token0"
+    ],
+    "packages": [
+        "ethereum-vault-connector=lib/ethereum-vault-connector/src",
+        "euler-vault-kit=lib/euler-vault-kit/src",
+        "forge-std=lib/forge-std/src",
+        "solmate=lib/euler-vault-kit/lib/permit2/lib/solmate"
+    ],
+    "compiler_map": {
+        "EulerEarnHarness": "solc-0.8.26",
+        "EthereumVaultConnector": "solc-0.8.26",
+        "Permit2": "solc-0.8.17",
+        "EulerEarnFactory": "solc-0.8.26",
+        "PerspectiveMock": "solc-0.8.26",
+        "IRMLinearKink": "solc-0.8.26",
+        "VaultMock0": "solc-0.8.26",
+        "VaultMock1": "solc-0.8.26",
+        "Token0": "solc-0.8.26",
+        "ERC20Helper": "solc-0.8.26"
+    },
+    "solc_optimize": "200",
+    "solc_via_ir": true,
+    "assert_autofinder_success": true,
+    "contract_recursion_limit": "1",
+    "process": "emv",
+    "prover_args": [
+        "-verifyCache ",
+        "-verifyTACDumps",
+        "-testMode",
+        "-checkRuleDigest",
+        "-callTraceHardFail on",
+        "-cvlFunctionRevert true"
+    ]
+}

certora/confs/Conversions.conf

@@ -0,0 +1,72 @@
+{
+    "build_cache" : true,
+    //"prover_version" : "master",
+    "verify": "EulerEarnHarness:certora/specs/ConversionRules.spec",
+    "msg": "conversion rules",
+    "rule": [
+        "conversionOfZero",
+        "convertToAssetsWeakAdditivity",
+        "convertToSharesWeakAdditivity",
+        "conversionWeakMonotonicity",
+        "conversionWeakIntegrity",
+    ],
+    "rule_sanity": "none",
+    "loop_iter": "1",
+    "optimistic_loop": true,
+    "global_timeout": "7200",
+    "smt_timeout": "6000",
+    "parametric_contracts": "EulerEarnHarness",
+    "files": [
+        "certora/harnesses/EulerEarnHarness.sol",
+        "lib/ethereum-vault-connector/src/EthereumVaultConnector.sol",
+        "lib/euler-vault-kit/lib/permit2/src/Permit2.sol",
+        "src/EulerEarnFactory.sol",
+        "test/mocks/PerspectiveMock.sol",
+        "certora/mocks/VaultMock0.sol",
+        "certora/mocks/VaultMock1.sol",
+        "certora/mocks/Token0.sol",
+        "certora/harnesses/ERC20Helper.sol"
+    ],
+    "link": [
+        "EulerEarnHarness:evc=EthereumVaultConnector",
+        "EulerEarnHarness:permit2Address=Permit2",
+        "EulerEarnFactory:permit2Address=Permit2",
+        "EulerEarnFactory:perspective=PerspectiveMock",
+        "VaultMock0:_asset=Token0",
+        "VaultMock1:_asset=Token0",
+        "EulerEarnHarness:_asset=Token0"
+    ],
+    "packages": [
+        "ethereum-vault-connector=lib/ethereum-vault-connector/src",
+        "euler-vault-kit=lib/euler-vault-kit/src",
+        "forge-std=lib/forge-std/src",
+        "solmate=lib/euler-vault-kit/lib/permit2/lib/solmate"
+    ],
+    "compiler_map": {
+        "EulerEarnHarness": "solc-0.8.26",
+        "EthereumVaultConnector": "solc-0.8.26",
+        "Permit2": "solc-0.8.17",
+        "EulerEarnFactory": "solc-0.8.26",
+        "PerspectiveMock": "solc-0.8.26",
+        "IRMLinearKink": "solc-0.8.26",
+        "VaultMock0": "solc-0.8.26",
+        "VaultMock1": "solc-0.8.26",
+        "Token0": "solc-0.8.26"
+        "ERC20Helper": "solc-0.8.26",
+    },
+    "solc_optimize": "200",
+    "solc_via_ir": true,
+    "assert_autofinder_success": true,
+    "contract_recursion_limit": "1",
+    "optimistic_summary_recursion" : true,
+    "process": "emv",
+    "prover_args": [
+        "-depth 20",
+        //"-verifyCache ",
+        //"-verifyTACDumps",
+        //"-testMode",
+        //"-checkRuleDigest",
+        //"-callTraceHardFail on",
+        "-cvlFunctionRevert true"
+    ]
+}