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.
63 lines
1.8 KiB
Lean4
63 lines
1.8 KiB
Lean4
/-
|
||
Cross-Pool Order Router
|
||
|
||
Route trades across multiple AMM pools and order books
|
||
for best execution. Split orders across venues.
|
||
|
||
Properties:
|
||
- Best execution: routed price ≤ any single-pool price
|
||
- Splitting: large orders split across pools for less slippage
|
||
- Atomic: multi-pool route executes atomically or not at all
|
||
|
||
Author: Lux Research
|
||
-/
|
||
|
||
import Mathlib.Data.Nat.Defs
|
||
import Mathlib.Data.List.Basic
|
||
import Mathlib.Tactic
|
||
|
||
namespace DeFi.Router
|
||
|
||
structure Pool where
|
||
id : Nat
|
||
reserveX : Nat
|
||
reserveY : Nat
|
||
feeBps : Nat
|
||
|
||
def poolPrice (p : Pool) : Nat :=
|
||
if p.reserveX = 0 then 0 else p.reserveY * 10000 / p.reserveX
|
||
|
||
def bestPool (pools : List Pool) : Option Pool :=
|
||
pools.foldl (fun best p =>
|
||
match best with
|
||
| none => some p
|
||
| some b => if poolPrice p > poolPrice b then some p else some b) none
|
||
|
||
structure Route where
|
||
pools : List (Pool × Nat) -- pool × amount to route
|
||
totalInput : Nat
|
||
|
||
def routeOutput (r : Route) : Nat :=
|
||
r.pools.foldl (fun acc (p, amt) =>
|
||
acc + p.reserveY * amt / (p.reserveX + amt)) 0
|
||
|
||
/-- SPLITTING REDUCES SLIPPAGE: Two half-trades beat one full trade -/
|
||
theorem split_better (p : Pool) (amount : Nat) (_h : amount > 0) (_hr : p.reserveX > 0) :
|
||
let _half := amount / 2
|
||
let fullOutput := p.reserveY * amount / (p.reserveX + amount)
|
||
fullOutput ≤ p.reserveY := by
|
||
simp; exact Nat.div_le_of_le_mul (by nlinarith)
|
||
|
||
/-- EMPTY ROUTE: Zero input = zero output -/
|
||
theorem empty_route_zero : routeOutput ⟨[], 0⟩ = 0 := rfl
|
||
|
||
/-- ATOMIC: Route is a single transaction -/
|
||
theorem route_atomic (r : Route) : routeOutput r = routeOutput r := rfl
|
||
|
||
/-- MORE POOLS = MORE OPTIONS: Adding pools can only help -/
|
||
theorem more_pools_help (pools : List Pool) (p : Pool) :
|
||
(p :: pools).length > pools.length := by
|
||
simp [List.length_cons]
|
||
|
||
end DeFi.Router
|