Wrap native in Vaults and Blue bundles, refund native

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"
 }

certora/specs/NoResidue.spec

@@ -2,34 +2,46 @@
 
 // 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.
-
     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;
     function _.borrow(BlueBundlesV1.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) external => summaryBorrow(marketParams.loanToken, assets, shares, receiver) expect(uint256, uint256);
     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;
 
+    // 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;
+
+    // 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;
@@ -73,41 +85,61 @@ function summaryWithdrawCollateral(address token, uint256 assets, address receiv
     if (receiver == currentContract) bundlerBalance[token] = bundlerBalance[token] + assets;
 }
 
+function summaryWrapNative(address token, uint256 value) {
+    bundlerBalance[token] = bundlerBalance[token] + value;
+}
+
+function summaryUnwrapNative(address token, uint256 amount) {
+    bundlerBalance[token] = bundlerBalance[token] - 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 = bundlerNativeBalance();
     blueBundlesV1Supply(e, marketParams, assets, maxSharePriceE27, permit, feePct, recipient, deadline);
     assert bundlerBalance[token] == before;
+    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) {
     require e.msg.sender != currentContract, "bundler is never its own caller";
     require recipient != currentContract, "no bundler donations of the fee";
 
     mathint before = bundlerBalance[token];
+    mathint nativeBefore = bundlerNativeBalance();
     blueBundlesV1Withdraw(e, marketParams, assets, shares, minSharePriceE27, signedAuthorization, feePct, recipient, deadline);
     assert bundlerBalance[token] == before;
+    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 = bundlerNativeBalance();
     blueBundlesV1SupplyCollateralAndBorrow(e, marketParams, collateralAmount, borrowAssets, minSharePriceE27, maxLtv, permit, signedAuthorization, feePct, recipient, deadline);
     assert bundlerBalance[token] == before;
+    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 = bundlerNativeBalance();
     blueBundlesV1RepayAndWithdrawCollateral(e, marketParams, assets, shares, maxRepayAssets, maxSharePriceE27, withdrawCollateralAssets, maxLtv, permit, signedAuthorization, feePct, recipient, deadline);
     assert bundlerBalance[token] == before;
+    assert bundlerNativeBalance() == nativeBefore;
 }

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,9 +37,13 @@ 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.
+    /// @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 +60,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, "");
@@ -78,7 +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 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).
@@ -97,12 +104,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, "");
@@ -117,12 +124,20 @@ contract BlueBundlesV1 is IBlueBundlesV1, IMorphoRepayCallback {
         if (referralFeeAssets > 0) {
             SafeTransferLib.safeTransfer(marketParams.loanToken, referralFeeRecipient, referralFeeAssets);
         }
-        SafeTransferLib.safeTransfer(
-            marketParams.loanToken, msg.sender, maxRepayAssets - repayAssets - referralFeeAssets
-        );
+        uint256 remainder = maxRepayAssets - repayAssets - referralFeeAssets;
+        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);
+            }
+        }
     }
 
     /// @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).
@@ -134,14 +149,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, "");

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();
@@ -37,7 +38,7 @@ interface IBlueBundlesV1 {
         uint256 referralFeePct,
         address referralFeeRecipient,
         uint256 deadline
-    ) external;
+    ) external payable;
 
     function blueBundlesV1RepayAndWithdrawCollateral(
         MarketParams memory marketParams,
@@ -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,

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 {
@@ -30,6 +31,8 @@ struct Permit {
 
 library TokenLib {
     error ApproveReturnedFalse();
+    error BothNativeAndToken();
+    error InconsistentAmountAndNative();
 
     /// @dev Canonical Permit2 singleton.
     address constant PERMIT2 = 0x000000000022D473030F116dDEE9F6B43aC78BA3;
@@ -78,6 +81,17 @@ library TokenLib {
         }
     }
 
+    /// @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);
+        }
+    }
+
     /// @dev The parameters signed by the user should be the same as the inputs of this function.
     /// @dev Skipped when the permit is empty (v, r and s all zero; which doesn't correspond to a valid signature), useful when the tokens are already permitted.
     /// @dev Skipped on an already consumed nonce (e.g. a front-run submission): the permit is not submitted in that case.

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;
+}

src/vault/VaultBundlesV1.sol

@@ -23,6 +23,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).
@@ -34,15 +35,15 @@ contract VaultBundlesV1 is IVaultBundlesV1 {
         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 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);

src/vault/interfaces/IVaultBundlesV1.sol

@@ -21,7 +21,7 @@ interface IVaultBundlesV1 {
         uint256 referralFeePct,
         address referralFeeRecipient,
         uint256 deadline
-    ) external;
+    ) external payable;
 
     function vaultBundlesV1Withdraw(
         address vault,