chore(ci): add certora CI integration (#40)

Author: 0x-r4bbit

.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

@@ -10,6 +10,7 @@ on:
   push:
     branches:
       - "main"
+      - "develop"
 
 jobs:
   lint:
@@ -117,3 +118,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

@@ -22,3 +22,5 @@ artifacts
 typechain
 typechain-types
 gmx-contracts
+
+.certora_internal

certora/certora.conf

@@ -0,0 +1,12 @@
+{
+  "files": ["contracts/StakeManager.sol"],
+  "msg": "Verifying StakeManager.sol",
+  "rule_sanity": "basic",
+  "verify": "StakeManager:certora/specs/StakeManager.spec",
+  "wait_for_results": "all",
+  "packages": [
+    "@openzeppelin=lib/openzeppelin-contracts"
+  ]
+}
+
+

certora/specs/StakeManager.spec

@@ -0,0 +1,4 @@
+
+rule shouldPass {
+  assert true;
+}

package.json

@@ -20,7 +20,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"
   }