Piku Redemption Fund Conservation

Every unit of modeled backing is either distributed, queued, retained, or assigned to treasury fees.

View Lean

Piku uses an Inverter oracle-priced funding manager for USP redemption. A user sells issuance tokens, the funding manager computes a collateral redemption amount, fees are split, and a manual payment queue later settles the order.

The property tracks one unit of value: redemption backing. After each modeled accounting transition, backing must be accounted for as user distributions, queued redemptions, retained backing, or treasury fees.

Why It Matters

A redemption system can look solvent while silently losing value between buckets. If an order creation or queue settlement step changed one bucket without the matching opposite update, users could be underpaid, fees could be overcounted, or retained backing could be overstated.

The invariant turns that accounting question into a checkable statement. The sum of all backing already distributed, still queued, still retained, and assigned to fees must equal the initial backing committed to the redemption pool.

What this invariant covers

The Solidity contract stores _openRedemptionAmount. The benchmark adds ghost accounting slots for initial backing, distributed backing, remaining backing, protocol fees, and project fees. Those slots make Piku's fund-conservation requirement explicit in the model.

Oracle pricing, ERC20 transfer return behavior, access control, payment-order array shape, blacklist fallback, and failed payment accounting are outside this case. The proof covers the successful redemption order creation and successful queue settlement accounting transitions.

How This Was Modeled and Proven

The benchmark pins the docs-matching Inverter implementation at commit 8b7bc438344d646bab05b751c8eb4a7f0c8ca588. The modeled Solidity source is FM_PC_Oracle_Redeeming_v1.sol.

The Verity model keeps the Solidity names for the functions and storage it models, including _sellOrder, amountPaid, and _openRedemptionAmount. Each non-trivial block in Contract.lean is annotated with the Solidity lines it models.

The proof first establishes exact slot-write facts for order creation and settlement. It then rewrites the readable spec in Specs.lean using those facts to discharge the fee split and bucket moves. The reference solution is in Proofs.lean.

Scope: the source functions in scope are _sellOrder and amountPaid. The payment processor functions processPayments and executePaymentQueue provide context for successful settlement, but the model focuses on the accounting updates after a valid order exists.

Conditional on the modeled transition preconditions below, all four public theorem targets compile. The fund-conservation proofs discharge the fee-split and bucket arithmetic in Lean. The proof in Proofs.lean uses no sorry and no axiom.

FunctionTheoremStatus
_sellOrder_sellOrder_records_redemption_bucketsproven
_sellOrder_sellOrder_preserves_fund_conservationproven
amountPaidamountPaid_records_distributionproven
amountPaidamountPaid_preserves_fund_conservationproven
Verify it yourself
git clone https://github.com/lfglabs-dev/verity-benchmark
cd verity-benchmark
git checkout piku-fund-conservation
lake build Benchmark.Cases.Piku.FundConservation.Compile

If the build succeeds, the theorem targets compile under the stated preconditions. Source repository

Assumptions

These theorem preconditions restrict the modeled transition.

  • hAmounttotal != 0

    _sellOrder theorem hypothesis

    The redemption amount must be non-zero. This mirrors the scoped Solidity guard on the sell path.

  • hFeesprotocolFeeBps + sellFee < 10000

    _sellOrder theorem hypothesis

    The combined protocol and project fee rate must stay below 100 percent. Without this, the fee split can stop representing a valid redemption amount.

  • hRemainingtotal <= remainingBacking

    _sellOrder theorem hypothesis

    The ghost solvency ledger must contain enough backing before an order is created. This is a benchmark precondition for the explicit fund-conservation ledger.

  • hOpenamount <= _openRedemptionAmount

    amountPaid theorem hypothesis

    Settlement cannot deduct more queued backing than the funding manager currently records as open redemption amount.

  • hFeeprotocolFeeAmount <= amount

    amountPaid theorem hypothesis

    The protocol fee paid during settlement must fit inside the settled order amount, so the user distribution is non-negative.

  • fund_conservation_specpre-state buckets sum to initialBacking

    Invariant induction hypothesis

    Preservation theorems are local transitions. They assume the invariant held before the transition and prove it still holds afterward.

Learn More

Piku documentation, including the public contract/module references used for scoping.

What is a formal proof? A short explanation for non-specialists.