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.

Hypotheses

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

  • queue passes its collateralization check

    ParetoDollarQueue.depositFunds

    The collateralized-mode gate in depositFunds succeeds. The modeled successful path starts after this check.

  • deposit does not exceed idle collateral

    ParetoDollarQueue.depositFunds

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

  • open epoch's pending is within reserved withdrawals

    ParetoDollarQueue.depositFunds

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

  • post-deposit reserve check passes

    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.

  • idle plus requested value does not overflow

    Uint256 arithmetic

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

  • Credit 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 prove virtualPrice correctness.

  • deposits do not also request vault withdrawals

    model boundary

    Deposit-mode calls do not request Credit Vault withdrawals. The modeled deposit path excludes manager actions that request them through the shared external-call helper. Those actions can change requested Credit Vault value and belong to a different queue transition.

  • scaled idle collateral matches token balances

    model boundary

    The scaled idle collateral matches the actual token balances. ERC20 balances and successful yield-source calls are summarized by idleCollateralScaled and depositedScaled.

Learn More