feat(certora): verify Blue net amount inversion - #120
feat(certora): verify Blue net amount inversion#120prd-carapulse[bot] wants to merge 12 commits into
Conversation
Add Certora rules for the documented penalty-aware net amount formula on withdraw and supplyCollateralAndBorrow. Co-authored-by: Bhargav <40268131+bhargavbh@users.noreply.github.com>
Apply Certora CVL formatter-compatible spacing and avoid unsupported loop syntax in the rule helpers. Co-authored-by: Bhargav <40268131+bhargavbh@users.noreply.github.com>
![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: b253eb02eb
ℹ️ 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".
Model allocator penalty transfers, native wrapping, caller/referrer aliasing, and full-precision gross-up arithmetic. Canonicalize the Certora config with jq. Co-authored-by: Bhargav <40268131+bhargavbh@users.noreply.github.com>
Replace unsupported compound assignments in the bounded penalty calculation. Co-authored-by: Bhargav <40268131+bhargavbh@users.noreply.github.com>
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: c58388c1f0
ℹ️ 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".
| if (d == 0) revert(); | ||
| mathint numerator = a * b; | ||
| mathint result = numerator / d; | ||
| assert result >= 0 && result <= max_uint256; |
There was a problem hiding this comment.
When targetNet is large and referralFeePct > 0—for example, targetNet == max_uint256 and referralFeePct == WAD() - 1—the quotient exceeds max_uint256, so this assertion gives both rules a counterexample before either entrypoint is called. Fresh evidence after the earlier review is that the revised full-precision implementation still asserts quotient representability; the real helper would revert when the result cannot fit, so guard this case with revert/require before require_uint256 instead.
AGENTS.md reference: AGENTS.md:L55-L56
Useful? React with 👍 / 👎.
| require reallocations.length > 0 => reallocations[0].vault != currentContract, "bundler is not a vault"; | ||
| require reallocations.length > 1 => reallocations[1].vault != currentContract, "bundler is not a vault"; | ||
| require reallocations.length > 2 => reallocations[2].vault != currentContract, "bundler is not a vault"; |
There was a problem hiding this comment.
When any reallocations[i].vault == e.msg.sender and its penalty is nonzero, the allocator donates that penalty to the vault, and cvlSafeTransferFrom records it in the same recipientBalance bucket as the final proceeds; the asserted delta is therefore targetNet + penalty, so both rules counterexample because symbolic addresses may coincide. Require every modeled vault to differ from e.msg.sender, or track only the final proceeds transfer separately.
AGENTS.md reference: AGENTS.md:L27-L30
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 68b23179ae
ℹ️ 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".
| } | ||
|
|
||
| function reallocationsAssumptions(BlueBundlesV1.PublicAllocations[] reallocations, address recipient) { | ||
| require reallocations.length <= 3, "loop bound"; |
There was a problem hiding this comment.
When a caller supplies four or more reallocations—a supported input because executePublicAllocations iterates the full dynamic array—this requirement eliminates the trace before either assertion. Consequently, the proof cannot detect an aggregation or conservation regression that affects later elements; prove the loop for arbitrary lengths or add coverage beyond this bound and explicitly document the remaining limitation.
AGENTS.md reference: AGENTS.md:L10-L11
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: bfc491b10a
ℹ️ 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".
| function _.deposit() external with(env e) => summaryWrapNative(calledContract, e.msg.value) expect void; | ||
| // The public allocator charges the caller mulDivUp(assets, penalty, WAD) of the destination | ||
| // loan token and sends it to the vault, and moves no other token of the caller. Proven of the | ||
| // implementation by BluePublicAllocatorPenalty.spec. Its revert conditions are dropped, which |
There was a problem hiding this comment.
The soundness justification for these handwritten call summaries names BluePublicAllocatorPenalty.spec, but a repo-wide tracked-file and history search finds no such spec. Consequently, CI never checks the premise that the allocator transfers exactly this token and amount; because CVL substitutes the summary without examining the Solidity implementation, allocator drift could leave these net-amount proofs passing unsoundly. Add the cited spec or otherwise verify and maintain this summary.
AGENTS.md reference: AGENTS.md:L50-L50
Useful? React with 👍 / 👎.
| require referralFeePct < WAD(); | ||
| reallocationsAssumptions(reallocations, e.msg.sender); | ||
|
|
||
| mathint penaltyAssets = sumPenaltyAssets(reallocations); |
There was a problem hiding this comment.
Neither main rule requires a reallocation or a nonzero penaltyAssets, so a zero-length array is feasible and follows the direct, non-flash-loan path already covered by the dedicated WithoutReallocations rules. Basic sanity can therefore mark these rules non-vacuous even if every nonzero-penalty callback trace is pruned, leaving the advertised penalty behavior unchecked; require penaltyAssets > 0 after this calculation in both main rules, or add an equivalent targeted sanity condition.
AGENTS.md reference: AGENTS.md:L10-L11
Useful? React with 👍 / 👎.
…prover performance
1 participant
Why
PR #117 added runtime fuzz coverage for the penalty-aware net amount formula. A Certora property makes the same invariant hold for all modeled inputs and guards both entrypoints against future arithmetic regressions.
What changed
BlueNetAmountInvertibility.specwith rules forblueBundlesV1WithdrawandblueBundlesV1SupplyCollateralAndBorrow.NoResidue-style balance summaries.Soundness boundary
The proof is scoped to the existing summary model: successful asset-based Morpho operations, no unsolicited token donations/callback behavior, and public-allocator penalty accounting represented by the shared
mulDivUpsummary. It proves the arithmetic inversion and bundler balance conservation under those explicit assumptions; it is not a full concrete Morpho/public-allocator integration proof.Verification
python3 -m json.tool.forge buildwas attempted but blocked while Foundry tried to install Solidity 0.8.28 fromhttps://binaries.soliditylang.org/linux-amd64/list.json; the executor returnedtunnel error: unsuccessful.Requested by: <@U09R4EQ040> | bhargav