Pareto Redemption Backing Guard

If the source reserve require and checked arithmetic succeed, the modeled post-state leaves closed redemption claims covered.

View Lean

Pareto USP groups redemption requests by epoch. When a user requests redemption, USP is burned and the queue records a claim. This proof checks the modeled post-condition of depositFunds: when the source reserve require and checked arithmetic succeed, the modeled post-state satisfies the closed-epoch reserve guard. The full Lean guard also records the current-pending and no-overflow side conditions needed to make that subtraction and sum well-defined.

Why It Matters

A redemption request burns USP before the user receives collateral. The queue must then preserve enough recognized value for already closed epochs while managers continue moving idle funds into yield sources. If that local guard were wrong, a manager action could make an older redemption epoch look processable while the queue no longer accounts for enough backing value.

The unit at risk is 18-decimal USP redemption value. The users affected are redeemers whose claims have already left the open current epoch. This proof does not show that every redemption is live or that Credit Vault prices are correct. It shows that the modeled successful depositFunds post-state satisfies the guard when the source reserve require and checked-arithmetic side conditions succeed.

How This Was Modeled and Proven

The Verity model focuses on the queue accounting slice around depositFunds. External ERC20 balances, yield-source calls, and Credit Vault pricing are represented by scaled ghost totals because the theorem targets the reserve check after those successful calls have returned.

The model is in Contract.lean. The closed-epoch reserve guard is in Specs.lean, and the reference proof is in Proofs.lean.

Scope

The proof covers the modeled successful path of depositFunds. The scalar depositedScaled summarizes the successful post-loop decrease in getUnlentBalanceScaled().

The proof does not cover global redemption solvency, every queue transition, Credit Vault valuation correctness, token transfer honesty, or claim liveness.

Proof artifacts
FunctionTheoremStatus
depositFundsdepositFunds_preserves_closed_epoch_reserve_guardproved under source reserve require
Verify it yourself
git clone https://github.com/lfglabs-dev/ethereum-verification-benchmark
cd ethereum-verification-benchmark
git checkout pareto-redemption-backing
lake build Benchmark.Cases.Pareto.RedemptionBacking.Proofs

If the build succeeds, the reference proof in ethereum-verification-benchmark checks under the pinned Lean and Verity dependencies.

Assumptions

These assumptions are part of the theorem scope. They are not hidden protocol guarantees.

  • hCollateralizedcollateralized-mode gate succeeds

    ParetoDollarQueue.depositFunds

    The modeled successful path starts after the queue passes its collateralization check.

  • hDepositLeIdledeposit does not exceed idle collateral

    ParetoDollarQueue.depositFunds

    The scaled deposit amount is no larger than the modeled idle collateral available before the manager deposit.

  • hCurrentLeReservedcurrent pending does not exceed reserved

    ParetoDollarQueue.depositFunds

    The open current epoch's pending amount is no larger than total reserved withdrawals, so closed claims can be computed as total reserved minus current pending.

  • hReserveGuardpost-deposit reserve guard holds

    ParetoDollarQueue.depositFunds

    The Solidity check at the end of depositFunds succeeds: closed-epoch reserved withdrawals are no larger than idle collateral plus requested Credit Vault withdrawal value.

  • hAddNoOverflowidle plus requested value does not overflow

    Uint256 arithmetic

    The modeled sum of post-deposit idle collateral and requested Credit Vault value stays within Uint256.

  • external valuationCredit Vault values are trusted inputs

    model boundary

    The proof assumes the scaled Credit Vault requested-withdrawal value is a valid accounting input. It does not provevirtualPrice correctness.

  • manager action scopedeposit-mode calls do not request Credit Vault withdrawals

    model boundary

    The modeled deposit path excludes manager actions that request Credit Vault withdrawals through the shared external-call helper. Those actions can mutate requested Credit Vault value and belong to a different queue transition.

  • token framescaled idle collateral matches token balances

    model boundary

    ERC20 balances and successful yield-source calls are summarized by idleCollateralScaled and depositedScaled.

Learn More