IPOR PlasmaVault Redeem Splitting

redeem_preserves_pps_specLean spec
The spec definition in Lean: every valid modeled redeem must satisfy ppsCrossNondecreasing. amountShares feeRate s m :=

validRedeemInputValid redeem
The preconditions from Specs.lean: positive virtual offset, enough shares, fee within range, fee shares not above redeemed shares, and payout within assets. amountSharesamountShares
The number of shares requested for this redeem. feeRatefeeRate
The withdraw fee rate, bounded by WAD in validRedeemInput. ss
The vault state before redeem: total assets A and total shares T. mm
The virtual-share offset. For this IPOR model, m = 100.  ->

ppsCrossNondecreasingPPS non-decrease
The cross-multiplied virtualized conversion ratio: redeem does not reduce (A + 1)/(T + m). s (redeem amountShares feeRate s m) m

equivalently: (A' + 1)A prime
A prime: vault assets after paying the redeem payout. * (T + m) >= (A + 1) * (T' + m)T prime
T prime: vault shares after burning the requested shares.

We proved that a successful modeled public redeem cannot reduce the virtualized conversion PPS used by the vault.

View Lean

IPOR Fusion PlasmaVault is an ERC4626-style vault: users hold vault shares, and redeeming shares returns underlying assets. This case studies one narrow accounting path, the public fee-charging PlasmaVault redeem path. The model keeps the arithmetic that matters for this claim: virtual shares, withdraw-fee shares, asset conversion, and the post-redeem state update.

The completed proof anchors a narrow safety claim: if a modeled public redeem succeeds, the cross-multiplied virtualized conversion PPS cannot go down.

In plain terms, the proof says this arithmetic slice does not make the remaining holders' redeemable-value ratio worse. It does not prove that split redemptions are fee-fair, and it does not cover every PlasmaVault path.

Why It Matters

PlasmaVault burns all requested shares in _redeem. In the fee-charging public redeem path, the user receives assets for the post-fee share amount, while fee value remains in totalAssets, which raises the virtualized conversion PPS for the remaining supply.

That retained-fee design means the important local safety question is not whether every redemption strategy pays the same effective fee. The theorem focuses on the remaining vault: after the modeled redeem transition, the virtualized conversion ratio must not get worse.

PlasmaVault instant redeem accounting

Vault state before

A = assetsT = sharesm = 100

The virtual offset is part of the ERC4626-style conversion.

Redeem request

paid sharesamountShares - feeShares

fee sharesfeeShares

Only paid shares determine the asset payout, but all requested shares are burned.

User receives

\texttt{payout}=\texttt{convertToAssets}(\texttt{paidShares})

The payout is floored by the conversion formula.

Vault keeps

A' = A - payoutT' = T - amountShares

Fee value is retained because assets are paid on fewer shares than the number burned.

Proved local invariant

before PPS

\frac{A+1}{T+m}

does not exceed

after PPS

\frac{A'+1}{T'+m}

Equivalent Lean-friendly form: (A' + 1)(T + m) >= (A + 1)(T' + m)

How This Was Modeled and Proven

The model uses DECIMALS_OFFSET = 2, so the virtual-share multiplier is m = 100. The conversion follows PlasmaVault's _convertToAssets formula with A + 1 and T + m. The public redeem path calls the fee-charging internal redeem, and the fee source is modeled from WithdrawManager.

In Specs.lean, the main spec is named redeem_preserves_pps_spec. It says that every validRedeemInput must satisfy ppsCrossNondecreasing. Cross-multiplied over natural numbers, that means:

(A' + 1) * (T + m) >= (A + 1) * (T' + m)

where:
  A  = assets before redeem
  T  = shares before redeem
  payout = floor((amountShares - feeShares) * (A + 1) / (T + m))
  A' = A - payout
  T' = T - amountShares
  m  = 100

The proof uses the floor-division bound payout * (T + m) <= amountShares * (A + 1) and normalizes the natural-number subtractions in the post-redeem state. The reference proof has no sorry and no custom axioms or admitted assumptions.

Rejected target

Formal verification started with a stronger fee-fairness target: splitting one redeem should not pay more than the one-shot redeem, except for a tiny rounding allowance. The model found that target was false.

candidate:
  splitPayout <= combinedPayout + 1

edge case:
  redeem first tranche
  fee value stays in s.assets
  PPS rises for shares still held by the same user
  redeem second tranche at the updated PPS

result:
  splitPayout can be greater than combinedPayout + 1

That counterexample is why the final theorem is not a split-redemption fairness theorem. The completed proof is the narrower redeem_preserves_pps_spec claim: a successful modeled redeem cannot decrease the virtualized PPS.

Scope

This case targets the public fee-charging redeem path in PlasmaVault.sol at commit 3a83157ee75a7c1752d9151aff43eb92a50cb346. The modeled arithmetic includes:

amountShares requested for public redeem.
Withdraw-fee shares computed from feeRate.
PlasmaVault's virtual offset m = 100.
Asset conversion using A + 1 and T + m.
Post-redeem vault assets and share supply.

Out of scope: withdraw, request redemption, release queues, markets, access control, external asset movement, the instant redemption buffer lifecycle, and fee fairness across all split strategies.

Proof artifacts

Contract.lean contains the redeem accounting model.
Specs.lean contains validRedeemInput, ppsCrossNondecreasing, and redeem_preserves_pps_spec.
Proofs.lean proves the PPS non-decrease theorem pinned to commit c5a0207.

Claim	Function	Theorem	Status
main theorem: redeem preserves virtualized conversion PPS	redeem	redeem_preserves_pps_spec / redeem_preserves_pps	proved
supporting bound: fee payout is no larger than fee-free payout	redeem	fee_payout_bounded_by_fee_free_spec / fee_payout_bounded_by_fee_free	proved

Verify it yourself

git clone https://github.com/lfglabs-dev/verity-benchmark
cd verity-benchmark
git checkout c5a02071e605a1a187072731e7e2f77139f0d88c
lake build Benchmark.Cases.IPOR.PlasmaVaultRedeemSplit.Proofs

This builds the reference proof module for the IPOR case.

Assumptions

These hypotheses bound the claim to the successful public redeem arithmetic slice and the virtual offset used by the pinned source.

successful redeemamountShares <= s.shares and payout <= s.assets
modeled successful path
The theorem excludes failed calls and Nat subtraction underflow. It proves the post-state property for a redeem that can execute.
fee domainfeeRate <= 1e18 and feeShares <= amountShares
withdraw-fee domain
This matches the intended withdraw-fee range. The proof does not rely on an artificial bound on split advantage.
arithmetic slicemarkets, release queues, access control, and external asset movement are outside scope
model boundary
The model focuses on redeem accounting. It should not be read as a proof of all PlasmaVault behavior or the withdraw/request redemption paths.
virtual offsetm = 100
DECIMALS_OFFSET = 2
The proof uses the real PlasmaVault virtual-share offset from the pinned source, not the smaller offset from the first abstract model.

Learn More

Read the source contract in PlasmaVault.sol, the withdraw fee implementation in WithdrawManager.sol, and the formal artifacts in the benchmark repository.

The result is deliberately modest. It rules out a decrease in the modeled virtualized ERC4626 conversion ratio for the public redeem path. It does not show that redeem splitting is fee-fair, and it should not be presented as a vulnerability proof.