[Certora] Net credit after pending fee stays constant#988
Conversation
The netCredit is the credit after updatePendingView minus all future pending fees. This value should never decrease as long as the user is not actively trading on the market or withdrawing the funds. The only notable exception is a liquidate that causes bad debt, so the rule for liquidate assumes no bad debt.
![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: c9f4d1aa07
ℹ️ About Codex in GitHub
Your team has set up Codex to 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 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
jhoenicke
force-pushed
the
certora-credit-nondecreasing
branch
from
c9f4d1a to
5e5c7d9
Compare
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 5e5c7d9969
ℹ️ About Codex in GitHub
Your team has set up Codex to 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 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
jhoenicke
changed the title
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 18981c0f6c
ℹ️ About Codex in GitHub
Your team has set up Codex to 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 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
Co-authored-by: Quentin Garchery <garchery.quentin@gmail.com> Signed-off-by: Jochen Hoenicke <hoenicke@gmail.com>
- use uint256 instead of mathint for ghost function. - allow different market - seller and buyer case for take
Signed-off-by: Quentin Garchery <garchery.quentin@gmail.com>
Co-authored-by: Jochen Hoenicke <hoenicke@gmail.com> Signed-off-by: Jochen Hoenicke <hoenicke@gmail.com>
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 64da25e7d9
ℹ️ About Codex in GitHub
Your team has set up Codex to 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 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
lilCertora
left a comment
lilCertora
left a comment
There was a problem hiding this comment.
Looks good, nice spec
3 participants
The net credit for a user is defined as
credit - pendingFeeafter calling updateView (applying bad debt).This spec file shows that this value is not affected by any operation except withdraw,take,liquidate.
For take and withdraw we show that other users do not affect the value.
For liquidate we show that the value is unaffected if no new bad debt occured (lossIndex unchanged).
We also prove that after maturity the pending fee is zero.
corresponding thread