[certora] Post Maturity Debt check#967
Conversation
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: b6d8aa7fd6
ℹ️ About Codex in GitHub
Codex has been enabled to automatically review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
When you sign up for Codex through ChatGPT, Codex can also answer questions or update the PR, like "@codex address that feedback".
| // This encodes a no-reentrancy assumption, justified because the property is about the effect of each | ||
| // function's own body on debt, not the full transaction including (re-entrant) callbacks. |
There was a problem hiding this comment.
Actually the interesting case was in callbacks in the previous code: we want to make sure that the lock is properly set there.
Now, it's not that it's "justified because the property is about the effect of each function's own body on debt, not the full transaction including (re-entrant) callbacks." We do care about the full transaction including callbacks. The reason why it's ok is because if you prove that no function can increase the debt without callbacks, then by induction you also prove that no function can increase the debt with callbacks (the inner-most call doesn't increase debt, and by the induction hypothesis the whole call without the inner-most call doesn't increase the debt)
Co-authored-by: Quentin Garchery <garchery.quentin@gmail.com> Signed-off-by: lilCertora <lilian@certora.com>
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 5f89574268
ℹ️ About Codex in GitHub
Codex has been enabled to automatically review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
When you sign up for Codex through ChatGPT, Codex can also answer questions or update the PR, like "@codex address that feedback".
2 participants
Post maturity the liquidation is locked or the debt cannot increase