[Certora] Check that isHealthy is preserved if price does not change#388
Conversation
MathisGD
changed the title
|
Prover struggles with the non-linear math here. If I use mulDiv without summary the function liquidate() times out: So I added axiomatic summaries for mulDivUp/Down; the math is really tricky here, especially for There are six mulDivs that need to be reasoned about to prove that liquidation doesn't create unhealthy positions, which makes the non-linear solvers really struggle. Each isHealthy has two mulDivs, and the seizedAsset/repaidUnits computation has another two mulDivs. And for the latter the ratio is different (WAD/lif instead of lltv/WAD) and the order they are applied differs. So the solution was to insert just the right axioms that I needed for this case and do it separately from the other cases. I also had to separate out the case where a different user/obligation is liquidated. There is a new problem in supplyCollateral, which would require precise bitvector reasoning (which is infeasible in combination with 256bit multiplications). The problem is the new bitmap for the isHealthy check. If we don't reason about xor precisely, the prover finds a counterexample where the xor in the iteration of the new collateral clears the bit of the previous collateral, so that it won't be iterated. To avoid this, I added a new isHealthyNoBitmap() function with the old implementation. We can prove that this is equivalent to isHealthy() later. I excluded take() for now as it has a counterexample because of the callback bug. |
jhoenicke
force-pushed
the
jochen/healthiness
branch
3 times, most recently
from
37ee828 to
85f026f
Compare
currently fails for take() (expected) and liquidate(). The latter is because of approximating non-linear math.
Reduce max number of collaterals for sameUser to one.
Documented all axioms used.
Use a different implementation of isHealthy that avoids relying on bit-precise reasoning. The plan is to later show the equivalence of this function and the real isHealthy.
jhoenicke
force-pushed
the
jochen/healthiness
branch
from
ff9ed82 to
910325f
Compare
Show that the correct bits are set in the bitmap Show that the toHealthy function is equal to one running over all collaterals.
Co-authored-by: Quentin Garchery <garchery.quentin@gmail.com> Signed-off-by: Jochen Hoenicke <hoenicke@gmail.com>
| assert callIsHealthy(obligation, globalId, globalBorrower), "user is healthy after call"; | ||
| } | ||
|
|
||
| rule stayHealthy(env e, method f, calldataarg args) filtered { f -> f.selector != sig:liquidate(Midnight.Obligation, uint256, uint256, uint256, address, bytes).selector && f.selector != sig:take(uint256, address, address, bytes, address, Midnight.Offer, Midnight.Signature, bytes32, bytes32[]).selector } { |
There was a problem hiding this comment.
it's not clear to me what prevents us from writing it as a strong invariant
There was a problem hiding this comment.
One is Aesthetics: stating the strong invariant "user is always healthy" feels wrong. Of course, it only holds if price doesn't change. It would also be an invariant that you cannot just require, as this would be unsound.
The other is that this would make splitting the cases for liquidate much harder.
Finally, the proof currently depends on delaying the invariant check before the callbacks, by using the auxiliary ghost variable. The reason we need that is that we have to require our axioms before the assert, but we cannot require them before liquidate (or we would need to compute seizedAssets/repaidDebt in CVL before). Writing it as a strong invariant would immediately assert the invariant before the callbacks and thus before the axioms are required.
There was a problem hiding this comment.
we could have had this one be a strong invariant and avoid this, but the liquidation one be a weak invariant. doesn't matter that much anyway
|
@codex review |
![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: adc359c6e7
ℹ️ 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".
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 2d91b6720b
ℹ️ 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".
The BitmapSummaries now defines only the summaries, nothing else. The invariant is proved in CollateralBitmap and the file now uses the summaries instead of bitprecise reasoning.
Use bitmap summaries in collateralbitmap
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: d775dd2500
ℹ️ 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".
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 8e20a3e842
ℹ️ 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".
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 91f59e5cd6
ℹ️ 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".
5 participants
This adds a new rule that isHealthy for some particular obligation,id, and user is preserved. The callbacks are summarized and they check that isHealthy() also holds when giving control to the callbacks. They then allow arbitrary state change as long as isHealthy() holds on return.
There are some manual struct copies, because the CVL language cannot store the obligation in ghost variables. Also some interesting assumptions like that lltv is not too high (I got a counterexample in liquidate without the assumption).
corresponding thread