mirror of
https://github.com/zooai/proofs.git
synced 2026-10-30 14:49:47 +00:00
zooqueenandHanzo Dev
d3bff5e2dc
The lean/ proof library (88 files) had ~180 type-check errors across ~45 files plus 31 proof-by-assumption axiom cheats. It now type-checks cleanly under Lean 4.14.0 + Mathlib, with every theorem genuinely proven from definitions. Errors fixed: - Stale Mathlib imports: Data.Nat.Basic / Data.Int.Basic were removed this rev -> Data.Nat.Defs / Data.Int.Defs (57 files). - Shared AI/Agent/Governance/Contract/DeFi/Ecology draft files: same proof-rot as the zoo-labs sibling library (now reconciled): omega missing in-scope bounds, dead tactics after simp, simp over-reduction, doc-comment placement, reserved-word binders, deriving Repr on Finset-bearing structs, noncomputable defs over opaque primitives. - Consensus/Liveness: collapsed a 74-error cascade (undefined shared state model inlined from Safety.lean; the |>. pipe-projection vs comparison parse trap on 14 lines rewritten to explicit dot projection). - Crypto (BLS/FROST/Corona/Hybrid/threshold/FHE), Consensus, Protocol, Warp, Trust, GPU, Compute, Network, DeFi: brought structure invariants into scope for omega, Nat-division bounds via Nat.div_le_of_le_mul / Nat.div_mul_le_self, noncomputable over opaque crypto ops, deriving Inhabited for index access. Integrity: - Removed all 31 `theorem X := X_ax` cheats (axiom asserting the identical statement) and proved each from definitions; removed the UNSOUND content_addressed axiom (hash-injectivity over a struct with free fields). - Quorum-intersection theorems (BFT/Quasar/Flare/Warp/BLS/GPU/Bridge): the draft hypothesis 3f<n is insufficient (n unbounded above makes them false); tightened to the optimal-resilience invariant n=3f+1 / 2t>n. Statement intent preserved. - Net axiom change: -35 / +1 (the one addition, honesty_static, is a fixed-validator-set modeling assumption matching sibling files). - Remaining axioms are trusted-base only: opaque crypto primitives (groups, pairings, hardness, hashes, FHE encrypt/decrypt, BLS soundness, forward secrecy, Fisher-Yates uniformity) and protocol modeling assumptions. No sorry/admit/native_decide. Verified all theorems trace to [propext, Classical.choice, Quot.sound] plus those primitives. Co-authored-by: Hanzo Dev <[email protected]>
119 lines
3.9 KiB
Lean4
119 lines
3.9 KiB
Lean4
/-
|
|
Authors: Antje Worring, Zach Kelling
|
|
|
|
Compensation Fairness Properties
|
|
|
|
Compensation flows from the DAO treasury to contributors
|
|
based on attested contributions. Fairness means:
|
|
- Proportional to weight
|
|
- No single contributor can drain treasury
|
|
- Threshold approval required for distributions
|
|
|
|
Maps to:
|
|
- zoo/zoo.vote: DAO voting + treasury management
|
|
- lux/threshold: multi-sig payout authorization
|
|
- zoo/ZIPs: governance proposals for compensation standards
|
|
|
|
Properties:
|
|
- Proportionality: payout ∝ weight / totalWeight
|
|
- Bounded: no single payout exceeds treasury
|
|
- Threshold: distribution requires t-of-n approval
|
|
- Conservation: payouts ≤ treasury balance
|
|
-/
|
|
|
|
import Mathlib.Data.Nat.Defs
|
|
import Mathlib.Tactic
|
|
|
|
namespace Governance.Compensation
|
|
|
|
/-- Treasury state -/
|
|
structure Treasury where
|
|
balance : Nat
|
|
totalDistributed : Nat
|
|
deriving DecidableEq, Repr
|
|
|
|
/-- A payout request -/
|
|
structure PayoutRequest where
|
|
recipient : Nat
|
|
amount : Nat
|
|
weight : Nat -- from SBOM+ contribution weight
|
|
totalWeight : Nat -- sum of all weights in this distribution
|
|
approvals : Nat -- number of threshold approvals
|
|
threshold : Nat -- required t-of-n
|
|
|
|
/-- Payout is authorized iff threshold met and within balance -/
|
|
def isAuthorized (t : Treasury) (p : PayoutRequest) : Bool :=
|
|
p.approvals ≥ p.threshold && p.amount ≤ t.balance
|
|
|
|
/-- Execute payout -/
|
|
def executePayout (t : Treasury) (p : PayoutRequest) : Treasury :=
|
|
if isAuthorized t p then
|
|
{ balance := t.balance - p.amount
|
|
, totalDistributed := t.totalDistributed + p.amount }
|
|
else t
|
|
|
|
/-- CONSERVATION: payout never exceeds treasury -/
|
|
theorem payout_conserves (t : Treasury) (p : PayoutRequest) :
|
|
(executePayout t p).balance ≤ t.balance := by
|
|
unfold executePayout
|
|
split <;> simp
|
|
|
|
/-- CONSERVATION: total assets are preserved -/
|
|
theorem total_preserved (t : Treasury) (p : PayoutRequest) :
|
|
(executePayout t p).balance + (executePayout t p).totalDistributed =
|
|
t.balance + t.totalDistributed := by
|
|
unfold executePayout
|
|
split
|
|
· next h =>
|
|
simp only [isAuthorized, Bool.and_eq_true, decide_eq_true_eq] at h
|
|
simp only []
|
|
omega
|
|
· rfl
|
|
|
|
/-- THRESHOLD: insufficient approvals block payout -/
|
|
theorem insufficient_approvals_blocked (t : Treasury) (p : PayoutRequest)
|
|
(h : p.approvals < p.threshold) :
|
|
executePayout t p = t := by
|
|
simp [executePayout, isAuthorized, Nat.not_le.mpr h]
|
|
|
|
/-- THRESHOLD: overdrawn payout blocked -/
|
|
theorem overdrawn_blocked (t : Treasury) (p : PayoutRequest)
|
|
(h : p.amount > t.balance) :
|
|
executePayout t p = t := by
|
|
simp [executePayout, isAuthorized]
|
|
intro h_approvals
|
|
simp [Nat.not_le.mpr h, Bool.and_false]
|
|
|
|
/-- PROPORTIONALITY: if weight is 0, payout should be 0 -/
|
|
def proportionalAmount (totalPayout weight totalWeight : Nat) : Nat :=
|
|
if totalWeight = 0 then 0
|
|
else totalPayout * weight / totalWeight
|
|
|
|
theorem zero_weight_zero_payout (totalPayout totalWeight : Nat) :
|
|
proportionalAmount totalPayout 0 totalWeight = 0 := by
|
|
simp [proportionalAmount]
|
|
|
|
/-- BOUNDED: proportional amount ≤ total payout -/
|
|
theorem proportional_bounded (totalPayout weight totalWeight : Nat)
|
|
(hw : weight ≤ totalWeight) :
|
|
proportionalAmount totalPayout weight totalWeight ≤ totalPayout := by
|
|
simp only [proportionalAmount]
|
|
split
|
|
· omega
|
|
· apply Nat.div_le_of_le_mul
|
|
calc totalPayout * weight ≤ totalPayout * totalWeight := Nat.mul_le_mul_left _ hw
|
|
_ = totalWeight * totalPayout := Nat.mul_comm _ _
|
|
|
|
/-- FAIRNESS: equal weight → equal payout -/
|
|
theorem equal_weight_equal_payout (totalPayout w totalWeight : Nat) :
|
|
proportionalAmount totalPayout w totalWeight =
|
|
proportionalAmount totalPayout w totalWeight := rfl
|
|
|
|
/-- Empty treasury blocks all payouts -/
|
|
theorem empty_treasury_blocks (p : PayoutRequest) (h : p.amount > 0) :
|
|
isAuthorized ⟨0, 0⟩ p = false := by
|
|
simp [isAuthorized]
|
|
omega
|
|
|
|
end Governance.Compensation
|