Skip to content
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.

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

migration to CVL2. AToken.spec get timedout #2

Open
wants to merge 101 commits into
base: master
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
101 commits
Select commit Hold shift + click to select a range
1048485
migration to CVL2. AToken.spec get timedout
nisnislevi Jun 21, 2023
91c01dc
migration to CVL2. AToken.spec get timedout
nisnislevi Jun 21, 2023
8774810
Merge branch 'cvl2-conversion' of github.com:Certora/aave-v3-core int…
nisnislevi Jun 21, 2023
38fd449
migration to CVL2. AToken.spec get timedout
nisnislevi Jun 21, 2023
7fe381f
Merge branch 'cvl2-conversion' of github.com:Certora/aave-v3-core int…
MichaelMorami Sep 13, 2023
be4d2ea
initial sanity checks
jar-ben Sep 14, 2023
12d2b99
Tadeas setup
tadeas-kucera Oct 11, 2023
55c8c08
Munge customers code: Change internal -> external
tadeas-kucera Oct 11, 2023
d92d864
Setup review passed
tadeas-kucera Oct 18, 2023
61d27db
Split spec file, fix many rules
tadeas-kucera Oct 30, 2023
0dfc14e
Add rayMul rayDiv precise summarizations, fix other problems
tadeas-kucera Nov 2, 2023
ce9998b
Fix raymuldiv summarizations and rule depositUpdatesUserATokenBalance
tadeas-kucera Nov 3, 2023
8e5df16
imports fixed.
otakar-trunda Nov 6, 2023
6a397fd
run script added
otakar-trunda Nov 6, 2023
761ffd4
Added invariant proposed by AAVE
otakar-trunda Nov 6, 2023
861e62d
Run script for user configuration added
otakar-trunda Nov 7, 2023
0b0f670
Aave Pool rules (#3)
tadeas-kucera Nov 7, 2023
0211de8
Add CVLMath, add supply_gte_debt invariant
tadeas-kucera Nov 7, 2023
9f5df3a
Add CVLMath.spec library
tadeas-kucera Nov 8, 2023
a54e961
added rule for property P19
martin-hruska Nov 9, 2023
5944ac4
Add ADDRESSES_PROVIDER
tadeas-kucera Nov 9, 2023
f32105b
Fix PoolAccurate.conf
tadeas-kucera Nov 9, 2023
f578b87
emv-xx- folders ignored
otakar-trunda Nov 10, 2023
ccedc46
Files added
otakar-trunda Nov 10, 2023
1becebe
3reserves summary added
otakar-trunda Nov 10, 2023
d472c48
run script added for reserveConfig
otakar-trunda Nov 10, 2023
017dc62
Summary added
otakar-trunda Nov 10, 2023
32a38d3
Bug fixed
otakar-trunda Nov 10, 2023
56f3856
Variables separated to two sub-structs to avoid compiler error.
otakar-trunda Nov 13, 2023
cb4d037
New updates.
otakar-trunda Nov 13, 2023
423e764
Merge branch 'otakar/ReserveConfig_Summary' into otakar/UserConfig_su…
otakar-trunda Nov 13, 2023
2b7cd6f
Inheritance removed.
otakar-trunda Nov 14, 2023
afa0096
Merge pull request #5 from Certora/otakar/UserConfig_summary
otakar-trunda Nov 14, 2023
9fccb9b
Typo fixed
otakar-trunda Nov 14, 2023
fc6e228
Conf fixed, run scripts added
otakar-trunda Nov 14, 2023
424035b
adding rule P21 and the related changes
martin-hruska Nov 15, 2023
ea229c5
Math summaries moved to a separate file.
otakar-trunda Nov 15, 2023
825650b
Fixed imports going outside "munged".
otakar-trunda Nov 15, 2023
a36f067
Path fixed
otakar-trunda Nov 15, 2023
5f0a696
Rule P20 and the related changes
martin-hruska Nov 15, 2023
58cf570
Merge branch 'cvl2-conversion' into martin/rules
martin-hruska Nov 15, 2023
d3bd81b
BV mock setup updated.
otakar-trunda Nov 15, 2023
9e8d99f
BV mock setup updated.
otakar-trunda Nov 15, 2023
dcabc67
Orig files added
otakar-trunda Nov 15, 2023
78ffc7c
Orig files added
otakar-trunda Nov 15, 2023
7ef0a97
Setup fixed
otakar-trunda Nov 15, 2023
9353632
Summaries removed
otakar-trunda Nov 15, 2023
d9afa7a
Math summaries moved.
otakar-trunda Nov 15, 2023
cad5eec
ATokenHarness used instead of Atoken
otakar-trunda Nov 15, 2023
f71c041
Setup updated
otakar-trunda Nov 20, 2023
7b118fd
Setup updated
otakar-trunda Nov 20, 2023
326c229
Changes in munged are stored via applyHarness.patch
otakar-trunda Nov 20, 2023
fe34abf
Munged files removed
otakar-trunda Nov 20, 2023
7b99210
Setup updated
otakar-trunda Nov 21, 2023
4e04f40
Munged files deleted. Will be ignored anyway
otakar-trunda Nov 21, 2023
4b0e0cc
Setup updated
otakar-trunda Nov 21, 2023
d7e52da
Reverting previous references to "_noBV" files.
otakar-trunda Nov 21, 2023
aec0dbc
DataTypes.sol are correctly munged
otakar-trunda Nov 21, 2023
efd4a6b
Setup updated
otakar-trunda Nov 21, 2023
39bb269
Bug fixed in spec
otakar-trunda Nov 21, 2023
ed09029
Setup updated
otakar-trunda Nov 22, 2023
77e76e1
Readme updated
otakar-trunda Nov 22, 2023
d42462c
Merge pull request #6 from Certora/otakar/BV-mocks-update
otakar-trunda Nov 22, 2023
ce67c4c
Merge branch 'cvl2-conversion' into martin/rules
martin-hruska Nov 22, 2023
b0a7215
Tadeas setup
tadeas-kucera Oct 11, 2023
a2d3a8d
Setup review passed
tadeas-kucera Oct 18, 2023
6c12538
Split spec file, fix many rules
tadeas-kucera Oct 30, 2023
c7ba642
Add rayMul rayDiv precise summarizations, fix other problems
tadeas-kucera Nov 2, 2023
035d864
imports fixed.
otakar-trunda Nov 6, 2023
daeeed4
run script added
otakar-trunda Nov 6, 2023
a164a0d
Added invariant proposed by AAVE
otakar-trunda Nov 6, 2023
b4709f9
Run script for user configuration added
otakar-trunda Nov 7, 2023
648e8e9
emv-xx- folders ignored
otakar-trunda Nov 10, 2023
05ca8b3
Files added
otakar-trunda Nov 10, 2023
88a2b1e
3reserves summary added
otakar-trunda Nov 10, 2023
fd75a80
run script added for reserveConfig
otakar-trunda Nov 10, 2023
8e219b1
Bug fixed
otakar-trunda Nov 10, 2023
64db0d1
Summary added
otakar-trunda Nov 10, 2023
a1b6f81
Variables separated to two sub-structs to avoid compiler error.
otakar-trunda Nov 13, 2023
2f85ee9
New updates.
otakar-trunda Nov 13, 2023
c05bb97
Inheritance removed.
otakar-trunda Nov 14, 2023
6fe1ec1
Add CVLMath, add supply_gte_debt invariant
tadeas-kucera Nov 7, 2023
5ab358b
New rules
otakar-trunda Nov 26, 2023
a8b9595
more linking, turning of bitVectors and special smt timeout
martin-hruska Dec 4, 2023
e0b8bab
adding needed dispatchers
martin-hruska Dec 4, 2023
14b04b2
adding my rules and related harness
martin-hruska Dec 4, 2023
59d6ca3
CleanUp
tadeas-kucera Dec 6, 2023
a0f4af5
Update applyHarness.patch
tadeas-kucera Dec 6, 2023
5fdde9f
Add rules in progress
tadeas-kucera Dec 6, 2023
e37b073
Cleanup methods blocks and comment out timeouting rules
tadeas-kucera Dec 7, 2023
7b6327a
things related to P21
martin-hruska Dec 7, 2023
647b095
added CVLMath
martin-hruska Dec 7, 2023
27e8321
More rules
otakar-trunda Mar 18, 2024
95f671f
Merge branch 'cvl2-conversion' into otakar/rules
otakar-trunda Mar 19, 2024
9e6ff26
Merge branch 'tadeas' of github.com:Certora/aave-v3-core into tadeas
otakar-trunda Mar 19, 2024
bc1dfec
Merge branch 'cvl2-conversion' into tadeas
otakar-trunda Mar 19, 2024
8c4ec9a
Merge branch 'tadeas' into cvl2-conversion
otakar-trunda Mar 19, 2024
0dd16f3
keeping both version of pool.spec
otakar-trunda Mar 19, 2024
ee2adc8
Merge fixes
otakar-trunda Mar 20, 2024
709de8e
Merge branch 'otakar/rules' into cvl2-conversion
otakar-trunda Mar 20, 2024
2ebc6b9
Keeping both versions of pool-no-summarizations.spec
otakar-trunda Mar 20, 2024
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
16 changes: 8 additions & 8 deletions .github/workflows/certora.yml
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ jobs:
with: { java-version: '11', java-package: jre }

- name: Install certora cli
run: pip install certora-cli==3.6.8.post3
run: pip install certora-cli

- name: Install solc
run: |
Expand All @@ -46,7 +46,7 @@ jobs:
make munged
cd ..
echo "key length" ${#CERTORAKEY}
sh certora/scripts/${{ matrix.rule }}
certoraRun certora/conf/${{ matrix.rule }}
env:
CERTORAKEY: ${{ secrets.CERTORAKEY }}

Expand All @@ -55,9 +55,9 @@ jobs:
max-parallel: 16
matrix:
rule:
- verifyAToken.sh
- verifyPool.sh getReserveNormalizedVariableDebtCheck
- verifyReserveConfiguration.sh
- verifyStableTokenCLI.sh
- verifyUserConfigCLI.sh
- verifyVariableTokenCLI.sh
- AToken.conf
- Pool.conf
- ReserveConfiguration.conf
- StableTokenCLI.conf
- UserConfigCLI.conf
- VariableTokenCLI.conf
4 changes: 3 additions & 1 deletion .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -26,4 +26,6 @@ deployments/
**.last_conf*
certora-logs
certora_debug_log.txt
resource_errors.json
resource_errors.json
emv*certora*/
ReserveLogic.xlsx
3 changes: 3 additions & 0 deletions certora/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -47,3 +47,6 @@ which can then be checked into git.
Note: there have been reports of unexpected behavior on mac, see
[issue CUST-62](https://certora.atlassian.net/browse/CUST-62?atlOrigin=eyJpIjoiZWI1MGFjNGZkZGE0NGFlNjkwYjUwYjY2NmE4ZmQ1OTIiLCJwIjoiaiJ9).

Our current `munging` replaces files `DataTypes.sol`, `ReserveConfiguration.sol` and `UserConfiguration.sol` by mock objects that provide the same functionality but don't use bitwise operations. This increases performance of our solver. After running `make munged`, the original files will be copied to `munged` folder with suffix `_orig` so that it's easy to switch back to the original implementation if needed.

The mock objects have been verified by `certora/specs/UserConfiguration.spec` and `certora/specs/ReserveConfiguration.spec` and all rules are passing.
Loading
Loading