[Certora] drop callback/token summaries#665
Conversation
Stacked on #645.
![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: 59eb0fed1e
ℹ️ 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".
Adjust scope per feedback: callback-time healthiness no longer matters.
prd-carapulse
Bot
changed the title
Per feedback, stop caring about healthiness during callbacks and simplify the proof accordingly.
prd-carapulse
Bot
changed the title
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 840dd2409e
ℹ️ 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".
Restore callback/token havoc modeling while keeping take inside the generic stayHealthy rule.
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: c931cac7ad
ℹ️ 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".
Per feedback, remove callback/token summaries entirely from Healthiness.
prd-carapulse
Bot
changed the title
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 035ad4133d
ℹ️ 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".
| "files": [ | ||
| "certora/helpers/MidnightWrapper.sol", | ||
| "certora/helpers/Havoc.sol" | ||
| "certora/helpers/MidnightWrapper.sol" |
There was a problem hiding this comment.
Fresh evidence in this commit: Healthiness.conf now removes certora/helpers/Havoc.sol, and the Healthiness.spec methods block no longer defines _.on*/_.transfer* summaries, so callback and token-transfer side effects are no longer modeled as reentrant behavior. In src/Midnight.sol, untrusted external hooks are invoked in take, repay, liquidate, and flashLoan; if those effects are excluded from the model, this proof can pass while missing borrower-health regressions that are only reachable through callback/token reentry.
Useful? React with 👍 / 👎.
MathisGD
changed the title
Fix failing Healthiness proof by excluding tracked take buyers from the generic stayHealthy rule.
prd-carapulse
Bot
changed the title
MathisGD
changed the title
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 95033d95bf
ℹ️ 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.
stayHealthyTakeOtherBorrower explicitly excludes cases where takeBuyer(taker, offer) == globalBorrower, and take is also excluded from the generic stayHealthy rule, so there is no remaining rule that checks healthiness when the tracked borrower is the buyer on the tracked obligation. This creates a concrete verification coverage gap for buyer-side take paths, allowing buyer-accounting regressions to evade this spec.
Useful? React with 👍 / 👎.
Restrict the same-seller Healthiness rule to fresh take entries where the tracked seller is not already transiently liquidation-locked. Stacked on #645.
|
see #679 |
1 participant
Summary
Healthiness.spectakeseller vs other-borrower split so buyer cases are not over-claimed by the generic ruleHavochelper fromHealthiness.conf