Rootstock Flyover Quote Lifecycle

\texttt{completed}(s\prime,q)=1

completed s' q
The quote is marked complete after a successful refund path.

\;\land\;

\texttt{registered}(s\prime,q)=0

registered s' q
The quote registration flag is cleared, so the same quote cannot be settled again.

\;\land\;

\texttt{lpQuoteAmountAssigned}\;\vee\;\texttt{userQuoteAmountAssigned}

lpQuoteAmountAssigned / userQuoteAmountAssigned
The Lean helpers state that the registered amount is assigned by direct payment or fallback balance.

A Rootstock Flyover peg-out quote can settle its registered RBTC amount once, either by direct transfer or by recipient fallback balance, while the collateral-slash call input is accounted separately.

View Lean

Rootstock Flyover lets liquidity providers front liquidity for bridge users. In the peg-out flow, a user locks RBTC on Rootstock, an LP pays the user on Bitcoin, and the Rootstock Liquidity Bridge Contract later settles the accepted quote.

Why It Matters

Rootstock Flyover lets liquidity providers speed up bridge flows by serving users before the slow side of the bridge has fully finalized. For peg-outs, the Liquidity Bridge Contract records a signed quote, accepts RBTC from the user, and later settles that quote through either the LP refund path or the user refund path.

A Flyover quote crosses several systems: signed quote data, Rootstock-side RBTC, Bitcoin transaction evidence, bridge confirmations, LP collateral, and fallback balances. The proof isolates the Rootstock accounting step where a small mistake would matter most: the registered quote amount must not disappear, be assigned twice, or be mixed with penalty collateral.

Failed direct transfers are a useful place for accounting bugs to hide. If the contract credits the wrong balance, uses the wrong recipient, or treats the fallback credit as separate from the quote settlement, RBTC can be stranded or assigned inconsistently. The invariant rules out that class of mistake for the modeled Rootstock-side settlement paths.

Peg-out quote settlement

Deposituser locks RBTC

→

Registered quote

\texttt{amount}[q]

→

One settlement

\texttt{LP}\;\text{or}\;\texttt{user}

\texttt{amount}[q] \;=\; \texttt{directPay} \;\lor\; \texttt{fallbackBalance}

Penalty collateral is a separate call input, not part of the RBTC quote amount.

How This Was Modeled and Proven

Verity is the modeling layer we use to write a small executable version of the Solidity behavior and then prove properties about that model in Lean. Here, the model keeps only the quote fields needed for Rootstock accounting: value, callFee, gasFee, and penaltyFee, plus the LP address, the user refund address, and the user-refund expiry fields. A separate quoteRegistered flag models quote existence so zero-value quotes are not confused with missing quotes.

The deposit path includes Solidity 0.8 checked-addition guards for value + callFee and the final required amount. It also models the change-refund branch: change below dustThreshold can remain, while change at or above the threshold requires the refund call to succeed.

The proof has three theorem-facing specs. The deposit theorem shows that the required amount, deposit timestamp, expiry data, and both stored recipients are recorded. The LP refund theorem reads the stored LP recipient, then proves the quote amount goes either to that direct transfer witness or to that recipient's fallback balance. The user refund theorem does the same for the stored user refund recipient after the quote has expired.

The benchmark artifacts live under Benchmark/Cases/Rootstock/FlyoverQuoteLifecycle, with the contract model in Contract.lean, the readable property in Specs.lean, and the checked theorem scripts in Proofs.lean.

Scope

This case targets PegOutContract.sol at commit 88a6d1ad64aeb3ad24e01042f4211ad8649784b9. The modeled functions are:

depositPegOut registers the required quote amount and handles change above the dust threshold.
refundPegOut settles to the LP or LP fallback balance and computes the penalty timing branch.
refundUserPegOut settles to the user refund address or user fallback balance.
_increaseBalance is represented by the recipient-keyed fallback balance.

Out of scope: EIP-712 signature verification, Bitcoin serialization, bridge precompile internals, provider registry internals, and collateral contract storage. Those checks gate successful execution but do not change the registered quote amount after the quote is accepted. The proof records the expected collateral-slash call amount, but does not prove CollateralManagement internal storage.

Proof artifacts

Contract.lean contains the source-shaped quote lifecycle model.
Specs.lean contains the deposit, LP refund, and user refund predicates.
Proofs.lean proves the benchmark target for the modeled settlement routes.
The case directory includes the compile target and generated task files.

Function	Theorem	Status
depositPegOut	depositPegOut_registers_required_amount	Proven
refundPegOut	refundPegOut_conserves_quote_amount	Proven
refundUserPegOut	refundUserPegOut_conserves_quote_amount	Proven

Verify it yourself

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

The command builds the proof target from the benchmark repository's main branch: Benchmark.Cases.Rootstock.FlyoverQuoteLifecycle.Proofs.

Assumptions

These are proof boundaries and model choices, not hidden axioms. Recipient identity is no longer assumed: deposit stores the LP and user refund addresses, and both refund proofs read those stored fields.

hRegisteredsuccessful refund starts from an accepted quote
Proofs.lean precondition
The refund theorems prove successful settlement paths. They start from a registered quote, matching the Solidity quote.lbcAddress check before a refund can proceed.
fallbackBalancemodel of _balances on failed transfer
Contract.lean / Specs.lean
Failed LP and user transfers credit the recipient address rather than the quote hash, matching Solidity _increaseBalance.
slashCallMatchesPenaltyLP penalty call input is separate accounting
Specs.lean
The model records the amount passed to the external collateral slash call. It proves the call input matches the quote penalty, but not CollateralManagement internal storage.

Learn More

1delta Caller-Address Integrity

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

for

Usual DaoCollateral Conservation

Formally verified direct swap and redeem accounting for Usual USD0 DaoCollateral.

for

Piku Redemption Fund Conservation

Formally verified fund-conservation accounting for Piku queued redemptions.

for