From a56da03797f913477e184936208e0af75a1208a8 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Wed, 9 Oct 2024 16:08:06 +0200 Subject: [PATCH] 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 805700641..3841d32c6 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 b31cecfa3..72e3e20e4 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 e946d31df..a37497230 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 a6a162f49..2eb966273 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 da6b7c558..0e1f805f7 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 0b4cf1895..30aeeab15 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 804928d2f..dc5efc342 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 2dafcec5e..f9196903f 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 15c3577f2..a7a409c49 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 7f8175a1a..c1d6dadc1 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 567f70d48..7364de175 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 a02ea90f8..632ee90cf 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" }