-
Notifications
You must be signed in to change notification settings - Fork 26
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #430 from morpho-org/certora/update-morpho-blue
[Certora] Update morpho-blue
- Loading branch information
Showing
21 changed files
with
349 additions
and
354 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,17 +1,20 @@ | ||
| { | ||
| "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": [ | ||
| "lib/morpho-blue/certora/harness/Util.sol", | ||
| "certora/helpers/MetaMorphoHarness.sol" | ||
| ], | ||
| "solc_map": { | ||
| "Util": "solc-0.8.19", | ||
| "MetaMorphoHarness": "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" | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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" | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,20 +1,19 @@ | ||
| { | ||
| "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_timeout": "7000", | ||
| "rule_sanity": "basic", | ||
| "server": "production", | ||
| "msg": "MetaMorpho Enabled" | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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" | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,23 +1,25 @@ | ||
| { | ||
| "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", | ||
| "lib/morpho-blue/certora/harness/Util.sol", | ||
| "certora/helpers/MetaMorphoHarness.sol", | ||
| "certora/helpers/ERC20Helper.sol" | ||
| ], | ||
| "solc_map": { | ||
| "MorphoHarness": "solc-0.8.19", | ||
| "Util": "solc-0.8.19", | ||
| "MetaMorphoHarness": "solc-0.8.21", | ||
| "ERC20Helper": "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" | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,25 +1,27 @@ | ||
| { | ||
| "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", | ||
| "lib/morpho-blue/certora/harness/Util.sol", | ||
| "certora/helpers/MetaMorphoHarness.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", | ||
| "ERC20Helper": "solc-0.8.21" | ||
| }, | ||
| "verify": "MetaMorphoHarness:certora/specs/Liveness.spec", | ||
| "loop_iter": "2", | ||
| "optimistic_loop": true, | ||
| "prover_args": [ | ||
| "-depth 0" | ||
| ], | ||
| "smt_timeout": "7000", | ||
| "rule_sanity": "basic", | ||
| "server": "production", | ||
| "msg": "MetaMorpho Liveness" | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,22 +1,25 @@ | ||
| { | ||
| "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": [ | ||
| "lib/morpho-blue/certora/harness/Util.sol", | ||
| "certora/helpers/MetaMorphoHarness.sol" | ||
| ], | ||
| "solc_map": { | ||
| "Util": "solc-0.8.19", | ||
| "MetaMorphoHarness": "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" | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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" | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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" | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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" | ||
| } |
Oops, something went wrong.