From 7d2dcb8fba1d72550454feee6940284480ce8742 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Tue, 5 Sep 2023 11:36:55 +0200 Subject: [PATCH 1/4] feat: enable via-IR --- certora/configuration/AccrueInterest.conf | 2 ++ certora/configuration/ConsistentState.conf | 2 ++ certora/configuration/ExactMath.conf | 2 ++ certora/configuration/ExitLiquidity.conf | 2 ++ certora/configuration/Health.conf | 2 ++ certora/configuration/LibSummary.conf | 2 ++ certora/configuration/Liveness.conf | 2 ++ certora/configuration/RatioMath.conf | 2 ++ certora/configuration/Reentrancy.conf | 2 ++ certora/configuration/Reverts.conf | 2 ++ certora/configuration/Transfer.conf | 2 ++ 11 files changed, 22 insertions(+) diff --git a/certora/configuration/AccrueInterest.conf b/certora/configuration/AccrueInterest.conf index fbc772df3..c7a96c942 100644 --- a/certora/configuration/AccrueInterest.conf +++ b/certora/configuration/AccrueInterest.conf @@ -3,6 +3,8 @@ "certora/harness/MorphoHarness.sol" ], "verify": "MorphoHarness:certora/specs/AccrueInterest.spec", + "solc_via_ir": true, + "solc_optimize": "4294967295", "prover_args": [ "-smt_hashingScheme plaininjectivity", "-mediumTimeout 30" diff --git a/certora/configuration/ConsistentState.conf b/certora/configuration/ConsistentState.conf index b9e774bc7..22ed316a7 100644 --- a/certora/configuration/ConsistentState.conf +++ b/certora/configuration/ConsistentState.conf @@ -3,5 +3,7 @@ "certora/harness/MorphoHarness.sol" ], "verify": "MorphoHarness:certora/specs/ConsistentState.spec", + "solc_via_ir": true, + "solc_optimize": "4294967295", "msg": "Morpho Blue Consistent State" } diff --git a/certora/configuration/ExactMath.conf b/certora/configuration/ExactMath.conf index 01c7f3f22..1b518595c 100644 --- a/certora/configuration/ExactMath.conf +++ b/certora/configuration/ExactMath.conf @@ -3,6 +3,8 @@ "certora/harness/MorphoHarness.sol" ], "verify": "MorphoHarness:certora/specs/ExactMath.spec", + "solc_via_ir": true, + "solc_optimize": "4294967295", "prover_args": [ "-smt_hashingScheme plaininjectivity", "-mediumTimeout 30" diff --git a/certora/configuration/ExitLiquidity.conf b/certora/configuration/ExitLiquidity.conf index b58c24657..8c572f1e0 100644 --- a/certora/configuration/ExitLiquidity.conf +++ b/certora/configuration/ExitLiquidity.conf @@ -3,5 +3,7 @@ "certora/harness/MorphoHarness.sol" ], "verify": "MorphoHarness:certora/specs/ExitLiquidity.spec", + "solc_via_ir": true, + "solc_optimize": "4294967295", "msg": "Morpho Blue Exit Liquidity" } diff --git a/certora/configuration/Health.conf b/certora/configuration/Health.conf index a84180e29..843c2de36 100644 --- a/certora/configuration/Health.conf +++ b/certora/configuration/Health.conf @@ -4,6 +4,8 @@ "src/mocks/OracleMock.sol" ], "verify": "MorphoHarness:certora/specs/Health.spec", + "solc_via_ir": true, + "solc_optimize": "4294967295", "prover_args": [ "-smt_hashingScheme plaininjectivity" ], diff --git a/certora/configuration/LibSummary.conf b/certora/configuration/LibSummary.conf index cc89d89ca..e5390adbd 100644 --- a/certora/configuration/LibSummary.conf +++ b/certora/configuration/LibSummary.conf @@ -3,5 +3,7 @@ "certora/harness/MorphoHarness.sol" ], "verify": "MorphoHarness:certora/specs/LibSummary.spec", + "solc_via_ir": true, + "solc_optimize": "4294967295", "msg": "Morpho Blue Lib Summary" } diff --git a/certora/configuration/Liveness.conf b/certora/configuration/Liveness.conf index 44cddd6d3..3d8ffd2b8 100644 --- a/certora/configuration/Liveness.conf +++ b/certora/configuration/Liveness.conf @@ -3,5 +3,7 @@ "certora/harness/MorphoInternalAccess.sol" ], "verify": "MorphoInternalAccess:certora/specs/Liveness.spec", + "solc_via_ir": true, + "solc_optimize": "4294967295", "msg": "Morpho Blue Liveness" } diff --git a/certora/configuration/RatioMath.conf b/certora/configuration/RatioMath.conf index ee100b758..88f4ffa1c 100644 --- a/certora/configuration/RatioMath.conf +++ b/certora/configuration/RatioMath.conf @@ -3,6 +3,8 @@ "certora/harness/MorphoHarness.sol" ], "verify": "MorphoHarness:certora/specs/RatioMath.spec", + "solc_via_ir": true, + "solc_optimize": "4294967295", "prover_args": [ "-smt_hashingScheme plaininjectivity" ], diff --git a/certora/configuration/Reentrancy.conf b/certora/configuration/Reentrancy.conf index f2e26e264..2319b8aa4 100644 --- a/certora/configuration/Reentrancy.conf +++ b/certora/configuration/Reentrancy.conf @@ -3,6 +3,8 @@ "certora/harness/MorphoHarness.sol" ], "verify": "MorphoHarness:certora/specs/Reentrancy.spec", + "solc_via_ir": true, + "solc_optimize": "4294967295", "prover_args": [ "-enableStorageSplitting false" ], diff --git a/certora/configuration/Reverts.conf b/certora/configuration/Reverts.conf index c414253b2..5d270d051 100644 --- a/certora/configuration/Reverts.conf +++ b/certora/configuration/Reverts.conf @@ -3,5 +3,7 @@ "certora/harness/MorphoHarness.sol" ], "verify": "MorphoHarness:certora/specs/Reverts.spec", + "solc_via_ir": true, + "solc_optimize": "4294967295", "msg": "Morpho Blue Reverts" } diff --git a/certora/configuration/Transfer.conf b/certora/configuration/Transfer.conf index ae018d869..c33b1dfc3 100644 --- a/certora/configuration/Transfer.conf +++ b/certora/configuration/Transfer.conf @@ -6,5 +6,7 @@ "certora/dispatch/ERC20NoRevert.sol" ], "verify": "TransferHarness:certora/specs/Transfer.spec", + "solc_via_ir": true, + "solc_optimize": "4294967295", "msg": "Morpho Blue Transfer" } From 40577909d20ff5440a0a8f3cabdd8a4d1524e5d9 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Fri, 20 Oct 2023 09:06:17 +0200 Subject: [PATCH 2/4] fix: use prover args for via-IR --- .github/workflows/certora.yml | 2 +- certora/configuration/AccrueInterest.conf | 1 + certora/configuration/ConsistentState.conf | 3 +++ certora/configuration/ExactMath.conf | 1 + certora/configuration/ExitLiquidity.conf | 3 +++ certora/configuration/Health.conf | 1 + certora/configuration/LibSummary.conf | 3 +++ certora/configuration/Liveness.conf | 3 +++ certora/configuration/RatioMath.conf | 1 + certora/configuration/Reentrancy.conf | 1 + certora/configuration/Reverts.conf | 3 +++ certora/configuration/Transfer.conf | 3 +++ certora/specs/AccrueInterest.spec | 2 +- certora/specs/ConsistentState.spec | 2 +- certora/specs/ExactMath.spec | 2 +- certora/specs/ExitLiquidity.spec | 2 +- certora/specs/Health.spec | 2 +- certora/specs/LibSummary.spec | 2 +- certora/specs/Liveness.spec | 2 +- certora/specs/RatioMath.spec | 2 +- certora/specs/Reentrancy.spec | 2 +- certora/specs/Reverts.spec | 2 +- 22 files changed, 34 insertions(+), 11 deletions(-) diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml index 34c0930ba..3b5fd9702 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 + run: pip install certora-cli-beta - name: Install solc run: | diff --git a/certora/configuration/AccrueInterest.conf b/certora/configuration/AccrueInterest.conf index c7a96c942..a74784832 100644 --- a/certora/configuration/AccrueInterest.conf +++ b/certora/configuration/AccrueInterest.conf @@ -6,6 +6,7 @@ "solc_via_ir": true, "solc_optimize": "4294967295", "prover_args": [ + "-functionFinderMode relaxed", "-smt_hashingScheme plaininjectivity", "-mediumTimeout 30" ], diff --git a/certora/configuration/ConsistentState.conf b/certora/configuration/ConsistentState.conf index 22ed316a7..302de8f93 100644 --- a/certora/configuration/ConsistentState.conf +++ b/certora/configuration/ConsistentState.conf @@ -5,5 +5,8 @@ "verify": "MorphoHarness:certora/specs/ConsistentState.spec", "solc_via_ir": true, "solc_optimize": "4294967295", + "prover_args": [ + "-functionFinderMode relaxed" + ], "msg": "Morpho Blue Consistent State" } diff --git a/certora/configuration/ExactMath.conf b/certora/configuration/ExactMath.conf index 1b518595c..01e076480 100644 --- a/certora/configuration/ExactMath.conf +++ b/certora/configuration/ExactMath.conf @@ -6,6 +6,7 @@ "solc_via_ir": true, "solc_optimize": "4294967295", "prover_args": [ + "-functionFinderMode relaxed", "-smt_hashingScheme plaininjectivity", "-mediumTimeout 30" ], diff --git a/certora/configuration/ExitLiquidity.conf b/certora/configuration/ExitLiquidity.conf index 8c572f1e0..e877f474e 100644 --- a/certora/configuration/ExitLiquidity.conf +++ b/certora/configuration/ExitLiquidity.conf @@ -5,5 +5,8 @@ "verify": "MorphoHarness:certora/specs/ExitLiquidity.spec", "solc_via_ir": true, "solc_optimize": "4294967295", + "prover_args": [ + "-functionFinderMode relaxed" + ], "msg": "Morpho Blue Exit Liquidity" } diff --git a/certora/configuration/Health.conf b/certora/configuration/Health.conf index 843c2de36..a4d41f736 100644 --- a/certora/configuration/Health.conf +++ b/certora/configuration/Health.conf @@ -7,6 +7,7 @@ "solc_via_ir": true, "solc_optimize": "4294967295", "prover_args": [ + "-functionFinderMode relaxed", "-smt_hashingScheme plaininjectivity" ], "msg": "Morpho Blue Health" diff --git a/certora/configuration/LibSummary.conf b/certora/configuration/LibSummary.conf index e5390adbd..cb422db6d 100644 --- a/certora/configuration/LibSummary.conf +++ b/certora/configuration/LibSummary.conf @@ -5,5 +5,8 @@ "verify": "MorphoHarness:certora/specs/LibSummary.spec", "solc_via_ir": true, "solc_optimize": "4294967295", + "prover_args": [ + "-functionFinderMode relaxed" + ], "msg": "Morpho Blue Lib Summary" } diff --git a/certora/configuration/Liveness.conf b/certora/configuration/Liveness.conf index 3d8ffd2b8..a3962c859 100644 --- a/certora/configuration/Liveness.conf +++ b/certora/configuration/Liveness.conf @@ -5,5 +5,8 @@ "verify": "MorphoInternalAccess:certora/specs/Liveness.spec", "solc_via_ir": true, "solc_optimize": "4294967295", + "prover_args": [ + "-functionFinderMode relaxed" + ], "msg": "Morpho Blue Liveness" } diff --git a/certora/configuration/RatioMath.conf b/certora/configuration/RatioMath.conf index 88f4ffa1c..79706675f 100644 --- a/certora/configuration/RatioMath.conf +++ b/certora/configuration/RatioMath.conf @@ -6,6 +6,7 @@ "solc_via_ir": true, "solc_optimize": "4294967295", "prover_args": [ + "-functionFinderMode relaxed", "-smt_hashingScheme plaininjectivity" ], "msg": "Morpho Blue Ratio Math" diff --git a/certora/configuration/Reentrancy.conf b/certora/configuration/Reentrancy.conf index 2319b8aa4..2bc66c580 100644 --- a/certora/configuration/Reentrancy.conf +++ b/certora/configuration/Reentrancy.conf @@ -6,6 +6,7 @@ "solc_via_ir": true, "solc_optimize": "4294967295", "prover_args": [ + "-functionFinderMode relaxed", "-enableStorageSplitting false" ], "msg": "Morpho Blue Reentrancy" diff --git a/certora/configuration/Reverts.conf b/certora/configuration/Reverts.conf index 5d270d051..1313245ef 100644 --- a/certora/configuration/Reverts.conf +++ b/certora/configuration/Reverts.conf @@ -5,5 +5,8 @@ "verify": "MorphoHarness:certora/specs/Reverts.spec", "solc_via_ir": true, "solc_optimize": "4294967295", + "prover_args": [ + "-functionFinderMode relaxed", + ], "msg": "Morpho Blue Reverts" } diff --git a/certora/configuration/Transfer.conf b/certora/configuration/Transfer.conf index c33b1dfc3..b76cf3575 100644 --- a/certora/configuration/Transfer.conf +++ b/certora/configuration/Transfer.conf @@ -8,5 +8,8 @@ "verify": "TransferHarness:certora/specs/Transfer.spec", "solc_via_ir": true, "solc_optimize": "4294967295", + "prover_args": [ + "-functionFinderMode relaxed" + ], "msg": "Morpho Blue Transfer" } diff --git a/certora/specs/AccrueInterest.spec b/certora/specs/AccrueInterest.spec index 3af214790..824cce07e 100644 --- a/certora/specs/AccrueInterest.spec +++ b/certora/specs/AccrueInterest.spec @@ -1,6 +1,6 @@ // SPDX-License-Identifier: GPL-2.0-or-later methods { - function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE(true); + function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE; function MathLib.mulDivDown(uint256 a, uint256 b, uint256 c) internal returns uint256 => ghostMulDivDown(a,b,c); function MathLib.mulDivUp(uint256 a, uint256 b, uint256 c) internal returns uint256 => ghostMulDivUp(a,b,c); function MathLib.wTaylorCompounded(uint256 a, uint256 b) internal returns uint256 => ghostTaylorCompounded(a, b); diff --git a/certora/specs/ConsistentState.spec b/certora/specs/ConsistentState.spec index 5324bd5b4..49e0c1df8 100644 --- a/certora/specs/ConsistentState.spec +++ b/certora/specs/ConsistentState.spec @@ -1,6 +1,6 @@ // SPDX-License-Identifier: GPL-2.0-or-later methods { - function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE(true); + function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE; function totalSupplyAssets(MorphoHarness.Id) external returns uint256 envfree; function totalSupplyShares(MorphoHarness.Id) external returns uint256 envfree; function totalBorrowAssets(MorphoHarness.Id) external returns uint256 envfree; diff --git a/certora/specs/ExactMath.spec b/certora/specs/ExactMath.spec index 3ca2c3736..6e08543c8 100644 --- a/certora/specs/ExactMath.spec +++ b/certora/specs/ExactMath.spec @@ -1,6 +1,6 @@ // SPDX-License-Identifier: GPL-2.0-or-later methods { - function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE(true); + function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE; function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; function virtualTotalSupplyAssets(MorphoHarness.Id) external returns uint256 envfree; function virtualTotalSupplyShares(MorphoHarness.Id) external returns uint256 envfree; diff --git a/certora/specs/ExitLiquidity.spec b/certora/specs/ExitLiquidity.spec index 30036108b..bf90ec31c 100644 --- a/certora/specs/ExitLiquidity.spec +++ b/certora/specs/ExitLiquidity.spec @@ -1,6 +1,6 @@ // SPDX-License-Identifier: GPL-2.0-or-later methods { - function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE(true); + function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE; function supplyShares(MorphoHarness.Id, address) external returns uint256 envfree; function borrowShares(MorphoHarness.Id, address) external returns uint256 envfree; function collateral(MorphoHarness.Id, address) external returns uint256 envfree; diff --git a/certora/specs/Health.spec b/certora/specs/Health.spec index 3602de29c..bac2aeba1 100644 --- a/certora/specs/Health.spec +++ b/certora/specs/Health.spec @@ -1,6 +1,6 @@ // SPDX-License-Identifier: GPL-2.0-or-later methods { - function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE(true); + function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE; function lastUpdate(MorphoHarness.Id) external returns uint256 envfree; function totalBorrowShares(MorphoHarness.Id) external returns uint256 envfree; function borrowShares(MorphoHarness.Id, address) external returns uint256 envfree; diff --git a/certora/specs/LibSummary.spec b/certora/specs/LibSummary.spec index 21cd67538..64322f7dc 100644 --- a/certora/specs/LibSummary.spec +++ b/certora/specs/LibSummary.spec @@ -1,6 +1,6 @@ // SPDX-License-Identifier: GPL-2.0-or-later methods { - function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE(true); + function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE; function libMulDivUp(uint256, uint256, uint256) external returns uint256 envfree; function libMulDivDown(uint256, uint256, uint256) external returns uint256 envfree; function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; diff --git a/certora/specs/Liveness.spec b/certora/specs/Liveness.spec index 5e7f46b1c..e5b96af82 100644 --- a/certora/specs/Liveness.spec +++ b/certora/specs/Liveness.spec @@ -1,6 +1,6 @@ // SPDX-License-Identifier: GPL-2.0-or-later methods { - function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE(true); + function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE; function totalSupplyAssets(MorphoInternalAccess.Id) external returns uint256 envfree; function totalSupplyShares(MorphoInternalAccess.Id) external returns uint256 envfree; function totalBorrowAssets(MorphoInternalAccess.Id) external returns uint256 envfree; diff --git a/certora/specs/RatioMath.spec b/certora/specs/RatioMath.spec index af690462e..2d138ad13 100644 --- a/certora/specs/RatioMath.spec +++ b/certora/specs/RatioMath.spec @@ -1,6 +1,6 @@ // SPDX-License-Identifier: GPL-2.0-or-later methods { - function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE(true); + function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE; function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; function virtualTotalSupplyAssets(MorphoHarness.Id) external returns uint256 envfree; function virtualTotalSupplyShares(MorphoHarness.Id) external returns uint256 envfree; diff --git a/certora/specs/Reentrancy.spec b/certora/specs/Reentrancy.spec index 0a55276ea..5cb2b1639 100644 --- a/certora/specs/Reentrancy.spec +++ b/certora/specs/Reentrancy.spec @@ -1,6 +1,6 @@ // SPDX-License-Identifier: GPL-2.0-or-later methods { - function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE(true); + function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE; function _.borrowRate(MorphoHarness.MarketParams marketParams, MorphoHarness.Market) external => summaryBorrowRate() expect uint256; } diff --git a/certora/specs/Reverts.spec b/certora/specs/Reverts.spec index c54c06a21..7ecb5be1c 100644 --- a/certora/specs/Reverts.spec +++ b/certora/specs/Reverts.spec @@ -1,6 +1,6 @@ // SPDX-License-Identifier: GPL-2.0-or-later methods { - function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE(true); + function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE; function owner() external returns address envfree; function totalSupplyAssets(MorphoHarness.Id) external returns uint256 envfree; function totalBorrowAssets(MorphoHarness.Id) external returns uint256 envfree; From bff6fe5067b8b7a947113445428730cb35208dc8 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Fri, 20 Oct 2023 09:58:35 +0200 Subject: [PATCH 3/4] fix: add prover version master --- certora/configuration/AccrueInterest.conf | 3 ++- certora/configuration/ConsistentState.conf | 3 ++- certora/configuration/ExactMath.conf | 3 ++- certora/configuration/ExitLiquidity.conf | 3 ++- certora/configuration/Health.conf | 3 ++- certora/configuration/LibSummary.conf | 3 ++- certora/configuration/Liveness.conf | 3 ++- certora/configuration/RatioMath.conf | 3 ++- certora/configuration/Reentrancy.conf | 3 ++- certora/configuration/Reverts.conf | 3 ++- certora/configuration/Transfer.conf | 3 ++- 11 files changed, 22 insertions(+), 11 deletions(-) diff --git a/certora/configuration/AccrueInterest.conf b/certora/configuration/AccrueInterest.conf index a74784832..81ad98c37 100644 --- a/certora/configuration/AccrueInterest.conf +++ b/certora/configuration/AccrueInterest.conf @@ -2,9 +2,10 @@ "files": [ "certora/harness/MorphoHarness.sol" ], - "verify": "MorphoHarness:certora/specs/AccrueInterest.spec", "solc_via_ir": true, "solc_optimize": "4294967295", + "verify": "MorphoHarness:certora/specs/AccrueInterest.spec", + "prover_version": "master", "prover_args": [ "-functionFinderMode relaxed", "-smt_hashingScheme plaininjectivity", diff --git a/certora/configuration/ConsistentState.conf b/certora/configuration/ConsistentState.conf index 302de8f93..893507640 100644 --- a/certora/configuration/ConsistentState.conf +++ b/certora/configuration/ConsistentState.conf @@ -2,9 +2,10 @@ "files": [ "certora/harness/MorphoHarness.sol" ], - "verify": "MorphoHarness:certora/specs/ConsistentState.spec", "solc_via_ir": true, "solc_optimize": "4294967295", + "verify": "MorphoHarness:certora/specs/ConsistentState.spec", + "prover_version": "master", "prover_args": [ "-functionFinderMode relaxed" ], diff --git a/certora/configuration/ExactMath.conf b/certora/configuration/ExactMath.conf index 01e076480..b3dd305f2 100644 --- a/certora/configuration/ExactMath.conf +++ b/certora/configuration/ExactMath.conf @@ -2,9 +2,10 @@ "files": [ "certora/harness/MorphoHarness.sol" ], - "verify": "MorphoHarness:certora/specs/ExactMath.spec", "solc_via_ir": true, "solc_optimize": "4294967295", + "verify": "MorphoHarness:certora/specs/ExactMath.spec", + "prover_version": "master", "prover_args": [ "-functionFinderMode relaxed", "-smt_hashingScheme plaininjectivity", diff --git a/certora/configuration/ExitLiquidity.conf b/certora/configuration/ExitLiquidity.conf index e877f474e..8141d4208 100644 --- a/certora/configuration/ExitLiquidity.conf +++ b/certora/configuration/ExitLiquidity.conf @@ -2,9 +2,10 @@ "files": [ "certora/harness/MorphoHarness.sol" ], - "verify": "MorphoHarness:certora/specs/ExitLiquidity.spec", "solc_via_ir": true, "solc_optimize": "4294967295", + "verify": "MorphoHarness:certora/specs/ExitLiquidity.spec", + "prover_version": "master", "prover_args": [ "-functionFinderMode relaxed" ], diff --git a/certora/configuration/Health.conf b/certora/configuration/Health.conf index a4d41f736..05f17ff31 100644 --- a/certora/configuration/Health.conf +++ b/certora/configuration/Health.conf @@ -3,9 +3,10 @@ "certora/harness/MorphoHarness.sol", "src/mocks/OracleMock.sol" ], - "verify": "MorphoHarness:certora/specs/Health.spec", "solc_via_ir": true, "solc_optimize": "4294967295", + "verify": "MorphoHarness:certora/specs/Health.spec", + "prover_version": "master", "prover_args": [ "-functionFinderMode relaxed", "-smt_hashingScheme plaininjectivity" diff --git a/certora/configuration/LibSummary.conf b/certora/configuration/LibSummary.conf index cb422db6d..684545312 100644 --- a/certora/configuration/LibSummary.conf +++ b/certora/configuration/LibSummary.conf @@ -2,9 +2,10 @@ "files": [ "certora/harness/MorphoHarness.sol" ], - "verify": "MorphoHarness:certora/specs/LibSummary.spec", "solc_via_ir": true, "solc_optimize": "4294967295", + "verify": "MorphoHarness:certora/specs/LibSummary.spec", + "prover_version": "master", "prover_args": [ "-functionFinderMode relaxed" ], diff --git a/certora/configuration/Liveness.conf b/certora/configuration/Liveness.conf index a3962c859..d88eda21f 100644 --- a/certora/configuration/Liveness.conf +++ b/certora/configuration/Liveness.conf @@ -2,9 +2,10 @@ "files": [ "certora/harness/MorphoInternalAccess.sol" ], - "verify": "MorphoInternalAccess:certora/specs/Liveness.spec", "solc_via_ir": true, "solc_optimize": "4294967295", + "verify": "MorphoInternalAccess:certora/specs/Liveness.spec", + "prover_version": "master", "prover_args": [ "-functionFinderMode relaxed" ], diff --git a/certora/configuration/RatioMath.conf b/certora/configuration/RatioMath.conf index 79706675f..ac87ac46b 100644 --- a/certora/configuration/RatioMath.conf +++ b/certora/configuration/RatioMath.conf @@ -2,9 +2,10 @@ "files": [ "certora/harness/MorphoHarness.sol" ], - "verify": "MorphoHarness:certora/specs/RatioMath.spec", "solc_via_ir": true, "solc_optimize": "4294967295", + "verify": "MorphoHarness:certora/specs/RatioMath.spec", + "prover_version": "master", "prover_args": [ "-functionFinderMode relaxed", "-smt_hashingScheme plaininjectivity" diff --git a/certora/configuration/Reentrancy.conf b/certora/configuration/Reentrancy.conf index 2bc66c580..707dcd312 100644 --- a/certora/configuration/Reentrancy.conf +++ b/certora/configuration/Reentrancy.conf @@ -2,9 +2,10 @@ "files": [ "certora/harness/MorphoHarness.sol" ], - "verify": "MorphoHarness:certora/specs/Reentrancy.spec", "solc_via_ir": true, "solc_optimize": "4294967295", + "verify": "MorphoHarness:certora/specs/Reentrancy.spec", + "prover_version": "master", "prover_args": [ "-functionFinderMode relaxed", "-enableStorageSplitting false" diff --git a/certora/configuration/Reverts.conf b/certora/configuration/Reverts.conf index 1313245ef..9801f4549 100644 --- a/certora/configuration/Reverts.conf +++ b/certora/configuration/Reverts.conf @@ -2,9 +2,10 @@ "files": [ "certora/harness/MorphoHarness.sol" ], - "verify": "MorphoHarness:certora/specs/Reverts.spec", "solc_via_ir": true, "solc_optimize": "4294967295", + "verify": "MorphoHarness:certora/specs/Reverts.spec", + "prover_version": "master", "prover_args": [ "-functionFinderMode relaxed", ], diff --git a/certora/configuration/Transfer.conf b/certora/configuration/Transfer.conf index b76cf3575..2c6a0aaea 100644 --- a/certora/configuration/Transfer.conf +++ b/certora/configuration/Transfer.conf @@ -5,9 +5,10 @@ "certora/dispatch/ERC20USDT.sol", "certora/dispatch/ERC20NoRevert.sol" ], - "verify": "TransferHarness:certora/specs/Transfer.spec", "solc_via_ir": true, "solc_optimize": "4294967295", + "verify": "TransferHarness:certora/specs/Transfer.spec", + "prover_version": "master", "prover_args": [ "-functionFinderMode relaxed" ], From e32ee4657e6ba064c4aa4dfb5b4b601f641dccb3 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Tue, 24 Oct 2023 16:51:02 +0200 Subject: [PATCH 4/4] fix: adapt function_finder_mode to 5.0.1 --- certora/configuration/AccrueInterest.conf | 2 +- certora/configuration/ConsistentState.conf | 4 +--- certora/configuration/ExactMath.conf | 2 +- certora/configuration/ExitLiquidity.conf | 4 +--- certora/configuration/Health.conf | 2 +- certora/configuration/LibSummary.conf | 4 +--- certora/configuration/Liveness.conf | 4 +--- certora/configuration/RatioMath.conf | 5 +---- certora/configuration/Reentrancy.conf | 2 +- certora/configuration/Reverts.conf | 4 +--- certora/configuration/Transfer.conf | 4 +--- 11 files changed, 11 insertions(+), 26 deletions(-) diff --git a/certora/configuration/AccrueInterest.conf b/certora/configuration/AccrueInterest.conf index 81ad98c37..fcab14340 100644 --- a/certora/configuration/AccrueInterest.conf +++ b/certora/configuration/AccrueInterest.conf @@ -6,8 +6,8 @@ "solc_optimize": "4294967295", "verify": "MorphoHarness:certora/specs/AccrueInterest.spec", "prover_version": "master", + "function_finder_mode": "relaxed", "prover_args": [ - "-functionFinderMode relaxed", "-smt_hashingScheme plaininjectivity", "-mediumTimeout 30" ], diff --git a/certora/configuration/ConsistentState.conf b/certora/configuration/ConsistentState.conf index 893507640..cc7b80d09 100644 --- a/certora/configuration/ConsistentState.conf +++ b/certora/configuration/ConsistentState.conf @@ -6,8 +6,6 @@ "solc_optimize": "4294967295", "verify": "MorphoHarness:certora/specs/ConsistentState.spec", "prover_version": "master", - "prover_args": [ - "-functionFinderMode relaxed" - ], + "function_finder_mode": "relaxed", "msg": "Morpho Blue Consistent State" } diff --git a/certora/configuration/ExactMath.conf b/certora/configuration/ExactMath.conf index b3dd305f2..094974c1b 100644 --- a/certora/configuration/ExactMath.conf +++ b/certora/configuration/ExactMath.conf @@ -6,8 +6,8 @@ "solc_optimize": "4294967295", "verify": "MorphoHarness:certora/specs/ExactMath.spec", "prover_version": "master", + "function_finder_mode": "relaxed", "prover_args": [ - "-functionFinderMode relaxed", "-smt_hashingScheme plaininjectivity", "-mediumTimeout 30" ], diff --git a/certora/configuration/ExitLiquidity.conf b/certora/configuration/ExitLiquidity.conf index 8141d4208..8a44fa297 100644 --- a/certora/configuration/ExitLiquidity.conf +++ b/certora/configuration/ExitLiquidity.conf @@ -6,8 +6,6 @@ "solc_optimize": "4294967295", "verify": "MorphoHarness:certora/specs/ExitLiquidity.spec", "prover_version": "master", - "prover_args": [ - "-functionFinderMode relaxed" - ], + "function_finder_mode": "relaxed", "msg": "Morpho Blue Exit Liquidity" } diff --git a/certora/configuration/Health.conf b/certora/configuration/Health.conf index 05f17ff31..3dc4b708b 100644 --- a/certora/configuration/Health.conf +++ b/certora/configuration/Health.conf @@ -7,8 +7,8 @@ "solc_optimize": "4294967295", "verify": "MorphoHarness:certora/specs/Health.spec", "prover_version": "master", + "function_finder_mode": "relaxed", "prover_args": [ - "-functionFinderMode relaxed", "-smt_hashingScheme plaininjectivity" ], "msg": "Morpho Blue Health" diff --git a/certora/configuration/LibSummary.conf b/certora/configuration/LibSummary.conf index 684545312..19860baf3 100644 --- a/certora/configuration/LibSummary.conf +++ b/certora/configuration/LibSummary.conf @@ -6,8 +6,6 @@ "solc_optimize": "4294967295", "verify": "MorphoHarness:certora/specs/LibSummary.spec", "prover_version": "master", - "prover_args": [ - "-functionFinderMode relaxed" - ], + "function_finder_mode": "relaxed", "msg": "Morpho Blue Lib Summary" } diff --git a/certora/configuration/Liveness.conf b/certora/configuration/Liveness.conf index d88eda21f..1f36ed79c 100644 --- a/certora/configuration/Liveness.conf +++ b/certora/configuration/Liveness.conf @@ -6,8 +6,6 @@ "solc_optimize": "4294967295", "verify": "MorphoInternalAccess:certora/specs/Liveness.spec", "prover_version": "master", - "prover_args": [ - "-functionFinderMode relaxed" - ], + "function_finder_mode": "relaxed", "msg": "Morpho Blue Liveness" } diff --git a/certora/configuration/RatioMath.conf b/certora/configuration/RatioMath.conf index ac87ac46b..4d6aeef31 100644 --- a/certora/configuration/RatioMath.conf +++ b/certora/configuration/RatioMath.conf @@ -6,9 +6,6 @@ "solc_optimize": "4294967295", "verify": "MorphoHarness:certora/specs/RatioMath.spec", "prover_version": "master", - "prover_args": [ - "-functionFinderMode relaxed", - "-smt_hashingScheme plaininjectivity" - ], + "function_finder_mode": "relaxed", "msg": "Morpho Blue Ratio Math" } diff --git a/certora/configuration/Reentrancy.conf b/certora/configuration/Reentrancy.conf index 707dcd312..d2ede5aa1 100644 --- a/certora/configuration/Reentrancy.conf +++ b/certora/configuration/Reentrancy.conf @@ -6,8 +6,8 @@ "solc_optimize": "4294967295", "verify": "MorphoHarness:certora/specs/Reentrancy.spec", "prover_version": "master", + "function_finder_mode": "relaxed", "prover_args": [ - "-functionFinderMode relaxed", "-enableStorageSplitting false" ], "msg": "Morpho Blue Reentrancy" diff --git a/certora/configuration/Reverts.conf b/certora/configuration/Reverts.conf index 9801f4549..0f44a6498 100644 --- a/certora/configuration/Reverts.conf +++ b/certora/configuration/Reverts.conf @@ -6,8 +6,6 @@ "solc_optimize": "4294967295", "verify": "MorphoHarness:certora/specs/Reverts.spec", "prover_version": "master", - "prover_args": [ - "-functionFinderMode relaxed", - ], + "function_finder_mode": "relaxed", "msg": "Morpho Blue Reverts" } diff --git a/certora/configuration/Transfer.conf b/certora/configuration/Transfer.conf index 2c6a0aaea..c13242a43 100644 --- a/certora/configuration/Transfer.conf +++ b/certora/configuration/Transfer.conf @@ -9,8 +9,6 @@ "solc_optimize": "4294967295", "verify": "TransferHarness:certora/specs/Transfer.spec", "prover_version": "master", - "prover_args": [ - "-functionFinderMode relaxed" - ], + "function_finder_mode": "relaxed", "msg": "Morpho Blue Transfer" }