Merge pull request #33 from morpho-labs/test/certora-ci

[round 2] Add certora to the CI

Author: QGarchery

.github/workflows/certora.yml

@@ -0,0 +1,42 @@
+name: Certora
+
+on:
+  push:
+  workflow_dispatch:
+
+jobs:
+  verify:
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v3
+
+      - name: Install python
+        uses: actions/setup-python@v4
+        with:
+          python-version: "3.10"
+
+      - name: Install certora
+        run: pip install certora-cli
+
+      - name: Install solc
+        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: Verify rule ${{ matrix.script }}
+        run: |
+          echo "key length" ${#CERTORAKEY}
+          bash certora/scripts/${{ matrix.script }} --solc solc8.17
+        env:
+          CERTORAKEY: ${{ secrets.CERTORAKEY }}
+
+    strategy:
+      fail-fast: false
+      max-parallel: 4
+
+      matrix:
+        script:
+          - dll-fifo.sh
+          - dll-simple.sh

certora/scripts/dll-fifo.sh

@@ -7,6 +7,5 @@ certoraRun \
     --verify MockDLL:certora/specs/dll-fifo.spec \
     --loop_iter 4 \
     --optimistic_loop \
-    --send_only \
     --msg "FIFO DLL verification" \
     $@

certora/scripts/dll-simple.sh

@@ -7,6 +7,5 @@ certoraRun \
     --verify MockDLL:certora/specs/dll-simple.spec \
     --loop_iter 7 \
     --optimistic_loop \
-    --send_only \
     --msg "Simple DLL verification" \
     $@

certora/scripts/sanity-fifo.sh

@@ -7,6 +7,5 @@ certoraRun \
     --verify MockDLL:certora/specs/sanity.spec \
     --loop_iter 7 \
     --optimistic_loop \
-    --send_only \
     --msg "FIFO DLL sanity" \
     $@

certora/scripts/sanity-simple.sh

@@ -7,6 +7,5 @@ certoraRun \
     --verify MockDLL:certora/specs/sanity.spec \
     --loop_iter 7 \
     --optimistic_loop \
-    --send_only \
     --msg "Simple DLL sanity" \
     $@