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

Assumptions

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.

hPartial_PARTIAL_FILL is set in desc.flags
MetaAggregationRouterV2 flag branch
The theorem is for the partial-fill branch. The non-partial branch has a different raw minimum-return check.
hRun_checkReturnAmount succeeds in the modeled execution
successful Solidity 0.8 helper path
Success includes both checked multiplications succeeding and the final require guard passing. If either multiplication overflows, Solidity 0.8 reverts and the theorem does not claim success.
price-floor readingspentAmount <= amount
economic interpretation, not enforced by the helper
The scaled inequality reads as an effective-price floor only when the fill spends no more source than the user quoted. The modeled helper does not check spentAmount against amount, 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.
helper scopespentAmount and returnAmount are inputs to the helper
benchmark scope
The proof does not establish how public swap paths compute those values or how token balances move outside the helper.

Learn More

More Research

1inch XYCSwap Curve Safety

Formally verified fee-adjusted constant-product curve safety for 1inch Aqua XYCSwap.

for

StarkGate Bridge Escrow Lower Bound

Formally verified escrow accounting for the StarkGate L1 token bridge deposit, withdrawal, and reclaim paths.

for

Pendle PY Supply Pairing

Formally verified PT and YT supply-pairing accounting for Pendle V2 mintPY and successful pre-expiry redeemPY paths.

for