Skip to content

[Certora] Call resolution problem #253

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

Jump to bottom
Draft
gd-colin wants to merge 3 commits into
base: main
Choose a base branch
from
Draft

[Certora] Call resolution problem #253

gd-colin wants to merge 3 commits into from

Conversation

@gd-colin
Copy link
Contributor

@gd-colin gd-colin commented Mar 7, 2025 •
edited
Loading

This draft PR:

  • showcase the call resolution problem where a forbidden call still gets resolved even though it should not;
  • the target call should reach an assert false, we attempt to provide hints to reach it however, the verification goes through instead of failing;
  • this could be used to improve the spec of Paraswap related to trusting the Augustus contract and its approvals.

You can check the outcome here : https://github.com/morpho-org/bundler3/actions/runs/13725079449/job/38389473996?pr=253

@gd-colin gd-colin added the verif Fromal verification with Certora label Mar 7, 2025
@gd-colin gd-colin requested a review from QGarchery March 7, 2025 16:32
@gd-colin gd-colin self-assigned this Mar 7, 2025
@gd-colin
Copy link
Contributor Author

gd-colin commented Mar 7, 2025

Wont fix the linter issue for the moment.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@QGarchery QGarchery Awaiting requested review from QGarchery

At least 2 approving reviews are required to merge this pull request.

Assignees

@gd-colin gd-colin

Labels

verif Fromal verification with Certora

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@gd-colin