feat: add certora CI integration (#10)

This adds a new command to package.json `verify` which can be run via
`pnpm verify`.

The command runs the certora CLI with a config file which has to be
adjusted for every individual project.

The commit also adds a dedicated task to our github actions, which
ensures, verification is done in every PR as well.

.github/PULL_REQUEST_TEMPLATE.md

@@ -10,3 +10,4 @@ Ensure you completed **all of the steps** below before submitting your pull requ
 - [ ] Ran `forge snapshot`?
 - [ ] Ran `pnpm lint`?
 - [ ] Ran `forge test`?
+- [ ] Ran `pnpm verify`?

.github/workflows/ci.yml

@@ -117,3 +117,51 @@ jobs:
         run: |
           echo "## Coverage result" >> $GITHUB_STEP_SUMMARY
           echo "✅ Uploaded to Codecov" >> $GITHUB_STEP_SUMMARY
+  verify:
+    needs: ["lint", "build"]
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v3
+        with:
+          submodules: recursive
+
+      - name: Install Python
+        uses: actions/setup-python@v2
+        with: { python-version: 3.9 }
+
+      - name: Install Java
+        uses: actions/setup-java@v1
+        with: { java-version: "11", java-package: jre }
+
+      - name: Install Certora CLI
+        run: pip3 install certora-cli==5.0.5
+
+      - name: Install Solidity
+        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
+
+      - name: "Install Pnpm"
+        uses: "pnpm/action-setup@v2"
+        with:
+          version: "8"
+
+      - name: "Install Node.js"
+        uses: "actions/setup-node@v3"
+        with:
+          cache: "pnpm"
+          node-version: "lts/*"
+
+      - name: "Install the Node.js dependencies"
+        run: "pnpm install"
+
+      - name: Verify rules
+        run: "pnpm verify"
+        env:
+          CERTORAKEY: ${{ secrets.CERTORAKEY }}
+
+    strategy:
+      fail-fast: false
+      max-parallel: 16

.gitignore

@@ -15,3 +15,5 @@ yarn.lock
 !broadcast
 broadcast/*
 broadcast/*/31337/
+
+.certora_internal

certora/certora.conf

@@ -0,0 +1,8 @@
+{
+  "files": ["src/Foo.sol"],
+  "msg": "Verifying Foo.sol",
+  "rule_sanity": "basic",
+  "verify": "Foo:certora/specs/Foo.spec",
+  "wait_for_results": "all",
+}
+

certora/specs/Foo.spec

@@ -0,0 +1,9 @@
+methods {
+  function id(uint256) external returns (uint256) envfree;
+}
+
+rule checkIdOutputIsAlwaysEqualToInput {
+  uint256 input;
+
+  assert id(input) == input;
+}

package.json

@@ -23,7 +23,8 @@
   "scripts": {
     "clean": "rm -rf cache out",
     "lint": "pnpm lint:sol && pnpm prettier:check",
-    "lint:sol": "forge fmt --check && pnpm solhint {script,src,test}/**/*.sol",
+    "verify": "certoraRun certora/certora.conf",
+    "lint:sol": "forge fmt --check && pnpm solhint {script,src,test,certora}/**/*.sol",
     "prettier:check": "prettier --check **/*.{json,md,yml} --ignore-path=.prettierignore",
     "prettier:write": "prettier --write **/*.{json,md,yml} --ignore-path=.prettierignore"
   }