From d7f4f9556cf968303e3bccfdbc092b0b64a42912 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Tue, 17 Oct 2023 12:06:36 +0200 Subject: [PATCH 1/8] feat: use configuration file instead of script --- .github/workflows/certora.yml | 2 +- certora/configuration/ConsistentState.conf | 8 ++++++++ certora/scripts/verifyConsistentState.sh | 9 --------- 3 files changed, 9 insertions(+), 10 deletions(-) create mode 100644 certora/configuration/ConsistentState.conf delete mode 100755 certora/scripts/verifyConsistentState.sh diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml index b27fd301f..60720fcfe 100644 --- a/.github/workflows/certora.yml +++ b/.github/workflows/certora.yml @@ -43,7 +43,7 @@ jobs: matrix: script: - verifyAccrueInterest.sh - - verifyConsistentState.sh + - certoraRun certora/configuration/ConsistentState.conf - verifyExactMath.sh - verifyExitLiquidity.sh - verifyHealth.sh diff --git a/certora/configuration/ConsistentState.conf b/certora/configuration/ConsistentState.conf new file mode 100644 index 000000000..5b507bf4b --- /dev/null +++ b/certora/configuration/ConsistentState.conf @@ -0,0 +1,8 @@ +{ + "files": [ + "certora/harness/MorphoHarness.sol" + ], + "msg": "Morpho Blue Consistent State", + "process": "emv", + "verify": "MorphoHarness:certora/specs/ConsistentState.spec" +} diff --git a/certora/scripts/verifyConsistentState.sh b/certora/scripts/verifyConsistentState.sh deleted file mode 100755 index 47dd684f2..000000000 --- a/certora/scripts/verifyConsistentState.sh +++ /dev/null @@ -1,9 +0,0 @@ -#!/bin/bash - -set -euxo pipefail - -certoraRun \ - certora/harness/MorphoHarness.sol \ - --verify MorphoHarness:certora/specs/ConsistentState.spec \ - --msg "Morpho Blue Consistent State" \ - "$@" From ac88f34941ee31fc707fd5084b33cadf17ceed55 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Tue, 17 Oct 2023 12:15:19 +0200 Subject: [PATCH 2/8] fix: use conf matrix --- .github/workflows/certora.yml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml index 60720fcfe..fc567c38f 100644 --- a/.github/workflows/certora.yml +++ b/.github/workflows/certora.yml @@ -34,6 +34,7 @@ jobs: run: | echo "key length" ${#CERTORAKEY} bash certora/scripts/${{ matrix.script }} --solc solc8.19 + certoraRun certora/configuration/${{ matrix.conf }} --solc solc8.19 env: CERTORAKEY: ${{ secrets.CERTORAKEY }} @@ -41,9 +42,10 @@ jobs: fail-fast: false matrix: + conf: + - ConsistentState.conf script: - verifyAccrueInterest.sh - - certoraRun certora/configuration/ConsistentState.conf - verifyExactMath.sh - verifyExitLiquidity.sh - verifyHealth.sh From 2f8d60123a2593b75d083373d5bef8d9c67e9d0f Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Tue, 17 Oct 2023 12:16:46 +0200 Subject: [PATCH 3/8] fix: remove unused script row --- .github/workflows/certora.yml | 12 ------------ 1 file changed, 12 deletions(-) diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml index fc567c38f..9dba61ddc 100644 --- a/.github/workflows/certora.yml +++ b/.github/workflows/certora.yml @@ -33,7 +33,6 @@ jobs: - name: Verify rule ${{ matrix.script }} run: | echo "key length" ${#CERTORAKEY} - bash certora/scripts/${{ matrix.script }} --solc solc8.19 certoraRun certora/configuration/${{ matrix.conf }} --solc solc8.19 env: CERTORAKEY: ${{ secrets.CERTORAKEY }} @@ -44,14 +43,3 @@ jobs: matrix: conf: - ConsistentState.conf - script: - - verifyAccrueInterest.sh - - verifyExactMath.sh - - verifyExitLiquidity.sh - - verifyHealth.sh - - verifyLibSummary.sh - - verifyLiveness.sh - - verifyRatioMath.sh - - verifyReentrancy.sh - - verifyReverts.sh - - verifyTransfer.sh From defa1e756d26a52079ce7eb532a52fc4117cee64 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Tue, 17 Oct 2023 12:17:45 +0200 Subject: [PATCH 4/8] chore: switch to certora-cli --- .github/workflows/certora.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml index 9dba61ddc..e0211d5cc 100644 --- a/.github/workflows/certora.yml +++ b/.github/workflows/certora.yml @@ -22,7 +22,7 @@ jobs: python-version: "3.10" - name: Install certora - run: pip install certora-cli-beta + run: pip install certora-cli - name: Install solc run: | From 473e750e55ce3516f56a2b180df3caad84a98c01 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Tue, 17 Oct 2023 13:18:06 +0200 Subject: [PATCH 5/8] feat: add every script as a configuration file --- .github/workflows/certora.yml | 16 +++++++++++++--- certora/configuration/AccrueInterest.conf | 12 ++++++++++++ certora/configuration/ExactMath.conf | 12 ++++++++++++ certora/configuration/ExitLiquidity.conf | 8 ++++++++ certora/configuration/Health.conf | 12 ++++++++++++ certora/configuration/LibSummary.conf | 8 ++++++++ certora/configuration/Liveness.conf | 8 ++++++++ certora/configuration/RatioMath.conf | 11 +++++++++++ certora/configuration/Reentrancy.conf | 11 +++++++++++ certora/configuration/Reverts.conf | 8 ++++++++ certora/configuration/Transfer.conf | 11 +++++++++++ certora/scripts/verifyAccrueInterest.sh | 10 ---------- certora/scripts/verifyExactMath.sh | 10 ---------- certora/scripts/verifyExitLiquidity.sh | 9 --------- certora/scripts/verifyHealth.sh | 11 ----------- certora/scripts/verifyLibSummary.sh | 9 --------- certora/scripts/verifyLiveness.sh | 9 --------- certora/scripts/verifyRatioMath.sh | 10 ---------- certora/scripts/verifyReentrancy.sh | 10 ---------- certora/scripts/verifyReverts.sh | 9 --------- certora/scripts/verifyTransfer.sh | 12 ------------ 21 files changed, 114 insertions(+), 102 deletions(-) create mode 100644 certora/configuration/AccrueInterest.conf create mode 100644 certora/configuration/ExactMath.conf create mode 100644 certora/configuration/ExitLiquidity.conf create mode 100644 certora/configuration/Health.conf create mode 100644 certora/configuration/LibSummary.conf create mode 100644 certora/configuration/Liveness.conf create mode 100644 certora/configuration/RatioMath.conf create mode 100644 certora/configuration/Reentrancy.conf create mode 100644 certora/configuration/Reverts.conf create mode 100644 certora/configuration/Transfer.conf delete mode 100755 certora/scripts/verifyAccrueInterest.sh delete mode 100755 certora/scripts/verifyExactMath.sh delete mode 100755 certora/scripts/verifyExitLiquidity.sh delete mode 100755 certora/scripts/verifyHealth.sh delete mode 100755 certora/scripts/verifyLibSummary.sh delete mode 100755 certora/scripts/verifyLiveness.sh delete mode 100755 certora/scripts/verifyRatioMath.sh delete mode 100755 certora/scripts/verifyReentrancy.sh delete mode 100755 certora/scripts/verifyReverts.sh delete mode 100755 certora/scripts/verifyTransfer.sh diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml index e0211d5cc..ec1780b07 100644 --- a/.github/workflows/certora.yml +++ b/.github/workflows/certora.yml @@ -28,12 +28,12 @@ jobs: 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/solc8.19 + sudo mv solc-static-linux /usr/local/bin/solc - name: Verify rule ${{ matrix.script }} run: | echo "key length" ${#CERTORAKEY} - certoraRun certora/configuration/${{ matrix.conf }} --solc solc8.19 + certoraRun certora/configuration/${{ matrix.conf }} env: CERTORAKEY: ${{ secrets.CERTORAKEY }} @@ -42,4 +42,14 @@ jobs: matrix: conf: - - ConsistentState.conf + - AccrueInterest + - ConsistentState + - ExactMath + - ExitLiquidity + - Health + - LibSummary + - Liveness + - RatioMath + - Reentrancy + - Reverts + - Transfer diff --git a/certora/configuration/AccrueInterest.conf b/certora/configuration/AccrueInterest.conf new file mode 100644 index 000000000..33696fef8 --- /dev/null +++ b/certora/configuration/AccrueInterest.conf @@ -0,0 +1,12 @@ +{ + "files": [ + "certora/harness/MorphoHarness.sol" + ], + "msg": "Morpho Blue Accrue Interest", + "process": "emv", + "prover_args": [ + "-smt_hashingScheme plaininjectivity", + "-mediumTimeout 30" + ], + "verify": "MorphoHarness:certora/specs/AccrueInterest.spec" +} diff --git a/certora/configuration/ExactMath.conf b/certora/configuration/ExactMath.conf new file mode 100644 index 000000000..ee362c157 --- /dev/null +++ b/certora/configuration/ExactMath.conf @@ -0,0 +1,12 @@ +{ + "files": [ + "certora/harness/MorphoHarness.sol" + ], + "msg": "Morpho Blue Exact Math", + "process": "emv", + "prover_args": [ + "-smt_hashingScheme plaininjectivity", + "-mediumTimeout 30" + ], + "verify": "MorphoHarness:certora/specs/ExactMath.spec" +} diff --git a/certora/configuration/ExitLiquidity.conf b/certora/configuration/ExitLiquidity.conf new file mode 100644 index 000000000..de28e803b --- /dev/null +++ b/certora/configuration/ExitLiquidity.conf @@ -0,0 +1,8 @@ +{ + "files": [ + "certora/harness/MorphoHarness.sol" + ], + "msg": "Morpho Blue Exit Liquidity", + "process": "emv", + "verify": "MorphoHarness:certora/specs/ExitLiquidity.spec" +} diff --git a/certora/configuration/Health.conf b/certora/configuration/Health.conf new file mode 100644 index 000000000..bdea9ff2a --- /dev/null +++ b/certora/configuration/Health.conf @@ -0,0 +1,12 @@ +{ + "files": [ + "certora/harness/MorphoHarness.sol", + "src/mocks/OracleMock.sol" + ], + "msg": "Morpho Blue Health", + "process": "emv", + "prover_args": [ + "-smt_hashingScheme plaininjectivity" + ], + "verify": "MorphoHarness:certora/specs/Health.spec" +} diff --git a/certora/configuration/LibSummary.conf b/certora/configuration/LibSummary.conf new file mode 100644 index 000000000..ecff125e1 --- /dev/null +++ b/certora/configuration/LibSummary.conf @@ -0,0 +1,8 @@ +{ + "files": [ + "certora/harness/MorphoHarness.sol" + ], + "msg": "Morpho Blue Lib Summary", + "process": "emv", + "verify": "MorphoHarness:certora/specs/LibSummary.spec" +} diff --git a/certora/configuration/Liveness.conf b/certora/configuration/Liveness.conf new file mode 100644 index 000000000..8481d19dd --- /dev/null +++ b/certora/configuration/Liveness.conf @@ -0,0 +1,8 @@ +{ + "files": [ + "certora/harness/MorphoInternalAccess.sol" + ], + "msg": "Morpho Blue Liveness", + "process": "emv", + "verify": "MorphoInternalAccess:certora/specs/Liveness.spec" +} diff --git a/certora/configuration/RatioMath.conf b/certora/configuration/RatioMath.conf new file mode 100644 index 000000000..c770cba68 --- /dev/null +++ b/certora/configuration/RatioMath.conf @@ -0,0 +1,11 @@ +{ + "files": [ + "certora/harness/MorphoHarness.sol" + ], + "msg": "Morpho Blue Ratio Math", + "process": "emv", + "prover_args": [ + "-smt_hashingScheme plaininjectivity" + ], + "verify": "MorphoHarness:certora/specs/RatioMath.spec" +} diff --git a/certora/configuration/Reentrancy.conf b/certora/configuration/Reentrancy.conf new file mode 100644 index 000000000..c093b7dcb --- /dev/null +++ b/certora/configuration/Reentrancy.conf @@ -0,0 +1,11 @@ +{ + "files": [ + "certora/harness/MorphoHarness.sol" + ], + "msg": "Morpho Blue Reentrancy", + "process": "emv", + "prover_args": [ + "-enableStorageSplitting false" + ], + "verify": "MorphoHarness:certora/specs/Reentrancy.spec" +} diff --git a/certora/configuration/Reverts.conf b/certora/configuration/Reverts.conf new file mode 100644 index 000000000..34c3bc958 --- /dev/null +++ b/certora/configuration/Reverts.conf @@ -0,0 +1,8 @@ +{ + "files": [ + "certora/harness/MorphoHarness.sol" + ], + "msg": "Morpho Blue Reverts", + "process": "emv", + "verify": "MorphoHarness:certora/specs/Reverts.spec" +} diff --git a/certora/configuration/Transfer.conf b/certora/configuration/Transfer.conf new file mode 100644 index 000000000..c732629ef --- /dev/null +++ b/certora/configuration/Transfer.conf @@ -0,0 +1,11 @@ +{ + "files": [ + "certora/harness/TransferHarness.sol", + "certora/dispatch/ERC20Standard.sol", + "certora/dispatch/ERC20USDT.sol", + "certora/dispatch/ERC20NoRevert.sol" + ], + "msg": "Morpho Blue Transfer", + "process": "emv", + "verify": "TransferHarness:certora/specs/Transfer.spec" +} \ No newline at end of file diff --git a/certora/scripts/verifyAccrueInterest.sh b/certora/scripts/verifyAccrueInterest.sh deleted file mode 100755 index 555a40d85..000000000 --- a/certora/scripts/verifyAccrueInterest.sh +++ /dev/null @@ -1,10 +0,0 @@ -#!/bin/bash - -set -euxo pipefail - -certoraRun \ - certora/harness/MorphoHarness.sol \ - --verify MorphoHarness:certora/specs/AccrueInterest.spec \ - --prover_args '-smt_hashingScheme plaininjectivity -mediumTimeout 30' \ - --msg "Morpho Blue Accrue Interest" \ - "$@" diff --git a/certora/scripts/verifyExactMath.sh b/certora/scripts/verifyExactMath.sh deleted file mode 100755 index 0effcb7bd..000000000 --- a/certora/scripts/verifyExactMath.sh +++ /dev/null @@ -1,10 +0,0 @@ -#!/bin/bash - -set -euxo pipefail - -certoraRun \ - certora/harness/MorphoHarness.sol \ - --verify MorphoHarness:certora/specs/ExactMath.spec \ - --prover_args '-smt_hashingScheme plaininjectivity -mediumTimeout 30' \ - --msg "Morpho Blue Exact Math" \ - "$@" diff --git a/certora/scripts/verifyExitLiquidity.sh b/certora/scripts/verifyExitLiquidity.sh deleted file mode 100755 index afdd603e6..000000000 --- a/certora/scripts/verifyExitLiquidity.sh +++ /dev/null @@ -1,9 +0,0 @@ -#!/bin/bash - -set -euxo pipefail - -certoraRun \ - certora/harness/MorphoHarness.sol \ - --verify MorphoHarness:certora/specs/ExitLiquidity.spec \ - --msg "Morpho Blue Exit Liquidity" \ - "$@" diff --git a/certora/scripts/verifyHealth.sh b/certora/scripts/verifyHealth.sh deleted file mode 100755 index 0bd7a7c2b..000000000 --- a/certora/scripts/verifyHealth.sh +++ /dev/null @@ -1,11 +0,0 @@ -#!/bin/bash - -set -euxo pipefail - -certoraRun \ - certora/harness/MorphoHarness.sol \ - src/mocks/OracleMock.sol \ - --verify MorphoHarness:certora/specs/Health.spec \ - --prover_args '-smt_hashingScheme plaininjectivity' \ - --msg "Morpho Blue Health Check" \ - "$@" diff --git a/certora/scripts/verifyLibSummary.sh b/certora/scripts/verifyLibSummary.sh deleted file mode 100755 index 41dcf9ca0..000000000 --- a/certora/scripts/verifyLibSummary.sh +++ /dev/null @@ -1,9 +0,0 @@ -#!/bin/bash - -set -euxo pipefail - -certoraRun \ - certora/harness/MorphoHarness.sol \ - --verify MorphoHarness:certora/specs/LibSummary.spec \ - --msg "Morpho Blue Lib Summary" \ - "$@" diff --git a/certora/scripts/verifyLiveness.sh b/certora/scripts/verifyLiveness.sh deleted file mode 100755 index 260bc3757..000000000 --- a/certora/scripts/verifyLiveness.sh +++ /dev/null @@ -1,9 +0,0 @@ -#!/bin/bash - -set -euxo pipefail - -certoraRun \ - certora/harness/MorphoInternalAccess.sol \ - --verify MorphoInternalAccess:certora/specs/Liveness.spec \ - --msg "Morpho Blue Liveness" \ - "$@" diff --git a/certora/scripts/verifyRatioMath.sh b/certora/scripts/verifyRatioMath.sh deleted file mode 100755 index c17eb1fc9..000000000 --- a/certora/scripts/verifyRatioMath.sh +++ /dev/null @@ -1,10 +0,0 @@ -#!/bin/bash - -set -euxo pipefail - -certoraRun \ - certora/harness/MorphoHarness.sol \ - --verify MorphoHarness:certora/specs/RatioMath.spec \ - --prover_args '-smt_hashingScheme plaininjectivity' \ - --msg "Morpho Blue Ratio Math" \ - "$@" diff --git a/certora/scripts/verifyReentrancy.sh b/certora/scripts/verifyReentrancy.sh deleted file mode 100755 index 0ffa2d570..000000000 --- a/certora/scripts/verifyReentrancy.sh +++ /dev/null @@ -1,10 +0,0 @@ -#!/bin/bash - -set -euxo pipefail - -certoraRun \ - certora/harness/MorphoHarness.sol \ - --verify MorphoHarness:certora/specs/Reentrancy.spec \ - --prover_args '-enableStorageSplitting false' \ - --msg "Morpho Blue Reentrancy" \ - "$@" diff --git a/certora/scripts/verifyReverts.sh b/certora/scripts/verifyReverts.sh deleted file mode 100755 index ae2675499..000000000 --- a/certora/scripts/verifyReverts.sh +++ /dev/null @@ -1,9 +0,0 @@ -#!/bin/bash - -set -euxo pipefail - -certoraRun \ - certora/harness/MorphoHarness.sol \ - --verify MorphoHarness:certora/specs/Reverts.spec \ - --msg "Morpho Blue Reverts" \ - "$@" diff --git a/certora/scripts/verifyTransfer.sh b/certora/scripts/verifyTransfer.sh deleted file mode 100755 index 396585896..000000000 --- a/certora/scripts/verifyTransfer.sh +++ /dev/null @@ -1,12 +0,0 @@ -#!/bin/bash - -set -euxo pipefail - -certoraRun \ - certora/harness/TransferHarness.sol \ - certora/dispatch/ERC20Standard.sol \ - certora/dispatch/ERC20USDT.sol \ - certora/dispatch/ERC20NoRevert.sol \ - --verify TransferHarness:certora/specs/Transfer.spec \ - --msg "Morpho Blue Transfer" \ - "$@" From 88c173958b18c663a4e8afe765307b5b57a4e73d Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Tue, 17 Oct 2023 13:20:11 +0200 Subject: [PATCH 6/8] fix: add missing extension on configuration files --- .github/workflows/certora.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml index ec1780b07..34c0930ba 100644 --- a/.github/workflows/certora.yml +++ b/.github/workflows/certora.yml @@ -33,7 +33,7 @@ jobs: - name: Verify rule ${{ matrix.script }} run: | echo "key length" ${#CERTORAKEY} - certoraRun certora/configuration/${{ matrix.conf }} + certoraRun certora/configuration/${{ matrix.conf }}.conf env: CERTORAKEY: ${{ secrets.CERTORAKEY }} From 093bcd2c5229b715cde6c2baeea41e8186b66574 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Tue, 17 Oct 2023 13:31:31 +0200 Subject: [PATCH 7/8] refactor: order parameters in configuration files --- certora/configuration/AccrueInterest.conf | 5 ++--- certora/configuration/ConsistentState.conf | 5 ++--- certora/configuration/ExactMath.conf | 5 ++--- certora/configuration/ExitLiquidity.conf | 3 +-- certora/configuration/Health.conf | 5 ++--- certora/configuration/Liveness.conf | 5 ++--- certora/configuration/RatioMath.conf | 5 ++--- certora/configuration/Reentrancy.conf | 5 ++--- certora/configuration/Reverts.conf | 5 ++--- certora/configuration/Transfer.conf | 7 +++---- 10 files changed, 20 insertions(+), 30 deletions(-) diff --git a/certora/configuration/AccrueInterest.conf b/certora/configuration/AccrueInterest.conf index 33696fef8..fbc772df3 100644 --- a/certora/configuration/AccrueInterest.conf +++ b/certora/configuration/AccrueInterest.conf @@ -2,11 +2,10 @@ "files": [ "certora/harness/MorphoHarness.sol" ], - "msg": "Morpho Blue Accrue Interest", - "process": "emv", + "verify": "MorphoHarness:certora/specs/AccrueInterest.spec", "prover_args": [ "-smt_hashingScheme plaininjectivity", "-mediumTimeout 30" ], - "verify": "MorphoHarness:certora/specs/AccrueInterest.spec" + "msg": "Morpho Blue Accrue Interest" } diff --git a/certora/configuration/ConsistentState.conf b/certora/configuration/ConsistentState.conf index 5b507bf4b..b9e774bc7 100644 --- a/certora/configuration/ConsistentState.conf +++ b/certora/configuration/ConsistentState.conf @@ -2,7 +2,6 @@ "files": [ "certora/harness/MorphoHarness.sol" ], - "msg": "Morpho Blue Consistent State", - "process": "emv", - "verify": "MorphoHarness:certora/specs/ConsistentState.spec" + "verify": "MorphoHarness:certora/specs/ConsistentState.spec", + "msg": "Morpho Blue Consistent State" } diff --git a/certora/configuration/ExactMath.conf b/certora/configuration/ExactMath.conf index ee362c157..01c7f3f22 100644 --- a/certora/configuration/ExactMath.conf +++ b/certora/configuration/ExactMath.conf @@ -2,11 +2,10 @@ "files": [ "certora/harness/MorphoHarness.sol" ], - "msg": "Morpho Blue Exact Math", - "process": "emv", + "verify": "MorphoHarness:certora/specs/ExactMath.spec", "prover_args": [ "-smt_hashingScheme plaininjectivity", "-mediumTimeout 30" ], - "verify": "MorphoHarness:certora/specs/ExactMath.spec" + "msg": "Morpho Blue Exact Math" } diff --git a/certora/configuration/ExitLiquidity.conf b/certora/configuration/ExitLiquidity.conf index de28e803b..5e31571b1 100644 --- a/certora/configuration/ExitLiquidity.conf +++ b/certora/configuration/ExitLiquidity.conf @@ -2,7 +2,6 @@ "files": [ "certora/harness/MorphoHarness.sol" ], - "msg": "Morpho Blue Exit Liquidity", - "process": "emv", "verify": "MorphoHarness:certora/specs/ExitLiquidity.spec" + "msg": "Morpho Blue Exit Liquidity" } diff --git a/certora/configuration/Health.conf b/certora/configuration/Health.conf index bdea9ff2a..a84180e29 100644 --- a/certora/configuration/Health.conf +++ b/certora/configuration/Health.conf @@ -3,10 +3,9 @@ "certora/harness/MorphoHarness.sol", "src/mocks/OracleMock.sol" ], - "msg": "Morpho Blue Health", - "process": "emv", + "verify": "MorphoHarness:certora/specs/Health.spec", "prover_args": [ "-smt_hashingScheme plaininjectivity" ], - "verify": "MorphoHarness:certora/specs/Health.spec" + "msg": "Morpho Blue Health" } diff --git a/certora/configuration/Liveness.conf b/certora/configuration/Liveness.conf index 8481d19dd..44cddd6d3 100644 --- a/certora/configuration/Liveness.conf +++ b/certora/configuration/Liveness.conf @@ -2,7 +2,6 @@ "files": [ "certora/harness/MorphoInternalAccess.sol" ], - "msg": "Morpho Blue Liveness", - "process": "emv", - "verify": "MorphoInternalAccess:certora/specs/Liveness.spec" + "verify": "MorphoInternalAccess:certora/specs/Liveness.spec", + "msg": "Morpho Blue Liveness" } diff --git a/certora/configuration/RatioMath.conf b/certora/configuration/RatioMath.conf index c770cba68..ee100b758 100644 --- a/certora/configuration/RatioMath.conf +++ b/certora/configuration/RatioMath.conf @@ -2,10 +2,9 @@ "files": [ "certora/harness/MorphoHarness.sol" ], - "msg": "Morpho Blue Ratio Math", - "process": "emv", + "verify": "MorphoHarness:certora/specs/RatioMath.spec", "prover_args": [ "-smt_hashingScheme plaininjectivity" ], - "verify": "MorphoHarness:certora/specs/RatioMath.spec" + "msg": "Morpho Blue Ratio Math" } diff --git a/certora/configuration/Reentrancy.conf b/certora/configuration/Reentrancy.conf index c093b7dcb..f2e26e264 100644 --- a/certora/configuration/Reentrancy.conf +++ b/certora/configuration/Reentrancy.conf @@ -2,10 +2,9 @@ "files": [ "certora/harness/MorphoHarness.sol" ], - "msg": "Morpho Blue Reentrancy", - "process": "emv", + "verify": "MorphoHarness:certora/specs/Reentrancy.spec", "prover_args": [ "-enableStorageSplitting false" ], - "verify": "MorphoHarness:certora/specs/Reentrancy.spec" + "msg": "Morpho Blue Reentrancy" } diff --git a/certora/configuration/Reverts.conf b/certora/configuration/Reverts.conf index 34c3bc958..c414253b2 100644 --- a/certora/configuration/Reverts.conf +++ b/certora/configuration/Reverts.conf @@ -2,7 +2,6 @@ "files": [ "certora/harness/MorphoHarness.sol" ], - "msg": "Morpho Blue Reverts", - "process": "emv", - "verify": "MorphoHarness:certora/specs/Reverts.spec" + "verify": "MorphoHarness:certora/specs/Reverts.spec", + "msg": "Morpho Blue Reverts" } diff --git a/certora/configuration/Transfer.conf b/certora/configuration/Transfer.conf index c732629ef..ae018d869 100644 --- a/certora/configuration/Transfer.conf +++ b/certora/configuration/Transfer.conf @@ -5,7 +5,6 @@ "certora/dispatch/ERC20USDT.sol", "certora/dispatch/ERC20NoRevert.sol" ], - "msg": "Morpho Blue Transfer", - "process": "emv", - "verify": "TransferHarness:certora/specs/Transfer.spec" -} \ No newline at end of file + "verify": "TransferHarness:certora/specs/Transfer.spec", + "msg": "Morpho Blue Transfer" +} From 80995c80207b023e1c359f0154b3a721884fe8e6 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Tue, 17 Oct 2023 13:33:06 +0200 Subject: [PATCH 8/8] fix: missing comma --- certora/configuration/ExitLiquidity.conf | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/certora/configuration/ExitLiquidity.conf b/certora/configuration/ExitLiquidity.conf index 5e31571b1..b58c24657 100644 --- a/certora/configuration/ExitLiquidity.conf +++ b/certora/configuration/ExitLiquidity.conf @@ -2,6 +2,6 @@ "files": [ "certora/harness/MorphoHarness.sol" ], - "verify": "MorphoHarness:certora/specs/ExitLiquidity.spec" + "verify": "MorphoHarness:certora/specs/ExitLiquidity.spec", "msg": "Morpho Blue Exit Liquidity" }