[Certora] liquidation liveness#834
Conversation
Co-authored-by: Quentin Garchery <garchery.quentin@gmail.com> Signed-off-by: lilCertora <lilian@certora.com>
![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: cd6315e477
ℹ️ 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: bc11ba8549
ℹ️ 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: 729f46d510
ℹ️ 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: b926c65cce
ℹ️ 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".
| mathint recovery0 = ghostMulDivUp(ghostMulDivUp(collateral(id, borrower, 0), ghostPrice(market.collateralParams[0].oracle), ORACLE_PRICE_SCALE()), WAD(), market.collateralParams[0].maxLif); | ||
| mathint recovery1 = ghostMulDivUp(ghostMulDivUp(collateral(id, borrower, 1), ghostPrice(market.collateralParams[1].oracle), ORACLE_PRICE_SCALE()), WAD(), market.collateralParams[1].maxLif); | ||
| mathint recovery2 = ghostMulDivUp(ghostMulDivUp(collateral(id, borrower, 2), ghostPrice(market.collateralParams[2].oracle), ORACLE_PRICE_SCALE()), WAD(), market.collateralParams[2].maxLif); |
There was a problem hiding this comment.
When a collateral price is below ORACLE_PRICE_SCALE, the current ghostMulDivUp axioms can model mulDivUp(collateral, price, ORACLE_PRICE_SCALE) as any value up to the full collateral amount, far above the real ceil result. Separate from the earlier RCF over-approximation thread, this value feeds the bad-debt recovery here, so debtAfterBadDebt can equal _debt even when the real liquidate would realize bad debt; then the badDebtCanBeLiquidated implication is skipped instead of checking the promised debt drop. Add the mulDivUpTightBound/upper-bound axiom before using this recovery reconstruction.
Useful? React with 👍 / 👎.
|
I replace some require by assert here: #1017. There are still two requires left, which should in principle also be provable. Otherwise, that looks good. I think all cases are covered except one minor special case: You can liquidate more than maxRepaid if only dust ist left. I don't think that is important enough. |
| } | ||
|
|
||
| function summaryMulDivDown(uint256 x, uint256 y, uint256 d) returns uint256 { | ||
| if (d == 0) { |
There was a problem hiding this comment.
An assumption we are making here is that there is no overflow, I think it's worth mentioning
| uint256 lltv = market.collateralParams[i].lltv; | ||
| uint256 maxLif = market.collateralParams[i].maxLif; | ||
|
|
||
| require lltv > 0 && lltv <= WAD(), "lltv in (0, WAD] for a created market (in CreatedMarkets.spec)"; |
There was a problem hiding this comment.
it does not prove that lltv > 0 right ?
What breaks if we don't have this assumption ?
|
|
||
| require lltv > 0 && lltv <= WAD(), "lltv in (0, WAD] for a created market (in CreatedMarkets.spec)"; | ||
| require maxLif >= WAD(), "maxLif >= WAD (maxLifIsAtLeastWad)"; | ||
| require lltv < WAD() => lltv * maxLif <= WAD() * (WAD() - 1), "lltv < WAD => lltv*maxLif <= WAD*(WAD-1) (lifTimesLltvStrictBound)"; |
There was a problem hiding this comment.
we don't have the lifTimesLltvStrictBound rule in main anymore, we should add it back (feasible because we kept the invariant liquidationCursor < WAD)
| threeCollatSetup(e, market, id, borrower); | ||
| require collateralIndex == 0 || collateralIndex == 1 || collateralIndex == 2, "seized index in {0,1,2} (<= loop_iter)"; | ||
| require summaryGetBit(collateralBitmap(id, borrower), collateralIndex), "the seized collateral is active"; | ||
| require getPrice(collateralIndex, market.collateralParams) > 0, "the seized collateral is priced (LIVENESS)"; |
There was a problem hiding this comment.
this should be added to the list of assumptions at the top
| uint256 maxLifJ = getMaxLif(collateralIndex, market.collateralParams); | ||
| uint256 priceJ = getPrice(collateralIndex, market.collateralParams); | ||
| uint128 collatJ = collateral(id, borrower, collateralIndex); | ||
| assert maxLifJ * lltvJ <= WAD() * (WAD() - 1), "maxLif*lltv <= WAD*(WAD-1) (lifTimesLltvStrictBound) => WAD*WAD - maxLif*lltv >= WAD >= 1"; |
There was a problem hiding this comment.
same, lifTimesLltvStrictBound doesn't exist anymore, although here it's an assert. This is a bit suspicious because you need to know that the liquidation cursor is < WAD
3 participants
No description provided.