From 99685a80a628fefe5fdb1c58bbfe6b5e31856359 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Tue, 29 Oct 2024 22:39:00 +0100 Subject: [PATCH 1/7] chore: update morpho-blue --- lib/morpho-blue | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/morpho-blue b/lib/morpho-blue index 731e3f7e..3de2df4e 160000 --- a/lib/morpho-blue +++ b/lib/morpho-blue @@ -1 +1 @@ -Subproject commit 731e3f7ed97cf15f8fe00b86e4be5365eb3802ac +Subproject commit 3de2df4eb94c3f6118963039d4f177839a228e2a From 0e4f7c9b7245255e07e2f30e017cff24ff57fde0 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Tue, 29 Oct 2024 22:51:36 +0100 Subject: [PATCH 2/7] chore: format .conf files --- certora/confs/ConsistentState.conf | 30 ++++++------ certora/confs/DistinctIdentifiers.conf | 32 ++++++------ certora/confs/Enabled.conf | 36 +++++++------- certora/confs/Immutability.conf | 30 ++++++------ certora/confs/LastUpdated.conf | 42 ++++++++-------- certora/confs/Liveness.conf | 46 ++++++++--------- certora/confs/MarketInteractions.conf | 40 +++++++-------- certora/confs/PendingValues.conf | 30 ++++++------ certora/confs/Range.conf | 34 ++++++------- certora/confs/Reentrancy.conf | 32 ++++++------ certora/confs/Reverts.conf | 62 +++++++++++------------ certora/confs/Roles.conf | 32 ++++++------ certora/confs/Timelock.conf | 44 ++++++++--------- certora/confs/Tokens.conf | 68 +++++++++++++------------- 14 files changed, 279 insertions(+), 279 deletions(-) diff --git a/certora/confs/ConsistentState.conf b/certora/confs/ConsistentState.conf index 4d064514..d4b3dbd1 100644 --- a/certora/confs/ConsistentState.conf +++ b/certora/confs/ConsistentState.conf @@ -1,17 +1,17 @@ { - "files": [ - "certora/helpers/MetaMorphoHarness.sol", - "certora/helpers/Util.sol", - ], - "solc": "solc-0.8.21", - "parametric_contracts": [ - "MetaMorphoHarness", - ], - "verify": "MetaMorphoHarness:certora/specs/ConsistentState.spec", - "loop_iter": "2", - "optimistic_loop": true, - "smt_timeout": "600", - "rule_sanity": "basic", - "server": "production", - "msg": "MetaMorpho Consistent State" + "files": [ + "certora/helpers/MetaMorphoHarness.sol", + "certora/helpers/Util.sol" + ], + "solc": "solc-0.8.21", + "parametric_contracts": [ + "MetaMorphoHarness" + ], + "verify": "MetaMorphoHarness:certora/specs/ConsistentState.spec", + "loop_iter": "2", + "optimistic_loop": true, + "smt_timeout": "600", + "rule_sanity": "basic", + "server": "production", + "msg": "MetaMorpho Consistent State" } diff --git a/certora/confs/DistinctIdentifiers.conf b/certora/confs/DistinctIdentifiers.conf index 59de60bc..38fc7516 100644 --- a/certora/confs/DistinctIdentifiers.conf +++ b/certora/confs/DistinctIdentifiers.conf @@ -1,18 +1,18 @@ { - "files": [ - "certora/helpers/MetaMorphoHarness.sol", - ], - "solc": "solc-0.8.21", - "verify": "MetaMorphoHarness:certora/specs/DistinctIdentifiers.spec", - "loop_iter": "2", - "optimistic_loop": true, - "prover_args": [ - "-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]", - "-depth 3", - "-mediumTimeout 20", - "-timeout 2000", - ], - "rule_sanity": "basic", - "server": "production", - "msg": "MetaMorpho Distinct Identifiers" + "files": [ + "certora/helpers/MetaMorphoHarness.sol" + ], + "solc": "solc-0.8.21", + "verify": "MetaMorphoHarness:certora/specs/DistinctIdentifiers.spec", + "loop_iter": "2", + "optimistic_loop": true, + "prover_args": [ + "-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]", + "-depth 3", + "-mediumTimeout 20", + "-timeout 2000" + ], + "rule_sanity": "basic", + "server": "production", + "msg": "MetaMorpho Distinct Identifiers" } diff --git a/certora/confs/Enabled.conf b/certora/confs/Enabled.conf index 703bacd5..15377686 100644 --- a/certora/confs/Enabled.conf +++ b/certora/confs/Enabled.conf @@ -1,20 +1,20 @@ { - "files": [ - "certora/helpers/MetaMorphoHarness.sol", - ], - "solc": "solc-0.8.21", - "verify": "MetaMorphoHarness:certora/specs/Enabled.spec", - "loop_iter": "2", - "optimistic_loop": true, - "prover_args": [ - "-solvers [z3:lia2,cvc5:nonlinNoDio,cvc4:nonlin,yices:def,z3:arith2]", - "-depth 3", - "-mediumTimeout 20", - "-timeout 1000", - "-smt_easy_LIA true", - ], - "smt_timeout": "7000", - "rule_sanity": "basic", - "server": "production", - "msg": "MetaMorpho Enabled" + "files": [ + "certora/helpers/MetaMorphoHarness.sol" + ], + "solc": "solc-0.8.21", + "verify": "MetaMorphoHarness:certora/specs/Enabled.spec", + "loop_iter": "2", + "optimistic_loop": true, + "prover_args": [ + "-solvers [z3:lia2,cvc5:nonlinNoDio,cvc4:nonlin,yices:def,z3:arith2]", + "-depth 3", + "-mediumTimeout 20", + "-timeout 1000", + "-smt_easy_LIA true" + ], + "smt_timeout": "7000", + "rule_sanity": "basic", + "server": "production", + "msg": "MetaMorpho Enabled" } diff --git a/certora/confs/Immutability.conf b/certora/confs/Immutability.conf index 2e3802f7..70c48632 100644 --- a/certora/confs/Immutability.conf +++ b/certora/confs/Immutability.conf @@ -1,17 +1,17 @@ { - "files": [ - "certora/helpers/MetaMorphoHarness.sol", - ], - "solc": "solc-0.8.21", - "verify": "MetaMorphoHarness:certora/specs/Immutability.spec", - "loop_iter": "2", - "optimistic_loop": true, - "prover_args": [ - "-depth 3", - "-mediumTimeout 20", - "-timeout 120", - ], - "rule_sanity": "basic", - "server": "production", - "msg": "MetaMorpho Immutability", + "files": [ + "certora/helpers/MetaMorphoHarness.sol" + ], + "solc": "solc-0.8.21", + "verify": "MetaMorphoHarness:certora/specs/Immutability.spec", + "loop_iter": "2", + "optimistic_loop": true, + "prover_args": [ + "-depth 3", + "-mediumTimeout 20", + "-timeout 120" + ], + "rule_sanity": "basic", + "server": "production", + "msg": "MetaMorpho Immutability" } diff --git a/certora/confs/LastUpdated.conf b/certora/confs/LastUpdated.conf index 81bc168c..4ddeca93 100644 --- a/certora/confs/LastUpdated.conf +++ b/certora/confs/LastUpdated.conf @@ -1,23 +1,23 @@ { - "files": [ - "lib/morpho-blue/certora/harness/MorphoHarness.sol", - "certora/helpers/MetaMorphoHarness.sol", - "certora/helpers/Util.sol", - ], - "solc_map": { - "MorphoHarness": "solc-0.8.19", - "MetaMorphoHarness": "solc-0.8.21", - "Util": "solc-0.8.21", - }, - "verify": "MetaMorphoHarness:certora/specs/LastUpdated.spec", - "loop_iter": "2", - "optimistic_loop": true, - "prover_args": [ - "-depth 3", - "-mediumTimeout 20", - "-timeout 300", - ], - "rule_sanity": "basic", - "server": "production", - "msg": "MetaMorpho Last Updated" + "files": [ + "lib/morpho-blue/certora/harness/MorphoHarness.sol", + "certora/helpers/MetaMorphoHarness.sol", + "certora/helpers/Util.sol" + ], + "solc_map": { + "MorphoHarness": "solc-0.8.19", + "MetaMorphoHarness": "solc-0.8.21", + "Util": "solc-0.8.21" + }, + "verify": "MetaMorphoHarness:certora/specs/LastUpdated.spec", + "loop_iter": "2", + "optimistic_loop": true, + "prover_args": [ + "-depth 3", + "-mediumTimeout 20", + "-timeout 300" + ], + "rule_sanity": "basic", + "server": "production", + "msg": "MetaMorpho Last Updated" } diff --git a/certora/confs/Liveness.conf b/certora/confs/Liveness.conf index f391344c..d4b4b83c 100644 --- a/certora/confs/Liveness.conf +++ b/certora/confs/Liveness.conf @@ -1,25 +1,25 @@ { - "files": [ - "lib/morpho-blue/certora/harness/MorphoHarness.sol", - "certora/helpers/MetaMorphoHarness.sol", - "certora/helpers/Util.sol", - ], - "link": [ - "MetaMorphoHarness:MORPHO=MorphoHarness", - ], - "solc_map": { - "MorphoHarness": "solc-0.8.19", - "MetaMorphoHarness": "solc-0.8.21", - "Util": "solc-0.8.21", - }, - "verify": "MetaMorphoHarness:certora/specs/Liveness.spec", - "loop_iter": "2", - "optimistic_loop": true, - "prover_args": [ - "-smt_easy_LIA true", - ], - "smt_timeout": "7000", - "rule_sanity": "basic", - "server": "production", - "msg": "MetaMorpho Liveness" + "files": [ + "lib/morpho-blue/certora/harness/MorphoHarness.sol", + "certora/helpers/MetaMorphoHarness.sol", + "certora/helpers/Util.sol" + ], + "link": [ + "MetaMorphoHarness:MORPHO=MorphoHarness" + ], + "solc_map": { + "MorphoHarness": "solc-0.8.19", + "MetaMorphoHarness": "solc-0.8.21", + "Util": "solc-0.8.21" + }, + "verify": "MetaMorphoHarness:certora/specs/Liveness.spec", + "loop_iter": "2", + "optimistic_loop": true, + "prover_args": [ + "-smt_easy_LIA true" + ], + "smt_timeout": "7000", + "rule_sanity": "basic", + "server": "production", + "msg": "MetaMorpho Liveness" } diff --git a/certora/confs/MarketInteractions.conf b/certora/confs/MarketInteractions.conf index f38dbb84..460fb93f 100644 --- a/certora/confs/MarketInteractions.conf +++ b/certora/confs/MarketInteractions.conf @@ -1,22 +1,22 @@ { - "files": [ - "certora/helpers/MetaMorphoHarness.sol", - "certora/helpers/Util.sol", - ], - "solc": "solc-0.8.21", - "parametric_contracts": [ - "MetaMorphoHarness", - ], - "verify": "MetaMorphoHarness:certora/specs/MarketInteractions.spec", - "loop_iter": "2", - "optimistic_loop": true, - "prover_args": [ - "-depth 3", - "-mediumTimeout 20", - "-timeout 120", - "-smt_nonLinearArithmetic false", - ], - "rule_sanity": "basic", - "server": "production", - "msg": "MetaMorpho Market Interactions" + "files": [ + "certora/helpers/MetaMorphoHarness.sol", + "certora/helpers/Util.sol" + ], + "solc": "solc-0.8.21", + "parametric_contracts": [ + "MetaMorphoHarness" + ], + "verify": "MetaMorphoHarness:certora/specs/MarketInteractions.spec", + "loop_iter": "2", + "optimistic_loop": true, + "prover_args": [ + "-depth 3", + "-mediumTimeout 20", + "-timeout 120", + "-smt_nonLinearArithmetic false" + ], + "rule_sanity": "basic", + "server": "production", + "msg": "MetaMorpho Market Interactions" } diff --git a/certora/confs/PendingValues.conf b/certora/confs/PendingValues.conf index 7db7a5e8..e608ff22 100644 --- a/certora/confs/PendingValues.conf +++ b/certora/confs/PendingValues.conf @@ -1,17 +1,17 @@ { - "files": [ - "certora/helpers/MetaMorphoHarness.sol", - ], - "solc": "solc-0.8.21", - "verify": "MetaMorphoHarness:certora/specs/PendingValues.spec", - "loop_iter": "2", - "optimistic_loop": true, - "prover_args": [ - "-depth 3", - "-mediumTimeout 20", - "-timeout 3600", - ], - "rule_sanity": "basic", - "server": "production", - "msg": "MetaMorpho Pending Values" + "files": [ + "certora/helpers/MetaMorphoHarness.sol" + ], + "solc": "solc-0.8.21", + "verify": "MetaMorphoHarness:certora/specs/PendingValues.spec", + "loop_iter": "2", + "optimistic_loop": true, + "prover_args": [ + "-depth 3", + "-mediumTimeout 20", + "-timeout 3600" + ], + "rule_sanity": "basic", + "server": "production", + "msg": "MetaMorpho Pending Values" } diff --git a/certora/confs/Range.conf b/certora/confs/Range.conf index 13b869d3..045025a1 100644 --- a/certora/confs/Range.conf +++ b/certora/confs/Range.conf @@ -1,19 +1,19 @@ { - "files": [ - "certora/helpers/MetaMorphoHarness.sol", - ], - "solc": "solc-0.8.21", - "verify": "MetaMorphoHarness:certora/specs/Range.spec", - "loop_iter": "2", - "optimistic_loop": true, - "prover_args": [ - "-depth 0", - "-timeout 300", - "-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:def{randomSeed=8},z3:def{randomSeed=9},z3:def{randomSeed=10}]", - ], - "rule_sanity": "basic", - "server": "production", - "msg": "MetaMorpho Range" + "files": [ + "certora/helpers/MetaMorphoHarness.sol" + ], + "solc": "solc-0.8.21", + "verify": "MetaMorphoHarness:certora/specs/Range.spec", + "loop_iter": "2", + "optimistic_loop": true, + "prover_args": [ + "-depth 0", + "-timeout 300", + "-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:def{randomSeed=8},z3:def{randomSeed=9},z3:def{randomSeed=10}]" + ], + "rule_sanity": "basic", + "server": "production", + "msg": "MetaMorpho Range" } diff --git a/certora/confs/Reentrancy.conf b/certora/confs/Reentrancy.conf index 2c078aef..c9dd0692 100644 --- a/certora/confs/Reentrancy.conf +++ b/certora/confs/Reentrancy.conf @@ -1,18 +1,18 @@ { - "files": [ - "certora/helpers/MetaMorphoHarness.sol", - ], - "solc": "solc-0.8.21", - "verify": "MetaMorphoHarness:certora/specs/Reentrancy.spec", - "loop_iter": "2", - "optimistic_loop": true, - "prover_args": [ - "-depth 3", - "-mediumTimeout 20", - "-timeout 120", - "-enableStorageSplitting false", - ], - "rule_sanity": "basic", - "server": "production", - "msg": "MetaMorpho Reentrancy", + "files": [ + "certora/helpers/MetaMorphoHarness.sol" + ], + "solc": "solc-0.8.21", + "verify": "MetaMorphoHarness:certora/specs/Reentrancy.spec", + "loop_iter": "2", + "optimistic_loop": true, + "prover_args": [ + "-depth 3", + "-mediumTimeout 20", + "-timeout 120", + "-enableStorageSplitting false" + ], + "rule_sanity": "basic", + "server": "production", + "msg": "MetaMorpho Reentrancy" } diff --git a/certora/confs/Reverts.conf b/certora/confs/Reverts.conf index 0960539b..bdb8b08b 100644 --- a/certora/confs/Reverts.conf +++ b/certora/confs/Reverts.conf @@ -1,33 +1,33 @@ { - "files": [ - "lib/morpho-blue/certora/harness/MorphoHarness.sol", - "certora/helpers/MetaMorphoHarness.sol", - "certora/helpers/Util.sol", - "certora/dispatch/ERC20Standard.sol", - ], - "link": [ - "MetaMorphoHarness:MORPHO=MorphoHarness", - ], - "solc_map": { - "MorphoHarness": "solc-0.8.19", - "MetaMorphoHarness": "solc-0.8.21", - "Util": "solc-0.8.21", - "ERC20Standard": "solc-0.8.21", - }, - "verify": "MetaMorphoHarness:certora/specs/Reverts.spec", - "loop_iter": "2", - "optimistic_loop": true, - "prover_args": [ - "-depth 5", - "-mediumTimeout 40", - "-splitParallel true", - "-splitParallelInitialDepth 4", - "-splitParallelTimelimit 7000", - "-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:def{randomSeed=8},z3:def{randomSeed=9},z3:def{randomSeed=10}]" - ], - "rule_sanity": "basic", - "server": "production", - "msg": "MetaMorpho Reverts", + "files": [ + "lib/morpho-blue/certora/harness/MorphoHarness.sol", + "certora/helpers/MetaMorphoHarness.sol", + "certora/helpers/Util.sol", + "certora/dispatch/ERC20Standard.sol" + ], + "link": [ + "MetaMorphoHarness:MORPHO=MorphoHarness" + ], + "solc_map": { + "MorphoHarness": "solc-0.8.19", + "MetaMorphoHarness": "solc-0.8.21", + "Util": "solc-0.8.21", + "ERC20Standard": "solc-0.8.21" + }, + "verify": "MetaMorphoHarness:certora/specs/Reverts.spec", + "loop_iter": "2", + "optimistic_loop": true, + "prover_args": [ + "-depth 5", + "-mediumTimeout 40", + "-splitParallel true", + "-splitParallelInitialDepth 4", + "-splitParallelTimelimit 7000", + "-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:def{randomSeed=8},z3:def{randomSeed=9},z3:def{randomSeed=10}]" + ], + "rule_sanity": "basic", + "server": "production", + "msg": "MetaMorpho Reverts" } diff --git a/certora/confs/Roles.conf b/certora/confs/Roles.conf index 0db5cb2d..cc71f1da 100644 --- a/certora/confs/Roles.conf +++ b/certora/confs/Roles.conf @@ -1,18 +1,18 @@ { - "files": [ - "certora/helpers/MetaMorphoHarness.sol", - ], - "solc": "solc-0.8.21", - "verify": "MetaMorphoHarness:certora/specs/Roles.spec", - "loop_iter": "2", - "optimistic_loop": true, - "prover_args": [ - "-depth 3", - "-mediumTimeout 20", - "-timeout 120", - "-superOptimisticReturnsize true", - ], - "rule_sanity": "basic", - "server": "production", - "msg": "MetaMorpho Roles", + "files": [ + "certora/helpers/MetaMorphoHarness.sol" + ], + "solc": "solc-0.8.21", + "verify": "MetaMorphoHarness:certora/specs/Roles.spec", + "loop_iter": "2", + "optimistic_loop": true, + "prover_args": [ + "-depth 3", + "-mediumTimeout 20", + "-timeout 120", + "-superOptimisticReturnsize true" + ], + "rule_sanity": "basic", + "server": "production", + "msg": "MetaMorpho Roles" } diff --git a/certora/confs/Timelock.conf b/certora/confs/Timelock.conf index e80470a5..1829751d 100644 --- a/certora/confs/Timelock.conf +++ b/certora/confs/Timelock.conf @@ -1,24 +1,24 @@ { - "files": [ - "lib/morpho-blue/certora/harness/MorphoHarness.sol", - "certora/helpers/MetaMorphoHarness.sol", - ], - "parametric_contracts": [ - "MetaMorphoHarness", - ], - "solc_map": { - "MorphoHarness": "solc-0.8.19", - "MetaMorphoHarness": "solc-0.8.21", - }, - "verify": "MetaMorphoHarness:certora/specs/Timelock.spec", - "loop_iter": "2", - "optimistic_loop": true, - "prover_args": [ - "-depth 3", - "-mediumTimeout 20", - "-timeout 3600", - ], - "rule_sanity": "basic", - "server": "production", - "msg": "MetaMorpho Timelock" + "files": [ + "lib/morpho-blue/certora/harness/MorphoHarness.sol", + "certora/helpers/MetaMorphoHarness.sol" + ], + "parametric_contracts": [ + "MetaMorphoHarness" + ], + "solc_map": { + "MorphoHarness": "solc-0.8.19", + "MetaMorphoHarness": "solc-0.8.21" + }, + "verify": "MetaMorphoHarness:certora/specs/Timelock.spec", + "loop_iter": "2", + "optimistic_loop": true, + "prover_args": [ + "-depth 3", + "-mediumTimeout 20", + "-timeout 3600" + ], + "rule_sanity": "basic", + "server": "production", + "msg": "MetaMorpho Timelock" } diff --git a/certora/confs/Tokens.conf b/certora/confs/Tokens.conf index e533c66b..e07d02bd 100644 --- a/certora/confs/Tokens.conf +++ b/certora/confs/Tokens.conf @@ -1,36 +1,36 @@ { - "files": [ - "lib/morpho-blue/certora/harness/MorphoHarness.sol", - "certora/helpers/MetaMorphoHarness.sol", - "certora/helpers/Util.sol", - "certora/dispatch/ERC20NoRevert.sol", - "certora/dispatch/ERC20Standard.sol", - "certora/dispatch/ERC20USDT.sol", - ], - "link": [ - "MetaMorphoHarness:MORPHO=MorphoHarness", - ], - "solc_map": { - "MorphoHarness": "solc-0.8.19", - "MetaMorphoHarness": "solc-0.8.21", - "Util": "solc-0.8.21", - "ERC20NoRevert": "solc-0.8.21", - "ERC20Standard": "solc-0.8.21", - "ERC20USDT": "solc-0.8.21", - }, - "verify": "MetaMorphoHarness:certora/specs/Tokens.spec", - "loop_iter": "2", - "optimistic_loop": true, - "prover_args": [ - "-depth 3", - "-mediumTimeout 20", - "-timeout 3600", - "-adaptiveSolverConfig false", - "-smt_nonLinearArithmetic false", - "-smt_hashingScheme plaininjectivity", - "-smt_easy_LIA true", - ], - "rule_sanity": "basic", - "server": "production", - "msg": "MetaMorpho Tokens", + "files": [ + "lib/morpho-blue/certora/harness/MorphoHarness.sol", + "certora/helpers/MetaMorphoHarness.sol", + "certora/helpers/Util.sol", + "certora/dispatch/ERC20NoRevert.sol", + "certora/dispatch/ERC20Standard.sol", + "certora/dispatch/ERC20USDT.sol" + ], + "link": [ + "MetaMorphoHarness:MORPHO=MorphoHarness" + ], + "solc_map": { + "MorphoHarness": "solc-0.8.19", + "MetaMorphoHarness": "solc-0.8.21", + "Util": "solc-0.8.21", + "ERC20NoRevert": "solc-0.8.21", + "ERC20Standard": "solc-0.8.21", + "ERC20USDT": "solc-0.8.21" + }, + "verify": "MetaMorphoHarness:certora/specs/Tokens.spec", + "loop_iter": "2", + "optimistic_loop": true, + "prover_args": [ + "-depth 3", + "-mediumTimeout 20", + "-timeout 3600", + "-adaptiveSolverConfig false", + "-smt_nonLinearArithmetic false", + "-smt_hashingScheme plaininjectivity", + "-smt_easy_LIA true" + ], + "rule_sanity": "basic", + "server": "production", + "msg": "MetaMorpho Tokens" } From f65c4f45e3f268000b84915fcaa22e49dc1d4284 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Tue, 29 Oct 2024 22:52:20 +0100 Subject: [PATCH 3/7] refactor: remove Morpho Util from Util --- certora/helpers/Util.sol | 16 +--------------- 1 file changed, 1 insertion(+), 15 deletions(-) diff --git a/certora/helpers/Util.sol b/certora/helpers/Util.sol index b38f9e03..e713bd38 100644 --- a/certora/helpers/Util.sol +++ b/certora/helpers/Util.sol @@ -1,21 +1,11 @@ // SPDX-License-Identifier: GPL-2.0-or-later pragma solidity 0.8.21; -import { - MarketParams, - MarketParamsLib, - IERC20, - SafeERC20, - IMorphoHarness, - SharesMathLib, - Id, - Market -} from "../munged/MetaMorpho.sol"; +import {IERC20, SafeERC20, IMorphoHarness, SharesMathLib, Id, Market} from "../munged/MetaMorpho.sol"; contract Util { using SafeERC20 for IERC20; using SharesMathLib for uint256; - using MarketParamsLib for MarketParams; function balanceOf(address token, address user) external view returns (uint256) { return IERC20(token).balanceOf(user); @@ -41,8 +31,4 @@ contract Util { return shares.toAssetsDown(market.totalSupplyAssets, market.totalSupplyShares); } } - - function libId(MarketParams memory marketParams) external pure returns (Id) { - return marketParams.id(); - } } From d24bf5ef9c5cd5427304565bce3faa71397daad8 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Tue, 29 Oct 2024 23:16:54 +0100 Subject: [PATCH 4/7] refactor: use Morpho Util, and rename Util to ERC20Helper --- certora/confs/ConsistentState.conf | 9 ++-- certora/confs/LastUpdated.conf | 6 ++- certora/confs/Liveness.conf | 6 ++- certora/confs/Reverts.conf | 6 ++- certora/confs/Tokens.conf | 6 ++- certora/helpers/{Util.sol => ERC20Helper.sol} | 2 +- certora/specs/ConsistentState.spec | 4 -- certora/specs/LastUpdated.spec | 6 +++ certora/specs/Reverts.spec | 2 +- certora/specs/Tokens.spec | 42 +++++++++---------- 10 files changed, 51 insertions(+), 38 deletions(-) rename certora/helpers/{Util.sol => ERC20Helper.sol} (97%) diff --git a/certora/confs/ConsistentState.conf b/certora/confs/ConsistentState.conf index d4b3dbd1..76b62919 100644 --- a/certora/confs/ConsistentState.conf +++ b/certora/confs/ConsistentState.conf @@ -1,9 +1,12 @@ { "files": [ - "certora/helpers/MetaMorphoHarness.sol", - "certora/helpers/Util.sol" + "lib/morpho-blue/certora/harness/Util.sol", + "certora/helpers/MetaMorphoHarness.sol" ], - "solc": "solc-0.8.21", + "solc_map": { + "Util": "solc-0.8.19", + "MetaMorphoHarness": "solc-0.8.21" + }, "parametric_contracts": [ "MetaMorphoHarness" ], diff --git a/certora/confs/LastUpdated.conf b/certora/confs/LastUpdated.conf index 4ddeca93..3f2a6d72 100644 --- a/certora/confs/LastUpdated.conf +++ b/certora/confs/LastUpdated.conf @@ -1,13 +1,15 @@ { "files": [ "lib/morpho-blue/certora/harness/MorphoHarness.sol", + "lib/morpho-blue/certora/harness/Util.sol", "certora/helpers/MetaMorphoHarness.sol", - "certora/helpers/Util.sol" + "certora/helpers/ERC20Helper.sol" ], "solc_map": { "MorphoHarness": "solc-0.8.19", + "Util": "solc-0.8.19", "MetaMorphoHarness": "solc-0.8.21", - "Util": "solc-0.8.21" + "ERC20Helper": "solc-0.8.21" }, "verify": "MetaMorphoHarness:certora/specs/LastUpdated.spec", "loop_iter": "2", diff --git a/certora/confs/Liveness.conf b/certora/confs/Liveness.conf index d4b4b83c..8ac74f10 100644 --- a/certora/confs/Liveness.conf +++ b/certora/confs/Liveness.conf @@ -1,16 +1,18 @@ { "files": [ "lib/morpho-blue/certora/harness/MorphoHarness.sol", + "lib/morpho-blue/certora/harness/Util.sol", "certora/helpers/MetaMorphoHarness.sol", - "certora/helpers/Util.sol" + "certora/helpers/ERC20Helper.sol" ], "link": [ "MetaMorphoHarness:MORPHO=MorphoHarness" ], "solc_map": { "MorphoHarness": "solc-0.8.19", + "Util": "solc-0.8.19", "MetaMorphoHarness": "solc-0.8.21", - "Util": "solc-0.8.21" + "ERC20Helper": "solc-0.8.21" }, "verify": "MetaMorphoHarness:certora/specs/Liveness.spec", "loop_iter": "2", diff --git a/certora/confs/Reverts.conf b/certora/confs/Reverts.conf index bdb8b08b..7d5fb42c 100644 --- a/certora/confs/Reverts.conf +++ b/certora/confs/Reverts.conf @@ -1,8 +1,9 @@ { "files": [ "lib/morpho-blue/certora/harness/MorphoHarness.sol", + "lib/morpho-blue/certora/harness/Util.sol", "certora/helpers/MetaMorphoHarness.sol", - "certora/helpers/Util.sol", + "certora/helpers/ERC20Helper.sol", "certora/dispatch/ERC20Standard.sol" ], "link": [ @@ -10,8 +11,9 @@ ], "solc_map": { "MorphoHarness": "solc-0.8.19", + "Util": "solc-0.8.19", "MetaMorphoHarness": "solc-0.8.21", - "Util": "solc-0.8.21", + "ERC20Helper": "solc-0.8.21", "ERC20Standard": "solc-0.8.21" }, "verify": "MetaMorphoHarness:certora/specs/Reverts.spec", diff --git a/certora/confs/Tokens.conf b/certora/confs/Tokens.conf index e07d02bd..8e493039 100644 --- a/certora/confs/Tokens.conf +++ b/certora/confs/Tokens.conf @@ -1,8 +1,9 @@ { "files": [ "lib/morpho-blue/certora/harness/MorphoHarness.sol", + "lib/morpho-blue/certora/harness/Util.sol", "certora/helpers/MetaMorphoHarness.sol", - "certora/helpers/Util.sol", + "certora/helpers/ERC20Helper.sol", "certora/dispatch/ERC20NoRevert.sol", "certora/dispatch/ERC20Standard.sol", "certora/dispatch/ERC20USDT.sol" @@ -12,8 +13,9 @@ ], "solc_map": { "MorphoHarness": "solc-0.8.19", + "Util": "solc-0.8.19", "MetaMorphoHarness": "solc-0.8.21", - "Util": "solc-0.8.21", + "ERC20Helper": "solc-0.8.21", "ERC20NoRevert": "solc-0.8.21", "ERC20Standard": "solc-0.8.21", "ERC20USDT": "solc-0.8.21" diff --git a/certora/helpers/Util.sol b/certora/helpers/ERC20Helper.sol similarity index 97% rename from certora/helpers/Util.sol rename to certora/helpers/ERC20Helper.sol index e713bd38..71f37dcf 100644 --- a/certora/helpers/Util.sol +++ b/certora/helpers/ERC20Helper.sol @@ -3,7 +3,7 @@ pragma solidity 0.8.21; import {IERC20, SafeERC20, IMorphoHarness, SharesMathLib, Id, Market} from "../munged/MetaMorpho.sol"; -contract Util { +contract ERC20Helper { using SafeERC20 for IERC20; using SharesMathLib for uint256; diff --git a/certora/specs/ConsistentState.spec b/certora/specs/ConsistentState.spec index fd2a7c15..6b58695b 100644 --- a/certora/specs/ConsistentState.spec +++ b/certora/specs/ConsistentState.spec @@ -5,10 +5,6 @@ using Util as Util; methods { function Util.libId(MetaMorphoHarness.MarketParams) external returns(MetaMorphoHarness.Id) envfree; - function Util.balanceOf(address, address) external returns(uint256) envfree; - function Util.totalSupply(address) external returns(uint256) envfree; - function Util.safeTransferFrom(address, address, address, uint256) external envfree; - function Util.withdrawnAssets(address, MetaMorphoHarness.Id, uint256, uint256) external returns (uint256) envfree; } // Check that the fee cannot accrue to an unset fee recipient. diff --git a/certora/specs/LastUpdated.spec b/certora/specs/LastUpdated.spec index 8e36b3b9..93b43bfa 100644 --- a/certora/specs/LastUpdated.spec +++ b/certora/specs/LastUpdated.spec @@ -2,8 +2,14 @@ import "ConsistentState.spec"; using MorphoHarness as Morpho; +using ERC20Helper as ERC20; methods { + function ERC20.balanceOf(address, address) external returns(uint256) envfree; + function ERC20.totalSupply(address) external returns(uint256) envfree; + function ERC20.safeTransferFrom(address, address, address, uint256) external envfree; + function ERC20.withdrawnAssets(address, MetaMorphoHarness.Id, uint256, uint256) external returns (uint256) envfree; + function Morpho.lastUpdate(MorphoHarness.Id) external returns(uint256) envfree; } diff --git a/certora/specs/Reverts.spec b/certora/specs/Reverts.spec index b8e66951..a95c1719 100644 --- a/certora/specs/Reverts.spec +++ b/certora/specs/Reverts.spec @@ -290,7 +290,7 @@ rule acceptCapInputValidation(env e, MetaMorphoHarness.MarketParams marketParams rule skimRevertCondition(env e, address token) { address skimRecipient = skimRecipient(); - require skimRecipient != currentContract => Util.balanceOf(token, skimRecipient) + Util.balanceOf(token, currentContract) <= to_mathint(Util.totalSupply(token)); + require skimRecipient != currentContract => ERC20.balanceOf(token, skimRecipient) + ERC20.balanceOf(token, currentContract) <= to_mathint(ERC20.totalSupply(token)); skim@withrevert(e, token); diff --git a/certora/specs/Tokens.spec b/certora/specs/Tokens.spec index 0c4eca41..ef51f68e 100644 --- a/certora/specs/Tokens.spec +++ b/certora/specs/Tokens.spec @@ -35,7 +35,7 @@ function summarySupply(MetaMorphoHarness.MarketParams marketParams, uint256 asse requireInvariant enabledHasConsistentAsset(marketParams); // Summarize supply as just a transfer for the purpose of this specification file, which is sound because only the properties about tokens are verified in this file. - Util.safeTransferFrom(marketParams.loanToken, currentContract, MORPHO(), assets); + ERC20.safeTransferFrom(marketParams.loanToken, currentContract, MORPHO(), assets); return (assets, shares); } @@ -51,9 +51,9 @@ function summaryWithdraw(MetaMorphoHarness.MarketParams marketParams, uint256 as requireInvariant enabledHasConsistentAsset(marketParams); // Use effective withdrawn assets if shares are given as input. - uint256 withdrawn = Util.withdrawnAssets(MORPHO(), id, assets, shares); + uint256 withdrawn = ERC20.withdrawnAssets(MORPHO(), id, assets, shares); // Summarize withdraw as just a transfer for the purpose of this specification file, which is sound because only the properties about tokens are verified in this file. - Util.safeTransferFrom(marketParams.loanToken, MORPHO(), currentContract, withdrawn); + ERC20.safeTransferFrom(marketParams.loanToken, MORPHO(), currentContract, withdrawn); return (withdrawn, shares); } @@ -69,13 +69,13 @@ rule depositTokenChange(env e, uint256 assets, address receiver) { require currentContract == 0x12; require e.msg.sender == 0x13; - uint256 balanceMorphoBefore = Util.balanceOf(asset, morpho); - uint256 balanceMetaMorphoBefore = Util.balanceOf(asset, currentContract); - uint256 balanceSenderBefore = Util.balanceOf(asset, e.msg.sender); + uint256 balanceMorphoBefore = ERC20.balanceOf(asset, morpho); + uint256 balanceMetaMorphoBefore = ERC20.balanceOf(asset, currentContract); + uint256 balanceSenderBefore = ERC20.balanceOf(asset, e.msg.sender); deposit(e, assets, receiver); - uint256 balanceMorphoAfter = Util.balanceOf(asset, morpho); - uint256 balanceMetaMorphoAfter = Util.balanceOf(asset, currentContract); - uint256 balanceSenderAfter = Util.balanceOf(asset, e.msg.sender); + uint256 balanceMorphoAfter = ERC20.balanceOf(asset, morpho); + uint256 balanceMetaMorphoAfter = ERC20.balanceOf(asset, currentContract); + uint256 balanceSenderAfter = ERC20.balanceOf(asset, e.msg.sender); assert assert_uint256(balanceMorphoAfter - balanceMorphoBefore) == assets; assert balanceMetaMorphoAfter == balanceMetaMorphoBefore; @@ -93,13 +93,13 @@ rule withdrawTokenChange(env e, uint256 assets, address receiver, address owner) require currentContract == 0x12; require receiver == 0x13; - uint256 balanceMorphoBefore = Util.balanceOf(asset, morpho); - uint256 balanceMetaMorphoBefore = Util.balanceOf(asset, currentContract); - uint256 balanceReceiverBefore = Util.balanceOf(asset, receiver); + uint256 balanceMorphoBefore = ERC20.balanceOf(asset, morpho); + uint256 balanceMetaMorphoBefore = ERC20.balanceOf(asset, currentContract); + uint256 balanceReceiverBefore = ERC20.balanceOf(asset, receiver); withdraw(e, assets, receiver, owner); - uint256 balanceMorphoAfter = Util.balanceOf(asset, morpho); - uint256 balanceMetaMorphoAfter = Util.balanceOf(asset, currentContract); - uint256 balanceReceiverAfter = Util.balanceOf(asset, receiver); + uint256 balanceMorphoAfter = ERC20.balanceOf(asset, morpho); + uint256 balanceMetaMorphoAfter = ERC20.balanceOf(asset, currentContract); + uint256 balanceReceiverAfter = ERC20.balanceOf(asset, receiver); assert assert_uint256(balanceMorphoBefore - balanceMorphoAfter) == assets; assert balanceMetaMorphoAfter == balanceMetaMorphoBefore; @@ -116,13 +116,13 @@ rule reallocateTokenChange(env e, MetaMorphoHarness.MarketAllocation[] allocatio require asset == 0x11; require currentContract == 0x12; - uint256 balanceMorphoBefore = Util.balanceOf(asset, morpho); - uint256 balanceMetaMorphoBefore = Util.balanceOf(asset, currentContract); - uint256 balanceSenderBefore = Util.balanceOf(asset, e.msg.sender); + uint256 balanceMorphoBefore = ERC20.balanceOf(asset, morpho); + uint256 balanceMetaMorphoBefore = ERC20.balanceOf(asset, currentContract); + uint256 balanceSenderBefore = ERC20.balanceOf(asset, e.msg.sender); reallocate(e, allocations); - uint256 balanceMorphoAfter = Util.balanceOf(asset, morpho); - uint256 balanceMetaMorphoAfter = Util.balanceOf(asset, currentContract); - uint256 balanceSenderAfter = Util.balanceOf(asset, e.msg.sender); + uint256 balanceMorphoAfter = ERC20.balanceOf(asset, morpho); + uint256 balanceMetaMorphoAfter = ERC20.balanceOf(asset, currentContract); + uint256 balanceSenderAfter = ERC20.balanceOf(asset, e.msg.sender); assert balanceMorphoAfter == balanceMorphoAfter; assert balanceMetaMorphoAfter == balanceMetaMorphoBefore; From c3b2c3a4a468b5c77bb154188bac0732aaf8b3ff Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Tue, 29 Oct 2024 23:21:01 +0100 Subject: [PATCH 5/7] fix: use Morpho Util in MarketInteractions --- certora/confs/MarketInteractions.conf | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/certora/confs/MarketInteractions.conf b/certora/confs/MarketInteractions.conf index 460fb93f..44e68878 100644 --- a/certora/confs/MarketInteractions.conf +++ b/certora/confs/MarketInteractions.conf @@ -1,9 +1,12 @@ { "files": [ - "certora/helpers/MetaMorphoHarness.sol", - "certora/helpers/Util.sol" + "lib/morpho-blue/certora/harness/Util.sol", + "certora/helpers/MetaMorphoHarness.sol" ], - "solc": "solc-0.8.21", + "solc_map": { + "Util": "solc-0.8.19", + "MetaMorphoHarness": "solc-0.8.21" + }, "parametric_contracts": [ "MetaMorphoHarness" ], From fb02d6975e549834f8bcc71cfe98a7d4d695a854 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Tue, 29 Oct 2024 23:58:14 +0100 Subject: [PATCH 6/7] refactor: remove withdrawnAssets from ERC20Helper --- certora/helpers/ERC20Helper.sol | 16 +--------------- certora/specs/ConsistentState.spec | 1 + certora/specs/LastUpdated.spec | 3 ++- certora/specs/Tokens.spec | 9 ++++++++- 4 files changed, 12 insertions(+), 17 deletions(-) diff --git a/certora/helpers/ERC20Helper.sol b/certora/helpers/ERC20Helper.sol index 71f37dcf..e92a243c 100644 --- a/certora/helpers/ERC20Helper.sol +++ b/certora/helpers/ERC20Helper.sol @@ -1,11 +1,10 @@ // SPDX-License-Identifier: GPL-2.0-or-later pragma solidity 0.8.21; -import {IERC20, SafeERC20, IMorphoHarness, SharesMathLib, Id, Market} from "../munged/MetaMorpho.sol"; +import {IERC20, SafeERC20} from "../munged/MetaMorpho.sol"; contract ERC20Helper { using SafeERC20 for IERC20; - using SharesMathLib for uint256; function balanceOf(address token, address user) external view returns (uint256) { return IERC20(token).balanceOf(user); @@ -18,17 +17,4 @@ contract ERC20Helper { function safeTransferFrom(address token, address from, address to, uint256 amount) external { IERC20(token).safeTransferFrom(from, to, amount); } - - function withdrawnAssets(IMorphoHarness morpho, Id id, uint256 assets, uint256 shares) - external - view - returns (uint256) - { - if (shares == 0) { - return assets; - } else { - Market memory market = morpho.market(id); - return shares.toAssetsDown(market.totalSupplyAssets, market.totalSupplyShares); - } - } } diff --git a/certora/specs/ConsistentState.spec b/certora/specs/ConsistentState.spec index 6b58695b..0fb4d71a 100644 --- a/certora/specs/ConsistentState.spec +++ b/certora/specs/ConsistentState.spec @@ -5,6 +5,7 @@ using Util as Util; methods { function Util.libId(MetaMorphoHarness.MarketParams) external returns(MetaMorphoHarness.Id) envfree; + function Util.libMulDivDown(uint256, uint256, uint256) external returns(uint256) envfree; } // Check that the fee cannot accrue to an unset fee recipient. diff --git a/certora/specs/LastUpdated.spec b/certora/specs/LastUpdated.spec index 93b43bfa..74a751e0 100644 --- a/certora/specs/LastUpdated.spec +++ b/certora/specs/LastUpdated.spec @@ -8,9 +8,10 @@ methods { function ERC20.balanceOf(address, address) external returns(uint256) envfree; function ERC20.totalSupply(address) external returns(uint256) envfree; function ERC20.safeTransferFrom(address, address, address, uint256) external envfree; - function ERC20.withdrawnAssets(address, MetaMorphoHarness.Id, uint256, uint256) external returns (uint256) envfree; function Morpho.lastUpdate(MorphoHarness.Id) external returns(uint256) envfree; + function Morpho.virtualTotalSupplyAssets(MorphoHarness.Id) external returns(uint256) envfree; + function Morpho.virtualTotalSupplyShares(MorphoHarness.Id) external returns(uint256) envfree; } function hasCuratorRole(address user) returns bool { diff --git a/certora/specs/Tokens.spec b/certora/specs/Tokens.spec index ef51f68e..d67be838 100644 --- a/certora/specs/Tokens.spec +++ b/certora/specs/Tokens.spec @@ -51,7 +51,14 @@ function summaryWithdraw(MetaMorphoHarness.MarketParams marketParams, uint256 as requireInvariant enabledHasConsistentAsset(marketParams); // Use effective withdrawn assets if shares are given as input. - uint256 withdrawn = ERC20.withdrawnAssets(MORPHO(), id, assets, shares); + uint256 withdrawn; + if (shares == 0) { + require withdrawn == assets; + } else { + uint256 totalAssets = Morpho.virtualTotalSupplyAssets(id); + uint256 totalShares = Morpho.virtualTotalSupplyShares(id); + require withdrawn == Util.libMulDivDown(shares, totalAssets, totalShares); + } // Summarize withdraw as just a transfer for the purpose of this specification file, which is sound because only the properties about tokens are verified in this file. ERC20.safeTransferFrom(marketParams.loanToken, MORPHO(), currentContract, withdrawn); From ba0f4919b8ed5535f82e0aac3e4ef6a43ad51b7f Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Wed, 6 Nov 2024 17:57:21 +0100 Subject: [PATCH 7/7] fix: timeout in Liveness --- certora/confs/Enabled.conf | 3 +-- certora/confs/Liveness.conf | 2 +- certora/confs/Tokens.conf | 3 +-- 3 files changed, 3 insertions(+), 5 deletions(-) diff --git a/certora/confs/Enabled.conf b/certora/confs/Enabled.conf index 15377686..2f69fd3a 100644 --- a/certora/confs/Enabled.conf +++ b/certora/confs/Enabled.conf @@ -10,8 +10,7 @@ "-solvers [z3:lia2,cvc5:nonlinNoDio,cvc4:nonlin,yices:def,z3:arith2]", "-depth 3", "-mediumTimeout 20", - "-timeout 1000", - "-smt_easy_LIA true" + "-timeout 1000" ], "smt_timeout": "7000", "rule_sanity": "basic", diff --git a/certora/confs/Liveness.conf b/certora/confs/Liveness.conf index 8ac74f10..3acab47b 100644 --- a/certora/confs/Liveness.conf +++ b/certora/confs/Liveness.conf @@ -18,7 +18,7 @@ "loop_iter": "2", "optimistic_loop": true, "prover_args": [ - "-smt_easy_LIA true" + "-depth 0" ], "smt_timeout": "7000", "rule_sanity": "basic", diff --git a/certora/confs/Tokens.conf b/certora/confs/Tokens.conf index 8e493039..403d8d5b 100644 --- a/certora/confs/Tokens.conf +++ b/certora/confs/Tokens.conf @@ -29,8 +29,7 @@ "-timeout 3600", "-adaptiveSolverConfig false", "-smt_nonLinearArithmetic false", - "-smt_hashingScheme plaininjectivity", - "-smt_easy_LIA true" + "-smt_hashingScheme plaininjectivity" ], "rule_sanity": "basic", "server": "production",