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" }