Colin@verif/setup

.github/workflows/certora.yml

@@ -0,0 +1,52 @@
+name: Certora
+
+on:
+  push:
+    branches:
+      - main
+  pull_request:
+  workflow_dispatch:
+
+jobs:
+  verify:
+    runs-on: ubuntu-latest
+
+    strategy:
+      fail-fast: false
+
+      matrix:
+        conf:
+          - Dummy
+
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          submodules: recursive
+
+      - name: Install python
+        uses: actions/setup-python@v5
+        with:
+          python-version: ">=3.11"
+
+      - name: Install certora
+        run: pip install certora-cli
+
+      - 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/solc-0.8.19
+
+      - name: Install solc (0.8.27)
+        run: |
+          wget https://github.com/ethereum/solidity/releases/download/v0.8.27/solc-static-linux
+          chmod +x solc-static-linux
+          sudo mv solc-static-linux /usr/local/bin/solc-0.8.27
+
+      - name: Apply munging
+        run: make -C certora munged
+
+      - name: Verify ${{ matrix.conf }} specification
+        run: certoraRun certora/confs/${{ matrix.conf }}.conf
+        env:
+          CERTORAKEY: ${{ secrets.CERTORAKEY }}

.gitignore

@@ -14,3 +14,9 @@ docs/
 .env
 
 .prettierignore
+
+# Emacs
+*~
+
+# Certora
+.certora_internal

certora/Makefile

@@ -0,0 +1,12 @@
+munged: $(wildcard ../src/*.sol) applyMunging.patch
+	@rm -rf munged
+	@cp -r ../src munged
+	@patch -p0 -d munged < applyMunging.patch
+
+record:
+	diff -ruN ../src munged | sed 's+\.\./src/++g' | sed 's+munged/++g' > applyMunging.patch
+
+clean:
+	rm -rf munged
+
+.PHONY: help clean # do not add munged here, as it is useful to protect munged edits

certora/README.md

@@ -0,0 +1,49 @@
+# Pre-liquidation Contract Formal Verification
+
+This folder contains the
+[CVL](https://docs.certora.com/en/latest/docs/cvl/index.html)
+specification and verification setup for the
+[pre-liquidation](../src/PreLiquidation.sol) contract using the
+[Certora Prover](https://www.certora.com/).
+
+## Getting Started
+
+This project depends on two different versions of
+[Solidity](https://soliditylang.org/) which are required for running
+the verification. The compiler binaries should be available under the
+following path names:
+
+  - `solc-0.8.19` for the solidity compiler version `0.8.19`, which is
+    used for `Morpho`;
+  - `solc-0.8.27` for the solidity compiler version `0.8.27`, which is
+    used for `PreLiquidation`.
+
+The verification is performed on modified source files, which can be
+generated by running the following command.
+
+``` shell
+make -C certora munged
+```
+
+### Installing the Certora Prover
+
+The Certora CLI can be installed by running `python3 -m pip3 install
+certora-cli`. Detailed installation instructions can be found on
+Certora's official
+[documentation](https://docs.certora.com/en/latest/docs/user-guide/install.html).
+
+To verifying a specification, run the command `certoraRun Spec.conf`
+where `Spec.conf` is the configuration file of the matching CVL
+specification. Configuration files are available in
+[`certora/conf`](./confs). Please ensure that `CERTORA_KEY` is set up
+in your environment.
+
+## Overview
+
+The PreLiquidation contract enables Morpho Blue borrowers to set up a
+safer liquidation plan on a given position, thus preventing undesired
+liquidations.
+
+## TODO
+
+- [ ] Provide an overview of the specification.

certora/confs/Dummy.conf

@@ -0,0 +1,18 @@
+{
+    "files": [
+        "certora/helpers/Dummy.sol",
+    ],
+    "solc": "solc-0.8.27",
+    "verify": "Dummy:certora/specs/Dummy.spec",
+    "loop_iter": "2",
+    "optimistic_loop": true,
+    "prover_args": [
+        "-depth 3",
+        "-mediumTimeout 20",
+        "-timeout 120",
+        "-superOptimisticReturnsize true",
+    ],
+    "rule_sanity": "basic",
+    "server": "production",
+    "msg": "PreLiquidation Dummy",
+}

certora/helpers/Dummy.sol

@@ -0,0 +1 @@
+contract Dummy {}

certora/specs/Dummy.spec

@@ -0,0 +1,2 @@
+invariant tt()
+    true;