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.

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.

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.

Assumptions

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 inputsPrice is external; swap quote is computed
Benchmark/Cases/Usual/DaoCollateral/Contract.lean
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 effectsERC20 and USD0 calls are ghosted
Benchmark/Cases/Usual/DaoCollateral/Contract.lean
Mint, burn, and transfer calls are represented by ghostUsd0Supply and ghostTreasuryCollateral ledgers. Token contract correctness is outside this case.
successful pathRevert conditions are preconditions
Benchmark/Cases/Usual/DaoCollateral/Proofs.lean
The proof focuses on successful executions: nonzero swap quote, uint128 swap amount bound, configured fee and CBR bounds, checked arithmetic, and sufficient ghost collateral are theorem hypotheses.

Learn More

Rootstock Flyover Quote Lifecycle

Formally verified peg-out quote conservation for Rootstock Flyover refunds.

for

1delta Caller-Address Integrity

Formally verified caller-address integrity for scoped OneDeltaComposerEthereum transfer and callback fund-pull paths.

for

Piku Redemption Fund Conservation

Formally verified fund-conservation accounting for Piku queued redemptions.

for