[Certora] add strong stayNotLiquidatable spec#661
Conversation
![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: f741be803f
ℹ️ 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".
| function summaryToId(Midnight.Obligation obligation, uint256 chainId, address morpho) returns (bytes32) { | ||
| bytes32 id; | ||
| if (equalsGlobalObligation(obligation) && morpho == currentContract) { | ||
| require id == globalId, "toId() is deterministic"; |
There was a problem hiding this comment.
IdLib.toId in the Solidity code includes chainId in the hash, but this summary enforces determinism/injectivity without considering chainId. In any proof path where the same obligation is evaluated with different chain IDs, this collapses distinct IDs into the same globalId, which can hide aliasing/collision behaviors and make the verification result less faithful to on-chain semantics.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 8600b795e7
ℹ️ 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 globalObligationCollateralLength <= 3, "too many collateralParams for the spec to handle"; | ||
|
|
||
| Midnight.Obligation globalObligation = getGlobalObligation(); | ||
| require (takeSeller(taker, offer) != globalBorrower && takeBuyer(taker, offer) != globalBorrower) || !equalsGlobalObligation(offer.obligation), "borrower is not a take participant on the tracked obligation"; |
There was a problem hiding this comment.
stayNotLiquidatableTakeOtherBorrower excludes both takeSeller and takeBuyer, and stayNotLiquidatableTakeSameSeller only handles the seller branch. That leaves the case where takeBuyer(taker, offer) == globalBorrower on the tracked obligation unverified, so regressions that make the buyer liquidatable during callbacks or by the end of take would not be detected by this spec.
Useful? React with 👍 / 👎.
| // This variable is set to false whenever not liquidatable is violated before a callback. Initially we set it to true. | ||
| notLiquidatableBeforeCallback = true; | ||
|
|
||
| require globalObligationCollateralLength <= 3, "too many collateralParams for the spec to handle"; |
There was a problem hiding this comment.
Each rule gates execution with globalObligationCollateralLength <= 3, but the protocol accepts obligations with many more collateral params. This means the spec’s “stays not liquidatable” guarantee is only checked for a bounded subset of valid obligations, so bugs that manifest with 4+ collaterals can pass unnoticed.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: b56c51ca2f
ℹ️ 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 globalObligationCollateralLength <= 3, "too many collateralParams for the spec to handle"; | ||
|
|
||
| Midnight.Obligation globalObligation = getGlobalObligation(); | ||
| require borrower != globalBorrower || !equalsGlobalObligation(obligation), "borrower or obligation differs"; |
There was a problem hiding this comment.
stayNotLiquidatableLiquidateOtherBorrower excludes the borrower == globalBorrower && equalsGlobalObligation(obligation) path, and stayNotLiquidatable filters liquidate out entirely, so the spec never checks successful liquidation of the tracked borrower on the tracked obligation. This leaves a blind spot where regressions in liquidation guards (for example, lock handling or the liquidatable predicate) could allow liquidating a borrower that was assumed not liquidatable without any rule failing.
Useful? React with 👍 / 👎.
MathisGD
changed the title
1 participant
Summary
NotLiquidatableCertora spec with a strong callback-level predicateliquidatable := !liquidationLocked(id, user) && (!isHealthy(...) || postMaturity)take/ non-liquidateentrypointstakewhen the tracked borrower is the seller on the tracked obligationtakewhen the tracked borrower is not a participant on the tracked obligation (or the obligation differs)supplyCollateralpreserves non-liquidatabilitytakeproof with the runtimetakepostcondition by checkingisHealthydirectlyHealthiness.spectake-proof fix on this branch so the shared Certora matrix is green when the PR is tested independentlyTest Plan
Stacked on #645. Parallel to #659.