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

Hypotheses

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

• route steps arrive already decoded

  Benchmark/Cases/LiFi/SwapAtomicity/Contract.lean

  Each route step is already decoded into booleans. 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 results are given as inputs

  Benchmark/Cases/LiFi/SwapAtomicity/Contract.lean

  Token, refund, transfer, and DEX calls enter the model as success or failure flags. The proof verifies LI.FI's response to those flags. It does not prove third-party DEX semantics, token contract internals, or price quality beyond the modeled minimum output gate.

• EVM rollback undoes reverted routes

  Benchmark/Cases/LiFi/SwapAtomicity/Specs.lean

  Option.none means no committed route result: 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.

• only the original GenericSwapFacet path

  cases/lifi/swap_atomicity/case.yaml

  The case covers the original GenericSwapFacet and the common SwapperV2 path. It excludes GenericSwapFacetV3, periphery Executor swap loops, the native-reserve overload, exact event fields, and exact leftover refund amounts.