Feat/blue X pa with on-demand reallocation

[bhargavbh]

alternate approach where reallocations are executed only as necessitated by the blue operation

[chatgpt-codex-connector]

💡 Codex Review

bundles/src/blue/BlueBundlesV1.sol

Line 78 in 2339786

uint256 nativeCollateralAssets = msg.value - maxNativePenalty;

Separate collateral from a decreasing penalty budget

If an allocator lowers any native penalty after this transaction is constructed, msg.value still contains the old quote while totalNativePenalty returns the lower current total, so the difference is assigned to nativeCollateralAssets. pullOrWrapNative then requires that difference to equal the entire collateral amount, causing both ERC20- and native-collateral transactions to revert instead of refunding the reduced penalty; use an explicit native-collateral amount or penalty budget so excess value remains refundable.

---

bundles/src/blue/BlueBundlesV1.sol

Line 67 in 2339786

PublicReallocation[] memory reallocations,

Update the CVL calls for the reallocation argument

In the checked certora/confs/NoResidue.conf suite, NoResidue.spec lines 116 and 129 still invoke the old blueBundlesV1Withdraw and blueBundlesV1SupplyCollateralAndBorrow arities. Adding this array parameter means Certora can no longer resolve those calls, so the pull-request verification job reaches certoraRun and fails before proving the residue rules; add a PublicReallocation[] rule parameter, pass it at both call sites, and model the allocator calls as needed.

AGENTS.md reference: AGENTS.md:L5-L6

ℹ️ 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".

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: b508adefed

ℹ️ 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".

[chatgpt-codex-connector]

Pass reallocations to the NoResidue rules

When the Certora job runs, supplyCollateralAndBorrowPreservesBalance in certora/specs/NoResidue.spec:129 still invokes this entry point without its PublicReallocation[] argument; the withdraw rule at line 116 has the same stale arity. These calls cannot resolve to the Solidity ABI signatures, so NoResidue.conf errors before verifying this new native-refund path. Add reallocation arrays to both rules and pass them into the calls.

AGENTS.md reference: AGENTS.md:L77-L77

Useful? React with 👍 / 👎.