Skip to content

Antti/specs #2

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
wants to merge 5 commits into from
Closed

Antti/specs #2

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
cffc02c
Improvements for CI and confs
aehyvari Aug 18, 2025
310482e
Compilation fixes in confs
aehyvari Aug 20, 2025
6d5413f
Add missing suffix to base config
aehyvari Aug 20, 2025
588bc5f
Use action v2 after fix backported
aehyvari Aug 20, 2025
2a4f5ff
Add missing loop_iter to Balances.conf
aehyvari Aug 20, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion .github/workflows/certora-prover.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ on:
pull_request:
branches:
- master
- certora/specs
workflow_dispatch:

jobs:
Expand Down Expand Up @@ -62,4 +63,3 @@ jobs:
certora-key: ${{ secrets.CERTORAKEY }}
env:
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}

33 changes: 2 additions & 31 deletions certora/confs/Balances.conf
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,11 +1,7 @@
{
"override_base_config": "certora/confs/BaseConfForInheritance.conf",
"verify": "EulerEarnHarness:certora/specs/Balances.spec",
"msg": "Euler Earn - Rules about Balances",
"loop_iter": "2",
"optimistic_loop": true,
"global_timeout": "7200",
"parametric_contracts": "EulerEarnHarness",
"rule_sanity": "basic",
"files": [
"certora/harnesses/EulerEarnHarness.sol",
"lib/ethereum-vault-connector/src/EthereumVaultConnector.sol",
Expand All @@ -26,30 +22,5 @@
"VaultMock1:_asset=Token0",
"EulerEarnHarness:_asset=Token0"
],
"packages": [
"ethereum-vault-connector=lib/ethereum-vault-connector/src",
"euler-vault-kit=lib/euler-vault-kit/src",
"forge-std=lib/forge-std/src",
"solmate=lib/euler-vault-kit/lib/permit2/lib/solmate"
],
"compiler_map": {
"EulerEarnHarness": "solc-0.8.26",
"EthereumVaultConnector": "solc-0.8.26",
"Permit2": "solc-0.8.17",
"EulerEarnFactory": "solc-0.8.26",
"PerspectiveMock": "solc-0.8.26",
"IRMLinearKink": "solc-0.8.26",
"VaultMock0": "solc-0.8.26",
"VaultMock1": "solc-0.8.26",
"Token0": "solc-0.8.26",
"ERC20Helper": "solc-0.8.26"
},
"solc_optimize": "200",
"solc_via_ir": true,
"assert_autofinder_success": true,
"contract_recursion_limit": "1",
"process": "emv",
"prover_args": [
"-cvlFunctionRevert true"
]
"loop_iter": 2
}
34 changes: 34 additions & 0 deletions certora/confs/BaseConfForInheritance.conf
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,34 @@
{
"optimistic_loop": true,
"global_timeout": "7200",
"parametric_contracts": "EulerEarnHarness",
"rule_sanity": "basic",
"packages": [
"ethereum-vault-connector=lib/ethereum-vault-connector/src",
"euler-vault-kit=lib/euler-vault-kit/src",
"forge-std=lib/forge-std/src",
"solmate=lib/euler-vault-kit/lib/permit2/lib/solmate"
],
"compiler_map": {
"EulerEarnHarness": "solc-0.8.26",
"EthereumVaultConnector": "solc-0.8.26",
"Permit2": "solc-0.8.17",
"EulerEarnFactory": "solc-0.8.26",
"PerspectiveMock": "solc-0.8.26",
"IRMLinearKink": "solc-0.8.26",
"VaultMock0": "solc-0.8.26",
"VaultMock1": "solc-0.8.26",
"Token0": "solc-0.8.26",
"ERC20Helper": "solc-0.8.26"
},
"solc_optimize": "200",
"solc_via_ir": true,
"assert_autofinder_success": true,
"contract_recursion_limit": "1",
"process": "emv",
"prover_args": [
"-cvlFunctionRevert true"
],
"build_cache": true,
"smt_timeout": "6000"
}
32 changes: 1 addition & 31 deletions certora/confs/ConsistentState.conf
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,11 +2,6 @@
"verify": "EulerEarnHarness:certora/specs/ConsistentState.spec",
"msg": "Euler Earn - Rules about Consistency of State",
"loop_iter": "2",
"optimistic_loop": true,
"global_timeout": "7200",
"smt_timeout" : "6000",
"parametric_contracts": "EulerEarnHarness",
"rule_sanity": "basic",
"exclude_rule" : "notInWithdrawQThenNoApproval",
"files": [
"certora/harnesses/EulerEarnHarness.sol",
Expand All @@ -28,30 +23,5 @@
"VaultMock1:_asset=Token0",
"EulerEarnHarness:_asset=Token0"
],
"packages": [
"ethereum-vault-connector=lib/ethereum-vault-connector/src",
"euler-vault-kit=lib/euler-vault-kit/src",
"forge-std=lib/forge-std/src",
"solmate=lib/euler-vault-kit/lib/permit2/lib/solmate"
],
"compiler_map": {
"EulerEarnHarness": "solc-0.8.26",
"EthereumVaultConnector": "solc-0.8.26",
"Permit2": "solc-0.8.17",
"EulerEarnFactory": "solc-0.8.26",
"PerspectiveMock": "solc-0.8.26",
"IRMLinearKink": "solc-0.8.26",
"VaultMock0": "solc-0.8.26",
"VaultMock1": "solc-0.8.26",
"Token0": "solc-0.8.26",
"ERC20Helper": "solc-0.8.26"
},
"solc_optimize": "200",
"solc_via_ir": true,
"assert_autofinder_success": true,
"contract_recursion_limit": "1",
"process": "emv",
"prover_args": [
"-cvlFunctionRevert true"
]
"override_base_config": "certora/confs/BaseConfForInheritance.conf"
}
32 changes: 2 additions & 30 deletions certora/confs/Conversions.conf
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
{
"build_cache": true,
"verify": "EulerEarnHarness:certora/specs/ConversionRules.spec",
"msg": "conversion rules",
"rule": [
Expand All @@ -9,12 +8,7 @@
"conversionWeakMonotonicity",
"conversionWeakIntegrity",
],
"rule_sanity": "basic",
"loop_iter": "1",
"optimistic_loop": true,
"global_timeout": "7200",
"smt_timeout": "6000",
"parametric_contracts": "EulerEarnHarness",
"files": [
"certora/harnesses/EulerEarnHarness.sol",
"lib/ethereum-vault-connector/src/EthereumVaultConnector.sol",
Expand All @@ -35,32 +29,10 @@
"VaultMock1:_asset=Token0",
"EulerEarnHarness:_asset=Token0"
],
"packages": [
"ethereum-vault-connector=lib/ethereum-vault-connector/src",
"euler-vault-kit=lib/euler-vault-kit/src",
"forge-std=lib/forge-std/src",
"solmate=lib/euler-vault-kit/lib/permit2/lib/solmate"
],
"compiler_map": {
"EulerEarnHarness": "solc-0.8.26",
"EthereumVaultConnector": "solc-0.8.26",
"Permit2": "solc-0.8.17",
"EulerEarnFactory": "solc-0.8.26",
"PerspectiveMock": "solc-0.8.26",
"IRMLinearKink": "solc-0.8.26",
"VaultMock0": "solc-0.8.26",
"VaultMock1": "solc-0.8.26",
"Token0": "solc-0.8.26",
"ERC20Helper": "solc-0.8.26"
},
"solc_optimize": "200",
"solc_via_ir": true,
"assert_autofinder_success": true,
"contract_recursion_limit": "1",
"optimistic_summary_recursion": true,
"process": "emv",
"prover_args": [
"-depth 20",
"-cvlFunctionRevert true"
]
],
"override_base_config": "certora/confs/BaseConfForInheritance.conf"
}
33 changes: 1 addition & 32 deletions certora/confs/ERC4626.conf
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
{
"build_cache": true,
"verify": "EulerEarnHarness:certora/specs/EulerEarnERC4626.spec",
"msg": "ERC4626-style properties and helper properties",
"rule": [
Expand All @@ -12,12 +11,7 @@
"zeroAllowanceOnAssets",
"onlyContributionMethodsReduceAssets",
],
"rule_sanity": "basic",
"loop_iter": "1",
"optimistic_loop": true,
"global_timeout": "7200",
"smt_timeout": "6000",
"parametric_contracts": "EulerEarnHarness",
"files": [
"certora/harnesses/EulerEarnHarness.sol",
"lib/ethereum-vault-connector/src/EthereumVaultConnector.sol",
Expand All @@ -38,31 +32,6 @@
"VaultMock1:_asset=Token0",
"EulerEarnHarness:_asset=Token0"
],
"packages": [
"ethereum-vault-connector=lib/ethereum-vault-connector/src",
"euler-vault-kit=lib/euler-vault-kit/src",
"forge-std=lib/forge-std/src",
"solmate=lib/euler-vault-kit/lib/permit2/lib/solmate"
],
"compiler_map": {
"EulerEarnHarness": "solc-0.8.26",
"EthereumVaultConnector": "solc-0.8.26",
"Permit2": "solc-0.8.17",
"EulerEarnFactory": "solc-0.8.26",
"PerspectiveMock": "solc-0.8.26",
"IRMLinearKink": "solc-0.8.26",
"VaultMock0": "solc-0.8.26",
"VaultMock1": "solc-0.8.26",
"Token0": "solc-0.8.26",
"ERC20Helper": "solc-0.8.26"
},
"solc_optimize": "200",
"solc_via_ir": true,
"assert_autofinder_success": true,
"contract_recursion_limit": "1",
"optimistic_summary_recursion": true,
"process": "emv",
"prover_args": [
"-cvlFunctionRevert true"
]
"override_base_config": "certora/confs/BaseConfForInheritance.conf"
}
30 changes: 1 addition & 29 deletions certora/confs/Enabled.conf
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,10 +2,6 @@
"verify": "EulerEarnHarness:certora/specs/Enabled.spec",
"msg": "Euler Earn - Rules about Enabled Markets",
"loop_iter": "2",
"optimistic_loop": true,
"global_timeout": "7200",
"parametric_contracts": "EulerEarnHarness",
"rule_sanity": "basic",
"files": [
"certora/harnesses/EulerEarnHarness.sol",
"lib/ethereum-vault-connector/src/EthereumVaultConnector.sol",
Expand All @@ -25,29 +21,5 @@
"VaultMock1:_asset=Token0",
"EulerEarnHarness:_asset=Token0"
],
"packages": [
"ethereum-vault-connector=lib/ethereum-vault-connector/src",
"euler-vault-kit=lib/euler-vault-kit/src",
"forge-std=lib/forge-std/src",
"solmate=lib/euler-vault-kit/lib/permit2/lib/solmate"
],
"compiler_map": {
"EulerEarnHarness": "solc-0.8.26",
"EthereumVaultConnector": "solc-0.8.26",
"Permit2": "solc-0.8.17",
"EulerEarnFactory": "solc-0.8.26",
"PerspectiveMock": "solc-0.8.26",
"IRMLinearKink": "solc-0.8.26",
"VaultMock0": "solc-0.8.26",
"VaultMock1": "solc-0.8.26",
"Token0": "solc-0.8.26"
},
"solc_optimize": "200",
"solc_via_ir": true,
"assert_autofinder_success": true,
"contract_recursion_limit": "1",
"process": "emv",
"prover_args": [
"-cvlFunctionRevert true"
]
"override_base_config": "certora/confs/BaseConfForInheritance.conf"
}
29 changes: 1 addition & 28 deletions certora/confs/Immutability.conf
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,10 +2,6 @@
"verify": "EulerEarnHarness:certora/specs/Immutability.spec",
"msg": "Euler Earn - Rules about Immutability",
"loop_iter": "2",
"optimistic_loop": true,
"global_timeout": "7200",
"parametric_contracts": "EulerEarnHarness",
"rule_sanity": "basic",
"files": [
"certora/harnesses/EulerEarnHarness.sol",
"lib/ethereum-vault-connector/src/EthereumVaultConnector.sol",
Expand All @@ -25,29 +21,6 @@
"VaultMock1:_asset=Token0",
"EulerEarnHarness:_asset=Token0"
],
"packages": [
"ethereum-vault-connector=lib/ethereum-vault-connector/src",
"euler-vault-kit=lib/euler-vault-kit/src",
"forge-std=lib/forge-std/src",
"solmate=lib/euler-vault-kit/lib/permit2/lib/solmate"
],
"compiler_map": {
"EulerEarnHarness": "solc-0.8.26",
"EthereumVaultConnector": "solc-0.8.26",
"Permit2": "solc-0.8.17",
"EulerEarnFactory": "solc-0.8.26",
"PerspectiveMock": "solc-0.8.26",
"IRMLinearKink": "solc-0.8.26",
"VaultMock0": "solc-0.8.26",
"VaultMock1": "solc-0.8.26",
"Token0": "solc-0.8.26"
},
"solc_optimize": "200",
"solc_via_ir": true,
"assert_autofinder_success": true,
"contract_recursion_limit": "1",
"process": "emv",
"prover_args": [
"-cvlFunctionRevert true"
]
"override_base_config": "certora/confs/BaseConfForInheritance.conf"
}
31 changes: 2 additions & 29 deletions certora/confs/Liveness.conf
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,11 +2,6 @@
"verify": "EulerEarnHarness:certora/specs/Liveness.spec",
"msg": "Euler Earn - rules about Liveness",
"loop_iter": "2",
"optimistic_loop": true,
"global_timeout": "7200",
"smt_timeout" : "6000",
"parametric_contracts": "EulerEarnHarness",
"rule_sanity": "basic",
"files": [
"certora/harnesses/EulerEarnHarness.sol",
"lib/ethereum-vault-connector/src/EthereumVaultConnector.sol",
Expand All @@ -27,31 +22,9 @@
"VaultMock1:_asset=Token0",
"EulerEarnHarness:_asset=Token0"
],
"packages": [
"ethereum-vault-connector=lib/ethereum-vault-connector/src",
"euler-vault-kit=lib/euler-vault-kit/src",
"forge-std=lib/forge-std/src",
"solmate=lib/euler-vault-kit/lib/permit2/lib/solmate"
],
"compiler_map": {
"EulerEarnHarness": "solc-0.8.26",
"EthereumVaultConnector": "solc-0.8.26",
"Permit2": "solc-0.8.17",
"EulerEarnFactory": "solc-0.8.26",
"PerspectiveMock": "solc-0.8.26",
"IRMLinearKink": "solc-0.8.26",
"VaultMock0": "solc-0.8.26",
"VaultMock1": "solc-0.8.26",
"Token0": "solc-0.8.26",
"ERC20Helper": "solc-0.8.26"
},
"solc_optimize": "200",
"solc_via_ir": true,
"assert_autofinder_success": true,
"contract_recursion_limit": "1",
"process": "emv",
"prover_args": [
"-depth 20",
"-cvlFunctionRevert true"
]
],
"override_base_config": "certora/confs/BaseConfForInheritance.conf"
}
Loading
Loading