diff --git a/certora/confs/BlueNetAmountInvertibility.conf b/certora/confs/BlueNetAmountInvertibility.conf new file mode 100644 index 0000000..fb70d86 --- /dev/null +++ b/certora/confs/BlueNetAmountInvertibility.conf @@ -0,0 +1,24 @@ +{ + "files": [ + "src/blue/BlueBundlesV1.sol" + ], + "verify": "BlueBundlesV1:certora/specs/BlueNetAmountInvertibility.spec", + "packages": [ + "lib/vault-v2/lib/morpho-blue=lib/morpho-blue" + ], + "solc": "solc-0.8.34", + "solc_via_ir": true, + "solc_evm_version": "osaka", + "use_relpaths_for_solc_json": true, + "optimistic_loop": true, + "optimistic_fallback": true, + "loop_iter": 2, + "msg": "BlueBundles: net amount inversion with public allocator penalties", + "prover_args": [ + "-splitParallel true", + "-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..f6c4604 --- /dev/null +++ b/certora/specs/BlueNetAmountInvertibility.spec @@ -0,0 +1,164 @@ +// SPDX-License-Identifier: GPL-2.0-or-later + +// 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); + 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 _.deposit() external with(env e) => summaryWrapNative(calledContract, e.msg.value) expect void; + + // 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; + + // 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; + + function UtilsLib.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); +} + +// 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; + +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(); + } + + return assert_uint256(a * b / d); +} + +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 { + 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 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) { + cvlTransferFrom(token, from, to, amount); +} + +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; + uint256 returnedShares; + return (assets, returnedShares); +} + +function summaryWithdraw(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 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, 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 != caller, "no penalty to caller"; + require reallocations.length > 1 => reallocations[1].vault != caller, "no penalty to caller"; +} + +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()); + } else if (reallocations.length > 0) { + return mulDivUpG(reallocations[0].assets, reallocations[0].penalty, WAD()); + } else { + return 0; + } +} + +// Check that grossing up the target amount offsets the referral fee. +rule referralFeeInversion(uint256 targetAssets, uint256 referralFeePct) { + require referralFeePct < WAD(), "valid fee"; + + uint256 receivedAssets = + summaryMulDivDown(targetAssets, WAD(), assert_uint256(WAD() - referralFeePct)); + + 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 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 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]; + + 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 == 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 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 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]; + + 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 == targetAssets; +}