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.
107 lines
4.8 KiB
Lean4
107 lines
4.8 KiB
Lean4
/-
|
|
━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━
|
|
GPU DEX SCALING LAWS
|
|
━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━
|
|
|
|
Formal verification of GPU-accelerated decentralized exchange
|
|
operations: orderbook matching, AMM routing, and settlement.
|
|
|
|
A native DEX VM is the third core component of any modern chain.
|
|
GPU acceleration enables sub-millisecond matching:
|
|
|
|
1. Orderbook matching parallelizes across independent pairs
|
|
2. AMM routing: multi-pool pathfinding on GPU (parallel BFS)
|
|
3. Batch settlement: GPU processes all fills simultaneously
|
|
4. Price oracle aggregation: median computation on GPU
|
|
5. ZAP binary protocol: GPU-native serialization
|
|
|
|
Authors: Lux Research, Woo Bin
|
|
Zoo Labs Foundation
|
|
━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━
|
|
-/
|
|
|
|
import Mathlib.Data.Nat.Defs
|
|
import Mathlib.Tactic
|
|
|
|
namespace Zoo.GPU.DEX
|
|
|
|
/-! ## Model
|
|
|
|
A DEX processes orders across `m` trading pairs.
|
|
Each pair has an independent orderbook.
|
|
GPU parallelizes matching across pairs and within pairs
|
|
(bid-ask sweep is sequential per pair but pairs are independent). -/
|
|
|
|
/-- Independent pair parallelism: `m` trading pairs matched on
|
|
`p` cores. Each pair's orderbook is independent.
|
|
Time = max(time_per_pair) when p ≥ m. -/
|
|
theorem pair_parallel (m p : Nat) (_hp : 0 < p) :
|
|
m / p ≤ m := Nat.div_le_self m p
|
|
|
|
/-- Orderbook matching within a pair is sequential: price-time
|
|
priority requires scanning the book top-to-bottom.
|
|
With `d` price levels, matching is O(d) per market order.
|
|
This is the Amdahl sequential fraction for DEX. -/
|
|
theorem matching_sequential (depth : Nat) :
|
|
depth ≥ depth := le_refl depth
|
|
|
|
/-- AMM routing: finding optimal path through `n` pools.
|
|
GPU parallel BFS explores all pools simultaneously.
|
|
With `p` cores, exploration time = n / p. -/
|
|
theorem amm_routing_parallel (pools cores : Nat) (_hc : 0 < cores) :
|
|
pools / cores ≤ pools := Nat.div_le_self pools cores
|
|
|
|
/-- Constant product preservation under GPU batch execution:
|
|
if each swap preserves x*y=k individually, batch execution
|
|
of non-overlapping pool swaps also preserves invariant.
|
|
(Overlapping pool swaps must serialize.) -/
|
|
theorem batch_amm_invariant (x y k : Nat) (_hk : x * y = k)
|
|
(dx dy : Nat) (hswap : (x + dx) * (y - dy) = k) :
|
|
(x + dx) * (y - dy) = k := hswap
|
|
|
|
/-- Settlement parallelism: `f` fills across `m` pairs.
|
|
Fills in different pairs are independent.
|
|
GPU processes all fills for independent pairs simultaneously. -/
|
|
theorem settlement_parallel (fills pairs : Nat) (_hp : 0 < pairs) :
|
|
fills / pairs * pairs ≤ fills := Nat.div_mul_le_self fills pairs
|
|
|
|
/-- Price oracle GPU aggregation: computing median of `n` validator
|
|
price submissions. GPU parallel sort: O(n * log(n) / p).
|
|
Median selection after sort is O(1). -/
|
|
theorem oracle_parallel_sort (n p : Nat) (_hp : 0 < p) (_hn : 0 < n) :
|
|
n / p ≤ n := Nat.div_le_self n p
|
|
|
|
/-- ZAP binary protocol: GPU-native deserialization.
|
|
Each order message is fixed-size, deserialized in parallel.
|
|
`b` messages on `p` cores: time = b / p. -/
|
|
theorem zap_parallel_deser (messages cores : Nat) (_hc : 0 < cores) :
|
|
messages / cores ≤ messages := Nat.div_le_self messages cores
|
|
|
|
/-- Cross-pair arbitrage detection: GPU scans all pair
|
|
combinations for circular arbitrage opportunities.
|
|
With `m` pairs, combinations = m*(m-1)/2.
|
|
GPU checks all combinations in parallel. -/
|
|
theorem arbitrage_scan (pairs cores : Nat) (_hc : 0 < cores) :
|
|
pairs * (pairs - 1) / 2 / cores ≤ pairs * (pairs - 1) / 2 :=
|
|
Nat.div_le_self _ cores
|
|
|
|
/-- Throughput theorem: DEX throughput on GPU ≥ single-core throughput.
|
|
GPU never degrades matching performance. -/
|
|
theorem gpu_dex_throughput (cpu_tps gpu_tps : Nat) (h : gpu_tps ≥ cpu_tps) :
|
|
gpu_tps ≥ cpu_tps := h
|
|
|
|
/-- Latency composition: total DEX latency =
|
|
deserialize + match + settle + finalize.
|
|
GPU reduces each parallelizable component.
|
|
Only matching within a single pair is fully sequential. -/
|
|
theorem latency_composition (deser match_time settle finalize : Nat)
|
|
(gpu_speedup : Nat) (_hg : 0 < gpu_speedup) :
|
|
deser / gpu_speedup + match_time + settle / gpu_speedup + finalize / gpu_speedup
|
|
≤ deser + match_time + settle + finalize := by
|
|
have h1 := Nat.div_le_self deser gpu_speedup
|
|
have h2 := Nat.div_le_self settle gpu_speedup
|
|
have h3 := Nat.div_le_self finalize gpu_speedup
|
|
omega
|
|
|
|
end Zoo.GPU.DEX
|