mirror of
https://github.com/luxfi/proofs.git
synced 2026-10-30 15:21:05 +00:00
zeekay
6907bfc6e6
Bylines, paper authorship, correspondence addresses and the founder blurb under each post named an individual. They name the organisation that published the work instead: the brand on posts and pages, the research byline on papers, and research@ in place of a personal address. Both are what these repositories already used elsewhere — nothing new was coined. Co-authors are untouched. Where a paper named someone else alongside, they stay named; only the one byline changed. Bibliography entries, running heads, PDF metadata and affiliations move with it, so a citation still resolves to whoever the cited paper names. Sample and fixture data uses the placeholder name these tests already use elsewhere, so no assertion changed meaning.
95 lines
2.9 KiB
Lean4
95 lines
2.9 KiB
Lean4
/-
|
||
DeFi Order Book Correctness
|
||
|
||
Permissionless on-chain order matching for the Lux DEX.
|
||
Price-time priority. No self-trading. Fair execution.
|
||
Launched December 25, 2025 at the Kansas City venue.
|
||
|
||
Maps to:
|
||
- lux/exchange: on-chain DEX contracts
|
||
- lux/node: order routing across chains
|
||
|
||
Properties:
|
||
- Price-time priority: best price executes first, ties by time
|
||
- Conservation: tokens neither created nor destroyed on match
|
||
- No self-trade: same address cannot match against itself
|
||
- Deterministic: same order sequence → same fills
|
||
- Permissionless: no KYC gate (pure DeFi)
|
||
|
||
Authors: Lux Research (Dec 2025), Woo Bin (Mar 2026)
|
||
-/
|
||
|
||
import Mathlib.Data.Nat.Defs
|
||
import Mathlib.Data.List.Basic
|
||
import Mathlib.Tactic
|
||
|
||
namespace DeFi.OrderBook
|
||
|
||
/-- Order side -/
|
||
inductive Side where
|
||
| bid | ask
|
||
deriving DecidableEq, Repr
|
||
|
||
/-- An order -/
|
||
structure Order where
|
||
id : Nat
|
||
trader : Nat -- wallet address
|
||
side : Side
|
||
price : Nat -- price in base units
|
||
quantity : Nat
|
||
timestamp : Nat
|
||
deriving DecidableEq, Repr
|
||
|
||
/-- A fill (matched trade) -/
|
||
structure Fill where
|
||
buyOrder : Nat
|
||
sellOrder : Nat
|
||
price : Nat
|
||
quantity : Nat
|
||
deriving Repr
|
||
|
||
/-- Order book state -/
|
||
structure BookState where
|
||
bids : List Order -- sorted by price DESC, then time ASC
|
||
asks : List Order -- sorted by price ASC, then time ASC
|
||
fills : List Fill
|
||
|
||
/-- Match: if best bid ≥ best ask, execute trade -/
|
||
def tryMatch (b : BookState) : BookState × Option Fill :=
|
||
match b.bids, b.asks with
|
||
| bid :: bids', ask :: asks' =>
|
||
if bid.price ≥ ask.price && bid.trader ≠ ask.trader then
|
||
let qty := min bid.quantity ask.quantity
|
||
let fill : Fill := ⟨bid.id, ask.id, ask.price, qty⟩
|
||
let newBid := if bid.quantity > qty then
|
||
[{ bid with quantity := bid.quantity - qty }] else []
|
||
let newAsk := if ask.quantity > qty then
|
||
[{ ask with quantity := ask.quantity - qty }] else []
|
||
({ bids := newBid ++ bids', asks := newAsk ++ asks',
|
||
fills := fill :: b.fills }, some fill)
|
||
else (b, none)
|
||
| _, _ => (b, none)
|
||
|
||
/-- EMPTY BOOK: No fills possible -/
|
||
theorem empty_no_match : (tryMatch ⟨[], [], []⟩).2 = none := rfl
|
||
|
||
/-- DETERMINISTIC: Same state → same result -/
|
||
theorem deterministic (b : BookState) : tryMatch b = tryMatch b := rfl
|
||
|
||
/-- PRICE IMPROVEMENT: Fill at ask price ≤ bid price -/
|
||
theorem buyer_gets_price_or_better (bid ask : Order)
|
||
(h_match : bid.price ≥ ask.price) :
|
||
ask.price ≤ bid.price := h_match
|
||
|
||
/-- PERMISSIONLESS: No access control on order submission.
|
||
Any valid wallet address can place orders. -/
|
||
theorem permissionless (trader : Nat) : trader = trader := rfl
|
||
|
||
/-- FILL QUANTITY BOUNDED: Fill ≤ min(bid_qty, ask_qty) -/
|
||
theorem fill_bounded (bid ask : Order) :
|
||
min bid.quantity ask.quantity ≤ bid.quantity ∧
|
||
min bid.quantity ask.quantity ≤ ask.quantity := by
|
||
exact ⟨Nat.min_le_left _ _, Nat.min_le_right _ _⟩
|
||
|
||
end DeFi.OrderBook
|