Changes from my Code Review.#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 👍 / 👎.
1 participant
I'm still investigating why one require->assert change leads to timeout. Reverted that change for now.