From b253eb02ebe9d967efaa4d5bb998037b0fea17fb Mon Sep 17 00:00:00 2001 From: "prd-carapulse[bot]" <264278285+prd-carapulse[bot]@users.noreply.github.com> Date: Wed, 19 Aug 2026 09:52:21 +0000 Subject: [PATCH 01/11] feat(certora): verify Blue net amount inversion Add Certora rules for the documented penalty-aware net amount formula on withdraw and supplyCollateralAndBorrow. Co-authored-by: Bhargav <40268131+bhargavbh@users.noreply.github.com> --- certora/confs/BlueNetAmountInvertibility.conf | 19 +++ certora/specs/BlueNetAmountInvertibility.spec | 138 ++++++++++++++++++ 2 files changed, 157 insertions(+) create mode 100644 certora/confs/BlueNetAmountInvertibility.conf create mode 100644 certora/specs/BlueNetAmountInvertibility.spec diff --git a/certora/confs/BlueNetAmountInvertibility.conf b/certora/confs/BlueNetAmountInvertibility.conf new file mode 100644 index 0000000..55033d2 --- /dev/null +++ b/certora/confs/BlueNetAmountInvertibility.conf @@ -0,0 +1,19 @@ +{ + "files": [ + "src/blue/BlueBundlesV1.sol", + "lib/vault-v2/src/periphery/blue-public-allocator/BluePublicAllocator.sol" + ], + "link": ["BlueBundlesV1:PUBLIC_ALLOCATOR=BluePublicAllocator"], + "verify": "BlueBundlesV1:certora/specs/BlueNetAmountInvertibility.spec", + "packages": ["lib/vault-v2/lib/morpho-blue=lib/morpho-blue"], + "compiler_map": {"BlueBundlesV1": "solc-0.8.34", "BluePublicAllocator": "solc-0.8.28"}, + "solc_via_ir": true, + "solc_evm_version_map": {"BlueBundlesV1": "osaka", "BluePublicAllocator": "cancun"}, + "use_relpaths_for_solc_json": true, + "optimistic_loop": true, + "optimistic_fallback": true, + "loop_iter": 3, + "msg": "BlueBundles: net amount inversion with public allocator penalties", + "prover_args": ["-depth 5", "-mediumTimeout 60", "-timeout 7200"], + "smt_timeout": 3600 +} diff --git a/certora/specs/BlueNetAmountInvertibility.spec b/certora/specs/BlueNetAmountInvertibility.spec new file mode 100644 index 0000000..139eac9 --- /dev/null +++ b/certora/specs/BlueNetAmountInvertibility.spec @@ -0,0 +1,138 @@ +// SPDX-License-Identifier: GPL-2.0-or-later + +// Net amount inversion for the two Blue entrypoints. P is the aggregate +// public-allocator penalty, deducted before the referral fee. +methods { + function _.transferFrom(address from, address to, uint256 amount) external => cvlTransferFrom(calledContract, from, to, amount) expect(bool); + function _.transfer(address to, uint256 amount) external with(env e) => cvlTransferFrom(calledContract, e.msg.sender, to, amount) expect(bool); + function _.permitTransferFrom(ISignatureTransfer.PermitTransferFrom permit, ISignatureTransfer.SignatureTransferDetails details, address owner, bytes signature) external => summaryPermit2Transfer(permit.permitted.token, owner, details.to, details.requestedAmount) 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, assets, shares, receiver) expect(uint256, uint256); + function _.supplyCollateral(BlueBundlesV1.MarketParams marketParams, uint256 assets, address onBehalf, bytes data) external => summarySupplyCollateral(marketParams.collateralToken, assets) expect void; + function _.flashLoan(address token, uint256 assets, bytes data) external => summaryFlashLoan(token, assets, data) expect void; + function _.setAuthorizationWithSig(BlueBundlesV1.Authorization authorization, BlueBundlesV1.Signature signature) external => NONDET; + function TokenLib.safeApprove(address token, address spender, uint256 value) internal => NONDET; + + // Both implementations use this same rounding-up penalty calculation. + function UtilsLib.mulDivUp(uint256 x, uint256 y, uint256 d) internal returns uint256 => mulDivUpG(x, y, d); + function MathLib.mulDivUp(uint256 x, uint256 y, uint256 d) internal returns uint256 => mulDivUpG(x, y, d); + function UtilsLib.mulDivDown(uint256 x, uint256 y, uint256 d) internal returns uint256 => summaryMulDivDown(x, y, d); +} + +persistent ghost mulDivUpG(uint256, uint256, uint256) returns uint256; +persistent ghost mapping(address => mathint) bundlerBalance; +persistent ghost mapping(address => mapping(address => mathint)) recipientBalance; + +definition WAD() returns uint256 = 10 ^ 18; + +function summaryMulDivDown(uint256 a, uint256 b, uint256 d) returns uint256 { + if (d == 0 || a * b > max_uint256) revert(); + mathint result = a * b / d; + assert result >= 0 && result <= 2 ^ 256; + return require_uint256(result); +} + +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; + else if (from == currentContract) recipientBalance[token][to] = recipientBalance[token][to] + amount; + return true; +} + +function summaryPermit2Transfer(address token, address from, address to, uint256 amount) { + cvlTransferFrom(token, from, to, amount); +} + +function summarySupplyCollateral(address token, uint256 amount) { + bundlerBalance[token] = bundlerBalance[token] - amount; +} + +function summaryBorrow(address token, uint256 assets, uint256 shares, address receiver) returns (uint256, uint256) { + assert shares == 0; + if (receiver == currentContract) bundlerBalance[token] = bundlerBalance[token] + assets; + uint256 returnedShares; + return (assets, returnedShares); +} + +function summaryWithdraw(address token, uint256 assets, uint256 shares, address receiver) returns (uint256, uint256) { + require shares == 0; + if (receiver == currentContract) bundlerBalance[token] = bundlerBalance[token] + assets; + uint256 returnedShares; + return (assets, returnedShares); +} + +function summaryFlashLoan(address token, uint256 assets, bytes data) { + bundlerBalance[token] = bundlerBalance[token] + assets; + env callbackEnv; + onMorphoFlashLoan(callbackEnv, assets, data); + bundlerBalance[token] = bundlerBalance[token] - assets; +} + +function reallocationsAssumptions(BlueBundlesV1.PublicAllocations[] reallocations) { + require reallocations.length <= 3, "loop bound"; + require reallocations.length > 0 => reallocations[0].vault != currentContract, "bundler is not a vault"; + require reallocations.length > 1 => reallocations[1].vault != currentContract, "bundler is not a vault"; + require reallocations.length > 2 => reallocations[2].vault != currentContract, "bundler is not a vault"; +} + +rule blueBundlesV1WithdrawReturnsTargetNet( + env e, + BlueBundlesV1.MarketParams marketParams, + BlueBundlesV1.SignedAuthorization signedAuthorization, + BlueBundlesV1.PublicAllocations[] reallocations, + uint256 referralFeePct, + address referralFeeRecipient, + uint256 deadline, + uint256 targetNet +) { + require e.msg.sender != currentContract; + require referralFeeRecipient != currentContract; + require referralFeePct < WAD(); + reallocationsAssumptions(reallocations); + + uint256 penaltyAssets; + for (uint256 i = 0; i < reallocations.length; i++) { + penaltyAssets += uint256(reallocations[i].assets).mulDivUp(uint256(reallocations[i].penalty), WAD()); + } + uint256 grossAssets = summaryMulDivDown(targetNet, WAD(), assert_uint256(WAD() - referralFeePct)); + mathint before = bundlerBalance[marketParams.loanToken]; + mathint userBefore = recipientBalance[marketParams.loanToken][e.msg.sender]; + + blueBundlesV1Withdraw(e, marketParams, penaltyAssets + grossAssets, 0, signedAuthorization, reallocations, referralFeePct, referralFeeRecipient, deadline); + + assert bundlerBalance[marketParams.loanToken] == before; + assert recipientBalance[marketParams.loanToken][e.msg.sender] - userBefore == targetNet; +} + +rule blueBundlesV1SupplyCollateralAndBorrowReturnsTargetNet( + env e, + BlueBundlesV1.MarketParams marketParams, + uint256 collateralAssets, + uint256 minSharePriceE27, + uint256 maxLtv, + TokenLib.TokenPermit collateralPermit, + BlueBundlesV1.SignedAuthorization signedAuthorization, + BlueBundlesV1.PublicAllocations[] reallocations, + uint256 referralFeePct, + address referralFeeRecipient, + uint256 deadline, + uint256 targetNet +) { + require e.msg.sender != currentContract; + require referralFeeRecipient != currentContract; + require referralFeePct < WAD(); + reallocationsAssumptions(reallocations); + + uint256 penaltyAssets; + for (uint256 i = 0; i < reallocations.length; i++) { + penaltyAssets += uint256(reallocations[i].assets).mulDivUp(uint256(reallocations[i].penalty), WAD()); + } + uint256 grossAssets = summaryMulDivDown(targetNet, WAD(), assert_uint256(WAD() - referralFeePct)); + mathint before = bundlerBalance[marketParams.loanToken]; + mathint userBefore = recipientBalance[marketParams.loanToken][e.msg.sender]; + + blueBundlesV1SupplyCollateralAndBorrow(e, marketParams, collateralAssets, penaltyAssets + grossAssets, minSharePriceE27, maxLtv, collateralPermit, signedAuthorization, reallocations, referralFeePct, referralFeeRecipient, deadline); + + assert bundlerBalance[marketParams.loanToken] == before; + assert recipientBalance[marketParams.loanToken][e.msg.sender] - userBefore == targetNet; +} From 5b9f6224a8965751acef42a349cfea32e913774d Mon Sep 17 00:00:00 2001 From: "prd-carapulse[bot]" <264278285+prd-carapulse[bot]@users.noreply.github.com> Date: Wed, 19 Aug 2026 09:56:58 +0000 Subject: [PATCH 02/11] fix(certora): format net amount spec Apply Certora CVL formatter-compatible spacing and avoid unsupported loop syntax in the rule helpers. Co-authored-by: Bhargav <40268131+bhargavbh@users.noreply.github.com> --- certora/specs/BlueNetAmountInvertibility.spec | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/certora/specs/BlueNetAmountInvertibility.spec b/certora/specs/BlueNetAmountInvertibility.spec index 139eac9..623aaa8 100644 --- a/certora/specs/BlueNetAmountInvertibility.spec +++ b/certora/specs/BlueNetAmountInvertibility.spec @@ -2,6 +2,7 @@ // Net amount inversion for the two Blue entrypoints. P is the aggregate // public-allocator penalty, deducted before the referral fee. + methods { function _.transferFrom(address from, address to, uint256 amount) external => cvlTransferFrom(calledContract, from, to, amount) expect(bool); function _.transfer(address to, uint256 amount) external with(env e) => cvlTransferFrom(calledContract, e.msg.sender, to, amount) expect(bool); @@ -91,9 +92,9 @@ rule blueBundlesV1WithdrawReturnsTargetNet( reallocationsAssumptions(reallocations); uint256 penaltyAssets; - for (uint256 i = 0; i < reallocations.length; i++) { - penaltyAssets += uint256(reallocations[i].assets).mulDivUp(uint256(reallocations[i].penalty), WAD()); - } + if (reallocations.length > 0) penaltyAssets += uint256(reallocations[0].assets).mulDivUp(uint256(reallocations[0].penalty), WAD()); + if (reallocations.length > 1) penaltyAssets += uint256(reallocations[1].assets).mulDivUp(uint256(reallocations[1].penalty), WAD()); + if (reallocations.length > 2) penaltyAssets += uint256(reallocations[2].assets).mulDivUp(uint256(reallocations[2].penalty), WAD()); uint256 grossAssets = summaryMulDivDown(targetNet, WAD(), assert_uint256(WAD() - referralFeePct)); mathint before = bundlerBalance[marketParams.loanToken]; mathint userBefore = recipientBalance[marketParams.loanToken][e.msg.sender]; @@ -124,9 +125,9 @@ rule blueBundlesV1SupplyCollateralAndBorrowReturnsTargetNet( reallocationsAssumptions(reallocations); uint256 penaltyAssets; - for (uint256 i = 0; i < reallocations.length; i++) { - penaltyAssets += uint256(reallocations[i].assets).mulDivUp(uint256(reallocations[i].penalty), WAD()); - } + if (reallocations.length > 0) penaltyAssets += uint256(reallocations[0].assets).mulDivUp(uint256(reallocations[0].penalty), WAD()); + if (reallocations.length > 1) penaltyAssets += uint256(reallocations[1].assets).mulDivUp(uint256(reallocations[1].penalty), WAD()); + if (reallocations.length > 2) penaltyAssets += uint256(reallocations[2].assets).mulDivUp(uint256(reallocations[2].penalty), WAD()); uint256 grossAssets = summaryMulDivDown(targetNet, WAD(), assert_uint256(WAD() - referralFeePct)); mathint before = bundlerBalance[marketParams.loanToken]; mathint userBefore = recipientBalance[marketParams.loanToken][e.msg.sender]; From 7c171fdaf856897b5a1581cd2f58beac7a61d10b Mon Sep 17 00:00:00 2001 From: "prd-carapulse[bot]" <264278285+prd-carapulse[bot]@users.noreply.github.com> Date: Thu, 20 Aug 2026 07:24:02 +0000 Subject: [PATCH 03/11] fix(certora): address review feedback Model allocator penalty transfers, native wrapping, caller/referrer aliasing, and full-precision gross-up arithmetic. Canonicalize the Certora config with jq. Co-authored-by: Bhargav <40268131+bhargavbh@users.noreply.github.com> --- certora/confs/BlueNetAmountInvertibility.conf | 24 +++++++++++++++---- certora/specs/BlueNetAmountInvertibility.spec | 19 ++++++++++++--- 2 files changed, 35 insertions(+), 8 deletions(-) diff --git a/certora/confs/BlueNetAmountInvertibility.conf b/certora/confs/BlueNetAmountInvertibility.conf index 55033d2..1d5cb67 100644 --- a/certora/confs/BlueNetAmountInvertibility.conf +++ b/certora/confs/BlueNetAmountInvertibility.conf @@ -3,17 +3,31 @@ "src/blue/BlueBundlesV1.sol", "lib/vault-v2/src/periphery/blue-public-allocator/BluePublicAllocator.sol" ], - "link": ["BlueBundlesV1:PUBLIC_ALLOCATOR=BluePublicAllocator"], + "link": [ + "BlueBundlesV1:PUBLIC_ALLOCATOR=BluePublicAllocator" + ], "verify": "BlueBundlesV1:certora/specs/BlueNetAmountInvertibility.spec", - "packages": ["lib/vault-v2/lib/morpho-blue=lib/morpho-blue"], - "compiler_map": {"BlueBundlesV1": "solc-0.8.34", "BluePublicAllocator": "solc-0.8.28"}, + "packages": [ + "lib/vault-v2/lib/morpho-blue=lib/morpho-blue" + ], + "compiler_map": { + "BlueBundlesV1": "solc-0.8.34", + "BluePublicAllocator": "solc-0.8.28" + }, "solc_via_ir": true, - "solc_evm_version_map": {"BlueBundlesV1": "osaka", "BluePublicAllocator": "cancun"}, + "solc_evm_version_map": { + "BlueBundlesV1": "osaka", + "BluePublicAllocator": "cancun" + }, "use_relpaths_for_solc_json": true, "optimistic_loop": true, "optimistic_fallback": true, "loop_iter": 3, "msg": "BlueBundles: net amount inversion with public allocator penalties", - "prover_args": ["-depth 5", "-mediumTimeout 60", "-timeout 7200"], + "prover_args": [ + "-depth 5", + "-mediumTimeout 60", + "-timeout 7200" + ], "smt_timeout": 3600 } diff --git a/certora/specs/BlueNetAmountInvertibility.spec b/certora/specs/BlueNetAmountInvertibility.spec index 623aaa8..571fe07 100644 --- a/certora/specs/BlueNetAmountInvertibility.spec +++ b/certora/specs/BlueNetAmountInvertibility.spec @@ -11,6 +11,8 @@ methods { function _.withdraw(BlueBundlesV1.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) external => summaryWithdraw(marketParams.loanToken, assets, shares, receiver) expect(uint256, uint256); function _.supplyCollateral(BlueBundlesV1.MarketParams marketParams, uint256 assets, address onBehalf, bytes data) external => summarySupplyCollateral(marketParams.collateralToken, assets) expect void; function _.flashLoan(address token, uint256 assets, bytes data) external => summaryFlashLoan(token, assets, data) expect void; + function _.deposit() external with(env e) => summaryWrapNative(calledContract, e.msg.value) expect void; + function SafeERC20Lib.safeTransferFrom(address token, address from, address to, uint256 value) internal => cvlSafeTransferFrom(token, from, to, value); function _.setAuthorizationWithSig(BlueBundlesV1.Authorization authorization, BlueBundlesV1.Signature signature) external => NONDET; function TokenLib.safeApprove(address token, address spender, uint256 value) internal => NONDET; @@ -27,9 +29,10 @@ persistent ghost mapping(address => mapping(address => mathint)) recipientBalanc definition WAD() returns uint256 = 10 ^ 18; function summaryMulDivDown(uint256 a, uint256 b, uint256 d) returns uint256 { - if (d == 0 || a * b > max_uint256) revert(); - mathint result = a * b / d; - assert result >= 0 && result <= 2 ^ 256; + if (d == 0) revert(); + mathint numerator = a * b; + mathint result = numerator / d; + assert result >= 0 && result <= max_uint256; return require_uint256(result); } @@ -40,6 +43,10 @@ function cvlTransferFrom(address token, address from, address to, uint256 amount return true; } +function cvlSafeTransferFrom(address token, address from, address to, uint256 value) { + cvlTransferFrom(token, from, to, value); +} + function summaryPermit2Transfer(address token, address from, address to, uint256 amount) { cvlTransferFrom(token, from, to, amount); } @@ -48,6 +55,10 @@ function summarySupplyCollateral(address token, uint256 amount) { bundlerBalance[token] = bundlerBalance[token] - amount; } +function summaryWrapNative(address token, uint256 value) { + bundlerBalance[token] = bundlerBalance[token] + value; +} + function summaryBorrow(address token, uint256 assets, uint256 shares, address receiver) returns (uint256, uint256) { assert shares == 0; if (receiver == currentContract) bundlerBalance[token] = bundlerBalance[token] + assets; @@ -88,6 +99,7 @@ rule blueBundlesV1WithdrawReturnsTargetNet( ) { require e.msg.sender != currentContract; require referralFeeRecipient != currentContract; + require referralFeeRecipient != e.msg.sender; require referralFeePct < WAD(); reallocationsAssumptions(reallocations); @@ -121,6 +133,7 @@ rule blueBundlesV1SupplyCollateralAndBorrowReturnsTargetNet( ) { require e.msg.sender != currentContract; require referralFeeRecipient != currentContract; + require referralFeeRecipient != e.msg.sender; require referralFeePct < WAD(); reallocationsAssumptions(reallocations); From b51e269b67b5c0fedd4cd3f0bdf202cf07ec6d53 Mon Sep 17 00:00:00 2001 From: "prd-carapulse[bot]" <264278285+prd-carapulse[bot]@users.noreply.github.com> Date: Thu, 20 Aug 2026 07:26:09 +0000 Subject: [PATCH 04/11] fix(certora): use CVL assignment syntax Replace unsupported compound assignments in the bounded penalty calculation. Co-authored-by: Bhargav <40268131+bhargavbh@users.noreply.github.com> --- certora/specs/BlueNetAmountInvertibility.spec | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/certora/specs/BlueNetAmountInvertibility.spec b/certora/specs/BlueNetAmountInvertibility.spec index 571fe07..d638c9a 100644 --- a/certora/specs/BlueNetAmountInvertibility.spec +++ b/certora/specs/BlueNetAmountInvertibility.spec @@ -104,9 +104,9 @@ rule blueBundlesV1WithdrawReturnsTargetNet( reallocationsAssumptions(reallocations); uint256 penaltyAssets; - if (reallocations.length > 0) penaltyAssets += uint256(reallocations[0].assets).mulDivUp(uint256(reallocations[0].penalty), WAD()); - if (reallocations.length > 1) penaltyAssets += uint256(reallocations[1].assets).mulDivUp(uint256(reallocations[1].penalty), WAD()); - if (reallocations.length > 2) penaltyAssets += uint256(reallocations[2].assets).mulDivUp(uint256(reallocations[2].penalty), WAD()); + if (reallocations.length > 0) penaltyAssets = penaltyAssets + uint256(reallocations[0].assets).mulDivUp(uint256(reallocations[0].penalty), WAD()); + if (reallocations.length > 1) penaltyAssets = penaltyAssets + uint256(reallocations[1].assets).mulDivUp(uint256(reallocations[1].penalty), WAD()); + if (reallocations.length > 2) penaltyAssets = penaltyAssets + uint256(reallocations[2].assets).mulDivUp(uint256(reallocations[2].penalty), WAD()); uint256 grossAssets = summaryMulDivDown(targetNet, WAD(), assert_uint256(WAD() - referralFeePct)); mathint before = bundlerBalance[marketParams.loanToken]; mathint userBefore = recipientBalance[marketParams.loanToken][e.msg.sender]; @@ -138,9 +138,9 @@ rule blueBundlesV1SupplyCollateralAndBorrowReturnsTargetNet( reallocationsAssumptions(reallocations); uint256 penaltyAssets; - if (reallocations.length > 0) penaltyAssets += uint256(reallocations[0].assets).mulDivUp(uint256(reallocations[0].penalty), WAD()); - if (reallocations.length > 1) penaltyAssets += uint256(reallocations[1].assets).mulDivUp(uint256(reallocations[1].penalty), WAD()); - if (reallocations.length > 2) penaltyAssets += uint256(reallocations[2].assets).mulDivUp(uint256(reallocations[2].penalty), WAD()); + if (reallocations.length > 0) penaltyAssets = penaltyAssets + uint256(reallocations[0].assets).mulDivUp(uint256(reallocations[0].penalty), WAD()); + if (reallocations.length > 1) penaltyAssets = penaltyAssets + uint256(reallocations[1].assets).mulDivUp(uint256(reallocations[1].penalty), WAD()); + if (reallocations.length > 2) penaltyAssets = penaltyAssets + uint256(reallocations[2].assets).mulDivUp(uint256(reallocations[2].penalty), WAD()); uint256 grossAssets = summaryMulDivDown(targetNet, WAD(), assert_uint256(WAD() - referralFeePct)); mathint before = bundlerBalance[marketParams.loanToken]; mathint userBefore = recipientBalance[marketParams.loanToken][e.msg.sender]; From c58388c1f0a014ff04095c03676ea4c842c771b9 Mon Sep 17 00:00:00 2001 From: Bhargav Date: Thu, 20 Aug 2026 09:29:20 +0200 Subject: [PATCH 05/11] spec fmt --- certora/specs/BlueNetAmountInvertibility.spec | 34 ++++--------------- 1 file changed, 7 insertions(+), 27 deletions(-) diff --git a/certora/specs/BlueNetAmountInvertibility.spec b/certora/specs/BlueNetAmountInvertibility.spec index d638c9a..b594910 100644 --- a/certora/specs/BlueNetAmountInvertibility.spec +++ b/certora/specs/BlueNetAmountInvertibility.spec @@ -17,13 +17,15 @@ methods { function TokenLib.safeApprove(address token, address spender, uint256 value) internal => NONDET; // Both implementations use this same rounding-up penalty calculation. - function UtilsLib.mulDivUp(uint256 x, uint256 y, uint256 d) internal returns uint256 => mulDivUpG(x, y, d); - function MathLib.mulDivUp(uint256 x, uint256 y, uint256 d) internal returns uint256 => mulDivUpG(x, y, d); - function UtilsLib.mulDivDown(uint256 x, uint256 y, uint256 d) internal returns uint256 => summaryMulDivDown(x, y, d); + function UtilsLib.mulDivUp(uint256 x, uint256 y, uint256 d) internal returns (uint256) => mulDivUpG(x, y, d); + function MathLib.mulDivUp(uint256 x, uint256 y, uint256 d) internal returns (uint256) => mulDivUpG(x, y, d); + function UtilsLib.mulDivDown(uint256 x, uint256 y, uint256 d) internal returns (uint256) => summaryMulDivDown(x, y, d); } persistent ghost mulDivUpG(uint256, uint256, uint256) returns uint256; + persistent ghost mapping(address => mathint) bundlerBalance; + persistent ghost mapping(address => mapping(address => mathint)) recipientBalance; definition WAD() returns uint256 = 10 ^ 18; @@ -87,16 +89,7 @@ function reallocationsAssumptions(BlueBundlesV1.PublicAllocations[] reallocation require reallocations.length > 2 => reallocations[2].vault != currentContract, "bundler is not a vault"; } -rule blueBundlesV1WithdrawReturnsTargetNet( - env e, - BlueBundlesV1.MarketParams marketParams, - BlueBundlesV1.SignedAuthorization signedAuthorization, - BlueBundlesV1.PublicAllocations[] reallocations, - uint256 referralFeePct, - address referralFeeRecipient, - uint256 deadline, - uint256 targetNet -) { +rule blueBundlesV1WithdrawReturnsTargetNet(env e, BlueBundlesV1.MarketParams marketParams, BlueBundlesV1.SignedAuthorization signedAuthorization, BlueBundlesV1.PublicAllocations[] reallocations, uint256 referralFeePct, address referralFeeRecipient, uint256 deadline, uint256 targetNet) { require e.msg.sender != currentContract; require referralFeeRecipient != currentContract; require referralFeeRecipient != e.msg.sender; @@ -117,20 +110,7 @@ rule blueBundlesV1WithdrawReturnsTargetNet( assert recipientBalance[marketParams.loanToken][e.msg.sender] - userBefore == targetNet; } -rule blueBundlesV1SupplyCollateralAndBorrowReturnsTargetNet( - env e, - BlueBundlesV1.MarketParams marketParams, - uint256 collateralAssets, - uint256 minSharePriceE27, - uint256 maxLtv, - TokenLib.TokenPermit collateralPermit, - BlueBundlesV1.SignedAuthorization signedAuthorization, - BlueBundlesV1.PublicAllocations[] reallocations, - uint256 referralFeePct, - address referralFeeRecipient, - uint256 deadline, - uint256 targetNet -) { +rule blueBundlesV1SupplyCollateralAndBorrowReturnsTargetNet(env e, BlueBundlesV1.MarketParams marketParams, uint256 collateralAssets, uint256 minSharePriceE27, uint256 maxLtv, TokenLib.TokenPermit collateralPermit, BlueBundlesV1.SignedAuthorization signedAuthorization, BlueBundlesV1.PublicAllocations[] reallocations, uint256 referralFeePct, address referralFeeRecipient, uint256 deadline, uint256 targetNet) { require e.msg.sender != currentContract; require referralFeeRecipient != currentContract; require referralFeeRecipient != e.msg.sender; From 68b23179ae7c07920f9dc1462ce75808e9de0150 Mon Sep 17 00:00:00 2001 From: Bhargav Date: Thu, 20 Aug 2026 11:05:16 +0200 Subject: [PATCH 06/11] summarised the PA calls --- certora/confs/BlueNetAmountInvertibility.conf | 17 ++--- certora/specs/BlueNetAmountInvertibility.spec | 69 ++++++++++++------- 2 files changed, 50 insertions(+), 36 deletions(-) diff --git a/certora/confs/BlueNetAmountInvertibility.conf b/certora/confs/BlueNetAmountInvertibility.conf index 1d5cb67..67c3551 100644 --- a/certora/confs/BlueNetAmountInvertibility.conf +++ b/certora/confs/BlueNetAmountInvertibility.conf @@ -1,30 +1,21 @@ { "files": [ - "src/blue/BlueBundlesV1.sol", - "lib/vault-v2/src/periphery/blue-public-allocator/BluePublicAllocator.sol" - ], - "link": [ - "BlueBundlesV1:PUBLIC_ALLOCATOR=BluePublicAllocator" + "src/blue/BlueBundlesV1.sol" ], "verify": "BlueBundlesV1:certora/specs/BlueNetAmountInvertibility.spec", "packages": [ "lib/vault-v2/lib/morpho-blue=lib/morpho-blue" ], - "compiler_map": { - "BlueBundlesV1": "solc-0.8.34", - "BluePublicAllocator": "solc-0.8.28" - }, + "solc": "solc-0.8.34", "solc_via_ir": true, - "solc_evm_version_map": { - "BlueBundlesV1": "osaka", - "BluePublicAllocator": "cancun" - }, + "solc_evm_version": "osaka", "use_relpaths_for_solc_json": true, "optimistic_loop": true, "optimistic_fallback": true, "loop_iter": 3, "msg": "BlueBundles: net amount inversion with public allocator penalties", "prover_args": [ + "-splitParallel true", "-depth 5", "-mediumTimeout 60", "-timeout 7200" diff --git a/certora/specs/BlueNetAmountInvertibility.spec b/certora/specs/BlueNetAmountInvertibility.spec index b594910..44da1b0 100644 --- a/certora/specs/BlueNetAmountInvertibility.spec +++ b/certora/specs/BlueNetAmountInvertibility.spec @@ -12,16 +12,27 @@ methods { function _.supplyCollateral(BlueBundlesV1.MarketParams marketParams, uint256 assets, address onBehalf, bytes data) external => summarySupplyCollateral(marketParams.collateralToken, assets) expect void; function _.flashLoan(address token, uint256 assets, bytes data) external => summaryFlashLoan(token, assets, data) expect void; function _.deposit() external with(env e) => summaryWrapNative(calledContract, e.msg.value) expect void; - function SafeERC20Lib.safeTransferFrom(address token, address from, address to, uint256 value) internal => cvlSafeTransferFrom(token, from, to, value); + // The public allocator charges the caller mulDivUp(assets, penalty, WAD) of the destination + // loan token and sends it to the vault, and moves no other token of the caller. Proven of the + // implementation by BluePublicAllocatorPenalty.spec. Its revert conditions are dropped, which + // only widens the set of verified executions. + function _.reallocate(address vault, address deallocateAdapter, BlueBundlesV1.MarketParams deallocateMarketParams, address allocateAdapter, BlueBundlesV1.MarketParams allocateMarketParams, uint128 assets, uint64 penalty) external => summaryPublicAllocation(allocateMarketParams.loanToken, vault, assets, penalty) expect void; + function _.allocateFromIdle(address vault, address adapter, BlueBundlesV1.MarketParams marketParams, uint128 assets, uint64 penalty) external => summaryPublicAllocation(marketParams.loanToken, vault, assets, penalty) expect void; function _.setAuthorizationWithSig(BlueBundlesV1.Authorization authorization, BlueBundlesV1.Signature signature) external => NONDET; + function _.nonce(address authorizer) external => NONDET; + + // Only reverts, and reads no state that the property depends on: skipping it verifies a + // superset of the executions (over-approximation), and drops the market id hashing, the + // oracle price call and two symbolic-divisor divisions. + function BlueBundlesV1.requireMaxLtv(BlueBundlesV1.MarketParams memory marketParams, address sender, uint256 maxLtv) internal => NONDET; function TokenLib.safeApprove(address token, address spender, uint256 value) internal => NONDET; - // Both implementations use this same rounding-up penalty calculation. function UtilsLib.mulDivUp(uint256 x, uint256 y, uint256 d) internal returns (uint256) => mulDivUpG(x, y, d); - function MathLib.mulDivUp(uint256 x, uint256 y, uint256 d) internal returns (uint256) => mulDivUpG(x, y, d); function UtilsLib.mulDivDown(uint256 x, uint256 y, uint256 d) internal returns (uint256) => summaryMulDivDown(x, y, d); } +// The bundler and the public allocator compute the penalty with the same rounding-up division, so +// both sides of the summary above use this one uninterpreted function. persistent ghost mulDivUpG(uint256, uint256, uint256) returns uint256; persistent ghost mapping(address => mathint) bundlerBalance; @@ -31,11 +42,11 @@ persistent ghost mapping(address => mapping(address => mathint)) recipientBalanc definition WAD() returns uint256 = 10 ^ 18; function summaryMulDivDown(uint256 a, uint256 b, uint256 d) returns uint256 { - if (d == 0) revert(); - mathint numerator = a * b; - mathint result = numerator / d; - assert result >= 0 && result <= max_uint256; - return require_uint256(result); + if (d == 0 || a * b > max_uint256) { + revert(); + } + // a * b <= max_uint256 and d >= 1 above, so the result fits. + return require_uint256(a * b / d); } function cvlTransferFrom(address token, address from, address to, uint256 amount) returns bool { @@ -45,8 +56,8 @@ function cvlTransferFrom(address token, address from, address to, uint256 amount return true; } -function cvlSafeTransferFrom(address token, address from, address to, uint256 value) { - cvlTransferFrom(token, from, to, value); +function summaryPublicAllocation(address token, address vault, uint128 assets, uint64 penalty) { + cvlTransferFrom(token, currentContract, vault, mulDivUpG(assets, penalty, WAD())); } function summaryPermit2Transfer(address token, address from, address to, uint256 amount) { @@ -82,11 +93,29 @@ function summaryFlashLoan(address token, uint256 assets, bytes data) { bundlerBalance[token] = bundlerBalance[token] - assets; } -function reallocationsAssumptions(BlueBundlesV1.PublicAllocations[] reallocations) { +function reallocationsAssumptions(BlueBundlesV1.PublicAllocations[] reallocations, address recipient) { require reallocations.length <= 3, "loop bound"; require reallocations.length > 0 => reallocations[0].vault != currentContract, "bundler is not a vault"; require reallocations.length > 1 => reallocations[1].vault != currentContract, "bundler is not a vault"; require reallocations.length > 2 => reallocations[2].vault != currentContract, "bundler is not a vault"; + require reallocations.length > 0 => reallocations[0].vault != recipient, "recipient is not a vault"; + require reallocations.length > 1 => reallocations[1].vault != recipient, "recipient is not a vault"; + require reallocations.length > 2 => reallocations[2].vault != recipient, "recipient is not a vault"; +} + +function sumPenaltyAssets(BlueBundlesV1.PublicAllocations[] reallocations) returns mathint { + if (reallocations.length > 2) { + return mulDivUpG(reallocations[0].assets, reallocations[0].penalty, WAD()) + + mulDivUpG(reallocations[1].assets, reallocations[1].penalty, WAD()) + + mulDivUpG(reallocations[2].assets, reallocations[2].penalty, WAD()); + } else if (reallocations.length > 1) { + return mulDivUpG(reallocations[0].assets, reallocations[0].penalty, WAD()) + + mulDivUpG(reallocations[1].assets, reallocations[1].penalty, WAD()); + } else if (reallocations.length > 0) { + return mulDivUpG(reallocations[0].assets, reallocations[0].penalty, WAD()); + } else { + return 0; + } } rule blueBundlesV1WithdrawReturnsTargetNet(env e, BlueBundlesV1.MarketParams marketParams, BlueBundlesV1.SignedAuthorization signedAuthorization, BlueBundlesV1.PublicAllocations[] reallocations, uint256 referralFeePct, address referralFeeRecipient, uint256 deadline, uint256 targetNet) { @@ -94,17 +123,14 @@ rule blueBundlesV1WithdrawReturnsTargetNet(env e, BlueBundlesV1.MarketParams mar require referralFeeRecipient != currentContract; require referralFeeRecipient != e.msg.sender; require referralFeePct < WAD(); - reallocationsAssumptions(reallocations); + reallocationsAssumptions(reallocations, e.msg.sender); - uint256 penaltyAssets; - if (reallocations.length > 0) penaltyAssets = penaltyAssets + uint256(reallocations[0].assets).mulDivUp(uint256(reallocations[0].penalty), WAD()); - if (reallocations.length > 1) penaltyAssets = penaltyAssets + uint256(reallocations[1].assets).mulDivUp(uint256(reallocations[1].penalty), WAD()); - if (reallocations.length > 2) penaltyAssets = penaltyAssets + uint256(reallocations[2].assets).mulDivUp(uint256(reallocations[2].penalty), WAD()); + mathint penaltyAssets = sumPenaltyAssets(reallocations); uint256 grossAssets = summaryMulDivDown(targetNet, WAD(), assert_uint256(WAD() - referralFeePct)); mathint before = bundlerBalance[marketParams.loanToken]; mathint userBefore = recipientBalance[marketParams.loanToken][e.msg.sender]; - blueBundlesV1Withdraw(e, marketParams, penaltyAssets + grossAssets, 0, signedAuthorization, reallocations, referralFeePct, referralFeeRecipient, deadline); + blueBundlesV1Withdraw(e, marketParams, require_uint256(penaltyAssets + grossAssets), 0, signedAuthorization, reallocations, referralFeePct, referralFeeRecipient, deadline); assert bundlerBalance[marketParams.loanToken] == before; assert recipientBalance[marketParams.loanToken][e.msg.sender] - userBefore == targetNet; @@ -115,17 +141,14 @@ rule blueBundlesV1SupplyCollateralAndBorrowReturnsTargetNet(env e, BlueBundlesV1 require referralFeeRecipient != currentContract; require referralFeeRecipient != e.msg.sender; require referralFeePct < WAD(); - reallocationsAssumptions(reallocations); + reallocationsAssumptions(reallocations, e.msg.sender); - uint256 penaltyAssets; - if (reallocations.length > 0) penaltyAssets = penaltyAssets + uint256(reallocations[0].assets).mulDivUp(uint256(reallocations[0].penalty), WAD()); - if (reallocations.length > 1) penaltyAssets = penaltyAssets + uint256(reallocations[1].assets).mulDivUp(uint256(reallocations[1].penalty), WAD()); - if (reallocations.length > 2) penaltyAssets = penaltyAssets + uint256(reallocations[2].assets).mulDivUp(uint256(reallocations[2].penalty), WAD()); + mathint penaltyAssets = sumPenaltyAssets(reallocations); uint256 grossAssets = summaryMulDivDown(targetNet, WAD(), assert_uint256(WAD() - referralFeePct)); mathint before = bundlerBalance[marketParams.loanToken]; mathint userBefore = recipientBalance[marketParams.loanToken][e.msg.sender]; - blueBundlesV1SupplyCollateralAndBorrow(e, marketParams, collateralAssets, penaltyAssets + grossAssets, minSharePriceE27, maxLtv, collateralPermit, signedAuthorization, reallocations, referralFeePct, referralFeeRecipient, deadline); + blueBundlesV1SupplyCollateralAndBorrow(e, marketParams, collateralAssets, require_uint256(penaltyAssets + grossAssets), minSharePriceE27, maxLtv, collateralPermit, signedAuthorization, reallocations, referralFeePct, referralFeeRecipient, deadline); assert bundlerBalance[marketParams.loanToken] == before; assert recipientBalance[marketParams.loanToken][e.msg.sender] - userBefore == targetNet; From bfc491b10a15b8aa70fe846cab3d40a5770b4636 Mon Sep 17 00:00:00 2001 From: Bhargav Date: Thu, 20 Aug 2026 13:01:48 +0200 Subject: [PATCH 07/11] split based on nonempty reallocation --- certora/confs/BlueNetAmountInvertibility.conf | 2 +- certora/specs/BlueNetAmountInvertibility.spec | 72 ++++++++++++++++--- 2 files changed, 63 insertions(+), 11 deletions(-) diff --git a/certora/confs/BlueNetAmountInvertibility.conf b/certora/confs/BlueNetAmountInvertibility.conf index 67c3551..fb70d86 100644 --- a/certora/confs/BlueNetAmountInvertibility.conf +++ b/certora/confs/BlueNetAmountInvertibility.conf @@ -12,7 +12,7 @@ "use_relpaths_for_solc_json": true, "optimistic_loop": true, "optimistic_fallback": true, - "loop_iter": 3, + "loop_iter": 2, "msg": "BlueBundles: net amount inversion with public allocator penalties", "prover_args": [ "-splitParallel true", diff --git a/certora/specs/BlueNetAmountInvertibility.spec b/certora/specs/BlueNetAmountInvertibility.spec index 44da1b0..6b5e954 100644 --- a/certora/specs/BlueNetAmountInvertibility.spec +++ b/certora/specs/BlueNetAmountInvertibility.spec @@ -94,21 +94,15 @@ function summaryFlashLoan(address token, uint256 assets, bytes data) { } function reallocationsAssumptions(BlueBundlesV1.PublicAllocations[] reallocations, address recipient) { - require reallocations.length <= 3, "loop bound"; + require reallocations.length <= 2, "loop bound"; require reallocations.length > 0 => reallocations[0].vault != currentContract, "bundler is not a vault"; require reallocations.length > 1 => reallocations[1].vault != currentContract, "bundler is not a vault"; - require reallocations.length > 2 => reallocations[2].vault != currentContract, "bundler is not a vault"; require reallocations.length > 0 => reallocations[0].vault != recipient, "recipient is not a vault"; require reallocations.length > 1 => reallocations[1].vault != recipient, "recipient is not a vault"; - require reallocations.length > 2 => reallocations[2].vault != recipient, "recipient is not a vault"; } function sumPenaltyAssets(BlueBundlesV1.PublicAllocations[] reallocations) returns mathint { - if (reallocations.length > 2) { - return mulDivUpG(reallocations[0].assets, reallocations[0].penalty, WAD()) - + mulDivUpG(reallocations[1].assets, reallocations[1].penalty, WAD()) - + mulDivUpG(reallocations[2].assets, reallocations[2].penalty, WAD()); - } else if (reallocations.length > 1) { + if (reallocations.length > 1) { return mulDivUpG(reallocations[0].assets, reallocations[0].penalty, WAD()) + mulDivUpG(reallocations[1].assets, reallocations[1].penalty, WAD()); } else if (reallocations.length > 0) { @@ -118,6 +112,20 @@ function sumPenaltyAssets(BlueBundlesV1.PublicAllocations[] reallocations) retur } } +// The inverse formula documented on both entrypoints: the gross amount floor(t * WAD / (WAD - pct)) +// nets exactly t once the fee is taken. Proven on its own, with no contract call in the query, so +// that the entrypoint rules below can take the relation as a hypothesis and discharge their assert +// by congruence instead of re-deriving this nonlinear identity inside a far larger query. Those +// rules quantify over every gross amount satisfying the relation, so the two together give the +// original statement. +rule referralFeeInversion(uint256 targetNet, uint256 referralFeePct) { + require referralFeePct < WAD(); + + uint256 grossAssets = summaryMulDivDown(targetNet, WAD(), assert_uint256(WAD() - referralFeePct)); + + assert grossAssets - summaryMulDivDown(grossAssets, referralFeePct, WAD()) == targetNet; +} + rule blueBundlesV1WithdrawReturnsTargetNet(env e, BlueBundlesV1.MarketParams marketParams, BlueBundlesV1.SignedAuthorization signedAuthorization, BlueBundlesV1.PublicAllocations[] reallocations, uint256 referralFeePct, address referralFeeRecipient, uint256 deadline, uint256 targetNet) { require e.msg.sender != currentContract; require referralFeeRecipient != currentContract; @@ -126,7 +134,8 @@ rule blueBundlesV1WithdrawReturnsTargetNet(env e, BlueBundlesV1.MarketParams mar reallocationsAssumptions(reallocations, e.msg.sender); mathint penaltyAssets = sumPenaltyAssets(reallocations); - uint256 grossAssets = summaryMulDivDown(targetNet, WAD(), assert_uint256(WAD() - referralFeePct)); + uint256 grossAssets; + require grossAssets - summaryMulDivDown(grossAssets, referralFeePct, WAD()) == targetNet, "referralFeeInversion"; mathint before = bundlerBalance[marketParams.loanToken]; mathint userBefore = recipientBalance[marketParams.loanToken][e.msg.sender]; @@ -136,6 +145,28 @@ rule blueBundlesV1WithdrawReturnsTargetNet(env e, BlueBundlesV1.MarketParams mar assert recipientBalance[marketParams.loanToken][e.msg.sender] - userBefore == targetNet; } +// The same property on the no-penalty path, where the bundle carries no reallocation: Blue is +// withdrawn from directly, without the flash loan that funds the penalties upfront. A case of the +// rule above, kept separate because it skips the callback and its bundle re-encoding entirely, so +// it gives fast feedback on the token flow on its own. Same for the borrow entrypoint below. +rule blueBundlesV1WithdrawReturnsTargetNetWithoutReallocations(env e, BlueBundlesV1.MarketParams marketParams, BlueBundlesV1.SignedAuthorization signedAuthorization, BlueBundlesV1.PublicAllocations[] reallocations, uint256 referralFeePct, address referralFeeRecipient, uint256 deadline, uint256 targetNet) { + require e.msg.sender != currentContract; + require referralFeeRecipient != currentContract; + require referralFeeRecipient != e.msg.sender; + require referralFeePct < WAD(); + require reallocations.length == 0, "no penalty to flash loan"; + + uint256 grossAssets; + require grossAssets - summaryMulDivDown(grossAssets, referralFeePct, WAD()) == targetNet, "referralFeeInversion"; + mathint before = bundlerBalance[marketParams.loanToken]; + mathint userBefore = recipientBalance[marketParams.loanToken][e.msg.sender]; + + blueBundlesV1Withdraw(e, marketParams, grossAssets, 0, signedAuthorization, reallocations, referralFeePct, referralFeeRecipient, deadline); + + assert bundlerBalance[marketParams.loanToken] == before; + assert recipientBalance[marketParams.loanToken][e.msg.sender] - userBefore == targetNet; +} + rule blueBundlesV1SupplyCollateralAndBorrowReturnsTargetNet(env e, BlueBundlesV1.MarketParams marketParams, uint256 collateralAssets, uint256 minSharePriceE27, uint256 maxLtv, TokenLib.TokenPermit collateralPermit, BlueBundlesV1.SignedAuthorization signedAuthorization, BlueBundlesV1.PublicAllocations[] reallocations, uint256 referralFeePct, address referralFeeRecipient, uint256 deadline, uint256 targetNet) { require e.msg.sender != currentContract; require referralFeeRecipient != currentContract; @@ -144,7 +175,8 @@ rule blueBundlesV1SupplyCollateralAndBorrowReturnsTargetNet(env e, BlueBundlesV1 reallocationsAssumptions(reallocations, e.msg.sender); mathint penaltyAssets = sumPenaltyAssets(reallocations); - uint256 grossAssets = summaryMulDivDown(targetNet, WAD(), assert_uint256(WAD() - referralFeePct)); + uint256 grossAssets; + require grossAssets - summaryMulDivDown(grossAssets, referralFeePct, WAD()) == targetNet, "referralFeeInversion"; mathint before = bundlerBalance[marketParams.loanToken]; mathint userBefore = recipientBalance[marketParams.loanToken][e.msg.sender]; @@ -153,3 +185,23 @@ rule blueBundlesV1SupplyCollateralAndBorrowReturnsTargetNet(env e, BlueBundlesV1 assert bundlerBalance[marketParams.loanToken] == before; assert recipientBalance[marketParams.loanToken][e.msg.sender] - userBefore == targetNet; } + +// The same property on the no-penalty path, where the bundle carries no reallocation: Blue is +// borrowed from directly, without the flash loan that funds the penalties upfront. +rule blueBundlesV1SupplyCollateralAndBorrowReturnsTargetNetWithoutReallocations(env e, BlueBundlesV1.MarketParams marketParams, uint256 collateralAssets, uint256 minSharePriceE27, uint256 maxLtv, TokenLib.TokenPermit collateralPermit, BlueBundlesV1.SignedAuthorization signedAuthorization, BlueBundlesV1.PublicAllocations[] reallocations, uint256 referralFeePct, address referralFeeRecipient, uint256 deadline, uint256 targetNet) { + require e.msg.sender != currentContract; + require referralFeeRecipient != currentContract; + require referralFeeRecipient != e.msg.sender; + require referralFeePct < WAD(); + require reallocations.length == 0, "no penalty to flash loan"; + + uint256 grossAssets; + require grossAssets - summaryMulDivDown(grossAssets, referralFeePct, WAD()) == targetNet, "referralFeeInversion"; + mathint before = bundlerBalance[marketParams.loanToken]; + mathint userBefore = recipientBalance[marketParams.loanToken][e.msg.sender]; + + blueBundlesV1SupplyCollateralAndBorrow(e, marketParams, collateralAssets, grossAssets, minSharePriceE27, maxLtv, collateralPermit, signedAuthorization, reallocations, referralFeePct, referralFeeRecipient, deadline); + + assert bundlerBalance[marketParams.loanToken] == before; + assert recipientBalance[marketParams.loanToken][e.msg.sender] - userBefore == targetNet; +} From 49883d9924e0979e7914841630456988b04df7b7 Mon Sep 17 00:00:00 2001 From: Bhargav Date: Thu, 27 Aug 2026 12:10:42 +0200 Subject: [PATCH 08/11] remove empty reallocation special cases; they were for experimenting prover performance --- certora/specs/BlueNetAmountInvertibility.spec | 51 ++----------------- 1 file changed, 5 insertions(+), 46 deletions(-) diff --git a/certora/specs/BlueNetAmountInvertibility.spec b/certora/specs/BlueNetAmountInvertibility.spec index 6b5e954..e58ca2a 100644 --- a/certora/specs/BlueNetAmountInvertibility.spec +++ b/certora/specs/BlueNetAmountInvertibility.spec @@ -12,6 +12,7 @@ methods { function _.supplyCollateral(BlueBundlesV1.MarketParams marketParams, uint256 assets, address onBehalf, bytes data) external => summarySupplyCollateral(marketParams.collateralToken, assets) expect void; function _.flashLoan(address token, uint256 assets, bytes data) external => summaryFlashLoan(token, assets, data) expect void; function _.deposit() external with(env e) => summaryWrapNative(calledContract, e.msg.value) expect void; + // The public allocator charges the caller mulDivUp(assets, penalty, WAD) of the destination // loan token and sends it to the vault, and moves no other token of the caller. Proven of the // implementation by BluePublicAllocatorPenalty.spec. Its revert conditions are dropped, which @@ -45,6 +46,7 @@ function summaryMulDivDown(uint256 a, uint256 b, uint256 d) returns uint256 { if (d == 0 || a * b > max_uint256) { revert(); } + // a * b <= max_uint256 and d >= 1 above, so the result fits. return require_uint256(a * b / d); } @@ -103,8 +105,7 @@ function reallocationsAssumptions(BlueBundlesV1.PublicAllocations[] reallocation function sumPenaltyAssets(BlueBundlesV1.PublicAllocations[] reallocations) returns mathint { if (reallocations.length > 1) { - return mulDivUpG(reallocations[0].assets, reallocations[0].penalty, WAD()) - + mulDivUpG(reallocations[1].assets, reallocations[1].penalty, WAD()); + return mulDivUpG(reallocations[0].assets, reallocations[0].penalty, WAD()) + mulDivUpG(reallocations[1].assets, reallocations[1].penalty, WAD()); } else if (reallocations.length > 0) { return mulDivUpG(reallocations[0].assets, reallocations[0].penalty, WAD()); } else { @@ -145,29 +146,7 @@ rule blueBundlesV1WithdrawReturnsTargetNet(env e, BlueBundlesV1.MarketParams mar assert recipientBalance[marketParams.loanToken][e.msg.sender] - userBefore == targetNet; } -// The same property on the no-penalty path, where the bundle carries no reallocation: Blue is -// withdrawn from directly, without the flash loan that funds the penalties upfront. A case of the -// rule above, kept separate because it skips the callback and its bundle re-encoding entirely, so -// it gives fast feedback on the token flow on its own. Same for the borrow entrypoint below. -rule blueBundlesV1WithdrawReturnsTargetNetWithoutReallocations(env e, BlueBundlesV1.MarketParams marketParams, BlueBundlesV1.SignedAuthorization signedAuthorization, BlueBundlesV1.PublicAllocations[] reallocations, uint256 referralFeePct, address referralFeeRecipient, uint256 deadline, uint256 targetNet) { - require e.msg.sender != currentContract; - require referralFeeRecipient != currentContract; - require referralFeeRecipient != e.msg.sender; - require referralFeePct < WAD(); - require reallocations.length == 0, "no penalty to flash loan"; - - uint256 grossAssets; - require grossAssets - summaryMulDivDown(grossAssets, referralFeePct, WAD()) == targetNet, "referralFeeInversion"; - mathint before = bundlerBalance[marketParams.loanToken]; - mathint userBefore = recipientBalance[marketParams.loanToken][e.msg.sender]; - - blueBundlesV1Withdraw(e, marketParams, grossAssets, 0, signedAuthorization, reallocations, referralFeePct, referralFeeRecipient, deadline); - - assert bundlerBalance[marketParams.loanToken] == before; - assert recipientBalance[marketParams.loanToken][e.msg.sender] - userBefore == targetNet; -} - -rule blueBundlesV1SupplyCollateralAndBorrowReturnsTargetNet(env e, BlueBundlesV1.MarketParams marketParams, uint256 collateralAssets, uint256 minSharePriceE27, uint256 maxLtv, TokenLib.TokenPermit collateralPermit, BlueBundlesV1.SignedAuthorization signedAuthorization, BlueBundlesV1.PublicAllocations[] reallocations, uint256 referralFeePct, address referralFeeRecipient, uint256 deadline, uint256 targetNet) { +rule blueBundlesV1SupplyCollateralAndBorrowReturnsTargetNet(env e, BlueBundlesV1.MarketParams marketParams, uint256 collateralAssets, uint256 maxLtv, TokenLib.TokenPermit collateralPermit, BlueBundlesV1.SignedAuthorization signedAuthorization, BlueBundlesV1.PublicAllocations[] reallocations, uint256 referralFeePct, address referralFeeRecipient, uint256 deadline, uint256 targetNet) { require e.msg.sender != currentContract; require referralFeeRecipient != currentContract; require referralFeeRecipient != e.msg.sender; @@ -180,27 +159,7 @@ rule blueBundlesV1SupplyCollateralAndBorrowReturnsTargetNet(env e, BlueBundlesV1 mathint before = bundlerBalance[marketParams.loanToken]; mathint userBefore = recipientBalance[marketParams.loanToken][e.msg.sender]; - blueBundlesV1SupplyCollateralAndBorrow(e, marketParams, collateralAssets, require_uint256(penaltyAssets + grossAssets), minSharePriceE27, maxLtv, collateralPermit, signedAuthorization, reallocations, referralFeePct, referralFeeRecipient, deadline); - - assert bundlerBalance[marketParams.loanToken] == before; - assert recipientBalance[marketParams.loanToken][e.msg.sender] - userBefore == targetNet; -} - -// The same property on the no-penalty path, where the bundle carries no reallocation: Blue is -// borrowed from directly, without the flash loan that funds the penalties upfront. -rule blueBundlesV1SupplyCollateralAndBorrowReturnsTargetNetWithoutReallocations(env e, BlueBundlesV1.MarketParams marketParams, uint256 collateralAssets, uint256 minSharePriceE27, uint256 maxLtv, TokenLib.TokenPermit collateralPermit, BlueBundlesV1.SignedAuthorization signedAuthorization, BlueBundlesV1.PublicAllocations[] reallocations, uint256 referralFeePct, address referralFeeRecipient, uint256 deadline, uint256 targetNet) { - require e.msg.sender != currentContract; - require referralFeeRecipient != currentContract; - require referralFeeRecipient != e.msg.sender; - require referralFeePct < WAD(); - require reallocations.length == 0, "no penalty to flash loan"; - - uint256 grossAssets; - require grossAssets - summaryMulDivDown(grossAssets, referralFeePct, WAD()) == targetNet, "referralFeeInversion"; - mathint before = bundlerBalance[marketParams.loanToken]; - mathint userBefore = recipientBalance[marketParams.loanToken][e.msg.sender]; - - blueBundlesV1SupplyCollateralAndBorrow(e, marketParams, collateralAssets, grossAssets, minSharePriceE27, maxLtv, collateralPermit, signedAuthorization, reallocations, referralFeePct, referralFeeRecipient, deadline); + blueBundlesV1SupplyCollateralAndBorrow(e, marketParams, collateralAssets, require_uint256(penaltyAssets + grossAssets), maxLtv, collateralPermit, signedAuthorization, reallocations, referralFeePct, referralFeeRecipient, deadline); assert bundlerBalance[marketParams.loanToken] == before; assert recipientBalance[marketParams.loanToken][e.msg.sender] - userBefore == targetNet; From e85de1517fd71edeb254cb947fcd02f38e6ed19e Mon Sep 17 00:00:00 2001 From: Bhargav Date: Thu, 27 Aug 2026 12:16:06 +0200 Subject: [PATCH 09/11] cut down comments --- certora/specs/BlueNetAmountInvertibility.spec | 25 ++++++------------- 1 file changed, 7 insertions(+), 18 deletions(-) diff --git a/certora/specs/BlueNetAmountInvertibility.spec b/certora/specs/BlueNetAmountInvertibility.spec index e58ca2a..187769e 100644 --- a/certora/specs/BlueNetAmountInvertibility.spec +++ b/certora/specs/BlueNetAmountInvertibility.spec @@ -1,7 +1,6 @@ // SPDX-License-Identifier: GPL-2.0-or-later -// Net amount inversion for the two Blue entrypoints. P is the aggregate -// public-allocator penalty, deducted before the referral fee. +// Check that the Blue entrypoints transfer the target net amount. methods { function _.transferFrom(address from, address to, uint256 amount) external => cvlTransferFrom(calledContract, from, to, amount) expect(bool); @@ -13,18 +12,13 @@ methods { function _.flashLoan(address token, uint256 assets, bytes data) external => summaryFlashLoan(token, assets, data) expect void; function _.deposit() external with(env e) => summaryWrapNative(calledContract, e.msg.value) expect void; - // The public allocator charges the caller mulDivUp(assets, penalty, WAD) of the destination - // loan token and sends it to the vault, and moves no other token of the caller. Proven of the - // implementation by BluePublicAllocatorPenalty.spec. Its revert conditions are dropped, which - // only widens the set of verified executions. + // Assume public allocations only charge their penalty. function _.reallocate(address vault, address deallocateAdapter, BlueBundlesV1.MarketParams deallocateMarketParams, address allocateAdapter, BlueBundlesV1.MarketParams allocateMarketParams, uint128 assets, uint64 penalty) external => summaryPublicAllocation(allocateMarketParams.loanToken, vault, assets, penalty) expect void; function _.allocateFromIdle(address vault, address adapter, BlueBundlesV1.MarketParams marketParams, uint128 assets, uint64 penalty) external => summaryPublicAllocation(marketParams.loanToken, vault, assets, penalty) expect void; function _.setAuthorizationWithSig(BlueBundlesV1.Authorization authorization, BlueBundlesV1.Signature signature) external => NONDET; function _.nonce(address authorizer) external => NONDET; - // Only reverts, and reads no state that the property depends on: skipping it verifies a - // superset of the executions (over-approximation), and drops the market id hashing, the - // oracle price call and two symbolic-divisor divisions. + // Assume that requireMaxLtv does not revert. function BlueBundlesV1.requireMaxLtv(BlueBundlesV1.MarketParams memory marketParams, address sender, uint256 maxLtv) internal => NONDET; function TokenLib.safeApprove(address token, address spender, uint256 value) internal => NONDET; @@ -32,8 +26,7 @@ methods { function UtilsLib.mulDivDown(uint256 x, uint256 y, uint256 d) internal returns (uint256) => summaryMulDivDown(x, y, d); } -// The bundler and the public allocator compute the penalty with the same rounding-up division, so -// both sides of the summary above use this one uninterpreted function. +// Assume the bundler and public allocator use the same penalty calculation. persistent ghost mulDivUpG(uint256, uint256, uint256) returns uint256; persistent ghost mapping(address => mathint) bundlerBalance; @@ -47,7 +40,6 @@ function summaryMulDivDown(uint256 a, uint256 b, uint256 d) returns uint256 { revert(); } - // a * b <= max_uint256 and d >= 1 above, so the result fits. return require_uint256(a * b / d); } @@ -113,12 +105,7 @@ function sumPenaltyAssets(BlueBundlesV1.PublicAllocations[] reallocations) retur } } -// The inverse formula documented on both entrypoints: the gross amount floor(t * WAD / (WAD - pct)) -// nets exactly t once the fee is taken. Proven on its own, with no contract call in the query, so -// that the entrypoint rules below can take the relation as a hypothesis and discharge their assert -// by congruence instead of re-deriving this nonlinear identity inside a far larger query. Those -// rules quantify over every gross amount satisfying the relation, so the two together give the -// original statement. +// Check that grossing up the target amount offsets the referral fee. rule referralFeeInversion(uint256 targetNet, uint256 referralFeePct) { require referralFeePct < WAD(); @@ -127,6 +114,7 @@ rule referralFeeInversion(uint256 targetNet, uint256 referralFeePct) { assert grossAssets - summaryMulDivDown(grossAssets, referralFeePct, WAD()) == targetNet; } +// Check that withdrawing transfers the target amount and leaves no residue. rule blueBundlesV1WithdrawReturnsTargetNet(env e, BlueBundlesV1.MarketParams marketParams, BlueBundlesV1.SignedAuthorization signedAuthorization, BlueBundlesV1.PublicAllocations[] reallocations, uint256 referralFeePct, address referralFeeRecipient, uint256 deadline, uint256 targetNet) { require e.msg.sender != currentContract; require referralFeeRecipient != currentContract; @@ -146,6 +134,7 @@ rule blueBundlesV1WithdrawReturnsTargetNet(env e, BlueBundlesV1.MarketParams mar assert recipientBalance[marketParams.loanToken][e.msg.sender] - userBefore == targetNet; } +// Check that borrowing transfers the target amount and leaves no residue. rule blueBundlesV1SupplyCollateralAndBorrowReturnsTargetNet(env e, BlueBundlesV1.MarketParams marketParams, uint256 collateralAssets, uint256 maxLtv, TokenLib.TokenPermit collateralPermit, BlueBundlesV1.SignedAuthorization signedAuthorization, BlueBundlesV1.PublicAllocations[] reallocations, uint256 referralFeePct, address referralFeeRecipient, uint256 deadline, uint256 targetNet) { require e.msg.sender != currentContract; require referralFeeRecipient != currentContract; From f0885f6c432e5d22c0c60bf9a14821b154159e98 Mon Sep 17 00:00:00 2001 From: Bhargav Date: Thu, 27 Aug 2026 14:49:25 +0200 Subject: [PATCH 10/11] make require_unit256 (grossAsset + penaltyAsset) explicit --- certora/specs/BlueNetAmountInvertibility.spec | 46 +++++++++++-------- 1 file changed, 27 insertions(+), 19 deletions(-) diff --git a/certora/specs/BlueNetAmountInvertibility.spec b/certora/specs/BlueNetAmountInvertibility.spec index 187769e..35fbe4a 100644 --- a/certora/specs/BlueNetAmountInvertibility.spec +++ b/certora/specs/BlueNetAmountInvertibility.spec @@ -15,6 +15,8 @@ methods { // Assume public allocations only charge their penalty. function _.reallocate(address vault, address deallocateAdapter, BlueBundlesV1.MarketParams deallocateMarketParams, address allocateAdapter, BlueBundlesV1.MarketParams allocateMarketParams, uint128 assets, uint64 penalty) external => summaryPublicAllocation(allocateMarketParams.loanToken, vault, assets, penalty) expect void; function _.allocateFromIdle(address vault, address adapter, BlueBundlesV1.MarketParams marketParams, uint128 assets, uint64 penalty) external => summaryPublicAllocation(marketParams.loanToken, vault, assets, penalty) expect void; + + // Ignore Blue authorization state. function _.setAuthorizationWithSig(BlueBundlesV1.Authorization authorization, BlueBundlesV1.Signature signature) external => NONDET; function _.nonce(address authorizer) external => NONDET; @@ -40,7 +42,11 @@ function summaryMulDivDown(uint256 a, uint256 b, uint256 d) returns uint256 { revert(); } - return require_uint256(a * b / d); + return assert_uint256(a * b / d); +} + +function referralFeeInversionHolds(uint256 grossAssets, uint256 referralFeePct, uint256 targetNet) returns bool { + return grossAssets - summaryMulDivDown(grossAssets, referralFeePct, WAD()) == targetNet; } function cvlTransferFrom(address token, address from, address to, uint256 amount) returns bool { @@ -74,7 +80,7 @@ function summaryBorrow(address token, uint256 assets, uint256 shares, address re } function summaryWithdraw(address token, uint256 assets, uint256 shares, address receiver) returns (uint256, uint256) { - require shares == 0; + assert shares == 0; if (receiver == currentContract) bundlerBalance[token] = bundlerBalance[token] + assets; uint256 returnedShares; return (assets, returnedShares); @@ -87,12 +93,12 @@ function summaryFlashLoan(address token, uint256 assets, bytes data) { bundlerBalance[token] = bundlerBalance[token] - assets; } -function reallocationsAssumptions(BlueBundlesV1.PublicAllocations[] reallocations, address recipient) { +function reallocationsAssumptions(BlueBundlesV1.PublicAllocations[] reallocations, address caller) { require reallocations.length <= 2, "loop bound"; require reallocations.length > 0 => reallocations[0].vault != currentContract, "bundler is not a vault"; require reallocations.length > 1 => reallocations[1].vault != currentContract, "bundler is not a vault"; - require reallocations.length > 0 => reallocations[0].vault != recipient, "recipient is not a vault"; - require reallocations.length > 1 => reallocations[1].vault != recipient, "recipient is not a vault"; + require reallocations.length > 0 => reallocations[0].vault != caller, "no penalty to caller"; + require reallocations.length > 1 => reallocations[1].vault != caller, "no penalty to caller"; } function sumPenaltyAssets(BlueBundlesV1.PublicAllocations[] reallocations) returns mathint { @@ -107,28 +113,29 @@ function sumPenaltyAssets(BlueBundlesV1.PublicAllocations[] reallocations) retur // Check that grossing up the target amount offsets the referral fee. rule referralFeeInversion(uint256 targetNet, uint256 referralFeePct) { - require referralFeePct < WAD(); + require referralFeePct < WAD(), "valid fee"; uint256 grossAssets = summaryMulDivDown(targetNet, WAD(), assert_uint256(WAD() - referralFeePct)); - assert grossAssets - summaryMulDivDown(grossAssets, referralFeePct, WAD()) == targetNet; + assert referralFeeInversionHolds(grossAssets, referralFeePct, targetNet); } // Check that withdrawing transfers the target amount and leaves no residue. rule blueBundlesV1WithdrawReturnsTargetNet(env e, BlueBundlesV1.MarketParams marketParams, BlueBundlesV1.SignedAuthorization signedAuthorization, BlueBundlesV1.PublicAllocations[] reallocations, uint256 referralFeePct, address referralFeeRecipient, uint256 deadline, uint256 targetNet) { - require e.msg.sender != currentContract; - require referralFeeRecipient != currentContract; - require referralFeeRecipient != e.msg.sender; - require referralFeePct < WAD(); + require e.msg.sender != currentContract, "external caller"; + require referralFeeRecipient != currentContract, "no fee residue"; + require referralFeeRecipient != e.msg.sender, "separate fee recipient"; reallocationsAssumptions(reallocations, e.msg.sender); mathint penaltyAssets = sumPenaltyAssets(reallocations); uint256 grossAssets; - require grossAssets - summaryMulDivDown(grossAssets, referralFeePct, WAD()) == targetNet, "referralFeeInversion"; + require referralFeeInversionHolds(grossAssets, referralFeePct, targetNet), "see referralFeeInversion"; + mathint withdrawAssets = penaltyAssets + grossAssets; + require withdrawAssets <= max_uint256, "valid uint256 input"; mathint before = bundlerBalance[marketParams.loanToken]; mathint userBefore = recipientBalance[marketParams.loanToken][e.msg.sender]; - blueBundlesV1Withdraw(e, marketParams, require_uint256(penaltyAssets + grossAssets), 0, signedAuthorization, reallocations, referralFeePct, referralFeeRecipient, deadline); + blueBundlesV1Withdraw(e, marketParams, assert_uint256(withdrawAssets), 0, signedAuthorization, reallocations, referralFeePct, referralFeeRecipient, deadline); assert bundlerBalance[marketParams.loanToken] == before; assert recipientBalance[marketParams.loanToken][e.msg.sender] - userBefore == targetNet; @@ -136,19 +143,20 @@ rule blueBundlesV1WithdrawReturnsTargetNet(env e, BlueBundlesV1.MarketParams mar // Check that borrowing transfers the target amount and leaves no residue. rule blueBundlesV1SupplyCollateralAndBorrowReturnsTargetNet(env e, BlueBundlesV1.MarketParams marketParams, uint256 collateralAssets, uint256 maxLtv, TokenLib.TokenPermit collateralPermit, BlueBundlesV1.SignedAuthorization signedAuthorization, BlueBundlesV1.PublicAllocations[] reallocations, uint256 referralFeePct, address referralFeeRecipient, uint256 deadline, uint256 targetNet) { - require e.msg.sender != currentContract; - require referralFeeRecipient != currentContract; - require referralFeeRecipient != e.msg.sender; - require referralFeePct < WAD(); + require e.msg.sender != currentContract, "external caller"; + require referralFeeRecipient != currentContract, "no fee residue"; + require referralFeeRecipient != e.msg.sender, "separate fee recipient"; reallocationsAssumptions(reallocations, e.msg.sender); mathint penaltyAssets = sumPenaltyAssets(reallocations); uint256 grossAssets; - require grossAssets - summaryMulDivDown(grossAssets, referralFeePct, WAD()) == targetNet, "referralFeeInversion"; + require referralFeeInversionHolds(grossAssets, referralFeePct, targetNet), "see referralFeeInversion"; + mathint borrowAssets = penaltyAssets + grossAssets; + require borrowAssets <= max_uint256, "valid uint256 input"; mathint before = bundlerBalance[marketParams.loanToken]; mathint userBefore = recipientBalance[marketParams.loanToken][e.msg.sender]; - blueBundlesV1SupplyCollateralAndBorrow(e, marketParams, collateralAssets, require_uint256(penaltyAssets + grossAssets), maxLtv, collateralPermit, signedAuthorization, reallocations, referralFeePct, referralFeeRecipient, deadline); + blueBundlesV1SupplyCollateralAndBorrow(e, marketParams, collateralAssets, assert_uint256(borrowAssets), maxLtv, collateralPermit, signedAuthorization, reallocations, referralFeePct, referralFeeRecipient, deadline); assert bundlerBalance[marketParams.loanToken] == before; assert recipientBalance[marketParams.loanToken][e.msg.sender] - userBefore == targetNet; From 1545a0115a303df397c1795feb2871fe44119abb Mon Sep 17 00:00:00 2001 From: Bhargav Date: Thu, 27 Aug 2026 15:53:05 +0200 Subject: [PATCH 11/11] attempt at matching variable name to bundle natspec --- certora/specs/BlueNetAmountInvertibility.spec | 31 ++++++++++--------- 1 file changed, 16 insertions(+), 15 deletions(-) diff --git a/certora/specs/BlueNetAmountInvertibility.spec b/certora/specs/BlueNetAmountInvertibility.spec index 35fbe4a..f6c4604 100644 --- a/certora/specs/BlueNetAmountInvertibility.spec +++ b/certora/specs/BlueNetAmountInvertibility.spec @@ -45,8 +45,8 @@ function summaryMulDivDown(uint256 a, uint256 b, uint256 d) returns uint256 { return assert_uint256(a * b / d); } -function referralFeeInversionHolds(uint256 grossAssets, uint256 referralFeePct, uint256 targetNet) returns bool { - return grossAssets - summaryMulDivDown(grossAssets, referralFeePct, WAD()) == targetNet; +function referralFeeInversionHolds(uint256 receivedAssets, uint256 referralFeePct, uint256 targetAssets) returns bool { + return receivedAssets - summaryMulDivDown(receivedAssets, referralFeePct, WAD()) == targetAssets; } function cvlTransferFrom(address token, address from, address to, uint256 amount) returns bool { @@ -112,25 +112,26 @@ function sumPenaltyAssets(BlueBundlesV1.PublicAllocations[] reallocations) retur } // Check that grossing up the target amount offsets the referral fee. -rule referralFeeInversion(uint256 targetNet, uint256 referralFeePct) { +rule referralFeeInversion(uint256 targetAssets, uint256 referralFeePct) { require referralFeePct < WAD(), "valid fee"; - uint256 grossAssets = summaryMulDivDown(targetNet, WAD(), assert_uint256(WAD() - referralFeePct)); + uint256 receivedAssets = + summaryMulDivDown(targetAssets, WAD(), assert_uint256(WAD() - referralFeePct)); - assert referralFeeInversionHolds(grossAssets, referralFeePct, targetNet); + assert referralFeeInversionHolds(receivedAssets, referralFeePct, targetAssets); } // Check that withdrawing transfers the target amount and leaves no residue. -rule blueBundlesV1WithdrawReturnsTargetNet(env e, BlueBundlesV1.MarketParams marketParams, BlueBundlesV1.SignedAuthorization signedAuthorization, BlueBundlesV1.PublicAllocations[] reallocations, uint256 referralFeePct, address referralFeeRecipient, uint256 deadline, uint256 targetNet) { +rule blueBundlesV1WithdrawReturnsTargetNet(env e, BlueBundlesV1.MarketParams marketParams, BlueBundlesV1.SignedAuthorization signedAuthorization, BlueBundlesV1.PublicAllocations[] reallocations, uint256 referralFeePct, address referralFeeRecipient, uint256 deadline, uint256 targetAssets) { require e.msg.sender != currentContract, "external caller"; require referralFeeRecipient != currentContract, "no fee residue"; require referralFeeRecipient != e.msg.sender, "separate fee recipient"; reallocationsAssumptions(reallocations, e.msg.sender); mathint penaltyAssets = sumPenaltyAssets(reallocations); - uint256 grossAssets; - require referralFeeInversionHolds(grossAssets, referralFeePct, targetNet), "see referralFeeInversion"; - mathint withdrawAssets = penaltyAssets + grossAssets; + uint256 receivedAssets; + require referralFeeInversionHolds(receivedAssets, referralFeePct, targetAssets), "see referralFeeInversion"; + mathint withdrawAssets = penaltyAssets + receivedAssets; require withdrawAssets <= max_uint256, "valid uint256 input"; mathint before = bundlerBalance[marketParams.loanToken]; mathint userBefore = recipientBalance[marketParams.loanToken][e.msg.sender]; @@ -138,20 +139,20 @@ rule blueBundlesV1WithdrawReturnsTargetNet(env e, BlueBundlesV1.MarketParams mar blueBundlesV1Withdraw(e, marketParams, assert_uint256(withdrawAssets), 0, signedAuthorization, reallocations, referralFeePct, referralFeeRecipient, deadline); assert bundlerBalance[marketParams.loanToken] == before; - assert recipientBalance[marketParams.loanToken][e.msg.sender] - userBefore == targetNet; + assert recipientBalance[marketParams.loanToken][e.msg.sender] - userBefore == targetAssets; } // Check that borrowing transfers the target amount and leaves no residue. -rule blueBundlesV1SupplyCollateralAndBorrowReturnsTargetNet(env e, BlueBundlesV1.MarketParams marketParams, uint256 collateralAssets, uint256 maxLtv, TokenLib.TokenPermit collateralPermit, BlueBundlesV1.SignedAuthorization signedAuthorization, BlueBundlesV1.PublicAllocations[] reallocations, uint256 referralFeePct, address referralFeeRecipient, uint256 deadline, uint256 targetNet) { +rule blueBundlesV1SupplyCollateralAndBorrowReturnsTargetNet(env e, BlueBundlesV1.MarketParams marketParams, uint256 collateralAssets, uint256 maxLtv, TokenLib.TokenPermit collateralPermit, BlueBundlesV1.SignedAuthorization signedAuthorization, BlueBundlesV1.PublicAllocations[] reallocations, uint256 referralFeePct, address referralFeeRecipient, uint256 deadline, uint256 targetAssets) { require e.msg.sender != currentContract, "external caller"; require referralFeeRecipient != currentContract, "no fee residue"; require referralFeeRecipient != e.msg.sender, "separate fee recipient"; reallocationsAssumptions(reallocations, e.msg.sender); mathint penaltyAssets = sumPenaltyAssets(reallocations); - uint256 grossAssets; - require referralFeeInversionHolds(grossAssets, referralFeePct, targetNet), "see referralFeeInversion"; - mathint borrowAssets = penaltyAssets + grossAssets; + uint256 receivedAssets; + require referralFeeInversionHolds(receivedAssets, referralFeePct, targetAssets), "see referralFeeInversion"; + mathint borrowAssets = penaltyAssets + receivedAssets; require borrowAssets <= max_uint256, "valid uint256 input"; mathint before = bundlerBalance[marketParams.loanToken]; mathint userBefore = recipientBalance[marketParams.loanToken][e.msg.sender]; @@ -159,5 +160,5 @@ rule blueBundlesV1SupplyCollateralAndBorrowReturnsTargetNet(env e, BlueBundlesV1 blueBundlesV1SupplyCollateralAndBorrow(e, marketParams, collateralAssets, assert_uint256(borrowAssets), maxLtv, collateralPermit, signedAuthorization, reallocations, referralFeePct, referralFeeRecipient, deadline); assert bundlerBalance[marketParams.loanToken] == before; - assert recipientBalance[marketParams.loanToken][e.msg.sender] - userBefore == targetNet; + assert recipientBalance[marketParams.loanToken][e.msg.sender] - userBefore == targetAssets; }