T3tris HWM Performance Fee

T3tris is a vault system with period-based fee settlement. This case targets the high-water-mark performance fee inside the period-fee arithmetic: once a gain has been fee-accounted, later loss and recovery steps whose pre-performance PPS remains at or below that stored high-water mark must not be charged again.

Why It Matters

A performance fee is supposed to charge only new gains. The tricky path is not a simple profitable settlement. It is a gain, a fee, a loss, and then a recovery. If the vault forgets that the earlier gain was already fee-accounted, LPs can pay twice for the same value returning to the portfolio.

The value at risk is LP share value. The proof focuses on the local accounting surface that decides whether performance fee assets and shares are charged, which high-water mark is persisted, and what base is used when a later settlement finally moves above the old fee-accounted peak.

How This Was Modeled and Proven

We modeled the arithmetic slice around FeatureFeesLib._computeLastPeriodFeesAndUpdateResult in Ethereum Verification Benchmark. The model keeps the source ordering that matters for the invariant: net supply excluding unclaimed fee shares, management-fee supply inflation, pre-performance PPS, HWM trigger, PnL, performance-fee shares, final post-fee PPS, and HWM persistence across settlements.

The reference proof is in Proofs.lean. The source-shaped arithmetic model is in Contract.lean, and the readable multi-step specifications are in Specs.lean.

git clone https://github.com/lfglabs-dev/ethereum-verification-benchmark
cd ethereum-verification-benchmark
git checkout 68f4a08b955258d792e2115dc11ceab7872f7184
lake build Benchmark.Cases.T3tris.HwmPerformanceFee.Proofs

Hypotheses

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

• fee-state guards, proven for modeled paths

  Benchmark/Cases/T3tris/HwmPerformanceFee/Specs.lean

  Proven for the modeled init, config, accrual, and claim paths: validated initialization starts HWM at one WAD, validated performance-fee updates keep the fee at or below 100%, period-fee accrual keeps unclaimed fee shares within total supply, and fee-claim share burns keep the same bound. Arbitrary corrupted storage and reverting arithmetic paths are still outside this theorem.

• gross asset values are given as inputs

  Benchmark/Cases/T3tris/HwmPerformanceFee/Contract.lean

  Gross assets are symbolic settlement inputs: each settlement receives its observed gross asset value as an input to the fee computation. Oracle, silo, and async-flow accounting are not re-proved here.

• management fee amount is given as input

  Benchmark/Cases/T3tris/HwmPerformanceFee/Contract.lean

  The management fee result is an explicit input. The model abstracts the timestamp formula for management fees, but preserves the source ordering where management fee shares inflate supply before the performance-fee PPS trigger.

• zero-supply HWM reanchor is excluded

  Benchmark/Cases/T3tris/HwmPerformanceFee/Specs.lean

  The zero-supply HWM reanchor is excluded. The no-double-charge theorem uses the normal non-reanchor settlement path. The zero-supply first-deposit lifecycle is a different branch and is outside this economic trajectory.