Doppler Multicurve Fee Conservation

Doppler provides infrastructure for launching tokens and creating their initial markets. In Doppler's orchestrated launch flow, its Multicurve system sells a newly launched asset against a numeraire token along a configurable price curve.

Each swap can generate fees. The FullRangeFeeRehype manager routes those fees to beneficiaries or reinvests them as full-range liquidity. If a conversion or liquidity operation uses only part of the available fee credit, the remainder stays in carry for a later transaction.

Why It Matters

Ignoring conversion for a moment, suppose the manager collects 100 fee units in one token. It sends 40 to beneficiaries and reserves 60 for liquidity. If the liquidity operation uses 45 of those 60 units as liquidity input, the remaining 15 must stay in carry for later.

A bookkeeping error could lose those 15 units or leave them in carry after they were already spent. The first error makes fees disappear. The second lets the same fee be counted and potentially spent twice. This is the failure the invariant is designed to prevent.

How This Was Modeled and Proven

For each current token denomination, we represented the accounting in three proof-only totals: waiting in carry, paid to beneficiaries, or used for liquidity. We then recreated the relevant fee-manager operations in Lean, including collection, partial conversion, deferred processing, payment, liquidity provision, and market closure.

For each operation, Lean checks that the token amounts represented by the returned spend, receive, and provide results are neither lost nor counted twice. A conversion may change both the denomination and amount, so this is token-credit accounting, not a proof of exchange-rate fairness or economic-value conservation. Lean also checks that live manager credit covers this market's carry plus the reservations of other markets using the same token.

Eighteen preservation theorems cover these modeled transitions at pinned DAMM revision 6424187967f93df1185f435f3adbcac0ce8fc7ec. The reference proof contains no case-specific axioms, sorry, or admit.

git clone https://github.com/lfglabs-dev/ethereum-verification-benchmark
cd ethereum-verification-benchmark
git checkout 047e3f9ab22a1c73b264710a9516a3c09e05e268
lake build Benchmark.Cases.Doppler.MulticurveFeeConservation.Compile

Hypotheses

These rows separate theorem premises, assumptions, runtime preconditions, verified execution facts, and scope exclusions. Together they define the boundary between the proved Lean result and deployed-contract behavior.

• theorem premise: consistent starting statethe accounting invariant holds before the modeled operation

  preservation theorem premise

  This is the strongest condition. The proof shows that correct accounting stays correct; it does not prove market initialization or repair an already inconsistent state.

• assumption: external calls report what they usedthe model uses the spent, received, and liquidity-input amounts returned by DAMM

  DAMM return values

  The amounts may be economically good or bad. The proof only assumes the returned numbers match the credit actually moved by the external swap or liquidity engine, whose internals are not proved here.

• verified fact: failed calls follow Solidity semanticsa caught failure defers that leg; an uncaught failure reverts the transaction

  Solidity try/catch and EVM rollback

  A caught failure leaves its unused fee credit waiting in carry. An uncaught failure produces no new state because the whole transaction rolls back.

• assumption: other markets stay unchanged during this steponly the selected market changes during the modeled transition

  token-wide reservations

  Other markets sharing the same token are summarized as one unchanged amount. This lets the proof check that manager credit still covers the complete token-wide reservation after the selected market changes.

• runtime precondition: no arithmetic revertchecked additions, subtractions, and uint128 casts succeed

  Solidity 0.8 and SafeCastLib

  Each stored carry cell is uint128. A checked cast or addition that would make one cell exceed 2^128 minus 1 raw units reverts. That limit is about 3.4e20 whole tokens at 18 decimals. Aggregate reservations and processing budgets use uint256; overspending, overflow, and underflow also revert.

Learn More

• Doppler
• Benchmark pull request
• What is a formal proof?