T3tris HWM Performance Fee

Invariant

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

Assumptions

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

• fee-state guardsProven for modeled init/config/accrual/claim paths

  Benchmark/Cases/T3tris/HwmPerformanceFee/Specs.lean

  The benchmark now proves these local guards for the modeled fee-state paths: validated initialization starts HWM at one WAD, validated performance-fee updates keep the fee at or below 100%, period-fee accrual preserves unclaimed fee shares within total supply, and fee-claim share burns preserve the same bound. Arbitrary corrupted storage and reverting arithmetic paths are still outside this theorem.

• NAV inputsGross assets are symbolic settlement inputs

  Benchmark/Cases/T3tris/HwmPerformanceFee/Contract.lean

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

• management feeManagement fee result is explicit input

  Benchmark/Cases/T3tris/HwmPerformanceFee/Contract.lean

  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.

• continuous LP lifecycleZero-supply HWM reanchor excluded

  Benchmark/Cases/T3tris/HwmPerformanceFee/Specs.lean

  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.