LI.FI Swap Route Atomicity

LI.FI routes users across same-chain swaps and cross-chain intents. This case targets the original GenericSwapFacet.swapTokensGeneric path and its shared SwapperV2 swap loop. The guarantee is about source-chain commit behavior for the provided _swapData, not about third-party DEX pricing or bridge completion.

Why It Matters

A route executor touches user funds, approvals, external DEX calls, leftover refunds, and the final receiver transfer in one transaction. The dangerous failure mode is partial success: a route looks complete to the user even though a modeled step or public-route guard failed.

The value at risk is the asset being routed through LI.FI's source-chain swap path. If the public final transfer could commit after a failed step, users and integrators could observe a completed route even though the route did not execute as supplied.

The proof checks the all-or-nothing control-flow layer. A failed receiver check, reentrancy guard, required deposit, allow-list check, approval, low-level call, leftover refund, minimum-output check, or final transfer prevents a committed final receiver transfer in the model.

How This Was Modeled and Proven

The model follows the public wrapper gates and helper ordering in the Solidity source. swapTokensGeneric includes the receiver, non-reentrant, and refund-excess-native gates around the helper call. It calls _depositAndSwap, then transfers the final receiving asset to the receiver. The shared executor deposits required assets, runs _executeSwaps, performs leftover refunds, checks minimum output, and returns the output amount.

Each SwapData item is represented by a decoded SwapStep. Route gates that live outside one step are represented by RouteGuards. The source-shaped model is in Contract.lean, the readable specs are in Specs.lean, and the no-sorry reference proofs are in Proofs.lean.

git clone https://github.com/lfglabs-dev/ethereum-verification-benchmark
cd ethereum-verification-benchmark
git checkout cc6f9f4a52fb9578071522c3d83658e87c18d2cc
lake build Benchmark.Cases.LiFi.SwapAtomicity.Compile

Assumptions

These assumptions name the proof boundary. They are scope limits, not hidden Lean axioms.

• decoded SwapDataEach route step is already decoded into booleans

  Benchmark/Cases/LiFi/SwapAtomicity/Contract.lean

  The model abstracts calldata bytes, token addresses, native versus ERC20 status, and allow-list lookups into explicit fields on SwapStep. Short calldata is represented by calldataWellFormed = false.

• external-call flagsToken, refund, transfer, and DEX calls are success inputs

  Benchmark/Cases/LiFi/SwapAtomicity/Contract.lean

  The proof verifies LI.FI's response to success or failure flags. It does not prove third-party DEX semantics, token contract internals, or price quality beyond the modeled minimum output gate.

• EVM rollbackOption.none means no committed route result

  Benchmark/Cases/LiFi/SwapAtomicity/Specs.lean

  Reverting routes produce no RouteCommit and no committed final receiver transfer. Rollback of earlier external effects is the standard EVM transaction semantics assumption, not a separate theorem about every third-party contract.

• scoped entrypointOriginal GenericSwapFacet and common SwapperV2 path

  cases/lifi/swap_atomicity/case.yaml

  The case excludes GenericSwapFacetV3, periphery Executor swap loops, the native-reserve overload, exact event fields, and exact leftover refund amounts.