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]>
94 lines
3.2 KiB
Lean4
94 lines
3.2 KiB
Lean4
/-
|
|
Authors: Antje Worring, Zach Kelling
|
|
|
|
Experience Ledger
|
|
|
|
Content-addressed, append-only log of semantic experiences.
|
|
Stored on IPFS/Arweave with on-chain registry.
|
|
DAO-curated quality scoring.
|
|
|
|
Maps to:
|
|
- zoo/papers/experience-ledger.tex: specification
|
|
- zoo/papers/experience-ledger-dso.tex: DSO integration
|
|
- uor.foundation: content-addressing scheme
|
|
|
|
Properties:
|
|
- Append-only: experiences cannot be deleted (immutable)
|
|
- Content-addressed: hash determines identity
|
|
- DAO-curated: quality scores via governance voting
|
|
- Merkle-verified: inclusion proofs for any experience
|
|
-/
|
|
|
|
import Mathlib.Data.Nat.Defs
|
|
import Mathlib.Data.List.Basic
|
|
import Mathlib.Tactic
|
|
|
|
namespace AI.ExperienceLedger
|
|
|
|
/-- Ledger entry -/
|
|
structure Entry where
|
|
hash : Nat -- content hash (uor.foundation/{hash}/{name})
|
|
contributor : Nat -- who contributed this
|
|
timestamp : Nat -- when
|
|
qualityVotes : Nat -- DAO quality score
|
|
domain : String -- task domain
|
|
deriving DecidableEq, Repr
|
|
|
|
/-- The ledger: append-only list -/
|
|
structure Ledger where
|
|
entries : List Entry
|
|
merkleRoot : Nat -- Merkle root of all entries
|
|
|
|
/-- Append an entry (the only mutation) -/
|
|
def append (l : Ledger) (e : Entry) : Ledger :=
|
|
{ entries := e :: l.entries
|
|
, merkleRoot := l.merkleRoot + e.hash } -- simplified Merkle update
|
|
|
|
/-- APPEND-ONLY: Ledger only grows -/
|
|
theorem append_grows (l : Ledger) (e : Entry) :
|
|
(append l e).entries.length = l.entries.length + 1 := by
|
|
simp [append, List.length_cons]
|
|
|
|
/-- IMMUTABILITY: Old entries are preserved -/
|
|
theorem append_preserves (l : Ledger) (e : Entry) (old : Entry)
|
|
(h : old ∈ l.entries) :
|
|
old ∈ (append l e).entries := by
|
|
simp only [append, List.mem_cons]; exact Or.inr h
|
|
|
|
/-- CONTENT ADDRESSING: a ledger is content-addressed when, among its own
|
|
entries, the hash uniquely determines the entry.
|
|
|
|
NOTE: this is a *property a well-formed ledger may satisfy*, NOT a global
|
|
truth. Asserting `∀ e1 e2 : Entry, e1.hash = e2.hash → e1 = e2` as an axiom
|
|
would be UNSOUND: `Entry` carries fields (contributor, timestamp, …) beyond
|
|
`hash`, so two entries can share a hash yet differ — that axiom would let one
|
|
derive `False`. Instead we make content-addressing a hypothesis a ledger
|
|
can be shown to meet (e.g. by deduplicating on insert). -/
|
|
def ContentAddressed (l : Ledger) : Prop :=
|
|
∀ e1 ∈ l.entries, ∀ e2 ∈ l.entries, e1.hash = e2.hash → e1 = e2
|
|
|
|
/-- EMPTY LEDGER -/
|
|
def emptyLedger : Ledger := ⟨[], 0⟩
|
|
|
|
theorem empty_has_zero : emptyLedger.entries.length = 0 := rfl
|
|
|
|
/-- The empty ledger is trivially content-addressed (it has no entries). -/
|
|
theorem empty_content_addressed : ContentAddressed emptyLedger := by
|
|
intro e1 he1 _ _ _
|
|
simp [emptyLedger] at he1
|
|
|
|
/-- QUALITY MONOTONE: Votes can only be added, not removed -/
|
|
def upvote (e : Entry) : Entry :=
|
|
{ e with qualityVotes := e.qualityVotes + 1 }
|
|
|
|
theorem upvote_increases (e : Entry) :
|
|
(upvote e).qualityVotes > e.qualityVotes := by
|
|
simp only [upvote]; omega
|
|
|
|
/-- MERKLE VERIFICATION: root changes with each append -/
|
|
theorem root_changes (l : Ledger) (e : Entry) (h : e.hash > 0) :
|
|
(append l e).merkleRoot > l.merkleRoot := by
|
|
simp [append]; omega
|
|
|
|
end AI.ExperienceLedger
|