Usual DaoCollateral Conservation

\Delta\texttt{ghostUsd0Supply}

Ghost USD0 supply ledger
The ghosted net result of DaoCollateral mint, burn, and fee mint calls.

\;=\;

\texttt{computedQuote}

swap_conservation_spec
On swap, the model computes the quote from explicit price and supported token unit.

\quad\text{or}\quad

-\texttt{amount}+

\texttt{feeMintedUsd0}(s)

redeem_conservation_spec
On redeem, supply decreases by the redeemed amount, except the explicit non-CBR fee remint.

\;\land\;

\Delta\texttt{ghostTreasuryCollateral}

Ghost collateral ledger
The modeled ledger is credited and debited; ERC20 transfer correctness is not claimed.

Every direct swap or redeem updates the ghost USD0 and collateral ledgers by the exact amounts DaoCollateral accounts for.

View Lean

Usual issues USD0, an RWA-backed stablecoin. The DaoCollateral contract is the direct market where eligible collateral enters and USD0 is minted, or USD0 is burned and collateral leaves.

Why It Matters

A direct mint and redeem contract has one accounting promise that matters most: minted or burned USD0 must match the collateral movement that DaoCollateral records. If those quantities diverge, a user could create unbacked USD0 or redeem more collateral than the contract accounting permits.

The theorem focuses on that conservation boundary. It does not prove the USD0 token contract, the oracle, or SwapperEngine. It proves the DaoCollateral equations after those dependencies provide the inputs that the direct path consumes.

How This Was Modeled and Proven

We modeled the verified implementation behind the public proxy in Verity Benchmark, keeping the direct swap and redeem paths. The model mirrors the fee calculation, computes the swap quote from explicit oracle price and supported token-unit inputs, models token-decimal normalization for collateral decimals 0 through 18, and keeps the CBR branch and floor-rounded collateral return calculation.

Scope

The proof covers direct swap accounting, direct redeem accounting, redeem fee calculation, CBR-adjusted returned collateral, supported token-unit gates, and floor-rounded oracle conversion. Out of scope: USD0 token internals, registry and token mapping correctness, access control, pause gates, permits, intents, SwapperEngine routing, event emission, and oracle correctness.

Proof artifacts

The source-shaped model is in Contract.lean, and the readable conservation specification is in Specs.lean. The reference proof is in Proofs.lean.

Function	Theorem	Status
swap	swap_conservation	Proven
swap	swap_value_conservation	Proven
redeem	redeem_fee_formula	Proven
redeem	redeem_return_formula	Proven
redeem	redeem_conservation	Proven

Verify it yourself

git clone https://github.com/lfglabs-dev/verity-benchmark
cd verity-benchmark
lake build Benchmark.Cases.Usual.DaoCollateral.Proofs

If the build succeeds, Lean has checked the direct swap and redeem conservation proofs for the modeled DaoCollateral paths from the public benchmark main branch.

Hypotheses

The assumptions below state the proof boundary: external values supplied to the local accounting model, explicitly ghosted token effects, and the successful execution conditions needed for the theorem.

oracle prices are taken as given
Benchmark/Cases/Usual/DaoCollateral/Contract.lean
The oracle price is an external input. The model parameterizes oracle price and token unit, then computes the swap quote internally. It proves DaoCollateral accounting given those values, not oracle honesty.
token calls are tracked as ghost ledgers
Benchmark/Cases/Usual/DaoCollateral/Contract.lean
ERC20 and USD0 calls are ghosted: mint, burn, and transfer calls are represented by ghostUsd0Supply and ghostTreasuryCollateral ledgers. Token contract correctness is outside this case.
only successful calls are proven
Benchmark/Cases/Usual/DaoCollateral/Proofs.lean
Revert conditions are theorem preconditions, so the proof covers successful executions only. The hypotheses are: nonzero swap quote, uint128 swap amount bound, configured fee and CBR bounds, checked arithmetic, and sufficient ghost collateral.

Learn More

Kuru V2 Shared Withdrawal Budget

A successful batch of ordinary withdrawals in the model reduces the shared budget by exactly its recorded payout value, across all accounts and tokens.

with

Dromos MetaDEX Allocation Conservation

In the root-ledger model, chain allocations sum to committed voting power.

with

KPK Shares Settlement Accounting

A successful kpkShares settlement batch processes each eligible request at most once and accounts exactly for its fees, shares and asset transfers.

with