authorizer: setup certora prover

.github/actions/certora/action.yml

@@ -0,0 +1,62 @@
+name: Certora Prover
+description: Run Certora Prover
+
+inputs:
+  workspace:
+    description: Yarn workspace to run prove script
+    required: true
+  certora-key:
+    description: Certora key
+    required: true
+  github-token:
+    description: Github token
+    required: true
+
+runs:
+  using: composite
+  steps:
+    - name: Set up environment
+      uses: ./.github/actions/setup
+    - name: Install python
+      uses: actions/setup-python@v4
+      with: { python-version: 3.9 }
+    - name: Install java
+      uses: actions/setup-java@v1
+      with: { java-version: '11', java-package: jre }
+    - name: Install certora cli
+      shell: bash
+      run: pip install certora-cli-beta
+    - name: Install solc
+      shell: bash
+      run: |
+        wget https://github.com/ethereum/solidity/releases/download/v0.8.17/solc-static-linux
+        chmod +x solc-static-linux
+        sudo mv solc-static-linux /usr/local/bin/solc8.17
+    - name: Build
+      shell: bash
+      run: yarn build
+    - name: Run certora prover
+      id: 'certora'
+      shell: bash
+      run: |
+        if CERTORA_OUTPUT=$(yarn --silent workspace ${{ inputs.workspace }} run --silent prove:ci); then
+          echo "$CERTORA_OUTPUT"
+          echo "CERTORA_JOB=$(echo "$CERTORA_OUTPUT" | tail -n 1)" >> $GITHUB_OUTPUT
+        else
+          echo "$CERTORA_OUTPUT"
+          exit 1
+        fi
+      env:
+        CERTORAKEY: ${{ inputs.certora-key }}
+    - name: Link certora build
+      if: ${{ steps.certora.outputs.CERTORA_JOB != '' }}
+      uses: actions/github-script@v5
+      with:
+        github-token: ${{ inputs.github-token }}
+        script: |
+          github.rest.issues.createComment({
+            issue_number: context.issue.number,
+            owner: context.repo.owner,
+            repo: context.repo.repo,
+            body: "${{ steps.certora.outputs.CERTORA_JOB }}"
+          })

.github/workflows/prover-authorizer.yml

@@ -0,0 +1,27 @@
+name: Prover
+
+env:
+  CI: true
+
+on:
+  push:
+    branches: "*"
+    paths:
+      - packages/authorizer/**
+  pull_request:
+    branches: "*"
+    paths:
+      - packages/authorizer/**
+
+jobs:
+  prove:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v3
+      - name: Prove
+        uses: ./.github/actions/certora
+        with:
+          workspace: '@mimic-fi/v3-authorizer'
+          certora-key: ${{ secrets.CERTORA_KEY }}
+          github-token: ${{ secrets.GITHUB_TOKEN }}

.gitignore

@@ -3,4 +3,6 @@ artifacts
 cache
 build
 dist
+.certora_internal
+.certora_recent_jobs.json
 *.log

packages/authorizer/certora/README.md

@@ -0,0 +1,9 @@
+# Authorizer verification  
+
+Using CVL2 see https://docs.certora.com/en/cvl_rewrite-main/docs/cvl/cvl2/changes.html
+
+### Run
+
+```sh
+certoraRun certora/conf/authorizer.conf
+```

packages/authorizer/certora/conf/authorizer.conf

@@ -0,0 +1,22 @@
+{
+  "files": [
+    "contracts/Authorizer.sol"
+  ],
+  "verify": "Authorizer:certora/specs/Authorizer.spec",
+  "loop_iter": "3",
+  "rule_sanity": "basic",
+  "send_only": true,
+  "optimistic_hashing": true,
+  "prover_args": [
+    "-copyLoopUnroll 8",
+    "-optimisticFallback true"
+  ],
+  "optimistic_loop": true,
+  "packages": [
+    "@mimic-fi=../../node_modules/@mimic-fi",
+    "@openzeppelin=../../node_modules/@openzeppelin"
+  ],
+  "solc_allow_path": ".",
+  "process": "emv",
+  "msg": "Authorizer"
+}

packages/authorizer/certora/specs/Authorizer.spec

@@ -0,0 +1,3 @@
+import "./General.spec";
+
+use rule sanity;

packages/authorizer/certora/specs/General.spec

@@ -0,0 +1,6 @@
+rule sanity(method f) good_description "Sanity" {
+    env e;
+    calldataarg args;
+    f(e, args);
+    assert false;
+}

packages/authorizer/package.json

@@ -12,13 +12,15 @@
     "dist"
   ],
   "scripts": {
+    "prepare": "yarn build",
     "build": "yarn compile && rm -rf dist && tsc",
     "compile": "hardhat compile",
     "lint": "yarn lint:solidity && yarn lint:typescript",
     "lint:solidity": "solhint 'contracts/**/*.sol' --config ../../node_modules/solhint-config-mimic/index.js",
     "lint:typescript": "eslint . --ext .ts",
     "test": "hardhat test",
-    "prepare": "yarn build"
+    "prove": "certoraRun certora/conf/authorizer.conf",
+    "prove:ci": "yarn prove --solc solc8.17"
   },
   "dependencies": {
     "@mimic-fi/v3-helpers": "0.1.0",