certora: model native wrapping in NoResidue#87
Merged
Conversation
The wrap-native change makes BlueBundlesV1 mint WNative to the bundler via WNative.deposit on native supply/repay and burn it via WNative.withdraw when refunding the unused native remainder. NoResidue only summarized ERC20 transfers and Morpho methods, so these calls left the persistent bundlerBalance ghost stale on native paths and the no-residue rules compared against a wrong balance. Add deposit/withdraw summaries that credit/debit bundlerBalance by the wrapped/unwrapped amount, keeping the no-residue rules exact on native paths instead of restricting them to msg.value == 0.
QGarchery
marked this pull request as ready for review
July 24, 2026 16:25
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Requested by Quentin Garchery · Slack thread
Stacked on top of #82 (base branch =
wrap-native).Before
The
certora/specs/NoResidue.specsuite only modeled ERC20 transfers and Morpho methods. On the new native paths added in #82 (wheremsg.value > 0),BlueBundlesV1mints WNative to the bundler viaWNative.depositand burns it viaWNative.withdrawwhen refunding the unused remainder. Those calls were left unsummarized, so the persistentbundlerBalanceghost stayed stale while the actual token balance moved. The no-residue rules therefore compared against a wrong balance and the suite would fail on native executions (unless the rules were narrowed tomsg.value == 0, which would drop native coverage entirely).After
The no-residue rules stay exact on the native paths too: wrapping and then supplying/repaying (and refunding any remainder) is proven to leave zero residue of every token, without excluding
msg.value > 0executions.How
In
certora/specs/NoResidue.spec, added two exact-signature summaries in themethodsblock for the WNative interface (src/libraries/interfaces/IWNative.sol), used byTokenLib.pullOrWrapNativeand the native refund inBlueBundlesV1:deposit()->summaryWrapNative(calledContract, e.msg.value)creditsbundlerBalanceby the forwarded native value (WNative minted to the bundler).withdraw(uint256)->summaryUnwrapNative(calledContract, amount)debitsbundlerBalanceby the unwrapped amount (WNative burned; the returned native is not a tracked token).These mirror the existing ERC20/Morpho summary style and keep the persistent
bundlerBalanceghost in sync across native wrap/unwrap.Addresses review comment: #82 (comment)