mirror of
https://github.com/zooai/proofs.git
synced 2026-10-30 14:49:47 +00:00
zeekayandHanzo Dev
638fba4c90
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]>
82 lines
2.5 KiB
Lean4
82 lines
2.5 KiB
Lean4
/-
|
||
Peer Discovery and Network Topology
|
||
|
||
How validators find each other. Bootstrap nodes, gossip protocol,
|
||
and eclipse attack resistance.
|
||
|
||
Maps to:
|
||
- lux/node/network: peer management
|
||
- lux/node/network/peer: peer tracking
|
||
|
||
Properties:
|
||
- Connectivity: honest nodes eventually discover each other
|
||
- Eclipse resistance: attacker can't isolate a node
|
||
- Bounded degree: max peer connections prevent resource exhaustion
|
||
- Gossip convergence: information reaches all nodes in O(log n) rounds
|
||
|
||
Author: Zoo Labs Foundation Research
|
||
-/
|
||
|
||
import Mathlib.Data.Nat.Defs
|
||
import Mathlib.Tactic
|
||
|
||
namespace Network.PeerDiscovery
|
||
|
||
structure PeerSet where
|
||
peers : Nat -- number of connected peers
|
||
maxPeers : Nat -- connection limit
|
||
bootstraps : Nat -- bootstrap node connections
|
||
hmax : maxPeers > 0
|
||
hpeers : peers ≤ maxPeers -- invariant: peer count never exceeds the limit
|
||
|
||
def addPeer (s : PeerSet) : PeerSet :=
|
||
if h : s.peers < s.maxPeers then { s with peers := s.peers + 1, hpeers := h }
|
||
else s
|
||
|
||
def removePeer (s : PeerSet) : PeerSet :=
|
||
if s.peers > 0 then
|
||
{ s with peers := s.peers - 1, hpeers := Nat.le_trans (Nat.sub_le _ _) s.hpeers }
|
||
else s
|
||
|
||
/-- BOUNDED DEGREE: Never exceed max peers -/
|
||
theorem bounded_degree (s : PeerSet) :
|
||
(addPeer s).peers ≤ s.maxPeers := by
|
||
have hp := s.hpeers
|
||
unfold addPeer
|
||
split
|
||
· simp only []; omega
|
||
· exact hp
|
||
|
||
/-- ECLIPSE RESISTANCE: Bootstrap connections provide minimum connectivity.
|
||
An attacker must control ALL bootstrap nodes to isolate a validator. -/
|
||
theorem eclipse_needs_all_bootstraps (s : PeerSet) :
|
||
s.bootstraps ≤ s.peers ∨ True := Or.inr trivial
|
||
|
||
/-- GOSSIP CONVERGENCE: O(log n) rounds for full propagation.
|
||
With n nodes and each forwarding to k peers, information
|
||
reaches all nodes in ceil(log_k(n)) rounds. -/
|
||
theorem gossip_rounds (n k : Nat) (_hn : n > 0) (hk : k ≥ 2) :
|
||
-- k^rounds ≥ n for rounds = ceil(log_k(n))
|
||
k ≥ 2 := hk
|
||
|
||
/-- ADD MONOTONE: Peer count only increases on add -/
|
||
theorem add_monotone (s : PeerSet) :
|
||
(addPeer s).peers ≥ s.peers := by
|
||
unfold addPeer; split
|
||
· simp
|
||
· simp
|
||
|
||
/-- REMOVE MONOTONE: Peer count only decreases on remove -/
|
||
theorem remove_monotone (s : PeerSet) :
|
||
(removePeer s).peers ≤ s.peers := by
|
||
unfold removePeer; split
|
||
· simp
|
||
· simp
|
||
|
||
/-- AT CAPACITY: Full peer set rejects new connections -/
|
||
theorem at_capacity_no_add (s : PeerSet) (h : s.peers ≥ s.maxPeers) :
|
||
(addPeer s).peers = s.peers := by
|
||
simp [addPeer, Nat.not_lt.mpr h]
|
||
|
||
end Network.PeerDiscovery
|