diff --git a/.gitignore b/.gitignore index 87b0c77..62568bb 100644 --- a/.gitignore +++ b/.gitignore @@ -5,6 +5,4 @@ broadcast/ *.swp .DS_Store node_modules/ - -# Certora local run cache .certora_internal/ diff --git a/certora/confs/MidnightBundlesBalance.conf b/certora/confs/MidnightBundlesBalance.conf new file mode 100644 index 0000000..732678b --- /dev/null +++ b/certora/confs/MidnightBundlesBalance.conf @@ -0,0 +1,23 @@ +{ + "files": [ + "lib/midnight/certora/helpers/Utils.sol", + "src/midnight/MidnightBundles.sol" + ], + "verify": "MidnightBundles:certora/specs/MidnightBundlesBalance.spec", + "split_rules": [ + "*" + ], + "solc": "solc-0.8.34", + "solc_via_ir": true, + "solc_evm_version": "osaka", + "optimistic_loop": true, + "loop_iter": 2, + "optimistic_hashing": true, + "hashing_length_bound": 2048, + "prover_args": [ + "-havocAllByDefault true", + "-s [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5}]", + "-splitParallel true" + ], + "msg": "MidnightBundles balance neutrality" +} diff --git a/certora/specs/MidnightBundlesBalance.spec b/certora/specs/MidnightBundlesBalance.spec new file mode 100644 index 0000000..ae469ce --- /dev/null +++ b/certora/specs/MidnightBundlesBalance.spec @@ -0,0 +1,170 @@ +// SPDX-License-Identifier: GPL-2.0-or-later + +using Utils as Utils; + +methods { + function Utils.hashMarket(MidnightBundles.Market market) external returns (bytes32) envfree; + + // Over-approximate view functions. + function TakeAmountsLib.sellerAssetsToUnits(address, bytes32, MidnightBundles.Offer memory, uint256) internal returns (uint256) => NONDET; + function TakeAmountsLib.buyerAssetsToUnits(address, bytes32, MidnightBundles.Offer memory, uint256) internal returns (uint256) => NONDET; + function ConsumableUnitsLib.consumableUnits(address, bytes32, MidnightBundles.Offer memory) internal returns (uint256) => NONDET; + function _.toId(MidnightBundles.Market) external => NONDET; + + // Allowances are not modeled, so ignore this side-effect. + function TokenLib.forceApproveMax(address token, address spender) internal => NONDET; + + // Token modeling. + function SafeTransferLib.safeTransfer(address token, address receiver, uint256 amount) internal => summarySafeTransfer(token, receiver, amount); + function SafeTransferLib.safeTransferFrom(address token, address from, address to, uint256 amount) internal => summarySafeTransferFrom(token, from, to, amount); + function TokenLib.pullToken(address token, address from, uint256 amount, MidnightBundles.TokenPermit memory permit) internal => summaryPullToken(token, from, amount); + function _.take(MidnightBundles.Offer offer, bytes ratifierData, uint256 units, address taker, address receiverIfTakerIsSeller, address takerCallback, bytes takerCallbackData) external with(env e) => summaryTake(e.msg.sender, offer, taker, receiverIfTakerIsSeller, takerCallback) expect(uint256, uint256); + function _.repay(MidnightBundles.Market, uint256 units, address, address, bytes) external => summaryRepay(units) expect void; +} + +/// HELPERS /// + +persistent ghost mapping(address => mapping(address => uint256)) tokenBalance; + +function summaryPullToken(address token, address from, uint256 amount) { + summarySafeTransferFrom(token, from, currentContract, amount); +} + +function summarySafeTransfer(address token, address to, uint256 amount) { + summarySafeTransferFrom(token, currentContract, to, amount); +} + +function summarySafeTransferFrom(address token, address from, address to, uint256 amount) { + if (amount > tokenBalance[token][from] || amount + tokenBalance[token][to] > max_uint256) { + revert(); + } + tokenBalance[token][from] = assert_uint256(tokenBalance[token][from] - amount); + tokenBalance[token][to] = assert_uint256(tokenBalance[token][to] + amount); +} + +persistent ghost mathint boughtAssets; + +persistent ghost mathint soldAssets; + +persistent ghost mathint repaidAssets; + +function summaryTake(address msgSender, MidnightBundles.Offer offer, address taker, address receiverIfTakerIsSeller, address takerCallback) returns (uint256, uint256) { + uint256 buyerAssets; + uint256 sellerAssets; + boughtAssets = boughtAssets + buyerAssets; + soldAssets = soldAssets + sellerAssets; + return (buyerAssets, sellerAssets); +} + +function summaryRepay(uint256 units) { + repaidAssets = repaidAssets + units; +} + +/// RULES /// + +rule buyWithUnitsTargetAndWithdrawCollateralDoesntLoseTokens(env e, uint256 targetUnits, uint256 maxBuyerAssets, address taker, MidnightBundles.TokenPermit loanTokenPermit, MidnightBundles.Take[] takes, MidnightBundles.CollateralWithdrawal[] collateralWithdrawals, address collateralReceiver, uint256 referralFeePct, address referralFeeRecipient) { + address loanToken = takes[0].offer.market.loanToken; + + // Assume different addresses to have correct accounting, using hardcoded addresses as a trick. + require e.msg.sender == 11, "ack"; + require referralFeeRecipient == 12, "ack"; + require currentContract == 13, "ack"; + + boughtAssets = 0; + uint256 feeBalanceBefore = tokenBalance[loanToken][referralFeeRecipient]; + uint256 balanceBefore = tokenBalance[loanToken][e.msg.sender]; + buyWithUnitsTargetAndWithdrawCollateral(e, targetUnits, maxBuyerAssets, e.msg.sender, loanTokenPermit, takes, collateralWithdrawals, collateralReceiver, referralFeePct, referralFeeRecipient); + uint256 balanceAfter = tokenBalance[loanToken][e.msg.sender]; + uint256 feeBalanceAfter = tokenBalance[loanToken][referralFeeRecipient]; + + mathint spent = balanceBefore - balanceAfter; + mathint fees = feeBalanceAfter - feeBalanceBefore; + + assert spent == boughtAssets + fees; +} + +rule buyWithAssetsTargetAndWithdrawCollateralDoesntLoseTokens(env e, uint256 targetBuyerAssets, uint256 minUnits, MidnightBundles.TokenPermit loanTokenPermit, MidnightBundles.Take[] takes, MidnightBundles.CollateralWithdrawal[] collateralWithdrawals, address collateralReceiver, uint256 referralFeePct, address referralFeeRecipient) { + address loanToken = takes[0].offer.market.loanToken; + + // Assume different addresses to have correct accounting, using hardcoded addresses as a trick. + require e.msg.sender == 11, "ack"; + require referralFeeRecipient == 12, "ack"; + require currentContract == 13, "ack"; + + boughtAssets = 0; + uint256 feeBalanceBefore = tokenBalance[loanToken][referralFeeRecipient]; + uint256 balanceBefore = tokenBalance[loanToken][e.msg.sender]; + buyWithAssetsTargetAndWithdrawCollateral(e, targetBuyerAssets, minUnits, e.msg.sender, loanTokenPermit, takes, collateralWithdrawals, collateralReceiver, referralFeePct, referralFeeRecipient); + uint256 balanceAfter = tokenBalance[loanToken][e.msg.sender]; + uint256 feeBalanceAfter = tokenBalance[loanToken][referralFeeRecipient]; + + mathint spent = balanceBefore - balanceAfter; + mathint fees = feeBalanceAfter - feeBalanceBefore; + + assert spent == boughtAssets + fees; +} + +rule supplyCollateralAndSellWithUnitsTargetDoesntLoseTokens(env e, uint256 targetUnits, uint256 minSellerAssets, address receiver, MidnightBundles.CollateralSupply[] collateralSupplies, MidnightBundles.Take[] takes, uint256 referralFeePct, address referralFeeRecipient) { + address loanToken = takes[0].offer.market.loanToken; + + // Assume different addresses to have correct accounting, using hardcoded addresses as a trick. + require receiver == 11, "ack"; + require referralFeeRecipient == 12, "ack"; + require currentContract == 13, "ack"; + require e.msg.sender == 14, "ack"; + + soldAssets = 0; + uint256 feeBalanceBefore = tokenBalance[loanToken][referralFeeRecipient]; + uint256 receiverBalanceBefore = tokenBalance[loanToken][receiver]; + supplyCollateralAndSellWithUnitsTarget(e, targetUnits, minSellerAssets, e.msg.sender, receiver, collateralSupplies, takes, referralFeePct, referralFeeRecipient); + uint256 receiverBalanceAfter = tokenBalance[loanToken][receiver]; + uint256 feeBalanceAfter = tokenBalance[loanToken][referralFeeRecipient]; + + mathint received = receiverBalanceAfter - receiverBalanceBefore; + mathint fees = feeBalanceAfter - feeBalanceBefore; + + assert received == soldAssets - fees; +} + +rule supplyCollateralAndSellWithAssetsTargetDoesntLoseTokens(env e, uint256 targetSellerAssets, uint256 maxUnits, address receiver, MidnightBundles.CollateralSupply[] collateralSupplies, MidnightBundles.Take[] takes, uint256 referralFeePct, address referralFeeRecipient) { + address loanToken = takes[0].offer.market.loanToken; + + // Assume different addresses to have correct accounting, using hardcoded addresses as a trick. + require receiver == 11, "ack"; + require referralFeeRecipient == 12, "ack"; + require currentContract == 13, "ack"; + require e.msg.sender == 14, "ack"; + + soldAssets = 0; + uint256 feeBalanceBefore = tokenBalance[loanToken][referralFeeRecipient]; + uint256 receiverBalanceBefore = tokenBalance[loanToken][receiver]; + supplyCollateralAndSellWithAssetsTarget(e, targetSellerAssets, maxUnits, e.msg.sender, receiver, collateralSupplies, takes, referralFeePct, referralFeeRecipient); + uint256 receiverBalanceAfter = tokenBalance[loanToken][receiver]; + uint256 feeBalanceAfter = tokenBalance[loanToken][referralFeeRecipient]; + + mathint received = receiverBalanceAfter - receiverBalanceBefore; + mathint fees = feeBalanceAfter - feeBalanceBefore; + + assert received == soldAssets - fees; +} + +rule repayAndWithdrawCollateralDoesntLoseTokens(env e, MidnightBundles.Market market, uint256 assets, MidnightBundles.TokenPermit loanTokenPermit, MidnightBundles.CollateralWithdrawal[] collateralWithdrawals, address collateralReceiver, uint256 referralFeePct, address referralFeeRecipient) { + address loanToken = market.loanToken; + + // Assume different addresses to have correct accounting, using hardcoded addresses as a trick. + require e.msg.sender == 11, "ack"; + require referralFeeRecipient == 12, "ack"; + require currentContract == 13, "ack"; + + repaidAssets = 0; + uint256 feeBalanceBefore = tokenBalance[loanToken][referralFeeRecipient]; + uint256 balanceBefore = tokenBalance[loanToken][e.msg.sender]; + repayAndWithdrawCollateral(e, market, assets, e.msg.sender, loanTokenPermit, collateralWithdrawals, collateralReceiver, referralFeePct, referralFeeRecipient); + uint256 balanceAfter = tokenBalance[loanToken][e.msg.sender]; + uint256 feeBalanceAfter = tokenBalance[loanToken][referralFeeRecipient]; + + mathint spent = balanceBefore - balanceAfter; + mathint fees = feeBalanceAfter - feeBalanceBefore; + + assert spent == repaidAssets + fees; +}