test: Add Certora conf files

aave · Dec 19, 2023 · 757be8c · 757be8c
1 parent 64ef916
commit 757be8c
Show file tree

Hide file tree

Showing 9 changed files with 186 additions and 0 deletions.
diff --git a/certora/conf/verifyFlashMinter.conf 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"
+}
diff --git a/certora/conf/verifyGhoAToken.conf 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"
+}
diff --git a/certora/conf/verifyGhoDiscountRateStrategy.conf 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"
+}
diff --git a/certora/conf/verifyGhoToken.conf 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"
+}
diff --git a/certora/conf/verifyGhoVariableDebtToken-rayMulDiv-summarization.conf 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"
+}
diff --git a/certora/conf/verifyGhoVariableDebtToken.conf 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"
+}
diff --git a/certora/conf/verifyGhoVariableDebtTokenInternal.conf 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"
+}
diff --git a/certora/conf/verifyGhoVariableDebtToken_specialBranch.conf 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"
+}
diff --git a/certora/conf/verifyGhoVariableDebtToken_summarized.conf 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"
+}