[Certora] liquidation liveness refactor#1017
Conversation
Make the price/lif/lltv accessors a definition
This leads to timeouts
![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: 9e0d0411d8
ℹ️ 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".
| definition ORACLE_PRICE_SCALE() returns uint256 = 10 ^ 36; | ||
|
|
||
|
|
||
| definition getPrice(uint256 collateralIndex, Midnight.CollateralParams[] params) returns uint256 = |
There was a problem hiding this comment.
This makes LiquidateLiveness.spec unloadable: Certora documents definitions as taking primitive arguments, but this new helper takes Midnight.CollateralParams[], a dynamic struct array. The same pattern is used by the two helpers below, so the liveness rules will fail before verification starts; keep the original inline ternaries or use a CVL function/primitive helper instead.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
It works in my tests. Maybe this is a new feature?
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: f00014c68c
ℹ️ 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".
| // maxRepaid (RCF check) = mulDivUp(debtAfter - maxDebt, WAD*WAD, WAD*WAD - lif*lltv), lif = maxLif here. | ||
| // Reconstructed bit-for-bit so the bound matches the RCF check exactly; denominator > 0 and debtAfter >= maxDebt from lowLltvScaffolding. | ||
| mathint maxRepaid = ghostMulDivUp(assert_uint256(debtAfter - maxDebt), assert_uint256(WAD() * WAD()), assert_uint256(WAD() * WAD() - maxLif * lltv)); | ||
| assert maxRepaid > 0, "it's possible to repay at least one unit"; |
There was a problem hiding this comment.
This assertion does not actually prevent the low-LLTV repay rule from becoming vacuous for the later requires: maxRepaid > 0 can hold while every positive repaidUnits is pruned by the collateral-fit guard. For example, with one active collateral unit priced below ORACLE_PRICE_SCALE, maxRepaid can be positive, but repaidUnits = 1 computes more seized collateral than the borrower has, so all paths are eliminated after this point. If the intent is to prove the safe interval is non-empty, add a satisfy/sanity check or assert a concrete amount also satisfies the debt and collateral guards.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
We may prove maxRepaid >= debtAfter - maxDebt. Maybe that is useful.
lilCertora
left a comment
lilCertora
left a comment
There was a problem hiding this comment.
this is nicer and easier to read , thanks
QGarchery
changed the title
| uint128 collatJ = collateral(id, borrower, collateralIndex); | ||
| require maxLifJ * lltvJ <= WAD() * (WAD() - 1), "maxLif*lltv <= WAD*(WAD-1) (lifTimesLltvStrictBound) => WAD*WAD - maxLif*lltv >= WAD >= 1"; | ||
| assert maxLifJ * lltvJ <= WAD() * (WAD() - 1), "maxLif*lltv <= WAD*(WAD-1) (lifTimesLltvStrictBound) => WAD*WAD - maxLif*lltv >= WAD >= 1"; | ||
| require ghostMulDivUp(ghostMulDivUp(collatJ, priceJ, ORACLE_PRICE_SCALE()), WAD(), maxLifJ) > ghostMulDivDown(ghostMulDivDown(collatJ, priceJ, ORACLE_PRICE_SCALE()), lltvJ, WAD()), "recoveryJ > maxDebtContribJ (seized lltv < WAD, collatJ*priceJ >= ORACLE_PRICE_SCALE)"; |
There was a problem hiding this comment.
If I replace this require with assert, the rule times out in sanity check. At least in multi-assert-mode, the rule goes through except for the vacuity check.
2 participants
I'm still investigating why one require->assert change leads to timeout. Reverted that change for now.