mirror of
https://github.com/zooai/proofs.git
synced 2026-10-30 14:49:47 +00:00
zeekayandHanzo Dev
638fba4c90
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. Co-authored-by: Hanzo Dev <[email protected]>
70 lines
2.1 KiB
Lean4
70 lines
2.1 KiB
Lean4
/-
|
||
Authors: Antje Worring, Zoo Labs Foundation Research
|
||
|
||
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: Zoo Labs Foundation 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
|
||
intro _half fullOutput
|
||
show p.reserveY * amount / (p.reserveX + amount) ≤ p.reserveY
|
||
apply Nat.div_le_of_le_mul
|
||
calc p.reserveY * amount ≤ p.reserveY * (p.reserveX + amount) :=
|
||
Nat.mul_le_mul_left _ (by omega)
|
||
_ = (p.reserveX + amount) * p.reserveY := Nat.mul_comm _ _
|
||
|
||
/-- 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
|