[Certora] no debt without collateral improvement#891
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: ea35e44ad0
ℹ️ 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".
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 47aa6e1ac8
ℹ️ 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".
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: d00e5b30f5
ℹ️ 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".
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: f716dc6ad7
ℹ️ 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".
| // Mirror the transient liquidation-lock slot into `ghostLocked`. | ||
| // This makes the persistent ghost the source of truth and sidesteps CVL's caveat that transient storage | ||
| // is only nullified in the base step of invariants (see https://docs.certora.com/en/latest/docs/cvl/transient.html). |
There was a problem hiding this comment.
I don't understand this, why is this modeling an issue ?
The problem with those summaries is that they use a persistent ghost, so that HAVOC_ALL does not impact the lock (as it should)
There was a problem hiding this comment.
Wording was a bit off that's right, there are 2 reasons for the ghosts being persistent , 1st is that the strong invariant's "Reset transient storage" check (transaction boundary) clears a real transient lock while the persistent debt/bitmap state persists which leads to a counter example on lockedOrNoDebtWithoutCollateral (lock=true, debt=1, bitmap=0, then reset → false). and the second is that -havocAllByDefault would havoc the non persistent ghost and during take the bitmap==0 => debt==0 can't hold at the callback boundary , the seller's debt is bumped at L414, before the callbacks, and solvency is only enforced at L476 so this would create a counter example, maybe that's not what you meant ?
There was a problem hiding this comment.
I meant why can't we use the native transient storage value (no ghost at all):
- first reason is weak invariant that should hold (there is a weak invariant about every transient variable, that this variable is 0). Maybe it's not possible to do in CVL but we could just document that it holds, instead of an actual
weak invariant - For the second reason, you would still need to state the strong invariant as
!liquidationLocked || (bitmap == 0 => debt == 0), but using the getter for the transient valueliquidationLocked
There was a problem hiding this comment.
but the strong invariant liquidationLocked || (bitmap == 0 => debt == 0) doesn't hold if HAVOC_ALL impact the lock and reset it to false while the debt has increased before the callback , and in reality the callback can't write the transient lock so we would over assume and get a spurious CEX here
There was a problem hiding this comment.
but the strong invariant liquidationLocked || (bitmap == 0 => debt == 0) doesn't hold if HAVOC_ALL impact the lock and reset it to false
why not ? Isn't it the same thing as HAVOC_ALL changing the bitmap or the debt variables ?
and in reality the callback can't write the transient lock so we would over assume and get a spurious CEX here
curious to see the CEX
There was a problem hiding this comment.
why not ? Isn't it the same thing as HAVOC_ALL changing the bitmap or the debt variables ?
I mean debt/bitmap are regular storage and a reentrant call into Midnight (take, liquidate, …) really can change them via the public entrypoints, so HAVOC_ALL havocing them is faithful and pinning them would be unsound but the lock is transient storage so not modifiable via reentrancy.
Here is the CEX without the ghost :
weak invariant liquidationLocked == falsefails after every method with an external call because-havocAllByDefaulthavocs the transient slot at the unresolved call, so the lock is nonzero when the method returns- the
strong invariant liquidationLocked || (bitmap==0 ⇒ debt==0)fails at the "Reset transient storage" step: the prover nullifies the lock at the tx boundary →liquidationLockedbecomes false while the persistentdebt/bitmapstill hold a mid-take state (debt>0, bitmap=0) → violation.
There was a problem hiding this comment.
the lock is transient storage so not modifiable via reentrancy.
I don't think this holds: I can create a function that changes the transient storage (take does it) and that function could change it in arbitrary ways. This means that a reentrancy could change the transient storage in arbitrary ways. So, without further analysis, the safe modeling is that external calls havoc the transient storage.
weak invariant liquidationLocked == falsefails after every method with an external call because -havocAllByDefaulthavocs the transient slot at the unresolved call, so the lock is nonzero when the method returns
For this counter-example, it's showing that we are missing a lemma to make the proof go through, not that we need to constrain the behavior of the transient storage.
here we are missing the property that each external call leaves the lock unchanged. This property can first be proven by assuming that external calls leave the lock unchanged as well, and by induction it would hold in the general case
the
strong invariant liquidationLocked || (bitmap==0 ⇒ debt==0)fails at the "Reset transient storage" step: the prover nullifies the lock at the tx boundary →liquidationLockedbecomes false while the persistentdebt/bitmapstill hold a mid-take state (debt>0, bitmap=0) → violation.
this explains the ghost, if there is no way to explain to the prover that weak invariant liquidationLocked == false is enough to rule out this counter-example. But we could still use a non-persistent ghost I think
review changes 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: 874caefd02
ℹ️ 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".
Co-authored-by: Quentin Garchery <garchery.quentin@gmail.com> Signed-off-by: lilCertora <lilian@certora.com>
2 participants
wishlist item : "no position can have collateral = 0 everywhere and some debt, see #764 (comment)"
Comes in complementary if the invariant in collateralBitmap
corresponding thread