proofs/lean/Consensus/Liveness.lean at main

mirror of https://github.com/zooai/proofs.git synced 2026-10-30 14:49:47 +00:00

Files

T

zeekayandHanzo Dev 638fba4c90 Publish under the org, not a person

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]>

2026-09-01 08:58:14 -07:00

186 lines

7.7 KiB

Lean4

Raw Permalink Blame History

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

 /-
   Authors: Antje Worring, Zoo Labs Foundation Research
   Consensus Liveness Proof
   Theorem: Under partial synchrony with f < n/3 Byzantine nodes,
   consensus eventually finalizes a value.
   Maps to Go code:
   - protocol/wave/wave.go: Wave.Tick loop (rounds advance)
   - protocol/ray/ray.go: Ray.Driver.run (linear chain progress)
   - protocol/wave/fpc/fpc.go: FPC theta selection ensures non-degenerate thresholds
   The argument:
 . After GST (Global Stabilization Time), all messages between honest nodes
      arrive within known bound delta.
 . Honest nodes form > 2n/3 of the network.
 . In any round after GST, a k-sample from honest-majority population will
      contain > alpha honest nodes preferring the same value (with high probability).
 . After beta consecutive such rounds, the value is finalized.
 . Expected rounds to finality = O(beta) after GST.
 -/
 import Mathlib.Data.Finset.Basic
 import Mathlib.Data.Nat.Defs
 import Mathlib.Tactic
 import Consensus.Safety
 -- The state machine is Consensus.Safety's, imported rather than restated.
 -- These declarations were duplicated here with the note that they "mirror"
 -- Safety's; mirrored types are distinct types, so the two modules could not
 -- be loaded together and the liveness theorem was stated over its own copy.
 namespace Consensus.Liveness
 open Consensus
 /-- Network timing model -/
 structure NetworkModel where
   gst   : Nat    -- Global Stabilization Time (round number)
   delta : Nat    -- max message delay after GST (in rounds)
 /-- A round is synchronous if it occurs after GST -/
 def isSynchronous (nm : NetworkModel) (round : Nat) : Prop :=
   round ≥ nm.gst
 /-- State trace: sequence of consensus states indexed by round. -/
 abbrev StateTrace (p : Params) := Nat → ConsensusState p
 /-- All honest nodes can communicate within delta after GST -/
 axiom post_gst_delivery :
   ∀ (p : Params) (nm : NetworkModel) (trace : StateTrace p) (r : Nat),
     isSynchronous nm r →
     -- Messages sent in round r arrive by round r + nm.delta
     -- All honest nodes at round r+delta have consistent state with round r senders
     ∀ (i j : Fin p.n),
       isHonest (trace r) i →
       isHonest (trace (r + nm.delta)) j →
       ((trace r).nodes i).preference = ((trace (r + nm.delta)).nodes j).preference ∨
       ((trace r).nodes i).preference = none
 /-- After GST, honest majority dominates any k-sample -/
 axiom honest_sample_dominance :
   ∀ (p : Params) (nm : NetworkModel) (trace : StateTrace p) (r : Nat),
     isSynchronous nm r →
     honestCount (trace r) > 2 * p.f →
     -- A random k-sample of size p.k contains > p.alpha honest nodes
     -- preferring the majority value (w.h.p. for k >= 20)
     ∀ (v : ValueId),
       honestPreferring (trace r) v > p.alpha →
       honestPreferring (trace (r + 1)) v > p.alpha
 /-
   Authors: Antje Worring, Zoo Labs Foundation Research
   If honest nodes have a common preference after GST,
   they accumulate confidence monotonically.
 -/
 axiom confidence_accumulation :
   ∀ (p : Params) (nm : NetworkModel) (trace : StateTrace p)
     (r : Nat) (i : Fin p.n) (v : ValueId),
     isSynchronous nm r →
     isHonest (trace r) i →
     ((trace r).nodes i).preference = some v →
     honestPreferring (trace r) v > p.alpha →
     -- Confidence increments (maps to wave.go:159: state.Count++)
     ((trace (r + 1)).nodes i).confidence > ((trace r).nodes i).confidence
 /-- When confidence reaches beta, finalization occurs.
     Maps to wave.go:161-163: if state.Count >= p.Beta { decide(item) } -/
 axiom beta_triggers_finalization :
   ∀ (p : Params) (trace : StateTrace p) (r : Nat) (i : Fin p.n) (v : ValueId),
     isHonest (trace r) i →
     ((trace r).nodes i).preference = some v →
     ((trace r).nodes i).confidence ≥ p.beta →
     hasFinalized (trace r) i v
 /-- After GST, honest nodes exist (BFT assumption ensures > 2f honest) -/
 axiom honest_node_exists :
   ∀ (p : Params) (s : ConsensusState p),
     honestCount s > 2 * p.f →
     ∃ (i : Fin p.n), isHonest s i ∧ (s.nodes i).preference ≠ none
 /-- Honest/Byzantine assignment is static across the trace: a node that is
     honest at one round is honest at every round (the adversary is fixed at
     the start of an epoch). Maps to the fixed validator set per epoch. -/
 axiom honesty_static :
   ∀ (p : Params) (trace : StateTrace p) (r r' : Nat) (i : Fin p.n),
     isHonest (trace r) i → isHonest (trace r') i
 /-- Preference stability: honest nodes with sustained majority keep their preference.
     Maps to wave.go: preference only changes on confidence reset. -/
 axiom preference_stable_under_majority :
   ∀ (p : Params) (trace : StateTrace p) (r : Nat) (i : Fin p.n) (v : ValueId),
     isHonest (trace r) i →
     ((trace r).nodes i).preference = some v →
     honestPreferring (trace r) v > p.alpha →
     ((trace (r + 1)).nodes i).preference = some v
 /-- Preference stability over multiple rounds -/
 axiom preference_stable_sustained :
   ∀ (p : Params) (trace : StateTrace p)
     (r₀ steps : Nat) (i : Fin p.n) (v : ValueId),
     isHonest (trace r₀) i →
     ((trace r₀).nodes i).preference = some v →
     (∀ r, r₀ ≤ r → r < r₀ + steps → honestPreferring (trace r) v > p.alpha) →
     ((trace (r₀ + steps)).nodes i).preference = some v
 /-- Confidence reaches beta after beta rounds of sustained majority.
     Combines confidence_accumulation over beta steps. -/
 axiom sustained_confidence :
   ∀ (p : Params) (nm : NetworkModel) (trace : StateTrace p)
     (r₀ : Nat) (i : Fin p.n) (v : ValueId),
     (∀ r, r₀ ≤ r → r < r₀ + p.beta → isSynchronous nm r) →
     isHonest (trace r₀) i →
     ((trace r₀).nodes i).preference = some v →
     (∀ r, r₀ ≤ r → r < r₀ + p.beta → honestPreferring (trace r) v > p.alpha) →
     ((trace (r₀ + p.beta)).nodes i).confidence ≥ p.beta
 /--
   Main Liveness Theorem
   After GST, if honest nodes have > 2f count and a common preference exists,
   finalization occurs within beta + delta rounds.
   Derived from: sustained_confidence + beta_triggers_finalization.
 -/
 theorem liveness
     (p : Params)
     (nm : NetworkModel)
     (trace : StateTrace p)
     (r₀ : Nat)
     (v : ValueId)
     (_hsync : isSynchronous nm r₀)
     (_hbft : honestCount (trace r₀) > 2 * p.f)
     (hpref : honestPreferring (trace r₀) v > p.alpha)
     -- Additional: synchrony persists and majority sustains
     (hsync_sustained : ∀ r, r₀ ≤ r → r < r₀ + p.beta → isSynchronous nm r)
     (hmaj_sustained : ∀ r, r₀ ≤ r → r < r₀ + p.beta → honestPreferring (trace r) v > p.alpha)
     : ∃ (r : Nat) (i : Fin p.n),
         r ≤ r₀ + p.beta + nm.delta ∧
         isHonest (trace r) i ∧
         hasFinalized (trace r) i v := by
   -- The majority is over the *target* value v, so the witnessing honest node
   -- must itself prefer v. Extract it from the nonempty filtered set underlying
   -- `honestPreferring (trace r₀) v`.
   have hne : (Finset.filter
       (fun i => ((trace r₀).nodes i).honest = true ∧ ((trace r₀).nodes i).preference = some v)
       Finset.univ).Nonempty := by
     rw [← Finset.card_pos]
     exact Nat.lt_of_le_of_lt (Nat.zero_le _) hpref
   obtain ⟨i, hi_mem⟩ := hne
   rw [Finset.mem_filter] at hi_mem
   obtain ⟨_, hi_honest, hv⟩ := hi_mem
   -- `i` is honest at r₀ and prefers v; honesty persists to round r₀ + p.beta.
   have hi_honest_late : isHonest (trace (r₀ + p.beta)) i :=
     honesty_static p trace r₀ (r₀ + p.beta) i hi_honest
   refine ⟨r₀ + p.beta, i, ?_, hi_honest_late, ?_⟩
   · omega
   · exact beta_triggers_finalization p trace (r₀ + p.beta) i v
       hi_honest_late
       (preference_stable_sustained p trace r₀ p.beta i v hi_honest hv hmaj_sustained)
       (sustained_confidence p nm trace r₀ i v hsync_sustained hi_honest hv hmaj_sustained)
 end Consensus.Liveness

186 lines 7.7 KiB Lean4 Raw Permalink Blame History Unescape Escape

186 lines

7.7 KiB

Lean4

Raw Permalink Blame History