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 It 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 Modeled and 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.

The upper bound relies on the exp assumption listed under Hypotheses.

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

Hypotheses

The proof relies on the following assumptions:

• exp behaves like a real exponential

  PRBMath SD59x18 trust boundaryMathLib_exp_nonpositive_le_D18

  The proof assumes exp(x) ≤ 1 for any x ≤ 0. The PRBMath exp implementation is a long polynomial approximation, and the proof does not re-verify every bit. We assume it satisfies this standard property of exponentials.

• the price band is well-formed

  openAuction input checkhBand

  The band must satisfy endPrice ≤ startPrice, so the 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 swap

  Used only at the end-time boundaryhStartNeEnd

  The proof assumes auction.startTime ≠ auction.endTime. This excludes the edge case where the launcher sets the same start and end time (an atomic swap). In that case the band collapses to a single price and the invariant holds trivially.

• the decay exponent fits in a signed integer

  Realistic auction rangeInteriorSafe.hKElapsedFitsInt

  The proof assumes k × elapsed < 2^255: 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.

• start price stays below about 10^59

  Realistic launcher rangeInteriorSafe.hMulNoOverflow

  The proof assumes startPrice stays below roughly 10⁵⁹. A stablecoin priced in ETH gives a startPrice around 10³⁰, and even a 1000:1 launcher band stays below 10³³. That 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.