From cf7a8b657495142c6b29be82d7c466b9e1c1fe9d Mon Sep 17 00:00:00 2001
From: r4bbit <445106+0x-r4bbit@users.noreply.github.com>
Date: Mon, 11 Dec 2023 15:10:41 +0100
Subject: [PATCH] chore(ci): add certora CI integration (#40)

---
 .github/PULL_REQUEST_TEMPLATE.md |  1 +
 .github/workflows/ci.yml         | 49 ++++++++++++++++++++++++++++++++
 .gitignore                       |  2 ++
 certora/certora.conf             | 12 ++++++++
 certora/specs/StakeManager.spec  |  4 +++
 package.json                     |  3 +-
 6 files changed, 70 insertions(+), 1 deletion(-)
 create mode 100644 certora/certora.conf
 create mode 100644 certora/specs/StakeManager.spec

diff --git a/.github/PULL_REQUEST_TEMPLATE.md b/.github/PULL_REQUEST_TEMPLATE.md
index 21d756d..8bf4f3d 100644
--- a/.github/PULL_REQUEST_TEMPLATE.md
+++ b/.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`?
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index e2d09a3..adde840 100644
--- a/.github/workflows/ci.yml
+++ b/.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
diff --git a/.gitignore b/.gitignore
index 8430dd9..e49ba38 100644
--- a/.gitignore
+++ b/.gitignore
@@ -22,3 +22,5 @@ artifacts
 typechain
 typechain-types
 gmx-contracts
+
+.certora_internal
diff --git a/certora/certora.conf b/certora/certora.conf
new file mode 100644
index 0000000..fcb2aeb
--- /dev/null
+++ b/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"
+  ]
+}
+
+
diff --git a/certora/specs/StakeManager.spec b/certora/specs/StakeManager.spec
new file mode 100644
index 0000000..c1f7813
--- /dev/null
+++ b/certora/specs/StakeManager.spec
@@ -0,0 +1,4 @@
+
+rule shouldPass {
+  assert true;
+}
diff --git a/package.json b/package.json
index ce539f3..30fe663 100644
--- a/package.json
+++ b/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"
   }