From 053c06331aa15f55e46ec65bbc9d948c50154e3c Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Thu, 23 Jul 2026 17:43:36 +0200 Subject: [PATCH 01/11] wrap native for supply collateral --- src/blue/BlueBundlesV1.sol | 5 +- src/blue/interfaces/IBlueBundlesV1.sol | 2 +- src/libraries/TokenLib.sol | 14 +++++ test/BlueBundlesTest.sol | 84 +++++++++++++++++++++++++- 4 files changed, 101 insertions(+), 4 deletions(-) diff --git a/src/blue/BlueBundlesV1.sol b/src/blue/BlueBundlesV1.sol index 084dd42..a44dd90 100644 --- a/src/blue/BlueBundlesV1.sol +++ b/src/blue/BlueBundlesV1.sol @@ -39,6 +39,7 @@ contract BlueBundlesV1 is IBlueBundlesV1, IMorphoRepayCallback { /// EXTERNAL /// /// @dev Pulls collateralAssets of marketParams.collateralToken from msg.sender (optionally via ERC-2612 or Permit2), supplies it as collateral on Blue for msg.sender, then borrows borrowAssets of the loan token on behalf of msg.sender. + /// @dev When native tokens are sent, they are wrapped into marketParams.collateralToken (which must be the wrapped-native token) instead of pulling. /// @dev The msg.sender must have authorized this contract on Blue, beforehand or via signedAuthorization. /// @dev referralFeeAssets = borrowAssets * referralFeePct / WAD; net = borrowAssets - referralFeeAssets. /// @dev To receive an amount W, pass borrowAssets = floor(W * WAD / (WAD - referralFeePct)). @@ -55,12 +56,12 @@ contract BlueBundlesV1 is IBlueBundlesV1, IMorphoRepayCallback { uint256 referralFeePct, address referralFeeRecipient, uint256 deadline - ) external { + ) external payable { require(block.timestamp <= deadline, DeadlinePassed()); require(referralFeePct < WAD, PctExceeded()); setAuthorizationWithSig(signedAuthorization); - TokenLib.pullToken(marketParams.collateralToken, msg.sender, collateralAssets, collateralPermit); + TokenLib.pullOrWrapNative(marketParams.collateralToken, msg.sender, collateralAssets, collateralPermit); if (collateralAssets > 0) { TokenLib.forceApproveMax(marketParams.collateralToken, BLUE); IMorpho(BLUE).supplyCollateral(marketParams, collateralAssets, msg.sender, ""); diff --git a/src/blue/interfaces/IBlueBundlesV1.sol b/src/blue/interfaces/IBlueBundlesV1.sol index 3f72846..8c586be 100644 --- a/src/blue/interfaces/IBlueBundlesV1.sol +++ b/src/blue/interfaces/IBlueBundlesV1.sol @@ -37,7 +37,7 @@ interface IBlueBundlesV1 { uint256 referralFeePct, address referralFeeRecipient, uint256 deadline - ) external; + ) external payable; function blueBundlesV1RepayAndWithdrawCollateral( MarketParams memory marketParams, diff --git a/src/libraries/TokenLib.sol b/src/libraries/TokenLib.sol index ed1c416..c71d0a6 100644 --- a/src/libraries/TokenLib.sol +++ b/src/libraries/TokenLib.sol @@ -4,6 +4,7 @@ pragma solidity >=0.8.0; import {SafeTransferLib} from "../../lib/midnight/src/libraries/SafeTransferLib.sol"; import {IERC20Permit} from "./interfaces/IERC20Permit.sol"; +import {IWNative} from "./interfaces/IWNative.sol"; import {IPermit2, ISignatureTransfer} from "../../lib/permit2/src/interfaces/IPermit2.sol"; enum PermitKind { @@ -19,6 +20,8 @@ struct TokenPermit { library TokenLib { error ApproveReturnedFalse(); + error BothNativeAndToken(); + error InconsistentAmountAndNative(); /// @dev Canonical Permit2 singleton. address constant PERMIT2 = 0x000000000022D473030F116dDEE9F6B43aC78BA3; @@ -66,4 +69,15 @@ library TokenLib { SafeTransferLib.safeTransferFrom(token, from, address(this), amount); } } + + /// @dev Same as pullToken, but when native tokens are sent with the call, instead wraps msg.value into token. + function pullOrWrapNative(address token, address from, uint256 amount, TokenPermit memory permit) internal { + if (msg.value > 0) { + require(permit.kind == PermitKind.None, BothNativeAndToken()); + require(amount == msg.value, InconsistentAmountAndNative()); + IWNative(token).deposit{value: msg.value}(); + } else { + pullToken(token, from, amount, permit); + } + } } diff --git a/test/BlueBundlesTest.sol b/test/BlueBundlesTest.sol index 1cc383a..02ae57c 100644 --- a/test/BlueBundlesTest.sol +++ b/test/BlueBundlesTest.sol @@ -12,9 +12,10 @@ import {ORACLE_PRICE_SCALE, AUTHORIZATION_TYPEHASH} from "../lib/morpho-blue/src import {OracleMock} from "../lib/morpho-blue/src/mocks/OracleMock.sol"; import {WAD} from "../lib/midnight/src/libraries/ConstantsLib.sol"; import {ERC20Permit} from "../lib/midnight/test/erc20s/ERC20Permit.sol"; +import {ERC20} from "../lib/midnight/test/erc20s/ERC20.sol"; import {BlueBundlesV1} from "../src/blue/BlueBundlesV1.sol"; import {IBlueBundlesV1, SignedAuthorization} from "../src/blue/interfaces/IBlueBundlesV1.sol"; -import {TokenPermit} from "../src/libraries/TokenLib.sol"; +import {TokenLib, TokenPermit, PermitKind} from "../src/libraries/TokenLib.sol"; contract BlueBundlesTest is Test { using MarketParamsLib for MarketParams; @@ -474,6 +475,77 @@ contract BlueBundlesTest is Test { assertEq(loanToken.balanceOf(address(blueBundles)), 0, "bundler residual"); } + /// @dev Sending native tokens (msg.value) wraps them into the collateral token and supplies them as collateral. + function testSupplyCollateralAndBorrowWrapNative(uint256 borrowAssets) public { + borrowAssets = bound(borrowAssets, 1, 1e30); + uint256 collateral = _collateralFor(borrowAssets); + + // Market whose collateral token is the wrapped-native token. + WETHMock weth = new WETHMock(); + MarketParams memory wethMarketParams = MarketParams({ + loanToken: address(loanToken), + collateralToken: address(weth), + oracle: address(oracle), + irm: address(0), + lltv: LLTV + }); + morpho.createMarket(wethMarketParams); + Id wethId = wethMarketParams.id(); + + // Seed loan-side liquidity so the borrow can be served. + deal(address(loanToken), supplier, LIQUIDITY); + vm.prank(supplier); + morpho.supply(wethMarketParams, LIQUIDITY, 0, supplier, ""); + + vm.deal(user, collateral); + // When native tokens are sent, collateralAssets must equal msg.value and no collateralPermit may be set. + vm.prank(user); + blueBundles.blueBundlesV1SupplyCollateralAndBorrow{value: collateral}( + wethMarketParams, + collateral, + borrowAssets, + 0, + WAD, + _noPermit(), + _noAuthSig(), + 0, + address(0), + block.timestamp + ); + + assertEq(morpho.collateral(wethId, user), collateral, "collateral"); + assertEq(morpho.expectedBorrowAssets(wethMarketParams, user), borrowAssets, "debt"); + assertEq(loanToken.balanceOf(user), borrowAssets, "user"); + assertEq(user.balance, 0, "user native residual"); + assertEq(address(blueBundles).balance, 0, "bundler native residual"); + assertEq(weth.balanceOf(address(blueBundles)), 0, "bundler wrapped residual"); + } + + /// @dev Sending native tokens together with a collateral permit reverts. + function testSupplyCollateralAndBorrowBothNativeAndToken() public { + uint256 collateral = _collateralFor(1e18); + vm.deal(user, collateral); + + TokenPermit memory permit = TokenPermit({kind: PermitKind.ERC2612, data: ""}); + vm.prank(user); + vm.expectRevert(TokenLib.BothNativeAndToken.selector); + blueBundles.blueBundlesV1SupplyCollateralAndBorrow{value: collateral}( + marketParams, collateral, 1e18, 0, WAD, permit, _noAuthSig(), 0, address(0), block.timestamp + ); + } + + /// @dev Sending native tokens with a collateral amount that does not match msg.value reverts. + function testSupplyCollateralAndBorrowInconsistentAmountAndNative() public { + uint256 collateral = _collateralFor(1e18); + vm.deal(user, collateral); + + vm.prank(user); + vm.expectRevert(TokenLib.InconsistentAmountAndNative.selector); + blueBundles.blueBundlesV1SupplyCollateralAndBorrow{value: collateral}( + marketParams, collateral + 1, 1e18, 0, WAD, _noPermit(), _noAuthSig(), 0, address(0), block.timestamp + ); + } + function testSupplyCollateralAndBorrowWithReferralFee(uint256 borrowAssets, uint256 referralFeePct) public { borrowAssets = bound(borrowAssets, 1, 1e30); referralFeePct = bound(referralFeePct, 0, WAD - 1); @@ -1348,3 +1420,13 @@ contract BlueBundlesTest is Test { ); } } + +/// @dev Minimal wrapped-native token: deposit() mints 1:1 for the native tokens sent. +contract WETHMock is ERC20 { + constructor() ERC20("Wrapped Ether", "WETH") {} + + function deposit() external payable { + balanceOf[msg.sender] += msg.value; + totalSupply += msg.value; + } +} From 53975ce415a700aba0588276b92c7a58e9034cfd Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Thu, 23 Jul 2026 18:31:53 +0200 Subject: [PATCH 02/11] add wrapped native everywhere --- src/blue/BlueBundlesV1.sol | 25 ++++-- src/blue/interfaces/IBlueBundlesV1.sol | 5 +- src/libraries/interfaces/IWNative.sol | 8 ++ src/vault/VaultBundlesV1.sol | 5 +- src/vault/interfaces/IVaultBundlesV1.sol | 2 +- test/BlueBundlesTest.sol | 103 +++++++++++++++++++++++ test/VaultBundlesTest.sol | 29 +++++++ 7 files changed, 165 insertions(+), 12 deletions(-) create mode 100644 src/libraries/interfaces/IWNative.sol diff --git a/src/blue/BlueBundlesV1.sol b/src/blue/BlueBundlesV1.sol index a44dd90..cee384b 100644 --- a/src/blue/BlueBundlesV1.sol +++ b/src/blue/BlueBundlesV1.sol @@ -4,6 +4,7 @@ pragma solidity 0.8.34; import {IBlueBundlesV1, SignedAuthorization} from "./interfaces/IBlueBundlesV1.sol"; import {TokenLib, TokenPermit} from "../libraries/TokenLib.sol"; +import {IWNative} from "../libraries/interfaces/IWNative.sol"; import { IMorpho, MarketParams, @@ -36,6 +37,9 @@ contract BlueBundlesV1 is IBlueBundlesV1, IMorphoRepayCallback { BLUE = _blue; } + /// @dev Receives the native tokens unwrapped from the wrapped-native token when reimbursing a native repay. + receive() external payable {} + /// EXTERNAL /// /// @dev Pulls collateralAssets of marketParams.collateralToken from msg.sender (optionally via ERC-2612 or Permit2), supplies it as collateral on Blue for msg.sender, then borrows borrowAssets of the loan token on behalf of msg.sender. @@ -80,6 +84,7 @@ contract BlueBundlesV1 is IBlueBundlesV1, IMorphoRepayCallback { } /// @dev Pulls maxRepayAssets from msg.sender, repays msg.sender's debt, reimburses the unused remainder at the end of the call, and withdraws collateral if collateralAssets > 0. + /// @dev When native tokens are sent, they are wrapped into marketParams.loanToken (which must be the wrapped-native token) instead of pulling, and the reimbursed remainder is unwrapped back to native. /// @dev The msg.sender must have authorized this contract on Blue, beforehand or via signedAuthorization, if some collateral is withdrawn. /// @dev Exactly one of repayAssets and repayShares should be non-zero: the debt is repaid by assets, or by shares. To close the full debt, pass msg.sender's full borrow shares as repayShares. /// @dev The fee is repaidAmount * referralFeePct / (WAD - referralFeePct). @@ -98,12 +103,12 @@ contract BlueBundlesV1 is IBlueBundlesV1, IMorphoRepayCallback { uint256 referralFeePct, address referralFeeRecipient, uint256 deadline - ) external { + ) external payable { require(block.timestamp <= deadline, DeadlinePassed()); require(referralFeePct < WAD, PctExceeded()); setAuthorizationWithSig(signedAuthorization); - TokenLib.pullToken(marketParams.loanToken, msg.sender, maxRepayAssets, loanTokenPermit); + TokenLib.pullOrWrapNative(marketParams.loanToken, msg.sender, maxRepayAssets, loanTokenPermit); TokenLib.forceApproveMax(marketParams.loanToken, BLUE); (repayAssets, repayShares) = IMorpho(BLUE).repay(marketParams, repayAssets, repayShares, msg.sender, ""); @@ -118,12 +123,18 @@ contract BlueBundlesV1 is IBlueBundlesV1, IMorphoRepayCallback { if (referralFeeAssets > 0) { SafeTransferLib.safeTransfer(marketParams.loanToken, referralFeeRecipient, referralFeeAssets); } - SafeTransferLib.safeTransfer( - marketParams.loanToken, msg.sender, maxRepayAssets - repayAssets - referralFeeAssets - ); + uint256 refund = maxRepayAssets - repayAssets - referralFeeAssets; + if (msg.value > 0) { + IWNative(marketParams.loanToken).withdraw(refund); + (bool success,) = msg.sender.call{value: refund}(""); + require(success, NativeTransferFailed()); + } else { + SafeTransferLib.safeTransfer(marketParams.loanToken, msg.sender, refund); + } } /// @dev Pulls assets from msg.sender (optionally via ERC-2612 or Permit2) and supplies them to the market for msg.sender. + /// @dev When native tokens are sent, they are wrapped into marketParams.loanToken (which must be the wrapped-native token) instead of pulling. /// @dev The referral fee is deducted from assets; the remainder is supplied to the market for msg.sender. /// @dev Fee = assets * referralFeePct / WAD; supplied = assets - fee. /// @dev maxSharePriceE27 upper-bounds the realized supply share price (supplied assets per share, scaled by 1e27). @@ -135,14 +146,14 @@ contract BlueBundlesV1 is IBlueBundlesV1, IMorphoRepayCallback { uint256 referralFeePct, address referralFeeRecipient, uint256 deadline - ) external { + ) external payable { require(block.timestamp <= deadline, DeadlinePassed()); require(referralFeePct < WAD, PctExceeded()); uint256 referralFeeAssets = assets.mulDivDown(referralFeePct, WAD); uint256 toSupply = assets - referralFeeAssets; - TokenLib.pullToken(marketParams.loanToken, msg.sender, assets, loanTokenPermit); + TokenLib.pullOrWrapNative(marketParams.loanToken, msg.sender, assets, loanTokenPermit); TokenLib.forceApproveMax(marketParams.loanToken, BLUE); (, uint256 suppliedShares) = IMorpho(BLUE).supply(marketParams, toSupply, 0, msg.sender, ""); diff --git a/src/blue/interfaces/IBlueBundlesV1.sol b/src/blue/interfaces/IBlueBundlesV1.sol index 8c586be..b6d90fa 100644 --- a/src/blue/interfaces/IBlueBundlesV1.sol +++ b/src/blue/interfaces/IBlueBundlesV1.sol @@ -18,6 +18,7 @@ interface IBlueBundlesV1 { error DeadlinePassed(); error InconsistentTokens(); error LtvExceeded(); + error NativeTransferFailed(); error PctExceeded(); error SlippageExceeded(); error UnauthorizedCallback(); @@ -52,7 +53,7 @@ interface IBlueBundlesV1 { uint256 referralFeePct, address referralFeeRecipient, uint256 deadline - ) external; + ) external payable; function blueBundlesV1Supply( MarketParams memory marketParams, @@ -62,7 +63,7 @@ interface IBlueBundlesV1 { uint256 referralFeePct, address referralFeeRecipient, uint256 deadline - ) external; + ) external payable; function blueBundlesV1Withdraw( MarketParams memory marketParams, diff --git a/src/libraries/interfaces/IWNative.sol b/src/libraries/interfaces/IWNative.sol new file mode 100644 index 0000000..a4e569e --- /dev/null +++ b/src/libraries/interfaces/IWNative.sol @@ -0,0 +1,8 @@ +// SPDX-License-Identifier: GPL-2.0-or-later +// Copyright (c) 2026 Morpho Association +pragma solidity >=0.8.0; + +interface IWNative { + function deposit() external payable; + function withdraw(uint256 amount) external; +} diff --git a/src/vault/VaultBundlesV1.sol b/src/vault/VaultBundlesV1.sol index 1977a0e..5776416 100644 --- a/src/vault/VaultBundlesV1.sol +++ b/src/vault/VaultBundlesV1.sol @@ -24,6 +24,7 @@ contract VaultBundlesV1 is IVaultBundlesV1 { /// EXTERNAL /// /// @dev Pulls assets of the vault asset from msg.sender (optionally via ERC-2612 or Permit2) and deposits them into vault. + /// @dev When native tokens are sent, they are wrapped into the vault asset (which must be the wrapped-native token) instead of pulling. /// @dev The referral fee is deducted from assets; the remainder is deposited into vault for msg.sender. /// @dev Fee = assets * referralFeePct / WAD; deposited = assets - fee. /// @dev maxSharePriceE27 upper-bounds the realized deposit share price (deposited assets per share, scaled by 1e27). @@ -35,7 +36,7 @@ contract VaultBundlesV1 is IVaultBundlesV1 { uint256 referralFeePct, address referralFeeRecipient, uint256 deadline - ) external { + ) external payable { require(block.timestamp <= deadline, DeadlinePassed()); require(referralFeePct < WAD, PctExceeded()); @@ -43,7 +44,7 @@ contract VaultBundlesV1 is IVaultBundlesV1 { uint256 toDeposit = assets - referralFeeAssets; address asset = IERC4626(vault).asset(); - TokenLib.pullToken(asset, msg.sender, assets, assetPermit); + TokenLib.pullOrWrapNative(asset, msg.sender, assets, assetPermit); TokenLib.forceApproveMax(asset, vault); uint256 shares = IERC4626(vault).deposit(toDeposit, msg.sender); diff --git a/src/vault/interfaces/IVaultBundlesV1.sol b/src/vault/interfaces/IVaultBundlesV1.sol index a7bc1bc..286bb76 100644 --- a/src/vault/interfaces/IVaultBundlesV1.sol +++ b/src/vault/interfaces/IVaultBundlesV1.sol @@ -32,7 +32,7 @@ interface IVaultBundlesV1 { uint256 referralFeePct, address referralFeeRecipient, uint256 deadline - ) external; + ) external payable; function vaultBundlesV1Withdraw( address vault, diff --git a/test/BlueBundlesTest.sol b/test/BlueBundlesTest.sol index 02ae57c..4154268 100644 --- a/test/BlueBundlesTest.sol +++ b/test/BlueBundlesTest.sol @@ -702,6 +702,75 @@ contract BlueBundlesTest is Test { assertEq(loanToken.balanceOf(address(blueBundles)), 0, "bundler residual"); } + /// @dev Sending native tokens (msg.value) wraps them into the loan token and repays msg.sender's debt. + function testRepayAndWithdrawCollateralWrapNative() public { + // Market whose loan token is the wrapped-native token. + WETHMock weth = new WETHMock(); + MarketParams memory wethMarketParams = MarketParams({ + loanToken: address(weth), + collateralToken: address(collateralToken), + oracle: address(oracle), + irm: address(0), + lltv: LLTV + }); + morpho.createMarket(wethMarketParams); + Id wethId = wethMarketParams.id(); + + uint256 borrowAssets = 100e18; + uint256 collateral = _collateralFor(borrowAssets); + + // Seed wrapped-native liquidity so the position can borrow. + vm.deal(supplier, LIQUIDITY); + vm.startPrank(supplier); + weth.deposit{value: LIQUIDITY}(); + weth.approve(address(morpho), type(uint256).max); + morpho.supply(wethMarketParams, LIQUIDITY, 0, supplier, ""); + vm.stopPrank(); + + // Open the user's borrow directly on Morpho. + deal(address(collateralToken), user, collateral); + vm.startPrank(user); + collateralToken.approve(address(morpho), type(uint256).max); + morpho.supplyCollateral(wethMarketParams, collateral, user, ""); + morpho.borrow(wethMarketParams, borrowAssets, 0, user, user); + vm.stopPrank(); + + // Discard the borrowed wrapped tokens; the user repays with native and the refund must come back as native. + deal(address(weth), user, 0); + + uint256 repayAssets = 40e18; + uint256 maxRepayAssets = 50e18; + // After repaying repayAssets, remaining debt is 60e18, needing 75e18 collateral (60/0.8) at 1:1 price. + uint256 withdrawCollateral = collateral - 75e18; + + vm.deal(user, maxRepayAssets); + // When native tokens are sent, maxRepayAssets must equal msg.value and no loanTokenPermit may be set. + vm.prank(user); + blueBundles.blueBundlesV1RepayAndWithdrawCollateral{value: maxRepayAssets}( + wethMarketParams, + repayAssets, + 0, + maxRepayAssets, + type(uint256).max, + withdrawCollateral, + WAD, + _noPermit(), + _noAuthSig(), + 0, + address(0), + block.timestamp + ); + + assertEq(morpho.expectedBorrowAssets(wethMarketParams, user), borrowAssets - repayAssets, "debt"); + assertEq(morpho.collateral(wethId, user), collateral - withdrawCollateral, "remaining collateral"); + assertEq(collateralToken.balanceOf(user), withdrawCollateral, "collateral to user"); + // The unused remainder is unwrapped and returned as native, not as the wrapped token. + assertEq(user.balance, maxRepayAssets - repayAssets, "native refund"); + assertEq(weth.balanceOf(user), 0, "no wrapped refund"); + assertEq(address(blueBundles).balance, 0, "bundler native residual"); + assertEq(weth.balanceOf(address(blueBundles)), 0, "bundler wrapped residual"); + } + /// @dev maxLtv caps the resulting LTV after a withdrawal: repaying 30e18 and withdrawing 100e18 leaves 70e18 /// debt against 100e18 collateral (LTV 0.7) — within the 0.8 LLTV Blue allows, but above a 0.6 maxLtv. function testRepayAndWithdrawCollateralLtvExceeded() public { @@ -987,6 +1056,34 @@ contract BlueBundlesTest is Test { assertEq(loanToken.balanceOf(address(blueBundles)), 0, "bundler residual"); } + /// @dev Sending native tokens (msg.value) wraps them into the loan token and supplies them to the market. + function testSupplyWrapNative(uint256 assets) public { + assets = bound(assets, 1, 1e30); + + // Market whose loan token is the wrapped-native token. + WETHMock weth = new WETHMock(); + MarketParams memory wethMarketParams = MarketParams({ + loanToken: address(weth), + collateralToken: address(collateralToken), + oracle: address(oracle), + irm: address(0), + lltv: LLTV + }); + morpho.createMarket(wethMarketParams); + + vm.deal(user, assets); + // When native tokens are sent, assets must equal msg.value and no loanTokenPermit may be set. + vm.prank(user); + blueBundles.blueBundlesV1Supply{value: assets}( + wethMarketParams, assets, type(uint256).max, _noPermit(), 0, address(0), block.timestamp + ); + + assertEq(morpho.expectedSupplyAssets(wethMarketParams, user), assets, "supply position"); + assertEq(user.balance, 0, "user native residual"); + assertEq(address(blueBundles).balance, 0, "bundler native residual"); + assertEq(weth.balanceOf(address(blueBundles)), 0, "bundler wrapped residual"); + } + /// WITHDRAW /// function testWithdraw(uint256 supplyAssets, uint256 withdrawAssets) public { @@ -1429,4 +1526,10 @@ contract WETHMock is ERC20 { balanceOf[msg.sender] += msg.value; totalSupply += msg.value; } + + function withdraw(uint256 amount) external { + balanceOf[msg.sender] -= amount; + totalSupply -= amount; + payable(msg.sender).transfer(amount); + } } diff --git a/test/VaultBundlesTest.sol b/test/VaultBundlesTest.sol index ee61c38..3162b83 100644 --- a/test/VaultBundlesTest.sol +++ b/test/VaultBundlesTest.sol @@ -225,6 +225,26 @@ contract VaultBundlesTest is Test { bundles.vaultBundlesV1Deposit(address(vaultV1), 1e18, RAY, noPermit, WAD, referralFeeRecipient, block.timestamp); } + /// @dev Sending native tokens (msg.value) wraps them into the vault asset and deposits them. + function testDepositWrapNative(uint256 assets) public { + assets = bound(assets, MIN_ASSETS, MAX_ASSETS); + + // Vault whose asset is the wrapped-native token. + WETHMock weth = new WETHMock(); + IERC4626 wethVault = _deployVaultV2(weth, bytes32(uint256(4))); + + vm.deal(user, assets); + // When native tokens are sent, assets must equal msg.value and no assetPermit may be set. + bundles.vaultBundlesV1Deposit{value: assets}( + address(wethVault), assets, RAY, noPermit, 0, address(0), block.timestamp + ); + + assertEq(user.balance, 0, "user native residual"); + assertEq(address(bundles).balance, 0, "bundler native residual"); + assertEq(weth.balanceOf(address(bundles)), 0, "bundler wrapped residual"); + assertApproxEqAbs(wethVault.convertToAssets(wethVault.balanceOf(user)), assets, 1, "user position"); + } + /// WITHDRAW /// function testWithdrawV1(uint256 assets) public { @@ -749,3 +769,12 @@ contract VaultBundlesTest is Test { ); } } + +/// @dev Minimal wrapped-native token: deposit() mints 1:1 for the native tokens sent. +contract WETHMock is ERC20Mock { + constructor() ERC20Mock(18) {} + + function deposit() external payable { + _mint(msg.sender, msg.value); + } +} From fbfb661f4237c7d25878da438ae1cf64997513ec Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Thu, 23 Jul 2026 19:03:18 +0200 Subject: [PATCH 03/11] return wrapped --- src/blue/BlueBundlesV1.sol | 12 ++++-------- test/BlueBundlesTest.sol | 8 ++++---- 2 files changed, 8 insertions(+), 12 deletions(-) diff --git a/src/blue/BlueBundlesV1.sol b/src/blue/BlueBundlesV1.sol index cee384b..60747e8 100644 --- a/src/blue/BlueBundlesV1.sol +++ b/src/blue/BlueBundlesV1.sol @@ -123,14 +123,10 @@ contract BlueBundlesV1 is IBlueBundlesV1, IMorphoRepayCallback { if (referralFeeAssets > 0) { SafeTransferLib.safeTransfer(marketParams.loanToken, referralFeeRecipient, referralFeeAssets); } - uint256 refund = maxRepayAssets - repayAssets - referralFeeAssets; - if (msg.value > 0) { - IWNative(marketParams.loanToken).withdraw(refund); - (bool success,) = msg.sender.call{value: refund}(""); - require(success, NativeTransferFailed()); - } else { - SafeTransferLib.safeTransfer(marketParams.loanToken, msg.sender, refund); - } + + SafeTransferLib.safeTransfer( + marketParams.loanToken, msg.sender, maxRepayAssets - repayAssets - referralFeeAssets + ); } /// @dev Pulls assets from msg.sender (optionally via ERC-2612 or Permit2) and supplies them to the market for msg.sender. diff --git a/test/BlueBundlesTest.sol b/test/BlueBundlesTest.sol index 4154268..92640e8 100644 --- a/test/BlueBundlesTest.sol +++ b/test/BlueBundlesTest.sol @@ -735,7 +735,7 @@ contract BlueBundlesTest is Test { morpho.borrow(wethMarketParams, borrowAssets, 0, user, user); vm.stopPrank(); - // Discard the borrowed wrapped tokens; the user repays with native and the refund must come back as native. + // Discard the borrowed wrapped tokens; the user repays with native and the refund comes back wrapped. deal(address(weth), user, 0); uint256 repayAssets = 40e18; @@ -764,9 +764,9 @@ contract BlueBundlesTest is Test { assertEq(morpho.expectedBorrowAssets(wethMarketParams, user), borrowAssets - repayAssets, "debt"); assertEq(morpho.collateral(wethId, user), collateral - withdrawCollateral, "remaining collateral"); assertEq(collateralToken.balanceOf(user), withdrawCollateral, "collateral to user"); - // The unused remainder is unwrapped and returned as native, not as the wrapped token. - assertEq(user.balance, maxRepayAssets - repayAssets, "native refund"); - assertEq(weth.balanceOf(user), 0, "no wrapped refund"); + // The unused remainder is returned as the wrapped token, not unwrapped back to native. + assertEq(weth.balanceOf(user), maxRepayAssets - repayAssets, "wrapped refund"); + assertEq(user.balance, 0, "no native refund"); assertEq(address(blueBundles).balance, 0, "bundler native residual"); assertEq(weth.balanceOf(address(blueBundles)), 0, "bundler wrapped residual"); } From dd5fb6a68d94ea6e0b867e876becfc0b2de2d007 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Thu, 23 Jul 2026 19:06:05 +0200 Subject: [PATCH 04/11] Revert "return wrapped" This reverts commit fbfb661f4237c7d25878da438ae1cf64997513ec. --- src/blue/BlueBundlesV1.sol | 12 ++++++++---- test/BlueBundlesTest.sol | 8 ++++---- 2 files changed, 12 insertions(+), 8 deletions(-) diff --git a/src/blue/BlueBundlesV1.sol b/src/blue/BlueBundlesV1.sol index 60747e8..cee384b 100644 --- a/src/blue/BlueBundlesV1.sol +++ b/src/blue/BlueBundlesV1.sol @@ -123,10 +123,14 @@ contract BlueBundlesV1 is IBlueBundlesV1, IMorphoRepayCallback { if (referralFeeAssets > 0) { SafeTransferLib.safeTransfer(marketParams.loanToken, referralFeeRecipient, referralFeeAssets); } - - SafeTransferLib.safeTransfer( - marketParams.loanToken, msg.sender, maxRepayAssets - repayAssets - referralFeeAssets - ); + uint256 refund = maxRepayAssets - repayAssets - referralFeeAssets; + if (msg.value > 0) { + IWNative(marketParams.loanToken).withdraw(refund); + (bool success,) = msg.sender.call{value: refund}(""); + require(success, NativeTransferFailed()); + } else { + SafeTransferLib.safeTransfer(marketParams.loanToken, msg.sender, refund); + } } /// @dev Pulls assets from msg.sender (optionally via ERC-2612 or Permit2) and supplies them to the market for msg.sender. diff --git a/test/BlueBundlesTest.sol b/test/BlueBundlesTest.sol index 92640e8..4154268 100644 --- a/test/BlueBundlesTest.sol +++ b/test/BlueBundlesTest.sol @@ -735,7 +735,7 @@ contract BlueBundlesTest is Test { morpho.borrow(wethMarketParams, borrowAssets, 0, user, user); vm.stopPrank(); - // Discard the borrowed wrapped tokens; the user repays with native and the refund comes back wrapped. + // Discard the borrowed wrapped tokens; the user repays with native and the refund must come back as native. deal(address(weth), user, 0); uint256 repayAssets = 40e18; @@ -764,9 +764,9 @@ contract BlueBundlesTest is Test { assertEq(morpho.expectedBorrowAssets(wethMarketParams, user), borrowAssets - repayAssets, "debt"); assertEq(morpho.collateral(wethId, user), collateral - withdrawCollateral, "remaining collateral"); assertEq(collateralToken.balanceOf(user), withdrawCollateral, "collateral to user"); - // The unused remainder is returned as the wrapped token, not unwrapped back to native. - assertEq(weth.balanceOf(user), maxRepayAssets - repayAssets, "wrapped refund"); - assertEq(user.balance, 0, "no native refund"); + // The unused remainder is unwrapped and returned as native, not as the wrapped token. + assertEq(user.balance, maxRepayAssets - repayAssets, "native refund"); + assertEq(weth.balanceOf(user), 0, "no wrapped refund"); assertEq(address(blueBundles).balance, 0, "bundler native residual"); assertEq(weth.balanceOf(address(blueBundles)), 0, "bundler wrapped residual"); } From 81dee74fda5bc661de21ebaf71576eca2441f959 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Fri, 24 Jul 2026 15:19:27 +0200 Subject: [PATCH 05/11] document remainder revert --- src/blue/BlueBundlesV1.sol | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/blue/BlueBundlesV1.sol b/src/blue/BlueBundlesV1.sol index cee384b..afaa741 100644 --- a/src/blue/BlueBundlesV1.sol +++ b/src/blue/BlueBundlesV1.sol @@ -85,6 +85,7 @@ contract BlueBundlesV1 is IBlueBundlesV1, IMorphoRepayCallback { /// @dev Pulls maxRepayAssets from msg.sender, repays msg.sender's debt, reimburses the unused remainder at the end of the call, and withdraws collateral if collateralAssets > 0. /// @dev When native tokens are sent, they are wrapped into marketParams.loanToken (which must be the wrapped-native token) instead of pulling, and the reimbursed remainder is unwrapped back to native. + /// @dev Reimbursing native tokens (even 0 amount) requires msg.sender to be able to receive native tokens, or else it will revert. /// @dev The msg.sender must have authorized this contract on Blue, beforehand or via signedAuthorization, if some collateral is withdrawn. /// @dev Exactly one of repayAssets and repayShares should be non-zero: the debt is repaid by assets, or by shares. To close the full debt, pass msg.sender's full borrow shares as repayShares. /// @dev The fee is repaidAmount * referralFeePct / (WAD - referralFeePct). @@ -123,13 +124,13 @@ contract BlueBundlesV1 is IBlueBundlesV1, IMorphoRepayCallback { if (referralFeeAssets > 0) { SafeTransferLib.safeTransfer(marketParams.loanToken, referralFeeRecipient, referralFeeAssets); } - uint256 refund = maxRepayAssets - repayAssets - referralFeeAssets; + uint256 remainder = maxRepayAssets - repayAssets - referralFeeAssets; if (msg.value > 0) { - IWNative(marketParams.loanToken).withdraw(refund); - (bool success,) = msg.sender.call{value: refund}(""); + IWNative(marketParams.loanToken).withdraw(remainder); + (bool success,) = msg.sender.call{value: remainder}(""); require(success, NativeTransferFailed()); } else { - SafeTransferLib.safeTransfer(marketParams.loanToken, msg.sender, refund); + SafeTransferLib.safeTransfer(marketParams.loanToken, msg.sender, remainder); } } From 115055863725851cf3b4ea05ea12d112a4ff2945 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Fri, 24 Jul 2026 16:21:24 +0200 Subject: [PATCH 06/11] fix potential 0 transfer --- src/blue/BlueBundlesV1.sol | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/src/blue/BlueBundlesV1.sol b/src/blue/BlueBundlesV1.sol index afaa741..ee5ab8b 100644 --- a/src/blue/BlueBundlesV1.sol +++ b/src/blue/BlueBundlesV1.sol @@ -83,9 +83,9 @@ contract BlueBundlesV1 is IBlueBundlesV1, IMorphoRepayCallback { SafeTransferLib.safeTransfer(marketParams.loanToken, msg.sender, borrowAssets - referralFeeAssets); } - /// @dev Pulls maxRepayAssets from msg.sender, repays msg.sender's debt, reimburses the unused remainder at the end of the call, and withdraws collateral if collateralAssets > 0. + /// @dev Pulls maxRepayAssets from msg.sender, repays msg.sender's debt, reimburses the unused remainder (if any) at the end of the call, and withdraws collateral if collateralAssets > 0. /// @dev When native tokens are sent, they are wrapped into marketParams.loanToken (which must be the wrapped-native token) instead of pulling, and the reimbursed remainder is unwrapped back to native. - /// @dev Reimbursing native tokens (even 0 amount) requires msg.sender to be able to receive native tokens, or else it will revert. + /// @dev Reimbursing native tokens requires msg.sender to be able to receive native tokens, or else it will revert. /// @dev The msg.sender must have authorized this contract on Blue, beforehand or via signedAuthorization, if some collateral is withdrawn. /// @dev Exactly one of repayAssets and repayShares should be non-zero: the debt is repaid by assets, or by shares. To close the full debt, pass msg.sender's full borrow shares as repayShares. /// @dev The fee is repaidAmount * referralFeePct / (WAD - referralFeePct). @@ -125,12 +125,14 @@ contract BlueBundlesV1 is IBlueBundlesV1, IMorphoRepayCallback { SafeTransferLib.safeTransfer(marketParams.loanToken, referralFeeRecipient, referralFeeAssets); } uint256 remainder = maxRepayAssets - repayAssets - referralFeeAssets; - if (msg.value > 0) { - IWNative(marketParams.loanToken).withdraw(remainder); - (bool success,) = msg.sender.call{value: remainder}(""); - require(success, NativeTransferFailed()); - } else { - SafeTransferLib.safeTransfer(marketParams.loanToken, msg.sender, remainder); + if (remainder > 0) { + if (msg.value > 0) { + IWNative(marketParams.loanToken).withdraw(remainder); + (bool success,) = msg.sender.call{value: remainder}(""); + require(success, NativeTransferFailed()); + } else { + SafeTransferLib.safeTransfer(marketParams.loanToken, msg.sender, remainder); + } } } From 7bb7f689f97c991c9b502c229e124de7e865c8ad Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 24 Jul 2026 14:59:31 +0000 Subject: [PATCH 07/11] certora: model native wrapping in NoResidue 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. --- certora/specs/NoResidue.spec | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/certora/specs/NoResidue.spec b/certora/specs/NoResidue.spec index aa8ef52..2476a7e 100644 --- a/certora/specs/NoResidue.spec +++ b/certora/specs/NoResidue.spec @@ -27,6 +27,11 @@ methods { function _.withdraw(BlueBundlesV1.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) external => summaryWithdraw(marketParams.loanToken, receiver) expect(uint256, uint256); function _.withdrawCollateral(BlueBundlesV1.MarketParams marketParams, uint256 assets, address onBehalf, address receiver) external => summaryWithdrawCollateral(marketParams.collateralToken, assets, receiver) expect void; + // WNative: the bundler wraps native by depositing msg.value (minting WNative to itself) and unwraps by withdrawing (burning WNative). + + function _.deposit() external with(env e) => summaryWrapNative(calledContract, e.msg.value) expect void; + function _.withdraw(uint256 amount) external => summaryUnwrapNative(calledContract, amount) expect void; + // Since calls are not summarized as havoc all by default, it is assumed that other calls don't change the bundler's balance of any token. } @@ -73,6 +78,16 @@ function summaryWithdrawCollateral(address token, uint256 assets, address receiv if (receiver == currentContract) bundlerBalance[token] = bundlerBalance[token] + assets; } +// Wrapping native mints an equal amount of WNative to the bundler (the caller). +function summaryWrapNative(address token, uint256 value) { + bundlerBalance[token] = bundlerBalance[token] + value; +} + +// Unwrapping burns WNative from the bundler; the returned native is not a tracked token. +function summaryUnwrapNative(address token, uint256 amount) { + bundlerBalance[token] = bundlerBalance[token] - amount; +} + rule supplyPreservesBalance(env e, BlueBundlesV1.MarketParams marketParams, uint256 assets, uint256 maxSharePriceE27, TokenLib.TokenPermit permit, uint256 feePct, address recipient, address token, uint256 deadline) { require permit.kind == TokenLib.PermitKind.None, "simplification for prover performance"; require e.msg.sender != currentContract, "bundler is never its own caller"; From 32486fcfe25c40b35f7434d9f16764dfe89778aa Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 24 Jul 2026 15:04:24 +0000 Subject: [PATCH 08/11] Trim comments to match spec house style --- certora/specs/NoResidue.spec | 2 -- 1 file changed, 2 deletions(-) diff --git a/certora/specs/NoResidue.spec b/certora/specs/NoResidue.spec index 2476a7e..55175be 100644 --- a/certora/specs/NoResidue.spec +++ b/certora/specs/NoResidue.spec @@ -78,12 +78,10 @@ function summaryWithdrawCollateral(address token, uint256 assets, address receiv if (receiver == currentContract) bundlerBalance[token] = bundlerBalance[token] + assets; } -// Wrapping native mints an equal amount of WNative to the bundler (the caller). function summaryWrapNative(address token, uint256 value) { bundlerBalance[token] = bundlerBalance[token] + value; } -// Unwrapping burns WNative from the bundler; the returned native is not a tracked token. function summaryUnwrapNative(address token, uint256 amount) { bundlerBalance[token] = bundlerBalance[token] - amount; } From 6a8a845df1e37798ac4c039d14f1cbab189ea33a Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 24 Jul 2026 15:17:01 +0000 Subject: [PATCH 09/11] Assert bundler native balance preserved in each rule --- certora/specs/NoResidue.spec | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/certora/specs/NoResidue.spec b/certora/specs/NoResidue.spec index 55175be..1382b8e 100644 --- a/certora/specs/NoResidue.spec +++ b/certora/specs/NoResidue.spec @@ -84,6 +84,7 @@ function summaryWrapNative(address token, uint256 value) { function summaryUnwrapNative(address token, uint256 amount) { bundlerBalance[token] = bundlerBalance[token] - amount; + nativeBalances[currentContract] = require_uint256(nativeBalances[currentContract] + amount); } rule supplyPreservesBalance(env e, BlueBundlesV1.MarketParams marketParams, uint256 assets, uint256 maxSharePriceE27, TokenLib.TokenPermit permit, uint256 feePct, address recipient, address token, uint256 deadline) { @@ -92,8 +93,10 @@ rule supplyPreservesBalance(env e, BlueBundlesV1.MarketParams marketParams, uint require recipient != currentContract, "no bundler donations of the fee"; mathint before = bundlerBalance[token]; + mathint nativeBefore = nativeBalances[currentContract]; blueBundlesV1Supply(e, marketParams, assets, maxSharePriceE27, permit, feePct, recipient, deadline); assert bundlerBalance[token] == before; + assert nativeBalances[currentContract] == nativeBefore; } rule withdrawPreservesBalance(env e, BlueBundlesV1.MarketParams marketParams, uint256 assets, uint256 shares, uint256 minSharePriceE27, BlueBundlesV1.SignedAuthorization signedAuthorization, uint256 feePct, address recipient, address token, uint256 deadline) { @@ -101,8 +104,10 @@ rule withdrawPreservesBalance(env e, BlueBundlesV1.MarketParams marketParams, ui require recipient != currentContract, "no bundler donations of the fee"; mathint before = bundlerBalance[token]; + mathint nativeBefore = nativeBalances[currentContract]; blueBundlesV1Withdraw(e, marketParams, assets, shares, minSharePriceE27, signedAuthorization, feePct, recipient, deadline); assert bundlerBalance[token] == before; + assert nativeBalances[currentContract] == nativeBefore; } rule supplyCollateralAndBorrowPreservesBalance(env e, BlueBundlesV1.MarketParams marketParams, uint256 collateralAmount, uint256 borrowAssets, uint256 minSharePriceE27, uint256 maxLtv, TokenLib.TokenPermit permit, BlueBundlesV1.SignedAuthorization signedAuthorization, uint256 feePct, address recipient, address token, uint256 deadline) { @@ -111,8 +116,10 @@ rule supplyCollateralAndBorrowPreservesBalance(env e, BlueBundlesV1.MarketParams require recipient != currentContract, "no bundler donations of the fee"; mathint before = bundlerBalance[token]; + mathint nativeBefore = nativeBalances[currentContract]; blueBundlesV1SupplyCollateralAndBorrow(e, marketParams, collateralAmount, borrowAssets, minSharePriceE27, maxLtv, permit, signedAuthorization, feePct, recipient, deadline); assert bundlerBalance[token] == before; + assert nativeBalances[currentContract] == nativeBefore; } rule repayAndWithdrawCollateralPreservesBalance(env e, BlueBundlesV1.MarketParams marketParams, uint256 assets, uint256 shares, uint256 maxRepayAssets, uint256 maxSharePriceE27, uint256 withdrawCollateralAssets, uint256 maxLtv, TokenLib.TokenPermit permit, BlueBundlesV1.SignedAuthorization signedAuthorization, uint256 feePct, address recipient, address token, uint256 deadline) { @@ -121,6 +128,8 @@ rule repayAndWithdrawCollateralPreservesBalance(env e, BlueBundlesV1.MarketParam require recipient != currentContract, "no bundler donations of the fee"; mathint before = bundlerBalance[token]; + mathint nativeBefore = nativeBalances[currentContract]; blueBundlesV1RepayAndWithdrawCollateral(e, marketParams, assets, shares, maxRepayAssets, maxSharePriceE27, withdrawCollateralAssets, maxLtv, permit, signedAuthorization, feePct, recipient, deadline); assert bundlerBalance[token] == before; + assert nativeBalances[currentContract] == nativeBefore; } From fc0318ba78598ece44cd67f5dfa82eca4dae4595 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Fri, 24 Jul 2026 17:21:57 +0200 Subject: [PATCH 10/11] tweak comment --- certora/specs/NoResidue.spec | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/certora/specs/NoResidue.spec b/certora/specs/NoResidue.spec index 1382b8e..3a9e368 100644 --- a/certora/specs/NoResidue.spec +++ b/certora/specs/NoResidue.spec @@ -13,13 +13,11 @@ persistent ghost mapping(address => mathint) bundlerBalance; methods { // ERC20: the bundler's own transfers move bundlerBalance. - function _.transferFrom(address from, address to, uint256 amt) external => cvlTransferFrom(calledContract, from, to, amt) expect(bool); function _.transfer(address to, uint256 amt) external with(env e) => cvlTransferFrom(calledContract, e.msg.sender, to, amt) expect(bool); // Morpho: pull on supply/repay/supplyCollateral, send on borrow/withdraw/withdrawCollateral. // Also assumes that the Morpho Blue address is different from the bundler's. - function _.supply(BlueBundlesV1.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) external => summarySupply(marketParams.loanToken, assets, shares) expect(uint256, uint256); function _.repay(BlueBundlesV1.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) external => summaryRepay(marketParams.loanToken) expect(uint256, uint256); function _.supplyCollateral(BlueBundlesV1.MarketParams marketParams, uint256 assets, address onBehalf, bytes data) external => summarySupplyCollateral(marketParams.collateralToken, assets) expect void; @@ -27,8 +25,7 @@ methods { function _.withdraw(BlueBundlesV1.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) external => summaryWithdraw(marketParams.loanToken, receiver) expect(uint256, uint256); function _.withdrawCollateral(BlueBundlesV1.MarketParams marketParams, uint256 assets, address onBehalf, address receiver) external => summaryWithdrawCollateral(marketParams.collateralToken, assets, receiver) expect void; - // WNative: the bundler wraps native by depositing msg.value (minting WNative to itself) and unwraps by withdrawing (burning WNative). - + // Model the WNative contract's deposit and withdraw behavior: mints on deposit and burns on withdraw. function _.deposit() external with(env e) => summaryWrapNative(calledContract, e.msg.value) expect void; function _.withdraw(uint256 amount) external => summaryUnwrapNative(calledContract, amount) expect void; From 8be0ce2f5a1a6f2d42cd779609fb17dbb487ee60 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Fri, 24 Jul 2026 18:24:18 +0200 Subject: [PATCH 11/11] summarize calls --- certora/confs/NoResidue.conf | 1 + certora/specs/NoResidue.spec | 43 +++++++++++++++++++++++------------- 2 files changed, 29 insertions(+), 15 deletions(-) diff --git a/certora/confs/NoResidue.conf b/certora/confs/NoResidue.conf index c1eac7a..25d7aad 100644 --- a/certora/confs/NoResidue.conf +++ b/certora/confs/NoResidue.conf @@ -7,6 +7,7 @@ "solc_via_ir": true, "solc_evm_version": "osaka", "optimistic_loop": true, + "optimistic_fallback": true, "loop_iter": 2, "msg": "BlueBundles: no token residue" } diff --git a/certora/specs/NoResidue.spec b/certora/specs/NoResidue.spec index 3a9e368..e8c0d41 100644 --- a/certora/specs/NoResidue.spec +++ b/certora/specs/NoResidue.spec @@ -2,14 +2,10 @@ // No token residue: every entry point preserves the bundler's balance of every token (delta 0). // Scope: all entry points, excluding migrate borrow position. -// Two assumptions shared with that suite: +// Assumptions shared with that suite: // - no bundler donations: the receiver and the recipient are different from the bundler. // - well-behaved ERC20 (no fee-on-transfer/rebasing): matching the token restriction in BlueBundles' header. - -definition WAD() returns mathint = 10 ^ 18; - -// The bundler's balance of every token, updated on every transfer that touches it. -persistent ghost mapping(address => mathint) bundlerBalance; +// - the bundler is not the wrapped-native token. methods { // ERC20: the bundler's own transfers move bundlerBalance. @@ -29,9 +25,23 @@ methods { function _.deposit() external with(env e) => summaryWrapNative(calledContract, e.msg.value) expect void; function _.withdraw(uint256 amount) external => summaryUnwrapNative(calledContract, amount) expect void; + // Summarized without state changes, as the HAVOC_ECF allows the callee to credit native tokens to the caller. + function _.setAuthorizationWithSig(BlueBundlesV1.Authorization authorization, BlueBundlesV1.Signature signature) external => NONDET; + function TokenLib.safeApprove(address token, address spender, uint256 value) internal => NONDET; + // Since calls are not summarized as havoc all by default, it is assumed that other calls don't change the bundler's balance of any token. } +definition WAD() returns mathint = 10 ^ 18; + +// The bundler's balance of every token, updated on every transfer that touches it. +persistent ghost mapping(address => mathint) bundlerBalance; + +// Native sent to the bundler by the wrapped-native contract on withdraw: summaries cannot write nativeBalances, so it is tracked separately and added to the bundler's native balance in the rules. +persistent ghost mathint unwrappedNative; + +definition bundlerNativeBalance() returns mathint = nativeBalances[currentContract] + unwrappedNative; + // well-behaved ERC20: transfers move balances by the amount. function cvlTransferFrom(address token, address from, address to, uint256 amount) returns bool { if (from == currentContract) bundlerBalance[token] = bundlerBalance[token] - amount; @@ -81,19 +91,20 @@ function summaryWrapNative(address token, uint256 value) { function summaryUnwrapNative(address token, uint256 amount) { bundlerBalance[token] = bundlerBalance[token] - amount; - nativeBalances[currentContract] = require_uint256(nativeBalances[currentContract] + amount); + unwrappedNative = unwrappedNative + amount; } rule supplyPreservesBalance(env e, BlueBundlesV1.MarketParams marketParams, uint256 assets, uint256 maxSharePriceE27, TokenLib.TokenPermit permit, uint256 feePct, address recipient, address token, uint256 deadline) { require permit.kind == TokenLib.PermitKind.None, "simplification for prover performance"; require e.msg.sender != currentContract, "bundler is never its own caller"; require recipient != currentContract, "no bundler donations of the fee"; + require marketParams.loanToken != currentContract, "the bundler is not the wrapped-native token"; mathint before = bundlerBalance[token]; - mathint nativeBefore = nativeBalances[currentContract]; + mathint nativeBefore = bundlerNativeBalance(); blueBundlesV1Supply(e, marketParams, assets, maxSharePriceE27, permit, feePct, recipient, deadline); assert bundlerBalance[token] == before; - assert nativeBalances[currentContract] == nativeBefore; + assert bundlerNativeBalance() == nativeBefore; } rule withdrawPreservesBalance(env e, BlueBundlesV1.MarketParams marketParams, uint256 assets, uint256 shares, uint256 minSharePriceE27, BlueBundlesV1.SignedAuthorization signedAuthorization, uint256 feePct, address recipient, address token, uint256 deadline) { @@ -101,32 +112,34 @@ rule withdrawPreservesBalance(env e, BlueBundlesV1.MarketParams marketParams, ui require recipient != currentContract, "no bundler donations of the fee"; mathint before = bundlerBalance[token]; - mathint nativeBefore = nativeBalances[currentContract]; + mathint nativeBefore = bundlerNativeBalance(); blueBundlesV1Withdraw(e, marketParams, assets, shares, minSharePriceE27, signedAuthorization, feePct, recipient, deadline); assert bundlerBalance[token] == before; - assert nativeBalances[currentContract] == nativeBefore; + assert bundlerNativeBalance() == nativeBefore; } rule supplyCollateralAndBorrowPreservesBalance(env e, BlueBundlesV1.MarketParams marketParams, uint256 collateralAmount, uint256 borrowAssets, uint256 minSharePriceE27, uint256 maxLtv, TokenLib.TokenPermit permit, BlueBundlesV1.SignedAuthorization signedAuthorization, uint256 feePct, address recipient, address token, uint256 deadline) { require permit.kind == TokenLib.PermitKind.None, "simplification for prover performance"; require e.msg.sender != currentContract, "bundler is never its own caller"; require recipient != currentContract, "no bundler donations of the fee"; + require marketParams.collateralToken != currentContract, "the bundler is not the wrapped-native token"; mathint before = bundlerBalance[token]; - mathint nativeBefore = nativeBalances[currentContract]; + mathint nativeBefore = bundlerNativeBalance(); blueBundlesV1SupplyCollateralAndBorrow(e, marketParams, collateralAmount, borrowAssets, minSharePriceE27, maxLtv, permit, signedAuthorization, feePct, recipient, deadline); assert bundlerBalance[token] == before; - assert nativeBalances[currentContract] == nativeBefore; + assert bundlerNativeBalance() == nativeBefore; } rule repayAndWithdrawCollateralPreservesBalance(env e, BlueBundlesV1.MarketParams marketParams, uint256 assets, uint256 shares, uint256 maxRepayAssets, uint256 maxSharePriceE27, uint256 withdrawCollateralAssets, uint256 maxLtv, TokenLib.TokenPermit permit, BlueBundlesV1.SignedAuthorization signedAuthorization, uint256 feePct, address recipient, address token, uint256 deadline) { require permit.kind == TokenLib.PermitKind.None, "simplification for prover performance"; require e.msg.sender != currentContract, "bundler is never its own caller"; require recipient != currentContract, "no bundler donations of the fee"; + require marketParams.loanToken != currentContract, "the bundler is not the wrapped-native token"; mathint before = bundlerBalance[token]; - mathint nativeBefore = nativeBalances[currentContract]; + mathint nativeBefore = bundlerNativeBalance(); blueBundlesV1RepayAndWithdrawCollateral(e, marketParams, assets, shares, maxRepayAssets, maxSharePriceE27, withdrawCollateralAssets, maxLtv, permit, signedAuthorization, feePct, recipient, deadline); assert bundlerBalance[token] == before; - assert nativeBalances[currentContract] == nativeBefore; + assert bundlerNativeBalance() == nativeBefore; }