From af07945a1346967d92eb16fce2ad95aceda39e52 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Wed, 19 Jun 2024 15:08:14 +0200 Subject: [PATCH 1/3] chore: update verification to use conf files --- .github/workflows/certora.yml | 24 ++++++++++--------- ...rnessFIFO.patch => applyHarnessFifo.patch} | 0 certora/confs/DllFifo.conf | 12 ++++++++++ certora/confs/DllSimple.conf | 12 ++++++++++ certora/makefile | 6 ++--- certora/scripts/dll-fifo.sh | 11 --------- certora/scripts/dll-simple.sh | 11 --------- certora/scripts/sanity-fifo.sh | 11 --------- certora/scripts/sanity-simple.sh | 11 --------- certora/specs/{dll-fifo.spec => DllFifo.spec} | 0 .../specs/{dll-simple.spec => DllSimple.spec} | 0 certora/specs/sanity.spec | 7 ------ 12 files changed, 40 insertions(+), 65 deletions(-) rename certora/{applyHarnessFIFO.patch => applyHarnessFifo.patch} (100%) create mode 100644 certora/confs/DllFifo.conf create mode 100644 certora/confs/DllSimple.conf delete mode 100755 certora/scripts/dll-fifo.sh delete mode 100755 certora/scripts/dll-simple.sh delete mode 100755 certora/scripts/sanity-fifo.sh delete mode 100755 certora/scripts/sanity-simple.sh rename certora/specs/{dll-fifo.spec => DllFifo.spec} (100%) rename certora/specs/{dll-simple.spec => DllSimple.spec} (100%) delete mode 100644 certora/specs/sanity.spec diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml index 9f27bc3e..89e9335e 100644 --- a/.github/workflows/certora.yml +++ b/.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,14 @@ 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 + certora + bash certora/scripts/${{ matrix.conf }}.conf env: CERTORAKEY: ${{ secrets.CERTORAKEY }} - - strategy: - fail-fast: false - max-parallel: 4 - - matrix: - script: - - dll-fifo.sh - - dll-simple.sh diff --git a/certora/applyHarnessFIFO.patch b/certora/applyHarnessFifo.patch similarity index 100% rename from certora/applyHarnessFIFO.patch rename to certora/applyHarnessFifo.patch diff --git a/certora/confs/DllFifo.conf b/certora/confs/DllFifo.conf new file mode 100644 index 00000000..9f343df3 --- /dev/null +++ b/certora/confs/DllFifo.conf @@ -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", +} diff --git a/certora/confs/DllSimple.conf b/certora/confs/DllSimple.conf new file mode 100644 index 00000000..14776914 --- /dev/null +++ b/certora/confs/DllSimple.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", +} diff --git a/certora/makefile b/certora/makefile index 61ca4a95..e22c5bdf 100644 --- a/certora/makefile +++ b/certora/makefile @@ -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 diff --git a/certora/scripts/dll-fifo.sh b/certora/scripts/dll-fifo.sh deleted file mode 100755 index a3da771e..00000000 --- a/certora/scripts/dll-fifo.sh +++ /dev/null @@ -1,11 +0,0 @@ -#!/bin/sh - -make -C certora munged-fifo - -certoraRun \ - certora/munged-fifo/MockDLL.sol \ - --verify MockDLL:certora/specs/dll-fifo.spec \ - --loop_iter 4 \ - --optimistic_loop \ - --msg "FIFO DLL verification" \ - "$@" diff --git a/certora/scripts/dll-simple.sh b/certora/scripts/dll-simple.sh deleted file mode 100755 index 4c039831..00000000 --- a/certora/scripts/dll-simple.sh +++ /dev/null @@ -1,11 +0,0 @@ -#!/bin/sh - -make -C certora munged-simple - -certoraRun \ - certora/munged-simple/MockDLL.sol \ - --verify MockDLL:certora/specs/dll-simple.spec \ - --loop_iter 7 \ - --optimistic_loop \ - --msg "Simple DLL verification" \ - "$@" diff --git a/certora/scripts/sanity-fifo.sh b/certora/scripts/sanity-fifo.sh deleted file mode 100755 index 22da88b8..00000000 --- a/certora/scripts/sanity-fifo.sh +++ /dev/null @@ -1,11 +0,0 @@ -#!/bin/sh - -make -C certora munged-fifo - -certoraRun \ - certora/munged-fifo/MockDLL.sol \ - --verify MockDLL:certora/specs/sanity.spec \ - --loop_iter 7 \ - --optimistic_loop \ - --msg "FIFO DLL sanity" \ - "$@" diff --git a/certora/scripts/sanity-simple.sh b/certora/scripts/sanity-simple.sh deleted file mode 100755 index c27d707b..00000000 --- a/certora/scripts/sanity-simple.sh +++ /dev/null @@ -1,11 +0,0 @@ -#!/bin/sh - -make -C certora munged-simple - -certoraRun \ - certora/munged-simple/MockDLL.sol \ - --verify MockDLL:certora/specs/sanity.spec \ - --loop_iter 7 \ - --optimistic_loop \ - --msg "Simple DLL sanity" \ - "$@" diff --git a/certora/specs/dll-fifo.spec b/certora/specs/DllFifo.spec similarity index 100% rename from certora/specs/dll-fifo.spec rename to certora/specs/DllFifo.spec diff --git a/certora/specs/dll-simple.spec b/certora/specs/DllSimple.spec similarity index 100% rename from certora/specs/dll-simple.spec rename to certora/specs/DllSimple.spec diff --git a/certora/specs/sanity.spec b/certora/specs/sanity.spec deleted file mode 100644 index be79b1d7..00000000 --- a/certora/specs/sanity.spec +++ /dev/null @@ -1,7 +0,0 @@ -rule sanity(method f) -{ - env e; - calldataarg args; - f(e,args); - assert false; -} From 2ea94675d0d1c89eb38dde8df8789532ea72896c Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Wed, 19 Jun 2024 15:12:12 +0200 Subject: [PATCH 2/3] fix: typo in verification line --- .github/workflows/certora.yml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml index 89e9335e..04a1e36b 100644 --- a/.github/workflows/certora.yml +++ b/.github/workflows/certora.yml @@ -41,7 +41,6 @@ jobs: echo "key length" ${#CERTORAKEY} make -C certora munged-simple make -C certora munged-fifo - certora - bash certora/scripts/${{ matrix.conf }}.conf + certora certora/confs/${{ matrix.conf }}.conf env: CERTORAKEY: ${{ secrets.CERTORAKEY }} From dedf7467e4460ef97386e75249d8ab38f5490c66 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Wed, 19 Jun 2024 15:15:49 +0200 Subject: [PATCH 3/3] fix: halmos deprecated argument --- .github/workflows/certora.yml | 2 +- .github/workflows/ci-foundry.yml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml index 04a1e36b..a4ceaa09 100644 --- a/.github/workflows/certora.yml +++ b/.github/workflows/certora.yml @@ -41,6 +41,6 @@ jobs: echo "key length" ${#CERTORAKEY} make -C certora munged-simple make -C certora munged-fifo - certora certora/confs/${{ matrix.conf }}.conf + certoraRun certora/confs/${{ matrix.conf }}.conf env: CERTORAKEY: ${{ secrets.CERTORAKEY }} diff --git a/.github/workflows/ci-foundry.yml b/.github/workflows/ci-foundry.yml index 788599da..59ef57c8 100644 --- a/.github/workflows/ci-foundry.yml +++ b/.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