From 74f40b749fe9cdbc4749ef92d70e3a2c9b2a7e87 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Wed, 9 Oct 2024 16:07:43 +0200 Subject: [PATCH 1/3] refactor: remove unnecessary ghost variable assignment --- certora/specs/Health.spec | 1 - 1 file changed, 1 deletion(-) diff --git a/certora/specs/Health.spec b/certora/specs/Health.spec index 6f2d395e..cb764b01 100644 --- a/certora/specs/Health.spec +++ b/certora/specs/Health.spec @@ -67,7 +67,6 @@ filtered { f -> !f.isView } mathint collateralBefore = collateral(id, user); - priceChanged = false; f(e, data); mathint collateralAfter = collateral(id, user); From a56da03797f913477e184936208e0af75a1208a8 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Wed, 9 Oct 2024 16:08:06 +0200 Subject: [PATCH 2/3] chore: format conf files according to prettier rules for JSON --- certora/confs/AccrueInterest.conf | 26 +++++++++++------------ certora/confs/AssetsAccounting.conf | 16 +++++++------- certora/confs/ConsistentState.conf | 16 +++++++------- certora/confs/ExactMath.conf | 33 ++++++++++++++--------------- certora/confs/ExchangeRate.conf | 24 ++++++++++----------- certora/confs/Health.conf | 24 ++++++++++----------- certora/confs/LibSummary.conf | 22 +++++++++---------- certora/confs/Liveness.conf | 16 +++++++------- certora/confs/Reentrancy.conf | 22 +++++++++---------- certora/confs/Reverts.conf | 16 +++++++------- certora/confs/StayHealthy.conf | 32 ++++++++++++++-------------- certora/confs/Transfer.conf | 22 +++++++++---------- 12 files changed, 134 insertions(+), 135 deletions(-) diff --git a/certora/confs/AccrueInterest.conf b/certora/confs/AccrueInterest.conf index 80570064..3841d32c 100644 --- a/certora/confs/AccrueInterest.conf +++ b/certora/confs/AccrueInterest.conf @@ -1,15 +1,15 @@ { - "files": [ - "certora/harness/MorphoHarness.sol", - ], - "solc": "solc-0.8.19", - "verify": "MorphoHarness:certora/specs/AccrueInterest.spec", - "prover_args": [ - "-depth 3", - "-mediumTimeout 30", - "-smt_hashingScheme plaininjectivity", - ], - "rule_sanity": "basic", - "server": "production", - "msg": "Morpho Blue Accrue Interest" + "files": [ + "certora/harness/MorphoHarness.sol" + ], + "solc": "solc-0.8.19", + "verify": "MorphoHarness:certora/specs/AccrueInterest.spec", + "prover_args": [ + "-depth 3", + "-mediumTimeout 30", + "-smt_hashingScheme plaininjectivity" + ], + "rule_sanity": "basic", + "server": "production", + "msg": "Morpho Blue Accrue Interest" } diff --git a/certora/confs/AssetsAccounting.conf b/certora/confs/AssetsAccounting.conf index b31cecfa..72e3e20e 100644 --- a/certora/confs/AssetsAccounting.conf +++ b/certora/confs/AssetsAccounting.conf @@ -1,10 +1,10 @@ { - "files": [ - "certora/harness/MorphoHarness.sol", - ], - "solc": "solc-0.8.19", - "verify": "MorphoHarness:certora/specs/AssetsAccounting.spec", - "rule_sanity": "basic", - "server": "production", - "msg": "Morpho Blue Assets Accounting" + "files": [ + "certora/harness/MorphoHarness.sol" + ], + "solc": "solc-0.8.19", + "verify": "MorphoHarness:certora/specs/AssetsAccounting.spec", + "rule_sanity": "basic", + "server": "production", + "msg": "Morpho Blue Assets Accounting" } diff --git a/certora/confs/ConsistentState.conf b/certora/confs/ConsistentState.conf index e946d31d..a3749723 100644 --- a/certora/confs/ConsistentState.conf +++ b/certora/confs/ConsistentState.conf @@ -1,10 +1,10 @@ { - "files": [ - "certora/harness/MorphoHarness.sol", - ], - "solc": "solc-0.8.19", - "verify": "MorphoHarness:certora/specs/ConsistentState.spec", - "rule_sanity": "basic", - "server": "production", - "msg": "Morpho Blue Consistent State" + "files": [ + "certora/harness/MorphoHarness.sol" + ], + "solc": "solc-0.8.19", + "verify": "MorphoHarness:certora/specs/ConsistentState.spec", + "rule_sanity": "basic", + "server": "production", + "msg": "Morpho Blue Consistent State" } diff --git a/certora/confs/ExactMath.conf b/certora/confs/ExactMath.conf index a6a162f4..2eb96627 100644 --- a/certora/confs/ExactMath.conf +++ b/certora/confs/ExactMath.conf @@ -1,19 +1,18 @@ { - "files": [ - "certora/harness/MorphoHarness.sol", - ], - "solc": "solc-0.8.19", - "verify": "MorphoHarness:certora/specs/ExactMath.spec", - "rule_sanity": "basic", - "prover_args": [ - "-depth 5", - "-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]", - ], - "cache": "none", - "server": "production", - "msg": "Morpho Blue Exact Math" + "files": [ + "certora/harness/MorphoHarness.sol" + ], + "solc": "solc-0.8.19", + "verify": "MorphoHarness:certora/specs/ExactMath.spec", + "rule_sanity": "basic", + "prover_args": [ + "-depth 5", + "-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", + "msg": "Morpho Blue Exact Math" } diff --git a/certora/confs/ExchangeRate.conf b/certora/confs/ExchangeRate.conf index da6b7c55..0e1f805f 100644 --- a/certora/confs/ExchangeRate.conf +++ b/certora/confs/ExchangeRate.conf @@ -1,14 +1,14 @@ { - "files": [ - "certora/harness/MorphoHarness.sol", - ], - "solc": "solc-0.8.19", - "verify": "MorphoHarness:certora/specs/ExchangeRate.spec", - "rule_sanity": "basic", - "prover_args": [ - "-smt_hashingScheme plaininjectivity", - "-smt_easy_LIA true", - ], - "server": "production", - "msg": "Morpho Blue Exchange Rate" + "files": [ + "certora/harness/MorphoHarness.sol" + ], + "solc": "solc-0.8.19", + "verify": "MorphoHarness:certora/specs/ExchangeRate.spec", + "rule_sanity": "basic", + "prover_args": [ + "-smt_hashingScheme plaininjectivity", + "-smt_easy_LIA true" + ], + "server": "production", + "msg": "Morpho Blue Exchange Rate" } diff --git a/certora/confs/Health.conf b/certora/confs/Health.conf index 0b4cf189..30aeeab1 100644 --- a/certora/confs/Health.conf +++ b/certora/confs/Health.conf @@ -1,14 +1,14 @@ { - "files": [ - "certora/harness/MorphoHarness.sol", - "src/mocks/OracleMock.sol" - ], - "solc": "solc-0.8.19", - "verify": "MorphoHarness:certora/specs/Health.spec", - "rule_sanity": "basic", - "prover_args": [ - "-smt_hashingScheme plaininjectivity", - ], - "server": "production", - "msg": "Morpho Blue Health" + "files": [ + "certora/harness/MorphoHarness.sol", + "src/mocks/OracleMock.sol" + ], + "solc": "solc-0.8.19", + "verify": "MorphoHarness:certora/specs/Health.spec", + "rule_sanity": "basic", + "prover_args": [ + "-smt_hashingScheme plaininjectivity" + ], + "server": "production", + "msg": "Morpho Blue Health" } diff --git a/certora/confs/LibSummary.conf b/certora/confs/LibSummary.conf index 804928d2..dc5efc34 100644 --- a/certora/confs/LibSummary.conf +++ b/certora/confs/LibSummary.conf @@ -1,13 +1,13 @@ { - "files": [ - "certora/harness/MorphoHarness.sol", - ], - "solc": "solc-0.8.19", - "verify": "MorphoHarness:certora/specs/LibSummary.spec", - "rule_sanity": "basic", - "prover_args": [ - "-smt_bitVectorTheory true" - ], - "server": "production", - "msg": "Morpho Blue Lib Summary" + "files": [ + "certora/harness/MorphoHarness.sol" + ], + "solc": "solc-0.8.19", + "verify": "MorphoHarness:certora/specs/LibSummary.spec", + "rule_sanity": "basic", + "prover_args": [ + "-smt_bitVectorTheory true" + ], + "server": "production", + "msg": "Morpho Blue Lib Summary" } diff --git a/certora/confs/Liveness.conf b/certora/confs/Liveness.conf index 2dafcec5..f9196903 100644 --- a/certora/confs/Liveness.conf +++ b/certora/confs/Liveness.conf @@ -1,10 +1,10 @@ { - "files": [ - "certora/harness/MorphoInternalAccess.sol", - ], - "solc": "solc-0.8.19", - "verify": "MorphoInternalAccess:certora/specs/Liveness.spec", - "rule_sanity": "basic", - "server": "production", - "msg": "Morpho Blue Liveness" + "files": [ + "certora/harness/MorphoInternalAccess.sol" + ], + "solc": "solc-0.8.19", + "verify": "MorphoInternalAccess:certora/specs/Liveness.spec", + "rule_sanity": "basic", + "server": "production", + "msg": "Morpho Blue Liveness" } diff --git a/certora/confs/Reentrancy.conf b/certora/confs/Reentrancy.conf index 15c3577f..a7a409c4 100644 --- a/certora/confs/Reentrancy.conf +++ b/certora/confs/Reentrancy.conf @@ -1,13 +1,13 @@ { - "files": [ - "certora/harness/MorphoHarness.sol", - ], - "solc": "solc-0.8.19", - "verify": "MorphoHarness:certora/specs/Reentrancy.spec", - "rule_sanity": "basic", - "prover_args": [ - "-enableStorageSplitting false", - ], - "server": "production", - "msg": "Morpho Blue Reentrancy" + "files": [ + "certora/harness/MorphoHarness.sol" + ], + "solc": "solc-0.8.19", + "verify": "MorphoHarness:certora/specs/Reentrancy.spec", + "rule_sanity": "basic", + "prover_args": [ + "-enableStorageSplitting false" + ], + "server": "production", + "msg": "Morpho Blue Reentrancy" } diff --git a/certora/confs/Reverts.conf b/certora/confs/Reverts.conf index 7f8175a1..c1d6dadc 100644 --- a/certora/confs/Reverts.conf +++ b/certora/confs/Reverts.conf @@ -1,10 +1,10 @@ { - "files": [ - "certora/harness/MorphoHarness.sol", - ], - "solc": "solc-0.8.19", - "verify": "MorphoHarness:certora/specs/Reverts.spec", - "rule_sanity": "basic", - "server": "production", - "msg": "Morpho Blue Reverts" + "files": [ + "certora/harness/MorphoHarness.sol" + ], + "solc": "solc-0.8.19", + "verify": "MorphoHarness:certora/specs/Reverts.spec", + "rule_sanity": "basic", + "server": "production", + "msg": "Morpho Blue Reverts" } diff --git a/certora/confs/StayHealthy.conf b/certora/confs/StayHealthy.conf index 567f70d4..7364de17 100644 --- a/certora/confs/StayHealthy.conf +++ b/certora/confs/StayHealthy.conf @@ -1,18 +1,18 @@ { - "files": [ - "certora/harness/MorphoHarness.sol", - "src/mocks/OracleMock.sol", - ], - "msg": "Morpho Blue Stay Healthy", - "process": "emv", - "prover_args": [ - "-depth 5", - "-mediumTimeout 5", - "-timeout 3600", - "-smt_hashingScheme plaininjectivity" - ], - "rule_sanity": "basic", - "server": "production", - "solc": "solc-0.8.19", - "verify": "MorphoHarness:certora/specs/StayHealthy.spec" + "files": [ + "certora/harness/MorphoHarness.sol", + "src/mocks/OracleMock.sol" + ], + "msg": "Morpho Blue Stay Healthy", + "process": "emv", + "prover_args": [ + "-depth 5", + "-mediumTimeout 5", + "-timeout 3600", + "-smt_hashingScheme plaininjectivity" + ], + "rule_sanity": "basic", + "server": "production", + "solc": "solc-0.8.19", + "verify": "MorphoHarness:certora/specs/StayHealthy.spec" } diff --git a/certora/confs/Transfer.conf b/certora/confs/Transfer.conf index a02ea90f..632ee90c 100644 --- a/certora/confs/Transfer.conf +++ b/certora/confs/Transfer.conf @@ -1,13 +1,13 @@ { - "files": [ - "certora/harness/TransferHarness.sol", - "certora/dispatch/ERC20Standard.sol", - "certora/dispatch/ERC20USDT.sol", - "certora/dispatch/ERC20NoRevert.sol", - ], - "solc": "solc-0.8.19", - "verify": "TransferHarness:certora/specs/Transfer.spec", - "rule_sanity": "basic", - "server": "production", - "msg": "Morpho Blue Transfer" + "files": [ + "certora/harness/TransferHarness.sol", + "certora/dispatch/ERC20Standard.sol", + "certora/dispatch/ERC20USDT.sol", + "certora/dispatch/ERC20NoRevert.sol" + ], + "solc": "solc-0.8.19", + "verify": "TransferHarness:certora/specs/Transfer.spec", + "rule_sanity": "basic", + "server": "production", + "msg": "Morpho Blue Transfer" } From 4446011f2a8f9c149399ed921d98d333022f8c66 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Wed, 9 Oct 2024 17:41:53 +0200 Subject: [PATCH 3/3] feat: solve StayHealthy timeout --- certora/confs/ExactMath.conf | 2 +- certora/confs/ExchangeRate.conf | 2 +- certora/confs/Health.conf | 2 +- certora/confs/LibSummary.conf | 2 +- certora/confs/Reentrancy.conf | 2 +- certora/confs/StayHealthy.conf | 13 +++++-------- 6 files changed, 10 insertions(+), 13 deletions(-) diff --git a/certora/confs/ExactMath.conf b/certora/confs/ExactMath.conf index 2eb96627..7a82fca5 100644 --- a/certora/confs/ExactMath.conf +++ b/certora/confs/ExactMath.conf @@ -4,7 +4,6 @@ ], "solc": "solc-0.8.19", "verify": "MorphoHarness:certora/specs/ExactMath.spec", - "rule_sanity": "basic", "prover_args": [ "-depth 5", "-mediumTimeout 5", @@ -13,6 +12,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]" ], + "rule_sanity": "basic", "server": "production", "msg": "Morpho Blue Exact Math" } diff --git a/certora/confs/ExchangeRate.conf b/certora/confs/ExchangeRate.conf index 0e1f805f..5a549a5e 100644 --- a/certora/confs/ExchangeRate.conf +++ b/certora/confs/ExchangeRate.conf @@ -4,11 +4,11 @@ ], "solc": "solc-0.8.19", "verify": "MorphoHarness:certora/specs/ExchangeRate.spec", - "rule_sanity": "basic", "prover_args": [ "-smt_hashingScheme plaininjectivity", "-smt_easy_LIA true" ], + "rule_sanity": "basic", "server": "production", "msg": "Morpho Blue Exchange Rate" } diff --git a/certora/confs/Health.conf b/certora/confs/Health.conf index 30aeeab1..0b47d05a 100644 --- a/certora/confs/Health.conf +++ b/certora/confs/Health.conf @@ -5,10 +5,10 @@ ], "solc": "solc-0.8.19", "verify": "MorphoHarness:certora/specs/Health.spec", - "rule_sanity": "basic", "prover_args": [ "-smt_hashingScheme plaininjectivity" ], + "rule_sanity": "basic", "server": "production", "msg": "Morpho Blue Health" } diff --git a/certora/confs/LibSummary.conf b/certora/confs/LibSummary.conf index dc5efc34..34526a1f 100644 --- a/certora/confs/LibSummary.conf +++ b/certora/confs/LibSummary.conf @@ -4,10 +4,10 @@ ], "solc": "solc-0.8.19", "verify": "MorphoHarness:certora/specs/LibSummary.spec", - "rule_sanity": "basic", "prover_args": [ "-smt_bitVectorTheory true" ], + "rule_sanity": "basic", "server": "production", "msg": "Morpho Blue Lib Summary" } diff --git a/certora/confs/Reentrancy.conf b/certora/confs/Reentrancy.conf index a7a409c4..6dbec607 100644 --- a/certora/confs/Reentrancy.conf +++ b/certora/confs/Reentrancy.conf @@ -4,10 +4,10 @@ ], "solc": "solc-0.8.19", "verify": "MorphoHarness:certora/specs/Reentrancy.spec", - "rule_sanity": "basic", "prover_args": [ "-enableStorageSplitting false" ], + "rule_sanity": "basic", "server": "production", "msg": "Morpho Blue Reentrancy" } diff --git a/certora/confs/StayHealthy.conf b/certora/confs/StayHealthy.conf index 7364de17..7179c674 100644 --- a/certora/confs/StayHealthy.conf +++ b/certora/confs/StayHealthy.conf @@ -3,16 +3,13 @@ "certora/harness/MorphoHarness.sol", "src/mocks/OracleMock.sol" ], - "msg": "Morpho Blue Stay Healthy", - "process": "emv", + "solc": "solc-0.8.19", + "verify": "MorphoHarness:certora/specs/StayHealthy.spec", "prover_args": [ - "-depth 5", - "-mediumTimeout 5", - "-timeout 3600", - "-smt_hashingScheme plaininjectivity" + "-smt_hashingScheme plaininjectivity", + "-solvers [yices,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:def{randomSeed=8},z3:def{randomSeed=9},z3:def{randomSeed=10}]" ], "rule_sanity": "basic", "server": "production", - "solc": "solc-0.8.19", - "verify": "MorphoHarness:certora/specs/StayHealthy.spec" + "msg": "Morpho Blue Stay Healthy" }