Reserve DTF Auction Price Band Invariant

Reserve DTF Protocol lets anyone deploy a Folio: an ERC-20 share that represents a basket of underlying tokens. When the composition needs to change, governance opens a Dutch auction. An AUCTION_LAUNCHER publishes a per-pair price band, and bidders swap one basket token for another within that band as the per-pair price p decays from startPrice (worst for the bidder) to endPrice (best for the bidder) over the auction window. The decay is exponential, computed via PRBMath fixed-point ln and exp.

We worked with Reserve to formally verify that _price, the function every bid runs through, always returns a value inside the launcher-published band. The proof covers all three branches of the function: the start-time boundary, the end-time boundary, and the interior exponential decay.

View source contract

Why this matters

If _price ever returns a value outside [endPrice, startPrice], a bidder can buy basket tokens at a price the launcher never authorized. Above startPrice, the protocol pays out more sell-token per unit of buy-token than the auction band allows; below endPrice, the opposite. Either way, value leaks out of the basket on every bid.

Every bid goes through _price, so a bug here would leak basket value at a per-bid rate that scales with auction volume.

How this was proven

The interior branch of _price uses non-linear fixed-point arithmetic: a logarithm to compute the decay rate, an exponential to compute the current price, and ceiling division to apply it. Bounded model checkers and similar tools cannot reason about ln and exp, because they are computed by long polynomial approximations whose every bit cannot be checked by symbolic execution.

We modeled the contract in Verity, our Lean 4 framework for reasoning about Solidity. Instead of re-checking every bit of ln and exp, we rely on one mathematical fact about exp: it never returns a value greater than 1 when its input is at most 0. That single property is enough to prove the band invariant.

git clone https://github.com/lfglabs-dev/verity-benchmark
cd verity-benchmark
lake build Benchmark.Cases.Reserve.AuctionPriceBand

Assumptions / hypotheses

The proof relies on the following assumptions:

• exp behaves like a real exponentialexp(x) ≤ 1 for any x ≤ 0MathLib_exp_nonpositive_le_D18

  PRBMath SD59x18 trust boundary

  The PRBMath exp implementation is a long polynomial approximation; the proof does not re-verify every bit. We assume it satisfies the standard mathematical property of exponentials.

• The launcher band is well-formedendPrice ≤ startPricehBand

  openAuction input check

  The auction launcher cannot publish a band where the best price for the bidder is higher than the worst. openAuction rejects any such input.

• The auction is not an atomic swapauction.startTime ≠ auction.endTimehStartNeEnd

  Used only at the end-time boundary

  Excludes the edge case where the launcher sets the same start and end time (an atomic swap). In that edge case the band collapses to a single price and the invariant holds trivially.

• The decay exponent fits in a signed integerk × elapsed < 2^255InteriorSafe.hKElapsedFitsInt

  Realistic auction range

  The decay-rate term times elapsed seconds stays within the positive int256 range. With Reserve's one-week maximum auction length and realistic launcher prices, this is met with many orders of magnitude of headroom.

• startPrice does not blow past 200 bitsstartPrice < ~10^59InteriorSafe.hMulNoOverflow

  Realistic launcher range

  A stablecoin priced in ETH gives a startPrice around 10³⁰; even a 1000:1 launcher band stays below 10³³. The bound here leaves 26 orders of magnitude of headroom against any realistic price.

View in LeanReserve dtfs

Learn more

What is a formal proof? A short explanation for non-specialists.