Royco Day Accounting Recovery FV

R = \min(G, D)

Junior recovery
R is the part of collateral gain G used to restore outstanding junior drawdown D.

Y = G - R

Remaining gain
Y is the collateral gain remaining after junior has been restored.

P_{junior} + P_{liquidity} \le Y

Premium bound
New junior and liquidity premiums cannot exceed the gain left after recovery.

1. Loss

Junior capital absorbs the drawdown first.

2. Recovery

Later gains restore that junior loss first.

3. Premiums

Only the remaining gain can fund premiums.

In the formal view, D is the unrecovered junior drawdown and G is the collateral gain.

View Lean

Royco Day divides a collateral position into a senior tranche, a junior first-loss tranche, and a liquidity tranche. The liquidity tranche supplies secondary liquidity for senior positions and receives a share of residual yield. This case models the v1.0.0 accountant slice in the pinned RoycoDayAccountant.sol source and checks the collateral recovery waterfall, premium arithmetic, share mint, six deposit and redemption checkpoints, and the inner liquidity reinvestment transition.

Why It Matters

Junior capital absorbs a collateral drawdown first. The amount junior lost is recorded as an unrecovered junior drawdown. When the collateral later gains, that gain first refills junior by that amount. Until then, junior holders are still below their earlier position, so the remaining collateral gain cannot fund new junior or liquidity premiums.

The units at risk are the raw and effective NAV assigned to the senior and junior tranches, plus the senior shares owned by the liquidity tranche and the protocol. A broken waterfall could overpay a premium, understate the junior claim, or mint senior shares to the wrong owner. The proofs show that the modeled successful transitions preserve the stated ordering, bounds, ownership split, and NAV conservation.

How This Was Modeled and Proven

We copied the part of Royco Day's accountant that applies one collateral gain or loss across Senior, Junior, and Liquidity. Think of it as copying the scorekeeper for this question, not the entire protocol.

Lean checked general rules: they must hold for every modeled call that meets the listed conditions. These include junior covering a collateral drawdown first, later collateral gains restoring junior before premiums are calculated, and premiums staying within the gain left after that restoration.

Scope

Included: the pure accountant's single-collateral loss and gain waterfall, derived market transition, premium calculation and share sizing, the six modeled deposit and redemption checkpoints, and the inner liquidity-reinvestment ledger update.

The v1.0.0 market transition keeps a market perpetual when senior effective NAV is zero or the post-deployment fixed-term grace period is still active, alongside the existing duration, junior-loss, expiry, dust, and liquidation-utilization conditions.

Scope exclusions: kernel cache choreography and coverage or liquidity enforcement, temporary multi-asset-flow state, external yield-manager, oracle, and Balancer behavior, token transfers, callbacks, access control, and events. The proof makes no claim about those omitted systems.

The post-operation theorems cover the accountant state transitions after the source has formed a valid checkpoint input. Kernel-level coverage and liquidity requirements can still reject a public call; those checks need a separate call-level theorem. The six modeled checkpoint shapes are senior, junior, and liquidity deposits and redemptions.

The reinvestment theorem starts after the settled senior-share rate and slippage floor have been computed. It covers the inner cap, zero-floor no-op, failed-call rollback, and successful liquidity-ledger update. It does not prove the operation-tail wrapper, a standalone cache-miss sync, the LPT mark commit, or external venue execution.

Proof artifacts

Contract.lean contains the source-structured protocol slice and simplification ledger.
Specs.lean defines the recovery, premium, conservation, ownership, and boundary properties.
Proofs.lean contains the machine-checked results.
At the pinned commit, the case adds no Lean axioms, sorry, or admit.
Compile.lean imports the complete case and evaluates the concrete witness.
Royco Day benchmark source contains the complete benchmark slice.

Function	Theorem	Status
sync arithmetic	_nat_uint256_refinement	proven
collateral gain	_recovery_before_yield	proven
premium calculation	_combined_premium_bound	proven
liquidity share	_lpt_premium_coverage_neutral	proven
premium mint	_lpt_premium_mint_split	proven
collateral drawdown	_st_loss_coverage_priority	proven
pre-operation sync	_sync_conserves_nav	proven
fee priority	_fees_require_full_recovery	proven
deposit / redemption	_post_op_no_yield	proven
deposit / redemption	_post_op_conserves_nav	proven
inner reinvestment	_inner_reinvestment_coverage_neutral	proven
partial recovery	_partial_recovery_no_fee_regression	proven

Verify it yourself

git clone https://github.com/lfglabs-dev/ethereum-verification-benchmark
cd ethereum-verification-benchmark
git checkout fd5c2bb83ef08abf8721fa172eaee2e68ec41062
lake build Benchmark.Cases.RoycoDay.LTLiquidityPremiumPriority.Proofs

A successful build means Lean checked the contract model, specifications, and all reference results at the pinned commit. Source repository

Hypotheses

External-input assumptions, arithmetic preconditions, runtime preconditions, scope exclusions, and verified facts are different boundaries. The exclusions are listed in Scope. The rows below state only assumptions and theorem preconditions.

Runtime preconditionsApplies to: sync, recovery, and premium theorems
sourceSyncDomain and successfulSyncDomain
Before a sync, collateral NAV equals senior plus junior effective NAV. The premium window is positive, accumulated junior and LPT yield shares fit within it, fee rates are at most 100%, and a loss cannot exceed the collateral NAV available to absorb it. Fixed-term expiry and the post-deployment grace period are supplied booleans used by the modeled market transition.
Arithmetic preconditionsApplies to: each theorem family
source domains
Inputs and successful results fit the source's storage and arithmetic widths, including uint64 configuration fields,uint128 accumulators, uint256 accounting, and the int256 conversions used by post-operation deltas. Checked arithmetic and full-precision calculations take successful paths.
Operation-specific preconditionsApplies only to the named mint, checkpoint, or reinvestment theorem
successfulMintDomain, successfulPostOpSourceDomain, and successfulReinvestmentDomain
The mint theorem requires fees not to exceed the gross LPT premium or retained tranche NAV. Checkpoint theorems require one of the six valid source-shaped operations and a balanced starting state. The reinvestment theorem requires a supplied venue result to satisfy the source floor before the success update can commit.
External-input assumptionsApplies only where external systems supply values
YieldConfig and successfulReinvestmentDomain
The accountant receives elapsed time and bounded yield-share accumulators from the omitted yield-manager path. The reinvestment model receives the venue success flag and minted LPT amount after external pricing and execution. The proofs verify the accountant behavior that follows, not those external producers.

View specs in Lean View proofs in Lean

Learn More

More Research

Doppler Multicurve Fee Conservation

Eighteen Lean theorems preserve manager-credit backing and the carry, beneficiary-credit, or liquidity-input partition under the modeled transition premises.

for

Velora BridgeStaking Allocation Safety

In the Lean accounting model, under stated token and external-call hypotheses, allocated Velora VLR and WETH never exceed their modeled BridgeStaking balances.

for

Aragon OSx Execute Authorization

Formally verified authorization admission, ROOT-gated permission mutation, and wildcard restrictions for a pinned Aragon OSx DAO slice.

for