Certora Setup

.github/workflows/certora.yml

@@ -0,0 +1,52 @@
+name: certora
+
+on:
+  push:
+    branches:
+      - main
+  pull_request:
+    branches:
+      - main
+
+  workflow_dispatch:
+
+jobs:
+  verify:
+    runs-on: ubuntu-latest
+    strategy:
+      matrix:
+        rule: ['verifySplitter.sh']
+
+    steps:
+      - uses: actions/checkout@v3
+
+      - name: Install python
+        uses: actions/setup-python@v4
+        with: { python-version: 3.11 }
+
+      - name: Install java
+        uses: actions/setup-java@v3
+        with: { java-version: '17', java-package: jre, distribution: semeru }
+
+      - name: Install certora cli
+        run: pip install -Iv certora-cli==6.3.1
+
+      - name: Install solc
+        run: |
+          wget https://github.com/ethereum/solidity/releases/download/v0.8.23/solc-static-linux
+          chmod +x solc-static-linux
+          sudo mv solc-static-linux /usr/local/bin/solc8.23
+
+      - name: Install dependencies
+        run: yarn install --frozen-lockfile
+
+      - name: Verify rule ${{ matrix.rule }}
+        run: |
+          cd certora
+          make munged
+          cd ..
+          echo "key length" ${#CERTORAKEY}
+          chmod +x ./certora/scripts/${{ matrix.rule }}
+          ./certora/scripts/${{ matrix.rule }}
+        env:
+          CERTORAKEY: ${{ secrets.CERTORA_KEY }}

.gitignore

@@ -7,3 +7,4 @@ script
 out
 .vscode
 lcov.info
+.certora_internal

.solhint.json

@@ -4,6 +4,7 @@
 	"rules": {
 		"prettier/prettier": "error",
 		"max-line-length": ["warn", 140],
-		"compiler-version": ["error", "^0.8.23"]
+		"compiler-version": "off",
+		"no-empty-blocks": "off"
 	}
 }

certora/.gitignore

@@ -0,0 +1 @@
+munged

certora/Makefile

@@ -0,0 +1,16 @@
+default: help
+
+CONTRACTS_DIR = ../src
+MUNGED_DIR    = munged
+
+help:
+	@echo "usage:"
+	@echo "  make clean:  remove all generated files (those ignored by git)"
+	@echo "  make munged: create $(MUNGED_DIR) directory"
+
+munged:  $(wildcard $(CONTRACTS_DIR)/*.sol)
+	rm -rf $@
+	cp -r $(CONTRACTS_DIR) $@
+
+clean:
+	git clean -fdX

certora/conf/splitter.conf

@@ -0,0 +1,17 @@
+{
+    "files": [
+        "certora/harnesses/SplitterHarness.sol"
+    ],
+    "hashing_length_bound": "352",
+    "loop_iter": "3",
+    "msg": "Splitter General Ruleset",
+    "optimistic_hashing": true,
+    "optimistic_loop": true,
+    "process": "emv",
+    "prover_args": [
+        " -optimisticFallback true -s z3 -copyLoopUnroll 5 -mediumTimeout 5 -depth 30"
+    ],
+    "rule_sanity": "basic",
+    "solc": "solc8.23",
+    "verify": "SplitterHarness:certora/specs/Splitter.spec"
+}

certora/harnesses/SplitterHarness.sol

@@ -0,0 +1,4 @@
+// SPDX-License-Identifier: LGPL-3.0-only
+import {Splitter} from "../munged/Splitter.sol";
+
+contract SplitterHarness is Splitter {}

certora/scripts/verifySplitter.sh

@@ -0,0 +1,12 @@
+#!/bin/bash
+
+params=("--send_only")
+
+if [[ -n "$CI" ]]; then
+    params=()
+fi
+
+certoraRun certora/conf/splitter.conf \
+    "${params[@]}" \
+    --msg "Splitter $*" \
+    "$@"

certora/specs/Splitter.spec

@@ -0,0 +1,3 @@
+rule demo() {
+    assert true;
+}