KyberSwap Partial-Fill Price Floor

\texttt{successfulRun}

Successful helper run
The theorem's hRun hypothesis: _checkReturnAmount completes successfully instead of reverting. Specs.lean states only isPartialFill ⇒ checkedScaledPriceFloorHolds; this run condition lives in the theorem, not the spec.

\;\wedge\;

\texttt{isPartialFill}(\texttt{desc}) = \texttt{true}

Partial-fill branch
The helper reads the _PARTIAL_FILL bit from desc.flags.

\;\Rightarrow\;

\texttt{checkedScaledPriceFloorHolds}

checkedScaledPriceFloorHolds
The Specs.lean helper that requires both products to fit in uint256 and the left product to be at least the right product.

(

\texttt{spentAmount}

spentAmount
The source amount the public path passes into _checkReturnAmount.

,

\texttt{returnAmount}

returnAmount
The destination amount the public path passes into _checkReturnAmount.

,

\texttt{desc}

desc
The modeled SwapDescriptionV2 fields: amount, minReturnAmount, and flags.

)

A successful partial-fill return check always enforces KyberSwap's scaled minimum-return floor on the values it receives.

View Lean

KyberSwap is a multi-chain decentralized exchange aggregator. This case targets the verified Ethereum deployment of MetaAggregationRouterV2 and proves one focused helper-level guard: successful partial-fill calls to _checkReturnAmount satisfy the checked scaled minimum-return predicate stated in Specs.lean.

Why It Matters

Partial fills let an aggregator execute less source volume than the user quoted. That flexibility is useful only if the return is scaled against the amount actually spent. Otherwise, a route could pass a raw minimum-return check while giving the user a worse effective price on the filled amount.

The router helper checks the two products that encode this floor: destination tokens returned times quoted input, compared with minimum destination tokens times spent input. The unit of value at risk is the user's swap input and expected output. The party affected is the trader whose transaction allowed a partial fill.

What failure would look like

If this helper accepted a partial-fill execution without the scaled floor, the router could report success even though the executed fill had too little return for its spent amount. This proof does not show that upstream route selection is optimal. It shows the modeled helper rejects successful partial-fill helper executions unless the scaled inequality holds.

How This Was Modeled and Proven

We modeled the private router helper in Contract.lean. The model keeps the branch structure of the Solidity helper: when the partial-fill flag is set, it computes both products with Solidity 0.8 checked multiplication through mulPanic, then requires the left product to be at least the right product.

The spec in Specs.lean uses the same helper names shown in the invariant: isPartialFill and checkedScaledPriceFloorHolds. The proof in Proofs.lean unfolds the helper, follows the successful checked-multiplication path, and reads the final require guard.

Scope

This is a helper-level benchmark. It covers _checkReturnAmount only.

Out of scope: public swap entrypoints, executor calls, route quality, token transfers, destination fees, refunds, permits, calldata decoding, events, and true user balance deltas. Those layers determine which values reach the helper. This proof is about the guard applied once those values are passed in.

Proof artifacts

Contract.lean models the helper and checked multiplication.
Specs.lean states the helper-level predicate.
Proofs.lean proves the successful partial-fill helper theorem.
Case directory contains the complete benchmark slice.

Function	Theorem	Status
_checkReturnAmount	checkReturnAmount_partial_fill_price_floor	proven

Verify it yourself

git clone https://github.com/lfglabs-dev/ethereum-verification-benchmark
cd ethereum-verification-benchmark
lake build Benchmark.Cases.KyberSwap.PartialFillPriceFloor.Compile

If the build succeeds, Lean has checked the model, spec, and proof. Source repository

Hypotheses

The theorem uses these explicit boundaries. It introduces no case-specific Lean axioms. The first two rows are proof hypotheses. The last two are scope and interpretation boundaries the proof does not assume.

partial-fill flag is set
MetaAggregationRouterV2 flag branch
The _PARTIAL_FILL flag is set in desc.flags, so the helper takes the partial-fill branch. The theorem covers only that branch. The non-partial branch has a different raw minimum-return check.
the return check succeeds
successful Solidity 0.8 helper path
_checkReturnAmount succeeds in the modeled execution. Success means both checked multiplications succeed and the final require guard passes. If either multiplication overflows, Solidity 0.8 reverts and the theorem does not claim success.
price floor holds only if the fill spends at most the quote
economic interpretation, not enforced by the helper
The scaled inequality reads as an effective-price floor only when spentAmount <= amount, that is, when the fill spends no more source than the user quoted. The modeled helper does not check this, and the theorem does not assume it. If a caller passed spentAmount > amount, the cross-multiplied check would be weaker than the raw minimum-return check. The proof covers the inequality as written.
spent and returned amounts are taken as given
benchmark scope
spentAmount and returnAmount are inputs to the helper. The proof does not establish how public swap paths compute those values or how token balances move outside the helper.

Learn More

More Research

Dromos MetaDEX Allocation Conservation

In the root-ledger model, chain allocations sum to committed voting power.

for

KPK Shares Settlement Accounting

A successful kpkShares settlement batch processes each eligible request at most once and accounts exactly for its fees, shares and asset transfers.

for

Railnet Queue Nominal Conservation

No matter how many partial redemptions happen, or in what order, the queue never records paying out more than it recorded receiving.

for