From 757be8cd6dda7c8958e3d456e5902ff776c02c6c Mon Sep 17 00:00:00 2001 From: miguelmtzinf Date: Tue, 19 Dec 2023 14:22:46 +0100 Subject: [PATCH] test: Add Certora conf files --- certora/conf/verifyFlashMinter.conf | 22 ++++++++++++++++ certora/conf/verifyGhoAToken.conf | 20 ++++++++++++++ .../conf/verifyGhoDiscountRateStrategy.conf | 15 +++++++++++ certora/conf/verifyGhoToken.conf | 12 +++++++++ ...ableDebtToken-rayMulDiv-summarization.conf | 26 +++++++++++++++++++ certora/conf/verifyGhoVariableDebtToken.conf | 25 ++++++++++++++++++ .../verifyGhoVariableDebtTokenInternal.conf | 16 ++++++++++++ ...ifyGhoVariableDebtToken_specialBranch.conf | 25 ++++++++++++++++++ ...verifyGhoVariableDebtToken_summarized.conf | 25 ++++++++++++++++++ 9 files changed, 186 insertions(+) create mode 100644 certora/conf/verifyFlashMinter.conf create mode 100644 certora/conf/verifyGhoAToken.conf create mode 100644 certora/conf/verifyGhoDiscountRateStrategy.conf create mode 100644 certora/conf/verifyGhoToken.conf create mode 100644 certora/conf/verifyGhoVariableDebtToken-rayMulDiv-summarization.conf create mode 100644 certora/conf/verifyGhoVariableDebtToken.conf create mode 100644 certora/conf/verifyGhoVariableDebtTokenInternal.conf create mode 100644 certora/conf/verifyGhoVariableDebtToken_specialBranch.conf create mode 100644 certora/conf/verifyGhoVariableDebtToken_summarized.conf diff --git a/certora/conf/verifyFlashMinter.conf b/certora/conf/verifyFlashMinter.conf new file mode 100644 index 00000000..d7c83438 --- /dev/null +++ b/certora/conf/verifyFlashMinter.conf @@ -0,0 +1,22 @@ +{ + "files": [ + "certora/munged/contracts/facilitators/flashMinter/GhoFlashMinter.sol:GhoFlashMinter", + "certora/munged/contracts/facilitators/aave/tokens/GhoAToken.sol:GhoAToken", + "certora/munged/contracts/gho/GhoToken.sol", + "certora/harness/MockFlashBorrower.sol" + ], + "link": [ + "MockFlashBorrower:Gho=GhoToken", + "MockFlashBorrower:AGho=GhoAToken", + "GhoFlashMinter:GHO_TOKEN=GhoToken", + "MockFlashBorrower:minter=GhoFlashMinter" + ], + "msg": "flashMinter check, all rules", + "optimistic_loop": true, + "process": "emv", + "prover_args": [ + " -contractRecursionLimit 1" + ], + "solc": "solc8.10", + "verify": "GhoFlashMinter:certora/specs/flashMinter.spec" +} \ No newline at end of file diff --git a/certora/conf/verifyGhoAToken.conf b/certora/conf/verifyGhoAToken.conf new file mode 100644 index 00000000..78b71cdc --- /dev/null +++ b/certora/conf/verifyGhoAToken.conf @@ -0,0 +1,20 @@ +{ + "files": [ + "certora/munged/contracts/facilitators/aave/tokens/GhoAToken.sol", + "certora/munged/contracts/facilitators/aave/tokens/GhoVariableDebtToken.sol", + "certora/munged/contracts/gho/GhoToken.sol", + "certora/harness/GhoTokenHarness.sol", + "certora/harness/DummyERC20A.sol", + "certora/harness/DummyERC20B.sol" + ], + "link": [ + "GhoAToken:_ghoVariableDebtToken=GhoVariableDebtToken", + "GhoVariableDebtToken:_ghoAToken=GhoAToken", + "GhoAToken:_underlyingAsset=GhoTokenHarness" + ], + "msg": "GhoAToken, all rules", + "optimistic_loop": true, + "process": "emv", + "solc": "solc8.10", + "verify": "GhoAToken:certora/specs/ghoAToken.spec" +} \ No newline at end of file diff --git a/certora/conf/verifyGhoDiscountRateStrategy.conf b/certora/conf/verifyGhoDiscountRateStrategy.conf new file mode 100644 index 00000000..c9780762 --- /dev/null +++ b/certora/conf/verifyGhoDiscountRateStrategy.conf @@ -0,0 +1,15 @@ +{ + "files": [ + "certora/harness/GhoDiscountRateStrategyHarness.sol:GhoDiscountRateStrategyHarness" + ], + "loop_iter": "2", + "msg": "GhoDiscountRateStrategy, all rules.", + "optimistic_loop": true, + "process": "emv", + "prover_args": [ + " -mediumTimeout 20 -depth 10" + ], + "smt_timeout": "500", + "solc": "solc8.10", + "verify": "GhoDiscountRateStrategyHarness:certora/specs/ghoDiscountRateStrategy.spec" +} \ No newline at end of file diff --git a/certora/conf/verifyGhoToken.conf b/certora/conf/verifyGhoToken.conf new file mode 100644 index 00000000..c6e8934c --- /dev/null +++ b/certora/conf/verifyGhoToken.conf @@ -0,0 +1,12 @@ +{ + "files": [ + "certora/harness/GhoTokenHarness.sol:GhoTokenHarness", + "certora/munged/contracts/gho/GhoToken.sol" + ], + "loop_iter": "3", + "msg": "GhoToken, all rules.", + "optimistic_loop": true, + "process": "emv", + "solc": "solc8.10", + "verify": "GhoTokenHarness:certora/specs/ghoToken.spec" +} \ No newline at end of file diff --git a/certora/conf/verifyGhoVariableDebtToken-rayMulDiv-summarization.conf b/certora/conf/verifyGhoVariableDebtToken-rayMulDiv-summarization.conf new file mode 100644 index 00000000..6bb193ba --- /dev/null +++ b/certora/conf/verifyGhoVariableDebtToken-rayMulDiv-summarization.conf @@ -0,0 +1,26 @@ +{ + "files": [ + "certora/harness/ghoVariableDebtTokenHarness.sol:GhoVariableDebtTokenHarness", + "certora/harness/DummyPool.sol", + "certora/harness/DummyERC20WithTimedBalanceOf.sol", + "certora/munged/contracts/facilitators/aave/interestStrategy/GhoDiscountRateStrategy.sol", + "certora/harness/DummyERC20A.sol", + "certora/harness/DummyERC20B.sol" + ], + "link": [ + "GhoVariableDebtTokenHarness:_discountToken=DummyERC20WithTimedBalanceOf", + "GhoVariableDebtTokenHarness:POOL=DummyPool", + "GhoVariableDebtTokenHarness:_discountRateStrategy=GhoDiscountRateStrategy" + ], + "loop_iter": "2", + "msg": " ", + "multi_assert_check": true, + "optimistic_loop": true, + "process": "emv", + "prover_args": [ + " -mediumTimeout 30 -depth 15" + ], + "smt_timeout": "900", + "solc": "solc8.10", + "verify": "GhoVariableDebtTokenHarness:certora/specs/ghoVariableDebtToken-rayMulDiv-summarization.spec" +} \ No newline at end of file diff --git a/certora/conf/verifyGhoVariableDebtToken.conf b/certora/conf/verifyGhoVariableDebtToken.conf new file mode 100644 index 00000000..30347d17 --- /dev/null +++ b/certora/conf/verifyGhoVariableDebtToken.conf @@ -0,0 +1,25 @@ +{ + "files": [ + "certora/harness/ghoVariableDebtTokenHarness.sol:GhoVariableDebtTokenHarness", + "certora/harness/DummyPool.sol", + "certora/harness/DummyERC20WithTimedBalanceOf.sol", + "certora/munged/contracts/facilitators/aave/interestStrategy/GhoDiscountRateStrategy.sol", + "certora/harness/DummyERC20A.sol", + "certora/harness/DummyERC20B.sol" + ], + "link": [ + "GhoVariableDebtTokenHarness:_discountRateStrategy=GhoDiscountRateStrategy", + "GhoVariableDebtTokenHarness:POOL=DummyPool", + "GhoVariableDebtTokenHarness:_discountToken=DummyERC20WithTimedBalanceOf" + ], + "loop_iter": "2", + "msg": "GhoVariableDebtToken", + "optimistic_loop": true, + "process": "emv", + "prover_args": [ + " -mediumTimeout 30 -depth 15" + ], + "smt_timeout": "900", + "solc": "solc8.10", + "verify": "GhoVariableDebtTokenHarness:certora/specs/ghoVariableDebtToken.spec" +} \ No newline at end of file diff --git a/certora/conf/verifyGhoVariableDebtTokenInternal.conf b/certora/conf/verifyGhoVariableDebtTokenInternal.conf new file mode 100644 index 00000000..49964c17 --- /dev/null +++ b/certora/conf/verifyGhoVariableDebtTokenInternal.conf @@ -0,0 +1,16 @@ +{ + "files": [ + "certora/harness/ghoVariableDebtTokenHarnessInternal.sol:GhoVariableDebtTokenHarnessInternal", + "certora/munged/contracts/facilitators/aave/interestStrategy/GhoDiscountRateStrategy.sol" + ], + "loop_iter": "2", + "msg": "GhoVariableDebtToken internal functions", + "optimistic_loop": true, + "process": "emv", + "prover_args": [ + " -mediumTimeout 30 -depth 15" + ], + "smt_timeout": "900", + "solc": "solc8.10", + "verify": "GhoVariableDebtTokenHarnessInternal:certora/specs/ghoVariableDebtTokenInternal.spec" +} \ No newline at end of file diff --git a/certora/conf/verifyGhoVariableDebtToken_specialBranch.conf b/certora/conf/verifyGhoVariableDebtToken_specialBranch.conf new file mode 100644 index 00000000..02d113a1 --- /dev/null +++ b/certora/conf/verifyGhoVariableDebtToken_specialBranch.conf @@ -0,0 +1,25 @@ +{ + "files": [ + "certora/harness/ghoVariableDebtTokenHarness.sol:GhoVariableDebtTokenHarness", + "certora/harness/DummyPool.sol", + "certora/harness/DummyERC20WithTimedBalanceOf.sol", + "certora/munged/contracts/facilitators/aave/interestStrategy/GhoDiscountRateStrategy.sol", + "certora/harness/DummyERC20A.sol", + "certora/harness/DummyERC20B.sol" + ], + "link": [ + "GhoVariableDebtTokenHarness:POOL=DummyPool", + "GhoVariableDebtTokenHarness:_discountToken=DummyERC20WithTimedBalanceOf", + "GhoVariableDebtTokenHarness:_discountRateStrategy=GhoDiscountRateStrategy" + ], + "loop_iter": "2", + "msg": "GhoVariableDebtToken", + "optimistic_loop": true, + "process": "emv", + "prover_args": [ + " -depth 0 -adaptiveSolverConfig false -smt_nonLinearArithmetic true" + ], + "prover_version": "shelly/z3-4-12-3-build", + "solc": "solc8.10", + "verify": "GhoVariableDebtTokenHarness:certora/specs/ghoVariableDebtToken.spec" +} \ No newline at end of file diff --git a/certora/conf/verifyGhoVariableDebtToken_summarized.conf b/certora/conf/verifyGhoVariableDebtToken_summarized.conf new file mode 100644 index 00000000..7953047c --- /dev/null +++ b/certora/conf/verifyGhoVariableDebtToken_summarized.conf @@ -0,0 +1,25 @@ +{ + "files": [ + "certora/harness/ghoVariableDebtTokenHarness.sol:GhoVariableDebtTokenHarness", + "certora/harness/DummyPool.sol", + "certora/harness/DummyERC20WithTimedBalanceOf.sol", + "certora/munged/contracts/facilitators/aave/interestStrategy/GhoDiscountRateStrategy.sol", + "certora/harness/DummyERC20A.sol", + "certora/harness/DummyERC20B.sol" + ], + "link": [ + "GhoVariableDebtTokenHarness:POOL=DummyPool", + "GhoVariableDebtTokenHarness:_discountToken=DummyERC20WithTimedBalanceOf", + "GhoVariableDebtTokenHarness:_discountRateStrategy=GhoDiscountRateStrategy" + ], + "loop_iter": "2", + "msg": "GhoVariableDebtToken", + "optimistic_loop": true, + "process": "emv", + "prover_args": [ + " -mediumTimeout 30 -depth 15" + ], + "smt_timeout": "900", + "solc": "solc8.10", + "verify": "GhoVariableDebtTokenHarness:certora/specs/ghoVariableDebtToken_summarized.spec" +} \ No newline at end of file