Railnet Queue Nominal Conservation

Railnet provides infrastructure for onchain asset management. Its QueryRedeemQueue matches queued share-redemption requests with asset amounts supplied by an authorized caller. Requests can settle in pieces and in different orders.

Why It Matters

A funding record can serve several requests. Each redemption consumes part of its input interval and calculates a rounded asset payout. If two requests reused the same interval, the queue could account for more payouts than that record funded.

For example, a record supplying 100 raw asset units must not contribute 120 units to the redemption ledger after several partial claims. The theorem rules out that accounting failure in the model, even when requests redeem out of order.

How This Was Modeled and Proven

We recreated the relevant Solidity functions in an executable Lean interpreter (Contract.lean), defined the accounting rule (Specs.lean), and used Lean to check its preservation across permitted inputs (Proofs.lean). The model keeps the queue's checks, branch structure, integer-floor calculations and 32-iteration redemption loop. That limit applies to one call, not to the number of calls or the length of a history.

The headline theorem, conservation_for_every_finite_history, states the invariant above for every finite sequence of calls that starts from a fresh initialization. We prove it by showing that each kind of call (demand, fulfill, redeem, resolve, retrieve) preserves a bookkeeping property that implies the invariant. A fresh queue satisfies that property, so every state reached after any number of calls, in any order and with any splitting of redemptions, satisfies it too. The same argument gives conservation_for_every_reachable_state, and nominal_conservation_all_histories is the benchmark's reference statement of the same result. A second theorem, conservation_for_callbacks, repeats the result when token transfers call back into the queue or fail partway.

The reference proof has no unfinished goals or custom axioms. Its five exported declarations use only Lean's standard axioms: propext, Classical.choice and Quot.sound. The combined Contract, Specs, Proofs and Compile build completed successfully with 3,243 jobs; the full benchmark build completed with 9,011 jobs.

git clone https://github.com/lfglabs-dev/ethereum-verification-benchmark
cd ethereum-verification-benchmark
git checkout d179132bb12d9e2eea6f1987e22c1ca797323ec5
lake build Benchmark.Cases.RailnetV2.QueryRedeemQueueV2.Proofs
lake build Benchmark.Cases.RailnetV2.QueryRedeemQueueV2.Compile

Hypotheses

The proof covers any sequence of calls after a fresh initialization. These rows are what applying it to the real contract depends on.

• assumption: the Lean model matches the Solidity

  Real-code applicability

  We translated the Solidity into Lean by hand. Lean proves the rule for that translation, but nothing checks the translation against the real code. If it differs in a way that affects the accounting, the result may not apply to the contract.

• assumption: the token behaves like a standard ERC20

  External token

  The ledger numbers match real token movement only if the token moves exactly the requested amount, with no transfer fees, rebasing or balance changes outside transfers. Under that assumption, and given our reading that fulfill pulls the funding amount and redeem sends the summed payouts, the tokens redeem sends out never exceed the tokens fulfill took in. This link is not proved in Lean.

• runtime precondition: calls pass the contract's checks

  Source-enforced operation guards

  A call only counts if it passes the contract's own checks: authorization, valid IDs, nonzero amounts and overflow-safe arithmetic. A call that fails changes nothing. These are checks in the Solidity, not trust in any outside system.

Learn More

• Benchmark PR and reproducibility notes
• Public explorer source
• Railnet documentation