Merge pull request #139 from morpho-org/certora/update-verification

[Certora] Update verification

Author: MathisGD

.github/workflows/certora.yml

@@ -11,6 +11,14 @@ jobs:
   verify:
     runs-on: ubuntu-latest
 
+    strategy:
+      fail-fast: false
+
+      matrix:
+        conf:
+          - DllFifo
+          - DllSimple
+
     steps:
       - uses: actions/checkout@v3
 
@@ -26,20 +34,13 @@ jobs:
         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
+          sudo mv solc-static-linux /usr/local/bin/solc-0.8.17
 
       - name: Verify rule ${{ matrix.script }}
         run: |
           echo "key length" ${#CERTORAKEY}
-          bash certora/scripts/${{ matrix.script }} --solc solc8.17
+          make -C certora munged-simple
+          make -C certora munged-fifo
+          certoraRun certora/confs/${{ matrix.conf }}.conf
         env:
           CERTORAKEY: ${{ secrets.CERTORAKEY }}
-
-    strategy:
-      fail-fast: false
-      max-parallel: 4
-
-      matrix:
-        script:
-          - dll-fifo.sh
-          - dll-simple.sh

.github/workflows/ci-foundry.yml

@@ -47,4 +47,4 @@ jobs:
         run: python3 -m pip install --upgrade halmos
 
       - name: Run halmos
-        run: halmos --function testProve --loop 4 --symbolic-storage --error-unknown --test-parallel --solver-parallel --solver-timeout-assertion 0
+        run: halmos --function testProve --loop 4 --symbolic-storage --test-parallel --solver-parallel --solver-timeout-assertion 0

certora/applyHarnessFIFO.patch renamed to certora/applyHarnessFifo.patch

@@ -0,0 +1,12 @@
+{
+    "files": [
+        "certora/munged-fifo/MockDLL.sol",
+    ],
+    "solc": "solc-0.8.17",
+    "verify": "MockDLL:certora/specs/DllFifo.spec",
+    "loop_iter": "4",
+    "optimistic_loop": true,
+    "rule_sanity": "basic",
+    "server": "production",
+    "msg": "FIFO DLL",
+}

certora/confs/DllFifo.conf

@@ -0,0 +1,12 @@
+{
+    "files": [
+        "certora/munged-simple/MockDLL.sol",
+    ],
+    "solc": "solc-0.8.17",
+    "verify": "MockDLL:certora/specs/DllSimple.spec",
+    "loop_iter": "7",
+    "optimistic_loop": true,
+    "rule_sanity": "basic",
+    "server": "production",
+    "msg": "Simple DLL",
+}

certora/confs/DllSimple.conf

@@ -9,13 +9,13 @@ munged-simple: $(wildcard ../src/*.sol) applyHarnessSimple.patch
 record-simple:
 	diff -ruN ../src munged-simple | sed 's+\.\./src/++g' | sed 's+munged-simple/++g' > applyHarnessSimple.patch
 
-munged-fifo: $(wildcard ../src/*.sol) applyHarnessFIFO.patch
+munged-fifo: $(wildcard ../src/*.sol) applyHarnessFifo.patch
 	@rm -rf munged-fifo
 	@cp -r ../src munged-fifo
-	@patch -p0 -d munged-fifo < applyHarnessFIFO.patch
+	@patch -p0 -d munged-fifo < applyHarnessFifo.patch
 
 record-fifo:
-	diff -ruN ../src munged-fifo | sed 's+\.\./src/++g' | sed 's+munged-fifo/++g' > applyHarnessFIFO.patch
+	diff -ruN ../src munged-fifo | sed 's+\.\./src/++g' | sed 's+munged-fifo/++g' > applyHarnessFifo.patch
 
 clean:
 	rm -rf munged-simple munged-fifo