-
Notifications
You must be signed in to change notification settings - Fork 0
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
setup, mock and rules for SafeMigration, SafeToL2Migration and SafeToL2Setup #1
base: main
Are you sure you want to change the base?
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Overall it looks good. Running with sanity advanced would give me a bit more confidence that there are not some paths pruned because of linking/dispatcher issues.
certora/conf/SafeMigration.conf
Outdated
"optimistic_loop": true, | ||
"process": "emv", | ||
"prover_args": [ | ||
" -smt_groundQuantifiers false" |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Do we need the quantifier options? If not, we could just not set the prover args.
This also applies to the other conf files.
certora/conf/SafeMigration.conf
Outdated
"loop_iter": "3", | ||
"msg": "SafeMigration", | ||
"optimistic_hashing": true, | ||
"optimistic_loop": true, |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
We could try without optimistic_loop here. I think there are no loops or unbounded hashing, so if we can prove it without, it would be better.
This also applies to the other conf files.
certora/conf/SafeMigration.conf
Outdated
"prover_args": [ | ||
" -smt_groundQuantifiers false" | ||
], | ||
"rule_sanity": "basic", |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Can you try with advanced sanity? The basic sanity will not check if the functions always revert, because you call them with @withreverted
.
Hi @jhoenicke ,
Following our brainstorming session for different rules, I prepared the following setup and rules.
I also added run links at the top of each spec file.
Those include runs of all the rules (both with and without sanity basic).
All the rules pass successfully.
Please review and advise if any changes should be made.
Thank you.