From 78e3bfe8de7c0e803fc0a90b33df7f7459f63685 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Thu, 11 Jun 2026 16:40:46 +0200 Subject: [PATCH 01/18] initial rule --- .github/workflows/certora.yml | 87 +++++++++++++++++++++++ certora/README.md | 13 ++++ certora/confs/MidnightBundlesBalance.conf | 19 +++++ certora/specs/MidnightBundlesBalance.spec | 50 +++++++++++++ 4 files changed, 169 insertions(+) create mode 100644 .github/workflows/certora.yml create mode 100644 certora/README.md create mode 100644 certora/confs/MidnightBundlesBalance.conf create mode 100644 certora/specs/MidnightBundlesBalance.spec diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml new file mode 100644 index 0000000..61ab056 --- /dev/null +++ b/.github/workflows/certora.yml @@ -0,0 +1,87 @@ +name: certora + +on: + push: + branches: + - main + pull_request: + workflow_dispatch: + +jobs: + format: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6 + + - uses: actions/setup-java@be666c2fcd27ec809703dec50e508c2fdc7f6654 # v5 + with: + distribution: temurin + java-version: "21" + + - uses: actions/setup-python@a309ff8b426b58ec0e2a45f0f869d46889d02405 # v6 + with: + python-version: ">=3.11" + + - name: Install certora + run: pip install certora-cli + + - name: Run Certora Specs Linter + run: | + for file in certora/specs/*.spec; do + echo "Fix lint errors by applying the following diff to $file:" + diff -u "$file" <(certoraCVLFormatter "$file") + done + + matrix: + runs-on: ubuntu-latest + outputs: + confs: ${{ steps.list.outputs.confs }} + steps: + - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6 + + - id: list + run: echo "confs=$(ls certora/confs/*.conf | xargs -I{} basename {} .conf | jq -nRc '[inputs]')" >> "$GITHUB_OUTPUT" + + verify: + needs: [matrix, format] + runs-on: ubuntu-latest + strategy: + fail-fast: false + matrix: + conf: ${{ fromJson(needs.matrix.outputs.confs) }} + + steps: + - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6 + + - uses: actions/setup-java@be666c2fcd27ec809703dec50e508c2fdc7f6654 # v5 + with: + distribution: temurin + java-version: "21" + + - name: Run Certora Config Linter + run: | + file="certora/confs/${{ matrix.conf }}.conf" + echo "Fix lint errors by applying the following diff to $file:" + diff -u "$file" <(jq < "$file") + + - uses: actions/setup-python@a309ff8b426b58ec0e2a45f0f869d46889d02405 # v6 + with: + python-version: ">=3.11" + + - name: Install certora + run: pip install certora-cli + + - name: Install solc (0.8.34) + env: + EXPECTED_SOLC_SHA256: d40adc6f9fdbb22a97d32a02fa05688bf2ee7886affc48c9851b0afd4a726b39 + run: | + wget https://github.com/ethereum/solidity/releases/download/v0.8.34/solc-static-linux + actual="$(sha256sum solc-static-linux | awk '{print $1}')" + [ "$actual" = "$EXPECTED_SOLC_SHA256" ] || { echo "solc hash mismatch"; exit 1; } + chmod +x solc-static-linux + sudo mv solc-static-linux /usr/local/bin/solc-0.8.34 + + - name: Verify ${{ matrix.conf }} + run: certoraRun certora/confs/${{ matrix.conf }}.conf + env: + CERTORAKEY: ${{ secrets.CERTORAKEY }} diff --git a/certora/README.md b/certora/README.md new file mode 100644 index 0000000..aa5c61e --- /dev/null +++ b/certora/README.md @@ -0,0 +1,13 @@ +This folder contains the verification of the Midnight protocol using CVL, Certora's Verification Language. + +# Verified properties + +## Core state and invariants + +# Verification setup + +# Getting started + +Install the `certora-cli` package with `pip install certora-cli`. +To verify a spec, pass its configuration file in the [`certora/confs`](confs) folder to `certoraRun`. +It requires having set the `CERTORAKEY` environment variable to a valid Certora key, and to have `solc-0.8.34` in the PATH. diff --git a/certora/confs/MidnightBundlesBalance.conf b/certora/confs/MidnightBundlesBalance.conf new file mode 100644 index 0000000..16f7984 --- /dev/null +++ b/certora/confs/MidnightBundlesBalance.conf @@ -0,0 +1,19 @@ +{ + "files": [ + "src/midnight/MidnightBundles.sol" + ], + "verify": "MidnightBundles:certora/specs/MidnightBundlesBalance.spec", + "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..1614bb5 --- /dev/null +++ b/certora/specs/MidnightBundlesBalance.spec @@ -0,0 +1,50 @@ +// SPDX-License-Identifier: GPL-2.0-or-later + +methods { + 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 _.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); +} + +/// HELPERS /// + +ghost mapping(address => mapping(address => uint256)) tokenBalance; + +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); +} + +ghost uint256 boughtAssets; + +ghost uint256 soldAssets; + +function summaryTake(address msgSender, MidnightBundles.Offer offer, address taker, address receiverIfTakerIsSeller, address takerCallback) returns (uint256, uint256) { + uint256 buyerAssets; + uint256 sellerAssets; + boughtAssets = require_uint256(boughtAssets + buyerAssets); + soldAssets = require_uint256(soldAssets + sellerAssets); + return (buyerAssets, sellerAssets); +} + +/// 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; + + boughtAssets = 0; + + uint256 balanceBefore = tokenBalance[loanToken][taker]; + buyWithUnitsTargetAndWithdrawCollateral(e, targetUnits, maxBuyerAssets, taker, loanTokenPermit, takes, collateralWithdrawals, collateralReceiver, referralFeePct, referralFeeRecipient); + uint256 balanceAfter = tokenBalance[loanToken][taker]; + + assert balanceBefore - balanceAfter == boughtAssets; +} From e00cc09186c9e48a3756c10b6e38b4999445f892 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Thu, 11 Jun 2026 17:24:21 +0200 Subject: [PATCH 02/18] first spec --- certora/confs/MidnightBundlesBalance.conf | 1 + certora/specs/MidnightBundlesBalance.spec | 23 +++++++++++++++++++---- 2 files changed, 20 insertions(+), 4 deletions(-) diff --git a/certora/confs/MidnightBundlesBalance.conf b/certora/confs/MidnightBundlesBalance.conf index 16f7984..7bcc6c9 100644 --- a/certora/confs/MidnightBundlesBalance.conf +++ b/certora/confs/MidnightBundlesBalance.conf @@ -1,5 +1,6 @@ { "files": [ + "lib/midnight/certora/helpers/Utils.sol", "src/midnight/MidnightBundles.sol" ], "verify": "MidnightBundles:certora/specs/MidnightBundlesBalance.spec", diff --git a/certora/specs/MidnightBundlesBalance.spec b/certora/specs/MidnightBundlesBalance.spec index 1614bb5..a049f07 100644 --- a/certora/specs/MidnightBundlesBalance.spec +++ b/certora/specs/MidnightBundlesBalance.spec @@ -1,14 +1,24 @@ // SPDX-License-Identifier: GPL-2.0-or-later +using Utils as Utils; + methods { 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 Utils.hashMarket(MidnightBundles.Market market) external returns (bytes32) envfree; + + function _.toId(MidnightBundles.Market market, uint256, address) external => summaryToId(market) expect(bytes32); + 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); } /// HELPERS /// +function summaryToId(MidnightBundles.Market market) returns (bytes32) { + return Utils.hashMarket(market); +} + ghost mapping(address => mapping(address => uint256)) tokenBalance; function summarySafeTransfer(address token, address to, uint256 amount) { @@ -39,12 +49,17 @@ function summaryTake(address msgSender, MidnightBundles.Offer offer, address tak 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; + address midnight = currentContract.MIDNIGHT; boughtAssets = 0; + uint256 midnightBalanceBefore = tokenBalance[loanToken][midnight]; + 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 midnightBalanceAfter = tokenBalance[loanToken][midnight]; - uint256 balanceBefore = tokenBalance[loanToken][taker]; - buyWithUnitsTargetAndWithdrawCollateral(e, targetUnits, maxBuyerAssets, taker, loanTokenPermit, takes, collateralWithdrawals, collateralReceiver, referralFeePct, referralFeeRecipient); - uint256 balanceAfter = tokenBalance[loanToken][taker]; + mathint spent = balanceBefore - balanceAfter; + mathint fees = midnightBalanceAfter - midnightBalanceBefore; - assert balanceBefore - balanceAfter == boughtAssets; + assert spent == boughtAssets + fees; } From c74733fc28f3f4751ef9b7a9db40104b78e2900f Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Thu, 11 Jun 2026 17:29:22 +0200 Subject: [PATCH 03/18] install submodules for certora --- .github/workflows/certora.yml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml index 61ab056..5ba0ee9 100644 --- a/.github/workflows/certora.yml +++ b/.github/workflows/certora.yml @@ -12,6 +12,8 @@ jobs: runs-on: ubuntu-latest steps: - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6 + with: + submodules: recursive - uses: actions/setup-java@be666c2fcd27ec809703dec50e508c2fdc7f6654 # v5 with: From a7150eaaee6b16dbdc6e4f3785a8935685ed9cb7 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Thu, 11 Jun 2026 17:30:53 +0200 Subject: [PATCH 04/18] recursive for verification --- .github/workflows/certora.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml index 5ba0ee9..008f029 100644 --- a/.github/workflows/certora.yml +++ b/.github/workflows/certora.yml @@ -12,8 +12,6 @@ jobs: runs-on: ubuntu-latest steps: - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6 - with: - submodules: recursive - uses: actions/setup-java@be666c2fcd27ec809703dec50e508c2fdc7f6654 # v5 with: @@ -54,6 +52,8 @@ jobs: steps: - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6 + with: + submodules: recursive - uses: actions/setup-java@be666c2fcd27ec809703dec50e508c2fdc7f6654 # v5 with: From 7f6388aeeca69bc74909ffc1c1a91ef0e507bdc1 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Thu, 11 Jun 2026 17:47:09 +0200 Subject: [PATCH 05/18] fix spec --- certora/specs/MidnightBundlesBalance.spec | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/certora/specs/MidnightBundlesBalance.spec b/certora/specs/MidnightBundlesBalance.spec index a049f07..a626658 100644 --- a/certora/specs/MidnightBundlesBalance.spec +++ b/certora/specs/MidnightBundlesBalance.spec @@ -8,7 +8,7 @@ methods { function Utils.hashMarket(MidnightBundles.Market market) external returns (bytes32) envfree; - function _.toId(MidnightBundles.Market market, uint256, address) external => summaryToId(market) expect(bytes32); + function _.toId(MidnightBundles.Market market) external => summaryToId(market) expect(bytes32); 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); } @@ -25,6 +25,10 @@ function summarySafeTransfer(address token, address to, uint256 amount) { summarySafeTransferFrom(token, currentContract, to, amount); } +function summaryPullToken(address token, address from, uint256 amount, MidnightBundles.TokenPermit permit) { + summarySafeTransferFrom(token, from, currentContract, amount); +} + function summarySafeTransferFrom(address token, address from, address to, uint256 amount) { if (amount > tokenBalance[token][from] || amount + tokenBalance[token][to] > max_uint256) { revert(); From 68993efcfddd8f6d53e08a6ba79b2a02d618c12f Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Thu, 11 Jun 2026 18:12:52 +0200 Subject: [PATCH 06/18] summarize pullToken and tickToPrice --- certora/specs/MidnightBundlesBalance.spec | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/certora/specs/MidnightBundlesBalance.spec b/certora/specs/MidnightBundlesBalance.spec index a626658..aa2c4f1 100644 --- a/certora/specs/MidnightBundlesBalance.spec +++ b/certora/specs/MidnightBundlesBalance.spec @@ -3,13 +3,15 @@ using Utils as Utils; methods { + function Utils.hashMarket(MidnightBundles.Market market) external returns (bytes32) envfree; + + function TickLib.tickToPrice(uint256 tick) internal returns (uint256) => NONDET; + 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 Utils.hashMarket(MidnightBundles.Market market) external returns (bytes32) envfree; + function TokenLib.pullToken(address token, address from, uint256 amount, MidnightBundles.TokenPermit memory permit) internal => summaryPullToken(token, from, amount); function _.toId(MidnightBundles.Market market) external => summaryToId(market) expect(bytes32); - 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); } @@ -25,7 +27,7 @@ function summarySafeTransfer(address token, address to, uint256 amount) { summarySafeTransferFrom(token, currentContract, to, amount); } -function summaryPullToken(address token, address from, uint256 amount, MidnightBundles.TokenPermit permit) { +function summaryPullToken(address token, address from, uint256 amount) { summarySafeTransferFrom(token, from, currentContract, amount); } From 3997efb7fb58bdb1143545643347eb23db8c25b5 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Thu, 11 Jun 2026 18:53:08 +0200 Subject: [PATCH 07/18] summarize havoced functions --- certora/specs/MidnightBundlesBalance.spec | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/certora/specs/MidnightBundlesBalance.spec b/certora/specs/MidnightBundlesBalance.spec index aa2c4f1..86b2bce 100644 --- a/certora/specs/MidnightBundlesBalance.spec +++ b/certora/specs/MidnightBundlesBalance.spec @@ -11,6 +11,10 @@ methods { 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); + // Those calls are assumed to not-reenter. + function TokenLib.safeApprove(address token, address spender, uint256 value) internal => NONDET; + function _.touchMarket(MidnightBundles.Market memory market) internal => NONDET; + function _.toId(MidnightBundles.Market market) external => summaryToId(market) expect(bytes32); 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); } @@ -23,14 +27,14 @@ function summaryToId(MidnightBundles.Market market) returns (bytes32) { ghost mapping(address => mapping(address => uint256)) tokenBalance; -function summarySafeTransfer(address token, address to, uint256 amount) { - summarySafeTransferFrom(token, currentContract, to, amount); -} - 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(); From 4b5a73d6719257857ee254e8f1fe5d116435d572 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Fri, 12 Jun 2026 09:36:48 +0200 Subject: [PATCH 08/18] persistent --- certora/specs/MidnightBundlesBalance.spec | 35 +++++++++++------------ 1 file changed, 17 insertions(+), 18 deletions(-) diff --git a/certora/specs/MidnightBundlesBalance.spec b/certora/specs/MidnightBundlesBalance.spec index 86b2bce..b8d0762 100644 --- a/certora/specs/MidnightBundlesBalance.spec +++ b/certora/specs/MidnightBundlesBalance.spec @@ -7,25 +7,23 @@ methods { function TickLib.tickToPrice(uint256 tick) internal returns (uint256) => NONDET; + function ConsumableUnitsLib.consumableUnits(address midnight, bytes32 id, MidnightBundles.Offer memory offer) internal returns (uint256) => NONDET; + function _.toId(MidnightBundles.Market market) external => NONDET; + 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); - - // Those calls are assumed to not-reenter. - function TokenLib.safeApprove(address token, address spender, uint256 value) internal => NONDET; - function _.touchMarket(MidnightBundles.Market memory market) internal => NONDET; - - function _.toId(MidnightBundles.Market market) external => summaryToId(market) expect(bytes32); 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); } /// HELPERS /// +// Persistent ghosts so that the unresolved external calls to MIDNIGHT (e.g. touchMarket, withdrawCollateral) which are havoc'd by the Prover do not havoc the tracked balances. -function summaryToId(MidnightBundles.Market market) returns (bytes32) { - return Utils.hashMarket(market); -} +persistent ghost mapping(address => mapping(address => uint256)) tokenBalance; -ghost mapping(address => mapping(address => uint256)) tokenBalance; +persistent ghost uint256 boughtAssets; + +persistent ghost uint256 soldAssets; function summaryPullToken(address token, address from, uint256 amount) { summarySafeTransferFrom(token, from, currentContract, amount); @@ -43,10 +41,6 @@ function summarySafeTransferFrom(address token, address from, address to, uint25 tokenBalance[token][to] = assert_uint256(tokenBalance[token][to] + amount); } -ghost uint256 boughtAssets; - -ghost uint256 soldAssets; - function summaryTake(address msgSender, MidnightBundles.Offer offer, address taker, address receiverIfTakerIsSeller, address takerCallback) returns (uint256, uint256) { uint256 buyerAssets; uint256 sellerAssets; @@ -59,17 +53,22 @@ function summaryTake(address msgSender, MidnightBundles.Offer offer, address tak 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; - address midnight = currentContract.MIDNIGHT; + + // The referral fee is paid to a third party, so it only leaves the taker if the recipient is distinct from the + // taker and from the bundler. + require e.msg.sender != currentContract; + require referralFeeRecipient != e.msg.sender; + require referralFeeRecipient != currentContract; boughtAssets = 0; - uint256 midnightBalanceBefore = tokenBalance[loanToken][midnight]; + 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 midnightBalanceAfter = tokenBalance[loanToken][midnight]; + uint256 feeBalanceAfter = tokenBalance[loanToken][referralFeeRecipient]; mathint spent = balanceBefore - balanceAfter; - mathint fees = midnightBalanceAfter - midnightBalanceBefore; + mathint fees = feeBalanceAfter - feeBalanceBefore; assert spent == boughtAssets + fees; } From c2cc9844dfa1ed9d42085dd6de6010882902e9ac Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Fri, 12 Jun 2026 10:45:50 +0200 Subject: [PATCH 09/18] methods summary --- certora/specs/MidnightBundlesBalance.spec | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) diff --git a/certora/specs/MidnightBundlesBalance.spec b/certora/specs/MidnightBundlesBalance.spec index b8d0762..032b152 100644 --- a/certora/specs/MidnightBundlesBalance.spec +++ b/certora/specs/MidnightBundlesBalance.spec @@ -5,11 +5,15 @@ using Utils as Utils; methods { function Utils.hashMarket(MidnightBundles.Market market) external returns (bytes32) envfree; - function TickLib.tickToPrice(uint256 tick) internal returns (uint256) => NONDET; - + // Over-approximate view functions. + function TakeAmountsLib.sellerAssetsToUnits(address midnight, bytes32 id, MidnightBundles.Offer memory offer, uint256 targetSellerAssets) internal returns (uint256) => NONDET; + function TakeAmountsLib.buyerAssetsToUnits(address midnight, bytes32 id, MidnightBundles.Offer memory offer, uint256 buyerAssets) internal returns (uint256) => NONDET; function ConsumableUnitsLib.consumableUnits(address midnight, bytes32 id, MidnightBundles.Offer memory offer) internal returns (uint256) => NONDET; function _.toId(MidnightBundles.Market market) external => NONDET; + // Over-approximate external calls. + function _.touchMarket(MidnightBundles.Market market) external => HAVOC_ALL; + 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); @@ -17,14 +21,9 @@ methods { } /// HELPERS /// -// Persistent ghosts so that the unresolved external calls to MIDNIGHT (e.g. touchMarket, withdrawCollateral) which are havoc'd by the Prover do not havoc the tracked balances. persistent ghost mapping(address => mapping(address => uint256)) tokenBalance; -persistent ghost uint256 boughtAssets; - -persistent ghost uint256 soldAssets; - function summaryPullToken(address token, address from, uint256 amount) { summarySafeTransferFrom(token, from, currentContract, amount); } @@ -41,6 +40,10 @@ function summarySafeTransferFrom(address token, address from, address to, uint25 tokenBalance[token][to] = assert_uint256(tokenBalance[token][to] + amount); } +persistent ghost uint256 boughtAssets; + +persistent ghost uint256 soldAssets; + function summaryTake(address msgSender, MidnightBundles.Offer offer, address taker, address receiverIfTakerIsSeller, address takerCallback) returns (uint256, uint256) { uint256 buyerAssets; uint256 sellerAssets; From 7202615dd4aaa302727577bcd57e94ac92c95fd6 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Fri, 12 Jun 2026 10:57:29 +0200 Subject: [PATCH 10/18] minimal summaries --- certora/specs/MidnightBundlesBalance.spec | 3 --- 1 file changed, 3 deletions(-) diff --git a/certora/specs/MidnightBundlesBalance.spec b/certora/specs/MidnightBundlesBalance.spec index 032b152..2c6aaa7 100644 --- a/certora/specs/MidnightBundlesBalance.spec +++ b/certora/specs/MidnightBundlesBalance.spec @@ -11,9 +11,6 @@ methods { function ConsumableUnitsLib.consumableUnits(address midnight, bytes32 id, MidnightBundles.Offer memory offer) internal returns (uint256) => NONDET; function _.toId(MidnightBundles.Market market) external => NONDET; - // Over-approximate external calls. - function _.touchMarket(MidnightBundles.Market market) external => HAVOC_ALL; - 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); From 729d88ee918c762bb96e11349fa77e39c76fd2fe Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Fri, 12 Jun 2026 11:01:22 +0200 Subject: [PATCH 11/18] remove args not needed --- certora/specs/MidnightBundlesBalance.spec | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/certora/specs/MidnightBundlesBalance.spec b/certora/specs/MidnightBundlesBalance.spec index 2c6aaa7..e465f07 100644 --- a/certora/specs/MidnightBundlesBalance.spec +++ b/certora/specs/MidnightBundlesBalance.spec @@ -6,10 +6,10 @@ methods { function Utils.hashMarket(MidnightBundles.Market market) external returns (bytes32) envfree; // Over-approximate view functions. - function TakeAmountsLib.sellerAssetsToUnits(address midnight, bytes32 id, MidnightBundles.Offer memory offer, uint256 targetSellerAssets) internal returns (uint256) => NONDET; - function TakeAmountsLib.buyerAssetsToUnits(address midnight, bytes32 id, MidnightBundles.Offer memory offer, uint256 buyerAssets) internal returns (uint256) => NONDET; - function ConsumableUnitsLib.consumableUnits(address midnight, bytes32 id, MidnightBundles.Offer memory offer) internal returns (uint256) => NONDET; - function _.toId(MidnightBundles.Market market) external => NONDET; + 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; 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); From ccbd829e6caff9004f6eba043df1449c8dff892e Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Fri, 12 Jun 2026 17:12:33 +0200 Subject: [PATCH 12/18] add other rules --- certora/specs/MidnightBundlesBalance.spec | 102 ++++++++++++++++++++++ 1 file changed, 102 insertions(+) diff --git a/certora/specs/MidnightBundlesBalance.spec b/certora/specs/MidnightBundlesBalance.spec index e465f07..d1eb4ec 100644 --- a/certora/specs/MidnightBundlesBalance.spec +++ b/certora/specs/MidnightBundlesBalance.spec @@ -11,10 +11,18 @@ methods { function ConsumableUnitsLib.consumableUnits(address, bytes32, MidnightBundles.Offer memory) internal returns (uint256) => NONDET; function _.toId(MidnightBundles.Market) external => NONDET; + // Are all of those necessary? + function TokenLib.safeApprove(address token, address spender, uint256 value) internal => NONDET; + function _.supplyCollateral(MidnightBundles.Market, uint256, uint256, address) external => NONDET; + function _.withdrawCollateral(MidnightBundles.Market, uint256, uint256, address, address) external => NONDET; + function _.touchMarket(MidnightBundles.Market) external => HAVOC_ALL; + + // 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 /// @@ -41,6 +49,8 @@ persistent ghost uint256 boughtAssets; persistent ghost uint256 soldAssets; +persistent ghost uint256 repaidAssets; + function summaryTake(address msgSender, MidnightBundles.Offer offer, address taker, address receiverIfTakerIsSeller, address takerCallback) returns (uint256, uint256) { uint256 buyerAssets; uint256 sellerAssets; @@ -49,6 +59,10 @@ function summaryTake(address msgSender, MidnightBundles.Offer offer, address tak return (buyerAssets, sellerAssets); } +function summaryRepay(uint256 units) { + repaidAssets = require_uint256(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) { @@ -72,3 +86,91 @@ rule buyWithUnitsTargetAndWithdrawCollateralDoesntLoseTokens(env e, uint256 targ 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; + + require e.msg.sender != currentContract; + require referralFeeRecipient != e.msg.sender; + require referralFeeRecipient != currentContract; + + 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; + + // The proceeds go to the receiver and the referral fee to its recipient: they only count as received/fee if they + // are third parties, distinct from the collateral payer (msg.sender) and from the bundler. + require e.msg.sender != currentContract; + require receiver != e.msg.sender; + require receiver != currentContract; + require referralFeeRecipient != e.msg.sender; + require referralFeeRecipient != currentContract; + require receiver != referralFeeRecipient; + + 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; + + require e.msg.sender != currentContract; + require receiver != e.msg.sender; + require receiver != currentContract; + require referralFeeRecipient != e.msg.sender; + require referralFeeRecipient != currentContract; + require receiver != referralFeeRecipient; + + 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; + + require e.msg.sender != currentContract; + require referralFeeRecipient != e.msg.sender; + require referralFeeRecipient != currentContract; + + 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; +} From 497ab8f6ebddb4882d3fe70671e6302ac1e8073c Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Fri, 12 Jun 2026 17:53:15 +0200 Subject: [PATCH 13/18] simplifications --- certora/specs/MidnightBundlesBalance.spec | 47 ++++++----------------- 1 file changed, 12 insertions(+), 35 deletions(-) diff --git a/certora/specs/MidnightBundlesBalance.spec b/certora/specs/MidnightBundlesBalance.spec index d1eb4ec..cb5fcd0 100644 --- a/certora/specs/MidnightBundlesBalance.spec +++ b/certora/specs/MidnightBundlesBalance.spec @@ -11,11 +11,8 @@ methods { function ConsumableUnitsLib.consumableUnits(address, bytes32, MidnightBundles.Offer memory) internal returns (uint256) => NONDET; function _.toId(MidnightBundles.Market) external => NONDET; - // Are all of those necessary? + // This seems needed for call resolution. function TokenLib.safeApprove(address token, address spender, uint256 value) internal => NONDET; - function _.supplyCollateral(MidnightBundles.Market, uint256, uint256, address) external => NONDET; - function _.withdrawCollateral(MidnightBundles.Market, uint256, uint256, address, address) external => NONDET; - function _.touchMarket(MidnightBundles.Market) external => HAVOC_ALL; // Token modeling. function SafeTransferLib.safeTransfer(address token, address receiver, uint256 amount) internal => summarySafeTransfer(token, receiver, amount); @@ -45,22 +42,22 @@ function summarySafeTransferFrom(address token, address from, address to, uint25 tokenBalance[token][to] = assert_uint256(tokenBalance[token][to] + amount); } -persistent ghost uint256 boughtAssets; +persistent ghost mathint boughtAssets; -persistent ghost uint256 soldAssets; +persistent ghost mathint soldAssets; -persistent ghost uint256 repaidAssets; +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 = require_uint256(boughtAssets + buyerAssets); - soldAssets = require_uint256(soldAssets + sellerAssets); + boughtAssets = boughtAssets + buyerAssets; + soldAssets = soldAssets + sellerAssets; return (buyerAssets, sellerAssets); } function summaryRepay(uint256 units) { - repaidAssets = require_uint256(repaidAssets + units); + repaidAssets = repaidAssets + units; } /// RULES /// @@ -68,11 +65,7 @@ function summaryRepay(uint256 units) { 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; - // The referral fee is paid to a third party, so it only leaves the taker if the recipient is distinct from the - // taker and from the bundler. - require e.msg.sender != currentContract; - require referralFeeRecipient != e.msg.sender; - require referralFeeRecipient != currentContract; + require referralFeeRecipient != e.msg.sender, "distinct fee recipient"; boughtAssets = 0; uint256 feeBalanceBefore = tokenBalance[loanToken][referralFeeRecipient]; @@ -90,9 +83,7 @@ rule buyWithUnitsTargetAndWithdrawCollateralDoesntLoseTokens(env e, uint256 targ 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; - require e.msg.sender != currentContract; - require referralFeeRecipient != e.msg.sender; - require referralFeeRecipient != currentContract; + require referralFeeRecipient != e.msg.sender, "distinct fee recipient to simplify accounting"; boughtAssets = 0; uint256 feeBalanceBefore = tokenBalance[loanToken][referralFeeRecipient]; @@ -110,14 +101,7 @@ rule buyWithAssetsTargetAndWithdrawCollateralDoesntLoseTokens(env e, uint256 tar 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; - // The proceeds go to the receiver and the referral fee to its recipient: they only count as received/fee if they - // are third parties, distinct from the collateral payer (msg.sender) and from the bundler. - require e.msg.sender != currentContract; - require receiver != e.msg.sender; - require receiver != currentContract; - require referralFeeRecipient != e.msg.sender; - require referralFeeRecipient != currentContract; - require receiver != referralFeeRecipient; + require receiver != referralFeeRecipient, "distinct recipients to simplify accounting"; soldAssets = 0; uint256 feeBalanceBefore = tokenBalance[loanToken][referralFeeRecipient]; @@ -135,12 +119,7 @@ rule supplyCollateralAndSellWithUnitsTargetDoesntLoseTokens(env e, uint256 targe 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; - require e.msg.sender != currentContract; - require receiver != e.msg.sender; - require receiver != currentContract; - require referralFeeRecipient != e.msg.sender; - require referralFeeRecipient != currentContract; - require receiver != referralFeeRecipient; + require receiver != referralFeeRecipient, "distinct recipients to simplify accounting"; soldAssets = 0; uint256 feeBalanceBefore = tokenBalance[loanToken][referralFeeRecipient]; @@ -158,9 +137,7 @@ rule supplyCollateralAndSellWithAssetsTargetDoesntLoseTokens(env e, uint256 targ 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; - require e.msg.sender != currentContract; - require referralFeeRecipient != e.msg.sender; - require referralFeeRecipient != currentContract; + require referralFeeRecipient != e.msg.sender, "distinct fee recipient to simplify accounting"; repaidAssets = 0; uint256 feeBalanceBefore = tokenBalance[loanToken][referralFeeRecipient]; From 5fb133b5ec9a5c79c281cde61db385db90793540 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Fri, 12 Jun 2026 18:09:08 +0200 Subject: [PATCH 14/18] address different trick --- certora/specs/MidnightBundlesBalance.spec | 27 ++++++++++++++++++----- 1 file changed, 22 insertions(+), 5 deletions(-) diff --git a/certora/specs/MidnightBundlesBalance.spec b/certora/specs/MidnightBundlesBalance.spec index cb5fcd0..70f0d03 100644 --- a/certora/specs/MidnightBundlesBalance.spec +++ b/certora/specs/MidnightBundlesBalance.spec @@ -65,7 +65,10 @@ function summaryRepay(uint256 units) { 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; - require referralFeeRecipient != e.msg.sender, "distinct fee recipient"; + // 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]; @@ -83,7 +86,10 @@ rule buyWithUnitsTargetAndWithdrawCollateralDoesntLoseTokens(env e, uint256 targ 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; - require referralFeeRecipient != e.msg.sender, "distinct fee recipient to simplify accounting"; + // Assume different addresses to have correct accounting, using hardcoded addresses as a trick. + require e.msg.sender == 11; + require referralFeeRecipient == 12; + require currentContract == 13; boughtAssets = 0; uint256 feeBalanceBefore = tokenBalance[loanToken][referralFeeRecipient]; @@ -101,7 +107,11 @@ rule buyWithAssetsTargetAndWithdrawCollateralDoesntLoseTokens(env e, uint256 tar 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; - require receiver != referralFeeRecipient, "distinct recipients to simplify accounting"; + // 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"; + require receiver == 14, "ack"; soldAssets = 0; uint256 feeBalanceBefore = tokenBalance[loanToken][referralFeeRecipient]; @@ -119,7 +129,11 @@ rule supplyCollateralAndSellWithUnitsTargetDoesntLoseTokens(env e, uint256 targe 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; - require receiver != referralFeeRecipient, "distinct recipients to simplify accounting"; + // 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"; + require receiver == 14, "ack"; soldAssets = 0; uint256 feeBalanceBefore = tokenBalance[loanToken][referralFeeRecipient]; @@ -137,7 +151,10 @@ rule supplyCollateralAndSellWithAssetsTargetDoesntLoseTokens(env e, uint256 targ 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; - require referralFeeRecipient != e.msg.sender, "distinct fee recipient to simplify accounting"; + // 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]; From ea8d8eb60a603f4650b3be1e7b633445a40e1c91 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Fri, 12 Jun 2026 18:17:09 +0200 Subject: [PATCH 15/18] quick fix --- certora/specs/MidnightBundlesBalance.spec | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/certora/specs/MidnightBundlesBalance.spec b/certora/specs/MidnightBundlesBalance.spec index 70f0d03..9ec0a96 100644 --- a/certora/specs/MidnightBundlesBalance.spec +++ b/certora/specs/MidnightBundlesBalance.spec @@ -87,9 +87,9 @@ rule buyWithAssetsTargetAndWithdrawCollateralDoesntLoseTokens(env e, uint256 tar 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; - require referralFeeRecipient == 12; - require currentContract == 13; + require e.msg.sender == 11, "ack"; + require referralFeeRecipient == 12, "ack"; + require currentContract == 13, "ack"; boughtAssets = 0; uint256 feeBalanceBefore = tokenBalance[loanToken][referralFeeRecipient]; From 2fcdf58c901d5798163a8cb41c877c00d2cca55e Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Mon, 15 Jun 2026 13:03:32 +0200 Subject: [PATCH 16/18] tweak --- .gitignore | 1 + certora/specs/MidnightBundlesBalance.spec | 10 ++++------ 2 files changed, 5 insertions(+), 6 deletions(-) diff --git a/.gitignore b/.gitignore index 3580437..62568bb 100644 --- a/.gitignore +++ b/.gitignore @@ -5,3 +5,4 @@ broadcast/ *.swp .DS_Store node_modules/ +.certora_internal/ diff --git a/certora/specs/MidnightBundlesBalance.spec b/certora/specs/MidnightBundlesBalance.spec index 9ec0a96..ff1b16d 100644 --- a/certora/specs/MidnightBundlesBalance.spec +++ b/certora/specs/MidnightBundlesBalance.spec @@ -11,8 +11,8 @@ methods { function ConsumableUnitsLib.consumableUnits(address, bytes32, MidnightBundles.Offer memory) internal returns (uint256) => NONDET; function _.toId(MidnightBundles.Market) external => NONDET; - // This seems needed for call resolution. - function TokenLib.safeApprove(address token, address spender, uint256 value) internal => NONDET; + // Over-approximate non-view function. + function TokenLib.forceApproveMax(address token, address spender, uint256 value) internal => HAVOC_ALL; // Token modeling. function SafeTransferLib.safeTransfer(address token, address receiver, uint256 amount) internal => summarySafeTransfer(token, receiver, amount); @@ -108,10 +108,9 @@ rule supplyCollateralAndSellWithUnitsTargetDoesntLoseTokens(env e, uint256 targe 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 receiver == 11, "ack"; require referralFeeRecipient == 12, "ack"; require currentContract == 13, "ack"; - require receiver == 14, "ack"; soldAssets = 0; uint256 feeBalanceBefore = tokenBalance[loanToken][referralFeeRecipient]; @@ -130,10 +129,9 @@ rule supplyCollateralAndSellWithAssetsTargetDoesntLoseTokens(env e, uint256 targ 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 receiver == 11, "ack"; require referralFeeRecipient == 12, "ack"; require currentContract == 13, "ack"; - require receiver == 14, "ack"; soldAssets = 0; uint256 feeBalanceBefore = tokenBalance[loanToken][referralFeeRecipient]; From 075d59f4694c046705a811dfafad8b439978264f Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Mon, 15 Jun 2026 19:04:48 +0200 Subject: [PATCH 17/18] config fix --- certora/confs/MidnightBundlesBalance.conf | 5 ++++- certora/specs/MidnightBundlesBalance.spec | 6 ++++-- 2 files changed, 8 insertions(+), 3 deletions(-) diff --git a/certora/confs/MidnightBundlesBalance.conf b/certora/confs/MidnightBundlesBalance.conf index 7bcc6c9..a7e4c09 100644 --- a/certora/confs/MidnightBundlesBalance.conf +++ b/certora/confs/MidnightBundlesBalance.conf @@ -4,6 +4,9 @@ "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", @@ -17,4 +20,4 @@ "-splitParallel true" ], "msg": "MidnightBundles balance neutrality" -} +} \ No newline at end of file diff --git a/certora/specs/MidnightBundlesBalance.spec b/certora/specs/MidnightBundlesBalance.spec index ff1b16d..ae469ce 100644 --- a/certora/specs/MidnightBundlesBalance.spec +++ b/certora/specs/MidnightBundlesBalance.spec @@ -11,8 +11,8 @@ methods { function ConsumableUnitsLib.consumableUnits(address, bytes32, MidnightBundles.Offer memory) internal returns (uint256) => NONDET; function _.toId(MidnightBundles.Market) external => NONDET; - // Over-approximate non-view function. - function TokenLib.forceApproveMax(address token, address spender, uint256 value) internal => HAVOC_ALL; + // 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); @@ -111,6 +111,7 @@ rule supplyCollateralAndSellWithUnitsTargetDoesntLoseTokens(env e, uint256 targe 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]; @@ -132,6 +133,7 @@ rule supplyCollateralAndSellWithAssetsTargetDoesntLoseTokens(env e, uint256 targ 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]; From 99379e59e3809ef29ddbe216428d5a231b9b8eb0 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Mon, 15 Jun 2026 19:23:03 +0200 Subject: [PATCH 18/18] lint conf file --- certora/confs/MidnightBundlesBalance.conf | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/certora/confs/MidnightBundlesBalance.conf b/certora/confs/MidnightBundlesBalance.conf index a7e4c09..732678b 100644 --- a/certora/confs/MidnightBundlesBalance.conf +++ b/certora/confs/MidnightBundlesBalance.conf @@ -20,4 +20,4 @@ "-splitParallel true" ], "msg": "MidnightBundles balance neutrality" -} \ No newline at end of file +}