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.

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

[Certora] Verif expected reverts #37

Merged
merged 30 commits into from
Oct 28, 2024
Merged

[Certora] Verif expected reverts #37

merged 30 commits into from
Oct 28, 2024

Conversation

colin-morpho
Copy link
Contributor

@colin-morpho colin-morpho commented Sep 27, 2024 •
edited
Loading

This PR implements the specification of the related issue and resolves #26.

Please make sure of the following before accepting this PR:

  • the verification succeeds;
  • the README file has been updated to provide some documentation;
  • the CI has been updated as required.

@colin-morpho colin-morpho added 👷‍♀️ work in progress verification Fromal verification with Certora labels Sep 27, 2024
@colin-morpho colin-morpho self-assigned this Sep 27, 2024
@colin-morpho colin-morpho mentioned this pull request Sep 27, 2024
Merged
3 tasks
@QGarchery
Copy link
Contributor

I think you can update your branch by doing some merging. Right now it show 54 commits

@colin-morpho colin-morpho mentioned this pull request Sep 27, 2024
Open
8 tasks
@colin-morpho colin-morpho mentioned this pull request Sep 29, 2024
Merged
3 tasks
Base automatically changed from colin@verif/setup to main September 30, 2024 11:26
@colin-morpho colin-morpho linked an issue Sep 30, 2024 that may be closed by this pull request
[Certora] Verify expected reverts #26
Closed
@colin-morpho
Copy link
Contributor Author

colin-morpho commented Sep 30, 2024 •
edited
Loading

@QGarchery and @MathisGD the specification nonLiquidatablePoisitionReverts introduced in commit c410c15 succeeds the verification. However, the version of commit 68bcaf6, updated to match the current implementation in solidity catch a possible division by zero. How should we handle this?

@MathisGD MathisGD changed the title Verif expected reverts [Certora] Verif expected reverts Oct 4, 2024
@colin-morpho colin-morpho marked this pull request as ready for review October 7, 2024 16:09
@colin-morpho colin-morpho mentioned this pull request Oct 7, 2024
Closed
MathisGD
MathisGD reviewed Oct 8, 2024
View reviewed changes
Copy link
Contributor

@MathisGD MathisGD left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

🔥

certora/specs/Reverts.spec Outdated Show resolved Hide resolved
certora/README.md Outdated Show resolved Hide resolved
certora/specs/Reverts.spec Outdated Show resolved Hide resolved
certora/specs/Reverts.spec Outdated Show resolved Hide resolved
certora/specs/Reverts.spec Outdated Show resolved Hide resolved
certora/specs/Reverts.spec Outdated Show resolved Hide resolved
certora/specs/Reverts.spec Outdated Show resolved Hide resolved
certora/specs/Reverts.spec Outdated Show resolved Hide resolved
certora/specs/Reverts.spec Outdated Show resolved Hide resolved
certora/specs/Reverts.spec Outdated Show resolved Hide resolved
QGarchery
QGarchery reviewed Oct 9, 2024
View reviewed changes
certora/specs/MarketExists.spec Outdated Show resolved Hide resolved
certora/specs/MarketExists.spec Outdated Show resolved Hide resolved
certora/specs/Reverts.spec Outdated Show resolved Hide resolved
certora/specs/Reverts.spec Outdated Show resolved Hide resolved
certora/specs/Reverts.spec Outdated Show resolved Hide resolved
certora/specs/Reverts.spec Outdated Show resolved Hide resolved
certora/specs/Reverts.spec Outdated Show resolved Hide resolved
colin-morpho
colin-morpho commented Oct 10, 2024
View reviewed changes
Copy link
Contributor Author

@colin-morpho colin-morpho left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Answered many remarks, some are still open.

certora/README.md Outdated Show resolved Hide resolved
certora/specs/MarketExists.spec Outdated Show resolved Hide resolved
certora/specs/MarketExists.spec Outdated Show resolved Hide resolved
certora/specs/Reverts.spec Outdated Show resolved Hide resolved
certora/specs/Reverts.spec Outdated Show resolved Hide resolved
certora/specs/Reverts.spec Outdated Show resolved Hide resolved
certora/specs/Reverts.spec Outdated Show resolved Hide resolved
certora/specs/Reverts.spec Outdated Show resolved Hide resolved
certora/specs/Reverts.spec Outdated Show resolved Hide resolved
certora/specs/Reverts.spec Outdated Show resolved Hide resolved
MathisGD
MathisGD previously approved these changes Oct 24, 2024
View reviewed changes
Copy link
Contributor

@MathisGD MathisGD left a comment •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

🔥

edit: I'm not approving, some comments have to the tackled before (shouldn't be too long)

certora/specs/ConsistentInstantiation.spec Show resolved Hide resolved
certora/specs/MarketExists.spec Show resolved Hide resolved
certora/specs/Reverts.spec Outdated Show resolved Hide resolved
certora/specs/Reverts.spec Outdated Show resolved Hide resolved
certora/specs/Reverts.spec Outdated Show resolved Hide resolved
certora/specs/Reverts.spec Outdated Show resolved Hide resolved
certora/specs/Reverts.spec Outdated Show resolved Hide resolved
certora/specs/Reverts.spec Outdated Show resolved Hide resolved
certora/specs/Reverts.spec Outdated Show resolved Hide resolved
certora/specs/Reverts.spec Show resolved Hide resolved
QGarchery
QGarchery reviewed Oct 24, 2024
View reviewed changes
certora/specs/MarketExists.spec Show resolved Hide resolved
certora/specs/Reverts.spec Outdated Show resolved Hide resolved
certora/specs/Reverts.spec Outdated Show resolved Hide resolved
certora/specs/Reverts.spec Outdated Show resolved Hide resolved
certora/specs/Reverts.spec Outdated Show resolved Hide resolved
certora/specs/Reverts.spec Outdated Show resolved Hide resolved
certora/confs/Reverts.conf Outdated Show resolved Hide resolved
certora/specs/Reverts.spec Outdated Show resolved Hide resolved
certora/specs/Reverts.spec Outdated Show resolved Hide resolved
certora/specs/Reverts.spec Outdated Show resolved Hide resolved
MathisGD
MathisGD previously approved these changes Oct 25, 2024
View reviewed changes
QGarchery
QGarchery reviewed Oct 25, 2024
View reviewed changes
Copy link
Contributor

@QGarchery QGarchery left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Much much nicer 🔥

certora/specs/Reverts.spec Outdated Show resolved Hide resolved
certora/specs/SummaryLib.spec Outdated Show resolved Hide resolved
certora/specs/Reverts.spec Outdated Show resolved Hide resolved
certora/specs/SummaryLib.spec Outdated Show resolved Hide resolved
QGarchery
QGarchery requested changes Oct 28, 2024
View reviewed changes
certora/specs/Reverts.spec Outdated Show resolved Hide resolved
QGarchery
QGarchery reviewed Oct 28, 2024
View reviewed changes
certora/specs/SummaryLib.spec Outdated Show resolved Hide resolved
certora/helpers/Util.sol Outdated Show resolved Hide resolved
@QGarchery QGarchery mentioned this pull request Oct 28, 2024
Merged
QGarchery
QGarchery previously approved these changes Oct 28, 2024
View reviewed changes
@MathisGD MathisGD merged commit 758138b into main Oct 28, 2024
7 checks passed
@MathisGD MathisGD deleted the colin@verif/expected-reverts branch October 28, 2024 16:00
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@MathisGD MathisGD MathisGD approved these changes

@QGarchery QGarchery QGarchery approved these changes

Assignees

@colin-morpho colin-morpho

Labels
done verification Fromal verification with Certora
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

[Certora] Verify expected reverts
3 participants
@colin-morpho @QGarchery @MathisGD