1inch XYCSwap Curve Safety

\texttt{output}

output
Amount of the output token the swap sends to the user. Computed by _quoteExactIn from the fee-adjusted constant-product formula.

\cdot

\texttt{denominator}

denominator
balanceIn + feeAdjustedInput. The post-deposit input reserve used as the divisor in the output formula.

\;\le\;

\texttt{feeAdjustedInput}

feeAdjustedInput
amountIn * (10000 - feeBps) / 10000. The input after the protocol fee in basis points is deducted.

\cdot

\texttt{balanceOut}

balanceOut
Output-token reserve held in the pool before the swap.

The output sent to the user times the post-deposit reserve never exceeds the fee-adjusted input times the output reserve.

View Lean

1inch Aqua is a shared liquidity layer for cross-chain swaps. XYCSwap is its constant-product AMM pool contract. This case proves that the output computed by the pool quoting function _quoteExactIn respects the constant-product curve bound stated in Specs.lean.

Why It Matters

A constant-product AMM must never let a quoted output exceed what the curve allows. If the quoting function returned too many output tokens for a given input, every swap would extract more value from the pool than the reserves can sustain. LPs would bleed value on every trade.

The guarantee is the fee-adjusted analog of Uniswap V2's K invariant. The quoting function computes output by dividing the fee-adjusted input times the output reserve by the input reserve plus the fee-adjusted input. Integer division rounds down. The theorem proves that this rounding-down property guarantees the output times the denominator never exceeds the fee-adjusted input times the output reserve.

What failure would look like

If the quoting function rounded up instead of down, or if a bug inverted the numerator and denominator, the pool could quote more output tokens than the constant-product curve permits. A trader could drain the output reserve over many swaps. This proof shows the modeled output formula preserves the curve bound. It does not prove the swap execution, token transfers, or callback logic.

How This Was Modeled and Proven

We modeled the quoting arithmetic in Contract.lean. The model keeps the fee-adjusted constant-product formula from Solidity: subtract the fee in basis points from the input, multiply by the output reserve, and divide by the input reserve plus the fee-adjusted input. The spec in Specs.lean states the curve bound. The proof in Proofs.lean reduces the Uint256 modular arithmetic to natural numbers and applies the integer division rounding-down property.

Scope

This is a pure-arithmetic benchmark. It covers the quoting function _quoteExactIn only.

Out of scope: AQUA liquidity layer calls, xycSwapCallback execution, _safeCheckAquaPush checks, token transfers, _quoteExactOut, the zeroForOne direction selector, and the Strategy struct fields beyond feeBps. Those layers determine how inputs reach the quoting function and how the output is used. This proof is about the arithmetic bound the formula produces.

Proof artifacts

Contract.lean models the fee-adjusted constant-product quoting arithmetic.
Specs.lean states the curve safety invariant.
Proofs.lean proves the theorem with zero axioms.
Case directory contains the complete benchmark slice.

Function	Theorem	Status
_quoteExactIn	quoteExactIn_curve_safety	proven

Verify it yourself

git clone https://github.com/lfglabs-dev/ethereum-verification-benchmark
cd ethereum-verification-benchmark
lake build Benchmark.Cases.OneInch.XYCSwapCurveSafety.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 four rows are proof hypotheses guarding against modular overflow. The last row is a scope boundary the proof does not assume.

fee is at most 100%
XYCSwap Strategy.feeBps range
The fee in basis points must satisfy feeBps <= 10000, which is 100%. Values above that would wrap to a negative subtraction.
fee-adjusted input fits in 256 bits
EVM Uint256 multiplication bound
The fee-adjusted input multiplication must not overflow: amountIn * (10000 - feeBps) < 2^256. Solidity 0.8.x checked arithmetic would revert on overflow, so this restricts the theorem to the non-reverting execution path.
swap denominator fits in 256 bits
EVM Uint256 addition bound
The denominator (input reserve plus fee-adjusted input) must not overflow: balanceIn + feeAdjustedInput < 2^256.
swap numerator fits in 256 bits
EVM Uint256 multiplication bound
The numerator product must not overflow: feeAdjustedInput * balanceOut < 2^256. This ensures the output is the exact quotient, not a wrapped value.
only the quote math is modeled
benchmark scope
The model covers _quoteExactIn only. The proof does not establish that the swap execution path uses this quoted output correctly, nor that token transfers or callbacks preserve pool solvency.

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