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

Assumptions

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.

hFeeRangefeeBps <= 10000
XYCSwap Strategy.feeBps range
The fee in basis points must not exceed 10000 (100%). Values above that would wrap to a negative subtraction.
hFeeMulNoOvfamountIn * (10000 - feeBps) < 2^256
EVM Uint256 multiplication bound
The fee-adjusted input multiplication must not overflow the 256-bit range. Solidity 0.8.x checked arithmetic would revert on overflow, so this hypothesis restricts the theorem to the non-reverting execution path.
hDenomNoOvfbalanceIn + feeAdjustedInput < 2^256
EVM Uint256 addition bound
The denominator (input reserve plus fee-adjusted input) must not overflow the 256-bit range.
hProductNoOvffeeAdjustedInput * balanceOut < 2^256
EVM Uint256 multiplication bound
The numerator product must not overflow the 256-bit range. This ensures the output is the exact quotient, not a wrapped value.
arithmetic scopemodeling covers _quoteExactIn only
benchmark scope
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

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

KyberSwap Partial-Fill Price Floor

Formally verified helper-level partial-fill price-floor guard for MetaAggregationRouterV2.

for