From b59e5668853f88269372600b72d5b164ee253c13 Mon Sep 17 00:00:00 2001 From: Bhargav Date: Sun, 26 Jul 2026 19:15:34 +0200 Subject: [PATCH 1/2] added no residue spec for vault bundles --- certora/confs/VaultNoResidue.conf | 12 ++++ certora/specs/VaultNoResidue.spec | 94 +++++++++++++++++++++++++++++++ 2 files changed, 106 insertions(+) create mode 100644 certora/confs/VaultNoResidue.conf create mode 100644 certora/specs/VaultNoResidue.spec diff --git a/certora/confs/VaultNoResidue.conf b/certora/confs/VaultNoResidue.conf new file mode 100644 index 0000000..b9465b2 --- /dev/null +++ b/certora/confs/VaultNoResidue.conf @@ -0,0 +1,12 @@ +{ + "files": [ + "src/vault/VaultBundlesV1.sol" + ], + "verify": "VaultBundlesV1:certora/specs/VaultNoResidue.spec", + "solc": "solc-0.8.34", + "solc_via_ir": true, + "solc_evm_version": "osaka", + "optimistic_loop": true, + "loop_iter": 2, + "msg": "VaultBundles: no token residue" +} diff --git a/certora/specs/VaultNoResidue.spec b/certora/specs/VaultNoResidue.spec new file mode 100644 index 0000000..04fc17b --- /dev/null +++ b/certora/specs/VaultNoResidue.spec @@ -0,0 +1,94 @@ +// SPDX-License-Identifier: GPL-2.0-or-later + +// No token residue: every entry point preserves the bundler's balance of every token (delta 0). +// Scope: all entry points. +// Two assumptions shared with the BlueBundles suite: +// - no bundler donations: the referral fee recipient and the caller are different from the bundler. +// - well-behaved ERC20 (no fee-on-transfer/rebasing): matching the token restriction in VaultBundles' header. +// Two assumptions specific to the vault bundles, since the vault is caller-supplied rather than an immutable: +// - well-behaved ERC4626: deposit pulls exactly its assets argument, withdraw and redeem send exactly the assets they report, and asset() is constant per vault. Migrate's asset consistency check relies on that last part. +// - non-reentrant vault and token: the permit and approve calls are unresolved, so reentering an entry point is out of model. +// Share amounts are also out of model: the vault's mints and burns don't move bundlerBalance, so token == vault is not a claim about share residue. Instead the summaries assert that the bundler is never a share receiver or owner, which is why no share can be left behind. + +// The bundler's balance of every token, updated on every transfer that touches it. +persistent ghost mapping(address => mathint) bundlerBalance; + +// Each vault's underlying asset, fixed per vault so that migrate's asset consistency check is exercised rather than assumed. +persistent ghost mapping(address => address) vaultAsset; + +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); + + // ERC4626: pull on deposit, send on withdraw/redeem. + + function _.asset() external => summaryAsset(calledContract) expect(address); + function _.deposit(uint256 assets, address receiver) external => summaryDeposit(calledContract, assets, receiver) expect(uint256); + function _.withdraw(uint256 assets, address receiver, address owner) external => summaryWithdraw(calledContract, assets, receiver, owner) expect(uint256); + function _.redeem(uint256 shares, address receiver, address owner) external => summaryRedeem(calledContract, receiver, owner) expect(uint256); + + // 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. +} + +// 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; + if (to == currentContract) bundlerBalance[token] = bundlerBalance[token] + amount; + return true; +} + +function summaryAsset(address vault) returns address { + return vaultAsset[vault]; +} + +// The receiver and owner assertions stand in for tracking share amounts: the bundler is never minted shares and never has its own burned, so it can hold no share residue. +function summaryDeposit(address vault, uint256 assets, address receiver) returns uint256 { + assert receiver != currentContract, "the bundler is never minted shares"; + bundlerBalance[vaultAsset[vault]] = bundlerBalance[vaultAsset[vault]] - assets; + uint256 returnedShares; + return returnedShares; +} + +function summaryWithdraw(address vault, uint256 assets, address receiver, address owner) returns uint256 { + assert owner != currentContract, "the bundler's own shares are never burned"; + if (receiver == currentContract) bundlerBalance[vaultAsset[vault]] = bundlerBalance[vaultAsset[vault]] + assets; + uint256 returnedShares; + return returnedShares; +} + +function summaryRedeem(address vault, address receiver, address owner) returns uint256 { + assert owner != currentContract, "the bundler's own shares are never burned"; + uint256 assets; + if (receiver == currentContract) bundlerBalance[vaultAsset[vault]] = bundlerBalance[vaultAsset[vault]] + assets; + return assets; +} + +rule depositPreservesBalance(env e, address vault, uint256 assets, uint256 maxSharePriceE27, TokenLib.TokenPermit permit, uint256 feePct, address recipient, address token, uint256 deadline) { + require permit.kind != TokenLib.PermitKind.Permit2, "simplification for prover performance"; + require e.msg.sender != currentContract, "bundler is never its own caller"; + require recipient != currentContract, "no bundler donations of the fee"; + + mathint before = bundlerBalance[token]; + vaultBundlesV1Deposit(e, vault, assets, maxSharePriceE27, permit, feePct, recipient, deadline); + assert bundlerBalance[token] == before; +} + +rule withdrawPreservesBalance(env e, address vault, uint256 assets, uint256 shares, uint256 minSharePriceE27, TokenLib.Permit sharesPermit, 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]; + vaultBundlesV1Withdraw(e, vault, assets, shares, minSharePriceE27, sharesPermit, feePct, recipient, deadline); + assert bundlerBalance[token] == before; +} + +rule migratePreservesBalance(env e, address sourceVault, address destVault, uint256 assetsWithdrawn, uint256 sharesRedeemed, uint256 sourceMinSharePriceE27, uint256 destMaxSharePriceE27, TokenLib.Permit sharesPermit, 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]; + vaultBundlesV1Migrate(e, sourceVault, destVault, assetsWithdrawn, sharesRedeemed, sourceMinSharePriceE27, destMaxSharePriceE27, sharesPermit, feePct, recipient, deadline); + assert bundlerBalance[token] == before; +} From cae7f999abeb9ff34fc634291f614874584ff5b3 Mon Sep 17 00:00:00 2001 From: Bhargav Date: Wed, 29 Jul 2026 10:27:43 +0200 Subject: [PATCH 2/2] works assuming permit.kind != permit2 --- certora/specs/VaultNoResidue.spec | 34 ++++++++++++++++++++++++------- 1 file changed, 27 insertions(+), 7 deletions(-) diff --git a/certora/specs/VaultNoResidue.spec b/certora/specs/VaultNoResidue.spec index 04fc17b..2b56fe5 100644 --- a/certora/specs/VaultNoResidue.spec +++ b/certora/specs/VaultNoResidue.spec @@ -1,13 +1,14 @@ // SPDX-License-Identifier: GPL-2.0-or-later -// No token residue: every entry point preserves the bundler's balance of every token (delta 0). +// No token residue: every entry point preserves the bundler's balance of every token, and its native balance (delta 0). // Scope: all entry points. -// Two assumptions shared with the BlueBundles suite: +// Three assumptions shared with the BlueBundles suite: // - no bundler donations: the referral fee recipient and the caller are different from the bundler. // - well-behaved ERC20 (no fee-on-transfer/rebasing): matching the token restriction in VaultBundles' header. +// - the bundler is not the wrapped-native token. // Two assumptions specific to the vault bundles, since the vault is caller-supplied rather than an immutable: // - well-behaved ERC4626: deposit pulls exactly its assets argument, withdraw and redeem send exactly the assets they report, and asset() is constant per vault. Migrate's asset consistency check relies on that last part. -// - non-reentrant vault and token: the permit and approve calls are unresolved, so reentering an entry point is out of model. +// - non-reentrant vault and token: the permit and approve calls are summarized without state changes, so reentering an entry point is out of model. // Share amounts are also out of model: the vault's mints and burns don't move bundlerBalance, so token == vault is not a claim about share residue. Instead the summaries assert that the bundler is never a share receiver or owner, which is why no share can be left behind. // The bundler's balance of every token, updated on every transfer that touches it. @@ -29,6 +30,13 @@ methods { function _.withdraw(uint256 assets, address receiver, address owner) external => summaryWithdraw(calledContract, assets, receiver, owner) expect(uint256); function _.redeem(uint256 shares, address receiver, address owner) external => summaryRedeem(calledContract, receiver, owner) expect(uint256); + // Model the WNative contract's deposit behavior: mints on deposit. Deposit wraps msg.value into the vault asset instead of pulling it. + function _.deposit() external with(env e) => summaryWrapNative(calledContract, e.msg.value) expect void; + + // Summarized without state changes, as the HAVOC_ECF allows the callee to credit native tokens to the caller. + function _.permit(address owner, address spender, uint256 value, uint256 deadline, uint8 v, bytes32 r, bytes32 s) 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. } @@ -43,6 +51,11 @@ function summaryAsset(address vault) returns address { return vaultAsset[vault]; } +// The native sent along is deducted by the call itself, so only the minted wrapped token is credited here. +function summaryWrapNative(address token, uint256 value) { + bundlerBalance[token] = bundlerBalance[token] + value; +} + // The receiver and owner assertions stand in for tracking share amounts: the bundler is never minted shares and never has its own burned, so it can hold no share residue. function summaryDeposit(address vault, uint256 assets, address receiver) returns uint256 { assert receiver != currentContract, "the bundler is never minted shares"; @@ -69,26 +82,33 @@ rule depositPreservesBalance(env e, address vault, uint256 assets, uint256 maxSh require permit.kind != TokenLib.PermitKind.Permit2, "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 vaultAsset[vault] != currentContract, "the bundler is not the wrapped-native token"; mathint before = bundlerBalance[token]; + mathint nativeBefore = nativeBalances[currentContract]; vaultBundlesV1Deposit(e, vault, assets, maxSharePriceE27, permit, feePct, recipient, deadline); assert bundlerBalance[token] == before; + assert nativeBalances[currentContract] == nativeBefore; } -rule withdrawPreservesBalance(env e, address vault, uint256 assets, uint256 shares, uint256 minSharePriceE27, TokenLib.Permit sharesPermit, uint256 feePct, address recipient, address token, uint256 deadline) { +rule withdrawPreservesBalance(env e, address vault, uint256 assets, uint256 shares, TokenLib.Permit sharesPermit, 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]; - vaultBundlesV1Withdraw(e, vault, assets, shares, minSharePriceE27, sharesPermit, feePct, recipient, deadline); + mathint nativeBefore = nativeBalances[currentContract]; + vaultBundlesV1Withdraw(e, vault, assets, shares, sharesPermit, feePct, recipient, deadline); assert bundlerBalance[token] == before; + assert nativeBalances[currentContract] == nativeBefore; } -rule migratePreservesBalance(env e, address sourceVault, address destVault, uint256 assetsWithdrawn, uint256 sharesRedeemed, uint256 sourceMinSharePriceE27, uint256 destMaxSharePriceE27, TokenLib.Permit sharesPermit, uint256 feePct, address recipient, address token, uint256 deadline) { +rule migratePreservesBalance(env e, address sourceVault, address destVault, uint256 assetsWithdrawn, uint256 sharesRedeemed, uint256 destMaxSharePriceE27, TokenLib.Permit sharesPermit, 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]; - vaultBundlesV1Migrate(e, sourceVault, destVault, assetsWithdrawn, sharesRedeemed, sourceMinSharePriceE27, destMaxSharePriceE27, sharesPermit, feePct, recipient, deadline); + mathint nativeBefore = nativeBalances[currentContract]; + vaultBundlesV1Migrate(e, sourceVault, destVault, assetsWithdrawn, sharesRedeemed, destMaxSharePriceE27, sharesPermit, feePct, recipient, deadline); assert bundlerBalance[token] == before; + assert nativeBalances[currentContract] == nativeBefore; }