Skip to content

Commit 982682e

Browse files
nisnislevinisnislevi
authored
fix: upgrade prover version to 7.26.0
1 parent c7b416b commit 982682e

32 files changed

+554
-615
lines changed

‎.github/workflows/certora.yml‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,9 +4,11 @@ on:
44
push:
55
branches:
66
- main
7+
- certora
78
pull_request:
89
branches:
910
- main
11+
- certora
1012

1113
workflow_dispatch:
1214

@@ -33,7 +35,7 @@ jobs:
3335
with: { java-version: "11", java-package: jre }
3436

3537
- name: Install certora cli
36-
run: pip3 install certora-cli==3.6.8.post3
38+
run: pip3 install certora-cli==7.26.0
3739

3840
- name: Install solc
3941
run: |

‎.gitignore‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,4 +6,6 @@
66
.env
77
.DS_Store
88
.gas-snapshot
9-
lcov.info
9+
lcov.info
10+
.certora_internal/
11+
.certora_recent_jobs.json

‎certora/conf/accrueYieldCheck.conf‎

Lines changed: 4 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -23,20 +23,14 @@
2323
"@openzeppelin-upgradeable=certora/munged/lib/openzeppelin-contracts-upgradeable/contracts",
2424
"@openzeppelin=certora/munged/lib/openzeppelin-contracts/contracts"
2525
],
26-
"verify": ["ATokenVaultHarness:certora/specs/accrueYieldCheck.spec"],
27-
"rule": ["accrueYieldCheck"],
2826
"optimistic_loop": true,
27+
"build_cache": true,
2928
"process": "emv",
29+
"rule": ["accrueYieldCheck"],
3030
"rule_sanity": "basic",
31-
"settings": [
32-
"-assumeUnwindCond",
33-
"-depth=15",
34-
"-mediumTimeout=1000",
35-
"-ruleSanityChecks=basic",
36-
"-t=2000"
37-
],
31+
"prover_args": ["-depth 15","-mediumTimeout 1000"],
3832
"smt_timeout": "2000",
3933
"solc": "solc8.10",
40-
"cloud": "" ,
34+
"verify": "ATokenVaultHarness:certora/specs/accrueYieldCheck.spec",
4135
"msg": "accrueYieldCheck"
4236
}

‎certora/conf/changeInContractBalanceShouldCauseAccrual.conf‎

Lines changed: 3 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@
1717
"SymbolicLendingPoolL1:underlyingToken=DummyERC20_aTokenUnderlying"
1818
],
1919
"msg": "changeInContractBalanceShouldCauseAccrual",
20+
"build_cache": true,
2021
"optimistic_loop": true,
2122
"packages": [
2223
"@aave-v3-core=certora/munged/lib/aave-v3-core/contracts",
@@ -30,18 +31,8 @@
3031
"changeInContractBalanceShouldCauseAccrual"
3132
],
3233
"rule_sanity": "basic",
33-
"settings": [
34-
"-assumeUnwindCond",
35-
"-depth=15",
36-
"-mediumTimeout=1000",
37-
"-rule=changeInContractBalanceShouldCauseAccrual",
38-
"-ruleSanityChecks=basic",
39-
"-t=2000"
40-
],
34+
"prover_args": ["-depth 15","-mediumTimeout 1000"],
4135
"smt_timeout": "2000",
4236
"solc": "solc8.10",
43-
"cloud": "" ,
44-
"verify": [
45-
"ATokenVaultHarness:certora/specs/changeInContractBalanceShouldCauseAccrual.spec"
46-
]
37+
"verify": "ATokenVaultHarness:certora/specs/changeInContractBalanceShouldCauseAccrual.spec"
4738
}

‎certora/conf/erc4626-previewOPERATIONS.conf‎

Lines changed: 8 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -24,21 +24,17 @@
2424
"@openzeppelin-upgradeable=certora/munged/lib/openzeppelin-contracts-upgradeable/contracts",
2525
"@openzeppelin=certora/munged/lib/openzeppelin-contracts/contracts"
2626
],
27+
"build_cache": true,
2728
"process": "emv",
2829
"rule": [
29-
"previewMint_amount_check","previewDeposit_amount_check","previewWithdraw_amount_check","previewRedeem_amount_check"
30-
],
31-
"settings": [
32-
"-assumeUnwindCond",
33-
"-depth=15",
34-
"-mediumTimeout=1000",
35-
"-t=2000"
30+
"previewDeposit_amount_check",
31+
"previewMint_amount_check",
32+
"previewWithdraw_amount_check",
33+
"previewRedeem_amount_check"
3634
],
35+
"prover_args": ["-depth 15","-mediumTimeout 1000"],
3736
"smt_timeout": "2000",
3837
"solc": "solc8.10",
39-
"cloud": "" ,
40-
"verify": [
41-
"ATokenVaultHarness:certora/specs/erc4626.spec"
42-
],
43-
"msg": "previewOPERATION_amount_check"
38+
"verify": "ATokenVaultHarness:certora/specs/erc4626.spec",
39+
"msg": "ERC4626: previewOPERATION_amount_check"
4440
}

‎certora/conf/fees_LEQ_ATokenBal.conf‎

Lines changed: 5 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -23,18 +23,12 @@
2323
"@openzeppelin-upgradeable=certora/munged/lib/openzeppelin-contracts-upgradeable/contracts",
2424
"@openzeppelin=certora/munged/lib/openzeppelin-contracts/contracts"
2525
],
26-
"cloud": "",
26+
"build_cache": true,
2727
"optimistic_loop": true,
2828
"process": "emv",
29-
"settings": [
30-
"-assumeUnwindCond",
31-
"-depth=15",
32-
"-mediumTimeout=1000",
33-
"-t=2000"
34-
],
29+
"prover_args": ["-depth 15","-mediumTimeout 1000"],
3530
"smt_timeout": "2000",
3631
"solc": "solc8.10",
37-
"verify": ["ATokenVaultHarness:certora/specs/fees_LEQ_ATokenBal.spec"],
38-
"rule": ["getCLMFees_LEQ_ATokenBAL_DM_other","getCLMFees_LEQ_ATokenBAL_RW"],
39-
"msg": "getclaimablefees LEQ Atoken.Balanceof[Vault]"
40-
}
32+
"verify": "ATokenVaultHarness:certora/specs/fees_LEQ_ATokenBal.spec",
33+
"msg": "getclaimablefees LEQ Atoken.Balanceof[Vault] getCLMFees_LEQ_ATokenBAL_DM_other for DEV - CVL2"
34+
}

‎certora/conf/lastVaultBalance_LEQ_ATokenBalThis.conf‎

Lines changed: 7 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,8 @@
1717
"SymbolicLendingPoolL1:aToken=AToken",
1818
"SymbolicLendingPoolL1:underlyingToken=DummyERC20_aTokenUnderlying"
1919
],
20+
"build_cache": true,
21+
"optimistic_loop": true,
2022
"packages": [
2123
"@aave-v3-core=certora/munged/lib/aave-v3-core/contracts",
2224
"@aave-v3-periphery=certora/munged/lib/aave-v3-periphery/contracts",
@@ -25,19 +27,12 @@
2527
"@openzeppelin=certora/munged/lib/openzeppelin-contracts/contracts"
2628
],
2729
"process": "emv",
28-
"optimistic_loop": true,
29-
"settings": [
30-
"-assumeUnwindCond",
31-
"-depth=15",
32-
"-mediumTimeout=1000",
33-
"-rule=lastVaultBalance_LEQ_ATokenBalThis",
34-
"-t=2000"
30+
"rule": [
31+
"lastVaultBalance_LEQ_ATokenBalThis"
3532
],
33+
"prover_args": ["-depth 15","-mediumTimeout 1000"],
3634
"smt_timeout": "2000",
3735
"solc": "solc8.10",
38-
"cloud": "" ,
39-
"verify": ["ATokenVaultHarness:certora/specs/lastVaultBal_LEQ_ATokenBalThis.spec"],
40-
"disableLocalTypeChecking": false,
41-
"rule": ["lastVaultBalance_LEQ_ATokenBalThis"],
42-
"msg": "_s.lastVaultBalance LEQ AToken.balance[this] accurate assertion"
36+
"verify": "ATokenVaultHarness:certora/specs/lastVaultBal_LEQ_ATokenBalThis.spec",
37+
"msg": "_s.lastVaultBalance LEQ AToken.balance[this] example for DEV - CVL2",
4338
}

‎certora/conf/positiveSupply_imply_positiveAssets-deposit.conf‎

Lines changed: 3 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -16,25 +16,20 @@
1616
"SymbolicLendingPoolL1:aToken=AToken",
1717
"SymbolicLendingPoolL1:underlyingToken=DummyERC20_aTokenUnderlying"
1818
],
19+
"build_cache": true,
1920
"packages": [
2021
"@aave-v3-core=certora/munged/lib/aave-v3-core/contracts",
2122
"@aave-v3-periphery=certora/munged/lib/aave-v3-periphery/contracts",
2223
"@aave/core-v3=certora/munged/lib/aave-v3-core",
2324
"@openzeppelin-upgradeable=certora/munged/lib/openzeppelin-contracts-upgradeable/contracts",
2425
"@openzeppelin=certora/munged/lib/openzeppelin-contracts/contracts"
2526
],
26-
"cloud": "",
2727
"optimistic_loop": true,
2828
"process": "emv",
29-
"settings": [
30-
"-assumeUnwindCond",
31-
"-depth=15",
32-
"-mediumTimeout=1000",
33-
"-t=2000"
34-
],
29+
"prover_args": ["-depth 15","-mediumTimeout 1000"],
3530
"smt_timeout": "2000",
3631
"solc": "solc8.10",
37-
"verify": ["ATokenVaultHarness:certora/specs/positiveSupply_imply_positiveAssets.spec"],
32+
"verify": "ATokenVaultHarness:certora/specs/positiveSupply_imply_positiveAssets.spec",
3833
"rule": ["positiveSupply_imply_positiveAssets_all_deposit"],
3934
"msg": "positiveSupply_imply_positiveAssets_all_deposit"
4035
}

‎certora/conf/positiveSupply_imply_positiveAssets-mint.conf‎

Lines changed: 3 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -16,25 +16,20 @@
1616
"SymbolicLendingPoolL1:aToken=AToken",
1717
"SymbolicLendingPoolL1:underlyingToken=DummyERC20_aTokenUnderlying"
1818
],
19+
"build_cache": true,
1920
"packages": [
2021
"@aave-v3-core=certora/munged/lib/aave-v3-core/contracts",
2122
"@aave-v3-periphery=certora/munged/lib/aave-v3-periphery/contracts",
2223
"@aave/core-v3=certora/munged/lib/aave-v3-core",
2324
"@openzeppelin-upgradeable=certora/munged/lib/openzeppelin-contracts-upgradeable/contracts",
2425
"@openzeppelin=certora/munged/lib/openzeppelin-contracts/contracts"
2526
],
26-
"cloud": "",
2727
"optimistic_loop": true,
2828
"process": "emv",
29-
"settings": [
30-
"-assumeUnwindCond",
31-
"-depth=15",
32-
"-mediumTimeout=1000",
33-
"-t=2000"
34-
],
29+
"prover_args": ["-depth 15","-mediumTimeout 1000"],
3530
"smt_timeout": "2000",
3631
"solc": "solc8.10",
37-
"verify": ["ATokenVaultHarness:certora/specs/positiveSupply_imply_positiveAssets.spec"],
32+
"verify": "ATokenVaultHarness:certora/specs/positiveSupply_imply_positiveAssets.spec",
3833
"rule": ["positiveSupply_imply_positiveAssets_all_mint"],
3934
"msg": "positiveSupply_imply_positiveAssets_all_mint"
4035
}

‎certora/conf/positiveSupply_imply_positiveAssets-other.conf‎

Lines changed: 3 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -16,25 +16,20 @@
1616
"SymbolicLendingPoolL1:aToken=AToken",
1717
"SymbolicLendingPoolL1:underlyingToken=DummyERC20_aTokenUnderlying"
1818
],
19+
"build_cache": true,
1920
"packages": [
2021
"@aave-v3-core=certora/munged/lib/aave-v3-core/contracts",
2122
"@aave-v3-periphery=certora/munged/lib/aave-v3-periphery/contracts",
2223
"@aave/core-v3=certora/munged/lib/aave-v3-core",
2324
"@openzeppelin-upgradeable=certora/munged/lib/openzeppelin-contracts-upgradeable/contracts",
2425
"@openzeppelin=certora/munged/lib/openzeppelin-contracts/contracts"
2526
],
26-
"cloud": "",
2727
"optimistic_loop": true,
2828
"process": "emv",
29-
"settings": [
30-
"-assumeUnwindCond",
31-
"-depth=15",
32-
"-mediumTimeout=1000",
33-
"-t=2000"
34-
],
29+
"prover_args": ["-depth 15","-mediumTimeout 1000"],
3530
"smt_timeout": "2000",
3631
"solc": "solc8.10",
37-
"verify": ["ATokenVaultHarness:certora/specs/positiveSupply_imply_positiveAssets.spec"],
32+
"verify": "ATokenVaultHarness:certora/specs/positiveSupply_imply_positiveAssets.spec",
3833
"rule": ["positiveSupply_imply_positiveAssets_other"],
3934
"msg": "positiveSupply_imply_positiveAssets_other"
4035
}

0 commit comments

Comments
 (0)