Skip to content

Commit 8a24b7e

Browse files
aehyvariaehyvari
committed
More conf refactoring
1 parent deb1d6b commit 8a24b7e

19 files changed

+27
-413
lines changed

‎certora/confs/Balances.conf‎

Lines changed: 0 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -2,25 +2,5 @@
22
"override_base_config": "certora/confs/BaseConfForInheritance.conf",
33
"verify": "EulerEarnHarness:certora/specs/Balances.spec",
44
"msg": "Euler Earn - Rules about Balances",
5-
"files": [
6-
"certora/harnesses/EulerEarnHarness.sol",
7-
"lib/ethereum-vault-connector/src/EthereumVaultConnector.sol",
8-
"lib/euler-vault-kit/lib/permit2/src/Permit2.sol",
9-
"src/EulerEarnFactory.sol",
10-
"test/mocks/PerspectiveMock.sol",
11-
"certora/mocks/VaultMock0.sol",
12-
"certora/mocks/VaultMock1.sol",
13-
"certora/mocks/Token0.sol",
14-
"certora/harnesses/ERC20Helper.sol"
15-
],
16-
"link": [
17-
"EulerEarnHarness:evc=EthereumVaultConnector",
18-
"EulerEarnHarness:permit2Address=Permit2",
19-
"EulerEarnFactory:permit2Address=Permit2",
20-
"EulerEarnFactory:perspective=PerspectiveMock",
21-
"VaultMock0:_asset=Token0",
22-
"VaultMock1:_asset=Token0",
23-
"EulerEarnHarness:_asset=Token0"
24-
],
255
"loop_iter": 2
266
}

‎certora/confs/BaseConfForInheritance.conf‎

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,26 @@
33
"global_timeout": "7200",
44
"parametric_contracts": "EulerEarnHarness",
55
"rule_sanity": "basic",
6+
"files": [
7+
"certora/harnesses/EulerEarnHarness.sol",
8+
"lib/ethereum-vault-connector/src/EthereumVaultConnector.sol",
9+
"lib/euler-vault-kit/lib/permit2/src/Permit2.sol",
10+
"src/EulerEarnFactory.sol",
11+
"test/mocks/PerspectiveMock.sol",
12+
"certora/mocks/VaultMock0.sol",
13+
"certora/mocks/VaultMock1.sol",
14+
"certora/mocks/Token0.sol",
15+
"certora/harnesses/ERC20Helper.sol"
16+
],
17+
"link": [
18+
"EulerEarnHarness:evc=EthereumVaultConnector",
19+
"EulerEarnHarness:permit2Address=Permit2",
20+
"EulerEarnFactory:permit2Address=Permit2",
21+
"EulerEarnFactory:perspective=PerspectiveMock",
22+
"VaultMock0:_asset=Token0",
23+
"VaultMock1:_asset=Token0",
24+
"EulerEarnHarness:_asset=Token0"
25+
],
626
"packages": [
727
"ethereum-vault-connector=lib/ethereum-vault-connector/src",
828
"euler-vault-kit=lib/euler-vault-kit/src",

‎certora/confs/ConsistentState.conf‎

Lines changed: 0 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -3,25 +3,5 @@
33
"msg": "Euler Earn - Rules about Consistency of State",
44
"loop_iter": "2",
55
"exclude_rule" : "notInWithdrawQThenNoApproval",
6-
"files": [
7-
"certora/harnesses/EulerEarnHarness.sol",
8-
"lib/ethereum-vault-connector/src/EthereumVaultConnector.sol",
9-
"lib/euler-vault-kit/lib/permit2/src/Permit2.sol",
10-
"src/EulerEarnFactory.sol",
11-
"test/mocks/PerspectiveMock.sol",
12-
"certora/mocks/VaultMock0.sol",
13-
"certora/mocks/VaultMock1.sol",
14-
"certora/mocks/Token0.sol",
15-
"certora/harnesses/ERC20Helper.sol"
16-
],
17-
"link": [
18-
"EulerEarnHarness:evc=EthereumVaultConnector",
19-
"EulerEarnHarness:permit2Address=Permit2",
20-
"EulerEarnFactory:permit2Address=Permit2",
21-
"EulerEarnFactory:perspective=PerspectiveMock",
22-
"VaultMock0:_asset=Token0",
23-
"VaultMock1:_asset=Token0",
24-
"EulerEarnHarness:_asset=Token0"
25-
],
266
"override_base_config": "certora/confs/BaseConfForInheritance.conf"
277
}

‎certora/confs/ConsistentStateNotInQueue.conf‎

Lines changed: 1 addition & 49 deletions
Original file line numberDiff line numberDiff line change
@@ -2,57 +2,9 @@
22
"verify": "EulerEarnHarness:certora/specs/ConsistentState.spec",
33
"msg": "Euler Earn - Rules about Consistency of State",
44
"loop_iter": "2",
5-
"optimistic_loop": true,
6-
"global_timeout": "7200",
7-
"smt_timeout" : "6000",
8-
"parametric_contracts": "EulerEarnHarness",
9-
"rule_sanity": "basic",
105
"rule" : "notInWithdrawQThenNoApproval",
11-
"files": [
12-
"certora/harnesses/EulerEarnHarness.sol",
13-
"lib/ethereum-vault-connector/src/EthereumVaultConnector.sol",
14-
"lib/euler-vault-kit/lib/permit2/src/Permit2.sol",
15-
"src/EulerEarnFactory.sol",
16-
"test/mocks/PerspectiveMock.sol",
17-
"certora/mocks/VaultMock0.sol",
18-
"certora/mocks/VaultMock1.sol",
19-
"certora/mocks/Token0.sol",
20-
"certora/harnesses/ERC20Helper.sol"
21-
],
22-
"link": [
23-
"EulerEarnHarness:evc=EthereumVaultConnector",
24-
"EulerEarnHarness:permit2Address=Permit2",
25-
"EulerEarnFactory:permit2Address=Permit2",
26-
"EulerEarnFactory:perspective=PerspectiveMock",
27-
"VaultMock0:_asset=Token0",
28-
"VaultMock1:_asset=Token0",
29-
"EulerEarnHarness:_asset=Token0"
30-
],
31-
"packages": [
32-
"ethereum-vault-connector=lib/ethereum-vault-connector/src",
33-
"euler-vault-kit=lib/euler-vault-kit/src",
34-
"forge-std=lib/forge-std/src",
35-
"solmate=lib/euler-vault-kit/lib/permit2/lib/solmate"
36-
],
37-
"compiler_map": {
38-
"EulerEarnHarness": "solc-0.8.26",
39-
"EthereumVaultConnector": "solc-0.8.26",
40-
"Permit2": "solc-0.8.17",
41-
"EulerEarnFactory": "solc-0.8.26",
42-
"PerspectiveMock": "solc-0.8.26",
43-
"IRMLinearKink": "solc-0.8.26",
44-
"VaultMock0": "solc-0.8.26",
45-
"VaultMock1": "solc-0.8.26",
46-
"Token0": "solc-0.8.26",
47-
"ERC20Helper": "solc-0.8.26"
48-
},
49-
"solc_optimize": "200",
50-
"solc_via_ir": true,
51-
"assert_autofinder_success": true,
52-
"contract_recursion_limit": "1",
53-
"process": "emv",
546
"prover_args": [
557
"-cvlFunctionRevert true",
56-
"DISABLE_SPLIT"
8+
"-split false"
579
]
5810
}

‎certora/confs/Conversions.conf‎

Lines changed: 1 addition & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -6,29 +6,9 @@
66
"convertToAssetsWeakAdditivity",
77
"convertToSharesWeakAdditivity",
88
"conversionWeakMonotonicity",
9-
"conversionWeakIntegrity",
9+
"conversionWeakIntegrity"
1010
],
1111
"loop_iter": "1",
12-
"files": [
13-
"certora/harnesses/EulerEarnHarness.sol",
14-
"lib/ethereum-vault-connector/src/EthereumVaultConnector.sol",
15-
"lib/euler-vault-kit/lib/permit2/src/Permit2.sol",
16-
"src/EulerEarnFactory.sol",
17-
"test/mocks/PerspectiveMock.sol",
18-
"certora/mocks/VaultMock0.sol",
19-
"certora/mocks/VaultMock1.sol",
20-
"certora/mocks/Token0.sol",
21-
"certora/harnesses/ERC20Helper.sol"
22-
],
23-
"link": [
24-
"EulerEarnHarness:evc=EthereumVaultConnector",
25-
"EulerEarnHarness:permit2Address=Permit2",
26-
"EulerEarnFactory:permit2Address=Permit2",
27-
"EulerEarnFactory:perspective=PerspectiveMock",
28-
"VaultMock0:_asset=Token0",
29-
"VaultMock1:_asset=Token0",
30-
"EulerEarnHarness:_asset=Token0"
31-
],
3212
"optimistic_summary_recursion": true,
3313
"prover_args": [
3414
"-depth 20",

‎certora/confs/ERC4626.conf‎

Lines changed: 1 addition & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -9,29 +9,9 @@
99
"zeroDepositZeroShares",
1010
"redeemingAllValidity",
1111
"zeroAllowanceOnAssets",
12-
"onlyContributionMethodsReduceAssets",
12+
"onlyContributionMethodsReduceAssets"
1313
],
1414
"loop_iter": "1",
15-
"files": [
16-
"certora/harnesses/EulerEarnHarness.sol",
17-
"lib/ethereum-vault-connector/src/EthereumVaultConnector.sol",
18-
"lib/euler-vault-kit/lib/permit2/src/Permit2.sol",
19-
"src/EulerEarnFactory.sol",
20-
"test/mocks/PerspectiveMock.sol",
21-
"certora/mocks/VaultMock0.sol",
22-
"certora/mocks/VaultMock1.sol",
23-
"certora/mocks/Token0.sol",
24-
"certora/harnesses/ERC20Helper.sol"
25-
],
26-
"link": [
27-
"EulerEarnHarness:evc=EthereumVaultConnector",
28-
"EulerEarnHarness:permit2Address=Permit2",
29-
"EulerEarnFactory:permit2Address=Permit2",
30-
"EulerEarnFactory:perspective=PerspectiveMock",
31-
"VaultMock0:_asset=Token0",
32-
"VaultMock1:_asset=Token0",
33-
"EulerEarnHarness:_asset=Token0"
34-
],
3515
"optimistic_summary_recursion": true,
3616
"override_base_config": "certora/confs/BaseConfForInheritance.conf"
3717
}

‎certora/confs/Enabled.conf‎

Lines changed: 0 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -2,24 +2,5 @@
22
"verify": "EulerEarnHarness:certora/specs/Enabled.spec",
33
"msg": "Euler Earn - Rules about Enabled Markets",
44
"loop_iter": "2",
5-
"files": [
6-
"certora/harnesses/EulerEarnHarness.sol",
7-
"lib/ethereum-vault-connector/src/EthereumVaultConnector.sol",
8-
"lib/euler-vault-kit/lib/permit2/src/Permit2.sol",
9-
"src/EulerEarnFactory.sol",
10-
"test/mocks/PerspectiveMock.sol",
11-
"certora/mocks/VaultMock0.sol",
12-
"certora/mocks/VaultMock1.sol",
13-
"certora/mocks/Token0.sol"
14-
],
15-
"link": [
16-
"EulerEarnHarness:evc=EthereumVaultConnector",
17-
"EulerEarnHarness:permit2Address=Permit2",
18-
"EulerEarnFactory:permit2Address=Permit2",
19-
"EulerEarnFactory:perspective=PerspectiveMock",
20-
"VaultMock0:_asset=Token0",
21-
"VaultMock1:_asset=Token0",
22-
"EulerEarnHarness:_asset=Token0"
23-
],
245
"override_base_config": "certora/confs/BaseConfForInheritance.conf"
256
}

‎certora/confs/Immutability.conf‎

Lines changed: 0 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -2,25 +2,6 @@
22
"verify": "EulerEarnHarness:certora/specs/Immutability.spec",
33
"msg": "Euler Earn - Rules about Immutability",
44
"loop_iter": "2",
5-
"files": [
6-
"certora/harnesses/EulerEarnHarness.sol",
7-
"lib/ethereum-vault-connector/src/EthereumVaultConnector.sol",
8-
"lib/euler-vault-kit/lib/permit2/src/Permit2.sol",
9-
"src/EulerEarnFactory.sol",
10-
"test/mocks/PerspectiveMock.sol",
11-
"certora/mocks/VaultMock0.sol",
12-
"certora/mocks/VaultMock1.sol",
13-
"certora/mocks/Token0.sol"
14-
],
15-
"link": [
16-
"EulerEarnHarness:evc=EthereumVaultConnector",
17-
"EulerEarnHarness:permit2Address=Permit2",
18-
"EulerEarnFactory:permit2Address=Permit2",
19-
"EulerEarnFactory:perspective=PerspectiveMock",
20-
"VaultMock0:_asset=Token0",
21-
"VaultMock1:_asset=Token0",
22-
"EulerEarnHarness:_asset=Token0"
23-
],
245
"contract_recursion_limit": "1",
256
"override_base_config": "certora/confs/BaseConfForInheritance.conf"
267
}

‎certora/confs/Liveness.conf‎

Lines changed: 0 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -2,26 +2,6 @@
22
"verify": "EulerEarnHarness:certora/specs/Liveness.spec",
33
"msg": "Euler Earn - rules about Liveness",
44
"loop_iter": "2",
5-
"files": [
6-
"certora/harnesses/EulerEarnHarness.sol",
7-
"lib/ethereum-vault-connector/src/EthereumVaultConnector.sol",
8-
"lib/euler-vault-kit/lib/permit2/src/Permit2.sol",
9-
"src/EulerEarnFactory.sol",
10-
"test/mocks/PerspectiveMock.sol",
11-
"certora/mocks/VaultMock0.sol",
12-
"certora/mocks/VaultMock1.sol",
13-
"certora/mocks/Token0.sol",
14-
"certora/harnesses/ERC20Helper.sol"
15-
],
16-
"link": [
17-
"EulerEarnHarness:evc=EthereumVaultConnector",
18-
"EulerEarnHarness:permit2Address=Permit2",
19-
"EulerEarnFactory:permit2Address=Permit2",
20-
"EulerEarnFactory:perspective=PerspectiveMock",
21-
"VaultMock0:_asset=Token0",
22-
"VaultMock1:_asset=Token0",
23-
"EulerEarnHarness:_asset=Token0"
24-
],
255
"prover_args": [
266
"-depth 20",
277
"-cvlFunctionRevert true"

‎certora/confs/LostAssets.conf‎

Lines changed: 0 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -2,25 +2,6 @@
22
"verify": "EulerEarnHarness:certora/specs/LostAssets.spec",
33
"msg": "Euler Earn - Properties on Lost Assets",
44
"loop_iter": "1",
5-
"files": [
6-
"certora/harnesses/EulerEarnHarness.sol",
7-
"lib/ethereum-vault-connector/src/EthereumVaultConnector.sol",
8-
"lib/euler-vault-kit/lib/permit2/src/Permit2.sol",
9-
"src/EulerEarnFactory.sol",
10-
"test/mocks/PerspectiveMock.sol",
11-
"certora/mocks/VaultMock0.sol",
12-
"certora/mocks/VaultMock1.sol",
13-
"certora/mocks/Token0.sol"
14-
],
15-
"link": [
16-
"EulerEarnHarness:evc=EthereumVaultConnector",
17-
"EulerEarnHarness:permit2Address=Permit2",
18-
"EulerEarnFactory:permit2Address=Permit2",
19-
"EulerEarnFactory:perspective=PerspectiveMock",
20-
"VaultMock0:_asset=Token0",
21-
"VaultMock1:_asset=Token0",
22-
"EulerEarnHarness:_asset=Token0"
23-
],
245
"prover_args": [
256
"-cvlFunctionRevert true",
267
"-solvers [z3:def{randomSeed=110},z3:def{randomSeed=111},z3:def{randomSeed=112},z3:def{randomSeed=113},z3:def{randomSeed=114},z3:def{randomSeed=115},z3:def{randomSeed=116},z3:def{randomSeed=117},z3:def{randomSeed=118},z3:def{randomSeed=119}]"

0 commit comments

Comments
 (0)