From 4be7d09fc1d0522b91c305c0bfa35043ddff43f0 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Wed, 3 Apr 2024 14:46:53 +0200 Subject: [PATCH 01/17] chore: fix exact math timeout --- .github/workflows/certora.yml | 2 +- certora/confs/ExactMath.conf | 4 +++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml index 47e091715..efd67bd0d 100644 --- a/.github/workflows/certora.yml +++ b/.github/workflows/certora.yml @@ -37,7 +37,7 @@ jobs: uses: actions/setup-python@v4 - name: Install certora - run: pip install certora-cli + run: pip install certora-cli-beta - name: Install solc run: | diff --git a/certora/confs/ExactMath.conf b/certora/confs/ExactMath.conf index c7fd84c69..344806e62 100644 --- a/certora/confs/ExactMath.conf +++ b/certora/confs/ExactMath.conf @@ -7,9 +7,11 @@ "rule_sanity": "basic", "prover_args": [ "-depth 3", - "-smt_hashingScheme plaininjectivity", "-mediumTimeout 30", "-timeout 3600", + "-smt_nonLinearArithmetic true", + "-adaptiveSolverConfig false", + "-solvers [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:lia2]", ], "server": "production", "msg": "Morpho Blue Exact Math" From cff19d99fd978a15b16baf580ea3947d4e4ab401 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Wed, 10 Apr 2024 10:58:06 +0200 Subject: [PATCH 02/17] feat: try new configuration for exact math --- certora/confs/ExactMath.conf | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/certora/confs/ExactMath.conf b/certora/confs/ExactMath.conf index 344806e62..ba5864d47 100644 --- a/certora/confs/ExactMath.conf +++ b/certora/confs/ExactMath.conf @@ -1,4 +1,5 @@ { + "fe_version": "latest", "files": [ "certora/harness/MorphoHarness.sol", ], @@ -6,12 +7,12 @@ "verify": "MorphoHarness:certora/specs/ExactMath.spec", "rule_sanity": "basic", "prover_args": [ - "-depth 3", - "-mediumTimeout 30", + "-depth 5", + "-mediumTimeout 5", "-timeout 3600", "-smt_nonLinearArithmetic true", "-adaptiveSolverConfig false", - "-solvers [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:lia2]", + "-solvers [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:lia2]" ], "server": "production", "msg": "Morpho Blue Exact Math" From 8baee1bf8e440798e991578dae25b6d8ee905183 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Wed, 10 Apr 2024 11:25:45 +0200 Subject: [PATCH 03/17] refactor: tweak exact math conf --- certora/confs/ExactMath.conf | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/certora/confs/ExactMath.conf b/certora/confs/ExactMath.conf index ba5864d47..648bfbf88 100644 --- a/certora/confs/ExactMath.conf +++ b/certora/confs/ExactMath.conf @@ -10,9 +10,8 @@ "-depth 5", "-mediumTimeout 5", "-timeout 3600", - "-smt_nonLinearArithmetic true", "-adaptiveSolverConfig false", - "-solvers [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:lia2]" + "-solvers [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:lia2]", ], "server": "production", "msg": "Morpho Blue Exact Math" From a7b1afd9145c9ca3a4975cdcb762519d744c7eae Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Wed, 10 Apr 2024 11:28:07 +0200 Subject: [PATCH 04/17] chore: get back 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 efd67bd0d..47e091715 100644 --- a/.github/workflows/certora.yml +++ b/.github/workflows/certora.yml @@ -37,7 +37,7 @@ jobs: uses: actions/setup-python@v4 - name: Install certora - run: pip install certora-cli-beta + run: pip install certora-cli - name: Install solc run: | From 7f862c2bbdbc22a1f994966cad96c63f1eb029d4 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Wed, 10 Apr 2024 11:42:38 +0200 Subject: [PATCH 05/17] refactor: specify non linear arithmetic --- certora/confs/ExactMath.conf | 1 + foundry.toml | 1 + 2 files changed, 2 insertions(+) diff --git a/certora/confs/ExactMath.conf b/certora/confs/ExactMath.conf index 648bfbf88..e0c01f166 100644 --- a/certora/confs/ExactMath.conf +++ b/certora/confs/ExactMath.conf @@ -10,6 +10,7 @@ "-depth 5", "-mediumTimeout 5", "-timeout 3600", + "-smt_nonLinearArithmetic true", "-adaptiveSolverConfig false", "-solvers [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:lia2]", ], diff --git a/foundry.toml b/foundry.toml index 4b0da7556..9b7733f1b 100644 --- a/foundry.toml +++ b/foundry.toml @@ -1,4 +1,5 @@ [profile.default] +libs = ["lib"] names = true sizes = true via-ir = true From b305f5171836478af4202ca2c7d5b9ea0118245d Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Wed, 10 Apr 2024 11:49:01 +0200 Subject: [PATCH 06/17] refactor: remove useless settings --- certora/confs/ExactMath.conf | 2 -- 1 file changed, 2 deletions(-) diff --git a/certora/confs/ExactMath.conf b/certora/confs/ExactMath.conf index e0c01f166..474f3af9c 100644 --- a/certora/confs/ExactMath.conf +++ b/certora/confs/ExactMath.conf @@ -1,5 +1,4 @@ { - "fe_version": "latest", "files": [ "certora/harness/MorphoHarness.sol", ], @@ -10,7 +9,6 @@ "-depth 5", "-mediumTimeout 5", "-timeout 3600", - "-smt_nonLinearArithmetic true", "-adaptiveSolverConfig false", "-solvers [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:lia2]", ], From 88dccc2fe38aa9b6f3dcf74745beda8872e9ecbf Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Wed, 10 Apr 2024 12:01:52 +0200 Subject: [PATCH 07/17] chore: certora-cli-beta --- .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 47e091715..efd67bd0d 100644 --- a/.github/workflows/certora.yml +++ b/.github/workflows/certora.yml @@ -37,7 +37,7 @@ jobs: uses: actions/setup-python@v4 - name: Install certora - run: pip install certora-cli + run: pip install certora-cli-beta - name: Install solc run: | From 8ed51ab202be11722f1de7b06c993bca2f6783b2 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Wed, 10 Apr 2024 12:12:22 +0200 Subject: [PATCH 08/17] chore: add back non linear arithmetic --- certora/confs/ExactMath.conf | 1 + 1 file changed, 1 insertion(+) diff --git a/certora/confs/ExactMath.conf b/certora/confs/ExactMath.conf index 474f3af9c..55edc50e7 100644 --- a/certora/confs/ExactMath.conf +++ b/certora/confs/ExactMath.conf @@ -10,6 +10,7 @@ "-mediumTimeout 5", "-timeout 3600", "-adaptiveSolverConfig false", + "-smt_nonLinearArithmetic true", "-solvers [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:lia2]", ], "server": "production", From bacb09f3872d73104fceb744db4c146d531302aa Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Wed, 10 Apr 2024 12:19:52 +0200 Subject: [PATCH 09/17] Revert "chore: add back non linear arithmetic" This reverts commit 8ed51ab202be11722f1de7b06c993bca2f6783b2. --- certora/confs/ExactMath.conf | 1 - 1 file changed, 1 deletion(-) diff --git a/certora/confs/ExactMath.conf b/certora/confs/ExactMath.conf index 55edc50e7..474f3af9c 100644 --- a/certora/confs/ExactMath.conf +++ b/certora/confs/ExactMath.conf @@ -10,7 +10,6 @@ "-mediumTimeout 5", "-timeout 3600", "-adaptiveSolverConfig false", - "-smt_nonLinearArithmetic true", "-solvers [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:lia2]", ], "server": "production", From fc0de85e54dcaa4fd89e0733ddb3da86fd365c4f Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Wed, 10 Apr 2024 13:16:44 +0200 Subject: [PATCH 10/17] chore: temporary version --- .github/workflows/certora.yml | 2 +- certora/confs/ExactMath.conf | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml index efd67bd0d..47e091715 100644 --- a/.github/workflows/certora.yml +++ b/.github/workflows/certora.yml @@ -37,7 +37,7 @@ jobs: uses: actions/setup-python@v4 - name: Install certora - run: pip install certora-cli-beta + run: pip install certora-cli - name: Install solc run: | diff --git a/certora/confs/ExactMath.conf b/certora/confs/ExactMath.conf index 474f3af9c..648bfbf88 100644 --- a/certora/confs/ExactMath.conf +++ b/certora/confs/ExactMath.conf @@ -1,4 +1,5 @@ { + "fe_version": "latest", "files": [ "certora/harness/MorphoHarness.sol", ], From 38437fe619bcb994db8f863f55878e39a0a7aeac Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Wed, 10 Apr 2024 14:29:31 +0200 Subject: [PATCH 11/17] chore: add back non linear arithmetic --- certora/confs/ExactMath.conf | 1 + 1 file changed, 1 insertion(+) diff --git a/certora/confs/ExactMath.conf b/certora/confs/ExactMath.conf index 648bfbf88..7059962f3 100644 --- a/certora/confs/ExactMath.conf +++ b/certora/confs/ExactMath.conf @@ -11,6 +11,7 @@ "-mediumTimeout 5", "-timeout 3600", "-adaptiveSolverConfig false", + "-smt_nonLinearArithmetic true", "-solvers [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:lia2]", ], "server": "production", From ce02888f5f0d4de8e301b2b6250db14bcf48f4b0 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Fri, 12 Apr 2024 15:30:28 +0200 Subject: [PATCH 12/17] chore: remove non linear arithmetic true --- certora/confs/ExactMath.conf | 1 - 1 file changed, 1 deletion(-) diff --git a/certora/confs/ExactMath.conf b/certora/confs/ExactMath.conf index 7059962f3..648bfbf88 100644 --- a/certora/confs/ExactMath.conf +++ b/certora/confs/ExactMath.conf @@ -11,7 +11,6 @@ "-mediumTimeout 5", "-timeout 3600", "-adaptiveSolverConfig false", - "-smt_nonLinearArithmetic true", "-solvers [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:lia2]", ], "server": "production", From 58e6a4b306cecf5fa117358efa8534dd83e659f3 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Mon, 15 Apr 2024 09:38:58 +0200 Subject: [PATCH 13/17] refactor: add nonlinear arith true --- certora/confs/ExactMath.conf | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/certora/confs/ExactMath.conf b/certora/confs/ExactMath.conf index 648bfbf88..55edc50e7 100644 --- a/certora/confs/ExactMath.conf +++ b/certora/confs/ExactMath.conf @@ -1,5 +1,4 @@ { - "fe_version": "latest", "files": [ "certora/harness/MorphoHarness.sol", ], @@ -11,6 +10,7 @@ "-mediumTimeout 5", "-timeout 3600", "-adaptiveSolverConfig false", + "-smt_nonLinearArithmetic true", "-solvers [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:lia2]", ], "server": "production", From b94a0c4a5e4eaf44547f4fb6cce36555f0d29f05 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Mon, 15 Apr 2024 11:06:40 +0200 Subject: [PATCH 14/17] chore: add back fe_version --- certora/confs/ExactMath.conf | 1 + 1 file changed, 1 insertion(+) diff --git a/certora/confs/ExactMath.conf b/certora/confs/ExactMath.conf index 55edc50e7..7059962f3 100644 --- a/certora/confs/ExactMath.conf +++ b/certora/confs/ExactMath.conf @@ -1,4 +1,5 @@ { + "fe_version": "latest", "files": [ "certora/harness/MorphoHarness.sol", ], From 184475e402942eee297097a5e9774dfe1f84b955 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Mon, 15 Apr 2024 12:30:18 +0200 Subject: [PATCH 15/17] chore: cache none --- certora/confs/ExactMath.conf | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/certora/confs/ExactMath.conf b/certora/confs/ExactMath.conf index 7059962f3..a6a162f49 100644 --- a/certora/confs/ExactMath.conf +++ b/certora/confs/ExactMath.conf @@ -1,5 +1,4 @@ { - "fe_version": "latest", "files": [ "certora/harness/MorphoHarness.sol", ], @@ -14,6 +13,7 @@ "-smt_nonLinearArithmetic true", "-solvers [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:lia2]", ], + "cache": "none", "server": "production", "msg": "Morpho Blue Exact Math" } From 6d76ef89a68dd38da45120556f5891b8f4205aab Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Mon, 15 Apr 2024 12:40:08 +0200 Subject: [PATCH 16/17] chore: remove cache --- certora/confs/ExactMath.conf | 1 - 1 file changed, 1 deletion(-) diff --git a/certora/confs/ExactMath.conf b/certora/confs/ExactMath.conf index a6a162f49..55edc50e7 100644 --- a/certora/confs/ExactMath.conf +++ b/certora/confs/ExactMath.conf @@ -13,7 +13,6 @@ "-smt_nonLinearArithmetic true", "-solvers [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:lia2]", ], - "cache": "none", "server": "production", "msg": "Morpho Blue Exact Math" } From db61a2b6ae0faddc096c7deb964c4e6050572c62 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Mon, 15 Apr 2024 14:51:30 +0200 Subject: [PATCH 17/17] Revert "chore: remove cache" This reverts commit 6d76ef89a68dd38da45120556f5891b8f4205aab. --- certora/confs/ExactMath.conf | 1 + 1 file changed, 1 insertion(+) diff --git a/certora/confs/ExactMath.conf b/certora/confs/ExactMath.conf index 55edc50e7..a6a162f49 100644 --- a/certora/confs/ExactMath.conf +++ b/certora/confs/ExactMath.conf @@ -13,6 +13,7 @@ "-smt_nonLinearArithmetic true", "-solvers [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:lia2]", ], + "cache": "none", "server": "production", "msg": "Morpho Blue Exact Math" }