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.
83 lines
2.4 KiB
Lean4
83 lines
2.4 KiB
Lean4
/-
|
|
On-Chain DEX Governance
|
|
|
|
DAO governance for DEX parameters: fee tiers, pool weights,
|
|
listing/delisting, upgrade proposals.
|
|
|
|
Maps to:
|
|
- lux/exchange: governance contracts
|
|
- lux/node: on-chain parameter updates
|
|
|
|
Properties:
|
|
- Quorum: parameter changes require vote threshold
|
|
- Timelock: changes have mandatory delay
|
|
- Bounded: parameters stay within safe ranges
|
|
- Monotone: governance power ∝ stake
|
|
|
|
Author: Lux Research
|
|
-/
|
|
|
|
import Mathlib.Data.Nat.Defs
|
|
import Mathlib.Tactic
|
|
|
|
namespace DeFi.Governance
|
|
|
|
inductive ParamChange where
|
|
| feeUpdate (newFeeBps : Nat)
|
|
| poolWeight (poolId : Nat) (weight : Nat)
|
|
| listing (tokenAddr : Nat)
|
|
| delisting (tokenAddr : Nat)
|
|
| upgrade (implAddr : Nat)
|
|
deriving DecidableEq, Repr
|
|
|
|
structure Proposal where
|
|
change : ParamChange
|
|
proposer : Nat
|
|
votesFor : Nat
|
|
votesAgainst : Nat
|
|
quorum : Nat
|
|
timelockBlocks : Nat
|
|
proposedAt : Nat
|
|
|
|
def passes (p : Proposal) : Bool :=
|
|
p.votesFor ≥ p.quorum && p.votesFor > p.votesAgainst
|
|
|
|
def timelockMet (p : Proposal) (currentBlock : Nat) : Bool :=
|
|
currentBlock ≥ p.proposedAt + p.timelockBlocks
|
|
|
|
def canExecute (p : Proposal) (currentBlock : Nat) : Bool :=
|
|
passes p && timelockMet p currentBlock
|
|
|
|
/-- QUORUM: Below quorum → rejected -/
|
|
theorem below_quorum_fails (p : Proposal) (h : p.votesFor < p.quorum) :
|
|
passes p = false := by
|
|
simp [passes, Nat.not_le.mpr h]
|
|
|
|
/-- TIMELOCK: Too early → blocked -/
|
|
theorem early_execution_blocked (p : Proposal) (block : Nat)
|
|
(h : block < p.proposedAt + p.timelockBlocks) :
|
|
canExecute p block = false := by
|
|
simp [canExecute, timelockMet, Nat.not_le.mpr h, Bool.and_false]
|
|
|
|
/-- BOTH REQUIRED: Must pass AND timelock for execution -/
|
|
theorem both_required (p : Proposal) (block : Nat) (h : canExecute p block = true) :
|
|
passes p = true ∧ timelockMet p block = true := by
|
|
simp [canExecute, Bool.and_eq_true] at h; exact h
|
|
|
|
/-- FEE BOUNDS: Fee changes must stay reasonable (< 1%) -/
|
|
def feeInBounds (change : ParamChange) : Bool :=
|
|
match change with
|
|
| .feeUpdate fee => fee ≤ 100 -- max 1%
|
|
| _ => true
|
|
|
|
theorem fee_bounded (fee : Nat) (h : fee > 100) :
|
|
feeInBounds (.feeUpdate fee) = false := by
|
|
simp [feeInBounds, Nat.not_le.mpr h]
|
|
|
|
/-- MAJORITY: More for than against -/
|
|
theorem majority_required (p : Proposal) (h : passes p = true) :
|
|
p.votesFor > p.votesAgainst := by
|
|
simp [passes, Bool.and_eq_true, Nat.ble_eq] at h; exact h.2
|
|
|
|
end DeFi.Governance
|