test: add max normal-mode liquidation Certora proof#969
test: add max normal-mode liquidation Certora proof#969prd-carapulse[bot] wants to merge 1 commit into
Conversation
Add Certora coverage for the requested normal-mode max liquidation input and same-collateral follow-up revert behavior.
![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: 61f30a09a3
ℹ️ 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".
| require badDebt <= debtOf(id, borrower), "bad debt is bounded by debt"; | ||
| require debtAfterBadDebt == debtOf(id, borrower) - badDebt, "debt after bad debt matches prestate"; | ||
| require badDebt == 0 || (totalUnits(id) > 0 && totalUnits(id) >= badDebt), "market can realize bad debt"; | ||
| require to_mathint(withdrawable(id)) + previewRepaid <= max_uint128, "withdrawable can increase by repayment"; |
There was a problem hiding this comment.
When the selector takes the full-seize branch, previewRepaid is the call input and remains zero, but liquidate recomputes repaidUnits from seizedAssets and then adds that amount to _marketState.withdrawable (src/Midnight.sol lines 649-675). As written, a state with withdrawable(id) near uint128.max can satisfy this setup even though the first liquidation reverts from the withdrawable addition overflow; constrain the full-seize branch with to_mathint(withdrawable(id)) + fullSeizeRepaid <= max_uint128 or return/check the actual repayment.
Useful? React with 👍 / 👎.
| uint256 lifTimesLltv = type(uint256).max; | ||
| if (lltv == 0 || lif <= type(uint256).max / lltv) lifTimesLltv = lif * lltv; | ||
| if (originalDebt > maxDebt && lifTimesLltv < WAD * WAD) { | ||
| maxRepaid = (originalDebt - maxDebt).mulDivUp(WAD * WAD, WAD * WAD - lifTimesLltv); |
There was a problem hiding this comment.
In states with badDebt > 0, the real liquidate path first subtracts bad debt from _position.debt and then computes the normal-mode RCF cap from that reduced debt (src/Midnight.sol lines 626-660). This preview uses originalDebt, so it can overstate maxRepaid and choose a repayment/full-seize input that is not actually allowed by the contract's RCF check; use debtAfterBadDebt - maxDebt here to mirror the implementation.
Useful? React with 👍 / 👎.
1 participant
Summary
MaxNormalModeLiquidation.specand.conffor the requested normal-mode max-liquidation proof.normalModeMaxLiquidationPreviewto the Certora wrapper so the spec can mirror the liquidation pre-loop and requested amount selector.certora/README.md.Proof scope
maxRepaidis belowmarket.rcfThreshold, liquidate withseizedAssets = collateral;repaidUnits = min(maxRepaid, debtAfterBadDebt).Request Context
Test Plan
forge fmt --check certora/helpers/MidnightWrapper.soljq < certora/confs/MaxNormalModeLiquidation.confcertoraCVLFormatter certora/specs/MaxNormalModeLiquidation.specforge buildcertoraRun certora/confs/MaxNormalModeLiquidation.conf --compilation_steps_onlycertoraRun certora/confs/Healthiness.conf --compilation_steps_only